From 8086ad7461e1445f1923a56e03f0423822c0637d Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sat, 9 May 2015 09:49:41 -0700 Subject: [PATCH] =?UTF-8?q?feat(library/init):=20define=20quot.hrec=5Fon?= =?UTF-8?q?=20and=20quot.hrec=5Fon=E2=82=82=20based=20on=20heterogeneous?= =?UTF-8?q?=20equality?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit They are easier to use than the version with nested eq.rec's --- library/init/logic.lean | 7 +++++++ library/init/quot.lean | 32 +++++++++++++++++++++++++++----- library/logic/cast.lean | 4 ---- library/logic/eq.lean | 11 ++++------- 4 files changed, 38 insertions(+), 16 deletions(-) diff --git a/library/init/logic.lean b/library/init/logic.lean index b5728fefc..20c5a2b64 100644 --- a/library/init/logic.lean +++ b/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) diff --git a/library/init/quot.lean b/library/init/quot.lean index cd166dcd2..66e1ab305 100644 --- a/library/init/quot.lean +++ b/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] diff --git a/library/logic/cast.lean b/library/logic/cast.lean index dc06984f9..54d48e997 100644 --- a/library/logic/cast.lean +++ b/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} diff --git a/library/logic/eq.lean b/library/logic/eq.lean index 6a00db451..a527a4c75 100644 --- a/library/logic/eq.lean +++ 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