coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Jean-Francois Monin <jeanfrancois.monin AT rd.francetelecom.com>
- To: "J. Zhang" <j.l.zhang AT durham.ac.uk>
- Cc: "coq" <coq-club AT pauillac.inria.fr>
- Subject: Re: [Coq-Club] new question on matrix implementation on Coq
- Date: Thu, 6 Mar 2003 12:44:46 +0100
- List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>
> 2> In Coq, when doing multi pattern matching on multi cases, how to escape
> for other pattern matching we don't really need to do. For example, in this
> case, we just need to do three pattern matching, but how to give the result
> on others. In haskell, we just write like that
> Cases m1 m1 of
> a b => c1
> | a _ => c2
> | otherwise => Print "others"
>
You can use the following syntax:
Definition myfun [n,m:nat] : nat :=
Cases n m of
| O O => O
| O _ => (S O)
| _ _ => (S (S O))
end.
> Inductive matrix : nat -> nat -> Set :=
> sig : nat -> (matrix (S O) (S O))
> | vec : nat -> (n:nat)(matrix (S O) n)->(matrix (S O) (S n))
> | row : (n:nat)(matrix (S O) n)->(m:nat)(matrix m n)->(matrix (S m) n).
>
>
> Fixpoint mat_plus [m,n:nat; m1:(matrix m n)]: (m,n:nat)(matrix m n) ->
> (matrix m n) := [m,n:nat][m2:(matrix m n)]
> <[m,n,_,_:nat](matrix m n)>
> Cases m1 m2 of
> (sig a) (sig b) =>
> (sig
> (plus a b))
> | (vec a n l) (vec a' n' l') => (vec
> (plus a a') n' (mat_plus (S O) n' l l'))
> | (row n' l' m' mtr') (row n'' l'' m'' mtr'') => (row n''
> (mat_plus (S O) n'' l' l'') n'' (mat_plus (S O) m'' n'' mtr' mtr''))
> | _ _ =>
> ????
> end.
I think that the first problem to be solved is not related
to multi pattern matching, but to the fact you want
the two matrices to have the same dimensions.
This can be done using Inversion, as in your next message,
but the following definition is more direct and probably
easier to use when doing proofs. Matrices are considered
as special cases of vectors.
Section vec.
Variable A:Set.
Inductive vector: nat -> Set :=
| Vnil : (vector O)
| Vcons : (a:A) (n:nat) (vector n) -> (vector (S n)).
Fixpoint Vbinary [g: A->A->A; n:nat; u: (vector n)] :
(vector n) -> (vector n) :=
<[x:nat](vector x)->(vector x)>Cases u of
| Vnil => [v]v
| (Vcons x n u) =>
[v:(vector (S n))]
let k =
<[x:nat]((vector (pred x))->(vector (pred x))) ->
(vector x)>
Cases v of
| Vnil => [_]Vnil
| (Vcons y n v) => [k](Vcons (g x y) n (k v))
end
in (k (Vbinary g (pred (S n)) u))
end.
End vec.
Section mat.
Variable A:Set.
Definition matrix [m,n:nat] := (vector (vector A n) m).
Definition Mbinary [g: A->A->A; m,n:nat] :
(matrix m n) -> (matrix m n) -> (matrix m n) :=
(Vbinary (vector A n) (Vbinary A g n) m).
End mat.
Regards,
Jean-Francois
- [Coq-Club] new question on matrix implementation on Coq, J. Zhang
- Re: [Coq-Club] new question on matrix implementation on Coq, Jean-Francois Monin
Archive powered by MhonArc 2.6.16.