diff --git a/doc/examples/bintree.lean b/doc/examples/bintree.lean index 6f775d8b5d..c1cb158bc3 100644 --- a/doc/examples/bintree.lean +++ b/doc/examples/bintree.lean @@ -282,7 +282,7 @@ theorem BinTree.find_insert_of_ne (b : BinTree β) (h : k ≠ k') (v : β) let ⟨t, h⟩ := b; simp induction t with simp | leaf => - split <;> (try simp) <;> split <;> (try simp) + intros have_eq k k' contradiction | node left key value right ihl ihr => diff --git a/src/Init.lean b/src/Init.lean index 7daabd1a7b..85edb624b9 100644 --- a/src/Init.lean +++ b/src/Init.lean @@ -8,6 +8,7 @@ import Init.Prelude import Init.Notation import Init.Tactics import Init.TacticsExtra +import Init.ByCases import Init.RCases import Init.Core import Init.Control @@ -23,6 +24,7 @@ import Init.MetaTypes import Init.Meta import Init.NotationExtra import Init.SimpLemmas +import Init.PropLemmas import Init.Hints import Init.Conv import Init.Guard diff --git a/src/Init/ByCases.lean b/src/Init/ByCases.lean new file mode 100644 index 0000000000..aeb86ae0e4 --- /dev/null +++ b/src/Init/ByCases.lean @@ -0,0 +1,74 @@ +/- +Copyright (c) 2024 Lean FRO. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Leonardo de Moura, Mario Carneiro +-/ +prelude +import Init.Classical + +/-! # by_cases tactic and if-then-else support -/ + +/-- +`by_cases (h :)? p` splits the main goal into two cases, assuming `h : p` in the first branch, and `h : ¬ p` in the second branch. +-/ +syntax "by_cases " (atomic(ident " : "))? term : tactic + +macro_rules + | `(tactic| by_cases $e) => `(tactic| by_cases h : $e) +macro_rules + | `(tactic| by_cases $h : $e) => + `(tactic| open Classical in refine if $h:ident : $e then ?pos else ?neg) + +/-! ## if-then-else -/ + +@[simp] theorem if_true {h : Decidable True} (t e : α) : ite True t e = t := if_pos trivial + +@[simp] theorem if_false {h : Decidable False} (t e : α) : ite False t e = e := if_neg id + +theorem ite_id [Decidable c] {α} (t : α) : (if c then t else t) = t := by split <;> rfl + +/-- A function applied to a `dite` is a `dite` of that function applied to each of the branches. -/ +theorem apply_dite (f : α → β) (P : Prop) [Decidable P] (x : P → α) (y : ¬P → α) : + f (dite P x y) = dite P (fun h => f (x h)) (fun h => f (y h)) := by + by_cases h : P <;> simp [h] + +/-- A function applied to a `ite` is a `ite` of that function applied to each of the branches. -/ +theorem apply_ite (f : α → β) (P : Prop) [Decidable P] (x y : α) : + f (ite P x y) = ite P (f x) (f y) := + apply_dite f P (fun _ => x) (fun _ => y) + +/-- Negation of the condition `P : Prop` in a `dite` is the same as swapping the branches. -/ +@[simp] theorem dite_not (P : Prop) {_ : Decidable P} (x : ¬P → α) (y : ¬¬P → α) : + dite (¬P) x y = dite P (fun h => y (not_not_intro h)) x := by + by_cases h : P <;> simp [h] + +/-- Negation of the condition `P : Prop` in a `ite` is the same as swapping the branches. -/ +@[simp] theorem ite_not (P : Prop) {_ : Decidable P} (x y : α) : ite (¬P) x y = ite P y x := + dite_not P (fun _ => x) (fun _ => y) + +@[simp] theorem dite_eq_left_iff {P : Prop} [Decidable P] {B : ¬ P → α} : + dite P (fun _ => a) B = a ↔ ∀ h, B h = a := by + by_cases P <;> simp [*, forall_prop_of_true, forall_prop_of_false] + +@[simp] theorem dite_eq_right_iff {P : Prop} [Decidable P] {A : P → α} : + (dite P A fun _ => b) = b ↔ ∀ h, A h = b := by + by_cases P <;> simp [*, forall_prop_of_true, forall_prop_of_false] + +@[simp] theorem ite_eq_left_iff {P : Prop} [Decidable P] : ite P a b = a ↔ ¬P → b = a := + dite_eq_left_iff + +@[simp] theorem ite_eq_right_iff {P : Prop} [Decidable P] : ite P a b = b ↔ P → a = b := + dite_eq_right_iff + +/-- A `dite` whose results do not actually depend on the condition may be reduced to an `ite`. -/ +@[simp] theorem dite_eq_ite [Decidable P] : (dite P (fun _ => a) fun _ => b) = ite P a b := rfl + +-- We don't mark this as `simp` as it is already handled by `ite_eq_right_iff`. +theorem ite_some_none_eq_none [Decidable P] : + (if P then some x else none) = none ↔ ¬ P := by + simp only [ite_eq_right_iff] + rfl + +@[simp] theorem ite_some_none_eq_some [Decidable P] : + (if P then some x else none) = some y ↔ P ∧ x = y := by + split <;> simp_all diff --git a/src/Init/Classical.lean b/src/Init/Classical.lean index 6e4727200f..ae2c589a33 100644 --- a/src/Init/Classical.lean +++ b/src/Init/Classical.lean @@ -4,8 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Leonardo de Moura, Mario Carneiro -/ prelude -import Init.Core -import Init.NotationExtra +import Init.PropLemmas universe u v @@ -112,8 +111,8 @@ theorem skolem {α : Sort u} {b : α → Sort v} {p : ∀ x, b x → Prop} : ( theorem propComplete (a : Prop) : a = True ∨ a = False := match em a with - | Or.inl ha => Or.inl (propext (Iff.intro (fun _ => ⟨⟩) (fun _ => ha))) - | Or.inr hn => Or.inr (propext (Iff.intro (fun h => hn h) (fun h => False.elim h))) + | Or.inl ha => Or.inl (eq_true ha) + | Or.inr hn => Or.inr (eq_false hn) -- this supercedes byCases in Decidable theorem byCases {p q : Prop} (hpq : p → q) (hnpq : ¬p → q) : q := @@ -123,15 +122,36 @@ theorem byCases {p q : Prop} (hpq : p → q) (hnpq : ¬p → q) : q := theorem byContradiction {p : Prop} (h : ¬p → False) : p := Decidable.byContradiction (dec := propDecidable _) h +/-- The Double Negation Theorem: `¬¬P` is equivalent to `P`. +The left-to-right direction, double negation elimination (DNE), +is classically true but not constructively. -/ +@[scoped simp] theorem not_not : ¬¬a ↔ a := Decidable.not_not + +@[simp] theorem not_forall {p : α → Prop} : (¬∀ x, p x) ↔ ∃ x, ¬p x := Decidable.not_forall + +theorem not_forall_not {p : α → Prop} : (¬∀ x, ¬p x) ↔ ∃ x, p x := Decidable.not_forall_not +theorem not_exists_not {p : α → Prop} : (¬∃ x, ¬p x) ↔ ∀ x, p x := Decidable.not_exists_not + +theorem forall_or_exists_not (P : α → Prop) : (∀ a, P a) ∨ ∃ a, ¬ P a := by + rw [← not_forall]; exact em _ + +theorem exists_or_forall_not (P : α → Prop) : (∃ a, P a) ∨ ∀ a, ¬ P a := by + rw [← not_exists]; exact em _ + +theorem or_iff_not_imp_left : a ∨ b ↔ (¬a → b) := Decidable.or_iff_not_imp_left +theorem or_iff_not_imp_right : a ∨ b ↔ (¬b → a) := Decidable.or_iff_not_imp_right + +theorem not_imp_iff_and_not : ¬(a → b) ↔ a ∧ ¬b := Decidable.not_imp_iff_and_not + +theorem not_and_iff_or_not_not : ¬(a ∧ b) ↔ ¬a ∨ ¬b := Decidable.not_and_iff_or_not_not + +theorem not_iff : ¬(a ↔ b) ↔ (¬a ↔ b) := Decidable.not_iff + end Classical -/-- -`by_cases (h :)? p` splits the main goal into two cases, assuming `h : p` in the first branch, and `h : ¬ p` in the second branch. --/ -syntax "by_cases " (atomic(ident " : "))? term : tactic +/-- Extract an element from a existential statement, using `Classical.choose`. -/ +-- This enables projection notation. +@[reducible] noncomputable def Exists.choose {p : α → Prop} (P : ∃ a, p a) : α := Classical.choose P -macro_rules - | `(tactic| by_cases $e) => `(tactic| by_cases h : $e) -macro_rules - | `(tactic| by_cases $h : $e) => - `(tactic| open Classical in refine if $h:ident : $e then ?pos else ?neg) +/-- Show that an element extracted from `P : ∃ a, p a` using `P.choose` satisfies `p`. -/ +theorem Exists.choose_spec {p : α → Prop} (P : ∃ a, p a) : p P.choose := Classical.choose_spec P diff --git a/src/Init/Core.lean b/src/Init/Core.lean index 96654601a4..0ad0c0a7f5 100644 --- a/src/Init/Core.lean +++ b/src/Init/Core.lean @@ -17,7 +17,9 @@ universe u v w at the application site itself (by comparison to the `@[inline]` attribute, which applies to all applications of the function). -/ -def inline {α : Sort u} (a : α) : α := a +@[simp] def inline {α : Sort u} (a : α) : α := a + +theorem id.def {α : Sort u} (a : α) : id a = a := rfl /-- `flip f a b` is `f b a`. It is useful for "point-free" programming, @@ -32,8 +34,32 @@ and `flip (·<·)` is the greater-than relation. @[simp] theorem Function.comp_apply {f : β → δ} {g : α → β} {x : α} : comp f g x = f (g x) := rfl +theorem Function.comp_def {α β δ} (f : β → δ) (g : α → β) : f ∘ g = fun x => f (g x) := rfl + attribute [simp] namedPattern +/-- +`Empty.elim : Empty → C` says that a value of any type can be constructed from +`Empty`. This can be thought of as a compiler-checked assertion that a code path is unreachable. + +This is a non-dependent variant of `Empty.rec`. +-/ +@[macro_inline] def Empty.elim {C : Sort u} : Empty → C := Empty.rec + +/-- Decidable equality for Empty -/ +instance : DecidableEq Empty := fun a => a.elim + +/-- +`PEmpty.elim : Empty → C` says that a value of any type can be constructed from +`PEmpty`. This can be thought of as a compiler-checked assertion that a code path is unreachable. + +This is a non-dependent variant of `PEmpty.rec`. +-/ +@[macro_inline] def PEmpty.elim {C : Sort _} : PEmpty → C := fun a => nomatch a + +/-- Decidable equality for PEmpty -/ +instance : DecidableEq PEmpty := fun a => a.elim + /-- Thunks are "lazy" values that are evaluated when first accessed using `Thunk.get/map/bind`. The value is then stored and not recomputed for all further accesses. -/ @@ -78,6 +104,8 @@ instance thunkCoe : CoeTail α (Thunk α) where abbrev Eq.ndrecOn.{u1, u2} {α : Sort u2} {a : α} {motive : α → Sort u1} {b : α} (h : a = b) (m : motive a) : motive b := Eq.ndrec m h +/-! # definitions -/ + /-- If and only if, or logical bi-implication. `a ↔ b` means that `a` implies `b` and vice versa. By `propext`, this implies that `a` and `b` are equal and hence any expression involving `a` @@ -126,6 +154,10 @@ inductive PSum (α : Sort u) (β : Sort v) where @[inherit_doc] infixr:30 " ⊕' " => PSum +instance {α β} [Inhabited α] : Inhabited (PSum α β) := ⟨PSum.inl default⟩ + +instance {α β} [Inhabited β] : Inhabited (PSum α β) := ⟨PSum.inr default⟩ + /-- `Sigma β`, also denoted `Σ a : α, β a` or `(a : α) × β a`, is the type of dependent pairs whose first component is `a : α` and whose second component is `b : β a` @@ -525,9 +557,7 @@ theorem not_not_intro {p : Prop} (h : p) : ¬ ¬ p := fun hn : ¬ p => hn h -- proof irrelevance is built in -theorem proofIrrel {a : Prop} (h₁ h₂ : a) : h₁ = h₂ := rfl - -theorem id.def {α : Sort u} (a : α) : id a = a := rfl +theorem proof_irrel {a : Prop} (h₁ h₂ : a) : h₁ = h₂ := rfl /-- If `h : α = β` is a proof of type equality, then `h.mp : α → β` is the induced @@ -575,8 +605,9 @@ theorem Ne.elim (h : a ≠ b) : a = b → False := h theorem Ne.irrefl (h : a ≠ a) : False := h rfl -theorem Ne.symm (h : a ≠ b) : b ≠ a := - fun h₁ => h (h₁.symm) +theorem Ne.symm (h : a ≠ b) : b ≠ a := fun h₁ => h (h₁.symm) + +theorem ne_comm {α} {a b : α} : a ≠ b ↔ b ≠ a := ⟨Ne.symm, Ne.symm⟩ theorem false_of_ne : a ≠ a → False := Ne.irrefl @@ -588,8 +619,8 @@ theorem ne_true_of_not : ¬p → p ≠ True := have : ¬True := h ▸ hnp this trivial -theorem true_ne_false : ¬True = False := - ne_false_of_self trivial +theorem true_ne_false : ¬True = False := ne_false_of_self trivial +theorem false_ne_true : False ≠ True := fun h => h.symm ▸ trivial end Ne @@ -668,22 +699,29 @@ protected theorem Iff.rfl {a : Prop} : a ↔ a := macro_rules | `(tactic| rfl) => `(tactic| exact Iff.rfl) +theorem Iff.of_eq (h : a = b) : a ↔ b := h ▸ Iff.rfl + theorem Iff.trans (h₁ : a ↔ b) (h₂ : b ↔ c) : a ↔ c := - Iff.intro - (fun ha => Iff.mp h₂ (Iff.mp h₁ ha)) - (fun hc => Iff.mpr h₁ (Iff.mpr h₂ hc)) + Iff.intro (h₂.mp ∘ h₁.mp) (h₁.mpr ∘ h₂.mpr) -theorem Iff.symm (h : a ↔ b) : b ↔ a := - Iff.intro (Iff.mpr h) (Iff.mp h) +-- This is needed for `calc` to work with `iff`. +instance : Trans Iff Iff Iff where + trans := Iff.trans -theorem Iff.comm : (a ↔ b) ↔ (b ↔ a) := - Iff.intro Iff.symm Iff.symm +theorem Eq.comm {a b : α} : a = b ↔ b = a := Iff.intro Eq.symm Eq.symm +theorem eq_comm {a b : α} : a = b ↔ b = a := Eq.comm -theorem Iff.of_eq (h : a = b) : a ↔ b := - h ▸ Iff.refl _ +theorem Iff.symm (h : a ↔ b) : b ↔ a := Iff.intro h.mpr h.mp +theorem Iff.comm: (a ↔ b) ↔ (b ↔ a) := Iff.intro Iff.symm Iff.symm +theorem iff_comm : (a ↔ b) ↔ (b ↔ a) := Iff.comm -theorem And.comm : a ∧ b ↔ b ∧ a := by - constructor <;> intro ⟨h₁, h₂⟩ <;> exact ⟨h₂, h₁⟩ +theorem And.symm : a ∧ b → b ∧ a := fun ⟨ha, hb⟩ => ⟨hb, ha⟩ +theorem And.comm : a ∧ b ↔ b ∧ a := Iff.intro And.symm And.symm +theorem and_comm : a ∧ b ↔ b ∧ a := And.comm + +theorem Or.symm : a ∨ b → b ∨ a := .rec .inr .inl +theorem Or.comm : a ∨ b ↔ b ∨ a := Iff.intro Or.symm Or.symm +theorem or_comm : a ∨ b ↔ b ∨ a := Or.comm /-! # Exists -/ @@ -883,8 +921,13 @@ protected theorem Subsingleton.helim {α β : Sort u} [h₁ : Subsingleton α] ( apply heq_of_eq apply Subsingleton.elim -instance (p : Prop) : Subsingleton p := - ⟨fun a b => proofIrrel a b⟩ +instance (p : Prop) : Subsingleton p := ⟨fun a b => proof_irrel a b⟩ + +instance : Subsingleton Empty := ⟨(·.elim)⟩ +instance : Subsingleton PEmpty := ⟨(·.elim)⟩ + +instance [Subsingleton α] [Subsingleton β] : Subsingleton (α × β) := + ⟨fun {..} {..} => by congr <;> apply Subsingleton.elim⟩ instance (p : Prop) : Subsingleton (Decidable p) := Subsingleton.intro fun @@ -895,6 +938,9 @@ instance (p : Prop) : Subsingleton (Decidable p) := | isTrue t₂ => absurd t₂ f₁ | isFalse _ => rfl +example [Subsingleton α] (p : α → Prop) : Subsingleton (Subtype p) := + ⟨fun ⟨x, _⟩ ⟨y, _⟩ => by congr; exact Subsingleton.elim x y⟩ + theorem recSubsingleton {p : Prop} [h : Decidable p] {h₁ : p → Sort u} @@ -1174,12 +1220,117 @@ gen_injective_theorems% Lean.Syntax @[simp] theorem beq_iff_eq [BEq α] [LawfulBEq α] (a b : α) : a == b ↔ a = b := ⟨eq_of_beq, by intro h; subst h; exact LawfulBEq.rfl⟩ -/-! # Quotients -/ +/-! # Prop lemmas -/ + +/-- *Ex falso* for negation: from `¬a` and `a` anything follows. This is the same as `absurd` with +the arguments flipped, but it is in the `Not` namespace so that projection notation can be used. -/ +def Not.elim {α : Sort _} (H1 : ¬a) (H2 : a) : α := absurd H2 H1 + +/-- Non-dependent eliminator for `And`. -/ +abbrev And.elim (f : a → b → α) (h : a ∧ b) : α := f h.left h.right + +/-- Non-dependent eliminator for `Iff`. -/ +def Iff.elim (f : (a → b) → (b → a) → α) (h : a ↔ b) : α := f h.mp h.mpr /-- Iff can now be used to do substitutions in a calculation -/ theorem Iff.subst {a b : Prop} {p : Prop → Prop} (h₁ : a ↔ b) (h₂ : p a) : p b := Eq.subst (propext h₁) h₂ +theorem Not.intro {a : Prop} (h : a → False) : ¬a := h + +theorem Not.imp {a b : Prop} (H2 : ¬b) (H1 : a → b) : ¬a := mt H1 H2 + +theorem not_congr (h : a ↔ b) : ¬a ↔ ¬b := ⟨mt h.2, mt h.1⟩ + +theorem not_not_not : ¬¬¬a ↔ ¬a := ⟨mt not_not_intro, not_not_intro⟩ + +theorem iff_of_true (ha : a) (hb : b) : a ↔ b := Iff.intro (fun _ => hb) (fun _ => ha) +theorem iff_of_false (ha : ¬a) (hb : ¬b) : a ↔ b := Iff.intro ha.elim hb.elim + +theorem iff_true_left (ha : a) : (a ↔ b) ↔ b := Iff.intro (·.mp ha) (iff_of_true ha) +theorem iff_true_right (ha : a) : (b ↔ a) ↔ b := Iff.comm.trans (iff_true_left ha) + +theorem iff_false_left (ha : ¬a) : (a ↔ b) ↔ ¬b := Iff.intro (mt ·.mpr ha) (iff_of_false ha) +theorem iff_false_right (ha : ¬a) : (b ↔ a) ↔ ¬b := Iff.comm.trans (iff_false_left ha) + +theorem of_iff_true (h : a ↔ True) : a := h.mpr trivial +theorem iff_true_intro (h : a) : a ↔ True := iff_of_true h trivial + +theorem not_of_iff_false : (p ↔ False) → ¬p := Iff.mp +theorem iff_false_intro (h : ¬a) : a ↔ False := iff_of_false h id + +theorem not_iff_false_intro (h : a) : ¬a ↔ False := iff_false_intro (not_not_intro h) +theorem not_true : (¬True) ↔ False := iff_false_intro (not_not_intro trivial) + +theorem not_false_iff : (¬False) ↔ True := iff_true_intro not_false + +theorem Eq.to_iff : a = b → (a ↔ b) := Iff.of_eq +theorem iff_of_eq : a = b → (a ↔ b) := Iff.of_eq +theorem neq_of_not_iff : ¬(a ↔ b) → a ≠ b := mt Iff.of_eq + +theorem iff_iff_eq : (a ↔ b) ↔ a = b := Iff.intro propext Iff.of_eq +@[simp] theorem eq_iff_iff : (a = b) ↔ (a ↔ b) := iff_iff_eq.symm + +theorem eq_self_iff_true (a : α) : a = a ↔ True := iff_true_intro rfl +theorem ne_self_iff_false (a : α) : a ≠ a ↔ False := not_iff_false_intro rfl + +theorem false_of_true_iff_false (h : True ↔ False) : False := h.mp trivial +theorem false_of_true_eq_false (h : True = False) : False := false_of_true_iff_false (Iff.of_eq h) + +theorem true_eq_false_of_false : False → (True = False) := False.elim + +theorem iff_def : (a ↔ b) ↔ (a → b) ∧ (b → a) := iff_iff_implies_and_implies a b +theorem iff_def' : (a ↔ b) ↔ (b → a) ∧ (a → b) := Iff.trans iff_def And.comm + +theorem true_iff_false : (True ↔ False) ↔ False := iff_false_intro (·.mp True.intro) +theorem false_iff_true : (False ↔ True) ↔ False := iff_false_intro (·.mpr True.intro) + +theorem iff_not_self : ¬(a ↔ ¬a) | H => let f h := H.1 h h; f (H.2 f) +theorem heq_self_iff_true (a : α) : HEq a a ↔ True := iff_true_intro HEq.rfl + +/-! ## implies -/ + +theorem not_not_of_not_imp : ¬(a → b) → ¬¬a := mt Not.elim + +theorem not_of_not_imp {a : Prop} : ¬(a → b) → ¬b := mt fun h _ => h + +@[simp] theorem imp_not_self : (a → ¬a) ↔ ¬a := Iff.intro (fun h ha => h ha ha) (fun h _ => h) + +theorem imp_intro {α β : Prop} (h : α) : β → α := fun _ => h + +theorem imp_imp_imp {a b c d : Prop} (h₀ : c → a) (h₁ : b → d) : (a → b) → (c → d) := (h₁ ∘ · ∘ h₀) + +theorem imp_iff_right {a : Prop} (ha : a) : (a → b) ↔ b := Iff.intro (· ha) (fun a _ => a) + +-- This is not marked `@[simp]` because we have `implies_true : (α → True) = True` +theorem imp_true_iff (α : Sort u) : (α → True) ↔ True := iff_true_intro (fun _ => trivial) + +theorem false_imp_iff (a : Prop) : (False → a) ↔ True := iff_true_intro False.elim + +theorem true_imp_iff (α : Prop) : (True → α) ↔ α := imp_iff_right True.intro + +@[simp] theorem imp_self : (a → a) ↔ True := iff_true_intro id + +theorem imp_false : (a → False) ↔ ¬a := Iff.rfl + +theorem imp.swap : (a → b → c) ↔ (b → a → c) := Iff.intro flip flip + +theorem imp_not_comm : (a → ¬b) ↔ (b → ¬a) := imp.swap + +theorem imp_congr_left (h : a ↔ b) : (a → c) ↔ (b → c) := Iff.intro (· ∘ h.mpr) (· ∘ h.mp) + +theorem imp_congr_right (h : a → (b ↔ c)) : (a → b) ↔ (a → c) := + Iff.intro (fun hab ha => (h ha).mp (hab ha)) (fun hcd ha => (h ha).mpr (hcd ha)) + +theorem imp_congr_ctx (h₁ : a ↔ c) (h₂ : c → (b ↔ d)) : (a → b) ↔ (c → d) := + Iff.trans (imp_congr_left h₁) (imp_congr_right h₂) + +theorem imp_congr (h₁ : a ↔ c) (h₂ : b ↔ d) : (a → b) ↔ (c → d) := imp_congr_ctx h₁ fun _ => h₂ + +theorem imp_iff_not (hb : ¬b) : a → b ↔ ¬a := imp_congr_right fun _ => iff_false_intro hb + +/-! # Quotients -/ + namespace Quot /-- The **quotient axiom**, or at least the nontrivial part of the quotient diff --git a/src/Init/Data/Array/DecidableEq.lean b/src/Init/Data/Array/DecidableEq.lean index f7f1cdbeca..6dd41dee8c 100644 --- a/src/Init/Data/Array/DecidableEq.lean +++ b/src/Init/Data/Array/DecidableEq.lean @@ -5,7 +5,7 @@ Authors: Leonardo de Moura -/ prelude import Init.Data.Array.Basic -import Init.Classical +import Init.ByCases namespace Array diff --git a/src/Init/Data/List/Basic.lean b/src/Init/Data/List/Basic.lean index 62c693e89d..a124f9c513 100644 --- a/src/Init/Data/List/Basic.lean +++ b/src/Init/Data/List/Basic.lean @@ -876,7 +876,7 @@ instance [BEq α] [LawfulBEq α] : LawfulBEq (List α) where cases bs with | nil => intro h; contradiction | cons b bs => - simp [show (a::as == b::bs) = (a == b && as == bs) from rfl] + simp [show (a::as == b::bs) = (a == b && as == bs) from rfl, -and_imp] intro ⟨h₁, h₂⟩ exact ⟨h₁, ih h₂⟩ rfl {as} := by diff --git a/src/Init/Data/Nat/Basic.lean b/src/Init/Data/Nat/Basic.lean index 707a383d96..78856c3bf6 100644 --- a/src/Init/Data/Nat/Basic.lean +++ b/src/Init/Data/Nat/Basic.lean @@ -147,7 +147,7 @@ protected theorem add_right_comm (n m k : Nat) : (n + m) + k = (n + k) + m := by protected theorem add_left_cancel {n m k : Nat} : n + m = n + k → m = k := by induction n with - | zero => simp; intros; assumption + | zero => simp | succ n ih => simp [succ_add]; intro h; apply ih h protected theorem add_right_cancel {n m k : Nat} (h : n + m = k + m) : n = k := by diff --git a/src/Init/Data/Nat/Linear.lean b/src/Init/Data/Nat/Linear.lean index 4fa179874e..35c98eaa62 100644 --- a/src/Init/Data/Nat/Linear.lean +++ b/src/Init/Data/Nat/Linear.lean @@ -5,8 +5,7 @@ Authors: Leonardo de Moura -/ prelude import Init.Coe -import Init.Classical -import Init.SimpLemmas +import Init.ByCases import Init.Data.Nat.Basic import Init.Data.List.Basic import Init.Data.Prod @@ -539,13 +538,13 @@ theorem Expr.eq_of_toNormPoly (ctx : Context) (a b : Expr) (h : a.toNormPoly = b theorem Expr.of_cancel_eq (ctx : Context) (a b c d : Expr) (h : Poly.cancel a.toNormPoly b.toNormPoly = (c.toPoly, d.toPoly)) : (a.denote ctx = b.denote ctx) = (c.denote ctx = d.denote ctx) := by have := Poly.denote_eq_cancel_eq ctx a.toNormPoly b.toNormPoly rw [h] at this - simp [toNormPoly, Poly.norm, Poly.denote_eq] at this + simp [toNormPoly, Poly.norm, Poly.denote_eq, -eq_iff_iff] at this exact this.symm theorem Expr.of_cancel_le (ctx : Context) (a b c d : Expr) (h : Poly.cancel a.toNormPoly b.toNormPoly = (c.toPoly, d.toPoly)) : (a.denote ctx ≤ b.denote ctx) = (c.denote ctx ≤ d.denote ctx) := by have := Poly.denote_le_cancel_eq ctx a.toNormPoly b.toNormPoly rw [h] at this - simp [toNormPoly, Poly.norm,Poly.denote_le] at this + simp [toNormPoly, Poly.norm,Poly.denote_le, -eq_iff_iff] at this exact this.symm theorem Expr.of_cancel_lt (ctx : Context) (a b c d : Expr) (h : Poly.cancel a.inc.toNormPoly b.toNormPoly = (c.inc.toPoly, d.toPoly)) : (a.denote ctx < b.denote ctx) = (c.denote ctx < d.denote ctx) := @@ -590,7 +589,7 @@ theorem PolyCnstr.denote_mul (ctx : Context) (k : Nat) (c : PolyCnstr) : (c.mul have : (1 == (0 : Nat)) = false := rfl have : (1 == (1 : Nat)) = true := rfl by_cases he : eq = true <;> simp [he, PolyCnstr.mul, PolyCnstr.denote, Poly.denote_le, Poly.denote_eq] - <;> by_cases hk : k == 0 <;> (try simp [eq_of_beq hk]) <;> simp [*] <;> apply propext <;> apply Iff.intro <;> intro h + <;> by_cases hk : k == 0 <;> (try simp [eq_of_beq hk]) <;> simp [*] <;> apply Iff.intro <;> intro h · exact Nat.eq_of_mul_eq_mul_left (Nat.zero_lt_succ _) h · rw [h] · exact Nat.le_of_mul_le_mul_left h (Nat.zero_lt_succ _) @@ -637,7 +636,7 @@ theorem Poly.of_isNonZero (ctx : Context) {p : Poly} (h : isNonZero p = true) : theorem PolyCnstr.eq_false_of_isUnsat (ctx : Context) {c : PolyCnstr} : c.isUnsat → c.denote ctx = False := by cases c; rename_i eq lhs rhs simp [isUnsat] - by_cases he : eq = true <;> simp [he, denote, Poly.denote_eq, Poly.denote_le] + by_cases he : eq = true <;> simp [he, denote, Poly.denote_eq, Poly.denote_le, -and_imp] · intro | Or.inl ⟨h₁, h₂⟩ => simp [Poly.of_isZero, h₁]; have := Nat.not_eq_zero_of_lt (Poly.of_isNonZero ctx h₂); simp [this.symm] | Or.inr ⟨h₁, h₂⟩ => simp [Poly.of_isZero, h₂]; have := Nat.not_eq_zero_of_lt (Poly.of_isNonZero ctx h₁); simp [this] @@ -650,7 +649,7 @@ theorem PolyCnstr.eq_false_of_isUnsat (ctx : Context) {c : PolyCnstr} : c.isUnsa theorem PolyCnstr.eq_true_of_isValid (ctx : Context) {c : PolyCnstr} : c.isValid → c.denote ctx = True := by cases c; rename_i eq lhs rhs simp [isValid] - by_cases he : eq = true <;> simp [he, denote, Poly.denote_eq, Poly.denote_le] + by_cases he : eq = true <;> simp [he, denote, Poly.denote_eq, Poly.denote_le, -and_imp] · intro ⟨h₁, h₂⟩ simp [Poly.of_isZero, h₁, h₂] · intro h @@ -658,12 +657,12 @@ theorem PolyCnstr.eq_true_of_isValid (ctx : Context) {c : PolyCnstr} : c.isValid theorem ExprCnstr.eq_false_of_isUnsat (ctx : Context) (c : ExprCnstr) (h : c.toNormPoly.isUnsat) : c.denote ctx = False := by have := PolyCnstr.eq_false_of_isUnsat ctx h - simp at this + simp [-eq_iff_iff] at this assumption theorem ExprCnstr.eq_true_of_isValid (ctx : Context) (c : ExprCnstr) (h : c.toNormPoly.isValid) : c.denote ctx = True := by have := PolyCnstr.eq_true_of_isValid ctx h - simp at this + simp [-eq_iff_iff] at this assumption theorem Certificate.of_combineHyps (ctx : Context) (c : PolyCnstr) (cs : Certificate) (h : (combineHyps c cs).denote ctx → False) : c.denote ctx → cs.denote ctx := by @@ -712,7 +711,7 @@ theorem Poly.denote_toExpr (ctx : Context) (p : Poly) : p.toExpr.denote ctx = p. theorem ExprCnstr.eq_of_toNormPoly_eq (ctx : Context) (c d : ExprCnstr) (h : c.toNormPoly == d.toPoly) : c.denote ctx = d.denote ctx := by have h := congrArg (PolyCnstr.denote ctx) (eq_of_beq h) - simp at h + simp [-eq_iff_iff] at h assumption theorem Expr.eq_of_toNormPoly_eq (ctx : Context) (e e' : Expr) (h : e.toNormPoly == e'.toPoly) : e.denote ctx = e'.denote ctx := by diff --git a/src/Init/PropLemmas.lean b/src/Init/PropLemmas.lean new file mode 100644 index 0000000000..b0b4b08a18 --- /dev/null +++ b/src/Init/PropLemmas.lean @@ -0,0 +1,443 @@ +/- +Copyright (c) 2024 Lean FRO. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Leonardo de Moura, Jeremy Avigad, Floris van Doorn, Mario Carneiro + +This provides additional lemmas about propositional types beyond what is +needed for Core and SimpLemmas. +-/ +prelude +import Init.Core +import Init.NotationExtra +set_option linter.missingDocs true -- keep it documented + +/-! ## not -/ + +theorem not_not_em (a : Prop) : ¬¬(a ∨ ¬a) := fun h => h (.inr (h ∘ .inl)) + +/-! ## and -/ + +theorem and_self_iff : a ∧ a ↔ a := Iff.of_eq (and_self a) +theorem and_not_self_iff (a : Prop) : a ∧ ¬a ↔ False := iff_false_intro and_not_self +theorem not_and_self_iff (a : Prop) : ¬a ∧ a ↔ False := iff_false_intro not_and_self + +theorem And.imp (f : a → c) (g : b → d) (h : a ∧ b) : c ∧ d := And.intro (f h.left) (g h.right) +theorem And.imp_left (h : a → b) : a ∧ c → b ∧ c := .imp h id +theorem And.imp_right (h : a → b) : c ∧ a → c ∧ b := .imp id h + +theorem and_congr (h₁ : a ↔ c) (h₂ : b ↔ d) : a ∧ b ↔ c ∧ d := + Iff.intro (And.imp h₁.mp h₂.mp) (And.imp h₁.mpr h₂.mpr) +theorem and_congr_left' (h : a ↔ b) : a ∧ c ↔ b ∧ c := and_congr h .rfl +theorem and_congr_right' (h : b ↔ c) : a ∧ b ↔ a ∧ c := and_congr .rfl h + +theorem not_and_of_not_left (b : Prop) : ¬a → ¬(a ∧ b) := mt And.left +theorem not_and_of_not_right (a : Prop) {b : Prop} : ¬b → ¬(a ∧ b) := mt And.right + +theorem and_congr_right_eq (h : a → b = c) : (a ∧ b) = (a ∧ c) := + propext (and_congr_right (Iff.of_eq ∘ h)) +theorem and_congr_left_eq (h : c → a = b) : (a ∧ c) = (b ∧ c) := + propext (and_congr_left (Iff.of_eq ∘ h)) + +theorem and_left_comm : a ∧ b ∧ c ↔ b ∧ a ∧ c := + Iff.intro (fun ⟨ha, hb, hc⟩ => ⟨hb, ha, hc⟩) + (fun ⟨hb, ha, hc⟩ => ⟨ha, hb, hc⟩) + +theorem and_right_comm : (a ∧ b) ∧ c ↔ (a ∧ c) ∧ b := + Iff.intro (fun ⟨⟨ha, hb⟩, hc⟩ => ⟨⟨ha, hc⟩, hb⟩) + (fun ⟨⟨ha, hc⟩, hb⟩ => ⟨⟨ha, hb⟩, hc⟩) + +theorem and_rotate : a ∧ b ∧ c ↔ b ∧ c ∧ a := by rw [and_left_comm, @and_comm a c] +theorem and_and_and_comm : (a ∧ b) ∧ c ∧ d ↔ (a ∧ c) ∧ b ∧ d := by rw [← and_assoc, @and_right_comm a, and_assoc] +theorem and_and_left : a ∧ (b ∧ c) ↔ (a ∧ b) ∧ a ∧ c := by rw [and_and_and_comm, and_self] +theorem and_and_right : (a ∧ b) ∧ c ↔ (a ∧ c) ∧ b ∧ c := by rw [and_and_and_comm, and_self] + +theorem and_iff_left (hb : b) : a ∧ b ↔ a := Iff.intro And.left (And.intro · hb) +theorem and_iff_right (ha : a) : a ∧ b ↔ b := Iff.intro And.right (And.intro ha ·) + +/-! ## or -/ + +theorem or_self_iff : a ∨ a ↔ a := or_self _ ▸ .rfl +theorem not_or_intro {a b : Prop} (ha : ¬a) (hb : ¬b) : ¬(a ∨ b) := (·.elim ha hb) + +theorem Or.resolve_left (h: a ∨ b) (na : ¬a) : b := h.elim (absurd · na) id +theorem Or.resolve_right (h: a ∨ b) (nb : ¬b) : a := h.elim id (absurd · nb) + +theorem Or.neg_resolve_left (h : ¬a ∨ b) (ha : a) : b := h.elim (absurd ha) id +theorem Or.neg_resolve_right (h : a ∨ ¬b) (nb : b) : a := h.elim id (absurd nb) + +theorem or_congr (h₁ : a ↔ c) (h₂ : b ↔ d) : (a ∨ b) ↔ (c ∨ d) := ⟨.imp h₁.mp h₂.mp, .imp h₁.mpr h₂.mpr⟩ +theorem or_congr_left (h : a ↔ b) : a ∨ c ↔ b ∨ c := or_congr h .rfl +theorem or_congr_right (h : b ↔ c) : a ∨ b ↔ a ∨ c := or_congr .rfl h + +theorem or_left_comm : a ∨ (b ∨ c) ↔ b ∨ (a ∨ c) := by rw [← or_assoc, ← or_assoc, @or_comm a b] +theorem or_right_comm : (a ∨ b) ∨ c ↔ (a ∨ c) ∨ b := by rw [or_assoc, or_assoc, @or_comm b] + +theorem or_or_or_comm : (a ∨ b) ∨ c ∨ d ↔ (a ∨ c) ∨ b ∨ d := by rw [← or_assoc, @or_right_comm a, or_assoc] + +theorem or_or_distrib_left : a ∨ b ∨ c ↔ (a ∨ b) ∨ a ∨ c := by rw [or_or_or_comm, or_self] +theorem or_or_distrib_right : (a ∨ b) ∨ c ↔ (a ∨ c) ∨ b ∨ c := by rw [or_or_or_comm, or_self] + +theorem or_rotate : a ∨ b ∨ c ↔ b ∨ c ∨ a := by simp only [or_left_comm, Or.comm] + +theorem or_iff_left (hb : ¬b) : a ∨ b ↔ a := or_iff_left_iff_imp.mpr hb.elim +theorem or_iff_right (ha : ¬a) : a ∨ b ↔ b := or_iff_right_iff_imp.mpr ha.elim + +/-! ## distributivity -/ + +theorem not_imp_of_and_not : a ∧ ¬b → ¬(a → b) + | ⟨ha, hb⟩, h => hb <| h ha + +theorem imp_and {α} : (α → b ∧ c) ↔ (α → b) ∧ (α → c) := + ⟨fun h => ⟨fun ha => (h ha).1, fun ha => (h ha).2⟩, fun h ha => ⟨h.1 ha, h.2 ha⟩⟩ + +theorem not_and' : ¬(a ∧ b) ↔ b → ¬a := Iff.trans not_and imp_not_comm + +/-- `∧` distributes over `∨` (on the left). -/ +theorem and_or_left : a ∧ (b ∨ c) ↔ (a ∧ b) ∨ (a ∧ c) := + Iff.intro (fun ⟨ha, hbc⟩ => hbc.imp (.intro ha) (.intro ha)) + (Or.rec (.imp_right .inl) (.imp_right .inr)) + +/-- `∧` distributes over `∨` (on the right). -/ +theorem or_and_right : (a ∨ b) ∧ c ↔ (a ∧ c) ∨ (b ∧ c) := by rw [@and_comm (a ∨ b), and_or_left, @and_comm c, @and_comm c] + +/-- `∨` distributes over `∧` (on the left). -/ +theorem or_and_left : a ∨ (b ∧ c) ↔ (a ∨ b) ∧ (a ∨ c) := + Iff.intro (Or.rec (fun ha => ⟨.inl ha, .inl ha⟩) (.imp .inr .inr)) + (And.rec <| .rec (fun _ => .inl ·) (.imp_right ∘ .intro)) + +/-- `∨` distributes over `∧` (on the right). -/ +theorem and_or_right : (a ∧ b) ∨ c ↔ (a ∨ c) ∧ (b ∨ c) := by rw [@or_comm (a ∧ b), or_and_left, @or_comm c, @or_comm c] + +theorem or_imp : (a ∨ b → c) ↔ (a → c) ∧ (b → c) := + Iff.intro (fun h => ⟨h ∘ .inl, h ∘ .inr⟩) (fun ⟨ha, hb⟩ => Or.rec ha hb) +theorem not_or : ¬(p ∨ q) ↔ ¬p ∧ ¬q := or_imp + +theorem not_and_of_not_or_not (h : ¬a ∨ ¬b) : ¬(a ∧ b) := h.elim (mt (·.1)) (mt (·.2)) + +/-! ## exists and forall -/ + +section quantifiers +variable {p q : α → Prop} {b : Prop} + +theorem forall_imp (h : ∀ a, p a → q a) : (∀ a, p a) → ∀ a, q a := fun h' a => h a (h' a) + +/-- +As `simp` does not index foralls, this `@[simp]` lemma is tried on every `forall` expression. +This is not ideal, and likely a performance issue, but it is difficult to remove this attribute at this time. +-/ +@[simp] theorem forall_exists_index {q : (∃ x, p x) → Prop} : + (∀ h, q h) ↔ ∀ x (h : p x), q ⟨x, h⟩ := + ⟨fun h x hpx => h ⟨x, hpx⟩, fun h ⟨x, hpx⟩ => h x hpx⟩ + +theorem Exists.imp (h : ∀ a, p a → q a) : (∃ a, p a) → ∃ a, q a + | ⟨a, hp⟩ => ⟨a, h a hp⟩ + +theorem Exists.imp' {β} {q : β → Prop} (f : α → β) (hpq : ∀ a, p a → q (f a)) : + (∃ a, p a) → ∃ b, q b + | ⟨_, hp⟩ => ⟨_, hpq _ hp⟩ + +theorem exists_imp : ((∃ x, p x) → b) ↔ ∀ x, p x → b := forall_exists_index + +@[simp] theorem exists_const (α) [i : Nonempty α] : (∃ _ : α, b) ↔ b := + ⟨fun ⟨_, h⟩ => h, i.elim Exists.intro⟩ + +section forall_congr + +theorem forall_congr' (h : ∀ a, p a ↔ q a) : (∀ a, p a) ↔ ∀ a, q a := + ⟨fun H a => (h a).1 (H a), fun H a => (h a).2 (H a)⟩ + +theorem exists_congr (h : ∀ a, p a ↔ q a) : (∃ a, p a) ↔ ∃ a, q a := + ⟨Exists.imp fun x => (h x).1, Exists.imp fun x => (h x).2⟩ + +variable {β : α → Sort _} + +theorem forall₂_congr {p q : ∀ a, β a → Prop} (h : ∀ a b, p a b ↔ q a b) : + (∀ a b, p a b) ↔ ∀ a b, q a b := + forall_congr' fun a => forall_congr' <| h a + +theorem exists₂_congr {p q : ∀ a, β a → Prop} (h : ∀ a b, p a b ↔ q a b) : + (∃ a b, p a b) ↔ ∃ a b, q a b := + exists_congr fun a => exists_congr <| h a + +variable {γ : ∀ a, β a → Sort _} +theorem forall₃_congr {p q : ∀ a b, γ a b → Prop} (h : ∀ a b c, p a b c ↔ q a b c) : + (∀ a b c, p a b c) ↔ ∀ a b c, q a b c := + forall_congr' fun a => forall₂_congr <| h a + +theorem exists₃_congr {p q : ∀ a b, γ a b → Prop} (h : ∀ a b c, p a b c ↔ q a b c) : + (∃ a b c, p a b c) ↔ ∃ a b c, q a b c := + exists_congr fun a => exists₂_congr <| h a + +variable {δ : ∀ a b, γ a b → Sort _} +theorem forall₄_congr {p q : ∀ a b c, δ a b c → Prop} (h : ∀ a b c d, p a b c d ↔ q a b c d) : + (∀ a b c d, p a b c d) ↔ ∀ a b c d, q a b c d := + forall_congr' fun a => forall₃_congr <| h a + +theorem exists₄_congr {p q : ∀ a b c, δ a b c → Prop} (h : ∀ a b c d, p a b c d ↔ q a b c d) : + (∃ a b c d, p a b c d) ↔ ∃ a b c d, q a b c d := + exists_congr fun a => exists₃_congr <| h a + +variable {ε : ∀ a b c, δ a b c → Sort _} +theorem forall₅_congr {p q : ∀ a b c d, ε a b c d → Prop} + (h : ∀ a b c d e, p a b c d e ↔ q a b c d e) : + (∀ a b c d e, p a b c d e) ↔ ∀ a b c d e, q a b c d e := + forall_congr' fun a => forall₄_congr <| h a + +theorem exists₅_congr {p q : ∀ a b c d, ε a b c d → Prop} + (h : ∀ a b c d e, p a b c d e ↔ q a b c d e) : + (∃ a b c d e, p a b c d e) ↔ ∃ a b c d e, q a b c d e := + exists_congr fun a => exists₄_congr <| h a + +end forall_congr + +@[simp] theorem not_exists : (¬∃ x, p x) ↔ ∀ x, ¬p x := exists_imp + +theorem forall_and : (∀ x, p x ∧ q x) ↔ (∀ x, p x) ∧ (∀ x, q x) := + ⟨fun h => ⟨fun x => (h x).1, fun x => (h x).2⟩, fun ⟨h₁, h₂⟩ x => ⟨h₁ x, h₂ x⟩⟩ + +theorem exists_or : (∃ x, p x ∨ q x) ↔ (∃ x, p x) ∨ ∃ x, q x := + ⟨fun | ⟨x, .inl h⟩ => .inl ⟨x, h⟩ | ⟨x, .inr h⟩ => .inr ⟨x, h⟩, + fun | .inl ⟨x, h⟩ => ⟨x, .inl h⟩ | .inr ⟨x, h⟩ => ⟨x, .inr h⟩⟩ + +@[simp] theorem exists_false : ¬(∃ _a : α, False) := fun ⟨_, h⟩ => h + +@[simp] theorem forall_const (α : Sort _) [i : Nonempty α] : (α → b) ↔ b := + ⟨i.elim, fun hb _ => hb⟩ + +theorem Exists.nonempty : (∃ x, p x) → Nonempty α | ⟨x, _⟩ => ⟨x⟩ + +theorem not_forall_of_exists_not {p : α → Prop} : (∃ x, ¬p x) → ¬∀ x, p x + | ⟨x, hn⟩, h => hn (h x) + +@[simp] theorem forall_eq {p : α → Prop} {a' : α} : (∀ a, a = a' → p a) ↔ p a' := + ⟨fun h => h a' rfl, fun h _ e => e.symm ▸ h⟩ + +@[simp] theorem forall_eq' {a' : α} : (∀ a, a' = a → p a) ↔ p a' := by simp [@eq_comm _ a'] + +@[simp] theorem exists_eq : ∃ a, a = a' := ⟨_, rfl⟩ + +@[simp] theorem exists_eq' : ∃ a, a' = a := ⟨_, rfl⟩ + +@[simp] theorem exists_eq_left : (∃ a, a = a' ∧ p a) ↔ p a' := + ⟨fun ⟨_, e, h⟩ => e ▸ h, fun h => ⟨_, rfl, h⟩⟩ + +@[simp] theorem exists_eq_right : (∃ a, p a ∧ a = a') ↔ p a' := + (exists_congr <| by exact fun a => And.comm).trans exists_eq_left + +@[simp] theorem exists_and_left : (∃ x, b ∧ p x) ↔ b ∧ (∃ x, p x) := + ⟨fun ⟨x, h, hp⟩ => ⟨h, x, hp⟩, fun ⟨h, x, hp⟩ => ⟨x, h, hp⟩⟩ + +@[simp] theorem exists_and_right : (∃ x, p x ∧ b) ↔ (∃ x, p x) ∧ b := by simp [And.comm] + +@[simp] theorem exists_eq_left' : (∃ a, a' = a ∧ p a) ↔ p a' := by simp [@eq_comm _ a'] + +@[simp] theorem forall_eq_or_imp : (∀ a, a = a' ∨ q a → p a) ↔ p a' ∧ ∀ a, q a → p a := by + simp only [or_imp, forall_and, forall_eq] + +@[simp] theorem exists_eq_or_imp : (∃ a, (a = a' ∨ q a) ∧ p a) ↔ p a' ∨ ∃ a, q a ∧ p a := by + simp only [or_and_right, exists_or, exists_eq_left] + +@[simp] theorem exists_eq_right_right : (∃ (a : α), p a ∧ q a ∧ a = a') ↔ p a' ∧ q a' := by + simp [← and_assoc] + +@[simp] theorem exists_eq_right_right' : (∃ (a : α), p a ∧ q a ∧ a' = a) ↔ p a' ∧ q a' := by + simp [@eq_comm _ a'] + +@[simp] theorem exists_prop : (∃ _h : a, b) ↔ a ∧ b := + ⟨fun ⟨hp, hq⟩ => ⟨hp, hq⟩, fun ⟨hp, hq⟩ => ⟨hp, hq⟩⟩ + +@[simp] theorem exists_apply_eq_apply (f : α → β) (a' : α) : ∃ a, f a = f a' := ⟨a', rfl⟩ + +theorem forall_prop_of_true {p : Prop} {q : p → Prop} (h : p) : (∀ h' : p, q h') ↔ q h := + @forall_const (q h) p ⟨h⟩ + +theorem forall_comm {p : α → β → Prop} : (∀ a b, p a b) ↔ (∀ b a, p a b) := + ⟨fun h b a => h a b, fun h a b => h b a⟩ + +theorem exists_comm {p : α → β → Prop} : (∃ a b, p a b) ↔ (∃ b a, p a b) := + ⟨fun ⟨a, b, h⟩ => ⟨b, a, h⟩, fun ⟨b, a, h⟩ => ⟨a, b, h⟩⟩ + +@[simp] theorem forall_apply_eq_imp_iff {f : α → β} {p : β → Prop} : + (∀ b a, f a = b → p b) ↔ ∀ a, p (f a) := by simp [forall_comm] + +@[simp] theorem forall_eq_apply_imp_iff {f : α → β} {p : β → Prop} : + (∀ b a, b = f a → p b) ↔ ∀ a, p (f a) := by simp [forall_comm] + +@[simp] theorem forall_apply_eq_imp_iff₂ {f : α → β} {p : α → Prop} {q : β → Prop} : + (∀ b a, p a → f a = b → q b) ↔ ∀ a, p a → q (f a) := + ⟨fun h a ha => h (f a) a ha rfl, fun h _ a ha hb => hb ▸ h a ha⟩ + +theorem forall_prop_of_false {p : Prop} {q : p → Prop} (hn : ¬p) : (∀ h' : p, q h') ↔ True := + iff_true_intro fun h => hn.elim h + +end quantifiers + +/-! ## decidable -/ + +theorem Decidable.not_not [Decidable p] : ¬¬p ↔ p := ⟨of_not_not, not_not_intro⟩ + +theorem Decidable.by_contra [Decidable p] : (¬p → False) → p := of_not_not + +/-- Construct a non-Prop by cases on an `Or`, when the left conjunct is decidable. -/ +protected def Or.by_cases [Decidable p] {α : Sort u} (h : p ∨ q) (h₁ : p → α) (h₂ : q → α) : α := + if hp : p then h₁ hp else h₂ (h.resolve_left hp) + +/-- Construct a non-Prop by cases on an `Or`, when the right conjunct is decidable. -/ +protected def Or.by_cases' [Decidable q] {α : Sort u} (h : p ∨ q) (h₁ : p → α) (h₂ : q → α) : α := + if hq : q then h₂ hq else h₁ (h.resolve_right hq) + +instance exists_prop_decidable {p} (P : p → Prop) + [Decidable p] [∀ h, Decidable (P h)] : Decidable (∃ h, P h) := +if h : p then + decidable_of_decidable_of_iff ⟨fun h2 => ⟨h, h2⟩, fun ⟨_, h2⟩ => h2⟩ +else isFalse fun ⟨h', _⟩ => h h' + +instance forall_prop_decidable {p} (P : p → Prop) + [Decidable p] [∀ h, Decidable (P h)] : Decidable (∀ h, P h) := +if h : p then + decidable_of_decidable_of_iff ⟨fun h2 _ => h2, fun al => al h⟩ +else isTrue fun h2 => absurd h2 h + +theorem decide_eq_true_iff (p : Prop) [Decidable p] : (decide p = true) ↔ p := by simp + +@[simp] theorem decide_eq_false_iff_not (p : Prop) {_ : Decidable p} : (decide p = false) ↔ ¬p := + ⟨of_decide_eq_false, decide_eq_false⟩ + +@[simp] theorem decide_eq_decide {p q : Prop} {_ : Decidable p} {_ : Decidable q} : + decide p = decide q ↔ (p ↔ q) := + ⟨fun h => by rw [← decide_eq_true_iff p, h, decide_eq_true_iff], fun h => by simp [h]⟩ + +theorem Decidable.of_not_imp [Decidable a] (h : ¬(a → b)) : a := + byContradiction (not_not_of_not_imp h) + +theorem Decidable.not_imp_symm [Decidable a] (h : ¬a → b) (hb : ¬b) : a := + byContradiction <| hb ∘ h + +theorem Decidable.not_imp_comm [Decidable a] [Decidable b] : (¬a → b) ↔ (¬b → a) := + ⟨not_imp_symm, not_imp_symm⟩ + +theorem Decidable.not_imp_self [Decidable a] : (¬a → a) ↔ a := by + have := @imp_not_self (¬a); rwa [not_not] at this + +theorem Decidable.or_iff_not_imp_left [Decidable a] : a ∨ b ↔ (¬a → b) := + ⟨Or.resolve_left, fun h => dite _ .inl (.inr ∘ h)⟩ + +theorem Decidable.or_iff_not_imp_right [Decidable b] : a ∨ b ↔ (¬b → a) := + or_comm.trans or_iff_not_imp_left + +theorem Decidable.not_imp_not [Decidable a] : (¬a → ¬b) ↔ (b → a) := + ⟨fun h hb => byContradiction (h · hb), mt⟩ + +theorem Decidable.not_or_of_imp [Decidable a] (h : a → b) : ¬a ∨ b := + if ha : a then .inr (h ha) else .inl ha + +theorem Decidable.imp_iff_not_or [Decidable a] : (a → b) ↔ (¬a ∨ b) := + ⟨not_or_of_imp, Or.neg_resolve_left⟩ + +theorem Decidable.imp_iff_or_not [Decidable b] : b → a ↔ a ∨ ¬b := + Decidable.imp_iff_not_or.trans or_comm + +theorem Decidable.imp_or [h : Decidable a] : (a → b ∨ c) ↔ (a → b) ∨ (a → c) := + if h : a then by + rw [imp_iff_right h, imp_iff_right h, imp_iff_right h] + else by + rw [iff_false_intro h, false_imp_iff, false_imp_iff, true_or] + +theorem Decidable.imp_or' [Decidable b] : (a → b ∨ c) ↔ (a → b) ∨ (a → c) := + if h : b then by simp [h] else by + rw [eq_false h, false_or]; exact (or_iff_right_of_imp fun hx x => (hx x).elim).symm + +theorem Decidable.not_imp_iff_and_not [Decidable a] : ¬(a → b) ↔ a ∧ ¬b := + ⟨fun h => ⟨of_not_imp h, not_of_not_imp h⟩, not_imp_of_and_not⟩ + +theorem Decidable.peirce (a b : Prop) [Decidable a] : ((a → b) → a) → a := + if ha : a then fun _ => ha else fun h => h ha.elim + +theorem peirce' {a : Prop} (H : ∀ b : Prop, (a → b) → a) : a := H _ id + +theorem Decidable.not_iff_not [Decidable a] [Decidable b] : (¬a ↔ ¬b) ↔ (a ↔ b) := by + rw [@iff_def (¬a), @iff_def' a]; exact and_congr not_imp_not not_imp_not + +theorem Decidable.not_iff_comm [Decidable a] [Decidable b] : (¬a ↔ b) ↔ (¬b ↔ a) := by + rw [@iff_def (¬a), @iff_def (¬b)]; exact and_congr not_imp_comm imp_not_comm + +theorem Decidable.not_iff [Decidable b] : ¬(a ↔ b) ↔ (¬a ↔ b) := + if h : b then by + rw [iff_true_right h, iff_true_right h] + else by + rw [iff_false_right h, iff_false_right h] + +theorem Decidable.iff_not_comm [Decidable a] [Decidable b] : (a ↔ ¬b) ↔ (b ↔ ¬a) := by + rw [@iff_def a, @iff_def b]; exact and_congr imp_not_comm not_imp_comm + +theorem Decidable.iff_iff_and_or_not_and_not {a b : Prop} [Decidable b] : + (a ↔ b) ↔ (a ∧ b) ∨ (¬a ∧ ¬b) := + ⟨fun e => if h : b then .inl ⟨e.2 h, h⟩ else .inr ⟨mt e.1 h, h⟩, + Or.rec (And.rec iff_of_true) (And.rec iff_of_false)⟩ + +theorem Decidable.iff_iff_not_or_and_or_not [Decidable a] [Decidable b] : + (a ↔ b) ↔ (¬a ∨ b) ∧ (a ∨ ¬b) := by + rw [iff_iff_implies_and_implies a b]; simp only [imp_iff_not_or, Or.comm] + +theorem Decidable.not_and_not_right [Decidable b] : ¬(a ∧ ¬b) ↔ (a → b) := + ⟨fun h ha => not_imp_symm (And.intro ha) h, fun h ⟨ha, hb⟩ => hb <| h ha⟩ + +theorem Decidable.not_and_iff_or_not_not [Decidable a] : ¬(a ∧ b) ↔ ¬a ∨ ¬b := + ⟨fun h => if ha : a then .inr (h ⟨ha, ·⟩) else .inl ha, not_and_of_not_or_not⟩ + +theorem Decidable.not_and_iff_or_not_not' [Decidable b] : ¬(a ∧ b) ↔ ¬a ∨ ¬b := + ⟨fun h => if hb : b then .inl (h ⟨·, hb⟩) else .inr hb, not_and_of_not_or_not⟩ + +theorem Decidable.or_iff_not_and_not [Decidable a] [Decidable b] : a ∨ b ↔ ¬(¬a ∧ ¬b) := by + rw [← not_or, not_not] + +theorem Decidable.and_iff_not_or_not [Decidable a] [Decidable b] : a ∧ b ↔ ¬(¬a ∨ ¬b) := by + rw [← not_and_iff_or_not_not, not_not] + +theorem Decidable.imp_iff_right_iff [Decidable a] : (a → b ↔ b) ↔ a ∨ b := + ⟨fun H => (Decidable.em a).imp_right fun ha' => H.1 fun ha => (ha' ha).elim, + fun H => H.elim imp_iff_right fun hb => iff_of_true (fun _ => hb) hb⟩ + +theorem Decidable.and_or_imp [Decidable a] : a ∧ b ∨ (a → c) ↔ a → b ∨ c := + if ha : a then by simp only [ha, true_and, true_imp_iff] + else by simp only [ha, false_or, false_and, false_imp_iff] + +theorem Decidable.or_congr_left' [Decidable c] (h : ¬c → (a ↔ b)) : a ∨ c ↔ b ∨ c := by + rw [or_iff_not_imp_right, or_iff_not_imp_right]; exact imp_congr_right h + +theorem Decidable.or_congr_right' [Decidable a] (h : ¬a → (b ↔ c)) : a ∨ b ↔ a ∨ c := by + rw [or_iff_not_imp_left, or_iff_not_imp_left]; exact imp_congr_right h + +/-- Transfer decidability of `a` to decidability of `b`, if the propositions are equivalent. +**Important**: this function should be used instead of `rw` on `Decidable b`, because the +kernel will get stuck reducing the usage of `propext` otherwise, +and `decide` will not work. -/ +@[inline] def decidable_of_iff (a : Prop) (h : a ↔ b) [Decidable a] : Decidable b := + decidable_of_decidable_of_iff h + +/-- Transfer decidability of `b` to decidability of `a`, if the propositions are equivalent. +This is the same as `decidable_of_iff` but the iff is flipped. -/ +@[inline] def decidable_of_iff' (b : Prop) (h : a ↔ b) [Decidable b] : Decidable a := + decidable_of_decidable_of_iff h.symm + +instance Decidable.predToBool (p : α → Prop) [DecidablePred p] : + CoeDep (α → Prop) p (α → Bool) := ⟨fun b => decide <| p b⟩ + +/-- Prove that `a` is decidable by constructing a boolean `b` and a proof that `b ↔ a`. +(This is sometimes taken as an alternate definition of decidability.) -/ +def decidable_of_bool : ∀ (b : Bool), (b ↔ a) → Decidable a + | true, h => isTrue (h.1 rfl) + | false, h => isFalse (mt h.2 Bool.noConfusion) + +protected theorem Decidable.not_forall {p : α → Prop} [Decidable (∃ x, ¬p x)] + [∀ x, Decidable (p x)] : (¬∀ x, p x) ↔ ∃ x, ¬p x := + ⟨Decidable.not_imp_symm fun nx x => Decidable.not_imp_symm (fun h => ⟨x, h⟩) nx, + not_forall_of_exists_not⟩ + +protected theorem Decidable.not_forall_not {p : α → Prop} [Decidable (∃ x, p x)] : + (¬∀ x, ¬p x) ↔ ∃ x, p x := + (@Decidable.not_iff_comm _ _ _ (decidable_of_iff (¬∃ x, p x) not_exists)).1 not_exists + +protected theorem Decidable.not_exists_not {p : α → Prop} [∀ x, Decidable (p x)] : + (¬∃ x, ¬p x) ↔ ∀ x, p x := by + simp only [not_exists, Decidable.not_not] diff --git a/src/Init/SimpLemmas.lean b/src/Init/SimpLemmas.lean index 9467d019dc..2accd35190 100644 --- a/src/Init/SimpLemmas.lean +++ b/src/Init/SimpLemmas.lean @@ -31,6 +31,9 @@ theorem eq_false_of_decide {p : Prop} {_ : Decidable p} (h : decide p = false) : theorem implies_congr {p₁ p₂ : Sort u} {q₁ q₂ : Sort v} (h₁ : p₁ = p₂) (h₂ : q₁ = q₂) : (p₁ → q₁) = (p₂ → q₂) := h₁ ▸ h₂ ▸ rfl +theorem iff_congr {p₁ p₂ q₁ q₂ : Prop} (h₁ : p₁ ↔ p₂) (h₂ : q₁ ↔ q₂) : (p₁ ↔ q₁) ↔ (p₂ ↔ q₂) := + Iff.of_eq (propext h₁ ▸ propext h₂ ▸ rfl) + theorem implies_dep_congr_ctx {p₁ p₂ q₁ : Prop} (h₁ : p₁ = p₂) {q₂ : p₂ → Prop} (h₂ : (h : p₂) → q₁ = q₂ h) : (p₁ → q₁) = ((h : p₂) → q₂ h) := propext ⟨ fun hl hp₂ => (h₂ hp₂).mp (hl (h₁.mpr hp₂)), @@ -93,11 +96,16 @@ theorem dite_cond_eq_true {α : Sort u} {c : Prop} {_ : Decidable c} {t : c → theorem dite_cond_eq_false {α : Sort u} {c : Prop} {_ : Decidable c} {t : c → α} {e : ¬ c → α} (h : c = False) : (dite c t e) = e (of_eq_false h) := by simp [h] end SimprocHelperLemmas @[simp] theorem ite_self {α : Sort u} {c : Prop} {d : Decidable c} (a : α) : ite c a a = a := by cases d <;> rfl -@[simp] theorem and_self (p : Prop) : (p ∧ p) = p := propext ⟨(·.1), fun h => ⟨h, h⟩⟩ + @[simp] theorem and_true (p : Prop) : (p ∧ True) = p := propext ⟨(·.1), (⟨·, trivial⟩)⟩ @[simp] theorem true_and (p : Prop) : (True ∧ p) = p := propext ⟨(·.2), (⟨trivial, ·⟩)⟩ @[simp] theorem and_false (p : Prop) : (p ∧ False) = False := eq_false (·.2) @[simp] theorem false_and (p : Prop) : (False ∧ p) = False := eq_false (·.1) +@[simp] theorem and_self (p : Prop) : (p ∧ p) = p := propext ⟨(·.left), fun h => ⟨h, h⟩⟩ +@[simp] theorem and_not_self : ¬(a ∧ ¬a) | ⟨ha, hn⟩ => absurd ha hn +@[simp] theorem not_and_self : ¬(¬a ∧ a) := and_not_self ∘ And.symm +@[simp] theorem and_imp : (a ∧ b → c) ↔ (a → b → c) := ⟨fun h ha hb => h ⟨ha, hb⟩, fun h ⟨ha, hb⟩ => h ha hb⟩ +@[simp] theorem not_and : ¬(a ∧ b) ↔ (a → ¬b) := and_imp @[simp] theorem or_self (p : Prop) : (p ∨ p) = p := propext ⟨fun | .inl h | .inr h => h, .inl⟩ @[simp] theorem or_true (p : Prop) : (p ∨ True) = True := eq_true (.inr trivial) @[simp] theorem true_or (p : Prop) : (True ∨ p) = True := eq_true (.inl trivial) @@ -114,6 +122,58 @@ end SimprocHelperLemmas @[simp] theorem not_false_eq_true : (¬ False) = True := eq_true False.elim @[simp] theorem not_true_eq_false : (¬ True) = False := by decide +@[simp] theorem not_iff_self : ¬(¬a ↔ a) | H => iff_not_self H.symm + +/-! ## and -/ + +theorem and_congr_right (h : a → (b ↔ c)) : a ∧ b ↔ a ∧ c := + Iff.intro (fun ⟨ha, hb⟩ => And.intro ha ((h ha).mp hb)) + (fun ⟨ha, hb⟩ => And.intro ha ((h ha).mpr hb)) +theorem and_congr_left (h : c → (a ↔ b)) : a ∧ c ↔ b ∧ c := + Iff.trans and_comm (Iff.trans (and_congr_right h) and_comm) + +theorem and_assoc : (a ∧ b) ∧ c ↔ a ∧ (b ∧ c) := + Iff.intro (fun ⟨⟨ha, hb⟩, hc⟩ => ⟨ha, hb, hc⟩) + (fun ⟨ha, hb, hc⟩ => ⟨⟨ha, hb⟩, hc⟩) + +@[simp] theorem and_self_left : a ∧ (a ∧ b) ↔ a ∧ b := by rw [←propext and_assoc, and_self] +@[simp] theorem and_self_right : (a ∧ b) ∧ b ↔ a ∧ b := by rw [ propext and_assoc, and_self] + +@[simp] theorem and_congr_right_iff : (a ∧ b ↔ a ∧ c) ↔ (a → (b ↔ c)) := + Iff.intro (fun h ha => by simp [ha] at h; exact h) and_congr_right +@[simp] theorem and_congr_left_iff : (a ∧ c ↔ b ∧ c) ↔ c → (a ↔ b) := by + rw [@and_comm _ c, @and_comm _ c, ← and_congr_right_iff] + +theorem and_iff_left_of_imp (h : a → b) : (a ∧ b) ↔ a := Iff.intro And.left (fun ha => And.intro ha (h ha)) +theorem and_iff_right_of_imp (h : b → a) : (a ∧ b) ↔ b := Iff.trans And.comm (and_iff_left_of_imp h) + +@[simp] theorem and_iff_left_iff_imp : ((a ∧ b) ↔ a) ↔ (a → b) := Iff.intro (And.right ∘ ·.mpr) and_iff_left_of_imp +@[simp] theorem and_iff_right_iff_imp : ((a ∧ b) ↔ b) ↔ (b → a) := Iff.intro (And.left ∘ ·.mpr) and_iff_right_of_imp + +@[simp] theorem iff_self_and : (p ↔ p ∧ q) ↔ (p → q) := by rw [@Iff.comm p, and_iff_left_iff_imp] +@[simp] theorem iff_and_self : (p ↔ q ∧ p) ↔ (p → q) := by rw [and_comm, iff_self_and] + +/-! ## or -/ + +theorem Or.imp (f : a → c) (g : b → d) (h : a ∨ b) : c ∨ d := h.elim (inl ∘ f) (inr ∘ g) +theorem Or.imp_left (f : a → b) : a ∨ c → b ∨ c := .imp f id +theorem Or.imp_right (f : b → c) : a ∨ b → a ∨ c := .imp id f + +theorem or_assoc : (a ∨ b) ∨ c ↔ a ∨ (b ∨ c) := + Iff.intro (.rec (.imp_right .inl) (.inr ∘ .inr)) + (.rec (.inl ∘ .inl) (.imp_left .inr)) + +@[simp] theorem or_self_left : a ∨ (a ∨ b) ↔ a ∨ b := by rw [←propext or_assoc, or_self] +@[simp] theorem or_self_right : (a ∨ b) ∨ b ↔ a ∨ b := by rw [ propext or_assoc, or_self] + +theorem or_iff_right_of_imp (ha : a → b) : (a ∨ b) ↔ b := Iff.intro (Or.rec ha id) .inr +theorem or_iff_left_of_imp (hb : b → a) : (a ∨ b) ↔ a := Iff.intro (Or.rec id hb) .inl + +@[simp] theorem or_iff_left_iff_imp : (a ∨ b ↔ a) ↔ (b → a) := Iff.intro (·.mp ∘ Or.inr) or_iff_left_of_imp +@[simp] theorem or_iff_right_iff_imp : (a ∨ b ↔ b) ↔ (a → b) := by rw [or_comm, or_iff_left_iff_imp] + +/-# Bool -/ + @[simp] theorem Bool.or_false (b : Bool) : (b || false) = b := by cases b <;> rfl @[simp] theorem Bool.or_true (b : Bool) : (b || true) = true := by cases b <;> rfl @[simp] theorem Bool.false_or (b : Bool) : (false || b) = b := by cases b <;> rfl @@ -166,11 +226,13 @@ theorem Bool.or_assoc (a b c : Bool) : (a || b || c) = (a || (b || c)) := by @[simp] theorem bne_self_eq_false [BEq α] [LawfulBEq α] (a : α) : (a != a) = false := by simp [bne] @[simp] theorem bne_self_eq_false' [DecidableEq α] (a : α) : (a != a) = false := by simp [bne] -@[simp] theorem Nat.le_zero_eq (a : Nat) : (a ≤ 0) = (a = 0) := - propext ⟨fun h => Nat.le_antisymm h (Nat.zero_le ..), fun h => by rw [h]; decide⟩ - @[simp] theorem decide_False : decide False = false := rfl @[simp] theorem decide_True : decide True = true := rfl @[simp] theorem bne_iff_ne [BEq α] [LawfulBEq α] (a b : α) : a != b ↔ a ≠ b := by simp [bne]; rw [← beq_iff_eq a b]; simp [-beq_iff_eq] + +/-# Nat -/ + +@[simp] theorem Nat.le_zero_eq (a : Nat) : (a ≤ 0) = (a = 0) := + propext ⟨fun h => Nat.le_antisymm h (Nat.zero_le ..), fun h => by rw [h]; decide⟩ diff --git a/tests/lean/1079.lean.expected.out b/tests/lean/1079.lean.expected.out index 0e3cf3de70..f40dfe5257 100644 --- a/tests/lean/1079.lean.expected.out +++ b/tests/lean/1079.lean.expected.out @@ -5,4 +5,32 @@ ?a = ?a with Ordering.eq = Ordering.lt -[Meta.Tactic.simp.rewrite] false_implies:1000, False → False ==> True +[Meta.Tactic.simp.unify] @forall_exists_index:1000, failed to unify + ∀ (h : ∃ x, ?p x), ?q h + with + False → False +[Meta.Tactic.simp.unify] @forall_eq:1000, failed to unify + ∀ (a : ?α), a = ?a' → ?p a + with + False → False +[Meta.Tactic.simp.unify] @forall_eq':1000, failed to unify + ∀ (a : ?α), ?a' = a → ?p a + with + False → False +[Meta.Tactic.simp.unify] @forall_eq_or_imp:1000, failed to unify + ∀ (a : ?α), a = ?a' ∨ ?q a → ?p a + with + False → False +[Meta.Tactic.simp.unify] @forall_apply_eq_imp_iff:1000, failed to unify + ∀ (b : ?β) (a : ?α), ?f a = b → ?p b + with + False → False +[Meta.Tactic.simp.unify] @forall_eq_apply_imp_iff:1000, failed to unify + ∀ (b : ?β) (a : ?α), b = ?f a → ?p b + with + False → False +[Meta.Tactic.simp.unify] @forall_apply_eq_imp_iff₂:1000, failed to unify + ∀ (b : ?β) (a : ?α), ?p a → ?f a = b → ?q b + with + False → False +[Meta.Tactic.simp.rewrite] @imp_self:1000, False → False ==> True diff --git a/tests/lean/276.lean b/tests/lean/276.lean index 36905318c8..bae43741a8 100644 --- a/tests/lean/276.lean +++ b/tests/lean/276.lean @@ -6,4 +6,4 @@ set_option pp.all true in -- but `def` doesn't work -- error: (kernel) compiler failed to infer low level type, unknown declaration 'PEmpty.rec' -def PEmpty.elim {α : Sort v} := PEmpty.rec (fun _ => α) +def PEmpty.elim' {α : Sort v} := PEmpty.rec (fun _ => α) diff --git a/tests/lean/276.lean.expected.out b/tests/lean/276.lean.expected.out index cb778a59bf..35e51a5f70 100644 --- a/tests/lean/276.lean.expected.out +++ b/tests/lean/276.lean.expected.out @@ -1,3 +1,3 @@ 276.lean:5:27-5:50: error: failed to elaborate eliminator, expected type is not available fun {α : Sort v} => @?m α : {α : Sort v} → @?m α -276.lean:9:32-9:55: error: failed to elaborate eliminator, expected type is not available +276.lean:9:33-9:56: error: failed to elaborate eliminator, expected type is not available diff --git a/tests/lean/run/1549.lean b/tests/lean/run/1549.lean index faf97f20c1..8b38c3f5dd 100644 --- a/tests/lean/run/1549.lean +++ b/tests/lean/run/1549.lean @@ -1,16 +1,12 @@ theorem not_mem_nil (a : Nat) : ¬ a ∈ [] := fun x => nomatch x -theorem forall_prop_of_false {p : Prop} {q : p → Prop} (hn : ¬ p) : - (∀ h' : p, q h') ↔ True := sorry - example (R : Nat → Prop) : (∀ (a' : Nat), a' ∈ [] → R a') := by simp only [forall_prop_of_false (not_mem_nil _)] exact fun _ => True.intro - -def Not.elim {α : Sort _} (H1 : ¬a) (H2 : a) : α := absurd H2 H1 -theorem iff_of_true (ha : a) (hb : b) : a ↔ b := ⟨fun _ => hb, fun _ => ha⟩ -theorem iff_true_intro (h : a) : a ↔ True := iff_of_true h ⟨⟩ +def Not.elim' {α : Sort _} (H1 : ¬a) (H2 : a) : α := absurd H2 H1 +theorem iff_of_true' (ha : a) (hb : b) : a ↔ b := ⟨fun _ => hb, fun _ => ha⟩ +theorem iff_true_intro' (h : a) : a ↔ True := iff_of_true h ⟨⟩ example {P : Prop} : ∀ (x : Nat) (_ : x ∈ []), P := by diff --git a/tests/lean/run/1842.lean b/tests/lean/run/1842.lean index c896679e11..0db8144bf0 100644 --- a/tests/lean/run/1842.lean +++ b/tests/lean/run/1842.lean @@ -4,12 +4,6 @@ inductive List.Pairwise : List α → Prop | nil : Pairwise [] | cons : ∀ {a : α} {l : List α}, (∀ {a} (_ : a' ∈ l), R a a') → Pairwise l → Pairwise (a :: l) -theorem and_assoc : (a ∧ b) ∧ c ↔ a ∧ (b ∧ c) := - ⟨fun ⟨⟨ha, hb⟩, hc⟩ => ⟨ha, hb, hc⟩, fun ⟨ha, hb, hc⟩ => ⟨⟨ha, hb⟩, hc⟩⟩ - -theorem and_left_comm : a ∧ (b ∧ c) ↔ b ∧ (a ∧ c) := by - rw [← and_assoc, ← and_assoc, @And.comm a b] - theorem pairwise_append {l₁ l₂ : List α} : (l₁ ++ l₂).Pairwise R ↔ l₁.Pairwise R ∧ l₂.Pairwise R ∧ ∀ {a} (_ : a ∈ l₁), ∀ {b} (_ : b ∈ l₂), R a b := by induction l₁ <;> simp [*, and_left_comm] diff --git a/tests/lean/run/2552.lean b/tests/lean/run/2552.lean index 3053252dbd..bfb3f05fd3 100644 --- a/tests/lean/run/2552.lean +++ b/tests/lean/run/2552.lean @@ -1,4 +1,4 @@ -@[inline] def decidable_of_iff {b : Prop} (a : Prop) (h : a ↔ b) [Decidable a] : Decidable b := +@[inline] def decidable_of_iff'' {b : Prop} (a : Prop) (h : a ↔ b) [Decidable a] : Decidable b := decidable_of_decidable_of_iff h theorem LE.le.lt_or_eq_dec {a b : Nat} (hab : a ≤ b) : a < b ∨ a = b := diff --git a/tests/lean/run/968.lean b/tests/lean/run/968.lean index 89d41553d0..7e8c127503 100644 --- a/tests/lean/run/968.lean +++ b/tests/lean/run/968.lean @@ -1,9 +1,3 @@ -theorem and_comm (a b : Prop) : (a ∧ b) = (b ∧ a) := sorry - -theorem and_assoc (a b c : Prop) : ((a ∧ b) ∧ c) = (a ∧ (b ∧ c)):= sorry - -theorem and_left_comm (a b c : Prop) : (a ∧ (b ∧ c)) = (b ∧ (a ∧ c)) := sorry - example (p q r : Prop) : (p ∧ q ∧ r) = (r ∧ p ∧ q) := by simp only [and_comm, and_left_comm, and_assoc] diff --git a/tests/lean/run/ac_rfl.lean b/tests/lean/run/ac_rfl.lean index 5250cefb53..63d15f9bb4 100644 --- a/tests/lean/run/ac_rfl.lean +++ b/tests/lean/run/ac_rfl.lean @@ -34,12 +34,6 @@ theorem le_of_not_le {a b : Nat} (h : ¬ a ≤ b) : b ≤ a := · exact Iff.intro .inr fun | .inl xy => Nat.le_trans ‹_› ‹_› | .inr xz => ‹_› · exact Iff.intro .inl fun | .inl xy => ‹_› | .inr xz => Nat.le_trans ‹_› (le_of_not_le ‹_›) -theorem or_assoc : (p ∨ q) ∨ r ↔ p ∨ (q ∨ r) := by - by_cases p <;> by_cases q <;> by_cases r <;> simp_all - -theorem or_comm : p ∨ q ↔ q ∨ p := by - by_cases p <;> by_cases q <;> simp_all - theorem max_assoc (n m k : Nat) : max (max n m) k = max n (max m k) := le_ext (by simp [or_assoc]) diff --git a/tests/lean/run/constProp.lean b/tests/lean/run/constProp.lean index 28ed047673..f5a1a62f99 100644 --- a/tests/lean/run/constProp.lean +++ b/tests/lean/run/constProp.lean @@ -526,11 +526,7 @@ theorem State.update_le_update (h : σ' ≼ σ) : σ'.update x v ≼ σ.update x simp [*] at he assumption next => - by_cases hxy : x = y <;> simp [*] - next => intros; assumption - next => - intro he' ih - exact ih he' + by_cases hxy : x = y <;> simp_all theorem Expr.eval_constProp_of_sub (e : Expr) (h : σ' ≼ σ) : (e.constProp σ').eval σ = e.eval σ := by induction e with simp [*] diff --git a/tests/lean/run/eq_some_iff_get_eq_issue.lean b/tests/lean/run/eq_some_iff_get_eq_issue.lean index 7adc3d1de1..ce8d9a4e19 100644 --- a/tests/lean/run/eq_some_iff_get_eq_issue.lean +++ b/tests/lean/run/eq_some_iff_get_eq_issue.lean @@ -1,6 +1,3 @@ -@[simp] -theorem exists_prop {p q : Prop} : (∃ h : p, q) ↔ p ∧ q := -Iff.intro (fun ⟨hp, hq⟩ => And.intro hp hq) (fun ⟨hp, hq⟩ => Exists.intro hp hq) namespace Option @@ -13,5 +10,5 @@ def get {α : Type u} : ∀ {o : Option α}, isSome o → α theorem eq_some_iff_get_eq {o : Option α} {a : α} : o = some a ↔ ∃ h : o.isSome, Option.get h = a := by - cases o; simp; intro h; cases h; contradiction + cases o; simp only [isSome_none, false_iff]; intro h; cases h; contradiction simp [exists_prop] diff --git a/tests/lean/run/recInfo1.lean b/tests/lean/run/recInfo1.lean index fa38cb19fc..d33fb0d50e 100644 --- a/tests/lean/run/recInfo1.lean +++ b/tests/lean/run/recInfo1.lean @@ -10,9 +10,6 @@ def showRecInfo (declName : Name) (majorPos? : Option Nat := none) : MetaM Unit let info ← mkRecursorInfo declName majorPos? print (toString info) -theorem Iff.elim {a b c} (h₁ : (a → b) → (b → a) → c) (h₂ : a ↔ b) : c := - h₁ h₂.1 h₂.2 - set_option trace.Meta true set_option trace.Meta.isDefEq false diff --git a/tests/lean/run/simp4.lean b/tests/lean/run/simp4.lean index 19277d45cf..ccd0f74455 100644 --- a/tests/lean/run/simp4.lean +++ b/tests/lean/run/simp4.lean @@ -56,8 +56,6 @@ theorem ex9 (y x : Nat) : y = 0 → x + y = 0 → x = 0 := by theorem ex10 (y x : Nat) : y = 0 → x + 0 = 0 → x = 0 := by simp - intro h₁ h₂ - simp [h₂] theorem ex11 : ∀ x : Nat, 0 + x + 0 = x := by simp diff --git a/tests/lean/run/simp6.lean b/tests/lean/run/simp6.lean index c9006bab76..59ecb1b5a3 100644 --- a/tests/lean/run/simp6.lean +++ b/tests/lean/run/simp6.lean @@ -21,7 +21,8 @@ theorem ex6 : (if "hello" = "world" then 1 else 2) = 2 := #print ex6 theorem ex7 : (if "hello" = "world" then 1 else 2) = 2 := by - fail_if_success simp (config := { decide := false }) + simp (config := { decide := false }) + -- Goal is now `⊢ "hello" = "world" → False` simp (config := { decide := true }) theorem ex8 : (10 + 2000 = 20) = False := diff --git a/tests/lean/run/wfOverapplicationIssue.lean b/tests/lean/run/wfOverapplicationIssue.lean index 0636801242..acaf6af1ce 100644 --- a/tests/lean/run/wfOverapplicationIssue.lean +++ b/tests/lean/run/wfOverapplicationIssue.lean @@ -4,7 +4,7 @@ theorem Array.sizeOf_lt_of_mem' [DecidableEq α] [SizeOf α] {as : Array α} (h unfold anyM.loop intro h split at h - · simp [Bind.bind, pure] at h; split at h + · simp only [bind, decide_eq_true_eq, pure] at h; split at h next he => subst a; apply sizeOf_get_lt next => have ih := aux (j+1) h; assumption · contradiction diff --git a/tests/lean/simp_trace.lean.expected.out b/tests/lean/simp_trace.lean.expected.out index 816a8d9308..4f92e81a9e 100644 --- a/tests/lean/simp_trace.lean.expected.out +++ b/tests/lean/simp_trace.lean.expected.out @@ -46,10 +46,12 @@ Try this: simp only [h, Nat.sub_add_cancel] [Meta.Tactic.simp.rewrite] h:1000, 1 ≤ x ==> True [Meta.Tactic.simp.rewrite] @Nat.sub_add_cancel:1000, x - 1 + 1 ==> x [Meta.Tactic.simp.rewrite] @eq_self:1000, x + 2 = x + 2 ==> True -Try this: simp (config := { contextual := true }) only [Nat.sub_add_cancel] +Try this: simp (config := { contextual := true }) only [Nat.sub_add_cancel, dite_eq_ite] [Meta.Tactic.simp.rewrite] h:1000, 1 ≤ x ==> True [Meta.Tactic.simp.rewrite] @Nat.sub_add_cancel:1000, x - 1 + 1 ==> x -[Meta.Tactic.simp.rewrite] @eq_self:1000, (if h : 1 ≤ x then x else 0) = if h : 1 ≤ x then x else 0 ==> True +[Meta.Tactic.simp.rewrite] @dite_eq_ite:1000, if h : 1 ≤ x then x else 0 ==> if 1 ≤ x then x else 0 +[Meta.Tactic.simp.rewrite] @dite_eq_ite:1000, if _h : 1 ≤ x then x else 0 ==> if 1 ≤ x then x else 0 +[Meta.Tactic.simp.rewrite] @eq_self:1000, (if 1 ≤ x then x else 0) = if 1 ≤ x then x else 0 ==> True Try this: simp only [and_self] [Meta.Tactic.simp.rewrite] and_self:1000, b ∧ b ==> b [Meta.Tactic.simp.rewrite] iff_self:1000, a ∧ b ↔ a ∧ b ==> True