The Coq mailing list

[anoun AT labri.fr]

Hi,
I usually have some technical problems using match construction.
For instance, we consider the following simpl example  :

(********************)

Set Implicit Arguments.
Inductive ress(A:Set):Set:=
|ress1:A-> ress A
|ress2:ress A->ress A->ress A
|ress3:ress A->ress A->ress A.



Inductive coucou(A:Set):Set:=
|cou1:nat ->ress A -> coucou A
|cou2:coucou A->coucou A -> coucou A.


Inductive ded(A:Set):coucou A ->ress A -> Set:=
|ded1:forall (r:ress A)(n:nat), ded (cou1 n r) r
|ded2:forall  (c1:coucou A)(r1 r2:ress A)(i:nat),
ded (cou2 c1 (cou1  i r1)) r2 ->
ded c1 (ress2 r2 r1)
|ded3:forall (c1 c2:coucou A)(r1 r2:ress A),
   ded c1 r1 -> ded c2 r2-> ded (cou2 c1 c2) (ress3 r1 r2).

Parameter eqdecRess:forall(A:Set) (r1 r2:ress A), {r1=r2}+{r1<>r2}.

Fixpoint getOtherDed (A:Set)(G:coucou A)(r:ress A)(d:ded G r)(G':coucou
A){struct d}:option (ded G' r):=
match d with
|ded1 r1 n1 =>match G' as c return (option (ded c r)) with
             |cou1  n2 r'=> match (eqdecRess r r') with
                                |left e=> Some (eq_rec_r (fun f=> (ded (cou1 
n2
r') f)) (ded1 r' n2) e)
                                |right _=>None
                         end
             |others =>None
    end
|ded2 c1 r1 r2 i D=>match (getOtherDed D (cou2 G' (cou1 0 r1))) with
                      |Some D1=>Some (ded2 D1)
                      |None =>None
                       end
|others =>None
end.

(* we got the following error!
The term
 "match getOtherDed A (cou2 c1 (cou1 i r1)) r2 D (cou2 G' (cou1 0 r1)) with
  | Some D1 => Some (ded2 D1)
  | None => None (A:=ded G' (ress2 r2 r1))
  end" has type "option (ded G' (ress2 r2 r1))"
 while it is expected to have type "option (ded G' r)" ?!*)

I can't understand this error as in the second clause where it appears we have
(B=(ress2 r2 r1))
Can anybody help me to understand this??
I have also another question concerning the key word (as _ return _) that we
sometimes use within a match construction... In this example if we ommit this
in the first clause we got an error! I want to know when we use this
instruction and what is its role??
Thanks a lot in advance

Houda

----------------------------------------------------------------
This message was sent using IMP, the Internet Messaging Program.