Skip to content

HTTPS clone URL

Subversion checkout URL

You can clone with
or
.
Download ZIP
Browse files

Some lemmas on property of rewriting. It will probably be worth at

some time to provide a library stating the groupoid structure of
equality proofs.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15976 85f007b7-540e-0410-9357-904b9bb8a0f7
  • Loading branch information...
commit ab388686675f65e796b0520f7e3de4cdfe48b9b1 1 parent 7538716
herbelin authored
Showing with 22 additions and 0 deletions.
  1. +22 −0 theories/Init/Logic.v
View
22 theories/Init/Logic.v
@@ -355,12 +355,34 @@ End Logic_lemmas.
Module EqNotations.
Notation "'rew' H 'in' H'" := (eq_rect _ _ H' _ H)
(at level 10, H' at level 10).
+ Notation "'rew' [ P ] H 'in' H'" := (eq_rect _ P H' _ H)
+ (at level 10, H' at level 10).
Notation "'rew' <- H 'in' H'" := (eq_rect_r _ H' H)
(at level 10, H' at level 10).
+ Notation "'rew' <- [ P ] H 'in' H'" := (eq_rect_r P H' H)
+ (at level 10, H' at level 10).
Notation "'rew' -> H 'in' H'" := (eq_rect _ _ H' _ H)
(at level 10, H' at level 10, only parsing).
+ Notation "'rew' -> [ P ] H 'in' H'" := (eq_rect _ P H' _ H)
+ (at level 10, H' at level 10).
End EqNotations.
+Import EqNotations.
+
+Lemma rew_opp_r : forall A (P:A->Type) (x y:A) (H:x=y) (a:P y), rew H in rew <- H in a = a.
+Proof.
+intros.
+destruct H.
+reflexivity.
+Defined.
+
+Lemma rew_opp_l : forall A (P:A->Type) (x y:A) (H:x=y) (a:P x), rew <- H in rew H in a = a.
+Proof.
+intros.
+destruct H.
+reflexivity.
+Defined.
+
Theorem f_equal2 :
forall (A1 A2 B:Type) (f:A1 -> A2 -> B) (x1 y1:A1)
(x2 y2:A2), x1 = y1 -> x2 = y2 -> f x1 x2 = f y1 y2.
Please sign in to comment.
Something went wrong with that request. Please try again.