The Coq mailing list

["Sylvain BOULM'E" <Sylvain.Boulme AT lip6.fr>]

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.