From 8ad6312764d078c052637c9870bcd7c87bda1d37 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Mon, 20 Jul 2015 14:56:50 -0700
Subject: [PATCH] feat(library/hlist): add helper eq.rec lemmas

---
 library/data/hlist.lean             | 26 +++++++++++++++-----------
 library/init/logic.lean             | 24 +++++++++++++++++++++++-
 library/init/reserved_notation.lean |  1 +
 library/logic/cast.lean             |  3 ---
 4 files changed, 39 insertions(+), 15 deletions(-)

diff --git a/library/data/hlist.lean b/library/data/hlist.lean
index 7f4d9fca4..0a92a23f4 100644
--- a/library/data/hlist.lean
+++ b/library/data/hlist.lean
@@ -5,7 +5,7 @@ Author: Leonardo de Moura
 
 Heterogeneous lists
 -/
-import data.list
+import data.list logic.cast
 open list
 
 inductive hlist {A : Type} (B : A → Type) : list A → Type :=
@@ -37,22 +37,26 @@ definition append : Π {l₁ l₂}, hlist B l₁ → hlist B l₂ → hlist B (l
 | ⌞[]⌟    l₂ nil         h₂ := h₂
 | ⌞a::l₁⌟ l₂ (cons b h₁) h₂ := cons b (append h₁ h₂)
 
-lemma append_left_nil : ∀ {l} (h : hlist B l), append nil h = h :=
+lemma append_nil_left : ∀ {l} (h : hlist B l), append nil h = h :=
 by intros; reflexivity
 
-lemma append_right_nil : ∀ {l} (h : hlist B l), append h nil == h
-| []     nil        := !heq.refl
+open eq.ops
+lemma eq_rec_on_cons : ∀ {a₁ a₂ l₁ l₂} (b : B a₁) (h : hlist B l₁) (e : a₁::l₁ = a₂::l₂),
+                         e ▹ cons b h = cons (head_eq_of_cons_eq e ▹ b) (tail_eq_of_cons_eq e ▹ h) :=
+begin
+  intros, injection e with e₁ e₂, revert e, subst a₂, subst l₂, intro e, esimp
+end
+
+lemma append_nil_right : ∀ {l} (h : hlist B l), append h nil = (list.append_nil_right l)⁻¹ ▹ h
+| []     nil        := by esimp
 | (a::l) (cons b h) :=
   begin
-    unfold append,
-    have ih  : append h nil == h, from append_right_nil h,
-    have aux : l ++ [] = l,       from list.append_nil_right l,
-    revert ih, generalize append h nil,
-    esimp [list.append], rewrite aux,
-    intro x ih,
-    rewrite [heq.to_eq ih]
+    unfold append, rewrite [append_nil_right h], xrewrite eq_rec_on_cons
   end
 
+lemma append_nil_right_heq {l} (h : hlist B l) : append h nil == h :=
+by rewrite append_nil_right; apply eq_rec_heq
+
 section get
 variables [decA : decidable_eq A]
 include decA
diff --git a/library/init/logic.lean b/library/init/logic.lean
index b180b5a80..b66783e76 100644
--- a/library/init/logic.lean
+++ b/library/init/logic.lean
@@ -64,6 +64,7 @@ namespace eq
     notation H `⁻¹` := symm H --input with \sy or \-1 or \inv
     notation H1 ⬝ H2 := trans H1 H2
     notation H1 ▸ H2 := subst H1 H2
+    notation H1 ▹ H2 := eq.rec H2 H1
   end ops
 end eq
 
@@ -165,14 +166,35 @@ namespace heq
   theorem of_eq_of_heq (H₁ : a = a') (H₂ : a' == b) : a == b :=
   trans (of_eq H₁) H₂
 
+  definition type_eq (H : a == b) : A = B :=
+  heq.rec_on H (eq.refl A)
 end heq
 
-theorem eq_rec_heq {A : Type} {P : A → Type} {a a' : A} (H : a = a') (p : P a) : eq.rec_on H p == p :=
+open eq.ops
+theorem eq_rec_heq {A : Type} {P : A → Type} {a a' : A} (H : a = a') (p : P a) : H ▹ p == p :=
 eq.drec_on H !heq.refl
 
+theorem eq_rec_of_heq_left : ∀ {A₁ A₂ : Type} {a₁ : A₁} {a₂ : A₂} (h : a₁ == a₂), heq.type_eq h ▹ a₁ = a₂
+| A A a a (heq.refl a) := rfl
+
+reveal eq.symm
+theorem eq_rec_of_heq_right : ∀ {A₁ A₂ : Type} {a₁ : A₁} {a₂ : A₂} (h : a₁ == a₂), a₁ = (heq.type_eq h)⁻¹ ▹ a₂
+| A A a a (heq.refl a) := rfl
+
+theorem heq_of_eq_rec_left {A : Type} {P : A → Type} : ∀ {a a' : A} {p₁ : P a} {p₂ : P a'} (e : a = a') (h₂ : e ▹ p₁ = p₂), p₁ == p₂
+| a a p₁ p₂ (eq.refl a) h := eq.rec_on h !heq.refl
+
+theorem heq_of_eq_rec_right {A : Type} {P : A → Type} : ∀ {a a' : A} {p₁ : P a} {p₂ : P a'} (e : a' = a) (h₂ : p₁ = e ▹ p₂), p₁ == p₂
+| a a p₁ p₂ (eq.refl a) h := eq.rec_on h !heq.refl
+
 theorem of_heq_true {a : Prop} (H : a == true) : a :=
 of_eq_true (heq.to_eq H)
 
+theorem eq_rec_compose : ∀ {A B C : Type} (p₁ : B = C) (p₂ : A = B) (a : A), p₁ ▹ (p₂ ▹ a : B) = (p₂ ⬝ p₁) ▹ a
+| A A A (eq.refl A) (eq.refl A) a := calc
+  eq.refl A ▹ eq.refl A ▹ a = eq.refl A ▹ a              : rfl
+            ...             = (eq.refl A ⬝ eq.refl A) ▹ a : {proof_irrel (eq.refl A) (eq.refl A ⬝ eq.refl A)}
+
 attribute heq.refl [refl]
 attribute heq.trans [trans]
 attribute heq.of_heq_of_eq [trans]
diff --git a/library/init/reserved_notation.lean b/library/init/reserved_notation.lean
index cbe19222a..e3c59b15f 100644
--- a/library/init/reserved_notation.lean
+++ b/library/init/reserved_notation.lean
@@ -51,6 +51,7 @@ reserve postfix `⁻¹`:std.prec.max_plus  -- input with \sy or \-1 or \inv
 
 reserve infixl `⬝`:75
 reserve infixr `▸`:75
+reserve infixr `▹`:75
 
 /- types and type constructors -/
 
diff --git a/library/logic/cast.lean b/library/logic/cast.lean
index 764ce7311..ffed5c9c7 100644
--- a/library/logic/cast.lean
+++ b/library/logic/cast.lean
@@ -29,9 +29,6 @@ namespace heq
   universe variable u
   variables {A B C : Type.{u}} {a a' : A} {b b' : B} {c : C}
 
-  definition type_eq (H : a == b) : A = B :=
-  heq.rec_on H (eq.refl A)
-
   theorem drec_on {C : Π {B : Type} (b : B), a == b → Type} (H₁ : a == b) (H₂ : C a (refl a)) :
     C b H₁ :=
   heq.rec (λ H₁ : a == a, show C a H₁, from H₂) H₁ H₁