The Coq mailing list

[Sylvain Boulme <Sylvain.Boulme AT imag.fr>]

On Mon, 31 Mar 2003, Frederic GAVA wrote:

> Bonjour,
>
> J'ai ecris cette petite axiomatization (en changeant mon ancienne) mais 
> j'ai maintenant
> des problemes " Cannot solve a second-order unification problem" et puis 
> plus tard des problemes
> de conversion de termes.
>
> Voici donc l'axiomatisation:
>
> ################################################################
>
> Require Export ProgInt.
>
> Require ZArith.
> Require Bool.
> Require Bool.Sumbool.
> Require Omega.
>
> (* ***** Parameters given by the BSMLlib library ***** *)
>
> Parameters bsp_p:unit -> Z;
>     Vector : Set -> Set;
>     at: (T:Set) (Vector T) -> (i:Z) `0<=i<(bsp_p tt)` -> T;
>     mkpar  : (T:Set) (Z -> T) -> (Vector T);
>     apply  : (T1,T2:Set) (Vector (T1 -> T2))
>                             -> (Vector T1) -> (Vector T2);
>     put    : (T:Set)(Vector (Z -> (option T)))
>                                    -> (Vector (Z -> (option T)));
>     ifat   : (T:Set) (Vector bool) -> Z -> T -> T -> T;
>     super  : (T1,T2:Set) (unit -> (Vector T1))
>       -> (unit -> (Vector T2))  -> ((Vector T1)*(Vector T2)).
>

> Pourquoi ?
> Est-ce le fait que "a" soit une preuve pour "(at Z p i Hyp_i)"
> et pas pour "root" ?
oui !

>
>
> Pour ne plus avoir ce probleme, je fais donc:
>
> Generalize (egal_reflexive ? ? ? e);Intros.
> NewInduction H.

Plus simplement:
 Generalize a; Rewrite e; Intros.

>
>
> Or "a" et "Hyp_root" sont de meme types et peuvent donc servir pour les
> meme choses.
>
> Comment maintenant prouver cette egalite ?????
> Est-ce possible ?
> Peut on remplacer "Hyp_root" partout par "a" ?
>
Non. C'est ce qui rend la manipulation des types dependants pas toujours
facile !

Dans ton cas, une solution simple consiste donc a ajouter un axiome
supplementaire dans ton axiomatisation qui dit que "at" renvoie toujours
le meme resultat, independamment des preuves qu'on lui passe.

Axiom foo:
 (T:Set; v: (Vector T); i: Z; H1,H2: ` 0<=i<(bsp_p tt)`)
       (at T v i H1)=(at T v i H2).

Cordialement,

Sylvain.
______________________________________________________________________
BOULME Sylvain, ENSIMAG-LSR     | e-mail :      
Sylvain.Boulme AT imag.fr
BP-72  38402 St-MARTIN D'HERES  | tel : 04-76-82-72-89, 06-86-24-41-70