diff --git a/Foundation.lean b/Foundation.lean index a0e0d24e8..23574c83a 100644 --- a/Foundation.lean +++ b/Foundation.lean @@ -1,4 +1,4 @@ -module -- shake: keep-all +module -- shake: keep-all --deprecated_module: ignore public import Foundation.FirstOrder.Arithmetic.Basic public import Foundation.FirstOrder.Arithmetic.Basic.Hierarchy diff --git a/Foundation/FirstOrder/Arithmetic/Basic/Hierarchy.lean b/Foundation/FirstOrder/Arithmetic/Basic/Hierarchy.lean index 176d0e1da..21eb0fce2 100644 --- a/Foundation/FirstOrder/Arithmetic/Basic/Hierarchy.lean +++ b/Foundation/FirstOrder/Arithmetic/Basic/Hierarchy.lean @@ -315,7 +315,7 @@ set_option linter.flexible false in lemma exsClosure : {n : ℕ} → {φ : Semiformula L ξ n} → Hierarchy 𝚺 (s + 1) φ → Hierarchy 𝚺 (s + 1) (exsClosure φ) | 0, _, hp => hp - | n + 1, φ, hp => by simpa using exsClosure (hp.exs) + | n + 1, φ, hp => exsClosure (φ := ∃⁰ φ) hp.exs instance : LogicalConnective.AndOrClosed (Hierarchy Γ s : Semiformula L ξ k → Prop) where verum := verum _ _ _ diff --git a/Foundation/FirstOrder/Arithmetic/Definability/Absoluteness.lean b/Foundation/FirstOrder/Arithmetic/Definability/Absoluteness.lean index 96b1bf4b3..fc72fc879 100644 --- a/Foundation/FirstOrder/Arithmetic/Definability/Absoluteness.lean +++ b/Foundation/FirstOrder/Arithmetic/Definability/Absoluteness.lean @@ -30,7 +30,7 @@ lemma Defined.shigmaZero_absolute {k} {R : (Fin k → ℕ) → Prop} {R' : (Fin lemma DefinedFunction.shigmaZero_absolute_func {k} {f : (Fin k → ℕ) → ℕ} {f' : (Fin k → V) → V} {φ : 𝚺₀.Semisentence (k + 1)} (hf : 𝚺₀.DefinedFunction f φ) (hf' : 𝚺₀.DefinedFunction f' φ) (v : Fin k → ℕ) : (f v : V) = f' (Nat.cast ∘ v) := by - simpa using Defined.shigmaZero_absolute V hf hf' (f v :> v) + simpa [Function.comp_def] using Defined.shigmaZero_absolute V hf hf' (f v :> v) lemma sigmaOne_upward_absolute {k} (φ : 𝚺₁.Semisentence k) (v : Fin k → ℕ) : φ.val.Evalb v → φ.val.Evalb (M := V) (Nat.cast ∘ v) := by @@ -56,7 +56,7 @@ lemma Defined.shigmaOne_absolute {k} {R : (Fin k → ℕ) → Prop} {R' : (Fin k lemma DefinedFunction.shigmaOne_absolute_func {k} {f : (Fin k → ℕ) → ℕ} {f' : (Fin k → V) → V} {φ : 𝚺₁.Semisentence (k + 1)} (hf : 𝚺₁.DefinedFunction f φ) (hf' : 𝚺₁.DefinedFunction f' φ) (v : Fin k → ℕ) : (f v : V) = f' (Nat.cast ∘ v) := by - simpa using Defined.shigmaOne_absolute V hf.graph_delta hf'.graph_delta (f v :> v) + simpa [Function.comp_def] using Defined.shigmaOne_absolute V hf.graph_delta hf'.graph_delta (f v :> v) variable {V} diff --git a/Foundation/FirstOrder/Arithmetic/Definability/BoundedDefinable.lean b/Foundation/FirstOrder/Arithmetic/Definability/BoundedDefinable.lean index 6d3124deb..bafbc73f3 100644 --- a/Foundation/FirstOrder/Arithmetic/Definability/BoundedDefinable.lean +++ b/Foundation/FirstOrder/Arithmetic/Definability/BoundedDefinable.lean @@ -55,8 +55,8 @@ lemma comp [V↓[ℒₒᵣ] ⊧* 𝗣𝗔⁻] {k} {f : (Fin l → V) → V} {g : choose tg htg using fun i ↦ (hg i).bounded exact ⟨Rew.subst tg tf, by intro v - simpa [Semiterm.val_substs] - using le_trans (htf (g · v)) (Structure.Monotone.term_monotone tf (fun i ↦ htg i v) (by simp))⟩ + simpa [Semiterm.val_substs, Function.comp_def] + using! le_trans (htf (g · v)) (Structure.Monotone.term_monotone tf (fun i ↦ htg i v) (by simp))⟩ end Bounded diff --git a/Foundation/FirstOrder/Arithmetic/Definability/Hierarchy.lean b/Foundation/FirstOrder/Arithmetic/Definability/Hierarchy.lean index fa974206d..21c831033 100644 --- a/Foundation/FirstOrder/Arithmetic/Definability/Hierarchy.lean +++ b/Foundation/FirstOrder/Arithmetic/Definability/Hierarchy.lean @@ -169,7 +169,7 @@ lemma ProvablyProperOn.ofProperOn [𝗘𝗤 ℒₒᵣ ⪯ T] {φ : 𝚫-[m].Semi (h : ∀ (M : Type w) [ORingStructure M] [M↓[ℒₒᵣ] ⊧* T], φ.ProperOn M) : φ.ProvablyProperOn T := by apply FirstOrder.Arithmetic.complete.{w} T _ ?_ intro M _ _ - simpa [models_iff] using (h M).iff + simpa [models_iff] using! (h M).iff variable {T} diff --git a/Foundation/FirstOrder/Arithmetic/Exponential/Bit.lean b/Foundation/FirstOrder/Arithmetic/Exponential/Bit.lean index 65737a098..97ac1397e 100644 --- a/Foundation/FirstOrder/Arithmetic/Exponential/Bit.lean +++ b/Foundation/FirstOrder/Arithmetic/Exponential/Bit.lean @@ -186,10 +186,10 @@ end model section model lemma mem_iff_mul_exp_add_exp_add {i a : V} : i ∈ a ↔ ∃ k, ∃ r < Exp.exp i, a = k * Exp.exp (i + 1) + Exp.exp i + r := by - simpa [mem_iff_bit, exp_succ] using lenbit_iff_add_mul (exp_pow2 i) (a := a) + simpa [mem_iff_bit, exp_succ] using! lenbit_iff_add_mul (exp_pow2 i) (a := a) lemma not_mem_iff_mul_exp_add {i a : V} : i ∉ a ↔ ∃ k, ∃ r < Exp.exp i, a = k * Exp.exp (i + 1) + r := by - simpa [mem_iff_bit, exp_succ] using not_lenbit_iff_add_mul (exp_pow2 i) (a := a) + simpa [mem_iff_bit, exp_succ] using! not_lenbit_iff_add_mul (exp_pow2 i) (a := a) section empty @@ -239,13 +239,13 @@ instance : LawfulSingleton V V where i ∈ insert j a ↔ i = j ∨ i ∈ a := by by_cases h : j ∈ a <;> simp [h, insert_eq, bitInsert] · by_cases e : i = j <;> simp [h, e] - · simpa [exp_inj.eq_iff] using + · simpa [exp_inj.eq_iff] using! lenbit_add_pow2_iff_of_not_lenbit (exp_pow2 i) (exp_pow2 j) h @[simp] lemma mem_bitRemove_iff {i j a : V} : i ∈ bitRemove j a ↔ i ≠ j ∧ i ∈ a := by by_cases h : j ∈ a - · simpa [h, bitRemove, exp_inj.eq_iff] using + · simpa [h, bitRemove, exp_inj.eq_iff] using! lenbit_sub_pow2_iff_of_lenbit (exp_pow2 i) (exp_pow2 j) h · simp only [bitRemove, h, ↓reduceIte, ne_eq, iff_and_self] rintro _ rfl; contradiction @@ -442,7 +442,7 @@ lemma nonempty_of_pos {a : V} (h : 0 < a) : ∃ i, i ∈ a := by simp [this] at h lemma eq_empty_or_nonempty (a : V) : a = ∅ ∨ ∃ i, i ∈ a := by - rcases zero_le a with (rfl | pos) + rcases Arithmetic.zero_le a with (rfl | pos) · simp [emptyset_def] · right; exact nonempty_of_pos pos @@ -457,7 +457,7 @@ lemma isempty_iff {s : V} : s = ∅ ↔ ∀ x, x ∉ s := by @[simp] lemma empty_subset (s : V) : ∅ ⊆ s := by intro x; simp lemma lt_of_lt_log {a b : V} (pos : 0 < b) (h : ∀ i ∈ a, i < log b) : a < b := by - rcases zero_le a with (rfl | apos) + rcases Arithmetic.zero_le a with (rfl | apos) · exact pos by_contra A exact not_lt_of_ge (log_monotone <| show b ≤ a by simpa using A) (h (log a) (log_mem_of_pos apos)) diff --git a/Foundation/FirstOrder/Arithmetic/Exponential/Log.lean b/Foundation/FirstOrder/Arithmetic/Exponential/Log.lean index e68557e25..a207651ec 100644 --- a/Foundation/FirstOrder/Arithmetic/Exponential/Log.lean +++ b/Foundation/FirstOrder/Arithmetic/Exponential/Log.lean @@ -25,7 +25,7 @@ lemma log_exists_unique_pos {y : V} (hy : 0 < y) : ∃! x, x < y ∧ ∃ y' ≤ exact ⟨x + 1, lt_of_lt_of_le (by simp [hxy]) (succ_le_double_of_pos (pos_of_gt hxy)), 2 * y', by simpa using gey, Exponential.exponential_succ_mul_two.mpr H, by simpa using lty⟩ case odd y IH => - rcases (zero_le y : 0 ≤ y) with (rfl | pos) + rcases (Arithmetic.zero_le y : 0 ≤ y) with (rfl | pos) · simp · rcases (IH pos : ∃ x < y, ∃ y' ≤ y, Exponential x y' ∧ y < 2 * y') with ⟨x, hxy, y', gey, H, lty⟩ exact ⟨x + 1, by simpa using lt_of_lt_of_le hxy (by simp), @@ -62,7 +62,7 @@ lemma log_lt_self_of_pos {y : V} (pos : 0 < y) : log y < y := ((Classical.choose!_spec (log_exists_unique y)).2 pos).1 @[simp] lemma log_le_self (a : V) : log a ≤ a := by - rcases zero_le a with (rfl | pos) + rcases Arithmetic.zero_le a with (rfl | pos) · simp · exact le_of_lt <| log_lt_self_of_pos pos @@ -121,9 +121,9 @@ lemma log_mul_pow2 {a p : V} (pos : 0 < a) (pp : Pow2 p) : log (a * p) = log a + simpa using log_mul_pow2_add_of_lt pos pp pp.pos lemma log_monotone {a b : V} (h : a ≤ b) : log a ≤ log b := by - rcases zero_le a with (rfl | posa) + rcases Arithmetic.zero_le a with (rfl | posa) · simp - rcases zero_le b with (rfl | posb) + rcases Arithmetic.zero_le b with (rfl | posb) · have := lt_of_lt_of_le posa h; simp_all rcases log_pos posa with ⟨a', ha', Ha, _⟩ rcases log_pos posb with ⟨b', _, Hb, hb⟩ @@ -147,12 +147,12 @@ lemma length_eq_binaryLength (a : V) : ‖a‖ = if 0 < a then log a + 1 else 0 lemma length_of_pos {a : V} (pos : 0 < a) : ‖a‖ = log a + 1 := by simp [length_eq_binaryLength, pos] @[simp] lemma length_le (a : V) : ‖a‖ ≤ a := by - rcases zero_le a with (rfl | pos) + rcases Arithmetic.zero_le a with (rfl | pos) · simp · simp [pos, length_of_pos, ←lt_iff_succ_le, log_lt_self_of_pos] lemma length_graph {i a : V} : i = ‖a‖ ↔ (0 < a → ∃ k ≤ a, k = log a ∧ i = k + 1) ∧ (a = 0 → i = 0) := by - rcases zero_le a with (rfl | pos) + rcases Arithmetic.zero_le a with (rfl | pos) · simp · simp [length_of_pos, pos, pos_iff_ne_zero.mp pos] @@ -174,7 +174,7 @@ lemma length_two_mul_of_pos {a : V} (pos : 0 < a) : ‖2 * a‖ = ‖a‖ + 1 := simp [pos, length_of_pos, log_two_mul_of_pos] lemma length_two_mul_add_one (a : V) : ‖2 * a + 1‖ = ‖a‖ + 1 := by - rcases zero_le a with (rfl | pos) + rcases Arithmetic.zero_le a with (rfl | pos) · simp · simp [pos, length_of_pos, log_two_mul_add_one_of_pos] @@ -185,7 +185,7 @@ lemma length_mul_pow2 {a p : V} (pos : 0 < a) (pp : Pow2 p) : ‖a * p‖ = ‖a simp [length_of_pos, pos, pp.pos, log_mul_pow2 pos pp, add_right_comm (log a) (log p) 1] lemma length_monotone {a b : V} (h : a ≤ b) : ‖a‖ ≤ ‖b‖ := by - rcases zero_le a with (rfl | posa) + rcases Arithmetic.zero_le a with (rfl | posa) · simp · simpa [length_of_pos posa, length_of_pos (lt_of_lt_of_le posa h)] using log_monotone h @@ -208,13 +208,13 @@ lemma exponential_log_le_self {a b : V} (pos : 0 < a) (h : Exponential (log a) b assumption lemma lt_exponential_log_self {a b : V} (h : Exponential (log a) b) : a < 2 * b := by - rcases zero_le a with (rfl | pos) + rcases Arithmetic.zero_le a with (rfl | pos) · simp at h; simp [h] rcases log_pos pos with ⟨_, _, H, _⟩; rcases H.uniq h assumption lemma lt_exp_len_self {a b : V} (h : Exponential ‖a‖ b) : a < b := by - rcases zero_le a with (rfl | pos) + rcases Arithmetic.zero_le a with (rfl | pos) · simp at h; simp [h] have : Exponential (log a + 1) b := by simpa [length_of_pos pos] using h rcases Exponential.exponential_succ.mp this with ⟨b, rfl, H⟩ @@ -225,7 +225,7 @@ lemma le_iff_le_log_of_exp {x y a : V} (H : Exponential x y) (pos : 0 < a) : y fun h ↦ by rcases log_pos pos with ⟨a', ha', Haa', _⟩; exact le_trans (Exponential.monotone_le H Haa' h) ha'⟩ lemma le_iff_lt_length_of_exp {x y a : V} (H : Exponential x y) : y ≤ a ↔ x < ‖a‖ := by - rcases zero_le a with (rfl | pos) + rcases Arithmetic.zero_le a with (rfl | pos) · simpa using pos_iff_ne_zero.mp H.range_pos simp [le_iff_le_log_of_exp H pos, length_of_pos pos, ←le_iff_lt_succ] @@ -242,7 +242,7 @@ lemma Exponential.le_log {x y : V} (H : Exponential x y) : x ≤ log y := (le_if lemma Exponential.lt_length {x y : V} (H : Exponential x y) : x < ‖y‖ := (le_iff_lt_length_of_exp H).mp (by rfl) lemma lt_exponential_length {a b : V} (h : Exponential ‖a‖ b) : a < b := by - rcases zero_le a with (rfl | pos) + rcases Arithmetic.zero_le a with (rfl | pos) · simp at h; simp [h] have : Exponential (log a + 1) b := by simpa [length_of_pos pos] using h rcases Exponential.exponential_succ.mp this with ⟨b, rfl, H⟩ @@ -261,7 +261,7 @@ lemma sq_len_le_three_mul (a : V) : ‖a‖ ^ 2 ≤ 3 * a := by _ ≤ 3 * a + 2 * a + a := by simp [←pos_iff_one_le, pos] _ = 3 * (2 * a) := by simp_all only [←two_add_one_eq_three, two_mul, add_mul, add_assoc, one_mul] case odd a IH => - rcases zero_le a with (rfl | pos) + rcases Arithmetic.zero_le a with (rfl | pos) · simp [←two_add_one_eq_three] calc ‖2 * a + 1‖ ^ 2 = (‖a‖ + 1) ^ 2 := by rw [length_two_mul_add_one a] @@ -380,7 +380,7 @@ lemma bexp_two_mul {a a' x : V} (hx : 2 * x < ‖a‖) (hx' : x < ‖a'‖) : bexp_eq_of_exp hx (exp_bexp_of_lt hx').bit_zero lemma bexp_two_mul_succ {a i : V} : bexp (2 * a) (i + 1) = 2 * bexp a i := by - rcases zero_le a with (rfl | pos) + rcases Arithmetic.zero_le a with (rfl | pos) · simp rcases show i ≥ ‖a‖ ∨ i < ‖a‖ from le_or_gt ‖a‖ i with (h | h) · simp [bexp_eq_zero_of_le, h, show ‖2 * a‖ ≤ i + 1 from by simp [length_two_mul_of_pos pos, h]] @@ -421,7 +421,7 @@ instance : Bounded₂ (fbit : V → V → V) := ⟨‘1’, λ _ ↦ by simp⟩ simp [fbit, bexp_two_mul_add_one_succ, Arithmetic.div_mul] @[simp] lemma fbit_two_mul_zero_eq_zero (a : V) : fbit (2 * a) 0 = 0 := by - rcases zero_le a with (rfl | pos) + rcases Arithmetic.zero_le a with (rfl | pos) · simp · have : bexp (2 * a) 0 = 1 := bexp_eq_of_exp (by simp [pos]) (by simp) simp [fbit, this] diff --git a/Foundation/FirstOrder/Arithmetic/Exponential/Pow2.lean b/Foundation/FirstOrder/Arithmetic/Exponential/Pow2.lean index d3f482de1..b5497603a 100644 --- a/Foundation/FirstOrder/Arithmetic/Exponential/Pow2.lean +++ b/Foundation/FirstOrder/Arithmetic/Exponential/Pow2.lean @@ -141,7 +141,7 @@ lemma not_lenbit_iff_rem {i a : V} : ¬LenBit i a ↔ (a / i) % 2 = 0 := by @[simp] lemma LenBit.self {a : V} (pos : 0 < a) : LenBit a a := by simp [LenBit.iff_rem, pos] lemma LenBit.mod {i a k : V} (h : 2 * i ∣ k) : LenBit i (a % k) ↔ LenBit i a := by - have : 0 ≤ i := zero_le i + have : 0 ≤ i := Arithmetic.zero_le i rcases (eq_or_lt_of_le this) with (rfl | pos) · simp rcases h with ⟨k', hk'⟩ @@ -158,7 +158,7 @@ lemma LenBit.mod {i a k : V} (h : 2 * i ∣ k) : LenBit i (a % k) ↔ LenBit i a @[simp] lemma LenBit.mod_two_mul_self {a i : V} : LenBit i (a % (2 * i)) ↔ LenBit i a := LenBit.mod (by simp) lemma LenBit.add {i a b : V} (h : 2 * i ∣ b) : LenBit i (a + b) ↔ LenBit i a := by - have : 0 ≤ i := zero_le i + have : 0 ≤ i := Arithmetic.zero_le i rcases (eq_or_lt_of_le this) with (rfl | pos) · simp rcases h with ⟨b', hb'⟩ @@ -307,7 +307,7 @@ lemma four_le {i : V} (hi : Pow2 i) (lt : 2 < i) : 4 ≤ i := by lemma mul_add_lt_of_mul_lt_of_pos {a b p q : V} (hp : Pow2 p) (hq : Pow2 q) (h : a * p < q) (hb : b < p) (hbq : b < q) : a * p + b < q := by - rcases zero_le a with (rfl | pos) + rcases Arithmetic.zero_le a with (rfl | pos) · simp [hbq] have : p ∣ q := dvd_of_le hp hq (le_of_lt <| lt_of_le_of_lt (le_mul_of_pos_left pos) h) diff --git a/Foundation/FirstOrder/Arithmetic/HFS/Basic.lean b/Foundation/FirstOrder/Arithmetic/HFS/Basic.lean index a3a88aed9..a29ef2fcf 100644 --- a/Foundation/FirstOrder/Arithmetic/HFS/Basic.lean +++ b/Foundation/FirstOrder/Arithmetic/HFS/Basic.lean @@ -64,7 +64,7 @@ lemma sUnion_lt_of_pos {a : V} (ha : 0 < a) : ⋃ʰᶠ a < a := exact lt_of_lt_of_le (lt_of_mem hi) (le_log_of_mem hx) @[simp] lemma sUnion_le (a : V) : ⋃ʰᶠ a ≤ a := by - rcases zero_le a with (rfl | pos) + rcases Arithmetic.zero_le a with (rfl | pos) · simp [←emptyset_def] · exact le_of_lt (sUnion_lt_of_pos pos) diff --git a/Foundation/FirstOrder/Arithmetic/HFS/PRF.lean b/Foundation/FirstOrder/Arithmetic/HFS/PRF.lean index 32048abe5..e2abbe729 100644 --- a/Foundation/FirstOrder/Arithmetic/HFS/PRF.lean +++ b/Foundation/FirstOrder/Arithmetic/HFS/PRF.lean @@ -140,7 +140,7 @@ lemma CSeq.exists (l : V) : ∃ s, c.CSeq v s ∧ l + 1 = lh s := by · apply HierarchySymbol.Definable.exs apply HierarchySymbol.Definable.and · exact ⟨p.cseqDef.rew (Rew.embSubsts <| #0 :> fun i ↦ &(v i)), by - intro w; simpa [Matrix.comp_vecCons''] using c.cseq_defined_iff (w 0 :> v)⟩ + intro w; simpa [Matrix.comp_vecCons''] using! c.cseq_defined_iff (w 0 :> v)⟩ · definability case zero => exact ⟨!⟦c.zero v⟧, CSeq.initial, by simp⟩ diff --git a/Foundation/FirstOrder/Arithmetic/IOpen/Basic.lean b/Foundation/FirstOrder/Arithmetic/IOpen/Basic.lean index fe38dfe74..d2af6d2e9 100644 --- a/Foundation/FirstOrder/Arithmetic/IOpen/Basic.lean +++ b/Foundation/FirstOrder/Arithmetic/IOpen/Basic.lean @@ -124,14 +124,14 @@ lemma div_mul_add (a b : V) {r} (hr : r < b) : (a * b + r) / b = a := lemma div_mul_add' (a b : V) {r} (hr : r < b) : (b * a + r) / b = a := by simpa [mul_comm] using div_mul_add a b hr @[simp] lemma zero_div (a : V) : 0 / a = 0 := by - rcases zero_le a with (rfl | pos) + rcases Arithmetic.zero_le a with (rfl | pos) · simp · exact div_eq_of (by simp) (by simpa) lemma div_mul (a b c : V) : a / (b * c) = a / b / c := by - rcases zero_le b with (rfl | hb) + rcases Arithmetic.zero_le b with (rfl | hb) · simp - rcases zero_le c with (rfl | hc) + rcases Arithmetic.zero_le c with (rfl | hc) · simp exact div_eq_of (by calc @@ -142,14 +142,14 @@ lemma div_mul (a b c : V) : a / (b * c) = a / b / c := by _ ≤ b * c * (a / b / c + 1) := by simpa [mul_assoc] using mul_le_mul_left (lt_iff_succ_le.mp <| lt_mul_div_succ (a / b) hc)) @[simp] lemma mul_div_le (a b : V) : b * (a / b) ≤ a := by - have : 0 ≤ b := by exact zero_le b + have : 0 ≤ b := by exact Arithmetic.zero_le b rcases this with (rfl | pos) · simp · rcases eq_mul_div_add_of_pos a pos with ⟨v, _, e⟩ simpa [← e] using show b * (a / b) ≤ b * (a / b) + v from le_self_add @[simp] lemma div_le (a b : V) : a / b ≤ a := by - have : 0 ≤ b := zero_le b + have : 0 ≤ b := Arithmetic.zero_le b rcases this with (rfl | pos) · simp · have : 1 * (a / b) ≤ b * (a / b) := mul_le_mul_of_nonneg_right (le_iff_lt_succ.mpr (by simp [pos])) (by simp) @@ -192,7 +192,7 @@ lemma div_mul_add_self' (a c : V) {b} (pos : 0 < b) : (b * a + c) / b = a + c / simpa using div_mul_add 0 b h @[simp] lemma div_sq (a : V) : a^2 / a = a := by - rcases zero_le a with (rfl | pos) + rcases Arithmetic.zero_le a with (rfl | pos) · simp · simp [sq, pos] @@ -208,14 +208,14 @@ lemma div_mul_add_self' (a c : V) {b} (pos : 0 < b) : (b * a + c) / b = a + c / simpa using div_add_mul_self a 1 pos lemma mul_div_self_of_dvd {a b : V} : a * (b / a) = b ↔ a ∣ b := by - rcases zero_le a with (rfl | pos) + rcases Arithmetic.zero_le a with (rfl | pos) · simp [eq_comm] · constructor · intro e; rw [←e]; simp · rintro ⟨r, rfl⟩; simp [pos] lemma div_lt_of_pos_of_one_lt {a b : V} (ha : 0 < a) (hb : 1 < b) : a / b < a := by - rcases zero_le (a / b) with (e | lt) + rcases Arithmetic.zero_le (a / b) with (e | lt) · simp [←e, ha] · exact lt_of_lt_of_le (lt_mul_of_one_lt_left lt hb) (mul_div_le a b) @@ -224,7 +224,7 @@ lemma le_two_mul_div_two_add_one (a : V) : a ≤ 2 * (a / 2) + 1 := by exact le_iff_lt_succ.mpr (by simpa [add_assoc, one_add_one_eq_two, mul_add] using this) lemma div_monotone {a b : V} (h : a ≤ b) (c : V) : a / c ≤ b / c := by - rcases zero_le c with (rfl | pos) + rcases Arithmetic.zero_le c with (rfl | pos) · simp by_contra A have : b / c + 1 ≤ a / c := succ_le_iff_lt.mpr (by simpa using A) @@ -280,7 +280,7 @@ lemma div_add_mod (a b : V) : b * (a / b) + (a % b) = a := @[simp] lemma zero_mod (a : V) : 0 % a = 0 := by simp [mod_def] @[simp] lemma mod_self (a : V) : a % a = 0 := by - rcases zero_le a with (rfl | h) + rcases Arithmetic.zero_le a with (rfl | h) · simp · simp [mod_def, h] @@ -300,7 +300,7 @@ lemma mod_mul_add_of_lt (a b : V) {r} (hr : r < b) : (a * b + r) % b = r := by simp [mul_comm b a, pos] @[simp] lemma mod_mul_self_left (a b : V) : (a * b) % b = 0 := by - rcases zero_le b with (rfl | h) + rcases Arithmetic.zero_le b with (rfl | h) · simp · simpa using mod_mul_add_of_lt a b h @@ -349,7 +349,7 @@ lemma mod_mul {a b m : V} (pos : 0 < m) : (a * b) % m = ((a % m) * (b % m)) % m _ = ((a % m) * (b % m)) % m := by simp [add_mul, mul_add, pos, mul_left_comm _ m, add_assoc, mul_assoc] @[simp] lemma mod_div (a b : V) : a % b / b = 0 := by - rcases zero_le b with (rfl | pos) + rcases Arithmetic.zero_le b with (rfl | pos) · simp · exact div_eq_zero_of_lt b (by simp [pos]) @@ -780,7 +780,7 @@ lemma polynomial_induction [V↓[ℒₒᵣ] ⊧* 𝗣𝗔⁻] (Γ m) [V↓[ℒ · exact hP case inst => exact inferInstance case ind x IH => - rcases zero_le x with (rfl | pos) + rcases Arithmetic.zero_le x with (rfl | pos) · exact zero · have : x / 2 < x := div_lt_of_pos_of_one_lt pos one_lt_two rcases even_or_odd' x with (hx | hx) diff --git a/Foundation/FirstOrder/Arithmetic/Induction.lean b/Foundation/FirstOrder/Arithmetic/Induction.lean index 0d32de6fb..2608035c0 100644 --- a/Foundation/FirstOrder/Arithmetic/Induction.lean +++ b/Foundation/FirstOrder/Arithmetic/Induction.lean @@ -39,7 +39,7 @@ theorem bounded_all_sigma1_order_induction {f : V → V → V} (hf : 𝚺₁-Fun rcases sigma₁_replacement₂ hf (under (x + 1)) (under (y + 1)) |>.exists with ⟨m, hm⟩ exact ⟨m, fun x' hx' y' hy' ↦ le_of_lt <| lt_of_mem <| hm (f x' y') |>.mpr - ⟨x', by simpa [lt_succ_iff_le] using hx', y', by simpa [lt_succ_iff_le] using hy', rfl⟩⟩ + ⟨x', by simpa [lt_succ_iff_le] using! hx', y', by simpa [lt_succ_iff_le] using! hy', rfl⟩⟩ intro x y have : ∀ k ≤ x, ∃ W, Seq W ∧ k + 1 = lh W ∧ ⟪0, y⟫ ∈ W ∧ diff --git a/Foundation/FirstOrder/Arithmetic/Omega1/Basic.lean b/Foundation/FirstOrder/Arithmetic/Omega1/Basic.lean index 3ca043870..8be6f77c6 100644 --- a/Foundation/FirstOrder/Arithmetic/Omega1/Basic.lean +++ b/Foundation/FirstOrder/Arithmetic/Omega1/Basic.lean @@ -93,7 +93,7 @@ lemma smash_comm (a b : V) : a ⨳ b = b ⨳ a := (exponential_smash a b).uniq ( exact lt_exponential_length this @[simp] lemma lt_smash_one_righs (a : V) : a ⨳ 1 ≤ 2 * a + 1 := by - rcases zero_le a with (rfl | pos) + rcases Arithmetic.zero_le a with (rfl | pos) · simp · exact (le_iff_lt_length_of_exp (exponential_smash a 1)).mpr (by suffices ‖a‖ < ‖a * 2 + 1‖ by simpa [mul_comm 2 a] @@ -120,7 +120,7 @@ lemma smash_two_mul (a : V) {b} (pos : 0 < b) : a ⨳ (2 * b) = (a ⨳ b) * (a exact h₁.uniq h₂ lemma smash_two_mul_le_sq_smash (a b : V) : a ⨳ (2 * b) ≤ (a ⨳ b) ^ 2 := by - rcases zero_le b with (rfl | pos) + rcases Arithmetic.zero_le b with (rfl | pos) · simp · simpa [smash_two_mul a pos, sq] using smash_monotone (by rfl) (pos_iff_one_le.mp pos) diff --git a/Foundation/FirstOrder/Arithmetic/Omega1/Nuon.lean b/Foundation/FirstOrder/Arithmetic/Omega1/Nuon.lean index 6dc920798..4564bc0e5 100644 --- a/Foundation/FirstOrder/Arithmetic/Omega1/Nuon.lean +++ b/Foundation/FirstOrder/Arithmetic/Omega1/Nuon.lean @@ -11,7 +11,7 @@ namespace Nuon @[simp] lemma llen_lt_len_smash_len (K : V) : ‖‖K‖‖ < ‖K ⨳ ‖K‖‖ := by suffices ‖‖K‖‖ ≤ ‖K‖ * ‖‖K‖‖ by simpa [length_smash, lt_succ_iff_le] - rcases zero_le ‖K‖ with (hK | pos) + rcases Arithmetic.zero_le ‖K‖ with (hK | pos) · simp [←hK] · exact le_mul_of_pos_left pos @@ -82,7 +82,7 @@ instance : Bounded₃ (ext : V → V → V → V) := ⟨#1, λ _ ↦ by simp⟩ @[simp] lemma ext_zero (L i : V) : 0{L}[i] = 0 := by simp [ext] lemma ext_zero_eq_self_of_le {L S : V} (h : ‖S‖ ≤ ‖L‖) : S{L}[0] = S := by - rcases zero_le S with (rfl | pos) + rcases Arithmetic.zero_le S with (rfl | pos) · simp [ext] · simp [ext] have : bexp S 0 = 1 := (exp_bexp_of_lt (show 0 < ‖S‖ from by simp [pos])).zero_uniq @@ -109,7 +109,7 @@ lemma ext_eq_smash_of_le {L S i : V} (h : i ≤ ‖I‖) : S / bexp (I ⨳ L) (i lemma ext_add₁_pow2 {L i S₁ S₂ p : V} (pp : Pow2 p) (h : (i + 1) * ‖L‖ < ‖p‖) : (S₁ + S₂ * p){L}[i] = S₁{L}[i] := by - rcases zero_le S₂ with (rfl | pos₂) + rcases Arithmetic.zero_le S₂ with (rfl | pos₂) · simp have lt_len : i * ‖L‖ < ‖S₁ + S₂ * p‖ := calc i * ‖L‖ ≤ (i + 1) * ‖L‖ := mul_le_mul_right (by simp) @@ -156,7 +156,7 @@ lemma len_append (I L S : V) {i X} (hi : i ≤ ‖I‖) (hX : 0 < X) : ‖append _ = ‖X‖ + i * ‖L‖ := by simp [log_bexp (mul_len_lt_len_smash hi)] lemma append_lt_smash (I L S : V) {i X} (hi : i < ‖I‖) (hX : ‖X‖ ≤ ‖L‖) : append I L S i X < I ⨳ L := by - rcases zero_le X with (rfl | pos) + rcases Arithmetic.zero_le X with (rfl | pos) · simpa [append_nil] using lt_of_lt_of_le (mod_lt _ (bexp_pos $ mul_len_lt_len_smash $ le_of_lt hi)) (by simp) · suffices ‖X‖ + i * ‖L‖ ≤ ‖I‖ * ‖L‖ by simpa [lt_smash_iff, len_append I L S (le_of_lt hi) pos] @@ -348,7 +348,7 @@ lemma Series.succ (hU : (I ⨳ L)^2 ≤ U) (hIL : ‖‖I‖^2‖ ≤ ‖L‖) hTlast ⟩ lemma div_mod_succ (a b : V) : ((a + 1) / b = a / b + 1 ∧ (a + 1) % b = 0 ∧ a % b + 1 = b) ∨ ((a + 1) / b = a / b ∧ (a + 1) % b = a % b + 1) := by - rcases zero_le b with (rfl | pos) + rcases Arithmetic.zero_le b with (rfl | pos) · simp have : a % b + 1 ≤ b := lt_iff_succ_le.mp <| mod_lt a (by simp [pos]) rcases this with (hb | ltb) @@ -573,7 +573,7 @@ lemma NuonAux.le {A k n : V} (H : NuonAux A k n) : n ≤ k := SeriesSegment.le H lemma NuonAux.uniq {A k n₁ n₂ : V} (H₁ : NuonAux A k n₁) (H₂ : NuonAux A k n₂) : n₁ = n₂ := SeriesSegment.uniq H₁ H₂ lemma NuonAux.succ {A k : V} (H : NuonAux A k n) (hk : k ≤ ‖A‖) : NuonAux A (k + 1) (n + fbit A k) := by - rcases zero_le A with (rfl | pos) + rcases Arithmetic.zero_le A with (rfl | pos) · rcases show n = 0 from H.uniq (NuonAux.zero k); simp exact SeriesSegment.succ (sq_polyI_smash_polyL_polybounded pos) (by simp [polyL]) (lt_of_le_of_lt hk $ polyI_le pos) H @@ -652,7 +652,7 @@ lemma Nuon.nuon_eq {a b : V} (h : Nuon a b) : nuon a = b := (nuon_nuon a).uniq h lemma Nuon.nuon_eq_iff {a b : V} : b = nuon a ↔ Nuon a b := Classical.choose!_eq_iff_right (Nuon.exists_unique a) lemma nuon_bit0 (a : V) : nuon (2 * a) = nuon a := by - rcases zero_le a with (rfl | pos) + rcases Arithmetic.zero_le a with (rfl | pos) · simp · have : Nuon (2 * a) (nuon a) := by simpa [Nuon, length_two_mul_of_pos pos] using (nuon_nuon a).two_mul (by simp) exact this.nuon_eq diff --git a/Foundation/FirstOrder/Arithmetic/PeanoMinus/Basic.lean b/Foundation/FirstOrder/Arithmetic/PeanoMinus/Basic.lean index ad37f8183..16fed26db 100644 --- a/Foundation/FirstOrder/Arithmetic/PeanoMinus/Basic.lean +++ b/Foundation/FirstOrder/Arithmetic/PeanoMinus/Basic.lean @@ -179,13 +179,17 @@ lemma add_eq_of_lt : ∀ x y : M, x < y → ∃ z, x + z = y := by simpa [models_iff] using Theory.models M _ PeanoMinus.addEqOfLt @[simp] protected lemma zero_le : ∀ x : M, 0 ≤ x := by - simpa [models_iff, Structure.le_iff_of_eq_of_lt] using Theory.models M _ PeanoMinus.zeroLe + have h := Theory.models M _ PeanoMinus.zeroLe + simp only [models_iff] at h + exact h lemma zero_lt_one : (0 : M) < 1 := by simpa [models_iff] using Theory.models M _ PeanoMinus.zeroLtOne lemma one_le_of_zero_lt : ∀ x : M, 0 < x → 1 ≤ x := by - simpa [models_iff, Structure.le_iff_of_eq_of_lt] using Theory.models M _ PeanoMinus.oneLeOfZeroLt + have h := Theory.models M _ PeanoMinus.oneLeOfZeroLt + simp [models_iff] at h + exact h lemma add_lt_add : ∀ x y z : M, x < y → x + z < y + z := by simpa [models_iff] using Theory.models M _ PeanoMinus.addLtAdd @@ -452,7 +456,7 @@ lemma two_pow_two_eq_four : 2 ^ 2 = (4 : M) := by lemma two_pos : (0 : M) < 2 := by exact _root_.two_pos @[simp] lemma le_mul_self (a : M) : a ≤ a * a := by - have : 0 ≤ a := by exact zero_le a + have : 0 ≤ a := Arithmetic.zero_le a rcases this with (rfl | pos) <;> simp [*, ←pos_iff_one_le] @[simp] lemma le_sq (a : M) : a ≤ a ^ 2 := by simp [sq] @@ -509,7 +513,7 @@ lemma lt_square_of_lt {a : M} (pos : 1 < a) : a < a^2 := by lemma two_mul_le_sq {i : M} (h : 2 ≤ i) : 2 * i ≤ i ^ 2 := by simpa [sq] using mul_le_mul_right h lemma two_mul_le_sq_add_one (i : M) : 2 * i ≤ i ^ 2 + 1 := by - rcases zero_le i with (rfl | pos) + rcases Arithmetic.zero_le i with (rfl | pos) · simp · rcases pos_iff_one_le.mp pos with (rfl | lt) · simp [one_add_one_eq_two] diff --git a/Foundation/FirstOrder/Arithmetic/PeanoMinus/Functions.lean b/Foundation/FirstOrder/Arithmetic/PeanoMinus/Functions.lean index d475724b9..bb6ac9e18 100644 --- a/Foundation/FirstOrder/Arithmetic/PeanoMinus/Functions.lean +++ b/Foundation/FirstOrder/Arithmetic/PeanoMinus/Functions.lean @@ -75,7 +75,7 @@ lemma add_tsub_self_of_le (h : b ≤ a) : b + (a - b) = a := by symm; exact sub_ @[simp] lemma zero_sub (a : V) : 0 - a = 0 := sub_spec_of_le (by simp) @[simp] lemma sub_zero (a : V) : a - 0 = a := by - simpa using sub_add_self_of_le (show 0 ≤ a from zero_le a) + simpa using sub_add_self_of_le (show 0 ≤ a from Arithmetic.zero_le a) lemma sub_remove_left (e : a = b + c) : a - c = b := by simp [e] diff --git a/Foundation/FirstOrder/Arithmetic/Q/Basic.lean b/Foundation/FirstOrder/Arithmetic/Q/Basic.lean index 1af2c1fd7..a86a38fbf 100644 --- a/Foundation/FirstOrder/Arithmetic/Q/Basic.lean +++ b/Foundation/FirstOrder/Arithmetic/Q/Basic.lean @@ -288,7 +288,8 @@ lemma iff_lt_numeral_exists_numeral {n : ℕ} {x : M} : x < numeral n ↔ ∃ m constructor; . omega; . apply succ_inj; - simpa using ha; + have ha' : (x : M) + 1 = numeral (n + 2) := by simpa using ha + rw [ha', numeral_add_one]; . obtain ⟨m, hm, rfl⟩ := iff_lt_numeral_exists_numeral (x := x) (n := n + 1) |>.mp $ by have ha : x + a = numeral (n + 1) := succ_inj $ by rwa [Arithmetic.add_succ] at ha; rw [←ha]; diff --git a/Foundation/FirstOrder/Arithmetic/TA/Nonstandard.lean b/Foundation/FirstOrder/Arithmetic/TA/Nonstandard.lean index 20561145d..43d23b769 100644 --- a/Foundation/FirstOrder/Arithmetic/TA/Nonstandard.lean +++ b/Foundation/FirstOrder/Arithmetic/TA/Nonstandard.lean @@ -89,7 +89,7 @@ lemma star_unbounded (n : ℕ) : n < ⋆ := by <| Set.mem_iUnion_of_mem (n + 1) <| Set.mem_union_right _ <| Set.mem_range_self (Fin.last n) - simpa [models_iff, numeral_eq_natCast] using this + simpa [models_iff, numeral_eq_natCast] using! this end Nonstandard diff --git a/Foundation/FirstOrder/Basic/Calculus.lean b/Foundation/FirstOrder/Basic/Calculus.lean index de15f1eee..143105fa2 100644 --- a/Foundation/FirstOrder/Basic/Calculus.lean +++ b/Foundation/FirstOrder/Basic/Calculus.lean @@ -25,7 +25,7 @@ open Semiformula def newVar (Γ : Sequent L) : ℕ := (Γ.map Semiformula.fvSup).foldr max 0 lemma not_fvar?_newVar {φ : Proposition L} {Γ : Sequent L} (h : φ ∈ Γ) : ¬FVar? φ Γ.newVar := - not_fvar?_of_lt_fvSup φ (by simpa [newVar] using List.le_max_of_le (List.mem_map_of_mem h) (by simp)) + not_fvar?_of_lt_fvSup φ (by simp only [newVar]; exact List.le_max_of_le (List.mem_map_of_mem h) (by simp)) @[simp] lemma lcHom_comm {Γ : List (Formula L ξ)} (f : Formula L ξ →ˡᶜ Proposition L) : (∼Γ).map f = ∼Γ.map f := by simp [List.tilde_def] @@ -334,11 +334,11 @@ instance (T U : Theory L) : U ⪯ T ∪ U := weakerThan_of_le (by simp) lemma provable_iff : T ⊢ φ ↔ ∃ Γ : List (Sentence L), (∀ ψ ∈ Γ, ψ ∈ T) ∧ Nonempty (⊢ᴸᴷ¹ φ :: ∼Sequent.embed Γ) := by - simpa using OneSidedLK.ContextualEntailment.provable_iff (𝓢 := T) (φ := φ) + simpa using! OneSidedLK.ContextualEntailment.provable_iff (𝓢 := T) (φ := φ) lemma inconsistent_iff : Entailment.Inconsistent T ↔ ∃ Γ : List (Sentence L), (∀ ψ ∈ Γ, ψ ∈ T) ∧ Nonempty (⊢ᴸᴷ¹ ∼Sequent.embed Γ) := by - simpa using OneSidedLK.ContextualEntailment.inconsistent_iff (𝓢 := T) + simpa using! OneSidedLK.ContextualEntailment.inconsistent_iff (𝓢 := T) open Entailment Derivation diff --git a/Foundation/FirstOrder/Basic/Eq.lean b/Foundation/FirstOrder/Basic/Eq.lean index cfcd6c90d..ae736456a 100644 --- a/Foundation/FirstOrder/Basic/Eq.lean +++ b/Foundation/FirstOrder/Basic/Eq.lean @@ -118,17 +118,17 @@ open Semiterm Theory Semiformula lemma eqv_refl (a : M) : eqv L a a := by have : M↓[L] ⊧ “∀ x, x = x” := H.models _ (Theory.eqAxiom.refl (L := L)) have : ∀ x : M, op(=)[L].val ![x, x] := by simpa [models_iff] using this - simpa using this a + exact this a lemma eqv_symm {a b : M} : eqv L a b → eqv L b a := by have : M↓[L] ⊧ “∀ x y, x = y → y = x” := H.models _ (Theory.eqAxiom.symm (L := L)) have : ∀ x y : M, op(=)[L].val ![x, y] → op(=)[L].val ![y, x] := by simpa [models_iff] using this - simpa using this a b + exact this a b lemma eqv_trans {a b c : M} : eqv L a b → eqv L b c → eqv L a c := by have : M↓[L] ⊧ “∀ x y z, x = y → y = z → x = z” := H.models _ (Theory.eqAxiom.trans (L := L)) have : ∀ x y z : M, op(=)[L].val ![x, y] → op(=)[L].val ![y, z] → op(=)[L].val ![x, z] := by simpa [models_iff] using this - simpa using this a b c + exact this a b c lemma eqv_funcExt {k} (f : L.Func k) {v w : Fin k → M} (h : ∀ i, eqv L (v i) (w i)) : eqv L (func f v) (func f w) := by @@ -137,9 +137,9 @@ lemma eqv_funcExt {k} (f : L.Func k) {v w : Fin k → M} (h : ∀ i, eqv L (v i) ∀ m : Fin (k + k) → M, (∀ (i : Fin k), op(=)[L].val ![m (Fin.addCast k i), m (i.addNat k)]) → op(=)[L].val ![func f fun i ↦ m (Fin.addCast k i), func f fun i ↦ m (i.addNat k)] := by - simpa [models_iff, Semiterm.val_func] using this - have := this (Matrix.vecAppend rfl v w) (fun i ↦ by simpa [Matrix.vecAppend_eq_ite] using h i) - simpa [Semiterm.val_func, Matrix.vecAppend_eq_ite] using this + simpa [models_iff, Semiterm.val_func] using! this + have := this (Matrix.vecAppend rfl v w) (fun i ↦ by simpa [Matrix.vecAppend_eq_ite, eqv] using h i) + simpa [Semiterm.val_func, Matrix.vecAppend_eq_ite, eqv] using this lemma eqv_relExt_aux {k} (r : L.Rel k) {v w : Fin k → M} (h : ∀ i, eqv L (v i) (w i)) : rel r v → rel r w := by @@ -148,9 +148,9 @@ lemma eqv_relExt_aux {k} (r : L.Rel k) {v w : Fin k → M} (h : ∀ i, eqv L (v ∀ m : Fin (k + k) → M, (∀ (i : Fin k), op(=)[L].val ![m (Fin.addCast k i), m (i.addNat k)]) → (rel r fun i ↦ m (Fin.addCast k i)) → rel r fun i ↦ m (i.addNat k) := by - simpa [models_iff, Semiterm.val_func] using this - have := this (Matrix.vecAppend rfl v w) (fun i ↦ by simpa [Matrix.vecAppend_eq_ite] using h i) - simpa [Semiterm.val_func, Matrix.vecAppend_eq_ite] using this + simpa [models_iff, Semiterm.val_func, eval_rel] using! this + have := this (Matrix.vecAppend rfl v w) (fun i ↦ by simpa [Matrix.vecAppend_eq_ite, eqv] using h i) + simpa [Semiterm.val_func, Matrix.vecAppend_eq_ite, eqv] using this lemma eqv_relExt {k} (r : L.Rel k) {v w : Fin k → M} (h : ∀ i, eqv L (v i) (w i)) : rel r v ↔ rel r w := by @@ -202,16 +202,17 @@ lemma eval_mk {bv fv} {φ : Semiformula L ξ n} : induction φ using Semiformula.rec' case hall n φ ih => constructor - · intro h a; exact (ih (bv := a :> bv)).mp (by simpa [Matrix.comp_vecCons] using h ⟦a⟧) + · intro h a; exact (ih (bv := a :> bv)).mp (by simp only [Matrix.comp_vecCons]; exact h ⟦a⟧) · intro h a; induction' a using Quotient.ind with a - simpa [Matrix.comp_vecCons] using ih.mpr (h a) + have h2 := ih.mpr (h a); simp only [Matrix.comp_vecCons] at h2; exact h2 case hexs n φ ih => constructor · intro ⟨a, h⟩ induction' a using Quotient.ind with a - exact ⟨a, (ih (bv := a :> bv)).mp (by simpa [Matrix.comp_vecCons] using h)⟩ - · intro ⟨a, h⟩; exact ⟨⟦a⟧, by simpa [Matrix.comp_vecCons] using ih.mpr h⟩ + exact ⟨a, (ih (bv := a :> bv)).mp (by simp only [Matrix.comp_vecCons]; exact h)⟩ + · intro ⟨a, h⟩; refine ⟨⟦a⟧, ?_⟩ + have h2 := ih.mpr h; simp only [Matrix.comp_vecCons] at h2; exact h2 case _ => simp [*] case _ => simp [*] case _ => simp [*, val_mk, rel_mk, Function.comp_def] @@ -221,11 +222,12 @@ lemma eval_mk {bv fv} {φ : Semiformula L ξ n} : lemma evalf_mk {fv} {φ : Formula L ξ} : φ.Evalf (M := QuotEq L M) (⟦fv ·⟧) ↔ φ.Evalf fv := by - simpa [Matrix.empty_eq] using eval_mk (bv := ![]) (fv := fv) (φ := φ) + have h := eval_mk (bv := ![]) (fv := fv) (φ := φ) + simp only [Matrix.empty_eq] at h; exact h lemma models_iff {σ : Sentence L} : (QuotEq L M)↓[L] ⊧ σ ↔ M↓[L] ⊧ σ := by - simpa [Empty.eq_elim, Matrix.empty_eq] using - eval_mk (M := M) (ξ := Empty) (φ := σ) (bv := ![]) (fv := Empty.elim) + have h := eval_mk (M := M) (ξ := Empty) (φ := σ) (bv := ![]) (fv := Empty.elim) + simp only [Empty.eq_elim, Matrix.empty_eq] at h; exact h variable (L M) diff --git a/Foundation/FirstOrder/Basic/Operator.lean b/Foundation/FirstOrder/Basic/Operator.lean index 0052b06a0..1932ad5f2 100644 --- a/Foundation/FirstOrder/Basic/Operator.lean +++ b/Foundation/FirstOrder/Basic/Operator.lean @@ -615,15 +615,21 @@ variable {L M} @[simp] lemma add_eq_of_lang [L.Add] [Add M] [Structure.Add L M] {v : Fin 2 → M} : Structure.func (L := L) Language.Add.add v = v 0 + v 1 := by - simpa [←Matrix.fun_eq_vec_two] using Structure.Add.add (L := L) (v 0) (v 1) + have h := Structure.Add.add (L := L) (v 0) (v 1) + simp [←Matrix.fun_eq_vec_two] at h + exact h @[simp] lemma mul_eq_of_lang [L.Mul] [Mul M] [Structure.Mul L M] {v : Fin 2 → M} : Structure.func (L := L) Language.Mul.mul v = v 0 * v 1 := by - simpa [←Matrix.fun_eq_vec_two] using Structure.Mul.mul (L := L) (v 0) (v 1) + have h := Structure.Mul.mul (L := L) (v 0) (v 1) + simp [←Matrix.fun_eq_vec_two] at h + exact h @[simp] lemma exp_eq_of_lang [L.Exp] [Exp M] [Structure.Exp L M] {v : Fin 1 → M} : Structure.func (L := L) Language.Exp.exp v = LO.Exp.exp (v 0) := by - simpa [←Matrix.fun_eq_vec_one] using Structure.Exp.exp (L := L) (v 0) + have h := Structure.Exp.exp (L := L) (v 0) + simp [←Matrix.fun_eq_vec_one] at h + exact h @[simp] lemma eq_iff_eq [Operator.Eq L] [Structure.Eq L M] {v : Fin 2 →M} : (@Operator.Eq.eq L _).val v ↔ v 0 = v 1 := by @@ -642,13 +648,13 @@ lemma le_iff_of_eq_of_lt [Operator.Eq L] [Operator.LT L] [LT M] [Structure.Eq L simp [Operator.LE.def_of_Eq_of_LT] @[simp] lemma eq_lang [L.Eq] [Structure.Eq L M] {v : Fin 2 → M} : - Structure.rel (L := L) Language.Eq.eq v ↔ v 0 = v 1 := by simpa [-eq_iff_eq] using eq_iff_eq (L := L) (v := v) + Structure.rel (L := L) Language.Eq.eq v ↔ v 0 = v 1 := by simpa [-eq_iff_eq] using! eq_iff_eq (L := L) (v := v) @[simp] lemma lt_lang [L.LT] [LT M] [Structure.LT L M] {v : Fin 2 → M} : - Structure.rel (L := L) Language.LT.lt v ↔ v 0 < v 1 := by simpa [-lt_iff_lt] using lt_iff_lt (L := L) (v := v) + Structure.rel (L := L) Language.LT.lt v ↔ v 0 < v 1 := by simpa [-lt_iff_lt] using! lt_iff_lt (L := L) (v := v) @[simp] lemma mem_lang [L.Mem] [Membership M M] [Structure.Mem L M] {v : Fin 2 → M} : - Structure.rel (L := L) Language.Mem.mem v ↔ v 0 ∈ v 1 := by simpa [-mem_iff_mem] using mem_iff_mem (L := L) (v := v) + Structure.rel (L := L) Language.Mem.mem v ↔ v 0 ∈ v 1 := by simpa [-mem_iff_mem] using! mem_iff_mem (L := L) (v := v) lemma operator_val_ofEquiv_iff (φ : M ≃ N) {k : ℕ} {o : Semiformula.Operator L k} {v : Fin k → N} : letI : Structure L N := ofEquiv φ diff --git a/Foundation/FirstOrder/Basic/Semantics/Elementary.lean b/Foundation/FirstOrder/Basic/Semantics/Elementary.lean index 17833aca9..316aba5cf 100644 --- a/Foundation/FirstOrder/Basic/Semantics/Elementary.lean +++ b/Foundation/FirstOrder/Basic/Semantics/Elementary.lean @@ -59,7 +59,7 @@ variable {L M M₁ M₂ M₃} instance : FunLike (M₁ →ₛ[L] M₂) M₁ M₂ where coe := fun φ => φ.toFun - coe_injective' := fun φ ψ h => by + coe_injective := fun φ ψ h => by rcases φ; rcases ψ simp only [Hom.mk.injEq] at h ⊢ ext; exact congr_fun h _ @@ -91,7 +91,7 @@ end HomClass instance : FunLike (M₁ ↪ₛ[L] M₂) M₁ M₂ where coe := fun φ => φ.toFun - coe_injective' := fun φ ψ h => by + coe_injective := fun φ ψ h => by rcases φ; rcases ψ; simp only [Embedding.mk.injEq] at h ⊢; ext; exact congr_fun h _ instance : EmbeddingClass (M₁ ↪ₛ[L] M₂) L M₁ M₂ where @@ -120,7 +120,7 @@ end EmbeddingClass instance : FunLike (M₁ ≃ₛ[L] M₂) M₁ M₂ where coe := fun φ => φ.toFun - coe_injective' := fun φ ψ h => by + coe_injective := fun φ ψ h => by rcases φ; rcases ψ; simp only [Iso.mk.injEq] at h ⊢; ext; exact congr_fun h _ instance : IsoClass (M₁ ≃ₛ[L] M₂) L M₁ M₂ where @@ -255,9 +255,9 @@ lemma eval_iff_of_equiv {f₁ f₂ b₁ b₂} φ.Eval b₁ f₁ ↔ φ.Eval b₂ f₂ := match φ with | .rel R v => by - simpa using hrel R fun i ↦ val_eq_of_equiv I hf hb hfunc (v i) + simpa [Function.comp_def] using hrel R fun i ↦ val_eq_of_equiv I hf hb hfunc (v i) | .nrel R v => by - simpa using not_congr <| hrel R fun i ↦ val_eq_of_equiv I hf hb hfunc (v i) + simpa [Function.comp_def] using not_congr <| hrel R fun i ↦ val_eq_of_equiv I hf hb hfunc (v i) | ⊤ => by simp | ⊥ => by simp | φ ⋏ ψ => by diff --git a/Foundation/FirstOrder/Basic/Semantics/Semantics.lean b/Foundation/FirstOrder/Basic/Semantics/Semantics.lean index cc67ba187..40753cb79 100644 --- a/Foundation/FirstOrder/Basic/Semantics/Semantics.lean +++ b/Foundation/FirstOrder/Basic/Semantics/Semantics.lean @@ -479,11 +479,11 @@ lemma eval_ofEquiv_iff {b : Fin n → N} {f : ξ → N} {φ : Semiformula L ξ n | ⊤ | ⊥ => by simp | φ ⋏ ψ | φ ⋎ ψ => by simp [eval_ofEquiv_iff (φ := φ), eval_ofEquiv_iff (φ := ψ)] | ∀⁰ φ => - ⟨fun h x ↦ by simpa [Matrix.comp_vecCons''] using eval_ofEquiv_iff.mp (h (Θ x)), - fun h x ↦ eval_ofEquiv_iff.mpr (by simpa [Matrix.comp_vecCons''] using h (Θ.symm x))⟩ + ⟨fun h x ↦ by have h' := eval_ofEquiv_iff.mp (h (Θ x)); simp [Matrix.comp_vecCons''] at h'; exact h', + fun h x ↦ eval_ofEquiv_iff.mpr (by simp only [Matrix.comp_vecCons'']; exact h (Θ.symm x))⟩ | ∃⁰ φ => - ⟨by rintro ⟨x, h⟩; exists Θ.symm x; simpa [Matrix.comp_vecCons''] using eval_ofEquiv_iff.mp h, - by rintro ⟨x, h⟩; exists Θ x; apply eval_ofEquiv_iff.mpr; simpa [Matrix.comp_vecCons''] using h⟩ + ⟨by rintro ⟨x, h⟩; exists Θ.symm x; have h' := eval_ofEquiv_iff.mp h; simp [Matrix.comp_vecCons''] at h'; exact h', + by rintro ⟨x, h⟩; exists Θ x; apply eval_ofEquiv_iff.mpr; simp only [Matrix.comp_vecCons'', Equiv.symm_apply_apply]; exact h⟩ lemma evalf_ofEquiv_iff {f : ξ → N} {φ : Formula L ξ} : Evalf (s := ofEquiv Θ) f φ ↔ Evalf (s := s) (Θ.symm ∘ f) φ := by simpa using eval_ofEquiv_iff (Θ := Θ) (f := f) (φ := φ) (b := ![]) diff --git a/Foundation/FirstOrder/Basic/Syntax/Rew.lean b/Foundation/FirstOrder/Basic/Syntax/Rew.lean index 62057f999..fc9ecb12b 100644 --- a/Foundation/FirstOrder/Basic/Syntax/Rew.lean +++ b/Foundation/FirstOrder/Basic/Syntax/Rew.lean @@ -300,7 +300,7 @@ lemma fvar?_rew [DecidableEq ξ₁] [DecidableEq ξ₂] · exact .inl h · exact .inr ⟨z, by simp [hi], hz⟩ case hall n φ ihp => - have : (Rew.bind (#0 :> fun i ↦ Rew.bShift (ω #i)) (fun z ↦ Rew.bShift (ω &z)) ▹ φ).FVar? x := by simpa [Rew.q_bind] using h + have : (Rew.bind (#0 :> fun i ↦ Rew.bShift (ω #i)) (fun z ↦ Rew.bShift (ω &z)) ▹ φ).FVar? x := h rcases ihp this with (⟨z, hz⟩ | ⟨z, hz⟩) · cases z using Fin.cases case zero => simp at hz @@ -310,7 +310,7 @@ lemma fvar?_rew [DecidableEq ξ₁] [DecidableEq ξ₂] · have : φ.FVar? z ∧ (ω &z).FVar? x := by simpa using hz exact .inr ⟨z, this⟩ case hexs n φ ihp => - have : (Rew.bind (#0 :> fun i ↦ Rew.bShift (ω #i)) (fun z ↦ Rew.bShift (ω &z)) ▹ φ).FVar? x := by simpa [Rew.q_bind] using h + have : (Rew.bind (#0 :> fun i ↦ Rew.bShift (ω #i)) (fun z ↦ Rew.bShift (ω &z)) ▹ φ).FVar? x := h rcases ihp this with (⟨z, hz⟩ | ⟨z, hz⟩) · cases z using Fin.cases case zero => simp at hz diff --git a/Foundation/FirstOrder/Bootstrapping/DerivabilityCondition/D1.lean b/Foundation/FirstOrder/Bootstrapping/DerivabilityCondition/D1.lean index 7dffa59ae..32c52217d 100644 --- a/Foundation/FirstOrder/Bootstrapping/DerivabilityCondition/D1.lean +++ b/Foundation/FirstOrder/Bootstrapping/DerivabilityCondition/D1.lean @@ -18,20 +18,20 @@ variable {L : Language} [L.Encodable] [L.LORDefinable] variable {T : Theory L} [T.Δ₁] lemma derivable_quote {Γ : Finset (Proposition L)} (d : T ⟹₂ Γ) : Derivable T (⌜Γ⌝ : V) := - ⟨⌜d⌝, by simpa [Semiformula.quote_def] using (⌜d⌝ : Theory.internalize V T ⊢!ᵈᵉʳ ⌜Γ⌝).derivationOf⟩ + ⟨⌜d⌝, by simpa [Semiformula.quote_def] using! (⌜d⌝ : Theory.internalize V T ⊢!ᵈᵉʳ ⌜Γ⌝).derivationOf⟩ /-- Hilbert–Bernays provability condition D1 -/ theorem internalize_provability {φ} : T ⊢ φ → Provable T (⌜φ⌝ : V) := fun h ↦ by - simpa using derivable_quote (V := V) (provable_iff_derivable2.mp h).some + simpa using! derivable_quote (V := V) (provable_iff_derivable2.mp h).some theorem internal_provable_of_outer_provable {φ} : T ⊢ φ → T.internalize V ⊢ ⌜φ⌝ := fun h ↦ by - simpa [TProvable.iff_provable] using internalize_provability (V := V) h + simpa [TProvable.iff_provable] using! internalize_provability (V := V) h @[simp] lemma Provable.complete {φ : Sentence L} : T.internalize ℕ ⊢ ⌜φ⌝ ↔ T ⊢ φ := - ⟨by simpa [TProvable.iff_provable] using Provable.sound, internal_provable_of_outer_provable⟩ + ⟨by simpa [TProvable.iff_provable] using! Provable.sound, internal_provable_of_outer_provable⟩ @[simp] lemma provable_iff_provable {T : Theory L} [T.Δ₁] {φ : Sentence L} : - Provable T (⌜φ⌝ : ℕ) ↔ T ⊢ φ := by simpa [TProvable.iff_provable] using Provable.complete + Provable T (⌜φ⌝ : ℕ) ↔ T ⊢ φ := by simpa [TProvable.iff_provable] using! Provable.complete end LO.FirstOrder.Arithmetic.Bootstrapping diff --git a/Foundation/FirstOrder/Bootstrapping/DerivabilityCondition/D2.lean b/Foundation/FirstOrder/Bootstrapping/DerivabilityCondition/D2.lean index 65ade2ae9..e817e9692 100644 --- a/Foundation/FirstOrder/Bootstrapping/DerivabilityCondition/D2.lean +++ b/Foundation/FirstOrder/Bootstrapping/DerivabilityCondition/D2.lean @@ -28,7 +28,7 @@ theorem modus_ponens {φ ψ : Proposition L} (hφψ : Provable T (⌜φ 🡒 ψ theorem modus_ponens_sentence {σ τ : Sentence L} (hστ : Provable T (⌜σ 🡒 τ⌝ : V)) (hσ : Provable T (⌜σ⌝ : V)) : Provable T (⌜τ⌝ : V) := by apply (tprovable_tquote_iff_provable_quote (L := L)).mp - have hστ : Theory.internalize V T ⊢ ⌜σ⌝ 🡒 ⌜τ⌝ := by simpa using (tprovable_tquote_iff_provable_quote (L := L)).mpr hστ + have hστ : Theory.internalize V T ⊢ ⌜σ⌝ 🡒 ⌜τ⌝ := by simpa using! (tprovable_tquote_iff_provable_quote (L := L)).mpr hστ have hσ : Theory.internalize V T ⊢ ⌜σ⌝ := (tprovable_tquote_iff_provable_quote (L := L)).mpr hσ exact hστ ⨀ hσ diff --git a/Foundation/FirstOrder/Bootstrapping/DerivabilityCondition/D3.lean b/Foundation/FirstOrder/Bootstrapping/DerivabilityCondition/D3.lean index 32b915c37..18619ed39 100644 --- a/Foundation/FirstOrder/Bootstrapping/DerivabilityCondition/D3.lean +++ b/Foundation/FirstOrder/Bootstrapping/DerivabilityCondition/D3.lean @@ -153,7 +153,7 @@ theorem sigma_one_provable_of_models {σ : Sentence ℒₒᵣ} (hσ : Hierarchy theorem sigma_one_complete {σ : Sentence ℒₒᵣ} (hσ : Hierarchy 𝚺 1 σ) : V↓[ℒₒᵣ] ⊧ σ → Provable T (⌜σ⌝ : V) := fun h ↦ by simpa [tprovable_iff_provable] - using Bootstrapping.Arithmetic.sigma_one_provable_of_models T hσ h + using! Bootstrapping.Arithmetic.sigma_one_provable_of_models T hσ h theorem provable_internalize {σ : Sentence ℒₒᵣ} : Provable T (⌜σ⌝ : V) → Provable T (⌜provabilityPred T σ⌝ : V) := by diff --git a/Foundation/FirstOrder/Bootstrapping/DerivabilityCondition/EquationalTheory.lean b/Foundation/FirstOrder/Bootstrapping/DerivabilityCondition/EquationalTheory.lean index 07f5d0b1a..f7392e6a0 100644 --- a/Foundation/FirstOrder/Bootstrapping/DerivabilityCondition/EquationalTheory.lean +++ b/Foundation/FirstOrder/Bootstrapping/DerivabilityCondition/EquationalTheory.lean @@ -32,13 +32,13 @@ open Entailment Entailment.FiniteContext Semiformula @[simp] lemma eq_refl (t : Term V ℒₒᵣ) : T.internalize V ⊢ t ≐ t := by have : T ⊢ “∀ x, x = x” := complete.{0} T _ fun (M : Type) _ _ ↦ by simp [models_iff] have : T.internalize V ⊢ ∀⁰ (#'0 ≐ #'0) := by - simpa using internal_provable_of_outer_provable this + simpa using! internal_provable_of_outer_provable this simpa using TProof.specialize! this t @[simp] lemma eq_symm (t u : Term V ℒₒᵣ) : T.internalize V ⊢ (t ≐ u) 🡒 (u ≐ t) := by have : T ⊢ “∀ x y, x = y → y = x” := complete.{0} T _ fun (M : Type) _ _ ↦ by simp [models_iff] have : T.internalize V ⊢ ∀⁰ ∀⁰ ((#'1 ≐ #'0) 🡒 (#'0 ≐ #'1)) := by - simpa using internal_provable_of_outer_provable this + simpa using! internal_provable_of_outer_provable this simpa using TProof.specialize₂! this u t @[simp] lemma ne_symm (t u : Term V ℒₒᵣ) : T.internalize V ⊢ (t ≉ u) 🡒 (u ≉ t) := by @@ -51,7 +51,7 @@ open Entailment Entailment.FiniteContext Semiformula @[simp] lemma eq_uniform_trans (t₁ t₂ t₃ : Term V ℒₒᵣ) : T.internalize V ⊢ (t₁ ≐ t₂) 🡒 (t₂ ≐ t₃) 🡒 (t₁ ≐ t₃) := by have : T ⊢ “∀ x y z, x = y → y = z → x = z” := complete.{0} T _ fun (M : Type) _ _ ↦ by simp [models_iff] have : T.internalize V ⊢ ∀⁰ ∀⁰ ∀⁰ ((#'2 ≐ #'1) 🡒 (#'1 ≐ #'0) 🡒 (#'2 ≐ #'0)) := by - simpa using internal_provable_of_outer_provable this + simpa using! internal_provable_of_outer_provable this simpa using TProof.specialize₃! this t₃ t₂ t₁ variable {T} @@ -146,7 +146,7 @@ lemma term_replace_aux (t : V) : T.internalize V ⊢ ∀⁰ ∀⁰ ((#'1 ≐ #'0) 🡒 ((t + u).subst ![#'1] ≐ (t + u).subst ![#'0])) by have := (tprovable_iff_provable (T := T)).mp this rw [veq] - simpa [-subst_add, val_all] using this + simpa [-subst_add, val_all] using! this let Γ : List (Formula V ℒₒᵣ) := [&'1 ≐ &'0] suffices Γ ⊢[T.internalize V] t⇞⇞.subst ![&'1] + u⇞⇞.subst ![&'1] ≐ t⇞⇞.subst ![&'0] + u⇞⇞.subst ![&'0] by @@ -159,10 +159,10 @@ lemma term_replace_aux (t : V) : simpa [u] using ih 1 (by simp) have iht : Γ ⊢[T.internalize V] (t⇞⇞.subst ![&'1] ≐ t⇞⇞.subst ![&'0]) := by have := TProof.specialize₂_shift! iht &'0 &'1 - simpa [Semiterm.shift_substs, Semiterm.substs_substs] using this + simpa [Semiterm.shift_substs, Semiterm.substs_substs] using! this have ihu : Γ ⊢[T.internalize V] (u⇞⇞.subst ![&'1] ≐ u⇞⇞.subst ![&'0]) := by have := TProof.specialize₂_shift! ihu &'0 &'1 - simpa [Semiterm.shift_substs, Semiterm.substs_substs] using this + simpa [Semiterm.shift_substs, Semiterm.substs_substs] using! this have := subst_add_eq_add T (t⇞⇞.subst ![&'1]) (t⇞⇞.subst ![&'0]) (u⇞⇞.subst ![&'1]) (u⇞⇞.subst ![&'0]) exact of'! this ⨀ iht ⨀ ihu @@ -173,7 +173,7 @@ lemma term_replace_aux (t : V) : T.internalize V ⊢ ∀⁰ ∀⁰ ((#'1 ≐ #'0) 🡒 ((t * u).subst ![#'1] ≐ (t * u).subst ![#'0])) by have := (tprovable_iff_provable (T := T)).mp this rw [veq] - simpa [-subst_mul, val_all] using this + simpa [-subst_mul, val_all] using! this let Γ : List (Formula V ℒₒᵣ) := [&'1 ≐ &'0] suffices Γ ⊢[T.internalize V] t⇞⇞.subst ![&'1] * u⇞⇞.subst ![&'1] ≐ t⇞⇞.subst ![&'0] * u⇞⇞.subst ![&'0] by @@ -186,10 +186,10 @@ lemma term_replace_aux (t : V) : simpa [u] using ih 1 (by simp) have iht : Γ ⊢[T.internalize V] (t⇞⇞.subst ![&'1] ≐ t⇞⇞.subst ![&'0]) := by have := TProof.specialize₂_shift! iht &'0 &'1 - simpa [Semiterm.shift_substs, Semiterm.substs_substs] using this + simpa [Semiterm.shift_substs, Semiterm.substs_substs] using! this have ihu : Γ ⊢[T.internalize V] (u⇞⇞.subst ![&'1] ≐ u⇞⇞.subst ![&'0]) := by have := TProof.specialize₂_shift! ihu &'0 &'1 - simpa [Semiterm.shift_substs, Semiterm.substs_substs] using this + simpa [Semiterm.shift_substs, Semiterm.substs_substs] using! this have := subst_mul_eq_mul T (t⇞⇞.subst ![&'1]) (t⇞⇞.subst ![&'0]) (u⇞⇞.subst ![&'1]) (u⇞⇞.subst ![&'0]) exact of'! this ⨀ iht ⨀ ihu @@ -408,14 +408,14 @@ lemma replace_aux (φ : V) : have veq : v = ?[t.val, u.val] := by simp [t, u, vec2_eq hv.lh] suffices T.internalize V ⊢ ∀⁰ ∀⁰ ((#'1 ≐ #'0) 🡒 (t ≐ u).subst ![#'1] 🡒 (t ≐ u).subst ![#'0]) by have := (tprovable_iff_provable (T := T)).mp this - simpa [-substs_equals, veq, val_all] using this + simpa [-substs_equals, veq, val_all] using! this simpa using replace_eq T t u · let t : Semiterm V ℒₒᵣ 1 := ⟨v.[0], by simpa using hv.nth (by simp)⟩ let u : Semiterm V ℒₒᵣ 1 := ⟨v.[1], by simpa using hv.nth (by simp)⟩ have veq : v = ?[t.val, u.val] := by simp [t, u, vec2_eq hv.lh] suffices T.internalize V ⊢ ∀⁰ ∀⁰ ((#'1 ≐ #'0) 🡒 (t <' u).subst ![#'1] 🡒 (t <' u).subst ![#'0]) by have := (tprovable_iff_provable (T := T)).mp this - simpa [-substs_lessThan, veq, val_all] using this + simpa [-substs_lessThan, veq, val_all] using! this simpa using replace_lt T t u case hnrel => intro k R v hR hv @@ -425,14 +425,14 @@ lemma replace_aux (φ : V) : have veq : v = ?[t.val, u.val] := by simp [t, u, vec2_eq hv.lh] suffices T.internalize V ⊢ ∀⁰ ∀⁰ ((#'1 ≐ #'0) 🡒 (t ≉ u).subst ![#'1] 🡒 (t ≉ u).subst ![#'0]) by have := (tprovable_iff_provable (T := T)).mp this - simpa [-substs_notEquals, veq, val_all] using this + simpa [-substs_notEquals, veq, val_all] using! this simpa using replace_ne T t u · let t : Semiterm V ℒₒᵣ 1 := ⟨v.[0], by simpa using hv.nth (by simp)⟩ let u : Semiterm V ℒₒᵣ 1 := ⟨v.[1], by simpa using hv.nth (by simp)⟩ have veq : v = ?[t.val, u.val] := by simp [t, u, vec2_eq hv.lh] suffices T.internalize V ⊢ ∀⁰ ∀⁰ ((#'1 ≐ #'0) 🡒 (t ≮' u).subst ![#'1] 🡒 (t ≮' u).subst ![#'0]) by have := (tprovable_iff_provable (T := T)).mp this - simpa [-substs_notLessThan, veq, val_all] using this + simpa [-substs_notLessThan, veq, val_all] using! this simpa using replace_nlt T t u case hall => intro p hp ih @@ -463,7 +463,7 @@ lemma replace_aux (φ : V) : simpa only [Nat.reduceAdd, Fin.isValue, Nat.succ_eq_add_one, val_all, val_imp, val_equals, Semiterm.bvar_val, Fin.coe_ofNat_eq_mod, Nat.mod_succ, Nat.cast_one, Nat.zero_mod, Nat.cast_zero, val_substs, SemitermVec.val_succ, Matrix.head_cons, - Matrix.tail_cons, SemitermVec.val_nil] using this + Matrix.tail_cons, SemitermVec.val_nil] using! this have ih : T.internalize V ⊢ ∀⁰ ∀⁰ ((#'1 ≐ #'0) 🡒 φ⤉⤉.free1.subst ![#'1] 🡒 φ⤉⤉.free1.subst ![#'0]) := by apply (tprovable_iff_provable (T := T)).mpr simpa using ih diff --git a/Foundation/FirstOrder/Bootstrapping/FixedPoint.lean b/Foundation/FirstOrder/Bootstrapping/FixedPoint.lean index 44781c7c1..efe2fbb94 100644 --- a/Foundation/FirstOrder/Bootstrapping/FixedPoint.lean +++ b/Foundation/FirstOrder/Bootstrapping/FixedPoint.lean @@ -177,7 +177,7 @@ noncomputable def exclusiveMultifixedpoint (θ : Fin k → Semisentence ℒₒ theorem exclusiveMultidiagonal (θ : Fin k → Semisentence ℒₒᵣ k) : T ⊢ exclusiveMultifixedpoint θ i 🡘 (Rew.subst fun j ↦ ⌜exclusiveMultifixedpoint θ j⌝) ▹ θ i := by have : T ⊢ exclusiveMultifixedpoint θ i 🡘 ((Rew.subst fun j ↦ ⌜exclusiveMultifixedpoint θ j⌝) ▹ θ i).padding ↑i := by - simpa using multidiagonal (T := T) (fun j ↦ (θ j).padding j) (i := i) + simpa using! multidiagonal (T := T) (fun j ↦ (θ j).padding j) (i := i) exact Entailment.E!_trans this (Entailment.padding_iff _ _) lemma multifixedpoint_pi {θ : Fin k → Semisentence ℒₒᵣ k} (h : ∀ i, Hierarchy 𝚷 (m + 1) (θ i)) : diff --git a/Foundation/FirstOrder/Bootstrapping/Syntax/Formula/Basic.lean b/Foundation/FirstOrder/Bootstrapping/Syntax/Formula/Basic.lean index 359769ba7..e214ebb52 100644 --- a/Foundation/FirstOrder/Bootstrapping/Syntax/Formula/Basic.lean +++ b/Foundation/FirstOrder/Bootstrapping/Syntax/Formula/Basic.lean @@ -1156,7 +1156,7 @@ variable {L} section instance bv.defined : 𝚺₁-Function₁ bv (V := V) L via bvGraph L := .mk fun v ↦ by - simpa [bvGraph, Matrix.comp_vecCons', Matrix.constant_eq_singleton] using (BV.construction L).result_defined.defined ![v 0, 0, v 1] + simpa [bvGraph, Matrix.comp_vecCons', Matrix.constant_eq_singleton] using! (BV.construction L).result_defined.defined ![v 0, 0, v 1] instance bv.definable : 𝚺₁-Function₁ bv (V := V) L := bv.defined.to_definable diff --git a/Foundation/FirstOrder/Bootstrapping/Syntax/Formula/Coding.lean b/Foundation/FirstOrder/Bootstrapping/Syntax/Formula/Coding.lean index 0d381160b..adbae6e2e 100644 --- a/Foundation/FirstOrder/Bootstrapping/Syntax/Formula/Coding.lean +++ b/Foundation/FirstOrder/Bootstrapping/Syntax/Formula/Coding.lean @@ -78,8 +78,8 @@ noncomputable instance : LCWQIsoGödelQuote (Semiproposition L) (Bootstrapping.S bot := rfl and _ _ := rfl or _ _ := rfl - neg _ := by simpa [typedQuote] using typedQuote_neg _ - imply _ _ := by simpa [Bootstrapping.Semiformula.imp_def, imp_eq, typedQuote] using typedQuote_neg _ + neg _ := by simpa [typedQuote] using! typedQuote_neg _ + imply _ _ := by simpa [Bootstrapping.Semiformula.imp_def, imp_eq, typedQuote] using! typedQuote_neg _ all _ := rfl exs _ := rfl diff --git a/Foundation/FirstOrder/Bootstrapping/Syntax/Formula/Functions.lean b/Foundation/FirstOrder/Bootstrapping/Syntax/Formula/Functions.lean index 727dd6d79..0661107e6 100644 --- a/Foundation/FirstOrder/Bootstrapping/Syntax/Formula/Functions.lean +++ b/Foundation/FirstOrder/Bootstrapping/Syntax/Formula/Functions.lean @@ -65,7 +65,7 @@ variable {L} section instance neg.defined : 𝚺₁-Function₁ neg (V := V) L via negGraph L := .mk fun v ↦ by - simpa [negGraph, Matrix.comp_vecCons', Matrix.constant_eq_singleton] using construction.result_defined.defined ![v 0, 0, v 1] + simpa [negGraph, Matrix.comp_vecCons', Matrix.constant_eq_singleton] using! construction.result_defined.defined ![v 0, 0, v 1] instance neg.definable : 𝚺₁-Function₁ neg (V := V) L := neg.defined.to_definable @@ -282,7 +282,7 @@ variable {L} section instance shift.defined : 𝚺₁-Function₁[V] shift L via shiftGraph L := .mk fun v ↦ by - simpa [shiftGraph, Matrix.comp_vecCons', Matrix.constant_eq_singleton] using (construction L).result_defined.defined ![v 0, 0, v 1] + simpa [shiftGraph, Matrix.comp_vecCons', Matrix.constant_eq_singleton] using! (construction L).result_defined.defined ![v 0, 0, v 1] instance shift.definable : 𝚺₁-Function₁[V] shift L := shift.defined.to_definable @@ -481,23 +481,23 @@ lemma isUFormula_subst_ISigma1.sigma1_succ_induction {P : V → V → V → Prop (hexs : ∀ w p, IsUFormula L p → P (qVec L w) p (subst L (qVec L w) p) → P w (^∃ p) (^∃ (subst L (qVec L w) p))) : ∀ {w p}, IsUFormula L p → P w p (subst L w p) := by suffices ∀ param p, IsUFormula L p → P param p ((construction L).result L param p) by - intro w p hp; simpa using this w p hp + intro w p hp; simpa using! this w p hp apply (construction L).uformula_result_induction (P := fun param p y ↦ P param p y) · definability - · intro param k R v hkR hv; simpa using hRel param k R v hkR hv - · intro param k R v hkR hv; simpa using hNRel param k R v hkR hv - · intro param; simpa using hverum param - · intro param; simpa using hfalsum param + · intro param k R v hkR hv; simpa using! hRel param k R v hkR hv + · intro param k R v hkR hv; simpa using! hNRel param k R v hkR hv + · intro param; simpa using! hverum param + · intro param; simpa using! hfalsum param · intro param p q hp hq ihp ihq - simpa [subst] using + simpa [subst] using! hand param p q hp hq (by simpa [subst] using ihp) (by simpa [subst] using ihq) · intro param p q hp hq ihp ihq - simpa [subst] using + simpa [subst] using! hor param p q hp hq (by simpa [subst] using ihp) (by simpa [subst] using ihq) · intro param p hp ihp - simpa using hall param p hp (by simpa [construction] using ihp) + simpa using! hall param p hp (by simpa [construction] using! ihp) · intro param p hp ihp - simpa using hexs param p hp (by simpa [construction] using ihp) + simpa using! hexs param p hp (by simpa [construction] using! ihp) lemma semiformula_subst_induction {P : V → V → V → V → Prop} (hP : 𝚺₁-Relation₄ P) (hRel : ∀ n w k R v, L.IsRel k R → IsSemitermVec L k n v → P n w (^relk R v) (^rel k R (termSubstVec L k w v))) @@ -514,23 +514,23 @@ lemma semiformula_subst_induction {P : V → V → V → V → Prop} (hP : 𝚺 P (n + 1) (qVec L w) p (subst L (qVec L w) p) → P n w (^∃ p) (^∃ (subst L (qVec L w) p))) : ∀ {n p w}, IsSemiformula L n p → P n w p (subst L w p) := by suffices ∀ param n p, IsSemiformula L n p → P n param p ((construction L).result L param p) by - intro n p w hp; simpa using this w n p hp + intro n p w hp; simpa using! this w n p hp apply (construction L).semiformula_result_induction (P := fun param n p y ↦ P n param p y) · definability - · intro n param k R v hkR hv; simpa using hRel n param k R v hkR hv - · intro n param k R v hkR hv; simpa using hNRel n param k R v hkR hv - · intro n param; simpa using hverum n param - · intro n param; simpa using hfalsum n param + · intro n param k R v hkR hv; simpa using! hRel n param k R v hkR hv + · intro n param k R v hkR hv; simpa using! hNRel n param k R v hkR hv + · intro n param; simpa using! hverum n param + · intro n param; simpa using! hfalsum n param · intro n param p q hp hq ihp ihq - simpa [subst] using + simpa [subst] using! hand n param p q hp hq (by simpa [subst] using ihp) (by simpa [subst] using ihq) · intro n param p q hp hq ihp ihq - simpa [subst] using + simpa [subst] using! hor n param p q hp hq (by simpa [subst] using ihp) (by simpa [subst] using ihq) · intro n param p hp ihp - simpa using hall n param p hp (by simpa [construction] using ihp) + simpa using! hall n param p hp (by simpa [construction] using! ihp) · intro n param p hp ihp - simpa using hexs n param p hp (by simpa [construction] using ihp) + simpa using! hexs n param p hp (by simpa [construction] using! ihp) @[simp] lemma IsSemiformula.subst {n p m w : V} : IsSemiformula L n p → IsSemitermVec L n m w → IsSemiformula L m (subst L w p) := by @@ -875,7 +875,7 @@ variable {L} section instance formulaComplexity.defined : 𝚺₁-Function₁[V] formulaComplexity L via formulaComplexityGraph L := .mk fun v ↦ by - simpa [formulaComplexityGraph, Matrix.comp_vecCons', Matrix.constant_eq_singleton] using construction.result_defined.defined ![v 0, 0, v 1] + simpa [formulaComplexityGraph, Matrix.comp_vecCons', Matrix.constant_eq_singleton] using! construction.result_defined.defined ![v 0, 0, v 1] instance formulaComplexity.definable : 𝚺₁-Function₁[V] formulaComplexity L := formulaComplexity.defined.to_definable @@ -1208,28 +1208,28 @@ notation:78 x:78 " ^< " y:79 => qqLT x y notation:78 x:78 " ^≮ " y:79 => qqNLT x y @[simp] lemma lt_qqEQ_left (x y : V) : x < x ^= y := by - simpa using nth_lt_qqRel_of_lt (i := 0) (k := 2) (r := (eqIndex : V)) (v := ?[x, y]) (by simp) + simpa using! nth_lt_qqRel_of_lt (i := 0) (k := 2) (r := (eqIndex : V)) (v := ?[x, y]) (by simp) @[simp] lemma lt_qqEQ_right (x y : V) : y < x ^= y := by - simpa using nth_lt_qqRel_of_lt (i := 1) (k := 2) (r := (eqIndex : V)) (v := ?[x, y]) (by simp) + simpa using! nth_lt_qqRel_of_lt (i := 1) (k := 2) (r := (eqIndex : V)) (v := ?[x, y]) (by simp) @[simp] lemma lt_qqLT_left (x y : V) : x < x ^< y := by - simpa using nth_lt_qqRel_of_lt (i := 0) (k := 2) (r := (ltIndex : V)) (v := ?[x, y]) (by simp) + simpa using! nth_lt_qqRel_of_lt (i := 0) (k := 2) (r := (ltIndex : V)) (v := ?[x, y]) (by simp) @[simp] lemma lt_qqLT_right (x y : V) : y < x ^< y := by - simpa using nth_lt_qqRel_of_lt (i := 1) (k := 2) (r := (ltIndex : V)) (v := ?[x, y]) (by simp) + simpa using! nth_lt_qqRel_of_lt (i := 1) (k := 2) (r := (ltIndex : V)) (v := ?[x, y]) (by simp) @[simp] lemma lt_qqNEQ_left (x y : V) : x < x ^≠ y := by - simpa using nth_lt_qqNRel_of_lt (i := 0) (k := 2) (r := (eqIndex : V)) (v := ?[x, y]) (by simp) + simpa using! nth_lt_qqNRel_of_lt (i := 0) (k := 2) (r := (eqIndex : V)) (v := ?[x, y]) (by simp) @[simp] lemma lt_qqNEQ_right (x y : V) : y < x ^≠ y := by - simpa using nth_lt_qqNRel_of_lt (i := 1) (k := 2) (r := (eqIndex : V)) (v := ?[x, y]) (by simp) + simpa using! nth_lt_qqNRel_of_lt (i := 1) (k := 2) (r := (eqIndex : V)) (v := ?[x, y]) (by simp) @[simp] lemma lt_qqNLT_left (x y : V) : x < x ^≮ y := by - simpa using nth_lt_qqNRel_of_lt (i := 0) (k := 2) (r := (ltIndex : V)) (v := ?[x, y]) (by simp) + simpa using! nth_lt_qqNRel_of_lt (i := 0) (k := 2) (r := (ltIndex : V)) (v := ?[x, y]) (by simp) @[simp] lemma lt_qqNLT_right (x y : V) : y < x ^≮ y := by - simpa using nth_lt_qqNRel_of_lt (i := 1) (k := 2) (r := (ltIndex : V)) (v := ?[x, y]) (by simp) + simpa using! nth_lt_qqNRel_of_lt (i := 1) (k := 2) (r := (ltIndex : V)) (v := ?[x, y]) (by simp) def _root_.LO.FirstOrder.Arithmetic.qqEQDef : 𝚺₁.Semisentence 3 := .mkSigma “p x y. ∃ v, !mkVec₂Def v x y ∧ !qqRelDef p 2 ↑eqIndex v” diff --git a/Foundation/FirstOrder/Bootstrapping/Syntax/Language.lean b/Foundation/FirstOrder/Bootstrapping/Syntax/Language.lean index d338cdfa2..61db8e8c6 100644 --- a/Foundation/FirstOrder/Bootstrapping/Syntax/Language.lean +++ b/Foundation/FirstOrder/Bootstrapping/Syntax/Language.lean @@ -141,9 +141,9 @@ instance : (ℒₒᵣ).LORDefinable where func := .mkSigma “k f. (k = 0 ∧ f = 0) ∨ (k = 0 ∧ f = 1) ∨ (k = 2 ∧ f = 0) ∨ (k = 2 ∧ f = 1)” rel := .mkSigma “k r. (k = 2 ∧ r = 0) ∨ (k = 2 ∧ r = 1)” func_iff {k c} := by - simpa [models_iff] using Language.ORing.of_mem_range_encode_func + simpa [models_iff] using! Language.ORing.of_mem_range_encode_func rel_iff {k c} := by - simpa [models_iff] using Language.ORing.of_mem_range_encode_rel + simpa [models_iff] using! Language.ORing.of_mem_range_encode_rel namespace Arithmetic @@ -162,22 +162,22 @@ def eqIndex : ℕ := Encodable.encode (Language.Eq.eq : (ℒₒᵣ : FirstOrder. def ltIndex : ℕ := Encodable.encode (Language.LT.lt : (ℒₒᵣ : FirstOrder.Language).Rel 2) @[simp] lemma LOR_func_zeroIndex : (ℒₒᵣ).IsFunc 0 (zeroIndex : V) := by - simpa using codeIn_func_quote (V := V) (L := ℒₒᵣ) Language.Zero.zero + simpa using! codeIn_func_quote (V := V) (L := ℒₒᵣ) Language.Zero.zero @[simp] lemma LOR_func_oneIndex : (ℒₒᵣ).IsFunc 0 (oneIndex : V) := by - simpa using codeIn_func_quote (V := V) (L := ℒₒᵣ) Language.One.one + simpa using! codeIn_func_quote (V := V) (L := ℒₒᵣ) Language.One.one @[simp] lemma LOR_func_addIndex : (ℒₒᵣ).IsFunc 2 (addIndex : V) := by - simpa using codeIn_func_quote (V := V) (L := ℒₒᵣ) Language.Add.add + simpa using! codeIn_func_quote (V := V) (L := ℒₒᵣ) Language.Add.add @[simp] lemma LOR_func_mulIndex : (ℒₒᵣ).IsFunc 2 (mulIndex : V) := by - simpa using codeIn_func_quote (V := V) (L := ℒₒᵣ) Language.Mul.mul + simpa using! codeIn_func_quote (V := V) (L := ℒₒᵣ) Language.Mul.mul @[simp] lemma LOR_rel_eqIndex : (ℒₒᵣ).IsRel 2 (eqIndex : V) := by - simpa using codeIn_rel_quote (V := V) (L := ℒₒᵣ) Language.Eq.eq + simpa using! codeIn_rel_quote (V := V) (L := ℒₒᵣ) Language.Eq.eq @[simp] lemma LOR_rel_ltIndex : (ℒₒᵣ).IsRel 2 (ltIndex : V) := by - simpa using codeIn_rel_quote (V := V) (L := ℒₒᵣ) Language.LT.lt + simpa using! codeIn_rel_quote (V := V) (L := ℒₒᵣ) Language.LT.lt lemma func_def_LOR : (ℒₒᵣ).isFunc = .mkSigma “k f. (k = 0 ∧ f = 0) ∨ (k = 0 ∧ f = 1) ∨ (k = 2 ∧ f = 0) ∨ (k = 2 ∧ f = 1)” := rfl diff --git a/Foundation/FirstOrder/Bootstrapping/Syntax/Proof/Basic.lean b/Foundation/FirstOrder/Bootstrapping/Syntax/Proof/Basic.lean index 9ccbad744..01a327daf 100644 --- a/Foundation/FirstOrder/Bootstrapping/Syntax/Proof/Basic.lean +++ b/Foundation/FirstOrder/Bootstrapping/Syntax/Proof/Basic.lean @@ -830,9 +830,9 @@ end Derivable lemma internal_provable_iff_internal_derivable {φ : V} : Provable T φ ↔ Derivable T (insert φ ∅ : V) := by constructor · rintro ⟨b, hb⟩ - exact ⟨b, by simpa using hb⟩ + exact ⟨b, by simpa using! hb⟩ · rintro ⟨b, hb⟩ - exact ⟨b, by simpa using hb⟩ + exact ⟨b, by simpa using! hb⟩ alias ⟨Provable.toDerivable, Derivable.toProvable⟩ := internal_provable_iff_internal_derivable diff --git a/Foundation/FirstOrder/Bootstrapping/Syntax/Proof/Coding.lean b/Foundation/FirstOrder/Bootstrapping/Syntax/Proof/Coding.lean index 8de393fd3..b3f52a742 100644 --- a/Foundation/FirstOrder/Bootstrapping/Syntax/Proof/Coding.lean +++ b/Foundation/FirstOrder/Bootstrapping/Syntax/Proof/Coding.lean @@ -149,28 +149,29 @@ lemma isFormulaSet_sound {s : ℕ} : IsFormulaSet L s → ∃ S : Finset (Propos · intro h rcases Derivation2.Sequent.mem_quote h with ⟨p, hp, rfl⟩ rcases by simpa using hp with ⟨x, hx, rfl⟩ - simpa [hps x (mem_iff_mem_bitIndices.mpr hx)] using mem_iff_mem_bitIndices.mpr hx + have hxs : x ∈ s := mem_iff_mem_bitIndices.mpr (Nat.mem_bitIndices.mpr hx) + simpa [hps x hxs] using hxs · intro h rw [←hps x h] - simpa [Derivation2.Sequent.mem_quote_iff, ←mem_iff_mem_bitIndices] using ⟨x, h, rfl⟩⟩ + simpa [Derivation2.Sequent.mem_quote_iff] using ⟨x, Nat.mem_bitIndices.mp (mem_iff_mem_bitIndices.mp h), rfl⟩⟩ variable (V) noncomputable def typedQuote {Γ : Finset (Proposition L)} : T ⟹₂ Γ → T.internalize V ⊢!ᵈᵉʳ ⌜Γ⌝ - | closed Δ φ h hn => TDerivation.em ⌜φ⌝ (by simpa) (by simpa using Sequent.quote_mem_quote.mpr hn) + | closed Δ φ h hn => TDerivation.em ⌜φ⌝ (by simpa) (by simpa using! Sequent.quote_mem_quote.mpr hn) | axm φ hT hΓ => TDerivation.byAxm ⌜φ⌝ (by simp only [tmem, internalize_theory] exact (Δ₁Class.mem_iff'' (T := T) (φ := φ)).mpr hT) (by - simpa using Sequent.quote_mem_quote.mpr hΓ) - | verum h => TDerivation.verum (by simpa using Sequent.quote_mem_quote.mpr h) + simpa using! Sequent.quote_mem_quote.mpr hΓ) + | verum h => TDerivation.verum (by simpa using! Sequent.quote_mem_quote.mpr h) | and (φ := φ) (ψ := ψ) h bp bq => - TDerivation.and' (show ⌜φ⌝ ⋏ ⌜ψ⌝ ∈ ⌜Γ⌝ by simpa using Sequent.quote_mem_quote.mpr h) (bp.typedQuote.cast (by simp)) (bq.typedQuote.cast (by simp)) + TDerivation.and' (show ⌜φ⌝ ⋏ ⌜ψ⌝ ∈ ⌜Γ⌝ by simpa using! Sequent.quote_mem_quote.mpr h) (bp.typedQuote.cast (by simp)) (bq.typedQuote.cast (by simp)) | or (φ := φ) (ψ := ψ) h b => - TDerivation.or' (show ⌜φ⌝ ⋎ ⌜ψ⌝ ∈ ⌜Γ⌝ by simpa using Sequent.quote_mem_quote.mpr h) <| b.typedQuote.cast (by simp) + TDerivation.or' (show ⌜φ⌝ ⋎ ⌜ψ⌝ ∈ ⌜Γ⌝ by simpa using! Sequent.quote_mem_quote.mpr h) <| b.typedQuote.cast (by simp) | all (φ := φ) h d => - TDerivation.all' (show ∀⁰ ⌜φ⌝ ∈ ⌜Γ⌝ by simpa using Sequent.quote_mem_quote.mpr h) <| d.typedQuote.cast (by simp) + TDerivation.all' (show ∀⁰ ⌜φ⌝ ∈ ⌜Γ⌝ by simpa using! Sequent.quote_mem_quote.mpr h) <| d.typedQuote.cast (by simp) | exs (φ := φ) h t d => - TDerivation.exs' (show ∃⁰ ⌜φ⌝ ∈ ⌜Γ⌝ by simpa using Sequent.quote_mem_quote.mpr h) ⌜t⌝ <| d.typedQuote.cast (by simp [Matrix.constant_eq_singleton]) + TDerivation.exs' (show ∃⁰ ⌜φ⌝ ∈ ⌜Γ⌝ by simpa using! Sequent.quote_mem_quote.mpr h) ⌜t⌝ <| d.typedQuote.cast (by simp [Matrix.constant_eq_singleton]) | wk d ss => TDerivation.wk d.typedQuote (by simpa) | shift d => (TDerivation.shift d.typedQuote).cast (by simp) | cut (φ := φ) d dn => @@ -188,7 +189,7 @@ lemma coe_typedQuote_val_eq (d : T ⟹₂ Γ) : ↑(d.typedQuote ℕ).val = (d.t | closed Δ φ h hn => by simp [typedQuote, axL, nat_cast_pair, Sequent.coe_eq, Semiformula.coe_quote_eq_quote'] | axm φ hT _ => by - simpa [typedQuote, Bootstrapping.axm, nat_cast_pair, Sequent.coe_eq] using Sentence.coe_quote_eq_quote (V := V) φ + simpa [typedQuote, Bootstrapping.axm, nat_cast_pair, Sequent.coe_eq] using! Sentence.coe_quote_eq_quote (V := V) φ | verum h => by simp [typedQuote, Bootstrapping.verumIntro, nat_cast_pair, Sequent.coe_eq] | and h b₁ b₂ => by @@ -237,7 +238,7 @@ lemma quote_proof_def {φ : Sentence L} (b : T ⊢! φ) : (⌜b⌝ : V) = ⌜b.t @[simp] lemma proof_of_quote_proof {φ : Sentence L} (b : T ⊢! φ) : Proof T (⌜b⌝ : V) ⌜φ⌝ := by let x := Derivation2.typedQuote V b.toProof2 suffices Proof T x.val ⌜φ⌝ from this - simpa using x.derivationOf + simpa using! x.derivationOf lemma coe_quote_proof_eq (d : T ⊢! φ) : (↑(⌜d⌝ : ℕ) : V) = ⌜d⌝ := by simp [quote_proof_def, Derivation2.coe_quote_eq] @@ -333,7 +334,7 @@ noncomputable def Provable.sound2 {φ : Proposition L} (h : Provable T (⌜φ⌝ exact Derivation2.cast (Classical.choice b) hΓ lemma Provable.sound {φ : Sentence L} (h : Provable T (⌜φ⌝ : ℕ)) : T ⊢ φ := - provable_iff_derivable2.mpr ⟨Provable.sound2 (by simpa using h)⟩ + provable_iff_derivable2.mpr ⟨Provable.sound2 (by simpa using! h)⟩ end Arithmetic.Bootstrapping diff --git a/Foundation/FirstOrder/Bootstrapping/Syntax/Proof/Typed.lean b/Foundation/FirstOrder/Bootstrapping/Syntax/Proof/Typed.lean index 1885452be..1de220485 100644 --- a/Foundation/FirstOrder/Bootstrapping/Syntax/Proof/Typed.lean +++ b/Foundation/FirstOrder/Bootstrapping/Syntax/Proof/Typed.lean @@ -147,9 +147,9 @@ lemma TProvable.iff_provable {σ : Formula V L} : T ⊢ σ ↔ Provable T.theory σ.val := by constructor · intro b - simpa [←singleton_eq_insert] using TDerivation.toDerivable b.get + simpa [←singleton_eq_insert] using! TDerivation.toDerivable b.get · intro h - exact ⟨Derivable.toTDerivation _ <| by simpa [←singleton_eq_insert] using h⟩ + exact ⟨Derivable.toTDerivation _ <| by simpa [←singleton_eq_insert] using! h⟩ alias ⟨toProvable, _root_.LO.FirstOrder.Arithmetic.Bootstrapping.Provable.toTProvable⟩ := TProvable.iff_provable @@ -212,13 +212,13 @@ noncomputable def or' (H : φ ⋎ ψ ∈ Γ) (dpq : T ⊢!ᵈᵉʳ insert φ (in (or' H dpq : T ⊢!ᵈᵉʳ Γ).val = orIntro Γ.val φ.val ψ.val dpq.val := rfl noncomputable def all' {φ : Semiformula V L 1} (H : ∀⁰ φ ∈ Γ) (dp : T ⊢!ᵈᵉʳ insert φ.free Γ.shift) : T ⊢!ᵈᵉʳ Γ := - ⟨allIntro Γ.val φ.val dp.val, by simp, Derivation.allIntro (by simpa) (by simpa using dp.derivationOf)⟩ + ⟨allIntro Γ.val φ.val dp.val, by simp, Derivation.allIntro (by simpa) (by simpa using! dp.derivationOf)⟩ @[simp] lemma all'_val {φ : Semiformula V L 1} (H : ∀⁰ φ ∈ Γ) (dp : T ⊢!ᵈᵉʳ insert φ.free Γ.shift) : (all' H dp : T ⊢!ᵈᵉʳ Γ).val = allIntro Γ.val φ.val dp.val := rfl noncomputable def exs' {φ : Semiformula V L 1} (H : ∃⁰ φ ∈ Γ) (t : Term V L) (dp : T ⊢!ᵈᵉʳ insert (φ.subst ![t]) Γ) : T ⊢!ᵈᵉʳ Γ := - ⟨exsIntro Γ.val φ.val t.val dp.val, by simp, Derivation.exsIntro (by simpa) (by simp) (by simpa using dp.derivationOf)⟩ + ⟨exsIntro Γ.val φ.val t.val dp.val, by simp, Derivation.exsIntro (by simpa) (by simp) (by simpa using! dp.derivationOf)⟩ @[simp] lemma exs'_val {φ : Semiformula V L 1} (H : ∃⁰ φ ∈ Γ) (t : Term V L) (dp : T ⊢!ᵈᵉʳ insert (φ.subst ![t]) Γ) : (exs' H t dp : T ⊢!ᵈᵉʳ Γ).val = exsIntro Γ.val φ.val t.val dp.val := rfl @@ -248,11 +248,11 @@ noncomputable def or (dpq : T ⊢!ᵈᵉʳ insert φ (insert ψ Γ)) : T ⊢!ᵈ noncomputable def all {φ : Semiformula V L 1} (dp : T ⊢!ᵈᵉʳ insert φ.free Γ.shift) : T ⊢!ᵈᵉʳ insert (∀⁰ φ) Γ := Derivable.toTDerivation _ <| by - simpa using Derivable.all (by simp) (by simpa using dp.toDerivable) + simpa using! Derivable.all (by simp) (by simpa using! dp.toDerivable) noncomputable def exs {φ : Semiformula V L 1} (t : Term V L) (dp : T ⊢!ᵈᵉʳ insert (φ.subst ![t]) Γ) : T ⊢!ᵈᵉʳ insert (∃⁰ φ) Γ := Derivable.toTDerivation _ <| by - simpa using Derivable.exs (by simp) t.isSemiterm (by simpa using dp.toDerivable) + simpa using! Derivable.exs (by simp) t.isSemiterm (by simpa using! dp.toDerivable) def ofSubset (h : T ⊆ U) (d : T ⊢!ᵈᵉʳ Γ) : U ⊢!ᵈᵉʳ Γ where val := d.val @@ -401,7 +401,7 @@ noncomputable instance : Entailment.Minimal T where · exact TDerivation.em r noncomputable instance : Entailment.Cl T where - dne {φ} := by simpa [Axioms.DNE, Semiformula.imp_def] using TDerivation.or (TDerivation.em φ) + dne {φ} := by simpa [Axioms.DNE, Semiformula.imp_def] using! TDerivation.or (TDerivation.em φ) noncomputable def exsIntro (φ : Semiformula V L 1) (t : Term V L) (b : T ⊢! φ.subst ![t]) : T ⊢! (∃⁰ φ) := TDerivation.exs t b @@ -435,11 +435,11 @@ lemma specialize₃! {φ : Semiformula V L 3} (b : T ⊢ ∀⁰ ∀⁰ ∀⁰ φ lemma specialize₄! {φ : Semiformula V L 4} (b : T ⊢ ∀⁰ ∀⁰ ∀⁰ ∀⁰ φ) (t₁ t₂ t₃ t₄ : Term V L) : T ⊢ φ.subst ![t₁, t₂, t₃, t₄] := ⟨specialize₄ b.get _ _ _ _⟩ -noncomputable def shift {φ : Formula V L} (d : T ⊢! φ) : T ⊢! φ.shift := by simpa using TDerivation.shift d +noncomputable def shift {φ : Formula V L} (d : T ⊢! φ) : T ⊢! φ.shift := by simpa using! TDerivation.shift d -lemma shift! {φ : Formula V L} (d : T ⊢ φ) : T ⊢ φ.shift := ⟨by simpa using TDerivation.shift d.get⟩ +lemma shift! {φ : Formula V L} (d : T ⊢ φ) : T ⊢ φ.shift := ⟨by simpa using! TDerivation.shift d.get⟩ -noncomputable def all {φ : Semiformula V L 1} (dp : T ⊢! φ.free) : T ⊢! ∀⁰ φ := TDerivation.all (by simpa using dp) +noncomputable def all {φ : Semiformula V L 1} (dp : T ⊢! φ.free) : T ⊢! ∀⁰ φ := TDerivation.all (by simpa using! dp) noncomputable def all₂ {φ : Semiformula V L 2} (d : T ⊢! φ.shift.shift.subst ![Semiterm.fvar 0, Semiterm.fvar 1]) : T ⊢! ∀⁰ ∀⁰ φ := by @@ -528,7 +528,7 @@ noncomputable def exsImpExs {Γ} {φ ψ : Semiformula V L 1} (d : Γ.map .shift noncomputable def exs_imp_exs! {Γ} {φ ψ : Semiformula V L 1} (d : Γ.map .shift ⊢[T] φ.free 🡒 ψ.free) : Γ ⊢[T] ∃⁰ φ 🡒 ∃⁰ ψ := ⟨exsImpExs d.get⟩ -noncomputable def exs {φ : Semiformula V L 1} (t) (dp : T ⊢! φ.subst ![t]) : T ⊢! ∃⁰ φ := TDerivation.exs t (by simpa using dp) +noncomputable def exs {φ : Semiformula V L 1} (t) (dp : T ⊢! φ.subst ![t]) : T ⊢! ∃⁰ φ := TDerivation.exs t (by simpa using! dp) lemma exs! {φ : Semiformula V L 1} (t) (dp : T ⊢ φ.subst ![t]) : T ⊢ ∃⁰ φ := ⟨exs t dp.get⟩ diff --git a/Foundation/FirstOrder/Bootstrapping/Syntax/Term/Basic.lean b/Foundation/FirstOrder/Bootstrapping/Syntax/Term/Basic.lean index 5b4b929e0..61ab6309c 100644 --- a/Foundation/FirstOrder/Bootstrapping/Syntax/Term/Basic.lean +++ b/Foundation/FirstOrder/Bootstrapping/Syntax/Term/Basic.lean @@ -219,7 +219,7 @@ lemma case_iff {t : V} : (∃ z, t = ^#z) ∨ (∃ x, t = ^&x) ∨ (∃ k f v : V, L.IsFunc k f ∧ IsUTermVec L k v ∧ t = ^func k f v) := by - simpa [construction, Phi, IsUTermVec, and_assoc] using (construction L).case + simpa [construction, Phi, IsUTermVec, and_assoc] using! (construction L).case alias ⟨case, mk⟩ := case_iff diff --git a/Foundation/FirstOrder/Bootstrapping/Syntax/Term/Functions.lean b/Foundation/FirstOrder/Bootstrapping/Syntax/Term/Functions.lean index f7577a520..86e9908ab 100644 --- a/Foundation/FirstOrder/Bootstrapping/Syntax/Term/Functions.lean +++ b/Foundation/FirstOrder/Bootstrapping/Syntax/Term/Functions.lean @@ -205,14 +205,14 @@ variable {n : V} section instance termShift.defined : 𝚺₁-Function₁ termShift (V := V) L via termShiftGraph L := .mk fun v ↦ by - simpa [termShiftGraph, termShift] using construction.result_defined.defined v + simpa [termShiftGraph, termShift] using! construction.result_defined.defined v instance termShift.definable : 𝚺₁-Function₁ termShift (V := V) L := termShift.defined.to_definable instance termShift.definable' : Γ-[i + 1]-Function₁ termShift (V := V) L := termShift.definable.of_sigmaOne instance termShiftVec.defined : 𝚺₁-Function₂ termShiftVec (V := V) L via termShiftVecGraph L := .mk fun v ↦ by - simpa [termShiftVecGraph, termShiftVec] using construction.resultVec_defined.defined v + simpa [termShiftVecGraph, termShiftVec] using! construction.resultVec_defined.defined v instance termShiftVec.definable : 𝚺₁-Function₂ termShiftVec (V := V) L := termShiftVec.defined.to_definable @@ -338,14 +338,14 @@ variable {L} section instance termBShift.defined : 𝚺₁-Function₁ termBShift (V := V) L via termBShiftGraph L := .mk fun v ↦ by - simpa using construction.result_defined.defined v + simpa using! construction.result_defined.defined v instance termBShift.definable : 𝚺₁-Function₁ termBShift (V := V) L := termBShift.defined.to_definable instance termBShift.definable' : Γ-[i + 1]-Function₁ termBShift (V := V) L := termBShift.definable.of_sigmaOne instance termBShiftVec.defined : 𝚺₁-Function₂ termBShiftVec (V := V) L via termBShiftVecGraph L := .mk fun v ↦ by - simpa using construction.resultVec_defined.defined v + simpa using! construction.resultVec_defined.defined v instance termBShiftVec.definable : 𝚺₁-Function₂ termBShiftVec (V := V) L := termBShiftVec.defined.to_definable @@ -658,16 +658,16 @@ instance : Γ-[m + 1]-Function₂ (qqMul : V → V → V) := .of_sigmaOne qqMul_ end @[simp] lemma lt_qqAdd_left (x y : V) : x < x ^+ y := by - simpa using nth_lt_qqFunc_of_lt (i := 0) (k := 2) (f := (addIndex : V)) (v := ?[x, y]) (by simp) + simpa using! nth_lt_qqFunc_of_lt (i := 0) (k := 2) (f := (addIndex : V)) (v := ?[x, y]) (by simp) @[simp] lemma lt_qqAdd_right (x y : V) : y < x ^+ y := by - simpa using nth_lt_qqFunc_of_lt (i := 1) (k := 2) (f := (addIndex : V)) (v := ?[x, y]) (by simp) + simpa using! nth_lt_qqFunc_of_lt (i := 1) (k := 2) (f := (addIndex : V)) (v := ?[x, y]) (by simp) @[simp] lemma lt_qqMul_left (x y : V) : x < x ^* y := by - simpa using nth_lt_qqFunc_of_lt (i := 0) (k := 2) (f := (mulIndex : V)) (v := ?[x, y]) (by simp) + simpa using! nth_lt_qqFunc_of_lt (i := 0) (k := 2) (f := (mulIndex : V)) (v := ?[x, y]) (by simp) @[simp] lemma lt_qqMul_right (x y : V) : y < x ^* y := by - simpa using nth_lt_qqFunc_of_lt (i := 1) (k := 2) (f := (mulIndex : V)) (v := ?[x, y]) (by simp) + simpa using! nth_lt_qqFunc_of_lt (i := 1) (k := 2) (f := (mulIndex : V)) (v := ?[x, y]) (by simp) set_option backward.isDefEq.respectTransparency false in lemma qqFunc_absolute (k f v : ℕ) : ((^func k f v : ℕ) : V) = ^func (k : V) (f : V) (v : V) := by simp [qqFunc, nat_cast_pair] diff --git a/Foundation/FirstOrder/Bootstrapping/Syntax/Theory.lean b/Foundation/FirstOrder/Bootstrapping/Syntax/Theory.lean index 4975c8bc5..cd91b2bbe 100644 --- a/Foundation/FirstOrder/Bootstrapping/Syntax/Theory.lean +++ b/Foundation/FirstOrder/Bootstrapping/Syntax/Theory.lean @@ -63,7 +63,7 @@ namespace Δ₁ open Arithmetic.HierarchySymbol.Semiformula LO.FirstOrder.Theory -instance add (dT : T.Δ₁) (dU : U.Δ₁) : (T ∪ U).Δ₁ where +def add (dT : T.Δ₁) (dU : U.Δ₁) : (T ∪ U).Δ₁ where ch := T.Δ₁ch ⋎ U.Δ₁ch mem_iff {φ} := by simp only [Nat.succ_eq_add_one, Nat.reduceAdd, val_or, LogicalConnective.HomClass.map_or, diff --git a/Foundation/FirstOrder/Completeness/CanonicalModel.lean b/Foundation/FirstOrder/Completeness/CanonicalModel.lean index 43d16c4aa..33aa58618 100644 --- a/Foundation/FirstOrder/Completeness/CanonicalModel.lean +++ b/Foundation/FirstOrder/Completeness/CanonicalModel.lean @@ -180,10 +180,10 @@ lemma complete {φ : Proposition L} : ℙ⁻ ∀⊩ᶜ φ ↔ 𝐋𝐊¹ ⊢ φ constructor · intro h by_contra b - let p : ℙ⁻ := ⟨[∼φ], ⟨fun bφ ↦ b ⟨by simpa using bφ⟩⟩⟩ + let p : ℙ⁻ := ⟨[∼φ], ⟨fun bφ ↦ b ⟨by simpa using! bφ⟩⟩⟩ have hp : p ⊩ φᴺ := h p have hn : p ⊩ᶜ ∼φ := ⟨Forces.refl (∼φ)⟩ - have : ∀ q ≤ p, ¬q ⊩ φᴺ := by simpa [not] using hn + have : ∀ q ≤ p, ¬q ⊩ φᴺ := by simpa [not] using! hn have : ¬p ⊩ φᴺ := this p (by simp) contradiction · intro b diff --git a/Foundation/FirstOrder/Incompleteness/Dense.lean b/Foundation/FirstOrder/Incompleteness/Dense.lean index 5e1b05d9a..3561a89b1 100644 --- a/Foundation/FirstOrder/Incompleteness/Dense.lean +++ b/Foundation/FirstOrder/Incompleteness/Dense.lean @@ -73,7 +73,7 @@ lemma FirstOrder.Arithmetic.dense (T : Theory ℒₒᵣ) [𝗜𝚺₁ ⪯ T] [T. intro σ con have : 𝗜𝚺₁ ⪯ T := inferInstance have : 𝗜𝚺₁ ⪯ insert σ T := WeakerThan.trans this (Axiomatized.le_of_subset (by simp)) - simpa using Arithmetic.incomplete' (insert σ T) + simpa using! Arithmetic.incomplete' (insert σ T) instance (T : Theory ℒₒᵣ) [𝗜𝚺₁ ⪯ T] [T.Δ₁] : DenselyOrdered (LindenbaumAlgebra T) where dense _ _ := FirstOrder.Arithmetic.dense T diff --git a/Foundation/FirstOrder/Incompleteness/Halting.lean b/Foundation/FirstOrder/Incompleteness/Halting.lean index e4c759905..61ef921bd 100644 --- a/Foundation/FirstOrder/Incompleteness/Halting.lean +++ b/Foundation/FirstOrder/Incompleteness/Halting.lean @@ -22,12 +22,12 @@ lemma incomplete_of_REPred_not_ComputablePred_Nat' {P : ℕ → Prop} (hRE : REP apply ComputablePred.computable_iff_re_compl_re.mpr; constructor; . assumption; - . suffices REPred fun a : ℕ ↦ T ⊬ φ/[a] by simpa [hP] using this; + . suffices REPred fun a : ℕ ↦ T ⊬ φ/[a] by simpa [hP] using! this; have : 𝚺₁-Predicate fun b : ℕ ↦ Bootstrapping.Provable T (Bootstrapping.neg ℒₒᵣ <| Bootstrapping.subst ℒₒᵣ ?[Bootstrapping.Arithmetic.numeral b] ⌜φ⌝) := by clear hP; definability; apply REPred.of_eq (re_iff_sigma1.mpr this); intro a; push Not at h; - apply Iff.trans ?_ $ show T ⊢ ∼φ/[a] ↔ ¬T ⊢ φ/[a] by simpa [hP] using h a |>.symm; + apply Iff.trans ?_ $ show T ⊢ ∼φ/[a] ↔ ¬T ⊢ φ/[a] by simpa [hP] using! h a |>.symm; constructor; . rintro hP apply Bootstrapping.Provable.sound @@ -39,11 +39,11 @@ lemma incomplete_of_REPred_not_ComputablePred_Nat' {P : ℕ → Prop} (hRE : REP rcases hd with (⟨hd₁, hd₂⟩ | ⟨hd₁, hd₂⟩); . use d; constructor; - . simpa [hP] using hd₁; + . simpa [hP] using! hd₁; . simpa; . exfalso; apply Entailment.Consistent.not_bot (𝓢 := T) inferInstance; - replace hd₁ : T ⊢ φ/[d] := by simpa [hP] using hd₁; + replace hd₁ : T ⊢ φ/[d] := by simpa [hP] using! hd₁; cl_prover [hd₁, hd₂]; /-- diff --git a/Foundation/FirstOrder/Incompleteness/ProvabilityAbstraction/Basic.lean b/Foundation/FirstOrder/Incompleteness/ProvabilityAbstraction/Basic.lean index e1ff4b549..692ff47e6 100644 --- a/Foundation/FirstOrder/Incompleteness/ProvabilityAbstraction/Basic.lean +++ b/Foundation/FirstOrder/Incompleteness/ProvabilityAbstraction/Basic.lean @@ -184,7 +184,7 @@ variable def gödel [L.ReferenceableBy L] {T₀ T : Theory L} [Diagonalization T₀] (𝔅 : Provability T₀ T) : Sentence L := fixedpoint T₀ “x. ¬!𝔅.prov x” -lemma gödel_spec : T₀ ⊢ (gödel 𝔅) 🡘 ∼𝔅 (gödel 𝔅) := by simpa [gödel] using diag “x. ¬!𝔅.prov x”; +lemma gödel_spec : T₀ ⊢ (gödel 𝔅) 🡘 ∼𝔅 (gödel 𝔅) := by simpa [gödel, Provability.pr] using diag “x. ¬!𝔅.prov x”; section First @@ -271,7 +271,7 @@ variable {σ : Sentence L} local notation "𝐊" => kreisel 𝔅 lemma kreisel_spec : T₀ ⊢ (𝐊 σ) 🡘 (𝔅 (𝐊 σ) 🡒 σ) := by - simpa [kreisel, Rew.subst_comp_subst, ←TransitiveRewriting.comp_app] using diag “x. !𝔅.prov x → !σ”; + simpa [kreisel, Provability.pr, Rew.subst_comp_subst, ←TransitiveRewriting.comp_app] using diag “x. !𝔅.prov x → !σ”; private lemma kreisel_specAux₂ : T₀ ⊢ (𝔅 (𝐊 σ) 🡒 σ) 🡒 (𝐊 σ) := K!_right kreisel_spec diff --git a/Foundation/FirstOrder/Incompleteness/ProvabilityAbstraction/Refutability.lean b/Foundation/FirstOrder/Incompleteness/ProvabilityAbstraction/Refutability.lean index b428edd50..62d4887be 100644 --- a/Foundation/FirstOrder/Incompleteness/ProvabilityAbstraction/Refutability.lean +++ b/Foundation/FirstOrder/Incompleteness/ProvabilityAbstraction/Refutability.lean @@ -117,7 +117,7 @@ lemma jeroslow_not_safe [𝔅.FormalizedCompleteOn 𝐉] : T ⊢ 𝐉 🡒 (𝔅 lemma unprovable_flon [consis : Consistent T] [𝔅.FormalizedCompleteOn 𝐉] : T ⊬ flon 𝔅 𝔚 := by contrapose! consis; replace consis : T ⊢ ∀⁰ safe 𝔅 𝔚 := by simpa [flon] using consis; - have h₁ : T ⊢ ∼(𝔅 𝐉 ⋏ 𝔚 𝐉) := by simpa [safe] using FirstOrder.Theory.Proof.specialize _ _ ⨀ consis; + have h₁ : T ⊢ ∼(𝔅 𝐉 ⋏ 𝔚 𝐉) := by simpa [safe] using! FirstOrder.Theory.Proof.specialize _ _ ⨀ consis; have h₂ : T ⊢ ∼𝐉 := (contra! jeroslow_not_safe) ⨀ h₁; have h₃ : T ⊢ 𝐉 🡘 𝔚 𝐉 := jeroslow_def'; have h₄ : T ⊢ 𝔚 𝐉 := R1' h₂; diff --git a/Foundation/FirstOrder/Incompleteness/RosserProvability.lean b/Foundation/FirstOrder/Incompleteness/RosserProvability.lean index 335200dbb..23cbb891a 100644 --- a/Foundation/FirstOrder/Incompleteness/RosserProvability.lean +++ b/Foundation/FirstOrder/Incompleteness/RosserProvability.lean @@ -45,7 +45,7 @@ lemma rosser_quote_def {φ : Proposition L} : T.RosserProvable (V := V) ⌜φ⌝ ↔ ∃ b : V, Proof T b ⌜φ⌝ ∧ ∀ b' < b, ¬Proof T b' ⌜∼φ⌝ := rosser_quote lemma rosser_quote_def₀ {φ : Sentence L} : - T.RosserProvable (V := V) ⌜φ⌝ ↔ ∃ b : V, Proof T b ⌜φ⌝ ∧ ∀ b' < b, ¬Proof T b' ⌜∼φ⌝ := by simpa [Sentence.quote_def] using rosser_quote + T.RosserProvable (V := V) ⌜φ⌝ ↔ ∃ b : V, Proof T b ⌜φ⌝ ∧ ∀ b' < b, ¬Proof T b' ⌜∼φ⌝ := by simpa [Sentence.quote_def] using! rosser_quote def RosserProvable.to_provable {φ : V} : T.RosserProvable φ → Provable T φ := ProvabilityComparison.le_to_provable @@ -73,7 +73,7 @@ def rosser_internalize [Entailment.Consistent T] {φ : Sentence L} : T ⊢ φ contradiction def rosser_internalize_sentence [Entailment.Consistent T] {σ : Sentence L} : T ⊢ σ → T.RosserProvable (⌜σ⌝ : V) := fun h ↦ by - simpa [Sentence.quote_def] using rosser_internalize h + simpa [Sentence.quote_def] using! rosser_internalize h open Classical in def not_rosserProvable [Entailment.Consistent T] {φ : Sentence L} : T ⊢ ∼φ → ¬T.RosserProvable (⌜φ⌝ : V) := by @@ -89,7 +89,7 @@ def not_rosserProvable [Entailment.Consistent T] {φ : Sentence L} : T ⊢ ∼φ contradiction def not_rosserProvable_sentence [Entailment.Consistent T] {σ : Sentence L} : T ⊢ ∼σ → ¬T.RosserProvable (⌜σ⌝ : V) := fun h ↦ by - simpa [Sentence.quote_def] using not_rosserProvable h + simpa [Sentence.quote_def] using! not_rosserProvable h end LO.FirstOrder.Arithmetic.Bootstrapping diff --git a/Foundation/FirstOrder/Incompleteness/Yablo.lean b/Foundation/FirstOrder/Incompleteness/Yablo.lean index 365d229e8..381e99deb 100644 --- a/Foundation/FirstOrder/Incompleteness/Yablo.lean +++ b/Foundation/FirstOrder/Incompleteness/Yablo.lean @@ -94,7 +94,7 @@ lemma iff_yablo_provable (n : ℕ) : U ⊢ T.yabloPred n ↔ U ⊢ “∀ m, ↑ intro V _ _; haveI : V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁ := ModelsTheory.of_provably_subtheory V 𝗜𝚺₁ U inferInstance; haveI : V ⊧/![ORingStructure.numeral n] (T.yablo) ↔ T.YabloSystem ⌜T.yablo⌝ (ORingStructure.numeral n) := yablo_diagonal_modeled _; - simpa [models_iff, Matrix.constant_eq_singleton, Matrix.comp_vecCons'] using this; + simpa [models_iff, Matrix.constant_eq_singleton, Matrix.comp_vecCons'] using! this; lemma iff_neg_yablo_provable (n : ℕ) : U ⊢ ∼(T.yabloPred n) ↔ U ⊢ “∃ m, ↑n < m ∧ ∃ nσ, !ssnum nσ ⌜T.yablo⌝ m ∧ !(provable T) (nσ)” := by suffices U ⊢ ∼T.yablo/[n] 🡘 “∃ m, ↑n < m ∧ ∃ nσ, !ssnum nσ ⌜T.yablo⌝ m ∧ !(provable T) (nσ)” by diff --git a/Foundation/FirstOrder/Interpretation.lean b/Foundation/FirstOrder/Interpretation.lean index ad4fbaa0b..aac919501 100644 --- a/Foundation/FirstOrder/Interpretation.lean +++ b/Foundation/FirstOrder/Interpretation.lean @@ -109,7 +109,7 @@ variable {π} lemma dom_iff {x : M} : π.Dom x ↔ M ⊧/![x] π.domain := iff_of_eq rfl lemma domain_exists [Nonempty M] [M↓[L₁] ⊧* T] : ∃ x : M, π.Dom x := by - simpa [models_iff] using models_of_provable (M := M) inferInstance π.domain_nonempty + simpa [models_iff] using! models_of_provable (M := M) inferInstance π.domain_nonempty variable (π M) @@ -446,7 +446,7 @@ variable {L₁ L₂ L₃ : Language} [L₁.Eq] [L₂.Eq] [L₃.Eq] {T₁ : Theor def compDirectTranslation (τ : DirectTranslation T₂ L₃) (π : T₁ ⊳ T₂) : DirectTranslation T₁ L₃ where domain := π.trln.domain ⋏ π.translate τ.domain - domain_nonempty := by simpa [exs] using π.of_provability τ.domain_nonempty + domain_nonempty := by simpa [exs] using! π.of_provability τ.domain_nonempty rel R := π.translate (τ.rel R) func {k} f := π.translate (τ.func f) func_defined {k} f := by diff --git a/Foundation/FirstOrder/Intuitionistic/Deduction.lean b/Foundation/FirstOrder/Intuitionistic/Deduction.lean index 8d5d193be..f4987cab0 100644 --- a/Foundation/FirstOrder/Intuitionistic/Deduction.lean +++ b/Foundation/FirstOrder/Intuitionistic/Deduction.lean @@ -24,7 +24,7 @@ namespace Hilbertᵢ instance : SetLike (Hilbertᵢ L) (Propositionᵢ L) where coe := Hilbertᵢ.axiomSet - coe_injective' := by rintro ⟨T, _⟩ ⟨U, _⟩; simp + coe_injective := by rintro ⟨T, _⟩ ⟨U, _⟩; simp instance : LE (Hilbertᵢ L) where @@ -140,7 +140,7 @@ scoped notation "‖" d "‖" => depth d def specialize {φ} (b : Λ ⊢! ∀⁰ φ) (t) : Λ ⊢! φ/[t] := all₁ φ t ⨀ b def implyAll {φ ψ} (b : Λ ⊢! shift φ 🡒 free ψ) : Λ ⊢! φ 🡒 ∀⁰ ψ := - have : Λ ⊢! ∀⁰ (φ/[] 🡒 ψ) := gen <| by simpa using b + have : Λ ⊢! ∀⁰ (φ/[] 🡒 ψ) := gen <| by simp; exact b all₂ φ ψ ⨀ this def geNOverFiniteContext {Γ φ} (b : Γ⁺ ⊢[Λ]! free φ) : Γ ⊢[Λ]! ∀⁰ φ := @@ -285,7 +285,7 @@ variable {𝓗 : Hilbertᵢ L} {T : Theoryᵢ L 𝓗} instance : SetLike (Theoryᵢ L 𝓗) (Sentenceᵢ L) where coe := theory - coe_injective' _ _ := Theoryᵢ.ext + coe_injective _ _ := Theoryᵢ.ext lemma mem_def : φ ∈ T ↔ φ ∈ T.theory := by rfl diff --git a/Foundation/FirstOrder/Kripke/Intuitionistic.lean b/Foundation/FirstOrder/Kripke/Intuitionistic.lean index edff4a58a..132ccc12b 100644 --- a/Foundation/FirstOrder/Kripke/Intuitionistic.lean +++ b/Foundation/FirstOrder/Kripke/Intuitionistic.lean @@ -251,8 +251,8 @@ lemma sound {T : Theoryᵢ L 𝗜𝗻𝘁¹} (b : T ⊢ φ) : W ∀⊩* T → W suffices ∀ φ ∈ Γ, w ⊩[![]|fun _ ↦ x] φ by simpa intro φ hφ rcases show ∃ x ∈ T.theory, ↑x = φ by simpa using HΓ φ hφ with ⟨φ, hφ', rfl⟩ - simpa using H _ hφ' w - simpa using this + simp only [Forces.forces_emb]; exact H _ hφ' w + simp only [Forces.forces_emb] at this; exact this end Forces₀ diff --git a/Foundation/FirstOrder/Kripke/WeakForcing.lean b/Foundation/FirstOrder/Kripke/WeakForcing.lean index 213ed518b..c7dc61334 100644 --- a/Foundation/FirstOrder/Kripke/WeakForcing.lean +++ b/Foundation/FirstOrder/Kripke/WeakForcing.lean @@ -289,7 +289,7 @@ lemma sound : 𝐋𝐊¹ ⊢ φ → ∀ p : ℙ, ∀ fv, (∀ i, p ⊩↓ fv i) exact Forces.sound p fv Hfv this lemma sound₀ {σ : Sentence L} : 𝐋𝐊¹ ⊢ (σ : Proposition L) → ℙ ∀⊩ᶜ σ := fun b p ↦ by - simpa using sound b p (fun _ ↦ (Classical.ofNonempty : p).val) fun _ ↦ by simp + simpa using! sound b p (fun _ ↦ (Classical.ofNonempty : p).val) fun _ ↦ by simp end WeaklyForces₀ diff --git a/Foundation/FirstOrder/SetTheory/LoewenheimSkolem.lean b/Foundation/FirstOrder/SetTheory/LoewenheimSkolem.lean index 1a1cf42ec..dc4481501 100644 --- a/Foundation/FirstOrder/SetTheory/LoewenheimSkolem.lean +++ b/Foundation/FirstOrder/SetTheory/LoewenheimSkolem.lean @@ -45,14 +45,14 @@ lemma closed {v : Fin k → V} (hv : ∀ i, v i ∈ Hull s) rw [str_eq] at this exact this -instance set_nonempty : (Hull s).Nonempty := Structure.SkolemHull.set_nonempty _ _ +lemma set_nonempty : (Hull s).Nonempty := Structure.SkolemHull.set_nonempty _ _ instance nonempty : Nonempty (Hull s) := Structure.SkolemHull.nonempty _ _ instance elementaryEquiv : (Hull s) ≡ₑ[ℒₛₑₜ] V where models {φ} := by simp [models_iff, Matrix.empty_eq] -instance set_countable [hs : Countable s] : (Hull s).Countable := Structure.SkolemHull.set_countable hs +lemma set_countable [hs : Countable s] : (Hull s).Countable := Structure.SkolemHull.set_countable hs instance countable [hs : Countable s] : Countable (Hull s) := Structure.SkolemHull.set_countable hs diff --git a/Foundation/FirstOrder/SetTheory/Ordinal.lean b/Foundation/FirstOrder/SetTheory/Ordinal.lean index e580eab2d..9d988403c 100644 --- a/Foundation/FirstOrder/SetTheory/Ordinal.lean +++ b/Foundation/FirstOrder/SetTheory/Ordinal.lean @@ -150,7 +150,7 @@ protected instance succ [h : IsOrdinal α] : IsOrdinal (succ α) where · simp_all · exact h.trichotomy β₁ h₁ β₂ h₂ -protected instance nat : α ∈ (ω : V) → IsOrdinal (α : V) := by +protected lemma nat : α ∈ (ω : V) → IsOrdinal (α : V) := by apply naturalNumber_induction · definability case zero => simp [zero_def] diff --git a/Foundation/FirstOrder/SetTheory/Universe.lean b/Foundation/FirstOrder/SetTheory/Universe.lean index d5d473014..2c6f352ec 100644 --- a/Foundation/FirstOrder/SetTheory/Universe.lean +++ b/Foundation/FirstOrder/SetTheory/Universe.lean @@ -31,7 +31,7 @@ variable {α : Type (u + 1)} instance : SetLike (UniverseFunctor α) α where coe := set - coe_injective' _ _ := UniverseFunctor.ext + coe_injective _ _ := UniverseFunctor.ext instance (s : UniverseFunctor α) : Small.{u} s.set := s.small @@ -90,7 +90,7 @@ noncomputable def mkFun {ι : Type u} (f : ι → Universe.{u}) : Universe.{u} : instance : SetLike Universe.{u} Universe.{u} where coe x := x.dest.set - coe_injective' x y e := by + coe_injective x y e := by have h (x : Universe.{u}) : mk x.dest.set = x := QPF.Fix.mk_dest _ have : mk x.dest.set = mk y.dest.set := by simp_all simpa [h] using this @@ -129,14 +129,14 @@ noncomputable def rec (g : (s : Set α) → [Small.{u} s] → α) : Universe → lemma rec_mk (g : (s : Set α) → [Small.{u} s] → α) (s : Set Universe.{u}) [small : Small.{u} s] : rec g (mk s) = g (rec g '' s) := by - simpa using QPF.Fix.rec_eq (F := UniverseFunctor) (fun p ↦ g p.set) ⟨s, small⟩ + exact QPF.Fix.rec_eq (F := UniverseFunctor) (fun p ↦ g p.set) ⟨s, small⟩ @[elab_as_elim] theorem ind {P : Universe.{u} → Prop} (ind : ∀ x, (∀ y ∈ x, P y) → P x) (x : Universe) : P x := - QPF.Fix.ind P (fun s hs ↦ ind (mk s.set) (by simpa using hs)) x + QPF.Fix.ind P (fun s hs ↦ ind (mk s.set) (by simpa using! hs)) x lemma wellFounded : WellFounded (α := Universe.{u}) (· ∈ ·) := ⟨ind fun x ih ↦ Acc.intro x ih⟩ diff --git a/Foundation/FirstOrder/SetTheory/Z.lean b/Foundation/FirstOrder/SetTheory/Z.lean index b9fe775cc..906fe0fa4 100644 --- a/Foundation/FirstOrder/SetTheory/Z.lean +++ b/Foundation/FirstOrder/SetTheory/Z.lean @@ -51,7 +51,7 @@ lemma SSubset.of_subset_of_not_mem_of_mem {x y z : V} (ss : x ⊆ y) (hzx : z /-! ## Axiom of empty set -/ -lemma empty_exists : ∃ e : V, IsEmpty e := by simpa [models_iff] using Theory.models V 𝗭 Zermelo.axiom_of_empty_set +lemma empty_exists : ∃ e : V, IsEmpty e := by simpa [models_iff] using! Theory.models V 𝗭 Zermelo.axiom_of_empty_set lemma empty_existsUnique : ∃! e : V, IsEmpty e := by rcases empty_exists (V := V) with ⟨e, he⟩ @@ -619,7 +619,7 @@ lemma IsInductive.zero {I : V} (hI : IsInductive I) : ∅ ∈ I := hI.1 lemma IsInductive.succ {I : V} (hI : IsInductive I) {x : V} (hx : x ∈ I) : succ x ∈ I := hI.2 x hx lemma isInductive_exists : ∃ I : V, IsInductive I := by - simpa [models_iff, Axiom.infinity] using Theory.models V 𝗭 Zermelo.axiom_of_infinity + simpa [models_iff, Axiom.infinity] using! Theory.models V 𝗭 Zermelo.axiom_of_infinity lemma omega_existsUnique : ∃! ω : V, ∀ x, x ∈ ω ↔ ∀ I : V, IsInductive I → x ∈ I := by rcases isInductive_exists (V := V) with ⟨I, hI⟩ diff --git a/Foundation/FirstOrder/Skolemization/Hull.lean b/Foundation/FirstOrder/Skolemization/Hull.lean index a5bcb32bc..e6b74def4 100644 --- a/Foundation/FirstOrder/Skolemization/Hull.lean +++ b/Foundation/FirstOrder/Skolemization/Hull.lean @@ -80,7 +80,7 @@ lemma closed_func {v : Fin k → M} (hv : ∀ i, v i ∈ SkolemHull L s) closed hv (φ := “#0 = !!(Semiterm.func f fun i ↦ #i.succ)”) (by simp [Semiterm.val_func]; simp [Function.comp_def]) rcases this with ⟨z, hz, e⟩ - have : z = func f v := by simpa [Semiterm.val_func] using e + have : z = func f v := by simpa [Semiterm.val_func] using! e rcases this; assumption variable (𝓼 s) @@ -89,7 +89,7 @@ instance (priority := 50) str : Structure L (SkolemHull L s) where func k f v := ⟨func f fun i ↦ (v i : M), closed_func (by simp)⟩ rel k R v := Structure.rel R fun i ↦ (v i : M) -instance set_nonempty : (SkolemHull L s).Nonempty := by +lemma set_nonempty : (SkolemHull L s).Nonempty := by have : ∃ z : M, (⊤ : Semisentence L 1).Evalb ![z] := by simp have : ∃ z, z ∈ SkolemHull L s := by simpa using closed (s := s) (by simp) this @@ -156,7 +156,7 @@ instance (priority := 50) membership : instance (priority := 50) mem [Operator.Mem L] [Membership M M] [Structure.Mem L M] : Structure.Mem L (SkolemHull L s) := ⟨fun x y ↦ by - simpa [Operator.val, Matrix.fun_eq_vec_two] using Structure.Mem.mem (L := L) (M := M) x.val y.val⟩ + simpa [Operator.val, Matrix.fun_eq_vec_two] using! Structure.Mem.mem (L := L) (M := M) x.val y.val⟩ end mem @@ -168,12 +168,12 @@ open Cardinal variable [L.Encodable] {s : Set M} -instance set_countable (hs : s.Countable) : (SkolemHull L s).Countable := by +lemma set_countable (hs : s.Countable) : (SkolemHull L s).Countable := by have : Countable s := hs have : Countable (Term L.skolemFunction₁ s) := Semiterm.countable exact Set.countable_range _ -instance countable (hs : s.Countable) : Countable (SkolemHull L s) := set_countable hs +lemma countable (hs : s.Countable) : Countable (SkolemHull L s) := set_countable hs instance countable₀ : Countable (SkolemHull₀ L M) := set_countable (by simp) diff --git a/Foundation/FirstOrder/Ultraproduct.lean b/Foundation/FirstOrder/Ultraproduct.lean index eb97a3e72..fa6ec0046 100644 --- a/Foundation/FirstOrder/Ultraproduct.lean +++ b/Foundation/FirstOrder/Ultraproduct.lean @@ -71,12 +71,12 @@ lemma eval_Uprod [(i : I) → Nonempty (A i)] {φ : Semiformula L ξ n} : case hrel k r v => simp [Semiterm.val_Uprod, Function.comp_def] case hnrel k r v => - simpa [*, eval_nrel, Semiterm.val_Uprod] - using Ultrafilter.compl_mem_iff_notMem.symm + simpa [*, eval_nrel, Semiterm.val_Uprod, Function.comp_def] + using! Ultrafilter.compl_mem_iff_notMem.symm case hand => - simpa [*, -Filter.inter_mem_iff] using Filter.inter_mem_iff.symm + simpa [*, -Filter.inter_mem_iff, Function.comp_def] using! Filter.inter_mem_iff.symm case hor φ ψ ihp ihq => - simpa [*, -Ultrafilter.union_mem_iff] using Ultrafilter.union_mem_iff.symm + simpa [*, -Ultrafilter.union_mem_iff, Function.comp_def] using! Ultrafilter.union_mem_iff.symm case hall φ _ => suffices (∀ x : Uprod A 𝓤, {i | (Eval (fun j ↦ ((x :> e) j).val i) fun x ↦ (ε x).val i) φ} ∈ 𝓤) ↔ diff --git a/Foundation/InterpretabilityLogic/Hilbert/Basic/Basic.lean b/Foundation/InterpretabilityLogic/Hilbert/Basic/Basic.lean index 3b0266727..793ae0566 100644 --- a/Foundation/InterpretabilityLogic/Hilbert/Basic/Basic.lean +++ b/Foundation/InterpretabilityLogic/Hilbert/Basic/Basic.lean @@ -53,7 +53,9 @@ instance : Logic.Substitution (Hilbert.Basic Ax) where subst {φ} s h := by rw [Logic.iff_provable] at h ⊢; induction h with - | @axm _ s' ih => simpa using Basic.axm (s := s' ∘ s) ih; + | @axm _ s' ih => + have h := Basic.axm (s := s' ∘ s) ih; + simp at h; exact h; | mdp hφψ hφ ihφψ ihφ => apply Basic.mdp ihφψ ihφ; | nec hφ ihφ => apply Basic.nec ihφ; | implyK φ ψ => apply Basic.implyK; @@ -116,15 +118,16 @@ variable [DecidableEq α] instance [Ax.HasJ1] : InterpretabilityLogic.Entailment.HasAxiomJ1 (Hilbert.Basic Ax) where axiomJ1! {φ ψ} := by constructor; - simpa [HasJ1.ne_pq] using Hilbert.Basic.axm + have h := Hilbert.Basic.axm (φ := InterpretabilityLogic.Axioms.J1 (.atom (HasJ1.p Ax)) (.atom (HasJ1.q Ax))) (s := λ b => if (HasJ1.p Ax) = b then φ else if (HasJ1.q Ax) = b then ψ else (.atom b)) (HasJ1.mem_J1); + simp [HasJ1.ne_pq] at h; exact h; instance [Ax.HasJ2] : InterpretabilityLogic.Entailment.HasAxiomJ2 (Hilbert.Basic Ax) where axiomJ2! {φ ψ χ} := by constructor; - simpa [HasJ2.ne_pq, HasJ2.ne_qr, HasJ2.ne_rp.symm] using Hilbert.Basic.axm + have h := Hilbert.Basic.axm (φ := InterpretabilityLogic.Axioms.J2 (.atom (HasJ2.p Ax)) (.atom (HasJ2.q Ax)) (.atom (HasJ2.r Ax))) (s := λ b => if (HasJ2.p Ax) = b then φ @@ -132,11 +135,12 @@ instance [Ax.HasJ2] : InterpretabilityLogic.Entailment.HasAxiomJ2 (Hilbert.Basic else if (HasJ2.r Ax) = b then χ else (.atom b)) $ HasJ2.mem_J2; + simp [HasJ2.ne_pq, HasJ2.ne_qr, HasJ2.ne_rp.symm] at h; exact h; instance [Ax.HasJ3] : InterpretabilityLogic.Entailment.HasAxiomJ3 (Hilbert.Basic Ax) where axiomJ3! {φ ψ χ} := by constructor; - simpa [HasJ3.ne_pq, HasJ3.ne_qr, HasJ3.ne_rp.symm] using Hilbert.Basic.axm + have h := Hilbert.Basic.axm (φ := InterpretabilityLogic.Axioms.J3 (.atom (HasJ3.p Ax)) (.atom (HasJ3.q Ax)) (.atom (HasJ3.r Ax))) (s := λ b => if (HasJ3.p Ax) = b then φ @@ -144,27 +148,30 @@ instance [Ax.HasJ3] : InterpretabilityLogic.Entailment.HasAxiomJ3 (Hilbert.Basic else if (HasJ3.r Ax) = b then χ else (.atom b)) $ HasJ3.mem_J3; + simp [HasJ3.ne_pq, HasJ3.ne_qr, HasJ3.ne_rp.symm] at h; exact h; instance [Ax.HasJ4] : InterpretabilityLogic.Entailment.HasAxiomJ4 (Hilbert.Basic Ax) where axiomJ4! {φ ψ} := by constructor; - simpa [HasJ4.ne_pq] using Hilbert.Basic.axm + have h := Hilbert.Basic.axm (φ := InterpretabilityLogic.Axioms.J4 (.atom (HasJ4.p Ax)) (.atom (HasJ4.q Ax))) (s := λ b => if (HasJ4.p Ax) = b then φ else if (HasJ4.q Ax) = b then ψ else (.atom b)) (HasJ4.mem_J4); + simp [HasJ4.ne_pq] at h; exact h; instance [Ax.HasJ5] : InterpretabilityLogic.Entailment.HasAxiomJ5 (Hilbert.Basic Ax) where axiomJ5! {φ} := by constructor; - simpa using Hilbert.Basic.axm + have h := Hilbert.Basic.axm (φ := InterpretabilityLogic.Axioms.J5 (.atom (HasJ5.p Ax))) (s := λ b => if (HasJ5.p Ax) = b then φ else (.atom b)) (HasJ5.mem_J5); + simp at h; exact h; instance [Ax.HasM] : InterpretabilityLogic.Entailment.HasAxiomM (Hilbert.Basic Ax) where axiomM! {φ ψ χ} := by constructor; - simpa [HasM.ne_pq, HasM.ne_qr, HasM.ne_rp.symm] using Hilbert.Basic.axm + have h := Hilbert.Basic.axm (φ := InterpretabilityLogic.Axioms.M (.atom (HasM.p Ax)) (.atom (HasM.q Ax)) (.atom (HasM.r Ax))) (s := λ b => if (HasM.p Ax) = b then φ @@ -172,11 +179,12 @@ instance [Ax.HasM] : InterpretabilityLogic.Entailment.HasAxiomM (Hilbert.Basic A else if (HasM.r Ax) = b then χ else (.atom b)) $ HasM.mem_M; + simp [HasM.ne_pq, HasM.ne_qr, HasM.ne_rp.symm] at h; exact h; instance [Ax.HasM] : InterpretabilityLogic.Entailment.HasAxiomM (Hilbert.Basic Ax) where axiomM! {φ ψ χ} := by constructor; - simpa [HasM.ne_pq, HasM.ne_qr, HasM.ne_rp.symm] using Hilbert.Basic.axm + have h := Hilbert.Basic.axm (φ := InterpretabilityLogic.Axioms.M (.atom (HasM.p Ax)) (.atom (HasM.q Ax)) (.atom (HasM.r Ax))) (s := λ b => if (HasM.p Ax) = b then φ @@ -184,11 +192,12 @@ instance [Ax.HasM] : InterpretabilityLogic.Entailment.HasAxiomM (Hilbert.Basic A else if (HasM.r Ax) = b then χ else (.atom b)) $ HasM.mem_M; + simp [HasM.ne_pq, HasM.ne_qr, HasM.ne_rp.symm] at h; exact h; instance [Ax.HasM₀] : InterpretabilityLogic.Entailment.HasAxiomM₀ (Hilbert.Basic Ax) where axiomM₀! {φ ψ χ} := by constructor; - simpa [HasM₀.ne_pq, HasM₀.ne_qr, HasM₀.ne_rp.symm] using Hilbert.Basic.axm + have h := Hilbert.Basic.axm (φ := InterpretabilityLogic.Axioms.M₀ (.atom (HasM₀.p Ax)) (.atom (HasM₀.q Ax)) (.atom (HasM₀.r Ax))) (s := λ b => if (HasM₀.p Ax) = b then φ @@ -196,35 +205,39 @@ instance [Ax.HasM₀] : InterpretabilityLogic.Entailment.HasAxiomM₀ (Hilbert.B else if (HasM₀.r Ax) = b then χ else (.atom b)) $ HasM₀.mem_M₀; + simp [HasM₀.ne_pq, HasM₀.ne_qr, HasM₀.ne_rp.symm] at h; exact h; instance [Ax.HasP] : InterpretabilityLogic.Entailment.HasAxiomP (Hilbert.Basic Ax) where axiomP! {φ ψ} := by constructor; - simpa [HasP.ne_pq] using Hilbert.Basic.axm + have h := Hilbert.Basic.axm (φ := InterpretabilityLogic.Axioms.P (.atom (HasP.p Ax)) (.atom (HasP.q Ax))) (s := λ b => if (HasP.p Ax) = b then φ else if (HasP.q Ax) = b then ψ else (.atom b)) (HasP.mem_P); + simp [HasP.ne_pq] at h; exact h; instance [Ax.HasP₀] : InterpretabilityLogic.Entailment.HasAxiomP₀ (Hilbert.Basic Ax) where axiomP₀! {φ ψ} := by constructor; - simpa [HasP₀.ne_pq] using Hilbert.Basic.axm + have h := Hilbert.Basic.axm (φ := InterpretabilityLogic.Axioms.P₀ (.atom (HasP₀.p Ax)) (.atom (HasP₀.q Ax))) (s := λ b => if (HasP₀.p Ax) = b then φ else if (HasP₀.q Ax) = b then ψ else (.atom b)) (HasP₀.mem_P₀); + simp [HasP₀.ne_pq] at h; exact h; instance [Ax.HasW] : InterpretabilityLogic.Entailment.HasAxiomW (Hilbert.Basic Ax) where axiomW! {φ ψ} := by constructor; - simpa [HasW.ne_pq] using Hilbert.Basic.axm + have h := Hilbert.Basic.axm (φ := InterpretabilityLogic.Axioms.W (.atom (HasW.p Ax)) (.atom (HasW.q Ax))) (s := λ b => if (HasW.p Ax) = b then φ else if (HasW.q Ax) = b then ψ else (.atom b)) (HasW.mem_W); + simp [HasW.ne_pq] at h; exact h; instance [Ax.HasWstar] : InterpretabilityLogic.Entailment.HasAxiomWstar (Hilbert.Basic Ax) where axiomWstar! {φ ψ χ} := by constructor; - simpa [HasWstar.ne_pq, HasWstar.ne_qr, HasWstar.ne_rp.symm] using Hilbert.Basic.axm + have h := Hilbert.Basic.axm (φ := InterpretabilityLogic.Axioms.Wstar (.atom (HasWstar.p Ax)) (.atom (HasWstar.q Ax)) (.atom (HasWstar.r Ax))) (s := λ b => if (HasWstar.p Ax) = b then φ @@ -232,35 +245,39 @@ instance [Ax.HasWstar] : InterpretabilityLogic.Entailment.HasAxiomWstar (Hilbert else if (HasWstar.r Ax) = b then χ else (.atom b)) $ HasWstar.mem_Wstar; + simp [HasWstar.ne_pq, HasWstar.ne_qr, HasWstar.ne_rp.symm] at h; exact h; instance [Ax.HasKW1Zero] : InterpretabilityLogic.Entailment.HasAxiomKW1Zero (Hilbert.Basic Ax) where axiomKW1Zero! {φ ψ} := by constructor; - simpa [HasKW1Zero.ne_pq] using Hilbert.Basic.axm + have h := Hilbert.Basic.axm (φ := InterpretabilityLogic.Axioms.KW1Zero (.atom (HasKW1Zero.p Ax)) (.atom (HasKW1Zero.q Ax))) (s := λ b => if (HasKW1Zero.p Ax) = b then φ else if (HasKW1Zero.q Ax) = b then ψ else (.atom b)) (HasKW1Zero.mem_KW1Zero); + simp [HasKW1Zero.ne_pq] at h; exact h; instance [Ax.HasKW2] : InterpretabilityLogic.Entailment.HasAxiomKW2 (Hilbert.Basic Ax) where axiomKW2! {φ ψ} := by constructor; - simpa [HasKW2.ne_pq] using Hilbert.Basic.axm + have h := Hilbert.Basic.axm (φ := InterpretabilityLogic.Axioms.KW2 (.atom (HasKW2.p Ax)) (.atom (HasKW2.q Ax))) (s := λ b => if (HasKW2.p Ax) = b then φ else if (HasKW2.q Ax) = b then ψ else (.atom b)) (HasKW2.mem_KW2); + simp [HasKW2.ne_pq] at h; exact h; instance [Ax.HasF] : InterpretabilityLogic.Entailment.HasAxiomF (Hilbert.Basic Ax) where axiomF! {φ} := by constructor; - simpa using Hilbert.Basic.axm + have h := Hilbert.Basic.axm (φ := InterpretabilityLogic.Axioms.F (.atom (HasF.p Ax))) (s := λ b => if (HasF.p Ax) = b then φ else (.atom b)) (HasF.mem_F); + simp at h; exact h; instance [Ax.HasR] : InterpretabilityLogic.Entailment.HasAxiomR (Hilbert.Basic Ax) where axiomR! {φ ψ χ} := by constructor; - simpa [HasR.ne_pq, HasR.ne_qr, HasR.ne_rp.symm] using Hilbert.Basic.axm + have h := Hilbert.Basic.axm (φ := InterpretabilityLogic.Axioms.R (.atom (HasR.p Ax)) (.atom (HasR.q Ax)) (.atom (HasR.r Ax))) (s := λ b => if (HasR.p Ax) = b then φ @@ -268,11 +285,12 @@ instance [Ax.HasR] : InterpretabilityLogic.Entailment.HasAxiomR (Hilbert.Basic A else if (HasR.r Ax) = b then χ else (.atom b)) $ HasR.mem_R; + simp [HasR.ne_pq, HasR.ne_qr, HasR.ne_rp.symm] at h; exact h; instance [Ax.HasRstar] : InterpretabilityLogic.Entailment.HasAxiomRstar (Hilbert.Basic Ax) where axiomRstar! {φ ψ χ} := by constructor; - simpa [HasRstar.ne_pq, HasRstar.ne_qr, HasRstar.ne_rp.symm] using Hilbert.Basic.axm + have h := Hilbert.Basic.axm (φ := InterpretabilityLogic.Axioms.Rstar (.atom (HasRstar.p Ax)) (.atom (HasRstar.q Ax)) (.atom (HasRstar.r Ax))) (s := λ b => if (HasRstar.p Ax) = b then φ @@ -280,6 +298,7 @@ instance [Ax.HasRstar] : InterpretabilityLogic.Entailment.HasAxiomRstar (Hilbert else if (HasRstar.r Ax) = b then χ else (.atom b)) $ HasRstar.mem_Rstar; + simp [HasRstar.ne_pq, HasRstar.ne_qr, HasRstar.ne_rp.symm] at h; exact h; end diff --git a/Foundation/InterpretabilityLogic/Hilbert/Minimal/Basic.lean b/Foundation/InterpretabilityLogic/Hilbert/Minimal/Basic.lean index 548bfa9c6..25e2851c0 100644 --- a/Foundation/InterpretabilityLogic/Hilbert/Minimal/Basic.lean +++ b/Foundation/InterpretabilityLogic/Hilbert/Minimal/Basic.lean @@ -69,7 +69,9 @@ instance : Logic.Substitution (Hilbert.Minimal Ax) where subst {φ} s h := by rw [Logic.iff_provable] at h ⊢; induction h with - | @axm _ s' ih => simpa using Minimal.axm (s := s' ∘ s) ih; + | @axm _ s' ih => + have hax := Minimal.axm (s := s' ∘ s) ih; + simp at hax; exact hax; | mdp hφψ hφ ihφψ ihφ => apply Minimal.mdp ihφψ ihφ; | nec hφ ihφ => apply Minimal.nec ihφ; | R1 hφψ ihφψ => apply Minimal.R1 ihφψ; @@ -134,15 +136,16 @@ variable [DecidableEq α] instance [Ax.HasJ1] : InterpretabilityLogic.Entailment.HasAxiomJ1 (Hilbert.Minimal Ax) where axiomJ1! {φ ψ} := by constructor; - simpa [HasJ1.ne_pq] using Hilbert.Minimal.axm + have hax := Hilbert.Minimal.axm (φ := InterpretabilityLogic.Axioms.J1 (.atom (HasJ1.p Ax)) (.atom (HasJ1.q Ax))) (s := λ b => if (HasJ1.p Ax) = b then φ else if (HasJ1.q Ax) = b then ψ else (.atom b)) (HasJ1.mem_J1); + simp [HasJ1.ne_pq] at hax; exact hax; instance [Ax.HasJ2] : InterpretabilityLogic.Entailment.HasAxiomJ2 (Hilbert.Minimal Ax) where axiomJ2! {φ ψ χ} := by constructor; - simpa [HasJ2.ne_pq, HasJ2.ne_qr, HasJ2.ne_rp.symm] using Hilbert.Minimal.axm + have hax := Hilbert.Minimal.axm (φ := InterpretabilityLogic.Axioms.J2 (.atom (HasJ2.p Ax)) (.atom (HasJ2.q Ax)) (.atom (HasJ2.r Ax))) (s := λ b => if (HasJ2.p Ax) = b then φ @@ -150,11 +153,12 @@ instance [Ax.HasJ2] : InterpretabilityLogic.Entailment.HasAxiomJ2 (Hilbert.Minim else if (HasJ2.r Ax) = b then χ else (.atom b)) $ HasJ2.mem_J2; + simp [HasJ2.ne_pq, HasJ2.ne_qr, HasJ2.ne_rp.symm] at hax; exact hax; instance [Ax.HasJ2Plus] : InterpretabilityLogic.Entailment.HasAxiomJ2Plus (Hilbert.Minimal Ax) where axiomJ2Plus! {φ ψ χ} := by constructor; - simpa [HasJ2Plus.ne_pq, HasJ2Plus.ne_qr, HasJ2Plus.ne_rp.symm] using Hilbert.Minimal.axm + have hax := Hilbert.Minimal.axm (φ := InterpretabilityLogic.Axioms.J2Plus (.atom (HasJ2Plus.p Ax)) (.atom (HasJ2Plus.q Ax)) (.atom (HasJ2Plus.r Ax))) (s := λ b => if (HasJ2Plus.p Ax) = b then φ @@ -162,11 +166,12 @@ instance [Ax.HasJ2Plus] : InterpretabilityLogic.Entailment.HasAxiomJ2Plus (Hilbe else if (HasJ2Plus.r Ax) = b then χ else (.atom b)) $ HasJ2Plus.mem_J2Plus; + simp [HasJ2Plus.ne_pq, HasJ2Plus.ne_qr, HasJ2Plus.ne_rp.symm] at hax; exact hax; instance [Ax.HasJ3] : InterpretabilityLogic.Entailment.HasAxiomJ3 (Hilbert.Minimal Ax) where axiomJ3! {φ ψ χ} := by constructor; - simpa [HasJ3.ne_pq, HasJ3.ne_qr, HasJ3.ne_rp.symm] using Hilbert.Minimal.axm + have hax := Hilbert.Minimal.axm (φ := InterpretabilityLogic.Axioms.J3 (.atom (HasJ3.p Ax)) (.atom (HasJ3.q Ax)) (.atom (HasJ3.r Ax))) (s := λ b => if (HasJ3.p Ax) = b then φ @@ -174,19 +179,21 @@ instance [Ax.HasJ3] : InterpretabilityLogic.Entailment.HasAxiomJ3 (Hilbert.Minim else if (HasJ3.r Ax) = b then χ else (.atom b)) $ HasJ3.mem_J3; + simp [HasJ3.ne_pq, HasJ3.ne_qr, HasJ3.ne_rp.symm] at hax; exact hax; instance [Ax.HasJ4] : InterpretabilityLogic.Entailment.HasAxiomJ4 (Hilbert.Minimal Ax) where axiomJ4! {φ ψ} := by constructor; - simpa [HasJ4.ne_pq] using Hilbert.Minimal.axm + have hax := Hilbert.Minimal.axm (φ := InterpretabilityLogic.Axioms.J4 (.atom (HasJ4.p Ax)) (.atom (HasJ4.q Ax))) (s := λ b => if (HasJ4.p Ax) = b then φ else if (HasJ4.q Ax) = b then ψ else (.atom b)) (HasJ4.mem_J4); + simp [HasJ4.ne_pq] at hax; exact hax; instance [Ax.HasJ4Plus] : InterpretabilityLogic.Entailment.HasAxiomJ4Plus (Hilbert.Minimal Ax) where axiomJ4Plus! {φ ψ χ} := by constructor; - simpa [HasJ4Plus.ne_pq, HasJ4Plus.ne_qr, HasJ4Plus.ne_rp.symm] using Hilbert.Minimal.axm + have hax := Hilbert.Minimal.axm (φ := InterpretabilityLogic.Axioms.J4Plus (.atom (HasJ4Plus.p Ax)) (.atom (HasJ4Plus.q Ax)) (.atom (HasJ4Plus.r Ax))) (s := λ b => if (HasJ4Plus.p Ax) = b then φ @@ -194,26 +201,29 @@ instance [Ax.HasJ4Plus] : InterpretabilityLogic.Entailment.HasAxiomJ4Plus (Hilbe else if (HasJ4Plus.r Ax) = b then χ else (.atom b)) $ HasJ4Plus.mem_J4Plus; + simp [HasJ4Plus.ne_pq, HasJ4Plus.ne_qr, HasJ4Plus.ne_rp.symm] at hax; exact hax; instance [Ax.HasJ5] : InterpretabilityLogic.Entailment.HasAxiomJ5 (Hilbert.Minimal Ax) where axiomJ5! {φ} := by constructor; - simpa using Hilbert.Minimal.axm + have hax := Hilbert.Minimal.axm (φ := InterpretabilityLogic.Axioms.J5 (.atom (HasJ5.p Ax))) (s := λ b => if (HasJ5.p Ax) = b then φ else (.atom b)) (HasJ5.mem_J5); + simp at hax; exact hax; instance [Ax.HasJ6] : InterpretabilityLogic.Entailment.HasAxiomJ6 (Hilbert.Minimal Ax) where axiomJ6! {φ} := by constructor; - simpa using Hilbert.Minimal.axm (φ := InterpretabilityLogic.Axioms.J6 (.atom (HasJ6.p Ax))) + have hax := Hilbert.Minimal.axm (φ := InterpretabilityLogic.Axioms.J6 (.atom (HasJ6.p Ax))) (s := λ b => if (HasJ6.p Ax) = b then φ else (.atom b)) (HasJ6.mem_J6); + simp at hax; exact hax; instance [Ax.HasM] : InterpretabilityLogic.Entailment.HasAxiomM (Hilbert.Minimal Ax) where axiomM! {φ ψ χ} := by constructor; - simpa [HasM.ne_pq, HasM.ne_qr, HasM.ne_rp.symm] using Hilbert.Minimal.axm + have hax := Hilbert.Minimal.axm (φ := InterpretabilityLogic.Axioms.M (.atom (HasM.p Ax)) (.atom (HasM.q Ax)) (.atom (HasM.r Ax))) (s := λ b => if (HasM.p Ax) = b then φ @@ -221,6 +231,7 @@ instance [Ax.HasM] : InterpretabilityLogic.Entailment.HasAxiomM (Hilbert.Minimal else if (HasM.r Ax) = b then χ else (.atom b)) $ HasM.mem_M; + simp [HasM.ne_pq, HasM.ne_qr, HasM.ne_rp.symm] at hax; exact hax; end @@ -291,43 +302,43 @@ instance buildAxioms.instHasJ6 : (buildAxioms l).HasJ6 where left; left; left; left; left; left; left; simp; -instance buildAxioms.instHasJ1 (h : l.contains .J1 := by decide) : (buildAxioms l).HasJ1 where +def buildAxioms.instHasJ1 (h : l.contains .J1 := by decide) : (buildAxioms l).HasJ1 where p := 0; q := 1; mem_J1 := by left; left; left; left; left; left; right; simpa using h; -instance buildAxioms.instHasJ2 (h : l.contains .J2 := by decide) : (buildAxioms l).HasJ2 where +def buildAxioms.instHasJ2 (h : l.contains .J2 := by decide) : (buildAxioms l).HasJ2 where p := 0; q := 1; r := 2; mem_J2 := by left; left; left; left; left; right; simpa using h; -instance buildAxioms.instHasJ2Plus (h : l.contains .J2Plus := by decide) : (buildAxioms l).HasJ2Plus where +def buildAxioms.instHasJ2Plus (h : l.contains .J2Plus := by decide) : (buildAxioms l).HasJ2Plus where p := 0; q := 1; r := 2; mem_J2Plus := by left; left; left; left; right; simpa using h; -instance buildAxioms.instHasJ4 (h : l.contains .J4 := by decide) : (buildAxioms l).HasJ4 where +def buildAxioms.instHasJ4 (h : l.contains .J4 := by decide) : (buildAxioms l).HasJ4 where p := 0; q := 1; mem_J4 := by left; left; left; right; simpa using h; -instance buildAxioms.instHasJ4Plus (h : l.contains .J4Plus := by decide) : (buildAxioms l).HasJ4Plus where +def buildAxioms.instHasJ4Plus (h : l.contains .J4Plus := by decide) : (buildAxioms l).HasJ4Plus where p := 0; q := 1; r := 2; mem_J4Plus := by left; left; right; simpa using h; -instance buildAxioms.instHasJ5 (h : l.contains .J5 := by decide) : (buildAxioms l).HasJ5 where +def buildAxioms.instHasJ5 (h : l.contains .J5 := by decide) : (buildAxioms l).HasJ5 where p := 0; mem_J5 := by left; right; simpa using h; -instance buildAxioms.instHasM (h : l.contains .M := by decide) : (buildAxioms l).HasM where +def buildAxioms.instHasM (h : l.contains .M := by decide) : (buildAxioms l).HasM where p := 0; q := 1; r := 2; mem_M := by right; diff --git a/Foundation/InterpretabilityLogic/Logic/Basic.lean b/Foundation/InterpretabilityLogic/Logic/Basic.lean index ee63f624c..484c4596a 100644 --- a/Foundation/InterpretabilityLogic/Logic/Basic.lean +++ b/Foundation/InterpretabilityLogic/Logic/Basic.lean @@ -125,8 +125,8 @@ lemma subset_of_weakerThan [L₁ ⪯ L₂] : L₁ ⊆ L₂ := by suffices L₁ ⊢ φ → L₂ ⊢ φ by grind; exact Entailment.WeakerThan.pbl; -instance [L₁ ≊ L₂] : L₁ ⪯ L₂ := Equiv.le inferInstance -instance [L₁ ≊ L₂] : L₂ ⪯ L₁ := Equiv.le $ .symm inferInstance +instance [L₁ ≊ L₂] : L₁ ⪯ L₂ := Entailment.Equiv.le inferInstance +instance [L₁ ≊ L₂] : L₂ ⪯ L₁ := Entailment.Equiv.le $ .symm inferInstance @[simp, grind .] lemma eq_of_equiv [L₁ ≊ L₂] : L₁ = L₂ := Set.Subset.antisymm subset_of_weakerThan subset_of_weakerThan diff --git a/Foundation/InterpretabilityLogic/Veltman/Hilbert.lean b/Foundation/InterpretabilityLogic/Veltman/Hilbert.lean index af0fed80d..e79dc6446 100644 --- a/Foundation/InterpretabilityLogic/Veltman/Hilbert.lean +++ b/Foundation/InterpretabilityLogic/Veltman/Hilbert.lean @@ -26,7 +26,7 @@ lemma soundness_frameclass (hV : C ⊧* Ax) : Hilbert.Minimal Ax ⊢ φ → C . assumption; | _ => grind; -instance instFrameClassSound (hV : C ⊧* Ax) : Sound (Hilbert.Minimal Ax) C := ⟨fun {_} => soundness_frameclass hV⟩ +def instFrameClassSound (hV : C ⊧* Ax) : Sound (Hilbert.Minimal Ax) C := ⟨fun {_} => soundness_frameclass hV⟩ lemma consistent_of_sound_frameclass (C : Veltman.FrameClass) (C_nonempty: C.Nonempty) @@ -66,7 +66,7 @@ lemma soundness_frameclass (hV : C ⊧* Ax) : Hilbert.Basic Ax ⊢ φ → C ⊧ . assumption; | _ => grind; -instance instFrameClassSound (hV : C ⊧* Ax) : Sound (Hilbert.Basic Ax) C := ⟨fun {_} => soundness_frameclass hV⟩ +def instFrameClassSound (hV : C ⊧* Ax) : Sound (Hilbert.Basic Ax) C := ⟨fun {_} => soundness_frameclass hV⟩ lemma consistent_of_sound_frameclass (C : Veltman.FrameClass) (C_nonempty: C.Nonempty) @@ -92,7 +92,7 @@ lemma soundness_frame [F.IsGL] (hV : F ⊧* Ax) : (Hilbert.Basic Ax) ⊢ φ → assumption; | _ => grind; -instance instFrameSound [F.IsGL] (hV : F ⊧* Ax) : Sound (Hilbert.Basic Ax) F := ⟨fun {_} => +def instFrameSound [F.IsGL] (hV : F ⊧* Ax) : Sound (Hilbert.Basic Ax) F := ⟨fun {_} => soundness_frame hV ⟩ diff --git a/Foundation/LinearLogic/FirstOrder/ClassicalEmbedding.lean b/Foundation/LinearLogic/FirstOrder/ClassicalEmbedding.lean index 0d0f59532..37c518ab3 100644 --- a/Foundation/LinearLogic/FirstOrder/ClassicalEmbedding.lean +++ b/Foundation/LinearLogic/FirstOrder/ClassicalEmbedding.lean @@ -126,7 +126,7 @@ end Derivation namespace Proof theorem forget {φ : Proposition L} : 𝐋𝐋₀ ⊢ φ → 𝐋𝐊¹ ⊢ φ.forget := fun h ↦ - ⟨by simpa using Derivation.forget h.get⟩ + ⟨by simpa using! Derivation.forget h.get⟩ end Proof @@ -447,7 +447,7 @@ namespace Proof variable [L.DecidableEq] theorem girard {φ : Proposition L} : 𝐋𝐊¹ ⊢ φ → 𝐋𝐋₀ ⊢ φ.Girard := fun h ↦ - ⟨by simpa using Derivation.toLL h.get⟩ + ⟨by simpa using! Derivation.toLL h.get⟩ theorem girard_faithful {φ : Proposition L} : 𝐋𝐋₀ ⊢ φ.Girard ↔ 𝐋𝐊¹ ⊢ φ := ⟨fun h ↦ by simpa using LinearLogic.Proof.forget h, girard⟩ diff --git a/Foundation/Logic/Calculus.lean b/Foundation/Logic/Calculus.lean index 2b09c10c4..4528f408c 100644 --- a/Foundation/Logic/Calculus.lean +++ b/Foundation/Logic/Calculus.lean @@ -96,7 +96,7 @@ variable {P : Type*} [Entailment P F] {𝓟 : P} [PrincipalEntailment 𝔇 𝓟] omit [LogicalConnective F] [DeMorgan F] [TildeInvolutive F] [OneSidedLK 𝔇] in lemma provable_iff : 𝓟 ⊢ φ ↔ Nonempty (𝔇 [φ]) := by - simpa using OneSidedLK.PrincipalEntailment.equiv.nonempty_congr + simpa using! OneSidedLK.PrincipalEntailment.equiv.nonempty_congr variable [OneSidedLK.Cut 𝔇] (𝓟) @@ -211,7 +211,7 @@ variable {S : Type*} [Entailment S F] [AdjunctiveSet F S] [ContextualEntailment omit [DeMorgan F] [TildeInvolutive F] [OneSidedLK 𝔇] in lemma provable_iff {𝓢 : S} : 𝓢 ⊢ φ ↔ ∃ Γ : List F, (∀ ψ ∈ Γ, ψ ∈ 𝓢) ∧ Nonempty (𝔇 (φ :: ∼Γ)) := by - simpa using equiv.nonempty_congr + simpa using! equiv.nonempty_congr def toProof (𝓢 : S) (d : 𝔇 [φ]) : 𝓢 ⊢! φ := equiv.symm ⟨⟨[], by simp⟩, d⟩ diff --git a/Foundation/Logic/LindenbaumAlgebra.lean b/Foundation/Logic/LindenbaumAlgebra.lean index d392b03e4..1eb91bdfa 100644 --- a/Foundation/Logic/LindenbaumAlgebra.lean +++ b/Foundation/Logic/LindenbaumAlgebra.lean @@ -51,16 +51,16 @@ instance : Top (LindenbaumAlgebra 𝓢) := ⟨⟦⊤⟧⟩ instance : Bot (LindenbaumAlgebra 𝓢) := ⟨⟦⊥⟧⟩ instance [DecidableEq F] : Min (LindenbaumAlgebra 𝓢) := ⟨Quotient.lift₂ (fun φ ψ ↦ ⟦φ ⋏ ψ⟧) fun φ₁ ψ₁ φ₂ ψ₂ hp hq ↦ by - simpa only [Quotient.eq] using EKK!_of_E!_of_E! hp hq⟩ + simp only [Quotient.eq]; exact EKK!_of_E!_of_E! hp hq⟩ instance [DecidableEq F] : Max (LindenbaumAlgebra 𝓢) := ⟨Quotient.lift₂ (fun φ ψ ↦ ⟦φ ⋎ ψ⟧) fun φ₁ ψ₁ φ₂ ψ₂ hp hq ↦ by - simpa only [Quotient.eq] using EAA!_of_E!_of_E! hp hq⟩ + simp only [Quotient.eq]; exact EAA!_of_E!_of_E! hp hq⟩ instance [DecidableEq F] : HImp (LindenbaumAlgebra 𝓢) := ⟨Quotient.lift₂ (fun φ ψ ↦ ⟦φ 🡒 ψ⟧) fun φ₁ ψ₁ φ₂ ψ₂ hp hq ↦ by - simpa only [Quotient.eq] using ECC!_of_E!_of_E! hp hq⟩ + simp only [Quotient.eq]; exact ECC!_of_E!_of_E! hp hq⟩ instance [DecidableEq F] : Compl (LindenbaumAlgebra 𝓢) := ⟨Quotient.lift (fun φ ↦ ⟦∼φ⟧) fun φ₁ φ₂ hp ↦ by - simpa only [Quotient.eq] using ENN!_of_E! hp⟩ + simp only [Quotient.eq]; exact ENN!_of_E! hp⟩ lemma top_def : (⊤ : LindenbaumAlgebra 𝓢) = ⟦⊤⟧ := rfl diff --git a/Foundation/Logic/LogicSymbol.lean b/Foundation/Logic/LogicSymbol.lean index 118f6acb4..404e3c90a 100644 --- a/Foundation/Logic/LogicSymbol.lean +++ b/Foundation/Logic/LogicSymbol.lean @@ -150,10 +150,10 @@ variable {α β γ} instance : FunLike (α →ˡᶜ β) α β where coe := toTr - coe_injective' := by + coe_injective := by intro f g h; rcases f; rcases g; simpa using h -instance : CoeFun (α →ˡᶜ β) (fun _ => α → β) := DFunLike.hasCoeToFun +instance : CoeFun (α →ˡᶜ β) (fun _ => α → β) := DFunLike.toCoeFun @[ext] lemma ext (f g : α →ˡᶜ β) (h : ∀ x, f x = g x) : f = g := DFunLike.ext f g h diff --git a/Foundation/Modal/Algebra/Basic.lean b/Foundation/Modal/Algebra/Basic.lean index 55a3b01db..0cd9edbc7 100644 --- a/Foundation/Modal/Algebra/Basic.lean +++ b/Foundation/Modal/Algebra/Basic.lean @@ -167,7 +167,8 @@ lemma lindenbaum_val_eq {φ} : (lindenbaum Ax ⊩ φ) = ⟦φ⟧ := by apply Entailment.LindenbaumAlgebra.box_def; lemma lindenbaum_complete_iff {φ : Formula α} : lindenbaum Ax ⊧ φ ↔ (Hilbert.Normal Ax) ⊢ φ := by - grind [lindenbaum_val_eq, Entailment.LindenbaumAlgebra.provable_iff_eq_top]; + rw [def_val, lindenbaum_val_eq]; + exact Entailment.LindenbaumAlgebra.provable_iff_eq_top.symm; instance : Sound (Hilbert.Normal Ax) (lindenbaum Ax) := ⟨lindenbaum_complete_iff.mpr⟩ instance : Complete (Hilbert.Normal Ax) (lindenbaum Ax) := ⟨lindenbaum_complete_iff.mp⟩ diff --git a/Foundation/Modal/Boxdot/Jerabek.lean b/Foundation/Modal/Boxdot/Jerabek.lean index 6923d88d8..7f6e0fc31 100644 --- a/Foundation/Modal/Boxdot/Jerabek.lean +++ b/Foundation/Modal/Boxdot/Jerabek.lean @@ -61,7 +61,7 @@ def Frame.twice.PMorphism (F : Frame) : F×2 →ₚ F where toFun := Prod.fst forth := by rintro ⟨x, _⟩ ⟨y, _⟩ h; - simpa using h; + exact h; back := by intro ⟨x, i⟩ y Rxy; use ⟨y, true⟩; diff --git a/Foundation/Modal/ComplementClosedConsistentFinset.lean b/Foundation/Modal/ComplementClosedConsistentFinset.lean index b6b96096f..12208b8f6 100644 --- a/Foundation/Modal/ComplementClosedConsistentFinset.lean +++ b/Foundation/Modal/ComplementClosedConsistentFinset.lean @@ -317,14 +317,14 @@ lemma iff_mem_imp replace hq := mem_compl_of_not_mem hsub_q hq; induction ψ using Formula.cases_neg with | hfalsum => exact efq!; - | hatom a => exact C_of_N $ Context.by_axm! (by simpa using hq); - | hbox ψ => exact C_of_N $ Context.by_axm! (by simpa using hq); + | hatom a => exact C_of_N $ Context.by_axm! hq; + | hbox ψ => exact C_of_N $ Context.by_axm! hq; | hneg ψ => simp only [Formula.complement.neg_def] at hq; exact CN!_of_! $ Context.by_axm! hq; | himp ψ χ h => simp only [Formula.complement.imp_def₁ h] at hq; - exact C_of_N $ Context.by_axm! (by simpa using hq); + exact C_of_N $ Context.by_axm! hq; . apply membership_iff (by assumption) |>.mpr; exact C!_of_conseq! $ membership_iff (by assumption) |>.mp $ iff_not_mem_compl (by assumption) |>.mpr hr; diff --git a/Foundation/Modal/Entailment/K.lean b/Foundation/Modal/Entailment/K.lean index d89eb9bf6..af7f31c33 100644 --- a/Foundation/Modal/Entailment/K.lean +++ b/Foundation/Modal/Entailment/K.lean @@ -571,8 +571,8 @@ lemma E_boxLe_succ! : 𝓢 ⊢ (□^≤[n + 1] φ) 🡘 (□^≤[n] φ) ⋏ (□ . suffices 𝓢 ⊢ (□^≤[n]φ) ⋏ (Finset.conj {(□^[(n + 1)]φ)}) 🡒 (□^≤[n + 1]φ) by simpa using this; dsimp only [Box.boxLe]; convert CKFconjFconjUnion! (𝓢 := 𝓢) (Γ := Finset.range (n + 1) |>.image (λ i => □^[i] φ)) (Δ := {(□^[(n + 1)]φ)}); - ext ψ; - grind; + rw [show n + 2 = n + 1 + 1 from rfl, Finset.range_add_one, Finset.image_insert, + Finset.insert_eq, Finset.union_comm]; lemma boxLe_regularity! (h : 𝓢 ⊢ φ 🡒 ψ) : 𝓢 ⊢ (□^≤[n] φ) 🡒 (□^≤[n] ψ) := by induction n with diff --git a/Foundation/Modal/Formula/Basic.lean b/Foundation/Modal/Formula/Basic.lean index 1177e2baf..24e84c376 100644 --- a/Foundation/Modal/Formula/Basic.lean +++ b/Foundation/Modal/Formula/Basic.lean @@ -545,7 +545,7 @@ lemma le_max_atoms_of_mem_atoms {a : ℕ} (ha : a ∈ φ.atoms) : a ≤ φ.atoms induction φ with | hfalsum => simp [atoms] at ha; | hatom b => simp [atoms] at ha ⊢; omega; - | hbox φ ihφ => apply ihφ; simpa using ha; + | hbox φ ihφ => apply ihφ; simpa [atoms] using ha; | himp φ ψ ihφ ihψ => rcases (show a ∈ φ.atoms ∨ a ∈ ψ.atoms by simpa [atoms] using ha) with (hφ | hψ); . by_cases hψ : ψ.atoms.Nonempty; diff --git a/Foundation/Modal/Hilbert/Normal/Basic.lean b/Foundation/Modal/Hilbert/Normal/Basic.lean index 22ba29c8e..2f6f99dc5 100644 --- a/Foundation/Modal/Hilbert/Normal/Basic.lean +++ b/Foundation/Modal/Hilbert/Normal/Basic.lean @@ -31,7 +31,8 @@ variable {Ax Ax₁ Ax₂ : Axiom α} @[grind <=] lemma axm' {φ} (h : φ ∈ Ax) : Normal Ax ⊢ φ := by apply Logic.iff_provable.mpr; - simpa using axm (s := .id) h; + have hax := axm (s := .id) h; + simp at hax; exact hax; @[grind <=] lemma axm! {φ} (s : Substitution _) (h : φ ∈ Ax) : Normal Ax ⊢ φ⟦s⟧ := by apply Logic.iff_provable.mpr; @@ -56,7 +57,9 @@ instance : Logic.Substitution (Hilbert.Normal Ax) where subst {φ} s h := by rw [Logic.iff_provable] at h ⊢; induction h with - | @axm _ s' ih => simpa using axm (s := s' ∘ s) ih; + | @axm _ s' ih => + have hax := axm (s := s' ∘ s) ih; + simp at hax; exact hax; | mdp hφψ hφ ihφψ ihφ => apply mdp ihφψ ihφ; | nec hφ ihφ => apply nec ihφ; | implyK φ ψ => apply implyK; @@ -112,192 +115,216 @@ variable [DecidableEq α] instance [Ax.HasK] : Entailment.HasAxiomK (Hilbert.Normal Ax) where K φ ψ := by constructor; - simpa [HasK.ne_pq] using Hilbert.Normal.axm + have hax := Hilbert.Normal.axm (φ := Axioms.K (.atom (HasK.p Ax)) (.atom (HasK.q Ax))) (s := λ b => if (HasK.p Ax) = b then φ else if (HasK.q Ax) = b then ψ else (.atom b)) (HasK.mem_K); + simp [HasK.ne_pq] at hax; exact hax; instance [Ax.HasK] : Logic.IsNormal (Hilbert.Normal Ax) where instance [Ax.HasT] : Entailment.HasAxiomT (Hilbert.Normal Ax) where T φ := by constructor; - simpa using Hilbert.Normal.axm + have hax := Hilbert.Normal.axm (φ := Axioms.T (.atom (HasT.p Ax))) (s := λ b => if (HasT.p Ax) = b then φ else (.atom b)) (HasT.mem_T); + simp at hax; exact hax; instance [Ax.HasD] : Entailment.HasAxiomD (Hilbert.Normal Ax) where D φ := by constructor; - simpa using Hilbert.Normal.axm + have hax := Hilbert.Normal.axm (φ := Axioms.D (.atom (HasD.p Ax))) (s := λ b => if (HasD.p Ax) = b then φ else (.atom b)) HasD.mem_D; + simp at hax; exact hax; instance [Ax.HasP] : Entailment.HasAxiomP (Hilbert.Normal Ax) where P := by constructor; - simpa using Hilbert.Normal.axm (s := .id) HasP.mem_P + have hax := Hilbert.Normal.axm (s := .id) (show _ ∈ Ax from HasP.mem_P) + simp at hax; exact hax; instance [Ax.HasB] : Entailment.HasAxiomB (Hilbert.Normal Ax) where B φ := by constructor; - simpa using Hilbert.Normal.axm + have hax := Hilbert.Normal.axm (φ := Axioms.B (.atom (HasB.p Ax))) (s := λ b => if (HasB.p Ax) = b then φ else (.atom b)) (HasB.mem_B); + simp at hax; exact hax; instance [Ax.HasFour] : Entailment.HasAxiomFour (Hilbert.Normal Ax) where Four φ := by constructor; - simpa using Hilbert.Normal.axm + have hax := Hilbert.Normal.axm (φ := Axioms.Four (.atom (HasFour.p Ax))) (s := λ b => if (HasFour.p Ax) = b then φ else (.atom b)) (HasFour.mem_Four); + simp at hax; exact hax; instance [Ax.HasFourN n] : Entailment.HasAxiomFourN n (Hilbert.Normal Ax) where FourN φ := by constructor; - simpa [Axioms.FourN] using Hilbert.Normal.axm + have hax := Hilbert.Normal.axm (φ := Axioms.FourN n (.atom (HasFourN.p n Ax))) (s := λ b => if (HasFourN.p n Ax) = b then φ else (.atom b)) (HasFourN.mem_FourN); + simp [Axioms.FourN] at hax ⊢; exact hax; instance [Ax.HasFive] : Entailment.HasAxiomFive (Hilbert.Normal Ax) where Five φ := by constructor; - simpa using Hilbert.Normal.axm + have hax := Hilbert.Normal.axm (φ := Axioms.Five (.atom (HasFive.p Ax))) (s := λ b => if (HasFive.p Ax) = b then φ else (.atom b)) (HasFive.mem_Five); + simp at hax; exact hax; instance [Ax.HasL] : Entailment.HasAxiomL (Hilbert.Normal Ax) where L φ := by constructor; - simpa using Hilbert.Normal.axm + have hax := Hilbert.Normal.axm (φ := Axioms.L (.atom (HasL.p Ax))) (s := λ b => if (HasL.p Ax) = b then φ else (.atom b)) (HasL.mem_L); + simp at hax; exact hax; instance [Ax.HasZ] : Entailment.HasAxiomZ (Hilbert.Normal Ax) where Z φ := by constructor; - simpa using Hilbert.Normal.axm + have hax := Hilbert.Normal.axm (φ := Axioms.Z (.atom (HasZ.p Ax))) (s := λ b => if (HasZ.p Ax) = b then φ else (.atom b)) (HasZ.mem_Z); + simp at hax; exact hax; instance [Ax.HasHen] : Entailment.HasAxiomHen (Hilbert.Normal Ax) where Hen φ := by constructor; - simpa using Hilbert.Normal.axm + have hax := Hilbert.Normal.axm (φ := Axioms.Hen (.atom (HasHen.p Ax))) (s := λ b => if (HasHen.p Ax) = b then φ else (.atom b)) (HasHen.mem_Hen); + simp at hax; exact hax; instance [Ax.HasPoint2] : Entailment.HasAxiomPoint2 (Hilbert.Normal Ax) where Point2 φ := by constructor; - simpa using Hilbert.Normal.axm + have hax := Hilbert.Normal.axm (φ := Axioms.Point2 (.atom (HasPoint2.p Ax))) (s := λ b => if (HasPoint2.p Ax) = b then φ else (.atom b)) (HasPoint2.mem_Point2); + simp at hax; exact hax; instance [Ax.HasWeakPoint2] : Entailment.HasAxiomWeakPoint2 (Hilbert.Normal Ax) where WeakPoint2 φ ψ := by constructor; - simpa [HasWeakPoint2.ne_pq] using Hilbert.Normal.axm + have hax := Hilbert.Normal.axm (φ := Axioms.WeakPoint2 (.atom (HasWeakPoint2.p Ax)) (.atom (HasWeakPoint2.q Ax))) (s := λ b => if (HasWeakPoint2.p Ax) = b then φ else if (HasWeakPoint2.q Ax) = b then ψ else (.atom b)) (HasWeakPoint2.mem_WeakPoint2); + simp [HasWeakPoint2.ne_pq] at hax; exact hax; instance [Ax.HasPoint3] : Entailment.HasAxiomPoint3 (Hilbert.Normal Ax) where Point3 φ ψ := by constructor; - simpa [HasPoint3.ne_pq] using Hilbert.Normal.axm + have hax := Hilbert.Normal.axm (φ := Axioms.Point3 (.atom (HasPoint3.p Ax)) (.atom (HasPoint3.q Ax))) (s := λ b => if (HasPoint3.p Ax) = b then φ else if (HasPoint3.q Ax) = b then ψ else (.atom b)) (HasPoint3.mem_Point3); + simp [HasPoint3.ne_pq] at hax; exact hax; instance [Ax.HasWeakPoint3] : Entailment.HasAxiomWeakPoint3 (Hilbert.Normal Ax) where WeakPoint3 φ ψ := by constructor; - simpa [HasWeakPoint3.ne_pq] using Hilbert.Normal.axm + have hax := Hilbert.Normal.axm (φ := Axioms.WeakPoint3 (.atom (HasWeakPoint3.p Ax)) (.atom (HasWeakPoint3.q Ax))) (s := λ b => if (HasWeakPoint3.p Ax) = b then φ else if (HasWeakPoint3.q Ax) = b then ψ else (.atom b)) (HasWeakPoint3.mem_WeakPoint3); + simp [HasWeakPoint3.ne_pq] at hax; exact hax; instance [Ax.HasPoint4] : Entailment.HasAxiomPoint4 (Hilbert.Normal Ax) where Point4 φ := by constructor; - simpa using Hilbert.Normal.axm + have hax := Hilbert.Normal.axm (φ := Axioms.Point4 (.atom (HasPoint4.p Ax))) (s := λ b => if (HasPoint4.p Ax) = b then φ else (.atom b)) (HasPoint4.mem_Point4); + simp at hax; exact hax; instance [Ax.HasGrz] : Entailment.HasAxiomGrz (Hilbert.Normal Ax) where Grz φ := by constructor; - simpa using Hilbert.Normal.axm + have hax := Hilbert.Normal.axm (φ := Axioms.Grz (.atom (HasGrz.p Ax))) (s := λ b => if (HasGrz.p Ax) = b then φ else (.atom b)) (HasGrz.mem_Grz); + simp at hax; exact hax; instance [Ax.HasDum] : Entailment.HasAxiomDum (Hilbert.Normal Ax) where Dum φ := by constructor; - simpa using Hilbert.Normal.axm + have hax := Hilbert.Normal.axm (φ := Axioms.Dum (.atom (HasDum.p Ax))) (s := λ b => if (HasDum.p Ax) = b then φ else (.atom b)) (HasDum.mem_Dum); + simp at hax; exact hax; instance [Ax.HasTc] : Entailment.HasAxiomTc (Hilbert.Normal Ax) where Tc φ := by constructor; - simpa using Hilbert.Normal.axm + have hax := Hilbert.Normal.axm (φ := Axioms.Tc (.atom (HasTc.p Ax))) (s := λ b => if (HasTc.p Ax) = b then φ else (.atom b)) (HasTc.mem_Tc); + simp at hax; exact hax; instance [Ax.HasVer] : Entailment.HasAxiomVer (Hilbert.Normal Ax) where Ver φ := by constructor; - simpa using Hilbert.Normal.axm + have hax := Hilbert.Normal.axm (φ := Axioms.Ver (.atom (HasVer.p Ax))) (s := λ b => if (HasVer.p Ax) = b then φ else (.atom b)) (HasVer.mem_Ver); + simp at hax; exact hax; instance [Ax.HasMcK] : Entailment.HasAxiomMcK (Hilbert.Normal Ax) where McK φ := by constructor; - simpa using Hilbert.Normal.axm + have hax := Hilbert.Normal.axm (φ := Axioms.McK (.atom (HasMcK.p Ax))) (s := λ b => if (HasMcK.p Ax) = b then φ else (.atom b)) (HasMcK.mem_McK); + simp at hax; exact hax; instance [Ax.HasMk] : Entailment.HasAxiomMk (Hilbert.Normal Ax) where Mk φ ψ := by constructor; - simpa [HasMk.ne_pq] using Hilbert.Normal.axm + have hax := Hilbert.Normal.axm (φ := Axioms.Mk (.atom (HasMk.p Ax)) (.atom (HasMk.q Ax))) (s := λ b => if (HasMk.p Ax) = b then φ else if (HasMk.q Ax) = b then ψ else (.atom b)) (HasMk.mem_Mk); + simp [HasMk.ne_pq] at hax; exact hax; instance [Ax.HasH1] : Entailment.HasAxiomH (Hilbert.Normal Ax) where H1 φ := by constructor; - simpa using Hilbert.Normal.axm + have hax := Hilbert.Normal.axm (φ := Axioms.H (.atom (HasH1.p Ax))) (s := λ b => if (HasH1.p Ax) = b then φ else (.atom b)) (HasH1.mem_H1); + simp at hax; exact hax; instance [Ax.HasGeach g] : Entailment.HasAxiomGeach g (Hilbert.Normal Ax) where Geach φ := by constructor; - simpa using Hilbert.Normal.axm + have hax := Hilbert.Normal.axm (φ := Axioms.Geach g (.atom (HasGeach.p g Ax))) (s := λ b => if (HasGeach.p g Ax) = b then φ else (.atom b)) (HasGeach.mem_Geach); + simp at hax; exact hax; end diff --git a/Foundation/Modal/Hilbert/WithHenkin/Basic.lean b/Foundation/Modal/Hilbert/WithHenkin/Basic.lean index d58f59e9d..c652c2eea 100644 --- a/Foundation/Modal/Hilbert/WithHenkin/Basic.lean +++ b/Foundation/Modal/Hilbert/WithHenkin/Basic.lean @@ -50,7 +50,10 @@ instance : Logic.Substitution (Hilbert.WithHenkin Ax) where subst {φ} s h := by rw [Logic.iff_provable] at h ⊢; induction h with - | @axm _ s' ih => simpa using axm (s := s' ∘ s) ih; + | @axm _ s' ih => + have h := axm (s := s' ∘ s) ih + rw [Formula.subst.def_comp] at h + exact h | mdp hφψ hφ ihφψ ihφ => apply mdp ihφψ ihφ; | nec hφ ihφ => apply nec ihφ; | henkin hφψ ihφψ => apply henkin ihφψ; @@ -109,18 +112,22 @@ variable [DecidableEq α] instance instHasAxiomK [Ax.HasK] : Entailment.HasAxiomK (Hilbert.WithHenkin Ax) where K φ ψ := by constructor; - simpa [HasK.ne_pq] using Hilbert.WithHenkin.axm + have h := Hilbert.WithHenkin.axm (φ := Axioms.K (.atom (HasK.p Ax)) (.atom (HasK.q Ax))) (s := λ b => if (HasK.p Ax) = b then φ else if (HasK.q Ax) = b then ψ else (.atom b)) - (by exact HasK.mem_K); + (show _ ∈ Ax from HasK.mem_K); + simp [HasK.ne_pq] at h; + exact h; instance instHasAxiomFour [Ax.HasFour] : Entailment.HasAxiomFour (Hilbert.WithHenkin Ax) where Four φ := by constructor; - simpa using Hilbert.WithHenkin.axm + have h := Hilbert.WithHenkin.axm (φ := Axioms.Four (.atom (HasFour.p Ax))) (s := λ b => if (HasFour.p Ax) = b then φ else (.atom b)) - (by exact HasFour.mem_Four); + (show _ ∈ Ax from HasFour.mem_Four); + simp at h; + exact h; end diff --git a/Foundation/Modal/Hilbert/WithLoeb/Basic.lean b/Foundation/Modal/Hilbert/WithLoeb/Basic.lean index a903e8c20..5ffb29356 100644 --- a/Foundation/Modal/Hilbert/WithLoeb/Basic.lean +++ b/Foundation/Modal/Hilbert/WithLoeb/Basic.lean @@ -50,7 +50,10 @@ instance : Logic.Substitution (Hilbert.WithLoeb Ax) where subst {φ} s h := by rw [Logic.iff_provable] at h ⊢; induction h with - | @axm _ s' ih => simpa using axm (s := s' ∘ s) ih; + | @axm _ s' ih => + have h := axm (s := s' ∘ s) ih + rw [Formula.subst.def_comp] at h + exact h | mdp hφψ hφ ihφψ ihφ => apply mdp ihφψ ihφ; | nec hφ ihφ => apply nec ihφ; | loeb hφψ ihφψ => apply loeb ihφψ; @@ -109,18 +112,22 @@ variable [DecidableEq α] instance instHasAxiomK [Ax.HasK] : Entailment.HasAxiomK (Hilbert.WithLoeb Ax) where K φ ψ := by constructor; - simpa [HasK.ne_pq] using Hilbert.WithLoeb.axm + have h := Hilbert.WithLoeb.axm (φ := Axioms.K (.atom (HasK.p Ax)) (.atom (HasK.q Ax))) (s := λ b => if (HasK.p Ax) = b then φ else if (HasK.q Ax) = b then ψ else (.atom b)) - (by exact HasK.mem_K); + (show _ ∈ Ax from HasK.mem_K); + simp [HasK.ne_pq] at h; + exact h; instance instHasAxiomFour [Ax.HasFour] : Entailment.HasAxiomFour (Hilbert.WithLoeb Ax) where Four φ := by constructor; - simpa using Hilbert.WithLoeb.axm + have h := Hilbert.WithLoeb.axm (φ := Axioms.Four (.atom (HasFour.p Ax))) (s := λ b => if (HasFour.p Ax) = b then φ else (.atom b)) - (by exact HasFour.mem_Four); + (show _ ∈ Ax from HasFour.mem_Four); + simp at h; + exact h; end diff --git a/Foundation/Modal/Hilbert/WithRE/Basic.lean b/Foundation/Modal/Hilbert/WithRE/Basic.lean index 84b35d5ea..a43e7d7ee 100644 --- a/Foundation/Modal/Hilbert/WithRE/Basic.lean +++ b/Foundation/Modal/Hilbert/WithRE/Basic.lean @@ -49,7 +49,7 @@ instance : Logic.Substitution (Hilbert.WithRE Ax) where subst {φ} s h := by rw [Logic.iff_provable] at h ⊢; induction h with - | @axm _ s' ih => simpa using axm (s := s' ∘ s) ih; + | @axm _ s' ih => show WithRE Ax _; simpa using axm (s := s' ∘ s) ih; | mdp hφψ hφ ihφψ ihφ => apply mdp ihφψ ihφ; | re hφψ ihφψ => apply re; assumption; | implyK φ ψ => apply implyK; @@ -106,18 +106,20 @@ variable [DecidableEq α] instance instHasAxiomM [Ax.HasM] : Entailment.HasAxiomM (Hilbert.WithRE Ax) where M φ ψ := by constructor; - simpa [HasM.ne_pq] using Hilbert.WithRE.axm + have h := Hilbert.WithRE.axm (φ := Axioms.M (.atom (HasM.p Ax)) (.atom (HasM.q Ax))) (s := λ b => if (HasM.p Ax) = b then φ else if (HasM.q Ax) = b then ψ else (.atom b)) - (by exact HasM.mem_m); + (show _ ∈ Ax from HasM.mem_m); + simp [HasM.ne_pq] at h; exact h; instance instHasAxiomC [Ax.HasC] : Entailment.HasAxiomC (Hilbert.WithRE Ax) where C φ ψ := by constructor; - simpa [HasC.ne_pq] using Hilbert.WithRE.axm + have h := Hilbert.WithRE.axm (φ := Axioms.C (.atom (HasC.p Ax)) (.atom (HasC.q Ax))) (s := λ b => if (HasC.p Ax) = b then φ else if (HasC.q Ax) = b then ψ else (.atom b)) - (by exact HasC.mem_c); + (show _ ∈ Ax from HasC.mem_c); + simp [HasC.ne_pq] at h; exact h; instance instHasAxiomN [Ax.HasN] : Entailment.HasAxiomN (Hilbert.WithRE Ax) where N := by constructor; apply Hilbert.WithRE.axm (φ := Axioms.N) (s := .id) (by exact HasN.mem_n); @@ -125,53 +127,62 @@ instance instHasAxiomN [Ax.HasN] : Entailment.HasAxiomN (Hilbert.WithRE Ax) wher instance instHasAxiomK [Ax.HasK] : Entailment.HasAxiomK (Hilbert.WithRE Ax) where K φ ψ := by constructor; - simpa [HasK.ne_pq] using Hilbert.WithRE.axm + have h := Hilbert.WithRE.axm (φ := Axioms.K (.atom (HasK.p Ax)) (.atom (HasK.q Ax))) (s := λ b => if (HasK.p Ax) = b then φ else if (HasK.q Ax) = b then ψ else (.atom b)) - (by exact HasK.mem_K); + (show _ ∈ Ax from HasK.mem_K); + simp [HasK.ne_pq] at h; exact h; instance instHasAxiomT [Ax.HasT] : Entailment.HasAxiomT (Hilbert.WithRE Ax) where T φ := by constructor; - simpa using Hilbert.WithRE.axm + have h := Hilbert.WithRE.axm (φ := Axioms.T (.atom (HasT.p Ax))) (s := λ b => if (HasT.p Ax) = b then φ else (.atom b)) - (by exact HasT.mem_T); + (show _ ∈ Ax from HasT.mem_T); + simp at h; exact h; instance instHasAxiomD [Ax.HasD] : Entailment.HasAxiomD (Hilbert.WithRE Ax) where D φ := by constructor; - simpa using Hilbert.WithRE.axm + have h := Hilbert.WithRE.axm (φ := Axioms.D (.atom (HasD.p Ax))) (s := λ b => if (HasD.p Ax) = b then φ else (.atom b)) - (by exact HasD.mem_D); + (show _ ∈ Ax from HasD.mem_D); + simp at h; exact h; instance instHasAxiomP [Ax.HasP] : Entailment.HasAxiomP (Hilbert.WithRE Ax) where - P := by constructor; simpa using Hilbert.WithRE.axm (φ := Axioms.P) (s := .id) (by exact HasP.mem_P); + P := by + constructor + have h := Hilbert.WithRE.axm (φ := Axioms.P) (s := .id) (show _ ∈ Ax from HasP.mem_P); + simp at h; exact h; instance instHasAxiomFour [Ax.HasFour] : Entailment.HasAxiomFour (Hilbert.WithRE Ax) where Four φ := by constructor; - simpa using Hilbert.WithRE.axm + have h := Hilbert.WithRE.axm (φ := Axioms.Four (.atom (HasFour.p Ax))) (s := λ b => if (HasFour.p Ax) = b then φ else (.atom b)) - (by exact HasFour.mem_Four); + (show _ ∈ Ax from HasFour.mem_Four); + simp at h; exact h; instance [Ax.HasB] : Entailment.HasAxiomB (Hilbert.WithRE Ax) where B φ := by constructor; - simpa using Hilbert.WithRE.axm + have h := Hilbert.WithRE.axm (φ := Axioms.B (.atom (HasB.p Ax))) (s := λ b => if (HasB.p Ax) = b then φ else (.atom b)) - (by exact HasB.mem_B); + (show _ ∈ Ax from HasB.mem_B); + simp at h; exact h; instance [Ax.HasFive] : Entailment.HasAxiomFive (Hilbert.WithRE Ax) where Five φ := by constructor; - simpa using Hilbert.WithRE.axm + have h := Hilbert.WithRE.axm (φ := Axioms.Five (.atom (HasFive.p Ax))) (s := λ b => if (HasFive.p Ax) = b then φ else (.atom b)) - (by exact HasFive.mem_Five); + (show _ ∈ Ax from HasFive.mem_Five); + simp at h; exact h; end diff --git a/Foundation/Modal/Kripke/Algebra.lean b/Foundation/Modal/Kripke/Algebra.lean index 804cd9735..a2538dd2b 100644 --- a/Foundation/Modal/Kripke/Algebra.lean +++ b/Foundation/Modal/Kripke/Algebra.lean @@ -48,7 +48,7 @@ lemma algebraic_satisfies (F : Kripke.Frame) (V : ℕ → F⁺) (x : F.World) : induction φ generalizing x with | hatom a => simp [Satisfies, Formula.value]; tauto; | hfalsum => simp [Satisfies]; - | himp φ ψ ihφ ihψ => simp [Satisfies, ihφ x, ihψ x]; tauto; + | himp φ ψ ihφ ihψ => simp [Satisfies, ihφ x, ihψ x]; | hbox φ ihφ => simp [Satisfies, ihφ, Frame.mem_def_box]; lemma algebraic_validOnFrame_imp : F ⊧ φ 🡒 ψ ↔ (∀ V : ℕ → F⁺, (V ⊩ φ) ≤ (V ⊩ ψ)) := by diff --git a/Foundation/Modal/Kripke/AxiomGeach.lean b/Foundation/Modal/Kripke/AxiomGeach.lean index a6bfe5981..aab1055a1 100644 --- a/Foundation/Modal/Kripke/AxiomGeach.lean +++ b/Foundation/Modal/Kripke/AxiomGeach.lean @@ -32,7 +32,9 @@ lemma serial [F.IsSerial] : ∀ x : F, ∃ y, x ≺ y := IsSerial.serial @[simp] instance [F.IsGeachConvergent ⟨0, 0, 1, 1⟩] : F.IsSerial where - serial := by simpa using IsGeachConvergent.gconv (F := F) (g := ⟨0, 0, 1, 1⟩); + serial := by + have h := IsGeachConvergent.gconv (F := F) (g := ⟨0, 0, 1, 1⟩); + simp at h; exact h; instance [F.IsSerial] : F.IsGeachConvergent ⟨0, 0, 1, 1⟩ where gconv x y z Rxy Rxz := by simp_all only [Rel.Iterate.iff_zero, Rel.Iterate.iff_succ, exists_eq_right, and_self]; @@ -95,7 +97,9 @@ lemma ps_convergent [F.IsPiecewiseStronglyConvergent] : ∀ {x y z : F.World}, x @[simp] instance [F.IsGeachConvergent ⟨1, 1, 1, 1⟩] : F.IsPiecewiseStronglyConvergent where - ps_convergent := by simpa using IsGeachConvergent.gconv (g := ⟨1, 1, 1, 1⟩) (F := F); + ps_convergent := by + have h := IsGeachConvergent.gconv (g := ⟨1, 1, 1, 1⟩) (F := F); + simp at h; exact h; instance [F.IsPiecewiseStronglyConvergent] : F.IsGeachConvergent ⟨1, 1, 1, 1⟩ where gconv x y z Rxy Rxz := by simp_all only [Rel.Iterate.iff_succ, Rel.Iterate.iff_zero, exists_eq_right]; diff --git a/Foundation/Modal/Kripke/AxiomGrz.lean b/Foundation/Modal/Kripke/AxiomGrz.lean index 2b8f5003d..476750303 100644 --- a/Foundation/Modal/Kripke/AxiomGrz.lean +++ b/Foundation/Modal/Kripke/AxiomGrz.lean @@ -42,7 +42,8 @@ lemma validate_AxiomGrz_of_refl_trans_wcwf [F.IsReflexive] [F.IsTransitive] [F.I have := Set.not_nonempty_iff_eq_empty.mpr this; have := Set.nonempty_def.not.mp this; push Not at this; - simpa [X] using this; + simp only [X, Set.mem_setOf_eq, not_and, not_not] at this; + exact this; rintro w (⟨hw₁, hw₂⟩ | ⟨hw₁, hw₂, hw₃⟩); . have : Satisfies M w (□((.atom 0) 🡒 □(.atom 0)) 🡒 (.atom 0)) := hw₁ w (Std.Refl.refl w); diff --git a/Foundation/Modal/Kripke/AxiomL.lean b/Foundation/Modal/Kripke/AxiomL.lean index 4d5c5fdd5..ed45cfcea 100644 --- a/Foundation/Modal/Kripke/AxiomL.lean +++ b/Foundation/Modal/Kripke/AxiomL.lean @@ -29,7 +29,8 @@ lemma validate_AxiomL_of_trans_cwf [F.IsTransitive] [F.IsConverseWellFounded] : obtain ⟨m, ⟨⟨Rwm, hm⟩, hm₂⟩⟩ := F.cwf.has_min ({ x | w ≺ x ∧ ¬(Satisfies ⟨F, V⟩ x φ) }) $ by use x; tauto; - replace hm₂ : ∀ x, w ≺ x → ¬Satisfies ⟨F, V⟩ x φ → ¬m ≺ x := by simpa using hm₂; + replace hm₂ : ∀ x, w ≺ x → ¬Satisfies ⟨F, V⟩ x φ → ¬m ≺ x := by + intro x hwx hns; exact hm₂ x ⟨hwx, hns⟩; apply Satisfies.not_box_def.mpr; use m; constructor; diff --git a/Foundation/Modal/Kripke/AxiomMk.lean b/Foundation/Modal/Kripke/AxiomMk.lean index a8acd71cd..9e3919216 100644 --- a/Foundation/Modal/Kripke/AxiomMk.lean +++ b/Foundation/Modal/Kripke/AxiomMk.lean @@ -35,7 +35,7 @@ lemma validate_axiomMk_of_satisfiesMakinsonCondition [F.SatisfiesMakinsonConditi . assumption; . apply Satisfies.and_def.mpr; constructor; - . suffices Satisfies ⟨F, V⟩ y (□^[2](.atom 0)) by simpa using this; + . suffices Satisfies ⟨F, V⟩ y (□^[2](.atom 0)) by exact this; apply Satisfies.boxItr_def.mpr intro z Ryz; apply hx₁; diff --git a/Foundation/Modal/Kripke/AxiomPoint3.lean b/Foundation/Modal/Kripke/AxiomPoint3.lean index 2742fc9a5..6c007c078 100644 --- a/Foundation/Modal/Kripke/AxiomPoint3.lean +++ b/Foundation/Modal/Kripke/AxiomPoint3.lean @@ -91,7 +91,7 @@ instance [Entailment.HasAxiomPoint3 𝓢] : (canonicalFrame 𝓢).IsPiecewiseStr . exact Rxy; . apply iff_mem₂_imp.mpr; constructor; - . simpa using hφy; + . exact hφy; . exact iff_not_mem₁_mem₂.mp hψy; . apply iff_mem₂_box.mpr; use z; @@ -99,7 +99,7 @@ instance [Entailment.HasAxiomPoint3 𝓢] : (canonicalFrame 𝓢).IsPiecewiseStr . exact Rxz; . apply iff_mem₂_imp.mpr; constructor; - . simpa using hψz; + . exact hψz; . exact iff_not_mem₁_mem₂.mp hφz; end canonicality diff --git a/Foundation/Modal/Kripke/AxiomWeakPoint3.lean b/Foundation/Modal/Kripke/AxiomWeakPoint3.lean index 654dcab11..60ef25149 100644 --- a/Foundation/Modal/Kripke/AxiomWeakPoint3.lean +++ b/Foundation/Modal/Kripke/AxiomWeakPoint3.lean @@ -87,13 +87,13 @@ instance [Entailment.HasAxiomWeakPoint3 𝓢] : (canonicalFrame 𝓢).IsPiecewis rcases hC with ⟨nRyz, neyz, nRzy⟩; obtain ⟨φ₁, hφ₁y, hφ₁z⟩ := Set.not_subset.mp nRyz; - replace hφ₁y : □φ₁ ∈ y.1.1 := by simpa using hφ₁y; + replace hφ₁y : □φ₁ ∈ y.1.1 := hφ₁y; replace hφ₁z : φ₁ ∈ z.1.2 := iff_not_mem₁_mem₂.mp hφ₁z; obtain ⟨φ₂, hφ₂y, hφ₂z⟩ := exists₁₂_of_ne neyz; let φ := φ₁ ⋎ φ₂; obtain ⟨ψ₁, hψz, hψy⟩ := Set.not_subset.mp nRzy; - replace hψ₁z : □ψ₁ ∈ z.1.1 := by simpa using hψz; + replace hψ₁z : □ψ₁ ∈ z.1.1 := hψz; replace hψ₁y : ψ₁ ∈ y.1.2 := iff_not_mem₁_mem₂.mp hψy; obtain ⟨ψ₂, hψ₂z, hψ₂y⟩ := exists₂₁_of_ne neyz; let ψ := ψ₁ ⋎ ψ₂; diff --git a/Foundation/Modal/Kripke/ComplexityLimited.lean b/Foundation/Modal/Kripke/ComplexityLimited.lean index 350e05ce5..82eb66a00 100644 --- a/Foundation/Modal/Kripke/ComplexityLimited.lean +++ b/Foundation/Modal/Kripke/ComplexityLimited.lean @@ -33,7 +33,7 @@ lemma iff_satisfy_complexityLimitedModel_aux obtain ⟨n, hn, hx⟩ := hx; simp [Formula.complexity] at hn; have : n + 1 ≤ φ.complexity - ψ.complexity := by - have : ψ.complexity + 1 ≤ φ.complexity := by simpa using subformulas.complexity_lower hq; + have : ψ.complexity + 1 ≤ φ.complexity := subformulas.complexity_lower hq; omega; constructor; . rintro h ⟨y, hy⟩ Rxy; diff --git a/Foundation/Modal/Kripke/ExtendRoot.lean b/Foundation/Modal/Kripke/ExtendRoot.lean index 3d05b9078..ac5a0bca6 100644 --- a/Foundation/Modal/Kripke/ExtendRoot.lean +++ b/Foundation/Modal/Kripke/ExtendRoot.lean @@ -81,7 +81,8 @@ lemma embed_rel_iterate_embed_iff_rel {i j : F} : embed (n := n) i ≺^[k] embed extendRoot.pMorphism.toFun_rel_iterate_toFun_iff_of_inj Sum.inr_injective @[simp] -lemma rel_root_original_root [F.IsRooted] : (F.extendRoot n).root.1 ≺ F.root.1 := by grind; +lemma rel_root_original_root [F.IsRooted] : (F.extendRoot n).root.1 ≺ F.root.1 := by + simp only [Frame.root, default, Frame.Rel']; @[grind →] lemma not_eq_extendRoot_root_of_rel_original_root [F.IsIrreflexive] (x : F.extendRoot n) (h : (extendRoot F n).root ≺ x) : x ≠ (extendRoot F n).root := by @@ -99,7 +100,7 @@ section lemma eq_root_or_eq_original (x : F.extendRoot 1) : x = (F.extendRoot 1).root ∨ ∃ x₀ : F, x = x₀ := by rcases eq_extend_or_eq_original x with (⟨i, hi, rfl⟩ | ⟨x₀, rfl⟩); - . simp [Frame.root, default]; grind; + . left; simp [Frame.root, default, extend]; . simp; lemma eq_original_of_rel_extendRoot_root₁ [F.IsIrreflexive] (x : F.extendRoot 1) (h : (extendRoot F 1).root ≺ x) @@ -307,7 +308,9 @@ lemma inr_satisfies_forall_axiomT_set {Γ : Finset (Modal.Formula ℕ)} : ∃ i : Fin n, ∀ γ ∈ Γ, Satisfies _ (extend i : M.extendRoot n) (□γ 🡒 γ) := by obtain ⟨i, hi⟩ := inr_satisfies_conj_axiomT_set (Γ := Γ) (M := M); use i; - simpa using Satisfies.fconj_def.mp hi; + have h := Satisfies.fconj_def.mp hi; + simp only [Finset.forall_mem_image] at h; + exact h; end Model.extendRoot diff --git a/Foundation/Modal/Kripke/Hilbert.lean b/Foundation/Modal/Kripke/Hilbert.lean index b1f967dca..60be88365 100644 --- a/Foundation/Modal/Kripke/Hilbert.lean +++ b/Foundation/Modal/Kripke/Hilbert.lean @@ -30,7 +30,7 @@ lemma soundness_of_validates_axioms (hV : C ⊧* Ax) : Hilbert.Normal Ax ⊢ φ | implyS => exact ValidOnFrame.implyS; | ec => exact ValidOnFrame.elimContra; -instance instSound_of_validates_axioms (hV : C ⊧* Ax) : Sound (Hilbert.Normal Ax) C := ⟨fun {_} => +def instSound_of_validates_axioms (hV : C ⊧* Ax) : Sound (Hilbert.Normal Ax) C := ⟨fun {_} => soundness_of_validates_axioms hV ⟩ @@ -61,7 +61,7 @@ lemma soundness_of_frame_validates_axioms (hV : F ⊧* Ax) : (Hilbert.Normal Ax) | implyS => exact ValidOnFrame.implyS; | ec => exact ValidOnFrame.elimContra; -instance instSound_of_frame_validates_axioms (hV : F ⊧* Ax) : Sound (Hilbert.Normal Ax) F := ⟨fun {_} => +def instSound_of_frame_validates_axioms (hV : F ⊧* Ax) : Sound (Hilbert.Normal Ax) F := ⟨fun {_} => soundness_of_frame_validates_axioms hV ⟩ diff --git a/Foundation/Modal/Kripke/Logic/GL/Completeness.lean b/Foundation/Modal/Kripke/Logic/GL/Completeness.lean index 50f7e14ea..c1c324a46 100644 --- a/Foundation/Modal/Kripke/Logic/GL/Completeness.lean +++ b/Foundation/Modal/Kripke/Logic/GL/Completeness.lean @@ -56,7 +56,7 @@ lemma truthlemma_lemma1 : ((□⁻¹'X.1 ∪ □'□⁻¹'X.1) ∪ {□ψ, -ψ}) ⊆ φ.subformulas⁻ := by intro χ hr; replace hr : χ = □ψ ∨ χ = -ψ ∨ □χ ∈ X ∨ ∃ a, □a ∈ X ∧ □a = χ := by - simpa [Finset.LO.preboxItr, Finset.LO.boxItr] using hr; + have h := hr; simp [Finset.LO.preboxItr, Finset.LO.boxItr] at h; exact h; rcases hr with (rfl | rfl | hp | ⟨χ, hr, rfl⟩); . apply Finset.mem_union.mpr; tauto; @@ -232,7 +232,7 @@ theorem finite_completeness_TFAE : [ tfae_have 4 → 2 := by rintro H F ⟨_, F_trans, F_irrefl⟩ V x; let M : Kripke.Model := ⟨F, V⟩; - simpa [Unique.uniq] using Model.pointGenerate.pMorphism M x |>.modal_equivalence _ |>.mp $ H (M↾x); + exact Model.pointGenerate.pMorphism M x |>.modal_equivalence ⟨x, by tauto⟩ |>.mp $ H (M↾x); tfae_finish; lemma iff_unprovable_exists_finite_rooted_model : Modal.GL ⊬ φ ↔ ∃ M : Model, ∃ _ : M.IsFinite, ∃ _ : M.IsTransitive, ∃ _ : M.IsIrreflexive, ∃ _ : M.IsRooted, ¬M.root.1 ⊧ φ := by diff --git a/Foundation/Modal/Kripke/Logic/GL/MDP.lean b/Foundation/Modal/Kripke/Logic/GL/MDP.lean index 9b1c0e4ab..b7ef0d315 100644 --- a/Foundation/Modal/Kripke/Logic/GL/MDP.lean +++ b/Foundation/Modal/Kripke/Logic/GL/MDP.lean @@ -69,7 +69,7 @@ def pMorphism₂ (F₁ F₂) : F₂ →ₚ (mdpCounterexmpleFrame F₁ F₂) whe lemma through_original_root (r₁ : F₁.Root) (r₂ : F₂.Root) (x : (mdpCounterexmpleFrame F₁ F₂).World) (h : (mdpCounterexmpleFrame F₁ F₂).root ≺ x) : (x = r₁ ∨ (Sum.inr (Sum.inl r₁.1) ≺ x)) ∨ (x = r₂ ∨ (Sum.inr (Sum.inr r₂.1) ≺ x)) := by match x with - | .inl x => grind; + | .inl x => simp only [Frame.Rel', Frame.root, default] at h; | .inr (.inl x) => by_cases e : x = r₁; . subst e; left; tauto; diff --git a/Foundation/Modal/Kripke/Logic/GL/Unnecessitation.lean b/Foundation/Modal/Kripke/Logic/GL/Unnecessitation.lean index a6314e154..0831ead16 100644 --- a/Foundation/Modal/Kripke/Logic/GL/Unnecessitation.lean +++ b/Foundation/Modal/Kripke/Logic/GL/Unnecessitation.lean @@ -44,7 +44,7 @@ lemma imply_boxdot_plain_of_imply_box_box : Modal.GL ⊢ □φ 🡒 □ψ → Mo push Not; use (Sum.inr M.root); constructor; - . grind; + . simp only [Frame.Rel', Frame.root, default]; . assumption; theorem unnecessitation! : Modal.GL ⊢ □φ → Modal.GL ⊢ φ := by diff --git a/Foundation/Modal/Kripke/Logic/GLPoint3.lean b/Foundation/Modal/Kripke/Logic/GLPoint3.lean index ed01b9d7c..ec59b07e7 100644 --- a/Foundation/Modal/Kripke/Logic/GLPoint3.lean +++ b/Foundation/Modal/Kripke/Logic/GLPoint3.lean @@ -76,7 +76,7 @@ private lemma complete.lemma₁ : Modal.GLPoint3 ⊢ ∼□φ 🡒 ◇(□φ ⋏ have := Satisfies.and_def.not.mp this; push Not at this; have := this h₂; - simpa using Satisfies.not_def.not.mp this; + exact not_not.mp (Satisfies.not_def.not.mp this); private lemma complete.lemma₂ {v : (canonicalModel Modal.GLPoint3).World } (h : ∼□φ ∈ v.1.1) : ∃! u, v ≺ u ∧ □φ ∈ u.1.1 ∧ φ ∈ u.1.2 := by @@ -201,7 +201,7 @@ private lemma complete.filteredModel.truthlemma : ∀ x : (complete.filteredMode . intro h y Rxy; apply ihψ y (by grind) |>.mpr; apply Rxy; - simpa using h; + exact h; open Classical in open complete in diff --git a/Foundation/Modal/Kripke/Logic/Grz/Completeness.lean b/Foundation/Modal/Kripke/Logic/Grz/Completeness.lean index 543634627..6b084409b 100644 --- a/Foundation/Modal/Kripke/Logic/Grz/Completeness.lean +++ b/Foundation/Modal/Kripke/Logic/Grz/Completeness.lean @@ -95,7 +95,7 @@ lemma truthlemma_lemma1 intro χ hr; apply Finset.mem_union.mpr; replace hr : χ = □(ψ 🡒 □ψ) ∨ χ = -ψ ∨ (∃ a, □a ∈ X ∧ □a = χ) := by - simpa [Finset.mem_union, Finset.LO.preboxItr, Finset.LO.boxItr] using hr; + have h := hr; simp [Finset.mem_union, Finset.LO.preboxItr, Finset.LO.boxItr] at h; exact h; rcases hr with (rfl | rfl | ⟨χ, hr, rfl⟩); . left; simp [Finset.LO.preboxItr]; diff --git a/Foundation/Modal/Kripke/Logic/KHen.lean b/Foundation/Modal/Kripke/Logic/KHen.lean index 55ab7d505..20b374f6b 100644 --- a/Foundation/Modal/Kripke/Logic/KHen.lean +++ b/Foundation/Modal/Kripke/Logic/KHen.lean @@ -106,7 +106,7 @@ lemma flat_to_flat : n♭ ≺ m♭ ↔ n > m := by simp [Frame.Rel']; lemma exists_flat_of_from_flat (h : n♭ ≺ x) : ∃ m, x = ⟨m, 1⟩ ∧ n > m := by match x with | ⟨m, 0⟩ => aesop; - | ⟨m, 1⟩ => use m; + | ⟨m, 1⟩ => exact ⟨m, rfl, flat_to_flat.mp h⟩; end cresswellFrame @@ -130,18 +130,19 @@ lemma cresswellModel.not_valid_axiomFour : ¬(Satisfies cresswellModel 2♯ (Axi | n♯ => intro h2n; suffices n ≠ 0 by simp [Satisfies]; grind + have := sharp_to_sharp.mp h2n; omega; | n♭ => simp [Satisfies]; . apply Satisfies.box_def.not.mpr push Not; use 1♯; constructor; - . omega; + . exact sharp_to_sharp.mpr (by omega); . apply Satisfies.box_def.not.mpr; push Not; use 0♯; constructor; - . omega; + . exact sharp_to_sharp.mpr (by omega); . tauto; @@ -287,21 +288,21 @@ lemma cresswellModel.valid_axiomHen : cresswellModel ⊧ □(□φ 🡘 φ) 🡒 rintro y Rny; match y with | _♭ => apply h; - | _♯ => apply hn_max; omega; + | _♯ => apply hn_max; have := sharp_to_sharp.mp Rny; omega; . apply Satisfies.imp_def₂.mpr; left; apply Satisfies.box_def.not.mpr; push Not; use (n + 1)♯; constructor; - . omega; + . exact sharp_to_sharp.mpr (by omega); . have : Satisfies cresswellModel (n + 1)♯ φ := hn_max (n + 1) (by omega); have : ¬Satisfies cresswellModel (n + 1)♯ (□φ) := by apply Satisfies.box_def.not.mpr; push Not; use n♯; constructor; - . omega; + . exact sharp_to_sharp.mpr (by omega); . apply hn; apply Satisfies.iff_def.not.mpr; tauto; diff --git a/Foundation/Modal/Kripke/Logic/KTMk.lean b/Foundation/Modal/Kripke/Logic/KTMk.lean index d44219da9..f50520a51 100644 --- a/Foundation/Modal/Kripke/Logic/KTMk.lean +++ b/Foundation/Modal/Kripke/Logic/KTMk.lean @@ -197,7 +197,6 @@ instance : Modal.KT ⪱ Modal.KTMk := by . exact { refl := by omega; } . suffices ∀ (x : Fin 3), 0 = x ∨ 1 = x → (∀ y, x = y ∨ x + 1 = y → ∀ z, y = z ∨ y + 1 = z → z ≠ 2) → x ≠ 0 ∧ x + 1 ≠ 0 by simp [Frame.Rel', Satisfies, Semantics.Models]; - grind; rintro x (rfl | rfl); . intro h; exfalso; diff --git a/Foundation/Modal/Kripke/Logic/S4Point2.lean b/Foundation/Modal/Kripke/Logic/S4Point2.lean index 359d35a35..42051b956 100644 --- a/Foundation/Modal/Kripke/Logic/S4Point2.lean +++ b/Foundation/Modal/Kripke/Logic/S4Point2.lean @@ -99,7 +99,18 @@ instance : Modal.S4 ⪱ Modal.S4Point2 := by constructor; . simp only [Set.mem_setOf_eq]; refine { refl := by omega, trans := by omega; }; . suffices ∃ x, (0 : M.World) ≺ x ∧ (∀ y, x ≺ y → y = 1) ∧ ∃ x, (0 : M.World) ≺ x ∧ ¬x ≺ 1 by - simpa [M, Semantics.Models, Satisfies]; + obtain ⟨x, h0x, hbox, y, h0y, hy1⟩ := this; + apply Satisfies.imp_def.not.mpr; + push Not; + refine ⟨?_, ?_⟩; + · exact Satisfies.dia_def.mpr ⟨x, h0x, Satisfies.box_def.mpr (fun z hxz => hbox z hxz)⟩; + · apply Satisfies.box_def.not.mpr; + push Not; + refine ⟨y, h0y, ?_⟩; + apply Satisfies.dia_def.not.mpr; + push Not; + intro w hyw hw; + exact hy1 (hw ▸ hyw); use 1; refine ⟨by omega, ?_, ?_⟩; . intro y; diff --git a/Foundation/Modal/Kripke/Logic/S4Point2McK.lean b/Foundation/Modal/Kripke/Logic/S4Point2McK.lean index 9d1294ebc..6670db194 100644 --- a/Foundation/Modal/Kripke/Logic/S4Point2McK.lean +++ b/Foundation/Modal/Kripke/Logic/S4Point2McK.lean @@ -68,7 +68,18 @@ instance : Modal.S4McK ⪱ Modal.S4Point2McK := by | 2 => use 2; tauto; } . suffices ∃ x, (0 : M.World) ≺ x ∧ (∀ y, x ≺ y → y = 1) ∧ ∃ x, (0 : M.World) ≺ x ∧ ¬x ≺ 1 by - simpa [M, Semantics.Models, Satisfies]; + obtain ⟨x, h0x, hbox, y, h0y, hy1⟩ := this; + apply Satisfies.imp_def.not.mpr; + push Not; + refine ⟨?_, ?_⟩; + · exact Satisfies.dia_def.mpr ⟨x, h0x, Satisfies.box_def.mpr (fun z hxz => hbox z hxz)⟩; + · apply Satisfies.box_def.not.mpr; + push Not; + refine ⟨y, h0y, ?_⟩; + apply Satisfies.dia_def.not.mpr; + push Not; + intro w hyw hw; + exact hy1 (hw ▸ hyw); use 1; refine ⟨?_, ?_, ?_⟩; . grind; diff --git a/Foundation/Modal/Kripke/Rank.lean b/Foundation/Modal/Kripke/Rank.lean index bf68ec420..de0e83254 100644 --- a/Foundation/Modal/Kripke/Rank.lean +++ b/Foundation/Modal/Kripke/Rank.lean @@ -94,7 +94,7 @@ lemma height_pos : 0 < (Frame.extendRoot F n).height := by rw [eq_extendRoot_height_rank_extendRoot_root]; apply lt_fcwHeight ?_ (by simp); · exact ↑F.root.1; - . grind; + . simp only [Frame.Rel', Frame.root, default]; @[simp] lemma height_succ : (F.extendRoot 1).height = F.height + 1 := by @@ -130,7 +130,7 @@ lemma height_succ : (F.extendRoot 1).height = F.height + 1 := by rcases exists_rank_terminal F.root.1 with ⟨j, hj⟩; use j, F.root; constructor; - . grind; + . exact Frame.extendRoot.rel_root_original_root; . exact embed_rel_iterate_embed_iff_rel.mpr hj; omit [F.IsRooted] in @@ -145,7 +145,8 @@ lemma eq_original_height : Frame.rank (x : F.extendRoot 1) = Frame.rank x := by . simp; . -- TODO: extract no loop lemma (x ≺^[n] i cannot happen where x is original and i is new elements by extension) exfalso; - have : (F.extendRoot 1).root ≺ (x : F.extendRoot 1) := by grind; + have : (F.extendRoot 1).root ≺ (x : F.extendRoot 1) := by + simp only [Frame.Rel', Frame.root, default]; have : (x : F.extendRoot 1) ≺ x := Rel.Iterate.unwrap_of_trans_of_pos (by omega) $ Rel.Iterate.comp (m := 1) |>.mp ⟨_, Rxy, by simpa⟩; @@ -166,7 +167,7 @@ lemma iff_eq_height_eq_original_root [F.IsRooted] {x : F.extendRoot 1} : Frame.r have := h ▸ height_succ (F := F); simp [Frame.height, Frame.root, default] at this; . intro h; - suffices x = F.root.1 by simp [this]; grind; + suffices x = F.root.1 by subst this; rfl; apply Frame.eq_height_root.mp; exact h ▸ Frame.extendRoot.eq_original_height.symm; . rintro rfl; diff --git a/Foundation/Modal/Logic/Basic.lean b/Foundation/Modal/Logic/Basic.lean index ac11469d7..2a234564b 100644 --- a/Foundation/Modal/Logic/Basic.lean +++ b/Foundation/Modal/Logic/Basic.lean @@ -128,8 +128,8 @@ lemma subset_of_weakerThan [L₁ ⪯ L₂] : L₁ ⊆ L₂ := by suffices L₁ ⊢ φ → L₂ ⊢ φ by grind; exact Entailment.WeakerThan.pbl; -instance [L₁ ≊ L₂] : L₁ ⪯ L₂ := Equiv.le inferInstance -instance [L₁ ≊ L₂] : L₂ ⪯ L₁ := Equiv.le $ .symm inferInstance +instance [L₁ ≊ L₂] : L₁ ⪯ L₂ := Entailment.Equiv.le inferInstance +instance [L₁ ≊ L₂] : L₂ ⪯ L₁ := Entailment.Equiv.le $ .symm inferInstance @[simp, grind .] lemma eq_of_equiv [L₁ ≊ L₂] : L₁ = L₂ := Set.Subset.antisymm subset_of_weakerThan subset_of_weakerThan diff --git a/Foundation/Modal/Logic/D/Basic.lean b/Foundation/Modal/Logic/D/Basic.lean index 05950b3cf..ea95cdc11 100644 --- a/Foundation/Modal/Logic/D/Basic.lean +++ b/Foundation/Modal/Logic/D/Basic.lean @@ -161,25 +161,36 @@ instance {F : Frame} [F.IsFinite] [F.IsIrreflexive] [F.IsTransitive] : F.IsConve namespace Model +/-- Accessibility for `tailModel₀`, factored out so the `tailModel₀` structure literal carries no + inline `match` (v4.31's equation-theorem generator chokes on the auto-generated World matcher when + the discriminant's structure literal embeds a `match`). `@[simp, grind]` keeps the old inline-match + reducibility for the `grind`/`simp`/`omega` proofs below. The row-2 pattern is narrowed from + `.inl _, _` to `.inl _, .inr _` to remove the overlap with row 1 (same semantics: `(.inl, .inl)` + still hits row 1 → False), also needed for v4.31's equation generator. -/ +@[simp, grind] def tailRel₀ (M : Kripke.Model) [M.IsPointRooted] : + (Unit ⊕ ℕ ⊕ M.World) → (Unit ⊕ ℕ ⊕ M.World) → Prop + | _ , .inl _ => False -- ¬(x ≺ ω) + | .inl _, .inr _ => True -- ω ≺ x where x is not ω + | .inr $ .inl x, .inr $ .inl y => x > y -- x ≺ y ↔ x > y where x, y ∈ ω + | .inr $ .inl _, .inr $ .inr _ => True + | .inr $ .inr _, .inr $ .inl _ => False + | .inr $ .inr x, .inr $ .inr y => x ≺ y + +/-- Valuation for `tailModel₀`, factored out for the same reason as `tailRel₀`. -/ +@[simp, grind] def tailVal₀ (M : Kripke.Model) [M.IsPointRooted] (o : ℕ → Prop) : + ℕ → (Unit ⊕ ℕ ⊕ M.World) → Prop + | p, .inl _ => o p + | p, .inr $ .inl _ => M.Val p M.root.1 + | p, .inr $ .inr x => M.Val p x + /-- `ω`-extend root model. Valuation on `n ∈ ω` is same on `M.root` and on point `ω` is by `o`. -/ abbrev tailModel₀ (M : Kripke.Model) [M.IsPointRooted] (o : ℕ → Prop) : Kripke.Model where World := Unit ⊕ ℕ ⊕ M.World -- `Unit` means `ω` - Rel x y := - match x, y with - | _ , .inl _ => False -- ¬(x ≺ ω) - | .inl _, _ => True -- ω ≺ x where x is not ω - | .inr $ .inl x, .inr $ .inl y => x > y -- x ≺ y ↔ x > y where x, y ∈ ω - | .inr $ .inl _, .inr $ .inr _ => True - | .inr $ .inr _, .inr $ .inl _ => False - | .inr $ .inr x, .inr $ .inr y => x ≺ y - Val p x := - match x with - | .inl _ => o p - | .inr $ .inl _ => M.Val p M.root.1 - | .inr $ .inr x => M.Val p x + Rel := M.tailRel₀ + Val := M.tailVal₀ o namespace tailModel₀ @@ -192,6 +203,8 @@ instance instPontRooted : (M.tailModel₀ o).IsPointRooted where have := r'.2 (.inl ()) (by grind); simp [Frame.Rel'] at this; +@[simp] lemma root_eq : (↑(M.tailModel₀ o).root : (M.tailModel₀ o).World) = Sum.inl () := rfl + instance instTransitive [M.IsTransitive] : (M.tailModel₀ o).IsTransitive := ⟨by grind⟩ @[coe] abbrev embed_nat (n : ℕ) : M.tailModel₀ o := .inr $ .inl n @@ -211,7 +224,7 @@ instance instCWF [M.IsConverseWellFounded] : (M.tailModel₀ o).IsConverseWellFo . let m := Set.IsWF.min (s := s₂) (Set.IsWF.of_wellFoundedLT _) (by assumption); use embed_nat m; constructor; - . simpa using Set.IsWF.min_mem (s := s₂) _ _; + . exact Set.IsWF.min_mem (Set.IsWF.of_wellFoundedLT s₂) hs₂; . intro x hx; match x with | .inl _ => grind; @@ -257,7 +270,8 @@ protected def pMorphism_extendRoot (M : Model) [M.IsPointRooted] (n) : (M.extend | .inr x => embed_original x forth := by rintro (x | x) (y | y) Rxy <;> - simp_all only [Model.extendRoot, Frame.extendRoot, tailModel₀]; + simp_all only [Model.extendRoot, Frame.extendRoot, tailModel₀, tailRel₀, tailVal₀, + Frame.Rel', embed_nat, embed_original]; case inl.inl => omega; back := by rintro (x | x) (y | y | y) Rxy; @@ -359,7 +373,7 @@ theorem GL_D_TFAE : apply Satisfies.not_box_def.mpr; use tailModel₀.embed_original M.root; constructor; - . grind; + . exact trivial; . tauto; | @axiomDz φ ψ => intro h; @@ -379,20 +393,20 @@ theorem GL_D_TFAE : have Rzx : z ≺ x := by unfold z; match x, y with - | .inr $ .inl _, .inr $ .inl _ => dsimp [tailModel₀]; omega; + | .inr $ .inl _, .inr $ .inl _ => simp only [Frame.Rel', tailModel₀, tailRel₀]; omega; | .inr $ .inr _, .inr $ .inl _ | .inr $ .inl _, .inr $ .inr _ | .inr $ .inr _, .inr $ .inr _ => grind; have Rzy : z ≺ y := by unfold z; match x, y with - | .inr $ .inl _, .inr $ .inl _ => dsimp [tailModel₀]; omega; + | .inr $ .inl _, .inr $ .inl _ => simp only [Frame.Rel', tailModel₀, tailRel₀]; omega; | .inr $ .inr _, .inr $ .inl _ | .inr $ .inl _, .inr $ .inr _ | .inr $ .inr _, .inr $ .inr _ => grind; use z; constructor; - . grind; + . exact trivial; . apply Satisfies.or_def.not.mpr; push Not; constructor; @@ -426,7 +440,7 @@ theorem GL_D_TFAE : exact (show ∀ ψ ∈ φ.subformulas, Satisfies _ _ ψ ↔ Satisfies M M.root ψ by intro ψ hψ; induction ψ with - | hatom p | hfalsum => simp [Satisfies]; + | hatom p | hfalsum => exact Iff.rfl; | himp φ ψ ihφ ihψ => simp [Satisfies, ihφ (by grind), ihψ (by grind)]; | hbox ψ ihψ => replace ihψ := ihψ (by grind); diff --git a/Foundation/Modal/Logic/GLPlusBoxBot/Basic.lean b/Foundation/Modal/Logic/GLPlusBoxBot/Basic.lean index 726650567..70498ee1c 100644 --- a/Foundation/Modal/Logic/GLPlusBoxBot/Basic.lean +++ b/Foundation/Modal/Logic/GLPlusBoxBot/Basic.lean @@ -44,7 +44,7 @@ lemma iff_provable_GLPlusBoxBot_provable_GL {n : ℕ} {φ} : Modal.GLPlusBoxBot replace h : Modal.GLPlusBoxBot n ⊢ (□^[n]⊥) 🡒 φ := sumQuasiNormal.mem₁! h; exact h ⨀ (by simp); -@[simp, grind =_] lemma eq_GLPlusBoxBot_omega_GL : (Modal.GLPlusBoxBot ⊤) = Modal.GL := by grind; +@[simp, grind =_] lemma eq_GLPlusBoxBot_omega_GL : (Modal.GLPlusBoxBot ⊤) = Modal.GL := rfl section diff --git a/Foundation/Modal/Logic/Global.lean b/Foundation/Modal/Logic/Global.lean index e7e82be02..7ad1253da 100644 --- a/Foundation/Modal/Logic/Global.lean +++ b/Foundation/Modal/Logic/Global.lean @@ -42,13 +42,15 @@ open LO.Entailment LO.Entailment.FiniteContext LO.Modal.Entailment variable {L : Logic α} {X Y : Set (Formula α)} {φ ψ : Formula α} instance : Entailment.Łukasiewicz (F := Formula α) (S := Logic α × Set (Formula α)) (L, X) where - mdp ihφψ ihφ := by simpa using GlobalConsequence.mdp ihφψ ihφ; + mdp ihφψ ihφ := by + have h := GlobalConsequence.mdp ihφψ ihφ; + rw [Set.union_self] at h; exact h; implyK := GlobalConsequence.implyK X implyS := GlobalConsequence.implyS X elimContra := GlobalConsequence.ec X instance : Entailment.Necessitation (F := Formula α) (S := Logic α × Set (Formula α)) (L, X) where - nec ihφ := by simpa using GlobalConsequence.nec ihφ + nec ihφ := by exact GlobalConsequence.nec ihφ instance [L.IsNormal] : Entailment.K (F := Formula α) (S := Logic α × Set (Formula α)) (L, X) where K _ _ := by diff --git a/Foundation/Modal/Logic/SumQuasiNormal.lean b/Foundation/Modal/Logic/SumQuasiNormal.lean index 430bc9d66..1b0f13764 100644 --- a/Foundation/Modal/Logic/SumQuasiNormal.lean +++ b/Foundation/Modal/Logic/SumQuasiNormal.lean @@ -11,10 +11,10 @@ namespace Logic variable {L L₁ L₂ : Logic α} {φ ψ : Formula α} {s : Substitution α} inductive sumQuasiNormal (L₁ L₂ : Logic α) : Logic α - | mem₁ {φ} : L₁ ⊢ φ → sumQuasiNormal L₁ L₂ φ - | mem₂ {φ} : L₂ ⊢ φ → sumQuasiNormal L₁ L₂ φ - | mdp {φ ψ} : sumQuasiNormal L₁ L₂ (φ 🡒 ψ) → sumQuasiNormal L₁ L₂ φ → sumQuasiNormal L₁ L₂ ψ - | subst {φ s} : sumQuasiNormal L₁ L₂ φ → sumQuasiNormal L₁ L₂ (φ⟦s⟧) + | mem₁ {φ : Formula α} : L₁ ⊢ φ → sumQuasiNormal L₁ L₂ φ + | mem₂ {φ : Formula α} : L₂ ⊢ φ → sumQuasiNormal L₁ L₂ φ + | mdp {φ ψ : Formula α} : sumQuasiNormal L₁ L₂ (φ 🡒 ψ) → sumQuasiNormal L₁ L₂ φ → sumQuasiNormal L₁ L₂ ψ + | subst {φ : Formula α} {s : Substitution α} : sumQuasiNormal L₁ L₂ φ → sumQuasiNormal L₁ L₂ (φ⟦s⟧) namespace sumQuasiNormal @@ -235,8 +235,8 @@ end sumQuasiNormal inductive sumQuasiNormal' (L₁ L₂ : Logic α) : Logic α -| mem₁ {φ} (s : Substitution _) : L₁ ⊢ φ → sumQuasiNormal' L₁ L₂ (φ⟦s⟧) -| mem₂ {φ} (s : Substitution _) : L₂ ⊢ φ → sumQuasiNormal' L₁ L₂ (φ⟦s⟧) +| mem₁ {φ : Formula α} (s : Substitution _) : L₁ ⊢ φ → sumQuasiNormal' L₁ L₂ (φ⟦s⟧) +| mem₂ {φ : Formula α} (s : Substitution _) : L₂ ⊢ φ → sumQuasiNormal' L₁ L₂ (φ⟦s⟧) | mdp {φ ψ : Formula α} : sumQuasiNormal' L₁ L₂ (φ 🡒 ψ) → sumQuasiNormal' L₁ L₂ φ → sumQuasiNormal' L₁ L₂ ψ namespace sumQuasiNormal' @@ -285,8 +285,14 @@ instance : (sumQuasiNormal' L₁ L₂).Substitution where subst s hφ := by rw [iff_provable] at ⊢ hφ; induction hφ with - | mem₁ s' h => simpa using mem₁ (s := s' ∘ s) h - | mem₂ s' h => simpa using mem₂ (s := s' ∘ s) h + | mem₁ s' h => + have h := mem₁ (L₂ := L₂) (s := s' ∘ s) h + rw [Formula.subst.def_comp] at h + exact h + | mem₂ s' h => + have h := mem₂ (L₁ := L₁) (s := s' ∘ s) h + rw [Formula.subst.def_comp] at h + exact h | mdp _ _ ihφψ ihφ => exact mdp ihφψ ihφ end sumQuasiNormal' diff --git a/Foundation/Modal/MaximalConsistentSet.lean b/Foundation/Modal/MaximalConsistentSet.lean index 9825e72cd..a3a2105b3 100644 --- a/Foundation/Modal/MaximalConsistentSet.lean +++ b/Foundation/Modal/MaximalConsistentSet.lean @@ -372,7 +372,7 @@ lemma iff_mem_imp : ((φ 🡒 ψ) ∈ Ω) ↔ (φ ∈ Ω) → (ψ ∈ Ω) := by apply membership_iff.mpr; exact dpq ⨀ dp; . intro h; - replace h : φ ∉ Ω.1 ∨ ψ ∈ Ω := or_iff_not_imp_left.mpr (by simpa using h); + replace h : φ ∉ Ω.1 ∨ ψ ∈ Ω := or_iff_not_imp_left.mpr (fun hn => h (not_not.mp hn)); cases h with | inl h => apply membership_iff.mpr; @@ -467,7 +467,7 @@ lemma iff_mem_boxItr : (□^[n]φ ∈ Ω) ↔ (∀ {Ω' : MaximalConsistentSet have : 𝓢 ⊬ ⋀((□^[n]'Γ)) 🡒 □^[n]φ := FiniteContext.provable_iff.not.mp $ this (□^[n]'Γ) (by intro ψ hq; obtain ⟨χ, hr₁, rfl⟩ := List.LO.exists_of_mem_boxItr hq; - simpa using hΓ₁ χ hr₁; + exact Set.LO.iff_mem_preboxItr.mp (hΓ₁ χ hr₁); ); contrapose! this; exact C!_trans collect_boxItr_conj! this; diff --git a/Foundation/Modal/Modality/Basic.lean b/Foundation/Modal/Modality/Basic.lean index 10f9b28e6..81155748e 100644 --- a/Foundation/Modal/Modality/Basic.lean +++ b/Foundation/Modal/Modality/Basic.lean @@ -2,6 +2,7 @@ module public import Foundation.Modal.Hilbert.Normal.Basic public import Foundation.Modal.Logic.SumNormal +public meta import Foundation.Modal.Formula.Basic @[expose] public section diff --git a/Foundation/Modal/PLoN/Completeness.lean b/Foundation/Modal/PLoN/Completeness.lean index 23f58deb3..b9d7a47b5 100644 --- a/Foundation/Modal/PLoN/Completeness.lean +++ b/Foundation/Modal/PLoN/Completeness.lean @@ -60,7 +60,7 @@ lemma truthlemma : ∀ {X : (canonicalModel 𝓢).World}, X ⊩ φ ↔ (φ ∈ X have : □φ ∉ X := iff_mem_neg.mp RXY.1; contradiction; -instance instComplete_of_mem_canonicalFrame {C : PLoN.FrameClass} (h : (canonicalFrame 𝓢) ∈ C) : Complete 𝓢 C := by +def instComplete_of_mem_canonicalFrame {C : PLoN.FrameClass} (h : (canonicalFrame 𝓢) ∈ C) : Complete 𝓢 C := by constructor; intro φ; contrapose!; diff --git a/Foundation/Modal/PLoN/Hilbert.lean b/Foundation/Modal/PLoN/Hilbert.lean index 23f827c16..73f1e483d 100644 --- a/Foundation/Modal/PLoN/Hilbert.lean +++ b/Foundation/Modal/PLoN/Hilbert.lean @@ -30,7 +30,7 @@ lemma soundness_frameclass (hV : C ⊧* Ax.instances) : Hilbert.Normal Ax ⊢ φ apply ValidOnModel.mdp (ihpq V) (ihp V); | _ => grind; -instance instFrameClassSound (hV : C ⊧* Ax.instances) : Sound (Hilbert.Normal Ax) C := ⟨fun {_} => soundness_frameclass hV⟩ +def instFrameClassSound (hV : C ⊧* Ax.instances) : Sound (Hilbert.Normal Ax) C := ⟨fun {_} => soundness_frameclass hV⟩ lemma consistent_of_nonempty_frameClass (C : PLoN.FrameClass) (hC : Set.Nonempty C) [sound : Sound (Hilbert.Normal Ax) C] : Entailment.Consistent (Hilbert.Normal Ax) := by apply Entailment.Consistent.of_unprovable (φ := ⊥); diff --git a/Foundation/Modal/Tableau.lean b/Foundation/Modal/Tableau.lean index e51405d89..11e8bb467 100644 --- a/Foundation/Modal/Tableau.lean +++ b/Foundation/Modal/Tableau.lean @@ -782,7 +782,7 @@ private lemma of_mem₂_boxItr : (□^[n]φ ∈ t.1.2) → (∃ t' : MaximalCons . rintro ψ hψ; obtain ⟨ξ, hξ, rfl⟩ := Finset.LO.exists_of_mem_boxItr hψ; simp at hΓ; - simpa using hΓ $ by simpa; + exact Set.LO.iff_mem_preboxItr.mp (hΓ $ by simpa); . simpa; use t'; constructor; diff --git a/Foundation/Propositional/Boolean/ZeroSubst.lean b/Foundation/Propositional/Boolean/ZeroSubst.lean index 11d91fcd1..1bd7d6e30 100644 --- a/Foundation/Propositional/Boolean/ZeroSubst.lean +++ b/Foundation/Propositional/Boolean/ZeroSubst.lean @@ -62,14 +62,14 @@ lemma vfSubst_tautology : v ⊧ φ ↔ (φ⟦(vfSubst v)⟧.IsTautology) := by apply ihφ.mpr; intro u; apply equiv_of_letterless ?_ u w |>.mpr hφ; - grind; + exact Formula.letterless_zeroSubst; . intro h hφ; apply ihψ.mpr; intro w; apply equiv_of_letterless ?_ v w |>.mp; . apply h; apply ihφ.mp hφ; - grind; + exact Formula.letterless_zeroSubst; | hor φ ψ ihφ ihψ => constructor; . rintro (h | h) w; @@ -81,12 +81,12 @@ lemma vfSubst_tautology : v ⊧ φ ↔ (φ⟦(vfSubst v)⟧.IsTautology) := by apply ihφ.mpr; intro w; apply equiv_of_letterless ?_ v w |>.mp hφ; - grind; + exact Formula.letterless_zeroSubst; . right; apply ihψ.mpr; intro w; apply equiv_of_letterless ?_ v w |>.mp hψ; - grind; + exact Formula.letterless_zeroSubst; | hand φ ψ ihφ ihψ => constructor; . rintro ⟨hφ, hψ⟩ w; @@ -99,11 +99,11 @@ lemma vfSubst_tautology : v ⊧ φ ↔ (φ⟦(vfSubst v)⟧.IsTautology) := by . apply ihφ.mpr; intro w; apply equiv_of_letterless ?_ v w |>.mp $ h v |>.1; - grind; + exact Formula.letterless_zeroSubst; . apply ihψ.mpr; intro w; apply equiv_of_letterless ?_ v w |>.mp $ h v |>.2; - grind; + exact Formula.letterless_zeroSubst; end LO.Propositional.Boolean end diff --git a/Foundation/Propositional/FMT/Hilbert/Basic.lean b/Foundation/Propositional/FMT/Hilbert/Basic.lean index b70cefb1d..ee5ba2feb 100644 --- a/Foundation/Propositional/FMT/Hilbert/Basic.lean +++ b/Foundation/Propositional/FMT/Hilbert/Basic.lean @@ -26,7 +26,7 @@ lemma soundness_frameclass (hV : C ⊧* H) : H ⊢ φ → C ⊧ φ := by | axm hi => apply hV.models <;> assumption; | _ => grind; -instance instFrameClassSound (hV : C ⊧* H) : Sound H C := ⟨fun {_} => soundness_frameclass hV⟩ +def instFrameClassSound (hV : C ⊧* H) : Sound H C := ⟨fun {_} => soundness_frameclass hV⟩ lemma consistent_of_sound_frameclass (C : FMT.FrameClass) (hC : Set.Nonempty C) [sound : Sound H C] : Entailment.Consistent H := by apply Entailment.Consistent.of_unprovable (φ := ⊥); @@ -58,7 +58,7 @@ lemma soundness_modelclass (hV : C ⊧* H) : H ⊢ φ → C ⊧ φ := by | axm hi => apply hV.models <;> assumption; | _ => grind -instance instModelClassSound (hV : C ⊧* H) : Sound H C := ⟨fun {_} => soundness_modelclass hV⟩ +def instModelClassSound (hV : C ⊧* H) : Sound H C := ⟨fun {_} => soundness_modelclass hV⟩ lemma consistent_of_sound_modelclass (C : FMT.ModelClass) (hC : Set.Nonempty C) [sound : Sound H C] : Entailment.Consistent H := by apply Entailment.Consistent.of_unprovable (φ := ⊥); diff --git a/Foundation/Propositional/FMT/Hilbert/VF.lean b/Foundation/Propositional/FMT/Hilbert/VF.lean index d830df237..0614e8e64 100644 --- a/Foundation/Propositional/FMT/Hilbert/VF.lean +++ b/Foundation/Propositional/FMT/Hilbert/VF.lean @@ -92,8 +92,18 @@ instance : (HilbertVF.VF : HilbertVF ℕ) ⪱ HilbertWF.WF := by }, 0; constructor; . tauto; - . simp; - grind; + . apply Forces.not_def_iff.mpr; + refine Or.inl ⟨1, trivial, ?_, ?_⟩; + · -- 1 ⊩ ⊤ 🡒 #0 ⋏ #1 (vacuous: 1 ≺[·] · reduces to 1 ≠ 1) + apply Forces.def_imp.mpr; + intro z hz; + exact absurd rfl hz; + · -- 1 ⊮ ⊤ 🡒 #1 ⋏ #0 (witnessed at world 2, where #1 fails) + intro hψ; + have h2 := Forces.def_imp.mp hψ (y := 2) (show (1 : Fin 3) ≤ 2 by decide) Forces.def_top; + have ha := (Forces.def_and.mp h2).1; + rw [Forces.def_atom] at ha; + simp at ha; end LO.Propositional end diff --git a/Foundation/Propositional/Heyting/Semantics.lean b/Foundation/Propositional/Heyting/Semantics.lean index c5612dcc8..88cb6b9bd 100644 --- a/Foundation/Propositional/Heyting/Semantics.lean +++ b/Foundation/Propositional/Heyting/Semantics.lean @@ -113,7 +113,7 @@ lemma sound {φ : Formula α} : H ⊢ φ → mod H ⊧ φ := by | axm hφ => apply hℍ.models_set; assumption; | @mdp φ ψ _ _ ihpq ihp => have : (ℍ ⊧ₕ φ) ≤ (ℍ ⊧ₕ ψ) := by simpa using ihpq - simpa [val_def'.mp ihp] using this + apply val_def'.mpr; simpa [val_def'.mp ihp] using this | _ => simp [himp_himp_inf_himp_inf_le, himp_inf_himp_inf_sup_le] instance : Sound H (mod H) := ⟨sound⟩ @@ -137,7 +137,8 @@ lemma lindenbaum_val_eq : (lindenbaum H ⊧ₕ φ) = ⟦φ⟧ := by | _ => rfl lemma lindenbaum_complete_iff {φ : Formula α} : lindenbaum H ⊧ φ ↔ H ⊢ φ := by - grind [val_def', lindenbaum_val_eq, provable_iff_eq_top] + rw [val_def', lindenbaum_val_eq] + exact provable_iff_eq_top.symm instance : Sound H (lindenbaum H) := ⟨lindenbaum_complete_iff.mpr⟩ diff --git a/Foundation/Propositional/Hilbert/F/Basic.lean b/Foundation/Propositional/Hilbert/F/Basic.lean index e94725cba..8aba21743 100644 --- a/Foundation/Propositional/Hilbert/F/Basic.lean +++ b/Foundation/Propositional/Hilbert/F/Basic.lean @@ -17,7 +17,7 @@ namespace HilbertF instance : SetLike (HilbertF α) (Formula α) where coe := HilbertF.schema - coe_injective' := by intro ⟨A, hA⟩ ⟨B, hB⟩ h; simpa + coe_injective := by intro ⟨A, hA⟩ ⟨B, hB⟩ h; simpa protected def F : HilbertF α := ⟨∅, by grind⟩ protected def F_Ser : HilbertF α := ⟨{ Axioms.Ser }, by grind⟩ diff --git a/Foundation/Propositional/Hilbert/F/Deduction.lean b/Foundation/Propositional/Hilbert/F/Deduction.lean index 92d00fed3..e143d93f3 100644 --- a/Foundation/Propositional/Hilbert/F/Deduction.lean +++ b/Foundation/Propositional/Hilbert/F/Deduction.lean @@ -10,7 +10,7 @@ open Entailment.Corsi attribute [grind <=] Entailment.mdp! -variable {α : Type*} {H : HilbertF α} {Γ : Set (Formula α)} {φ ψ : Formula α} +variable {α : Type*} {H : HilbertF α} {Γ : Set (Formula α)} inductive Deduction (H : HilbertF α) (Γ : Set (Formula α)) : Formula α → Prop | protected ctx {φ} : φ ∈ Γ → Deduction H Γ φ @@ -18,6 +18,8 @@ inductive Deduction (H : HilbertF α) (Γ : Set (Formula α)) : Formula α → P | protected mp {φ ψ} : H ⊢ (φ 🡒 ψ) → Deduction H Γ φ → Deduction H Γ ψ | protected andIR {φ ψ} : Deduction H Γ φ → Deduction H Γ ψ → Deduction H Γ (φ ⋏ ψ) +variable {φ ψ : Formula α} + @[grind ⇒] lemma deducible_of_provable (hφ : H ⊢ φ) : Deduction H Γ φ := by apply Deduction.thm hφ; @[simp, grind =] @@ -78,7 +80,7 @@ lemma DT_list {Γ : List (Formula α)} : (Deduction H Γ.toFinset φ) ↔ H ⊢ | hcons ψ Γ hΓ ih => sorry; -lemma DT_finset {Γ : Finset (Formula α)} : (Deduction H Γ φ) ↔ (H ⊢ Γ.conj 🡒 φ) := by simpa using DT_list (Γ := Γ.toList); +lemma DT_finset {Γ : Finset (Formula α)} : (Deduction H Γ φ) ↔ (H ⊢ Γ.conj 🡒 φ) := by simpa [Finset.conj] using DT_list (Γ := Γ.toList); lemma DT_set {Γ : Set (Formula α)} : (Deduction H Γ φ) ↔ ∃ Δ : Finset (Formula α), ↑Δ ⊆ Γ ∧ Deduction H Δ φ := by constructor; diff --git a/Foundation/Propositional/Hilbert/Minimal/Basic.lean b/Foundation/Propositional/Hilbert/Minimal/Basic.lean index 1b9e748ad..aaa7572a7 100644 --- a/Foundation/Propositional/Hilbert/Minimal/Basic.lean +++ b/Foundation/Propositional/Hilbert/Minimal/Basic.lean @@ -21,7 +21,7 @@ namespace Hilbert instance : SetLike (Hilbert α) (Formula α) where coe := Hilbert.schema - coe_injective' := by intro ⟨A, hA⟩ ⟨B, hB⟩ h; simpa; + coe_injective := by intro ⟨A, hA⟩ ⟨B, hB⟩ h; simpa; protected def Min : Hilbert α := ⟨∅, by tauto⟩ protected def Int : Hilbert α := ⟨{ Axioms.EFQ φ | φ }, by grind⟩ diff --git a/Foundation/Propositional/Hilbert/VF/Basic.lean b/Foundation/Propositional/Hilbert/VF/Basic.lean index 2e8175dfd..bd208c53e 100644 --- a/Foundation/Propositional/Hilbert/VF/Basic.lean +++ b/Foundation/Propositional/Hilbert/VF/Basic.lean @@ -17,7 +17,7 @@ namespace HilbertVF instance : SetLike (HilbertVF α) (Formula α) where coe := HilbertVF.schema - coe_injective' := by intro ⟨A, hA⟩ ⟨B, hB⟩ h; simpa + coe_injective := by intro ⟨A, hA⟩ ⟨B, hB⟩ h; simpa protected def VF : HilbertVF α := ⟨∅, by grind⟩ protected def VF_Ser : HilbertVF α := ⟨{ Axioms.Ser }, by grind⟩ diff --git a/Foundation/Propositional/Hilbert/WF/Basic.lean b/Foundation/Propositional/Hilbert/WF/Basic.lean index 05f090218..46e86d7d1 100644 --- a/Foundation/Propositional/Hilbert/WF/Basic.lean +++ b/Foundation/Propositional/Hilbert/WF/Basic.lean @@ -17,7 +17,7 @@ namespace HilbertWF instance : SetLike (HilbertWF α) (Formula α) where coe := HilbertWF.schema - coe_injective' := by intro ⟨A, hA⟩ ⟨B, hB⟩ h; simpa + coe_injective := by intro ⟨A, hA⟩ ⟨B, hB⟩ h; simpa protected def WF : HilbertWF α := ⟨∅, by grind⟩ diff --git a/Foundation/Propositional/Kripke/AxiomWLEM.lean b/Foundation/Propositional/Kripke/AxiomWLEM.lean index 08a91fc2f..e4c5d13ac 100644 --- a/Foundation/Propositional/Kripke/AxiomWLEM.lean +++ b/Foundation/Propositional/Kripke/AxiomWLEM.lean @@ -85,7 +85,7 @@ instance [Entailment.HasAxiomWLEM 𝓢] : (canonicalFrame 𝓢).IsPiecewiseStron suffices Tableau.Consistent 𝓢 (y.1.1 ∪ z.1.1, ∅) by obtain ⟨w, hw⟩ := lindenbaum (𝓢 := 𝓢) this; use w; - simpa using hw; + simpa [canonicalFrame.rel₁] using hw; intro Γ Δ; intro hΓ hΔ h; diff --git a/Foundation/Propositional/Kripke/Basic.lean b/Foundation/Propositional/Kripke/Basic.lean index f83a3d9d6..95d563b44 100644 --- a/Foundation/Propositional/Kripke/Basic.lean +++ b/Foundation/Propositional/Kripke/Basic.lean @@ -371,8 +371,10 @@ lemma all.validates_AxiomEFQ : FrameClass.all.ValidatesFormula (Axioms.EFQ (.ato exact Formula.Kripke.ValidOnFrame.efq; lemma Validates.withAxiomEFQ (hV : C.Validates Γ) : C.Validates (insert (Axioms.EFQ (.atom 0)) Γ) := by - convert Validates.inter_of all.validates_AxiomEFQ hV; - tauto_set; + intro F hF φ hφ; + rcases hφ with rfl | hφ; + · exact Formula.Kripke.ValidOnFrame.efq; + · exact hV F hF φ hφ; protected abbrev finite_all : FrameClass := { F | F.IsFinite } diff --git a/Foundation/Propositional/Kripke/Filtration.lean b/Foundation/Propositional/Kripke/Filtration.lean index 62a96a325..e821dbacd 100644 --- a/Foundation/Propositional/Kripke/Filtration.lean +++ b/Foundation/Propositional/Kripke/Filtration.lean @@ -329,7 +329,7 @@ instance finestFiltrationTransitiveClosureModel.filterOf : FilterOf (finestFiltr obtain ⟨u, rfl⟩ := Quotient.exists_rep U; intro φ hφ hx; refine @ih u ?_ φ hφ ?_; - . simpa using RUY; + . exact RUY; . have : v ⊧ φ := FilterEqvQuotient.iff_of_eq exv _ hφ |>.mp hx; have : w ⊧ φ := formula_hereditary Rvw this; exact FilterEqvQuotient.iff_of_eq euw _ hφ |>.mpr this; diff --git a/Foundation/Propositional/Kripke2/Hilbert/Basic.lean b/Foundation/Propositional/Kripke2/Hilbert/Basic.lean index 0ccd4df6e..b61a28664 100644 --- a/Foundation/Propositional/Kripke2/Hilbert/Basic.lean +++ b/Foundation/Propositional/Kripke2/Hilbert/Basic.lean @@ -26,7 +26,7 @@ lemma soundness_frameclass (hV : C ⊧* H) : H ⊢ φ → C ⊧ φ := by | axm hi => apply hV.models <;> assumption; | _ => grind; -instance instFrameClassSound (hV : C ⊧* H) : Sound H C := ⟨fun {_} => soundness_frameclass hV⟩ +def instFrameClassSound (hV : C ⊧* H) : Sound H C := ⟨fun {_} => soundness_frameclass hV⟩ lemma consistent_of_sound_frameclass (sound : Sound H C) (hC : Set.Nonempty C) : Entailment.Consistent H := by apply Entailment.Consistent.of_unprovable (φ := ⊥); @@ -58,7 +58,7 @@ lemma soundness_modelclass (hV : C ⊧* H) : H ⊢ φ → C ⊧ φ := by | axm hi => apply hV.models <;> assumption; | _ => grind -instance instModelClassSound (hV : C ⊧* H) : Sound H C := ⟨fun {_} => soundness_modelclass hV⟩ +def instModelClassSound (hV : C ⊧* H) : Sound H C := ⟨fun {_} => soundness_modelclass hV⟩ lemma consistent_of_sound_modelclass (sound : Sound H C) (hC : Set.Nonempty C) : Entailment.Consistent H := by apply Entailment.Consistent.of_unprovable (φ := ⊥); diff --git a/Foundation/Propositional/Logic/Basic.lean b/Foundation/Propositional/Logic/Basic.lean index c0be2ce7a..1fbb738b0 100644 --- a/Foundation/Propositional/Logic/Basic.lean +++ b/Foundation/Propositional/Logic/Basic.lean @@ -20,7 +20,7 @@ namespace Logic instance : SetLike (Logic α) (Formula α) where coe := logic - coe_injective' _ _ := Logic.ext + coe_injective _ _ := Logic.ext class IsTrivial (L : Logic α) : Prop where eq_univ : L.logic = Set.univ diff --git a/Foundation/Propositional/Logic/Superintuitionistic.lean b/Foundation/Propositional/Logic/Superintuitionistic.lean index 8a1cfe3d6..040c8bb37 100644 --- a/Foundation/Propositional/Logic/Superintuitionistic.lean +++ b/Foundation/Propositional/Logic/Superintuitionistic.lean @@ -15,7 +15,7 @@ variable {L : SuperintuitionisticLogic α} {φ ψ : Formula α} lemma subset_Int (h : φ ∈ Propositional.Int) : φ ∈ L.logic := L.subset_L h lemma trivial_of_mem_bot (h : ⊥ ∈ L.toLogic) : ∀ {φ}, φ ∈ L.toLogic := L.mdp (L.subset_Int Entailment.efq!) h -instance (h : ⊥ ∈ L.toLogic) : L.IsTrivial := ⟨Set.eq_univ_iff_forall.mpr $ @trivial_of_mem_bot α L h⟩ +lemma isTrivial_of_mem_bot (h : ⊥ ∈ L.toLogic) : L.IsTrivial := ⟨Set.eq_univ_iff_forall.mpr $ @trivial_of_mem_bot α L h⟩ class Consistent (L : SuperintuitionisticLogic α) : Prop where not_mem_bot : ⊥ ∉ L.logic diff --git a/Foundation/Propositional/Neighborhood/NB/Basic.lean b/Foundation/Propositional/Neighborhood/NB/Basic.lean index e18aadfe4..1ecaae408 100644 --- a/Foundation/Propositional/Neighborhood/NB/Basic.lean +++ b/Foundation/Propositional/Neighborhood/NB/Basic.lean @@ -69,8 +69,8 @@ instance : CoeFun (Model) (λ M => Formula ℕ → 𝒫 M.𝓧) := ⟨truthset @[simp, grind =] lemma truthset_or : M (φ ⋎ ψ) = ⟨M φ ∪ M ψ, M.𝓧_closed_union⟩ := rfl @[simp, grind =] lemma truthset_imp : M (φ 🡒 ψ) = ⟨{ w | (M φ, M ψ) ∈ M.NB w }, M.𝓧_closed_imp⟩ := rfl @[simp, grind .] lemma truthset_top : (M ⊤).1 = Set.univ := by simp [truthset, M.NB_spec]; -@[simp, grind =] lemma truthset_neg : M (∼φ) = ⟨{ w | (M φ, ∅) ∈ M.NB w }, M.𝓧_closed_imp⟩ := by grind; -@[simp, grind =] lemma truthset_iff : M (φ 🡘 ψ) = ⟨{ w | (M φ, M ψ) ∈ M.NB w ∧ (M ψ, M φ) ∈ M.NB w }, @M.𝓧_closed_inter (M (φ 🡒 ψ)) (M (ψ 🡒 φ))⟩ := by grind; +@[simp, grind =] lemma truthset_neg : M (∼φ) = ⟨{ w | (M φ, ∅) ∈ M.NB w }, M.𝓧_closed_imp⟩ := rfl +@[simp, grind =] lemma truthset_iff : M (φ 🡘 ψ) = ⟨{ w | (M φ, M ψ) ∈ M.NB w ∧ (M ψ, M φ) ∈ M.NB w }, @M.𝓧_closed_inter (M (φ 🡒 ψ)) (M (ψ 🡒 φ))⟩ := rfl end Model diff --git a/Foundation/Propositional/Neighborhood/NB/Hilbert/Basic.lean b/Foundation/Propositional/Neighborhood/NB/Hilbert/Basic.lean index ae696bb8f..eb3af5606 100644 --- a/Foundation/Propositional/Neighborhood/NB/Hilbert/Basic.lean +++ b/Foundation/Propositional/Neighborhood/NB/Hilbert/Basic.lean @@ -26,7 +26,7 @@ lemma soundness_frameclass (hV : C ⊧* H) : H ⊢ φ → C ⊧ φ := by | axm hi => apply hV.models <;> assumption; | _ => grind; -instance instFrameClassSound (hV : C ⊧* H) : Sound H C := ⟨fun {_} => soundness_frameclass hV⟩ +def instFrameClassSound (hV : C ⊧* H) : Sound H C := ⟨fun {_} => soundness_frameclass hV⟩ lemma consistent_of_sound_frameclass (C : NBNeighborhood.FrameClass) (hC : Set.Nonempty C) [sound : Sound H C] : Entailment.Consistent H := by apply Entailment.Consistent.of_unprovable (φ := ⊥); @@ -58,7 +58,7 @@ lemma soundness_modelclass (hV : C ⊧* H) : H ⊢ φ → C ⊧ φ := by | axm hi => apply hV.models <;> assumption; | _ => grind -instance instModelClassSound (hV : C ⊧* H) : Sound H C := ⟨fun {_} => soundness_modelclass hV⟩ +def instModelClassSound (hV : C ⊧* H) : Sound H C := ⟨fun {_} => soundness_modelclass hV⟩ lemma consistent_of_sound_modelclass (C : NBNeighborhood.ModelClass) (hC : Set.Nonempty C) [sound : Sound H C] : Entailment.Consistent H := by apply Entailment.Consistent.of_unprovable (φ := ⊥); diff --git a/Foundation/Propositional/Neighborhood/NB/Hilbert/WF.lean b/Foundation/Propositional/Neighborhood/NB/Hilbert/WF.lean index 55472dc2d..dde6ef2f5 100644 --- a/Foundation/Propositional/Neighborhood/NB/Hilbert/WF.lean +++ b/Foundation/Propositional/Neighborhood/NB/Hilbert/WF.lean @@ -122,9 +122,9 @@ lemma unprovable_axiomD : HilbertWF.WF ⊬ Axioms.D #0 #1 #2 := by apply not_or.mpr; constructor; . dsimp; - grind; + simp_all [Set.subset_def]; . simpa; - grind; + simp [Set.ext_iff]; lemma unprovable_AxiomI : HilbertWF.WF ⊬ Axioms.I #0 #1 #2 := by apply Sound.not_provable_of_countermodel (𝓜 := NBNeighborhood.FrameClass.WF); diff --git a/Foundation/Semantics/CoherenceSpace/StableFunction.lean b/Foundation/Semantics/CoherenceSpace/StableFunction.lean index 1ab93abfe..aaaa300d6 100644 --- a/Foundation/Semantics/CoherenceSpace/StableFunction.lean +++ b/Foundation/Semantics/CoherenceSpace/StableFunction.lean @@ -39,7 +39,7 @@ variable {α β γ δ : Type*} [CoherenceSpace α] [CoherenceSpace β] [Coherenc instance : FunLike (α →ₛ β) (Point α) (Point β) where coe := toFun - coe_injective' _ _ := StableFunction.ext + coe_injective _ _ := StableFunction.ext lemma monotone {f : α →ₛ β} {a b : Point α} : a ≤ b → f a ≤ f b := f.monotone' diff --git a/Foundation/Syntax/Predicate/Language.lean b/Foundation/Syntax/Predicate/Language.lean index ddc29c238..756993ae3 100644 --- a/Foundation/Syntax/Predicate/Language.lean +++ b/Foundation/Syntax/Predicate/Language.lean @@ -154,7 +154,7 @@ instance (k) : Encodable (oRing.Func k) where instance Func1IsEmpty : IsEmpty (oRing.Func 1) := ⟨by rintro ⟨⟩⟩ -instance FuncGe3IsEmpty : ∀ k ≥ 3, IsEmpty (oRing.Func k) +lemma FuncGe3IsEmpty : ∀ k ≥ 3, IsEmpty (oRing.Func k) | 0 => by simp | 1 => by simp [show ¬3 ≤ 1 from of_decide_eq_false rfl] | 2 => by simp [show ¬3 ≤ 2 from of_decide_eq_false rfl] diff --git a/Foundation/Syntax/Predicate/Rew.lean b/Foundation/Syntax/Predicate/Rew.lean index b2e299c75..5ae29f8de 100644 --- a/Foundation/Syntax/Predicate/Rew.lean +++ b/Foundation/Syntax/Predicate/Rew.lean @@ -38,9 +38,9 @@ variable (ω : Rew L ξ₁ n₁ ξ₂ n₂) instance : FunLike (Rew L ξ₁ n₁ ξ₂ n₂) (Semiterm L ξ₁ n₁) (Semiterm L ξ₂ n₂) where coe := fun f => f.toFun - coe_injective' := fun f g h => by rcases f; rcases g; simpa using h + coe_injective := fun f g h => by rcases f; rcases g; simpa using h -instance : CoeFun (Rew L ξ₁ n₁ ξ₂ n₂) (fun _ => Semiterm L ξ₁ n₁ → Semiterm L ξ₂ n₂) := DFunLike.hasCoeToFun +instance : CoeFun (Rew L ξ₁ n₁ ξ₂ n₂) (fun _ => Semiterm L ξ₁ n₁ → Semiterm L ξ₂ n₂) := DFunLike.toCoeFun @[simp] protected lemma func {k} (f : L.Func k) (v : Fin k → Semiterm L ξ₁ n₁) : ω (func f v) = func f (ω ∘ v) := ω.func'' f v @@ -169,7 +169,7 @@ lemma map_inj {b : Fin n₁ → Fin n₂} {e : ξ₁ → ξ₂} (hb : Function.I have : f = g := by simp [Rew.func] at h; simp_all rcases this have : v = w := by - have : (fun i ↦ (map b e) (v i)) = (fun i ↦ (map b e) (w i)) := by simpa [Rew.func] using h + have : (fun i ↦ (map b e) (v i)) = (fun i ↦ (map b e) (w i)) := by simpa [Rew.func, Function.comp_def] using h funext i; exact map_inj hb he (congrFun this i) simp_all @@ -624,7 +624,7 @@ lemma fixitr_succ (m) : induction m · simp [*] case succ m ih => - simpa [ih] using comp_app fix (fixitr (L := L) n m) #x + rw [fixitr_succ, comp_app, ih]; simp [Fin.castSucc_castAdd] lemma fixitr_fvar (n m) (x : ℕ) : fixitr n m (&x : SyntacticSemiterm L n) = if h : x < m then #(Fin.natAdd n ⟨x, h⟩) else &(x - m) := by diff --git a/Foundation/Vorspiel/Arithmetic.lean b/Foundation/Vorspiel/Arithmetic.lean index 1be048f32..e0daf38e9 100644 --- a/Foundation/Vorspiel/Arithmetic.lean +++ b/Foundation/Vorspiel/Arithmetic.lean @@ -2,6 +2,7 @@ module public import Foundation.Vorspiel.List.Basic public import Mathlib.Computability.Halting +public import Mathlib.Computability.PartrecBasis public import Mathlib.Logic.Godel.GodelBetaFunction @[expose] public section @@ -163,7 +164,7 @@ lemma comp₁ (f : ℕ →. ℕ) (hf : @ArithPart₁ 1 fun v => f (v.get 0)) {n lemma comp₂ (f : ℕ → ℕ →. ℕ) (hf : @ArithPart₁ 2 fun v => f (v.get 0) (v.get 1)) {n g h} (hg : @Arithmetic₁ n g) (hh : @Arithmetic₁ n h) : @ArithPart₁ n fun v => f (g v) (h v) := - (hf.comp ![g, h] (fun i => i.cases hg (fun i => by simpa using hh))).of_eq + (hf.comp ![g, h] (fun i => i.cases hg (fun i => by simp only [Matrix.cons_val_succ, Matrix.cons_val_fin_one]; exact hh))).of_eq (by intro i have : (fun j ↦ (![↑g, h] : Fin 2 → List.Vector ℕ n →. ℕ) j i) = (fun j => pure (![g i, h i] j)) := by funext j; cases j using Fin.cases <;> simp @@ -224,7 +225,7 @@ lemma comp₁ (f : ℕ → ℕ) (hf : @Arithmetic₁ 1 fun v => f (v.get 0)) {n lemma comp₂ (f : ℕ → ℕ → ℕ) (hf : @Arithmetic₁ 2 fun v => f (v.get 0) (v.get 1)) {n g h} (hg : @Arithmetic₁ n g) (hh : @Arithmetic₁ n h) : @Arithmetic₁ n fun v => f (g v) (h v) := - (hf.comp ![g, h] (fun i => i.cases hg (fun i => by simpa using hh))).of_eq (by simp) + (hf.comp ![g, h] (fun i => i.cases hg (fun i => by simp only [Matrix.cons_val_succ, Matrix.cons_val_fin_one]; exact hh))).of_eq (by simp) lemma succ {n} (i : Fin n) : Arithmetic₁ (fun v => v.get i + 1) := (add 0 1).comp₂ _ (proj i) one diff --git a/Foundation/Vorspiel/Finset/Basic.lean b/Foundation/Vorspiel/Finset/Basic.lean index 10a0af15f..354aec68c 100644 --- a/Foundation/Vorspiel/Finset/Basic.lean +++ b/Foundation/Vorspiel/Finset/Basic.lean @@ -66,7 +66,7 @@ lemma erase_union [DecidableEq α] {a : α} {s t : Finset α} : @[simp] lemma sup_univ_equiv {α α'} [DecidableEq α] [Fintype α] [Fintype α'] [SemilatticeSup β] [OrderBot β] (f : α → β) (e : α' ≃ α) : Finset.sup Finset.univ (fun i => f (e i)) = Finset.sup Finset.univ f := by - simpa [Function.comp] using Eq.symm <| Finset.sup_image Finset.univ e f + simpa [Function.comp] using! Eq.symm <| Finset.sup_image Finset.univ e f lemma sup_univ_cast {α : Type _} [SemilatticeSup α] [OrderBot α] {n} (f : Fin n → α) (n') {h : n' = n} : Finset.sup Finset.univ (fun (i : Fin n') => f (i.cast h)) = Finset.sup Finset.univ f := by rcases h with rfl; simp diff --git a/Foundation/Vorspiel/List/Basic.lean b/Foundation/Vorspiel/List/Basic.lean index 63558eef5..98b206346 100644 --- a/Foundation/Vorspiel/List/Basic.lean +++ b/Foundation/Vorspiel/List/Basic.lean @@ -7,6 +7,12 @@ public import Foundation.Vorspiel.Matrix @[expose] public section +/-- Compatibility shim: mathlib v4.31 removed the named `Finset.toSet` that used to back the +`Finset → Set` coercion (the coercion is now an inline lambda). Re-introduce the name as a +reducible alias for the coercion so existing `.toSet` call-sites keep elaborating and the +`Finset.coe_*` simp lemmas continue to fire through it. -/ +@[reducible] def _root_.Finset.toSet {α : Type*} (s : Finset α) : Set α := (s : Set α) + namespace List variable {l : List α} @@ -75,7 +81,7 @@ lemma sup_ofFn (f : Fin n → α) : (ofFn f).sup = Finset.sup Finset.univ f := b · have h₁ : (Finset.univ : Finset (Fin (n + 1))) = insert 0 ((Finset.univ : Finset (Fin n)).image Fin.succ) := by ext i; simp have h₂ : Finset.sup Finset.univ (fun i ↦ f (Fin.succ i)) = Finset.sup {0}ᶜ f := by - simpa [Function.comp] using Eq.symm <| Finset.sup_image (Finset.univ : Finset (Fin n)) Fin.succ f + simpa [Function.comp] using! Eq.symm <| Finset.sup_image (Finset.univ : Finset (Fin n)) Fin.succ f calc (ofFn f).sup = (f 0 ⊔ Finset.univ.sup fun i : Fin _ ↦ f i.succ) := by simp [ih] _ = f 0 ⊔ Finset.sup {0}ᶜ f := by rw [h₂] diff --git a/Foundation/Vorspiel/Nat/Matrix.lean b/Foundation/Vorspiel/Nat/Matrix.lean index 0d4846d29..a65fedaae 100644 --- a/Foundation/Vorspiel/Nat/Matrix.lean +++ b/Foundation/Vorspiel/Nat/Matrix.lean @@ -22,7 +22,7 @@ variable {n : ℕ} suffices v 0 :> v ∘ Fin.succ = v by simp only [vecToNat, foldr_succ, natToVec, unpair_pair, Option.map_eq_some_iff] use vecTail v - simpa using ih (vecTail v) + simpa using! ih (vecTail v) exact funext (fun i ↦ i.cases (by simp) (by simp)) lemma lt_of_eq_natToVec {e : ℕ} {v : Fin n → ℕ} (h : e.natToVec n = some v) (i : Fin n) : v i < e := by diff --git a/Foundation/Vorspiel/Order/Dense.lean b/Foundation/Vorspiel/Order/Dense.lean index 1c6f34311..6052560b5 100644 --- a/Foundation/Vorspiel/Order/Dense.lean +++ b/Foundation/Vorspiel/Order/Dense.lean @@ -18,7 +18,7 @@ lemma monotone_of_succ_monotone {r : ℕ → ℕ → Prop} (rfx : Reflexive r) ( induction d case zero => simp [rfx n] case succ d ih => - simpa using tr.trans _ _ _ ih (succ (n + d)) + simpa using! tr.trans _ _ _ ih (succ (n + d)) end Nat @@ -115,7 +115,7 @@ namespace DenseSet instance : SetLike (DenseSet α) α where coe s := s.set - coe_injective' s t e := by ext; simp_all + coe_injective s t e := by ext; simp_all noncomputable def choose (d : DenseSet α) (a : α) : α := (d.is_dense a).choose diff --git a/Foundation/Vorspiel/Quotient.lean b/Foundation/Vorspiel/Quotient.lean index 6c61bd0db..deb72832b 100644 --- a/Foundation/Vorspiel/Quotient.lean +++ b/Foundation/Vorspiel/Quotient.lean @@ -30,7 +30,7 @@ def liftVec : ∀ {n} (f : (Fin n → α) → β), lemma liftVec_mk {n} (f : (Fin n → α) → β) (h) (v : Fin n → α) : liftVec f h (Quotient.mk s ∘ v) = f v := by induction' n with n ih <;> simp [liftVec, empty_eq] - simpa using ih (fun v' => f (vecHead v :> v')) + simpa using! ih (fun v' => f (vecHead v :> v')) (fun v₁ v₂ hv => h (vecHead v :> v₁) (vecHead v :> v₂) (Fin.cases (refl _) hv)) (vecTail v) @[simp] lemma liftVec_mk₁ (f : (Fin 1 → α) → β) (h) (a : α) : diff --git a/lake-manifest.json b/lake-manifest.json index 85e2d961d..fcdffcaf5 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -1,31 +1,31 @@ -{"version": "1.1.0", +{"version": "1.2.0", "packagesDir": ".lake/packages", "packages": [{"url": "https://github.com/leanprover-community/mathlib4", "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "1a37cd3c8e618022c5e78dee604c75c3c946a681", + "rev": "fabf563a7c95a166b8d7b6efca11c8b4dc9d911f", "name": "mathlib", "manifestFile": "lake-manifest.json", - "inputRev": "master", + "inputRev": "v4.31.0", "inherited": false, "configFile": "lakefile.lean"}, {"url": "https://github.com/leanprover/doc-gen4", "type": "git", "subDir": null, "scope": "leanprover", - "rev": "fbfa185b60c17f8efb9c78863ccf3cf873b6721b", + "rev": "0bc516c1b9db83658d6475c40d9b1ed71219b921", "name": "«doc-gen4»", "manifestFile": "lake-manifest.json", - "inputRev": "main", + "inputRev": "v4.31.0", "inherited": false, "configFile": "lakefile.lean"}, {"url": "https://github.com/leanprover-community/plausible", "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "83e90935a17ca19ebe4b7893c7f7066e266f50d3", + "rev": "63045536fe95024e6c18fc7b48e03f506701c5bc", "name": "plausible", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -45,7 +45,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "48d5698bc464786347c1b0d859b18f938420f060", + "rev": "5c7542ed018c78194f1e2b903eaf6a792b74c03d", "name": "importGraph", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -55,7 +55,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "00fe208b8e1364736cca3a9b9601c4fe865856af", + "rev": "24b0d9dc081c5423f8eec7e866c441e5184f29d9", "name": "proofwidgets", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -65,7 +65,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "7152850e7b216a0d409701617721b6e469d34bf6", + "rev": "e3cb2f741431ce31bf73549fb52316a57368b06f", "name": "aesop", "manifestFile": "lake-manifest.json", "inputRev": "master", @@ -75,7 +75,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "707efb56d0696634e9e965523a1bbe9ac6ce141d", + "rev": "f46324995fca5f0483b742e4eb4daec7f4ee50d2", "name": "Qq", "manifestFile": "lake-manifest.json", "inputRev": "master", @@ -85,37 +85,37 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "756e3321fd3b02a85ffda19fef789916223e578c", + "rev": "fa08db58b30eb033edcdab331bba000827f9f785", "name": "batteries", "manifestFile": "lake-manifest.json", "inputRev": "main", "inherited": true, "configFile": "lakefile.toml"}, - {"url": "https://github.com/leanprover/lean4-cli", + {"url": "https://github.com/leanprover/leansqlite", "type": "git", "subDir": null, - "scope": "leanprover", - "rev": "7802da01beb530bf051ab657443f9cd9bc3e1a29", - "name": "Cli", + "scope": "", + "rev": "0be4df908d1a8e75b58961041e2b4973692623df", + "name": "leansqlite", "manifestFile": "lake-manifest.json", - "inputRev": "v4.29.0", + "inputRev": "main", "inherited": true, - "configFile": "lakefile.toml"}, - {"url": "https://github.com/kim-em/leansqlite", + "configFile": "lakefile.lean"}, + {"url": "https://github.com/leanprover/lean4-cli", "type": "git", "subDir": null, - "scope": "", - "rev": "d14544c72b593af6a66131bc34cdab16bf7c0940", - "name": "leansqlite", + "scope": "leanprover", + "rev": "92564e5770e4d09f2d86dfbf8ada1e9c715b384c", + "name": "Cli", "manifestFile": "lake-manifest.json", - "inputRev": "suppress-reducibility-warning", + "inputRev": "v4.31.0", "inherited": true, - "configFile": "lakefile.lean"}, + "configFile": "lakefile.toml"}, {"url": "https://github.com/fgdorais/lean4-unicode-basic", "type": "git", "subDir": null, "scope": "", - "rev": "629254926fb54ef83d582bd41a0b9eb72b934015", + "rev": "a2e430a4c9d3ad24078b8581fe0162fc5b0c9a6c", "name": "UnicodeBasic", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -142,4 +142,5 @@ "inherited": true, "configFile": "lakefile.lean"}], "name": "Foundation", - "lakeDir": ".lake"} + "lakeDir": ".lake", + "fixedToolchain": false} diff --git a/lakefile.toml b/lakefile.toml index 3a0fc4bcc..39df8ae44 100644 --- a/lakefile.toml +++ b/lakefile.toml @@ -14,7 +14,9 @@ name = "Foundation" [[require]] scope = "leanprover" name = "doc-gen4" +rev = "v4.31.0" [[require]] scope = "leanprover-community" name = "mathlib" +rev = "v4.31.0" diff --git a/lean-toolchain b/lean-toolchain index d324cad1f..133a3f7d6 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:v4.29.0 \ No newline at end of file +leanprover/lean4:v4.31.0 \ No newline at end of file