The Coq mailing list

[Christine Paulin <paulin AT lri.fr>]

Sylvain,

Pour ce qui est de l'egalite, il est tres probable qu'elle ne soit pas
montrable, l'axiome eq_req_eq de Eqdep prend cela en compte lorsque 
T:A->Set.
En fait l'alternative est de prendre comme axiome 

Variable A:Set.
Axiom eq_refl : (x:A)(H:x=x)(H==(refl_equal A x)).

La propriete que tu cherches a montrer ainsi que l'axiome eq_rec_eq
sont alors demontrable est l'axiome d'unicite de la preuve de x=x est 
coherent avec les modeles etudies par Streicher et Hoffman.

Tranparent eq_rect.
Lemma eq_rect_eq : (T:A->Type)(x:A)(t:(T x))(H:x=x)t==(eq_rect A x T t x H).
Intros.
Rewrite (eq_refl x H); Trivial.
Save.

Lemma eq_rec_eq : (T:A->Set)(x:A)(t:(T x))(H:x=x)t=(eq_rec A x T t x H).
Intros.
Rewrite (eq_refl x H); Trivial.
Save.

Pour ce qui est de l'extensionalite, oui la solution actuelle est de
eta-expanse a la main ...

Merci du rapport de bug de l'inversion.

Christine.

In his message of Mon February 8, 1999, Sylvain BOULM'E writes: 
> 
> Bonjour,
> 
> 
> J'ai 2 petites questions (naives ?)
> 
> 1. Peut-on prouver Goal (A:Set)(T:A->Type)(x:A)(t:(T x))(H:x=x)t==(eq_rect 
> A x 
> T t x H) ?
> 
> Je sais prouver le but precedent dans lequel on remplace "eq" par 
> "identity"...
> 
> 
> Remarque : il y a un petit bug sans importance 
> Sur le but precedent,
>     Intros A T x t H; Dependent Inversion H.
> "donne" :
>   Invalid argument: "List.fold_left2".
>   If this is in user-written tactic code, then it needs to be modified.
>   If this is in system code, then it needs to be reported.
> 
> 
> Dans le cas contraire est-il raisonnable de prendre comme axiome ?
> 
>    Axiom eq_rect_idT: (A:Set)(T:A->Type)(x:A)(t:(T x))(H:x=x)t===(eq_rect A 
> x 
> T t x H).
> 
> 
> 2. Apparement il n'y a pas de regle d'eta-conversion dans Coq. Comment 
> vivre 
> sans ?
>    => Est-il raisonnable de poser un axiome :
>    Axiom eta_conv: (A:Type)(B:A->Type)(f:(x:A)(B x))f===[x:A](f x).
>    => Ou doit-on s'arranger pour reformuler ses theoremes ou axiomes.
>       Par ex:    
>         Axiom eq_rect_idT_2: 
>           (A:Set)(T:A->Type)(x:A)(t:(T x))(H:x=x)t===(eq_rect A x [x:A](T 
> x) t 
> x H)
>       Le mieux est alors de systematiquement eta-expanser ???
> 
> 
> 
> Merci,
> 
> 
> Sylvain. 

-- 
  Christine Paulin-Mohring             mailto : 
Christine.Paulin AT lri.fr
  LRI, URA 410 CNRS, Bat 490, Université Paris Sud,   91405 ORSAY Cedex 
  LRI   tel : (+33) (0)1 69 15 66 35       fax : (+33) (0)1 69 15 65 86
  INRIA tel : (+33) (0)1 39 63 54 60       fax : (+33) (0)1 39 63 56 84
  Tatoo tel : 06 04 24 44 75