From 2dfd262e4da86d850f3588e537b665ac2daa7ed4 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 24 Mar 2021 09:26:15 -0700 Subject: [PATCH] chore: cleanup --- src/Init/Core.lean | 113 ++++++++++++++++++++++----------------------- 1 file changed, 56 insertions(+), 57 deletions(-) diff --git a/src/Init/Core.lean b/src/Init/Core.lean index fb906f2f55..557900781b 100644 --- a/src/Init/Core.lean +++ b/src/Init/Core.lean @@ -316,16 +316,16 @@ theorem decideFalseEqFalse (h : Decidable False) : @decide False h = false := /-- Similar to `decide`, but uses an explicit instance -/ @[inline] def toBoolUsing {p : Prop} (d : Decidable p) : Bool := - @decide p d + decide p (h := d) theorem toBoolUsingEqTrue {p : Prop} (d : Decidable p) (h : p) : toBoolUsing d = true := - @decideEqTrue _ d h + decideEqTrue (s := d) h theorem ofBoolUsingEqTrue {p : Prop} {d : Decidable p} (h : toBoolUsing d = true) : p := - @ofDecideEqTrue _ d h + ofDecideEqTrue (s := d) h theorem ofBoolUsingEqFalse {p : Prop} {d : Decidable p} (h : toBoolUsing d = false) : ¬ p := - @ofDecideEqFalse _ d h + ofDecideEqFalse (s := d) h instance : Decidable True := isTrue trivial @@ -396,40 +396,39 @@ instance {p q} [Decidable p] [Decidable q] : Decidable (p ↔ q) := theorem ifPos {c : Prop} [h : Decidable c] (hc : c) {α : Sort u} {t e : α} : (ite c t e) = t := match h with - | (isTrue hc) => rfl - | (isFalse hnc) => absurd hc hnc + | isTrue hc => rfl + | isFalse hnc => absurd hc hnc theorem ifNeg {c : Prop} [h : Decidable c] (hnc : ¬c) {α : Sort u} {t e : α} : (ite c t e) = e := match h with - | (isTrue hc) => absurd hc hnc - | (isFalse hnc) => rfl + | isTrue hc => absurd hc hnc + | isFalse hnc => rfl theorem difPos {c : Prop} [h : Decidable c] (hc : c) {α : Sort u} {t : c → α} {e : ¬ c → α} : (dite c t e) = t hc := match h with - | (isTrue hc) => rfl - | (isFalse hnc) => absurd hc hnc + | isTrue hc => rfl + | isFalse hnc => absurd hc hnc theorem difNeg {c : Prop} [h : Decidable c] (hnc : ¬c) {α : Sort u} {t : c → α} {e : ¬ c → α} : (dite c t e) = e hnc := match h with - | (isTrue hc) => absurd hc hnc - | (isFalse hnc) => rfl + | isTrue hc => absurd hc hnc + | isFalse hnc => rfl -- Remark: dite and ite are "defally equal" when we ignore the proofs. theorem difEqIf (c : Prop) [h : Decidable c] {α : Sort u} (t : α) (e : α) : dite c (fun h => t) (fun h => e) = ite c t e := match h with - | (isTrue hc) => rfl - | (isFalse hnc) => rfl + | isTrue hc => rfl + | isFalse hnc => rfl instance {c t e : Prop} [dC : Decidable c] [dT : Decidable t] [dE : Decidable e] : Decidable (if c then t else e) := match dC with - | (isTrue hc) => dT - | (isFalse hc) => dE + | isTrue hc => dT + | isFalse hc => dE instance {c : Prop} {t : c → Prop} {e : ¬c → Prop} [dC : Decidable c] [dT : ∀ h, Decidable (t h)] [dE : ∀ h, Decidable (e h)] : Decidable (if h : c then t h else e h) := match dC with - | (isTrue hc) => dT hc - | (isFalse hc) => dE hc - + | isTrue hc => dT hc + | isFalse hc => dE hc /- Inhabited -/ @@ -453,8 +452,7 @@ theorem nonemptyOfExists {α : Sort u} {p : α → Prop} : Exists (fun x => p x) /- Subsingleton -/ class Subsingleton (α : Sort u) : Prop where - intro :: - allEq : (a b : α) → a = b + intro :: allEq : (a b : α) → a = b protected def Subsingleton.elim {α : Sort u} [h : Subsingleton α] : (a b : α) → a = b := h.allEq @@ -469,12 +467,12 @@ instance (p : Prop) : Subsingleton p := instance (p : Prop) : Subsingleton (Decidable p) := Subsingleton.intro fun - | (isTrue t₁) => fun - | (isTrue t₂) => proofIrrel t₁ t₂ ▸ rfl - | (isFalse f₂) => absurd t₁ f₂ - | (isFalse f₁) => fun - | (isTrue t₂) => absurd t₂ f₁ - | (isFalse f₂) => proofIrrel f₁ f₂ ▸ rfl + | isTrue t₁ => fun + | isTrue t₂ => rfl + | isFalse f₂ => absurd t₁ f₂ + | isFalse f₁ => fun + | isTrue t₂ => absurd t₂ f₁ + | isFalse f₂ => rfl theorem recSubsingleton {p : Prop} [h : Decidable p] @@ -484,8 +482,8 @@ theorem recSubsingleton [h₄ : ∀ (h : ¬p), Subsingleton (h₂ h)] : Subsingleton (Decidable.casesOn (motive := fun _ => Sort u) h h₂ h₁) := match h with - | (isTrue h) => h₃ h - | (isFalse h) => h₄ h + | isTrue h => h₃ h + | isFalse h => h₄ h structure Equivalence {α : Sort u} (r : α → α → Prop) : Prop where refl : ∀ x, r x x @@ -543,14 +541,14 @@ instance Sum.inhabitedRight [h : Inhabited β] : Inhabited (Sum α β) where instance {α : Type u} {β : Type v} [DecidableEq α] [DecidableEq β] : DecidableEq (Sum α β) := fun a b => match a, b with - | (Sum.inl a), (Sum.inl b) => + | Sum.inl a, Sum.inl b => if h : a = b then isTrue (h ▸ rfl) - else isFalse (fun h' => Sum.noConfusion h' (fun h' => absurd h' h)) - | (Sum.inr a), (Sum.inr b) => + else isFalse fun h' => Sum.noConfusion h' fun h' => absurd h' h + | Sum.inr a, Sum.inr b => if h : a = b then isTrue (h ▸ rfl) - else isFalse (fun h' => Sum.noConfusion h' (fun h' => absurd h' h)) - | (Sum.inr a), (Sum.inl b) => isFalse (fun h => Sum.noConfusion h) - | (Sum.inl a), (Sum.inr b) => isFalse (fun h => Sum.noConfusion h) + else isFalse fun h' => Sum.noConfusion h' fun h' => absurd h' h + | Sum.inr a, Sum.inl b => isFalse fun h => Sum.noConfusion h + | Sum.inl a, Sum.inr b => isFalse fun h => Sum.noConfusion h end @@ -560,16 +558,16 @@ instance [Inhabited α] [Inhabited β] : Inhabited (α × β) where default := (arbitrary, arbitrary) instance [DecidableEq α] [DecidableEq β] : DecidableEq (α × β) := - fun ⟨a, b⟩ ⟨a', b'⟩ => - match (decEq a a') with - | (isTrue e₁) => - match (decEq b b') with - | (isTrue e₂) => isTrue (e₁ ▸ e₂ ▸ rfl) - | (isFalse n₂) => isFalse (fun h => Prod.noConfusion h (fun e₁' e₂' => absurd e₂' n₂)) - | (isFalse n₁) => isFalse (fun h => Prod.noConfusion h (fun e₁' e₂' => absurd e₁' n₁)) + fun (a, b) (a', b') => + match decEq a a' with + | isTrue e₁ => + match decEq b b' with + | isTrue e₂ => isTrue (e₁ ▸ e₂ ▸ rfl) + | isFalse n₂ => isFalse fun h => Prod.noConfusion h fun e₁' e₂' => absurd e₂' n₂ + | isFalse n₁ => isFalse fun h => Prod.noConfusion h fun e₁' e₂' => absurd e₁' n₁ instance [BEq α] [BEq β] : BEq (α × β) where - beq := fun ⟨a₁, b₁⟩ ⟨a₂, b₂⟩ => a₁ == a₂ && b₁ == b₂ + beq := fun (a₁, b₁) (a₂, b₂) => a₁ == a₂ && b₁ == b₂ instance [HasLess α] [HasLess β] : HasLess (α × β) where Less s t := s.1 < t.1 ∨ (s.1 = t.1 ∧ s.2 < t.2) @@ -914,10 +912,10 @@ variable (r : α → α → Prop) instance {α : Sort u} {s : Setoid α} [d : ∀ (a b : α), Decidable (a ≈ b)] : DecidableEq (Quotient s) := fun (q₁ q₂ : Quotient s) => Quotient.recOnSubsingleton₂ (motive := fun a b => Decidable (a = b)) q₁ q₂ - (fun a₁ a₂ => - match (d a₁ a₂) with - | (isTrue h₁) => isTrue (Quotient.sound h₁) - | (isFalse h₂) => isFalse (fun h => absurd (Quotient.exact h) h₂)) + fun a₁ a₂ => + match d a₁ a₂ with + | isTrue h₁ => isTrue (Quotient.sound h₁) + | isFalse h₂ => isFalse fun h => absurd (Quotient.exact h) h₂ /- Function extensionality -/ @@ -936,8 +934,8 @@ protected theorem Equiv.trans {f₁ f₂ f₃ : ∀ (x : α), β x} : Equiv f₁ fun h₁ h₂ x => Eq.trans (h₁ x) (h₂ x) protected theorem Equiv.isEquivalence (α : Sort u) (β : α → Sort v) : Equivalence (@Function.Equiv α β) := { - refl := Equiv.refl, - symm := Equiv.symm, + refl := Equiv.refl + symm := Equiv.symm trans := Equiv.trans } @@ -964,8 +962,9 @@ theorem funext {f₁ f₂ : ∀ (x : α), β x} (h : ∀ x, f₁ x = f₂ x) : f end -instance {α : Sort u} {β : α → Sort v} [∀ a, Subsingleton (β a)] : Subsingleton (∀ a, β a) := - ⟨fun f₁ f₂ => funext (fun a => Subsingleton.elim (f₁ a) (f₂ a))⟩ +instance {α : Sort u} {β : α → Sort v} [∀ a, Subsingleton (β a)] : Subsingleton (∀ a, β a) where + allEq f₁ f₂ := + funext (fun a => Subsingleton.elim (f₁ a) (f₂ a)) /- Squash -/ @@ -979,12 +978,12 @@ theorem Squash.ind {α : Type u} {motive : Squash α → Prop} (h : ∀ (a : α) @[inline] def Squash.lift {α β} [Subsingleton β] (s : Squash α) (f : α → β) : β := Quot.lift f (fun a b _ => Subsingleton.elim _ _) s -instance {α} : Subsingleton (Squash α) := ⟨fun a b => - Squash.ind (motive := fun a => a = b) - (fun a => Squash.ind (motive := fun b => Squash.mk a = b) - (fun b => show Quot.mk _ a = Quot.mk _ b by apply Quot.sound; exact trivial) - b) - a⟩ +instance : Subsingleton (Squash α) where + allEq a b := by + induction a using Squash.ind + induction b using Squash.ind + apply Quot.sound + exact trivial namespace Lean /- Kernel reduction hints -/