From: Andrea Asperti Date: Mon, 9 Oct 2006 11:00:31 +0000 (+0000) Subject: The two coercions sym_eq e eq_f gives BIG TROUBLES when checking composition during X-Git-Tag: 0.4.95@7852~923 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=a5ba8bfcd6ae3b5033e58792092924455cc51837;p=helm.git The two coercions sym_eq e eq_f gives BIG TROUBLES when checking composition during qed. In particular, checking composition calls unification, that calls reductions, that is problematic when there are a lot of lein in the context (as is it the case with proofs generated by TPTP: see eg GRP486-1.p.ma ) --- diff --git a/matita/library/logic/equality.ma b/matita/library/logic/equality.ma index 0561fb993..3b242c667 100644 --- a/matita/library/logic/equality.ma +++ b/matita/library/logic/equality.ma @@ -65,8 +65,15 @@ theorem eq_f: \forall A,B:Type.\forall f:A\to B. intros.elim H.apply refl_eq. qed. +theorem eq_f': \forall A,B:Type.\forall f:A\to B. +\forall x,y:A. x=y \to f y = f x. +intros.elim H.apply refl_eq. +qed. + +(* coercion cic:/matita/logic/equality/sym_eq.con. coercion cic:/matita/logic/equality/eq_f.con. +*) default "equality" cic:/matita/logic/equality/eq.ind @@ -75,7 +82,7 @@ default "equality" cic:/matita/logic/equality/eq_ind.con cic:/matita/logic/equality/eq_elim_r.con cic:/matita/logic/equality/eq_f.con - cic:/matita/logic/equality/eq_OF_eq.con. (* \x.sym (eq_f x) *) + cic:/matita/logic/equality/eq_f'.con. (* \x.sym (eq_f x) *) theorem eq_f2: \forall A,B,C:Type.\forall f:A\to B \to C. \forall x1,x2:A. \forall y1,y2:B.