The Coq mailing list

[Houda Anoun <anoun AT labri.fr>]

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

--
==============================
|      Houda ANOUN           |
|         LaBRI              |
| 351 Cours de la libération |
|      33405 Talence         |
|    phone: 0540002489       |
|  e-mail 
:anoun AT labri.fr
    |
=============================