The Coq mailing list

[casteran AT labri.fr]

Hi Houda,


   Your example looks a little too big for the post-holiday week :-)
Are you sure that this is the shortest example with the same problem?
For instance, can it be wtitten with less constructors, or without
the decidability hypothesis?

  A method for dealing with such complex examples could be trying
an interactive construction of the function you want to build.

 like :

Fixpoint getOtherDed (A:Set)(G:coucou A)(r:ress A)(d:ded G r)
    (G':coucou A):option (ded G' r).
intros A G r d; elim d.
...
Defined.

and then looking at the generated term.

About the use of "as _ return _" , there are some pages about
that in the book by Yves Bertot et al. :-)
(section 6.5 on dependent inductive
types, see also the section "Dependent Pattern Matching" in chapter 14.)


Pierre


Selon 
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.
> --------------------------------------------------------
> Bug reports: http://coq.inria.fr/bin/coq-bugs
> Archives: http://pauillac.inria.fr/pipermail/coq-club
>           http://pauillac.inria.fr/bin/wilma/coq-club
> Info: http://pauillac.inria.fr/mailman/listinfo/coq-club
>




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