The Coq mailing list

[Pierre Letouzey <Pierre.Letouzey AT lri.fr>]

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...
>

You need to help the last "match" via the "return" construction:

Definition getProof(n:nat)(pf:toto n):fofo (extractInt n pf) n:=
match pf return fofo (extractInt n pf) n with
| to1 _ pf1 => pf1
end.

You can find more documentation about the variants of "match" in Coq
Reference Manual.

Pierre Letouzey