feat(library/init): define quot.hrec_on and quot.hrec_on₂ based on heterogeneous equality

They are easier to use than the version with nested eq.rec's

library/init/logic.lean

@@ -60,6 +60,9 @@ namespace eq
     notation H1 ⬝ H2 := trans H1 H2
     notation H1 ▸ H2 := subst H1 H2
   end ops
+
+  protected definition drec_on {B : Πa' : A, a = a' → Type} (H₁ : a = a') (H₂ : B a (refl a)) : B a' H₁ :=
+  eq.rec (λH₁ : a = a, show B a H₁, from H₂) H₁ H₁
 end eq
 
 theorem congr {A B : Type} {f₁ f₂ : A → B} {a₁ a₂ : A} (H₁ : f₁ = f₂) (H₂ : a₁ = a₂) : f₁ a₁ = f₂ a₂ :=
@@ -154,8 +157,12 @@ namespace heq
 
   theorem of_eq_of_heq (H₁ : a = a') (H₂ : a' == b) : a == b :=
   trans (of_eq H₁) H₂
+
 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 :=
+eq.drec_on H !heq.refl
+
 theorem of_heq_true {a : Prop} (H : a == true) : a :=
 of_eq_true (heq.to_eq H)
 

library/init/quot.lean

@@ -55,7 +55,7 @@ namespace quot
   protected lemma lift_indep_pr1
     (f : Π a, B ⟦a⟧) (H : ∀ (a b : A) (p : a ≈ b), eq.rec (f a) (sound p) = f b)
     (q : quot s) : (lift (indep f) (indep_coherent f H) q).1 = q  :=
-  ind (λ a, by esimp) q
+  quot.ind (λ a, by esimp) q
 
   protected definition rec [reducible]
      (f : Π a, B ⟦a⟧) (H : ∀ (a b : A) (p : a ≈ b), eq.rec (f a) (sound p) = f b)
@@ -65,11 +65,18 @@ namespace quot
 
   protected definition rec_on [reducible]
      (q : quot s) (f : Π a, B ⟦a⟧) (H : ∀ (a b : A) (p : a ≈ b), eq.rec (f a) (sound p) = f b) : B q :=
-  rec f H q
+  quot.rec f H q
 
   protected definition rec_on_subsingleton [reducible]
      [H : ∀ a, subsingleton (B ⟦a⟧)] (q : quot s) (f : Π a, B ⟦a⟧) : B q :=
-  rec f (λ a b h, !subsingleton.elim) q
+  quot.rec f (λ a b h, !subsingleton.elim) q
+
+  protected definition hrec_on [reducible]
+     (q : quot s) (f : Π a, B ⟦a⟧) (c : ∀ (a b : A) (p : a ≈ b), f a == f b) : B q :=
+  quot.rec_on q f
+    (λ a b p, heq.to_eq (calc
+      eq.rec (f a) (sound p) == f a : eq_rec_heq
+                         ... == f b : c a b p))
   end
 
   section
@@ -80,14 +87,14 @@ namespace quot
   protected definition lift₂ [reducible]
      (f : A → B → C)(c : ∀ a₁ a₂ b₁ b₂, a₁ ≈ b₁ → a₂ ≈ b₂ → f a₁ a₂ = f b₁ b₂)
      (q₁ : quot s₁) (q₂ : quot s₂) : C :=
-  lift
+  quot.lift
     (λ a₁, lift (λ a₂, f a₁ a₂) (λ a b H, c a₁ a a₁ b (setoid.refl a₁) H) q₂)
     (λ a b H, ind (λ a', proof c a a' b a' H (setoid.refl a') qed) q₂)
     q₁
 
   protected definition lift_on₂ [reducible]
     (q₁ : quot s₁) (q₂ : quot s₂) (f : A → B → C) (c : ∀ a₁ a₂ b₁ b₂, a₁ ≈ b₁ → a₂ ≈ b₂ → f a₁ a₂ = f b₁ b₂) : C :=
-  lift₂ f c q₁ q₂
+  quot.lift₂ f c q₁ q₂
 
   protected theorem ind₂ {C : quot s₁ → quot s₂ → Prop} (H : ∀ a b, C ⟦a⟧ ⟦b⟧) (q₁ : quot s₁) (q₂ : quot s₂) : C q₁ q₂ :=
   quot.ind (λ a₁, quot.ind (λ a₂, H a₁ a₂) q₂) q₁
@@ -115,6 +122,19 @@ namespace quot
   @quot.rec_on_subsingleton _ _ _
     (λ a, quot.ind _ _)
     q₁ (λ a, quot.rec_on_subsingleton q₂ (λ b, f a b))
+
+  protected definition hrec_on₂ [reducible]
+     {C : quot s₁ → quot s₂ → Type₁} (q₁ : quot s₁) (q₂ : quot s₂)
+     (f : Π a b, C ⟦a⟧ ⟦b⟧) (c : ∀ a₁ a₂ b₁ b₂, a₁ ≈ b₁ → a₂ ≈ b₂ → f a₁ a₂ == f b₁ b₂) : C q₁ q₂:=
+  hrec_on q₁
+    (λ a, hrec_on q₂ (λ b, f a b) (λ b₁ b₂ p, c _ _ _ _ !setoid.refl p))
+    (λ a₁ a₂ p, quot.induction_on q₂
+      (λ b,
+        have aux : f a₁ b == f a₂ b, from c _ _ _ _ p !setoid.refl,
+        calc quot.hrec_on ⟦b⟧ (λ (b : B), f a₁ b) _
+                 == f a₁ b                                 : eq_rec_heq
+             ... == f a₂ b                                 : aux
+             ... == quot.hrec_on ⟦b⟧ (λ (b : B), f a₂ b) _ : eq_rec_heq))
   end
 end quot
 
@@ -122,7 +142,9 @@ attribute quot.mk                   [constructor]
 attribute quot.lift_on              [unfold-c 4]
 attribute quot.rec                  [unfold-c 6]
 attribute quot.rec_on               [unfold-c 4]
+attribute quot.hrec_on              [unfold-c 4]
 attribute quot.rec_on_subsingleton  [unfold-c 5]
 attribute quot.lift₂                [unfold-c 8]
 attribute quot.lift_on₂             [unfold-c 6]
+attribute quot.hrec_on₂             [unfold-c 6]
 attribute quot.rec_on_subsingleton₂ [unfold-c 7]

library/logic/cast.lean

@@ -42,10 +42,6 @@ namespace heq
   drec_on H !cast_eq
 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 :=
-eq.drec_on H !heq.refl
-
 section
   universe variables u v
   variables {A A' B C : Type.{u}} {P P' : A → Type.{v}} {a a' : A} {b : B}

library/logic/eq.lean

@@ -19,30 +19,27 @@ namespace eq
   theorem id_refl (H₁ : a = a) : H₁ = (eq.refl a) :=
   rfl
 
-  definition drec_on {B : Πa' : A, a = a' → Type} (H₁ : a = a') (H₂ : B a (refl a)) : B a' H₁ :=
-  eq.rec (λH₁ : a = a, show B a H₁, from H₂) H₁ H₁
-
   theorem rec_on_id {B : A → Type} (H : a = a) (b : B a) : eq.rec_on H b = b :=
   rfl
 
   theorem rec_on_constant (H : a = a') {B : Type} (b : B) : eq.rec_on H b = b :=
-  drec_on H rfl
+  eq.drec_on H rfl
 
   theorem rec_on_constant2 (H₁ : a₁ = a₂) (H₂ : a₃ = a₄) (b : B) : eq.rec_on H₁ b = eq.rec_on H₂ b :=
   rec_on_constant H₁ b ⬝ (rec_on_constant H₂ b)⁻¹
 
   theorem rec_on_irrel_arg {f : A → B} {D : B → Type} (H : a = a') (H' : f a = f a') (b : D (f a)) :
                        eq.rec_on H b = eq.rec_on H' b :=
-  drec_on H (λ(H' : f a = f a), !rec_on_id⁻¹) H'
+  eq.drec_on H (λ(H' : f a = f a), !rec_on_id⁻¹) H'
 
   theorem rec_on_irrel {a a' : A} {D : A → Type} (H H' : a = a') (b : D a) :
-      drec_on H b = drec_on H' b :=
+      eq.drec_on H b = eq.drec_on H' b :=
   proof_irrel H H' ▸ rfl
 
   theorem rec_on_compose {a b c : A} {P : A → Type} (H₁ : a = b) (H₂ : b = c)
           (u : P a) : eq.rec_on H₂ (eq.rec_on H₁ u) = eq.rec_on (trans H₁ H₂) u :=
     (show ∀ H₂ : b = c, eq.rec_on H₂ (eq.rec_on H₁ u) = eq.rec_on (trans H₁ H₂) u,
-      from drec_on H₂ (take (H₂ : b = b), rec_on_id H₂ _))
+      from eq.drec_on H₂ (take (H₂ : b = b), rec_on_id H₂ _))
     H₂
 end eq