The Coq mailing list

[Pierre Casteran <casteran AT labri.fr>]

Bonjour Houda,

  This problem can be solve as follows.

  When some function body seems too hard to build, I try ato build it 
interactively, and look at the printed term.

Inductive fofo:nat ->nat-> Set:=
fo1:forall (n:nat), fofo n (n+2).

Inductive toto(n:nat):Set:=
to1: forall (m:nat), fofo m n -> toto n.

Definition extractInt (n:nat)(pf:toto n):nat:=
match pf with
to1 m _ => m
end.

Definition getProof(n:nat)(pf:toto n):fofo (extractInt n pf) n.
 destruct pf.
 simpl.
 assumption.
Qed.

Print getProof.

getProof =
fun (n : nat) (pf : toto n) =>
match pf as t return (fofo (extractInt n t) n) with
| to1 m f => f
end
     : forall (n : nat) (pf : toto n), fofo (extractInt n pf) n




:-)  :-)
Ok, the solution is in the match ... as .. return ...
construct.


In the book, Yves wrote some pages 'bout that in section "Dependent 
inductive types" (section 6.5).








Houda Anoun wrote:
> Hi everybody;
> I found problems while trying to extract sub proofs whose  type is not 
> known in a first time
> Let's take a simple example :
>
> Inductive fofo:nat ->nat-> Set:=
> fo1:forall (n:nat), fofo n (n+2).
>
> Inductive toto(n:nat):Set:=
> to1: forall (m:nat), fofo m n -> toto n.
>
> If we consider that pf is a proof of (toto n) for a natural number n, I 
> want to extract from this proof a proof of (fofo m n) that has been used 
> to prove (toto n).
> The problem is that m is unknown and has to be calculated
> The solution I found doesn't work, it's the following one:
>
> Definition extractInt (n:nat)(pf:toto n):nat:=
> match pf with
> to1 m _ => m
> end.
>
> Definition getProof(n:nat)(pf:toto n):fofo (extractInt n pf) n:=
> match pf with
> | to1 _ pf1 => pf1
> end.
>
> But it seems that there is a problem of type conversion in this solution 
> ...
> Can anyone help me to solve this...
>
> Thanks in advance
> Houda



--
Pierre Casteran,
LaBRI, Universite Bordeaux-I      |
351 Cours de la Liberation        |
F-33405 TALENCE Cedex             |
France                            |
tel : (+ 33) 5 40 00 69 31
fax : (+ 33) 5 40 00 66 69
email: Pierre . Casteran @ labri .  fr  (but whithout white space)
www: http://www.labri.fr/Perso/~casteran