The Coq mailing list

[Jean-Francois Monin <jeanfrancois.monin AT rd.francetelecom.com>]

 > 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