The Coq mailing list

[Christine Paulin <paulin AT serveur3-5.lri.fr>]

What you probably want to define in 


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 in ded G r return (option (ded G' r)) with
|ded1 r1 n1 =>match G' return (option (ded G' r1)) with
             |cou1  n2 r'=> match (eqdecRess r1 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.

I will try to explain the purpose of the return clause.
In Coq pattern-matching is done on generalised inductive types as in
your example, which means that the type of each branch depends on the
constructor in the corresponding pattern. 

Assume we have an inductive family I of type A -> Set 
with one constructor C of type B -> (I t)

If c has type (I a), I can write 
        match c with (C b) => t end 

What is the type of this expression ?
In non-dependent type-theory, the type of the expression is the same
as the type of t
In dependent type theory, the type of the result may depend on 
the index of the inductive definition (in that case "a" because c has
type (I a)" and also from the term c itself.
>From the internal point of view, the match operation takes as an
argument a type family P of type forall (z:A) (x:(I z)), Set 

The match term will have type (P a c) 
and the term t in the branch should have type (P t (C b)) 

The system try to find itself a convenient type family P but it
usually fails in case you really need a dependent type.
This is the case in particular when doing a match on x with the type
of x being an inductive family (and not just an inductive type)

The general syntax of the match operation is 
        match c as x in (I z) return T with
                (C b) => t
        end
with x and z new variables
the expected predicate P will be fun (z:A) (x:I z) => T
in case T does not depend on z, you can remove the in part 
and simply write
        match c as x return T with
                (C b) => t
        end
P will be fun (z:A) (x:I z) => T
If c is already a variable you can also remove the as x part and
        simply write
        match c return T with
                (C b) => t
        end
P will be fun (z:A) (c:I z) => T

I Hope it helps understanding this particular construction. Looking at
the type of the recursor ded_rect may also help.

Christine Paulin


anoun AT labri.fr
 writes:
 > 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

-- 
  Christine Paulin-Mohring             mailto : 
Christine.Paulin AT lri.fr
  LRI, UMR 8623 CNRS, Bat 490, Université Paris Sud,   91405 ORSAY Cedex 
  tel : (+33) (0)1 69 15 66 35         fax : (+33) (0)1 69 15 65 86