From 2f6c4d91e409105aa7d1bf727f500f20dc7bdd4d Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 10 Mar 2017 14:00:55 -0800 Subject: [PATCH] feat(library/init/core): simplify proofs --- library/init/core.lean | 20 ++++++-------------- 1 file changed, 6 insertions(+), 14 deletions(-) diff --git a/library/init/core.lean b/library/init/core.lean index 87055a9e2e..5f54e0ebcc 100644 --- a/library/init/core.lean +++ b/library/init/core.lean @@ -171,31 +171,23 @@ have ∀ (α' : Sort u) (a' : α') (h₁ : @heq α a α' a') (h₂ : α = α'), show (eq.rec_on (eq.refl α) a : α) = a', from this α a' h (eq.refl α) --- The following four lemmas could not be automatically generated when the --- structures were declared, so we prove them manually here. +/- The following four lemmas could not be automatically generated when the + structures were declared, so we prove them manually here. -/ lemma prod.mk.inj {α : Type u} {β : Type v} {x₁ : α} {y₁ : β} {x₂ : α} {y₂ : β} : (x₁, y₁) = (x₂, y₂) → and (x₁ = x₂) (y₁ = y₂) := -assume (H_eq : (x₁, y₁) = (x₂, y₂)), -have H_nc : (x₁ = x₂ → y₁ = y₂ → and (x₁ = x₂) (y₁ = y₂)) → and (x₁ = x₂) (y₁ = y₂), from - @prod.no_confusion _ _ (and (x₁ = x₂) (y₁ = y₂)) _ _ H_eq, -H_nc (assume Hx Hy, and.intro Hx Hy) +λ h, prod.no_confusion h (λ h₁ h₂, ⟨h₁, h₂⟩) lemma prod.mk.inj_arrow {α : Type u} {β : Type v} {x₁ : α} {y₁ : β} {x₂ : α} {y₂ : β} : (x₁, y₁) = (x₂, y₂) → Π ⦃P : Sort w⦄, (x₁ = x₂ → y₁ = y₂ → P) → P := -assume H_eq P, -@prod.no_confusion _ _ P _ _ H_eq +λ h₁ _ h₂, prod.no_confusion h₁ h₂ lemma pprod.mk.inj {α : Sort u} {β : Sort v} {x₁ : α} {y₁ : β} {x₂ : α} {y₂ : β} : pprod.mk x₁ y₁ = pprod.mk x₂ y₂ → and (x₁ = x₂) (y₁ = y₂) := -assume (H_eq : pprod.mk x₁ y₁ = pprod.mk x₂ y₂), -have H_nc : (x₁ = x₂ → y₁ = y₂ → and (x₁ = x₂) (y₁ = y₂)) → and (x₁ = x₂) (y₁ = y₂), from - @pprod.no_confusion _ _ (and (x₁ = x₂) (y₁ = y₂)) _ _ H_eq, -H_nc (assume Hx Hy, and.intro Hx Hy) +λ h, pprod.no_confusion h (λ h₁ h₂, ⟨h₁, h₂⟩) lemma pprod.mk.inj_arrow {α : Type u} {β : Type v} {x₁ : α} {y₁ : β} {x₂ : α} {y₂ : β} : (x₁, y₁) = (x₂, y₂) → Π ⦃P : Sort w⦄, (x₁ = x₂ → y₁ = y₂ → P) → P := -assume H_eq P, -@prod.no_confusion _ _ P _ _ H_eq +λ h₁ _ h₂, prod.no_confusion h₁ h₂ inductive sum (α : Type u) (β : Type v) | inl {} : α → sum