The Coq mailing list

[Benjamin Werner <werner AT lix.polytechnique.fr>]

Hi,

You need to insert one use of eq_rec somehow.

Here is a (really) quick & dirty script :

Require Arith.

Definition getProof(n:nat)(pf:toto n):fofo (extractInt n pf) n.
intros.
inversion pf.
inversion H.
rewrite <- H1.
replace (extractInt n pf) with m.
 apply fo1.
 elim pf.
   simpl in |- *.
   induction 1.
   generalize H1; do 4 rewrite <- plus_n_Sm; do 2 rewrite <-  plus_n_O;
    simpl in |- *; injection 1; auto.
Defined.


Hope it helps,

Benjamin


On Tue, 6 Jul 2004, 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
> 
>