From 4575799f8ee8eb27a18c0fa62bfe87e44541c588 Mon Sep 17 00:00:00 2001 From: Kyle Miller Date: Thu, 31 Jul 2025 14:28:59 -0700 Subject: [PATCH] chore: library style cleanup (#9654) This PR cleans up the style of the library in anticipation of a future PR that requires strict indentation for tactic sequences. --- src/Init/Data/Array/Lemmas.lean | 12 +- src/Init/Data/Array/Mem.lean | 4 +- src/Init/Data/BitVec/Lemmas.lean | 18 +- src/Init/Data/Int/Compare.lean | 10 +- src/Init/Data/Int/Linear.lean | 104 +++++------ .../Lemmas/Combinators/Monadic/FilterMap.lean | 2 +- .../Iterators/Lemmas/Consumers/Collect.lean | 4 +- .../Data/Iterators/Lemmas/Consumers/Loop.lean | 6 +- .../Lemmas/Consumers/Monadic/Collect.lean | 6 +- .../Lemmas/Consumers/Monadic/Loop.lean | 4 +- src/Init/Data/List/Erase.lean | 2 +- src/Init/Data/List/FinRange.lean | 2 +- src/Init/Data/List/Lemmas.lean | 2 +- src/Init/Data/List/Nat/TakeDrop.lean | 8 +- src/Init/Data/List/Zip.lean | 2 +- src/Init/Data/Nat/Bitwise/Lemmas.lean | 17 +- src/Init/Data/Nat/Compare.lean | 10 +- src/Init/Data/Nat/Lemmas.lean | 5 +- src/Init/Data/Nat/Log2.lean | 2 +- src/Init/Data/Range/Polymorphic/Lemmas.lean | 2 +- src/Init/Data/SInt/Lemmas.lean | 10 +- src/Init/Data/UInt/Lemmas.lean | 4 +- src/Init/Data/Vector/Lemmas.lean | 4 +- src/Init/Grind/Module/Envelope.lean | 63 +++---- src/Init/Grind/Ring/Envelope.lean | 122 ++++++------- src/Init/Grind/Ring/Field.lean | 6 +- src/Init/Grind/Ring/OfSemiring.lean | 40 ++--- src/Init/Grind/Ring/Poly.lean | 12 +- src/Init/GrindInstances/Ring/Fin.lean | 4 +- .../DHashMap/Internal/AssocList/Lemmas.lean | 26 +-- src/Std/Data/DHashMap/Internal/Model.lean | 8 +- src/Std/Data/DHashMap/Internal/WF.lean | 80 ++++----- src/Std/Data/DHashMap/Lemmas.lean | 4 +- src/Std/Data/DTreeMap/Internal/Balanced.lean | 4 +- src/Std/Data/DTreeMap/Internal/Balancing.lean | 6 +- .../Data/DTreeMap/Internal/Operations.lean | 24 +-- src/Std/Data/DTreeMap/Internal/WF/Lemmas.lean | 4 +- src/Std/Data/Internal/List/Associative.lean | 162 +++++++++--------- .../Iterators/Lemmas/Combinators/Drop.lean | 2 +- .../Lemmas/Combinators/DropWhile.lean | 2 +- .../Iterators/Lemmas/Combinators/Take.lean | 2 +- .../Lemmas/Consumers/Monadic/Collect.lean | 2 +- src/Std/Do/SPred/Laws.lean | 2 +- src/Std/Sat/AIG/Basic.lean | 4 +- src/Std/Sat/AIG/CNF.lean | 12 +- src/Std/Sat/AIG/CachedLemmas.lean | 10 +- src/Std/Sat/AIG/LawfulOperator.lean | 6 +- src/Std/Sat/AIG/Lemmas.lean | 24 +-- src/Std/Sat/AIG/RefVecOperator/Fold.lean | 2 +- src/Std/Sat/AIG/RefVecOperator/Map.lean | 2 +- src/Std/Sat/AIG/Relabel.lean | 6 +- src/Std/Sat/AIG/RelabelNat.lean | 16 +- .../BVDecide/Bitblast/BVExpr/Basic.lean | 2 +- .../Bitblast/BVExpr/Circuit/Impl/Expr.lean | 18 +- .../Bitblast/BVExpr/Circuit/Lemmas/Expr.lean | 14 +- .../BVExpr/Circuit/Lemmas/Operations/Add.lean | 2 +- .../BVExpr/Circuit/Lemmas/Operations/Clz.lean | 64 +++---- .../BVExpr/Circuit/Lemmas/Operations/Mul.lean | 16 +- .../Circuit/Lemmas/Operations/ShiftLeft.lean | 12 +- .../Circuit/Lemmas/Operations/ShiftRight.lean | 22 +-- .../Circuit/Lemmas/Operations/Udiv.lean | 12 +- .../Circuit/Lemmas/Operations/Umod.lean | 8 +- .../Circuit/Lemmas/Operations/ZeroExtend.lean | 4 +- .../Bitblast/BVExpr/Circuit/Lemmas/Pred.lean | 2 +- .../Bitblast/BVExpr/Circuit/Lemmas/Var.lean | 2 +- .../BVDecide/LRAT/Internal/Convert.lean | 2 +- .../BVDecide/LRAT/Internal/Entails.lean | 4 +- .../LRAT/Internal/Formula/Lemmas.lean | 56 +++--- .../LRAT/Internal/Formula/RatAddResult.lean | 4 +- .../LRAT/Internal/Formula/RatAddSound.lean | 30 ++-- .../LRAT/Internal/Formula/RupAddResult.lean | 86 +++++----- .../LRAT/Internal/Formula/RupAddSound.lean | 88 +++++----- tests/lean/grind/experiments/bitvec.lean | 6 +- tests/lean/grind/experiments/list.lean | 2 +- tests/lean/run/1017.lean | 6 +- tests/lean/run/1337.lean | 6 +- tests/lean/run/1711.lean | 20 +-- tests/lean/run/1841.lean | 6 +- tests/lean/run/andCasesOnBug.lean | 3 +- tests/lean/run/as_aux_lemma.lean | 15 +- tests/lean/run/doLogicTests.lean | 2 - tests/lean/run/grind_bitvec2.lean | 10 +- tests/lean/run/issue2982.lean | 2 +- tests/lean/run/nomatch_regression.lean | 24 +-- 84 files changed, 698 insertions(+), 749 deletions(-) diff --git a/src/Init/Data/Array/Lemmas.lean b/src/Init/Data/Array/Lemmas.lean index f572ecad40..2ed9bc44da 100644 --- a/src/Init/Data/Array/Lemmas.lean +++ b/src/Init/Data/Array/Lemmas.lean @@ -3312,11 +3312,11 @@ theorem foldl_induction let rec go {i j b} (h₁ : j ≤ as.size) (h₂ : as.size ≤ i + j) (H : motive j b) : (motive as.size) (foldlM.loop (m := Id) f as as.size (Nat.le_refl _) i j b) := by unfold foldlM.loop; split - · next hj => + next hj => split · cases Nat.not_le_of_gt (by simp [hj]) h₂ · exact go hj (by rwa [Nat.succ_add] at h₂) (hf ⟨j, hj⟩ b H) - · next hj => exact Nat.le_antisymm h₁ (Nat.ge_of_not_lt hj) ▸ H + next hj => exact Nat.le_antisymm h₁ (Nat.ge_of_not_lt hj) ▸ H simpa [foldl, foldlM] using go (Nat.zero_le _) (Nat.le_refl _) h0 theorem foldr_induction @@ -3326,13 +3326,13 @@ theorem foldr_induction let rec go {i b} (hi : i ≤ as.size) (H : motive i b) : (motive 0) (foldrM.fold (m := Id) f as 0 i hi b) := by unfold foldrM.fold; simp; split - · next hi => exact (hi ▸ H) - · next hi => + next hi => exact (hi ▸ H) + next hi => split; {simp at hi} - · next i hi' => + next i hi' => exact go _ (hf ⟨i, hi'⟩ b H) simp [foldr, foldrM]; split; {exact go _ h0} - · next h => exact (Nat.eq_zero_of_not_pos h ▸ h0) + next h => exact (Nat.eq_zero_of_not_pos h ▸ h0) @[congr] theorem foldl_congr {as bs : Array α} (h₀ : as = bs) {f g : β → α → β} (h₁ : f = g) diff --git a/src/Init/Data/Array/Mem.lean b/src/Init/Data/Array/Mem.lean index 736a8558be..b961aa8ce8 100644 --- a/src/Init/Data/Array/Mem.lean +++ b/src/Init/Data/Array/Mem.lean @@ -18,11 +18,11 @@ set_option linter.indexVariables true -- Enforce naming conventions for index va namespace Array theorem sizeOf_lt_of_mem [SizeOf α] {as : Array α} (h : a ∈ as) : sizeOf a < sizeOf as := by - cases as with | _ as => + cases as with | _ as exact Nat.lt_trans (List.sizeOf_lt_of_mem h.val) (by simp +arith) theorem sizeOf_get [SizeOf α] (as : Array α) (i : Nat) (h : i < as.size) : sizeOf as[i] < sizeOf as := by - cases as with | _ as => + cases as with | _ as simpa using Nat.lt_trans (List.sizeOf_get _ ⟨i, h⟩) (by simp +arith) @[simp] theorem sizeOf_getElem [SizeOf α] (as : Array α) (i : Nat) (h : i < as.size) : diff --git a/src/Init/Data/BitVec/Lemmas.lean b/src/Init/Data/BitVec/Lemmas.lean index a1b953e0bd..dc6425d3aa 100644 --- a/src/Init/Data/BitVec/Lemmas.lean +++ b/src/Init/Data/BitVec/Lemmas.lean @@ -702,7 +702,7 @@ theorem eq_zero_or_eq_one (a : BitVec 1) : a = 0#1 ∨ a = 1#1 := by have acases : a = 0 ∨ a = 1 := by omega rcases acases with ⟨rfl | rfl⟩ · simp - · case inr h => + case inr h => subst h simp @@ -1393,7 +1393,7 @@ theorem or_eq_zero_iff {x y : BitVec w} : (x ||| y) = 0#w ↔ x = 0#w ∧ y = 0# · intro h constructor all_goals - · ext i ih + ext i ih have := BitVec.eq_of_getElem_eq_iff.mp h i ih simp only [getElem_or, getElem_zero, Bool.or_eq_false_iff] at this simp [this] @@ -1493,7 +1493,7 @@ theorem and_eq_allOnes_iff {x y : BitVec w} : · intro h constructor all_goals - · ext i ih + ext i ih have := BitVec.eq_of_getElem_eq_iff.mp h i ih simp only [getElem_and, getElem_allOnes, Bool.and_eq_true] at this simp [this] @@ -4419,8 +4419,8 @@ theorem neg_one_ediv_toInt_eq {w : Nat} {y : BitVec w} : rcases w with _|_|w · simp [of_length_zero] · cases eq_zero_or_eq_one y - · case _ h => simp [h] - · case _ h => simp [h] + case _ h => simp [h] + case _ h => simp [h] · by_cases 0 < y.toInt · simp [Int.sign_eq_one_of_pos (a := y.toInt) (by omega), Int.neg_one_ediv] omega @@ -5766,16 +5766,16 @@ theorem clzAuxRec_eq_clzAuxRec_of_le (x : BitVec w) (h : w - 1 ≤ n) : let k := n - (w - 1) rw [show n = (w - 1) + k by omega] induction k - · case zero => simp - · case succ k ihk => + case zero => simp + case succ k ihk => simp [show w - 1 + (k + 1) = (w - 1 + k) + 1 by omega, clzAuxRec_succ, ihk, show x.getLsbD (w - 1 + k + 1) = false by simp only [show w ≤ w - 1 + k + 1 by omega, getLsbD_of_ge]] theorem clzAuxRec_eq_clzAuxRec_of_getLsbD_false {x : BitVec w} (h : ∀ i, n < i → x.getLsbD i = false) : x.clzAuxRec n = x.clzAuxRec (n + k) := by induction k - · case zero => simp - · case succ k ihk => + case zero => simp + case succ k ihk => simp only [show n + (k + 1) = (n + k) + 1 by omega, clzAuxRec_succ] by_cases hxn : x.getLsbD (n + k + 1) · have : ¬ ∀ (i : Nat), n < i → x.getLsbD i = false := by diff --git a/src/Init/Data/Int/Compare.lean b/src/Init/Data/Int/Compare.lean index 08710b9f70..f412213f1c 100644 --- a/src/Init/Data/Int/Compare.lean +++ b/src/Init/Data/Int/Compare.lean @@ -27,7 +27,7 @@ theorem compare_eq_ite_lt (a b : Int) : simp only [compare, compareOfLessAndEq] split · rfl - · next h => + next h => match Int.lt_or_eq_of_le (Int.not_lt.1 h) with | .inl h => simp [h, Int.ne_of_gt h] | .inr rfl => simp @@ -36,11 +36,11 @@ theorem compare_eq_ite_le (a b : Int) : compare a b = if a ≤ b then if b ≤ a then .eq else .lt else .gt := by rw [compare_eq_ite_lt] split - · next hlt => simp [Int.le_of_lt hlt, Int.not_le.2 hlt] - · next hge => + next hlt => simp [Int.le_of_lt hlt, Int.not_le.2 hlt] + next hge => split - · next hgt => simp [Int.not_le.2 hgt] - · next hle => simp [Int.not_lt.1 hge, Int.not_lt.1 hle] + next hgt => simp [Int.not_le.2 hgt] + next hle => simp [Int.not_lt.1 hge, Int.not_lt.1 hle] protected theorem compare_swap (a b : Int) : (compare a b).swap = compare b a := by simp only [compare_eq_ite_le]; (repeat' split) <;> try rfl diff --git a/src/Init/Data/Int/Linear.lean b/src/Init/Data/Int/Linear.lean index 0bcc590ed0..971ad781c4 100644 --- a/src/Init/Data/Int/Linear.lean +++ b/src/Init/Data/Int/Linear.lean @@ -747,7 +747,7 @@ def dvd_elim_cert (k₁ : Int) (p₁ : Poly) (k₂ : Int) (p₂ : Poly) : Bool : theorem dvd_elim (ctx : Context) (k₁ : Int) (p₁ : Poly) (k₂ : Int) (p₂ : Poly) : dvd_elim_cert k₁ p₁ k₂ p₂ → k₁ ∣ p₁.denote' ctx → k₂ ∣ p₂.denote' ctx := by rcases p₁ <;> simp [dvd_elim_cert] - next a _ p => + rename_i a _ p intro _ _; subst k₂ p₂ rw [Int.add_comm] apply dvd_gcd_of_dvd @@ -815,7 +815,7 @@ theorem dvd_solve_combine (ctx : Context) (d₁ : Int) (p₁ : Poly) (d₂ : Int : dvd_solve_combine_cert d₁ p₁ d₂ p₂ d p g α β → d₁ ∣ p₁.denote' ctx → d₂ ∣ p₂.denote' ctx → d ∣ p.denote' ctx := by simp [dvd_solve_combine_cert] split <;> simp - next a₁ x₁ p₁ a₂ x₂ p₂ => + rename_i a₁ x₁ p₁ a₂ x₂ p₂ intro _ hg hd hp; subst x₁ p simp intro h₁ h₂ @@ -836,7 +836,7 @@ theorem dvd_solve_elim (ctx : Context) (d₁ : Int) (p₁ : Poly) (d₂ : Int) ( : dvd_solve_elim_cert d₁ p₁ d₂ p₂ d p → d₁ ∣ p₁.denote' ctx → d₂ ∣ p₂.denote' ctx → d ∣ p.denote' ctx := by simp [dvd_solve_elim_cert] split <;> simp - next a₁ x₁ p₁ a₂ x₂ p₂ => + rename_i a₁ x₁ p₁ a₂ x₂ p₂ intro _ hd _; subst x₁ p; simp [Int.neg_mul] intro h₁ h₂ rw [Int.add_comm] at h₁ h₂ @@ -1290,17 +1290,17 @@ theorem cooper_dvd_left (ctx : Context) (p₁ p₂ p₃ : Poly) (d : Int) (n : N → p₂.denote' ctx ≤ 0 → d ∣ p₃.denote' ctx → OrOver n (cooper_dvd_left_split ctx p₁ p₂ p₃ d) := by - unfold cooper_dvd_left_split - cases p₁ <;> cases p₂ <;> cases p₃ <;> simp [cooper_dvd_left_cert, Poly.tail, -Poly.denote'_eq_denote] - next a x p b y q c z s => - intro _ _; subst y z - intro ha hb hd - intro; subst n - simp only [Poly.denote'_add, Poly.leadCoeff] - intro h₁ h₂ h₃ - simp only [denote'_mul_combine_mul_addConst_eq] - simp only [denote'_addConst_eq] - exact cooper_dvd_left_core ha hb hd h₁ h₂ h₃ + unfold cooper_dvd_left_split + cases p₁ <;> cases p₂ <;> cases p₃ <;> simp [cooper_dvd_left_cert, Poly.tail, -Poly.denote'_eq_denote] + rename_i a x p b y q c z s + intro _ _; subst y z + intro ha hb hd + intro; subst n + simp only [Poly.denote'_add, Poly.leadCoeff] + intro h₁ h₂ h₃ + simp only [denote'_mul_combine_mul_addConst_eq] + simp only [denote'_addConst_eq] + exact cooper_dvd_left_core ha hb hd h₁ h₂ h₃ @[expose] def cooper_dvd_left_split_ineq_cert (p₁ p₂ : Poly) (k : Int) (b : Int) (p' : Poly) : Bool := @@ -1376,18 +1376,18 @@ theorem cooper_left (ctx : Context) (p₁ p₂ : Poly) (n : Nat) → p₁.denote' ctx ≤ 0 → p₂.denote' ctx ≤ 0 → OrOver n (cooper_left_split ctx p₁ p₂) := by - unfold cooper_left_split - cases p₁ <;> cases p₂ <;> simp [cooper_left_cert, Poly.tail, -Poly.denote'_eq_denote] - next a x p b y q => - intro; subst y - intro ha hb - intro; subst n - simp only [Poly.denote'_add, Poly.leadCoeff] - intro h₁ h₂ - have := cooper_left_core ha hb h₁ h₂ - simp only [denote'_mul_combine_mul_addConst_eq] - simp only [denote'_addConst_eq] - assumption + unfold cooper_left_split + cases p₁ <;> cases p₂ <;> simp [cooper_left_cert, Poly.tail, -Poly.denote'_eq_denote] + rename_i a x p b y q + intro; subst y + intro ha hb + intro; subst n + simp only [Poly.denote'_add, Poly.leadCoeff] + intro h₁ h₂ + have := cooper_left_core ha hb h₁ h₂ + simp only [denote'_mul_combine_mul_addConst_eq] + simp only [denote'_addConst_eq] + assumption @[expose] def cooper_left_split_ineq_cert (p₁ p₂ : Poly) (k : Int) (b : Int) (p' : Poly) : Bool := @@ -1465,18 +1465,18 @@ theorem cooper_dvd_right (ctx : Context) (p₁ p₂ p₃ : Poly) (d : Int) (n : → p₂.denote' ctx ≤ 0 → d ∣ p₃.denote' ctx → OrOver n (cooper_dvd_right_split ctx p₁ p₂ p₃ d) := by - unfold cooper_dvd_right_split - cases p₁ <;> cases p₂ <;> cases p₃ <;> simp [cooper_dvd_right_cert, Poly.tail, -Poly.denote'_eq_denote] - next a x p b y q c z s => - intro _ _; subst y z - intro ha hb hd - intro; subst n - simp only [Poly.denote'_add, Poly.leadCoeff] - intro h₁ h₂ h₃ - have := cooper_dvd_right_core ha hb hd h₁ h₂ h₃ - simp only [denote'_mul_combine_mul_addConst_eq] - simp only [denote'_addConst_eq] - exact cooper_dvd_right_core ha hb hd h₁ h₂ h₃ + unfold cooper_dvd_right_split + cases p₁ <;> cases p₂ <;> cases p₃ <;> simp [cooper_dvd_right_cert, Poly.tail, -Poly.denote'_eq_denote] + rename_i a x p b y q c z s + intro _ _; subst y z + intro ha hb hd + intro; subst n + simp only [Poly.denote'_add, Poly.leadCoeff] + intro h₁ h₂ h₃ + have := cooper_dvd_right_core ha hb hd h₁ h₂ h₃ + simp only [denote'_mul_combine_mul_addConst_eq] + simp only [denote'_addConst_eq] + exact cooper_dvd_right_core ha hb hd h₁ h₂ h₃ @[expose] def cooper_dvd_right_split_ineq_cert (p₁ p₂ : Poly) (k : Int) (a : Int) (p' : Poly) : Bool := @@ -1551,18 +1551,18 @@ theorem cooper_right (ctx : Context) (p₁ p₂ : Poly) (n : Nat) → p₁.denote' ctx ≤ 0 → p₂.denote' ctx ≤ 0 → OrOver n (cooper_right_split ctx p₁ p₂) := by - unfold cooper_right_split - cases p₁ <;> cases p₂ <;> simp [cooper_right_cert, Poly.tail, -Poly.denote'_eq_denote] - next a x p b y q => - intro; subst y - intro ha hb - intro; subst n - simp only [Poly.denote'_add, Poly.leadCoeff] - intro h₁ h₂ - have := cooper_right_core ha hb h₁ h₂ - simp only [denote'_mul_combine_mul_addConst_eq] - simp only [denote'_addConst_eq] - assumption + unfold cooper_right_split + cases p₁ <;> cases p₂ <;> simp [cooper_right_cert, Poly.tail, -Poly.denote'_eq_denote] + rename_i a x p b y q + intro; subst y + intro ha hb + intro; subst n + simp only [Poly.denote'_add, Poly.leadCoeff] + intro h₁ h₂ + have := cooper_right_core ha hb h₁ h₂ + simp only [denote'_mul_combine_mul_addConst_eq] + simp only [denote'_addConst_eq] + assumption @[expose] def cooper_right_split_ineq_cert (p₁ p₂ : Poly) (k : Int) (a : Int) (p' : Poly) : Bool := @@ -1685,11 +1685,11 @@ theorem cooper_unsat (ctx : Context) (p₁ p₂ p₃ : Poly) (d : Int) (α β : p₁.denote' ctx ≤ 0 → p₂.denote' ctx ≤ 0 → d ∣ p₃.denote' ctx → False := by unfold cooper_unsat_cert <;> cases p₁ <;> cases p₂ <;> cases p₃ <;> simp only [Poly.casesOnAdd, Bool.false_eq_true, Poly.denote'_add, false_implies] - next k₁ x p₁ k₂ y p₂ c z p₃ => + rename_i k₁ x p₁ k₂ y p₂ c z p₃ cases p₁ <;> cases p₂ <;> cases p₃ <;> simp only [Poly.casesOnNum, Int.reduceNeg, Bool.and_eq_true, beq_iff_eq, decide_eq_true_eq, and_imp, Bool.false_eq_true, mul_def, add_def, false_implies, Poly.denote] - next a b e => + rename_i a b e intro _ _ _ _; subst k₁ k₂ y z intro h₁ h₃ h₆; generalize Var.denote ctx x = x' intro h₄ h₅ h₂ diff --git a/src/Init/Data/Iterators/Lemmas/Combinators/Monadic/FilterMap.lean b/src/Init/Data/Iterators/Lemmas/Combinators/Monadic/FilterMap.lean index 8d18a55228..e63f23593b 100644 --- a/src/Init/Data/Iterators/Lemmas/Combinators/Monadic/FilterMap.lean +++ b/src/Init/Data/Iterators/Lemmas/Combinators/Monadic/FilterMap.lean @@ -251,7 +251,7 @@ instance {α β γ : Type w} {m : Type w → Type w'} {n : Type w → Type w''} simp only [LawfulIteratorCollect.toArrayMapped_eq] simp only [IteratorCollect.toArrayMapped] rw [LawfulIteratorCollect.toArrayMapped_eq] - induction it using IterM.inductSteps with | step it ih_yield ih_skip => + induction it using IterM.inductSteps with | step it ih_yield ih_skip rw [IterM.DefaultConsumers.toArrayMapped_eq_match_step] rw [IterM.DefaultConsumers.toArrayMapped_eq_match_step] simp only [bind_assoc] diff --git a/src/Init/Data/Iterators/Lemmas/Consumers/Collect.lean b/src/Init/Data/Iterators/Lemmas/Consumers/Collect.lean index 85031b05c1..c7369f57bd 100644 --- a/src/Init/Data/Iterators/Lemmas/Consumers/Collect.lean +++ b/src/Init/Data/Iterators/Lemmas/Consumers/Collect.lean @@ -97,7 +97,7 @@ theorem Iter.getElem?_toList_eq_atIdxSlow? {α β} [Iterator α Id β] [Finite α Id] [IteratorCollect α Id Id] [LawfulIteratorCollect α Id Id] {it : Iter (α := α) β} {k : Nat} : it.toList[k]? = it.atIdxSlow? k := by - induction it using Iter.inductSteps generalizing k with | step it ihy ihs => + induction it using Iter.inductSteps generalizing k with | step it ihy ihs rw [toList_eq_match_step, atIdxSlow?] obtain ⟨step, h⟩ := it.step cases step @@ -117,7 +117,7 @@ theorem Iter.isPlausibleIndirectOutput_of_mem_toList [Iterator α Id β] [Finite α Id] [IteratorCollect α Id Id] [LawfulIteratorCollect α Id Id] {it : Iter (α := α) β} {b : β} : b ∈ it.toList → it.IsPlausibleIndirectOutput b := by - induction it using Iter.inductSteps with | step it ihy ihs => + induction it using Iter.inductSteps with | step it ihy ihs rw [toList_eq_match_step] cases it.step using PlausibleIterStep.casesOn case yield it' out h => diff --git a/src/Init/Data/Iterators/Lemmas/Consumers/Loop.lean b/src/Init/Data/Iterators/Lemmas/Consumers/Loop.lean index 81b9699dc1..0be561a3bd 100644 --- a/src/Init/Data/Iterators/Lemmas/Consumers/Loop.lean +++ b/src/Init/Data/Iterators/Lemmas/Consumers/Loop.lean @@ -143,7 +143,7 @@ theorem Iter.mem_toList_iff_isPlausibleIndirectOutput {α β} [Iterator α Id β [LawfulIteratorCollect α Id Id] [LawfulDeterministicIterator α Id] {it : Iter (α := α) β} {out : β} : out ∈ it.toList ↔ it.IsPlausibleIndirectOutput out := by - induction it using Iter.inductSteps with | step it ihy ihs => + induction it using Iter.inductSteps with | step it ihy ihs rw [toList_eq_match_step] constructor · intro h @@ -194,7 +194,7 @@ theorem Iter.forIn'_toList {α β : Type w} [Iterator α Id β] {f : (out : β) → _ → γ → m (ForInStep γ)} : letI : ForIn' m (Iter (α := α) β) β _ := Iter.instForIn' ForIn'.forIn' it.toList init f = ForIn'.forIn' it init (fun out h acc => f out (Iter.mem_toList_iff_isPlausibleIndirectOutput.mpr h) acc) := by - induction it using Iter.inductSteps generalizing init with case step it ihy ihs => + induction it using Iter.inductSteps generalizing init with | step it ihy ihs have := it.toList_eq_match_step generalize hs : it.step = step at this rw [forIn'_toList.aux this] @@ -239,7 +239,7 @@ theorem Iter.forIn_toList {α β : Type w} [Iterator α Id β] {f : β → γ → m (ForInStep γ)} : ForIn.forIn it.toList init f = ForIn.forIn it init f := by rw [List.forIn_eq_foldlM] - induction it using Iter.inductSteps generalizing init with case step it ihy ihs => + induction it using Iter.inductSteps generalizing init with | step it ihy ihs rw [forIn_eq_match_step, Iter.toList_eq_match_step] simp only [map_eq_pure_bind] generalize it.step = step diff --git a/src/Init/Data/Iterators/Lemmas/Consumers/Monadic/Collect.lean b/src/Init/Data/Iterators/Lemmas/Consumers/Monadic/Collect.lean index 92fe39179f..87680df70c 100644 --- a/src/Init/Data/Iterators/Lemmas/Consumers/Monadic/Collect.lean +++ b/src/Init/Data/Iterators/Lemmas/Consumers/Monadic/Collect.lean @@ -21,8 +21,7 @@ theorem IterM.DefaultConsumers.toArrayMapped.go.aux₁ [Monad n] [LawfulMonad n] [Finite α m] {b : γ} {bs : Array γ} : IterM.DefaultConsumers.toArrayMapped.go lift f it (#[b] ++ bs) (m := m) = (#[b] ++ ·) <$> IterM.DefaultConsumers.toArrayMapped.go lift f it bs (m := m) := by - induction it, bs using IterM.DefaultConsumers.toArrayMapped.go.induct - next it bs ih₁ ih₂ => + induction it, bs using IterM.DefaultConsumers.toArrayMapped.go.induct with | _ it bs ih₁ ih₂ rw [go, map_eq_pure_bind, go, bind_assoc] apply bind_congr intro step @@ -93,8 +92,7 @@ theorem IterM.toList_eq_match_step [Monad m] [LawfulMonad m] [Iterator α m β] theorem IterM.toListRev.go.aux₁ [Monad m] [LawfulMonad m] [Iterator α m β] [Finite α m] {it : IterM (α := α) m β} {b : β} {bs : List β} : IterM.toListRev.go it (bs ++ [b]) = (· ++ [b]) <$> IterM.toListRev.go it bs:= by - induction it, bs using IterM.toListRev.go.induct - next it bs ih₁ ih₂ => + induction it, bs using IterM.toListRev.go.induct with | _ it bs ih₁ ih₂ rw [go, go, map_eq_pure_bind, bind_assoc] apply bind_congr intro step diff --git a/src/Init/Data/Iterators/Lemmas/Consumers/Monadic/Loop.lean b/src/Init/Data/Iterators/Lemmas/Consumers/Monadic/Loop.lean index 9a31db0671..597f7cf373 100644 --- a/src/Init/Data/Iterators/Lemmas/Consumers/Monadic/Loop.lean +++ b/src/Init/Data/Iterators/Lemmas/Consumers/Monadic/Loop.lean @@ -208,7 +208,7 @@ theorem IterM.toList_eq_fold {α β : Type w} {m : Type w → Type w'} [Iterator it.fold (init := l') (fun l out => l ++ [out]) by specialize h [] simpa using h - induction it using IterM.inductSteps with | step it ihy ihs => + induction it using IterM.inductSteps with | step it ihy ihs intro l' rw [IterM.toList_eq_match_step, IterM.fold_eq_match_step] simp only [map_eq_pure_bind, bind_assoc] @@ -253,7 +253,7 @@ theorem IterM.drain_eq_map_toList {α β : Type w} {m : Type w → Type w'} [Ite [IteratorCollect α m m] [LawfulIteratorCollect α m m] {it : IterM (α := α) m β} : it.drain = (fun _ => .unit) <$> it.toList := by - induction it using IterM.inductSteps with | step it ihy ihs => + induction it using IterM.inductSteps with | step it ihy ihs rw [IterM.drain_eq_match_step, IterM.toList_eq_match_step] simp only [map_eq_pure_bind, bind_assoc] apply bind_congr diff --git a/src/Init/Data/List/Erase.lean b/src/Init/Data/List/Erase.lean index f55fc86144..516dbe12fa 100644 --- a/src/Init/Data/List/Erase.lean +++ b/src/Init/Data/List/Erase.lean @@ -337,7 +337,7 @@ theorem erase_of_not_mem [LawfulBEq α] {a : α} : ∀ {l : List α}, a ∉ l theorem erase_eq_eraseP' (a : α) (l : List α) : l.erase a = l.eraseP (· == a) := by induction l · simp - · next b t ih => + next b t ih => rw [erase_cons, eraseP_cons, ih] if h : b == a then simp [h] else simp [h] diff --git a/src/Init/Data/List/FinRange.lean b/src/Init/Data/List/FinRange.lean index 028b024f1c..97a56a8168 100644 --- a/src/Init/Data/List/FinRange.lean +++ b/src/Init/Data/List/FinRange.lean @@ -46,7 +46,7 @@ theorem finRange_succ_last {n} : getElem_map, Fin.castSucc_mk, getElem_singleton] split · rfl - · next h => exact Fin.eq_last_of_not_lt h + next h => exact Fin.eq_last_of_not_lt h @[grind _=_] theorem finRange_reverse {n} : (finRange n).reverse = (finRange n).map Fin.rev := by diff --git a/src/Init/Data/List/Lemmas.lean b/src/Init/Data/List/Lemmas.lean index eff0046e15..a04524b274 100644 --- a/src/Init/Data/List/Lemmas.lean +++ b/src/Init/Data/List/Lemmas.lean @@ -2152,7 +2152,7 @@ theorem flatMap_eq_foldl {f : α → List β} {l : List α} : intro l' induction l generalizing l' · simp - · next ih => rw [flatMap_cons, ← append_assoc, ih, foldl_cons] + next ih => rw [flatMap_cons, ← append_assoc, ih, foldl_cons] /-! ### replicate -/ diff --git a/src/Init/Data/List/Nat/TakeDrop.lean b/src/Init/Data/List/Nat/TakeDrop.lean index c6537b8fc9..440b952232 100644 --- a/src/Init/Data/List/Nat/TakeDrop.lean +++ b/src/Init/Data/List/Nat/TakeDrop.lean @@ -61,8 +61,8 @@ theorem getElem?_take_eq_none {l : List α} {i j : Nat} (h : i ≤ j) : @[grind =] theorem getElem?_take {l : List α} {i j : Nat} : (l.take i)[j]? = if j < i then l[j]? else none := by split - · next h => exact getElem?_take_of_lt h - · next h => exact getElem?_take_eq_none (Nat.le_of_not_lt h) + next h => exact getElem?_take_of_lt h + next h => exact getElem?_take_eq_none (Nat.le_of_not_lt h) theorem head?_take {l : List α} {i : Nat} : (l.take i).head? = if i = 0 then none else l.head? := by @@ -114,7 +114,7 @@ theorem take_set_of_le {a : α} {i j : Nat} {l : List α} (h : j ≤ i) : List.ext_getElem? fun i => by rw [getElem?_take, getElem?_take] split - · next h' => rw [getElem?_set_ne (by omega)] + next h' => rw [getElem?_set_ne (by omega)] · rfl @[deprecated take_set_of_le (since := "2025-02-04")] @@ -384,7 +384,7 @@ theorem take_reverse {α} {xs : List α} {i : Nat} : by_cases h : i ≤ xs.length · induction xs generalizing i <;> simp only [reverse_cons, drop, reverse_nil, Nat.zero_sub, length, take_nil] - next hd tl xs_ih => + rename_i hd tl xs_ih cases Nat.lt_or_eq_of_le h with | inl h' => have h' := Nat.le_of_succ_le_succ h' diff --git a/src/Init/Data/List/Zip.lean b/src/Init/Data/List/Zip.lean index 85532273da..8c436b53cd 100644 --- a/src/Init/Data/List/Zip.lean +++ b/src/Init/Data/List/Zip.lean @@ -306,7 +306,7 @@ theorem of_mem_zip {a b} : ∀ {l₁ : List α} {l₂ : List β}, (a, b) ∈ zip cases h case head => simp case tail h => - · have := of_mem_zip h + have := of_mem_zip h exact ⟨Mem.tail _ this.1, Mem.tail _ this.2⟩ theorem map_fst_zip : diff --git a/src/Init/Data/Nat/Bitwise/Lemmas.lean b/src/Init/Data/Nat/Bitwise/Lemmas.lean index c46325e781..8abc41d929 100644 --- a/src/Init/Data/Nat/Bitwise/Lemmas.lean +++ b/src/Init/Data/Nat/Bitwise/Lemmas.lean @@ -78,8 +78,7 @@ noncomputable def div2Induction {motive : Nat → Sort u} simp only [HAnd.hAnd, AndOp.and, land] at andz simp only [HAnd.hAnd, AndOp.and, land] unfold bitwise - cases mod_two_eq_zero_or_one x with | _ p => - simp [xz, p, andz] + cases mod_two_eq_zero_or_one x with | _ p => simp [xz, p, andz] /-! ### testBit -/ @@ -182,9 +181,8 @@ theorem exists_testBit_ne_of_ne {x y : Nat} (p : x ≠ y) : ∃ i, testBit x i apply Exists.intro 0 simp only [testBit_zero] revert lsb_diff - cases mod_two_eq_zero_or_one x with | _ p => - cases mod_two_eq_zero_or_one y with | _ q => - simp [p,q] + cases mod_two_eq_zero_or_one x with + | _ p => cases mod_two_eq_zero_or_one y with | _ q => simp [p,q] @[deprecated exists_testBit_ne_of_ne (since := "2025-04-04")] abbrev ne_implies_bit_diff := @exists_testBit_ne_of_ne @@ -260,8 +258,7 @@ private theorem succ_mod_two : succ x % 2 = 1 - x % 2 := by private theorem testBit_succ_zero : testBit (x + 1) 0 = !(testBit x 0) := by simp only [testBit_eq_decide_div_mod_eq, Nat.pow_zero, Nat.div_one, succ_mod_two] - cases Nat.mod_two_eq_zero_or_one x with | _ p => - simp [p] + cases Nat.mod_two_eq_zero_or_one x with | _ p => simp [p] theorem testBit_two_pow_add_eq (x i : Nat) : testBit (2^i + x) i = !(testBit x i) := by simp only [testBit_eq_decide_div_mod_eq, add_div_left, Nat.two_pow_pos, succ_mod_two] @@ -277,8 +274,7 @@ theorem testBit_mul_two_pow_add_eq (a b i : Nat) : testBit_mul_two_pow_add_eq a, testBit_two_pow_add_eq, Nat.succ_mod_two] - cases mod_two_eq_zero_or_one a with - | _ p => simp [p] + cases mod_two_eq_zero_or_one a with | _ p => simp [p] theorem testBit_two_pow_add_gt {i j : Nat} (j_lt_i : j < i) (x : Nat) : testBit (2^i + x) j = testBit x j := by @@ -853,8 +849,7 @@ theorem shiftLeft_add_eq_or_of_lt {b : Nat} (b_lt : b < 2^i) (a : Nat) : /-! ### le -/ theorem le_of_testBit {n m : Nat} (h : ∀ i, n.testBit i = true → m.testBit i = true) : n ≤ m := by - induction n using div2Induction generalizing m - next n ih => + induction n using div2Induction generalizing m with | _ n ih have : n / 2 ≤ m / 2 := by rcases n with (_|n) · simp diff --git a/src/Init/Data/Nat/Compare.lean b/src/Init/Data/Nat/Compare.lean index 5a5e608783..85a97cd623 100644 --- a/src/Init/Data/Nat/Compare.lean +++ b/src/Init/Data/Nat/Compare.lean @@ -24,7 +24,7 @@ theorem compare_eq_ite_lt (a b : Nat) : simp only [compare, compareOfLessAndEq] split · rfl - · next h => + next h => match Nat.lt_or_eq_of_le (Nat.not_lt.1 h) with | .inl h => simp [h, Nat.ne_of_gt h] | .inr rfl => simp @@ -36,11 +36,11 @@ theorem compare_eq_ite_le (a b : Nat) : compare a b = if a ≤ b then if b ≤ a then .eq else .lt else .gt := by rw [compare_eq_ite_lt] split - · next hlt => simp [Nat.le_of_lt hlt, Nat.not_le.2 hlt] - · next hge => + next hlt => simp [Nat.le_of_lt hlt, Nat.not_le.2 hlt] + next hge => split - · next hgt => simp [Nat.not_le.2 hgt] - · next hle => simp [Nat.not_lt.1 hge, Nat.not_lt.1 hle] + next hgt => simp [Nat.not_le.2 hgt] + next hle => simp [Nat.not_lt.1 hge, Nat.not_lt.1 hle] @[deprecated compare_eq_ite_le (since := "2025-03_28")] def compare_def_le := compare_eq_ite_le diff --git a/src/Init/Data/Nat/Lemmas.lean b/src/Init/Data/Nat/Lemmas.lean index 5b5a38336d..52c44644ae 100644 --- a/src/Init/Data/Nat/Lemmas.lean +++ b/src/Init/Data/Nat/Lemmas.lean @@ -1145,8 +1145,7 @@ protected theorem pow_lt_pow_succ (h : 1 < a) : a ^ n < a ^ (n + 1) := by protected theorem pow_lt_pow_of_lt {a n m : Nat} (h : 1 < a) (w : n < m) : a ^ n < a ^ m := by have := Nat.exists_eq_add_of_lt w - cases this - case intro k p => + cases this with | intro k p rw [Nat.add_right_comm] at p subst p rw [Nat.pow_add, ← Nat.mul_one (a^n)] @@ -1561,7 +1560,7 @@ theorem mul_add_mod_of_lt {a b c : Nat} (h : c < b) : (a * b + c) % b = c := by @[simp] theorem mod_div_self (m n : Nat) : m % n / n = 0 := by cases n · exact (m % 0).div_zero - · case succ n => exact Nat.div_eq_of_lt (m.mod_lt n.succ_pos) + case succ n => exact Nat.div_eq_of_lt (m.mod_lt n.succ_pos) theorem mod_eq_iff {a b c : Nat} : a % b = c ↔ (b = 0 ∧ a = c) ∨ (c < b ∧ Exists fun k => a = b * k + c) := diff --git a/src/Init/Data/Nat/Log2.lean b/src/Init/Data/Nat/Log2.lean index da2f60c147..a0038099c0 100644 --- a/src/Init/Data/Nat/Log2.lean +++ b/src/Init/Data/Nat/Log2.lean @@ -42,7 +42,7 @@ decreasing_by exact log2_terminates _ ‹_› theorem log2_le_self (n : Nat) : Nat.log2 n ≤ n := by unfold Nat.log2; split - · next h => + next h => have := log2_le_self (n / 2) exact Nat.lt_of_le_of_lt this (Nat.div_lt_self (Nat.le_of_lt h) (by decide)) · apply Nat.zero_le diff --git a/src/Init/Data/Range/Polymorphic/Lemmas.lean b/src/Init/Data/Range/Polymorphic/Lemmas.lean index d5c90ee75b..748abc9c4b 100644 --- a/src/Init/Data/Range/Polymorphic/Lemmas.lean +++ b/src/Init/Data/Range/Polymorphic/Lemmas.lean @@ -115,7 +115,7 @@ theorem pairwise_toList_upwardEnumerableLt {sl su} [UpwardEnumerable α] r.toList.Pairwise (fun a b => UpwardEnumerable.LT a b) := by rw [Internal.toList_eq_toList_iter] generalize Internal.iter r = it - induction it using Iter.inductSteps with | step it ihy ihs => + induction it using Iter.inductSteps with | step it ihy ihs rw [RangeIterator.toList_eq_match] repeat' split <;> (try exact .nil; done) rename_i a _ _ diff --git a/src/Init/Data/SInt/Lemmas.lean b/src/Init/Data/SInt/Lemmas.lean index ff6f1e9d6c..cf55470e2d 100644 --- a/src/Init/Data/SInt/Lemmas.lean +++ b/src/Init/Data/SInt/Lemmas.lean @@ -1069,7 +1069,7 @@ theorem Int8.toNatClampNeg_ofIntTruncate_of_lt {n : Int} (h₁ : n < 2 ^ 7) : rw [ofIntTruncate] split · rw [dif_pos (by rw [toInt_maxValue]; omega), toNatClampNeg_ofIntLE] - · next h => + next h => rw [toNatClampNeg_minValue, eq_comm, Int.toNat_eq_zero] rw [toInt_minValue] at h omega @@ -1078,7 +1078,7 @@ theorem Int16.toNatClampNeg_ofIntTruncate_of_lt {n : Int} (h₁ : n < 2 ^ 15) : rw [ofIntTruncate] split · rw [dif_pos (by rw [toInt_maxValue]; omega), toNatClampNeg_ofIntLE] - · next h => + next h => rw [toNatClampNeg_minValue, eq_comm, Int.toNat_eq_zero] rw [toInt_minValue] at h omega @@ -1087,7 +1087,7 @@ theorem Int32.toNatClampNeg_ofIntTruncate_of_lt {n : Int} (h₁ : n < 2 ^ 31) : rw [ofIntTruncate] split · rw [dif_pos (by rw [toInt_maxValue]; omega), toNatClampNeg_ofIntLE] - · next h => + next h => rw [toNatClampNeg_minValue, eq_comm, Int.toNat_eq_zero] rw [toInt_minValue] at h omega @@ -1096,7 +1096,7 @@ theorem Int64.toNatClampNeg_ofIntTruncate_of_lt {n : Int} (h₁ : n < 2 ^ 63) : rw [ofIntTruncate] split · rw [dif_pos (by rw [toInt_maxValue]; omega), toNatClampNeg_ofIntLE] - · next h => + next h => rw [toNatClampNeg_minValue, eq_comm, Int.toNat_eq_zero] rw [toInt_minValue] at h omega @@ -1105,7 +1105,7 @@ theorem ISize.toNatClampNeg_ofIntTruncate_of_lt_two_pow_numBits {n : Int} (h₁ rw [ofIntTruncate] split · rw [dif_pos (by rw [toInt_maxValue]; omega), toNatClampNeg_ofIntLE] - · next h => + next h => rw [toNatClampNeg_minValue, eq_comm, Int.toNat_eq_zero] rw [toInt_minValue] at h omega diff --git a/src/Init/Data/UInt/Lemmas.lean b/src/Init/Data/UInt/Lemmas.lean index ace65eeeb8..9ee08760b6 100644 --- a/src/Init/Data/UInt/Lemmas.lean +++ b/src/Init/Data/UInt/Lemmas.lean @@ -885,9 +885,9 @@ theorem USize.ofNatTruncate_eq_ofNat (n : Nat) (hn : n < USize.size) : apply USize.toNat.inj simp only [UInt32.toNat_toUSize, toNat_toUInt32, Nat.reducePow, USize.toNat_mod] cases USize.size_eq - · next h => rw [Nat.mod_eq_of_lt (h ▸ n.toNat_lt_size), USize.toNat_ofNat, + next h => rw [Nat.mod_eq_of_lt (h ▸ n.toNat_lt_size), USize.toNat_ofNat, ← USize.size_eq_two_pow, h, Nat.mod_self, Nat.mod_zero] - · next h => rw [USize.toNat_ofNat_of_lt]; simp_all + next h => rw [USize.toNat_ofNat_of_lt]; simp_all -- Note: we are currently missing the following four results for which there does not seem to -- be a good candidate for the RHS: diff --git a/src/Init/Data/Vector/Lemmas.lean b/src/Init/Data/Vector/Lemmas.lean index 776d7e24e1..deb7898913 100644 --- a/src/Init/Data/Vector/Lemmas.lean +++ b/src/Init/Data/Vector/Lemmas.lean @@ -1951,8 +1951,8 @@ set_option linter.listVariables false in /-- Two vectors of constant length vectors are equal iff their flattens coincide. -/ theorem eq_iff_flatten_eq {xss xss' : Vector (Vector α n) m} : xss = xss' ↔ xss.flatten = xss'.flatten := by - induction xss using vector₂_induction with | of xss h₁ h₂ => - induction xss' using vector₂_induction with | of xss' h₁' h₂' => + induction xss using vector₂_induction with | of xss h₁ h₂ + induction xss' using vector₂_induction with | of xss' h₁' h₂' simp only [eq_mk, flatten_mk, Array.map_map, Function.comp_apply, Array.map_subtype, Array.unattach_attach, Array.map_id_fun', id_eq] constructor diff --git a/src/Init/Grind/Module/Envelope.lean b/src/Init/Grind/Module/Envelope.lean index 3ef39336d4..869e203279 100644 --- a/src/Init/Grind/Module/Envelope.lean +++ b/src/Init/Grind/Module/Envelope.lean @@ -39,8 +39,7 @@ theorem r_sym {a b : α × α} : r α a b → r α b a := by cases a; cases b; simp [r]; intro h w; refine ⟨h, ?_⟩; simp [w, AddCommMonoid.add_comm] theorem r_trans {a b c : α × α} : r α a b → r α b c → r α a c := by - cases a; cases b; cases c; - next a₁ a₂ b₁ b₂ c₁ c₂ => + obtain ⟨a₁, a₂⟩ := a; obtain ⟨b₁, b₂⟩ := b; obtain ⟨c₁, c₂⟩ := c simp [r] intro k₁ h₁ k₂ h₂ refine ⟨(k₁ + k₂ + b₁ + b₂), ?_⟩ @@ -122,33 +121,29 @@ attribute [local simp] Q.mk (0, 0) theorem neg_add_cancel (a : Q α) : add (neg a) a = zero := by - induction a using Quot.ind - next a => - cases a; simp + obtain ⟨⟨_, _⟩⟩ := a + simp apply Quot.sound; simp; refine ⟨0, ?_⟩; ac_rfl theorem add_comm (a b : Q α) : add a b = add b a := by - induction a using Quot.ind - induction b using Quot.ind - next a b => - cases a; cases b; simp; apply Quot.sound; simp; refine ⟨0, ?_⟩; ac_rfl + obtain ⟨⟨_, _⟩⟩ := a + obtain ⟨⟨_, _⟩⟩ := b + simp; apply Quot.sound; simp; refine ⟨0, ?_⟩; ac_rfl theorem add_zero (a : Q α) : add a zero = a := by induction a using Quot.ind next a => cases a; simp theorem add_assoc (a b c : Q α) : add (add a b) c = add a (add b c) := by - induction a using Quot.ind - induction b using Quot.ind - induction c using Quot.ind - next a b c => - cases a; cases b; cases c; simp; apply Quot.sound; simp; refine ⟨0, ?_⟩; ac_rfl + obtain ⟨⟨_, _⟩⟩ := a + obtain ⟨⟨_, _⟩⟩ := b + obtain ⟨⟨_, _⟩⟩ := c + simp; apply Quot.sound; simp; refine ⟨0, ?_⟩; ac_rfl theorem sub_eq_add_neg (a b : Q α) : sub a b = add a (neg b) := by - induction a using Quot.ind - induction b using Quot.ind - next a b => - cases a; cases b; simp; apply Quot.sound; simp; refine ⟨0, ?_⟩; ac_rfl + obtain ⟨⟨_, _⟩⟩ := a + obtain ⟨⟨_, _⟩⟩ := b + simp; apply Quot.sound; simp; refine ⟨0, ?_⟩; ac_rfl theorem one_zsmul (a : Q α) : zsmul 1 a = a := by induction a using Quot.ind @@ -159,8 +154,7 @@ theorem zero_zsmul (a : Q α) : zsmul 0 a = zero := by next a => cases a; simp theorem add_zsmul (a b : Int) (c : Q α) : zsmul (a + b) c = add (zsmul a c) (zsmul b c) := by - induction c using Q.ind - next c => + induction c using Q.ind with | _ c rcases c with ⟨c₁, c₂⟩; simp by_cases hb : b < 0 · simp only [if_pos hb] @@ -203,8 +197,7 @@ theorem add_zsmul (a b : Int) (c : Q α) : zsmul (a + b) c = add (zsmul a c) (zs ac_rfl theorem zsmul_natCast_eq_nsmul (n : Nat) (a : Q α) : zsmul (n : Int) a = nsmul n a := by - induction a using Q.ind - next a => + induction a using Q.ind with | _ a rcases a with ⟨a₁, a₂⟩; simp; omega def ofNatModule : IntModule (Q α) := { @@ -264,11 +257,8 @@ instance [NatModule α] [AddRightCancel α] [NoNatZeroDivisors α] : NoNatZeroDi no_nat_zero_divisors := by intro k a b h₁ h₂ replace h₂ : k * a = k * b := h₂ - induction a using Quot.ind - induction b using Quot.ind - next a b => - rcases a with ⟨a₁, a₂⟩ - rcases b with ⟨b₁, b₂⟩ + obtain ⟨⟨a₁, a₂⟩⟩ := a + obtain ⟨⟨b₁, b₂⟩⟩ := b replace h₂ := Q.exact h₂ simp [r] at h₂ rcases h₂ with ⟨k', h₂⟩ @@ -299,17 +289,14 @@ instance [Preorder α] [OrderedAdd α] : LE (OfNatModule.Q α) where instance [Preorder α] [OrderedAdd α] : Preorder (OfNatModule.Q α) where le_refl a := by - induction a using Quot.ind - next a => - rcases a with ⟨a₁, a₂⟩ + obtain ⟨⟨a₁, a₂⟩⟩ := a change Q.mk _ ≤ Q.mk _ simp only [mk_le_mk] simp [AddCommMonoid.add_comm]; exact Preorder.le_refl (a₁ + a₂) le_trans {a b c} h₁ h₂ := by - induction a using Q.ind - induction b using Q.ind - induction c using Q.ind - next a b c => + induction a using Q.ind with | _ a + induction b using Q.ind with | _ b + induction c using Q.ind with | _ c rcases a with ⟨a₁, a₂⟩; rcases b with ⟨b₁, b₂⟩; rcases c with ⟨c₁, c₂⟩ simp only [mk_le_mk] at h₁ h₂ ⊢ rw [OrderedAdd.add_le_left_iff (b₁ + b₂)] @@ -341,11 +328,9 @@ theorem toQ_lt [Preorder α] [OrderedAdd α] {a b : α} : toQ a < toQ b ↔ a < instance [Preorder α] [OrderedAdd α] : OrderedAdd (OfNatModule.Q α) where add_le_left_iff := by intro a b c - induction a using Quot.ind - induction b using Quot.ind - induction c using Quot.ind - next a b c => - rcases a with ⟨a₁, a₂⟩; rcases b with ⟨b₁, b₂⟩; rcases c with ⟨c₁, c₂⟩ + obtain ⟨⟨a₁, a₂⟩⟩ := a + obtain ⟨⟨b₁, b₂⟩⟩ := b + obtain ⟨⟨c₁, c₂⟩⟩ := c change a₁ + b₂ ≤ a₂ + b₁ ↔ (a₁ + c₁) + _ ≤ _ have : a₁ + c₁ + (b₂ + c₂) = a₁ + b₂ + (c₁ + c₂) := by ac_rfl rw [this]; clear this diff --git a/src/Init/Grind/Ring/Envelope.lean b/src/Init/Grind/Ring/Envelope.lean index b614140dcd..524d5d62b5 100644 --- a/src/Init/Grind/Ring/Envelope.lean +++ b/src/Init/Grind/Ring/Envelope.lean @@ -43,8 +43,7 @@ theorem r_sym {a b : α × α} : r α a b → r α b a := by cases a; cases b; simp [r]; intro h w; refine ⟨h, ?_⟩; simp [w, Semiring.add_comm] theorem r_trans {a b c : α × α} : r α a b → r α b c → r α a c := by - cases a; cases b; cases c; - next a₁ a₂ b₁ b₂ c₁ c₂ => + obtain ⟨a₁, a₂⟩ := a; obtain ⟨b₁, b₂⟩ := b; obtain ⟨c₁, c₂⟩ := c simp [r] intro k₁ h₁ k₂ h₂ refine ⟨(k₁ + k₂ + b₁ + b₂), ?_⟩ @@ -145,33 +144,29 @@ attribute [local simp] Semiring.natCast_zero Semiring.natCast_one Semiring.mul_zero Semiring.zero_mul theorem neg_add_cancel (a : Q α) : add (neg a) a = natCast 0 := by - induction a using Quot.ind - next a => - cases a; simp + obtain ⟨⟨_, _⟩⟩ := a + simp apply Quot.sound; simp; refine ⟨0, ?_⟩; ac_rfl theorem add_comm (a b : Q α) : add a b = add b a := by - induction a using Quot.ind - induction b using Quot.ind - next a b => - cases a; cases b; simp; apply Quot.sound; simp; refine ⟨0, ?_⟩; ac_rfl + obtain ⟨⟨_, _⟩⟩ := a + obtain ⟨⟨_, _⟩⟩ := b + simp; apply Quot.sound; simp; refine ⟨0, ?_⟩; ac_rfl theorem add_zero (a : Q α) : add a (natCast 0) = a := by induction a using Quot.ind next a => cases a; simp theorem add_assoc (a b c : Q α) : add (add a b) c = add a (add b c) := by - induction a using Quot.ind - induction b using Quot.ind - induction c using Quot.ind - next a b c => - cases a; cases b; cases c; simp; apply Quot.sound; simp; refine ⟨0, ?_⟩; ac_rfl + obtain ⟨⟨_, _⟩⟩ := a + obtain ⟨⟨_, _⟩⟩ := b + obtain ⟨⟨_, _⟩⟩ := c + simp; apply Quot.sound; simp; refine ⟨0, ?_⟩; ac_rfl theorem sub_eq_add_neg (a b : Q α) : sub a b = add a (neg b) := by - induction a using Quot.ind - induction b using Quot.ind - next a b => - cases a; cases b; simp; apply Quot.sound; simp; refine ⟨0, ?_⟩; ac_rfl + obtain ⟨⟨_, _⟩⟩ := a + obtain ⟨⟨_, _⟩⟩ := b + simp; apply Quot.sound; simp; refine ⟨0, ?_⟩; ac_rfl theorem intCast_neg (i : Int) : intCast (α := α) (-i) = neg (intCast i) := by simp; split <;> split <;> simp @@ -188,43 +183,36 @@ theorem ofNat_succ (a : Nat) : natCast (α := α) (a + 1) = add (natCast a) (nat simp; apply Quot.sound; simp [Semiring.natCast_add] theorem mul_assoc (a b c : Q α) : mul (mul a b) c = mul a (mul b c) := by - induction a using Quot.ind - induction b using Quot.ind - induction c using Quot.ind - next a b c => - cases a; cases b; cases c; simp; apply Quot.sound + obtain ⟨⟨_, _⟩⟩ := a + obtain ⟨⟨_, _⟩⟩ := b + obtain ⟨⟨_, _⟩⟩ := c + simp; apply Quot.sound simp [Semiring.left_distrib, Semiring.right_distrib]; refine ⟨0, ?_⟩; ac_rfl theorem mul_one (a : Q α) : mul a (natCast 1) = a := by - induction a using Quot.ind - next a => cases a; simp +obtain ⟨⟨_, _⟩⟩ := a; simp theorem one_mul (a : Q α) : mul (natCast 1) a = a := by - induction a using Quot.ind - next a => cases a; simp + obtain ⟨⟨_, _⟩⟩ := a; simp theorem zero_mul (a : Q α) : mul (natCast 0) a = natCast 0 := by - induction a using Quot.ind - next a => cases a; simp + obtain ⟨⟨_, _⟩⟩ := a; simp theorem mul_zero (a : Q α) : mul a (natCast 0) = natCast 0 := by - induction a using Quot.ind - next a => cases a; simp + obtain ⟨⟨_, _⟩⟩ := a; simp theorem left_distrib (a b c : Q α) : mul a (add b c) = add (mul a b) (mul a c) := by - induction a using Quot.ind - induction b using Quot.ind - induction c using Quot.ind - next a b c => - cases a; cases b; cases c; simp; apply Quot.sound + obtain ⟨⟨_, _⟩⟩ := a + obtain ⟨⟨_, _⟩⟩ := b + obtain ⟨⟨_, _⟩⟩ := c + simp; apply Quot.sound simp [Semiring.left_distrib]; refine ⟨0, ?_⟩; ac_rfl theorem right_distrib (a b c : Q α) : mul (add a b) c = add (mul a c) (mul b c) := by - induction a using Quot.ind - induction b using Quot.ind - induction c using Quot.ind - next a b c => - cases a; cases b; cases c; simp; apply Quot.sound + obtain ⟨⟨_, _⟩⟩ := a + obtain ⟨⟨_, _⟩⟩ := b + obtain ⟨⟨_, _⟩⟩ := c + simp; apply Quot.sound simp [Semiring.right_distrib]; refine ⟨0, ?_⟩; ac_rfl def npow (a : Q α) (n : Nat) : Q α := @@ -243,9 +231,8 @@ def zsmul (i : Int) (a : Q α) : Q α := mul (intCast i) a theorem neg_zsmul (i : Int) (a : Q α) : zsmul (-i) a = neg (zsmul i a) := by - induction a using Quot.ind - next a => - cases a; simp [zsmul] + obtain ⟨⟨_, _⟩⟩ := a + simp [zsmul] split <;> rename_i h₁ · split <;> rename_i h₂ · omega @@ -340,11 +327,8 @@ instance [Semiring α] [AddRightCancel α] [NoNatZeroDivisors α] : NoNatZeroDiv no_nat_zero_divisors := by intro k a b h₁ h₂ replace h₂ : mul (natCast k) a = mul (natCast k) b := h₂ - induction a using Quot.ind - induction b using Quot.ind - next a b => - rcases a with ⟨a₁, a₂⟩ - rcases b with ⟨b₁, b₂⟩ + obtain ⟨⟨a₁, a₂⟩⟩ := a + obtain ⟨⟨b₁, b₂⟩⟩ := b simp [mul] at h₂ replace h₂ := Q.exact h₂ simp [r] at h₂ @@ -397,17 +381,14 @@ instance [Preorder α] [OrderedAdd α] : LE (OfSemiring.Q α) where instance [Preorder α] [OrderedAdd α] : Preorder (OfSemiring.Q α) where le_refl a := by - induction a using Quot.ind - next a => - rcases a with ⟨a₁, a₂⟩ + obtain ⟨⟨a₁, a₂⟩⟩ := a change Q.mk _ ≤ Q.mk _ simp only [mk_le_mk] simp [Semiring.add_comm]; exact Preorder.le_refl (a₁ + a₂) le_trans {a b c} h₁ h₂ := by - induction a using Q.ind - induction b using Q.ind - induction c using Q.ind - next a b c => + induction a using Q.ind with | _ a + induction b using Q.ind with | _ b + induction c using Q.ind with | _ c rcases a with ⟨a₁, a₂⟩; rcases b with ⟨b₁, b₂⟩; rcases c with ⟨c₁, c₂⟩ simp only [mk_le_mk] at h₁ h₂ ⊢ rw [OrderedAdd.add_le_left_iff (b₁ + b₂)] @@ -436,11 +417,9 @@ theorem toQ_lt [Preorder α] [OrderedAdd α] {a b : α} : toQ a < toQ b ↔ a < instance [Preorder α] [OrderedAdd α] : OrderedAdd (OfSemiring.Q α) where add_le_left_iff := by intro a b c - induction a using Quot.ind - induction b using Quot.ind - induction c using Quot.ind - next a b c => - rcases a with ⟨a₁, a₂⟩; rcases b with ⟨b₁, b₂⟩; rcases c with ⟨c₁, c₂⟩ + obtain ⟨⟨a₁, a₂⟩⟩ := a + obtain ⟨⟨b₁, b₂⟩⟩ := b + obtain ⟨⟨c₁, c₂⟩⟩ := c change a₁ + b₂ ≤ a₂ + b₁ ↔ (a₁ + c₁) + _ ≤ _ have : a₁ + c₁ + (b₂ + c₂) = a₁ + b₂ + (c₁ + c₂) := by ac_rfl rw [this]; clear this @@ -455,10 +434,9 @@ instance [Preorder α] [OrderedRing α] [ExistsAddOfLT α] : OrderedRing (OfSemi exact OrderedRing.zero_lt_one mul_lt_mul_of_pos_left := by intro a b c h₁ h₂ - induction a using Q.ind - induction b using Q.ind - induction c using Q.ind - next a b c => + induction a using Q.ind with | _ a + induction b using Q.ind with | _ b + induction c using Q.ind with | _ c rcases a with ⟨a₁, a₂⟩; rcases b with ⟨b₁, b₂⟩; rcases c with ⟨c₁, c₂⟩ simp at h₁ h₂ ⊢ obtain ⟨d, d_pos, rfl⟩ := ExistsAddOfLT.exists_add_of_le h₂ @@ -473,10 +451,9 @@ instance [Preorder α] [OrderedRing α] [ExistsAddOfLT α] : OrderedRing (OfSemi simpa [Semiring.left_distrib] using OrderedRing.mul_lt_mul_of_pos_left h₁ d_pos mul_lt_mul_of_pos_right := by intro a b c h₁ h₂ - induction a using Q.ind - induction b using Q.ind - induction c using Q.ind - next a b c => + induction a using Q.ind with | _ a + induction b using Q.ind with | _ b + induction c using Q.ind with | _ c rcases a with ⟨a₁, a₂⟩; rcases b with ⟨b₁, b₂⟩; rcases c with ⟨c₁, c₂⟩ simp at h₁ h₂ ⊢ obtain ⟨d, d_pos, rfl⟩ := ExistsAddOfLT.exists_add_of_le h₂ @@ -515,10 +492,9 @@ variable {α} attribute [local simp] OfSemiring.Q.mk OfSemiring.Q.liftOn₂ Semiring.add_zero theorem mul_comm (a b : OfSemiring.Q α) : OfSemiring.mul a b = OfSemiring.mul b a := by - induction a using Quot.ind - induction b using Quot.ind - next a b => - cases a; cases b; apply Quot.sound; refine ⟨0, ?_⟩; simp; ac_rfl + obtain ⟨⟨a₁, a₂⟩⟩ := a + obtain ⟨⟨b₁, b₂⟩⟩ := b + apply Quot.sound; refine ⟨0, ?_⟩; simp; ac_rfl def ofCommSemiring : CommRing (OfSemiring.Q α) := { OfSemiring.ofSemiring with diff --git a/src/Init/Grind/Ring/Field.lean b/src/Init/Grind/Ring/Field.lean index 98e500366d..88c144f0bf 100644 --- a/src/Init/Grind/Ring/Field.lean +++ b/src/Init/Grind/Ring/Field.lean @@ -95,9 +95,9 @@ theorem zero_eq_inv_iff {a : α} : 0 = a⁻¹ ↔ 0 = a := by rw [eq_comm, inv_eq_zero_iff, eq_comm] theorem of_mul_eq_zero {a b : α} : a*b = 0 → a = 0 ∨ b = 0 := by - cases (Classical.em (a = 0)); simp [*, Semiring.zero_mul] - cases (Classical.em (b = 0)); simp [*, Semiring.mul_zero] - next h₁ h₂ => + cases (Classical.em (a = 0)); · simp [*, Semiring.zero_mul] + cases (Classical.em (b = 0)); · simp [*, Semiring.mul_zero] + rename_i h₁ h₂ replace h₁ := Field.mul_inv_cancel h₁ replace h₂ := Field.mul_inv_cancel h₂ intro h diff --git a/src/Init/Grind/Ring/OfSemiring.lean b/src/Init/Grind/Ring/OfSemiring.lean index 6645fb478e..61edfbe0ec 100644 --- a/src/Init/Grind/Ring/OfSemiring.lean +++ b/src/Init/Grind/Ring/OfSemiring.lean @@ -141,9 +141,9 @@ theorem Poly.denoteS_insert {α} [CommSemiring α] (ctx : Context α) (k : Int) simp at h <;> simp [*, Mon.denote, denoteS_addConst, add_comm] next => fun_induction insert.go <;> simp_all +zetaDelta [denoteS] - next h₁ h₂ => - intro _ hn; cases hn - next a m p _ _ hk hn₁ hn₂ => + next a m p _ _ h₁ h₂ => + intro hk hn + cases hn; rename_i hn₁ hn₂ replace h₂ : k.toNat + a.toNat = 0 := by apply Int.ofNat_inj.mp rw [Int.natCast_add, Int.toNat_of_nonneg hn₁, @@ -154,8 +154,7 @@ theorem Poly.denoteS_insert {α} [CommSemiring α] (ctx : Context α) (k : Int) intro _ hn; cases hn rw [Int.toNat_add, natCast_add, right_distrib, add_assoc, Mon.eq_of_grevlex h₁] <;> assumption next ih => - intro hk hn; cases hn - next hn₁ hn₂ => + intro hk hn; cases hn; rename_i hn₁ hn₂ rw [ih hk hn₂, add_left_comm] theorem Poly.denoteS_concat {α} [CommSemiring α] (ctx : Context α) (p₁ p₂ : Poly) @@ -174,9 +173,8 @@ theorem Poly.denoteS_mulConst {α} [CommSemiring α] (ctx : Context α) (k : Int next => intro _ h₂; cases h₂ rw [Int.toNat_mul, natCast_mul] <;> assumption - next => - intro _ h₂; cases h₂ - next ih h₁ h₂ h₃ => + next ih => + intro h₁ h₂; cases h₂; rename_i h₂ h₃ rw [Int.toNat_mul, natCast_mul, left_distrib, mul_assoc, ih h₁ h₃] <;> assumption theorem Poly.denoteS_mulMon {α} [CommSemiring α] (ctx : Context α) (k : Int) (m : Mon) (p : Poly) @@ -196,9 +194,8 @@ theorem Poly.denoteS_mulMon {α} [CommSemiring α] (ctx : Context α) (k : Int) rw [Int.toNat_mul] simp [natCast_mul, CommSemiring.mul_comm, CommSemiring.mul_left_comm, mul_assoc] assumption; assumption - next => - intro h₁ h₂; cases h₂ - next ih h₂ h₃ => + next ih => + intro h₁ h₂; cases h₂; rename_i h₂ h₃ rw [Int.toNat_mul] simp [Mon.denote_mul, natCast_mul, left_distrib, CommSemiring.mul_left_comm, mul_assoc, ih h₁ h₃] assumption; assumption @@ -211,30 +208,29 @@ theorem Poly.denoteS_combine {α} [CommSemiring α] (ctx : Context α) (p₁ p case case2 => intros h₁ h₂; cases h₁; cases h₂; simp [denoteS, Int.toNat_add, natCast_add, *] case case3 => intro h₁ h₂; cases h₁; simp [denoteS, denoteS_addConst, add_comm, *] case case4 => intro h₁ h₂; cases h₂; simp [denoteS, denoteS_addConst, *] - case case5 k₁ _ _ k₂ _ _ hg _ h _ => + case case5 k₁ _ _ k₂ _ _ hg _ h ih => intro h₁ h₂ cases h₁; cases h₂ simp +zetaDelta at h - next ih h₁ h₂ h₃ h₄ => + rename_i h₁ h₂ h₃ h₄ simp [ih h₂ h₄, denoteS, Mon.eq_of_grevlex hg] replace h : k₂.toNat + k₁.toNat = 0 := by rw [← Int.toNat_add, Int.add_comm, h]; rfl; assumption; assumption rw [add_left_comm, ← add_assoc, ← add_assoc, ← right_distrib, ← natCast_add, h] simp - case case6 hg k h _ => + case case6 hg k h ih => intro h₁ h₂ cases h₁; cases h₂ simp +zetaDelta - next ih h₁ h₂ h₃ h₄ => simp [denoteS, Int.toNat_add, natCast_add, right_distrib, Mon.eq_of_grevlex hg, add_left_comm, add_assoc, *] - case case7 => + case case7 ih => intro h₁ h₂; cases h₁ - next ih _ h₁ => + rename_i h₁ simp [denoteS, ih h₁ h₂, add_left_comm, add_assoc] - case case8 => + case case8 ih => intro h₁ h₂; cases h₂ - next ih _ h₂ => + rename_i h₂ simp [denoteS, ih h₁ h₂, add_left_comm, add_assoc] theorem Poly.mulConst_NonnegCoeffs {p : Poly} {k : Int} : k ≥ 0 → p.NonnegCoeffs → (p.mulConst k).NonnegCoeffs := by @@ -301,7 +297,7 @@ theorem Poly.mul_go_NonnegCoeffs (p₁ p₂ acc : Poly) fun_induction mul.go next => intro h₁ h₂ h₃ - cases h₁; next h₁ => + cases h₁; rename_i h₁ have := mulConst_NonnegCoeffs h₁ h₂ apply combine_NonnegCoeffs <;> assumption next ih => @@ -329,11 +325,11 @@ theorem Poly.denoteS_mul_go {α} [CommSemiring α] (ctx : Context α) (p₁ p₂ : p₁.NonnegCoeffs → p₂.NonnegCoeffs → acc.NonnegCoeffs → (mul.go p₂ p₁ acc).denoteS ctx = acc.denoteS ctx + p₁.denoteS ctx * p₂.denoteS ctx := by fun_induction mul.go <;> intro h₁ h₂ h₃ next k => - cases h₁; next h₁ => + cases h₁; rename_i h₁ have := p₂.mulConst_NonnegCoeffs h₁ h₂ simp [denoteS, denoteS_combine, denoteS_mulConst, *] next acc a m p ih => - cases h₁; next h₁ h₁' => + cases h₁; rename_i h₁ h₁' have := p₂.mulMon_NonnegCoeffs m h₁ h₂ have := acc.combine_NonnegCoeffs h₃ this replace ih := ih h₁' h₂ this diff --git a/src/Init/Grind/Ring/Poly.lean b/src/Init/Grind/Ring/Poly.lean index 24991b74e5..c1104b15e9 100644 --- a/src/Init/Grind/Ring/Poly.lean +++ b/src/Init/Grind/Ring/Poly.lean @@ -105,7 +105,7 @@ protected noncomputable def Mon.beq' (m₁ : Mon) : Mon → Bool := @[simp] theorem Mon.beq'_eq (m₁ m₂ : Mon) : m₁.beq' m₂ = (m₁ = m₂) := by induction m₁ generalizing m₂ <;> cases m₂ <;> simp [Mon.beq'] - next pw₁ _ ih _ m₂ => + rename_i pw₁ _ ih _ m₂ intro; subst pw₁ simp [← ih m₂, ← Bool.and'_eq_and] rfl @@ -330,7 +330,7 @@ protected noncomputable def Poly.beq' (p₁ : Poly) : Poly → Bool := @[simp] theorem Poly.beq'_eq (p₁ p₂ : Poly) : p₁.beq' p₂ = (p₁ = p₂) := by induction p₁ generalizing p₂ <;> cases p₂ <;> simp [Poly.beq'] - next k₁ m₁ p₁ ih k₂ m₂ p₂ => + rename_i k₁ m₁ p₁ ih k₂ m₂ p₂ rw [← eq_iff_iff] intro _ _; subst k₁ m₁ simp [← ih p₂, ← Bool.and'_eq_and]; rfl @@ -339,13 +339,13 @@ instance : LawfulBEq Poly where eq_of_beq {a} := by induction a <;> intro b <;> cases b <;> simp_all! [BEq.beq] intro h₁ h₂ h₃ - next m₁ p₁ _ m₂ p₂ ih => + rename_i m₁ p₁ _ m₂ p₂ ih replace h₂ : m₁ == m₂ := h₂ simp [ih h₃, eq_of_beq h₂] rfl := by intro a induction a <;> simp! [BEq.beq] - next k m p ih => + rename_i k m p ih change m == m ∧ p == p simp [ih] @@ -842,7 +842,7 @@ theorem Power.denote_eq {α} [Semiring α] (ctx : Context α) (p : Power) theorem Mon.denote'_eq_denote {α} [Semiring α] (ctx : Context α) (m : Mon) : m.denote' ctx = m.denote ctx := by cases m <;> simp [denote', denote] - next pw m => + rename_i pw m generalize pw.denote ctx = acc fun_induction denote'.go next => simp [denote, Semiring.mul_one] @@ -1698,7 +1698,7 @@ def eq_gcd_cert (a b : Int) (p₁ p₂ p : Poly) : Bool := theorem eq_gcd {α} [CommRing α] (ctx : Context α) (a b : Int) (p₁ p₂ p : Poly) : eq_gcd_cert a b p₁ p₂ p → p₁.denote ctx = 0 → p₂.denote ctx = 0 → p.denote ctx = 0 := by simp [eq_gcd_cert]; cases p₁ <;> cases p₂ <;> cases p <;> simp [Poly.denote] - next n m g => + rename_i n m g apply gcd_eq_0 g n m a b @[expose] diff --git a/src/Init/GrindInstances/Ring/Fin.lean b/src/Init/GrindInstances/Ring/Fin.lean index 3c735c0217..578a2f51aa 100644 --- a/src/Init/GrindInstances/Ring/Fin.lean +++ b/src/Init/GrindInstances/Ring/Fin.lean @@ -68,8 +68,8 @@ theorem sub_eq_add_neg [NeZero n] (a b : Fin n) : a - b = a + -b := by cases a; cases b; simp [Fin.neg_def, Fin.sub_def, Fin.add_def, Nat.add_comm] private theorem neg_neg [NeZero n] (a : Fin n) : - - a = a := by - cases a; simp [Fin.neg_def] - next a h => cases a; simp; next a => + obtain ⟨a, h⟩ := a; simp [Fin.neg_def] + cases a; simp; next a => rw [Nat.self_sub_mod n (a+1)] have : NeZero (n - (a + 1)) := ⟨by omega⟩ rw [Nat.self_sub_mod, Nat.sub_sub_eq_min, Nat.min_eq_right (Nat.le_of_lt h)] diff --git a/src/Std/Data/DHashMap/Internal/AssocList/Lemmas.lean b/src/Std/Data/DHashMap/Internal/AssocList/Lemmas.lean index 4c8ba673ef..59339f99ce 100644 --- a/src/Std/Data/DHashMap/Internal/AssocList/Lemmas.lean +++ b/src/Std/Data/DHashMap/Internal/AssocList/Lemmas.lean @@ -48,7 +48,7 @@ theorem length_eq {l : AssocList α β} : l.length = l.toList.length := by suffices ∀ n, l.toList.foldl (fun d _ => d + 1) n = l.toList.length + n by simp induction l · simp - · next _ _ t ih => + next _ _ t ih => intro n simp [ih, Nat.add_assoc, Nat.add_comm n 1] @@ -72,14 +72,14 @@ theorem getCast_eq [BEq α] [LawfulBEq α] {l : AssocList α β} {a : α} {h} : l.getCast a h = getValueCast a l.toList (contains_eq.symm.trans h) := by induction l · simp [contains] at h - · next k v t ih => simp only [getCast, toList_cons, List.getValueCast_cons, ih] + next k v t ih => simp only [getCast, toList_cons, List.getValueCast_cons, ih] @[simp] theorem get_eq {β : Type v} [BEq α] {l : AssocList α (fun _ => β)} {a : α} {h} : l.get a h = getValue a l.toList (contains_eq.symm.trans h) := by induction l · simp [contains] at h - · next k v t ih => simp only [get, toList_cons, List.getValue_cons, ih] + next k v t ih => simp only [get, toList_cons, List.getValue_cons, ih] @[simp] theorem getCastD_eq [BEq α] [LawfulBEq α] {l : AssocList α β} {a : α} {fallback : β a} : @@ -127,7 +127,7 @@ theorem getKey_eq [BEq α] {l : AssocList α β} {a : α} {h} : l.getKey a h = List.getKey a l.toList (contains_eq.symm.trans h) := by induction l · simp [contains] at h - · next k v t ih => simp only [getKey, toList_cons, List.getKey_cons, ih] + next k v t ih => simp only [getKey, toList_cons, List.getKey_cons, ih] @[simp] theorem getKeyD_eq [BEq α] {l : AssocList α β} {a fallback : α} : @@ -148,14 +148,14 @@ theorem toList_replace [BEq α] {l : AssocList α β} {a : α} {b : β a} : (l.replace a b).toList = replaceEntry a b l.toList := by induction l · simp [replace] - · next k v t ih => cases h : k == a <;> simp_all [replace, List.replaceEntry_cons] + next k v t ih => cases h : k == a <;> simp_all [replace, List.replaceEntry_cons] @[simp] theorem toList_erase [BEq α] {l : AssocList α β} {a : α} : (l.erase a).toList = eraseKey a l.toList := by induction l · simp [erase] - · next k v t ih => cases h : k == a <;> simp_all [erase, List.eraseKey_cons] + next k v t ih => cases h : k == a <;> simp_all [erase, List.eraseKey_cons] theorem toList_filterMap {f : (a : α) → β a → Option (γ a)} {l : AssocList α β} : Perm (l.filterMap f).toList (l.toList.filterMap fun p => (f p.1 p.2).map (⟨p.1, ·⟩)) := by @@ -166,11 +166,11 @@ theorem toList_filterMap {f : (a : α) → β a → Option (γ a)} {l : AssocLis intros l l' induction l' generalizing l · simp [filterMap.go] - · next k v t ih => + next k v t ih => simp only [filterMap.go, toList_cons, List.filterMap_cons] split - · next h => exact (ih _).trans (by simp [h]) - · next h => + next h => exact (ih _).trans (by simp [h]) + next h => refine (ih _).trans ?_ simp only [toList_cons, List.cons_append] exact perm_middle.symm.trans (by simp [h]) @@ -184,7 +184,7 @@ theorem toList_map {f : (a : α) → β a → γ a} {l : AssocList α β} : intros l l' induction l' generalizing l · simp [map.go] - · next k v t ih => + next k v t ih => simp only [map.go, toList_cons, List.map_cons] refine (ih _).trans ?_ simpa using perm_middle.symm @@ -198,7 +198,7 @@ theorem toList_filter {f : (a : α) → β a → Bool} {l : AssocList α β} : intros l l' induction l' generalizing l · simp [filter.go] - · next k v t ih => + next k v t ih => simp only [filter.go, toList_cons, List.filter_cons, cond_eq_if] split · exact (ih _).trans (by simpa using perm_middle.symm) @@ -237,7 +237,7 @@ theorem modify_eq_alter [BEq α] [LawfulBEq α] {a : α} {f : β a → β a} {l modify a f l = alter a (·.map f) l := by induction l · rfl - · next ih => simp only [modify, beq_iff_eq, alter, Option.map_some, ih] + next ih => simp only [modify, beq_iff_eq, alter, Option.map_some, ih] namespace Const @@ -257,7 +257,7 @@ theorem modify_eq_alter [BEq α] [EquivBEq α] {a : α} {f : β → β} {l : Ass modify a f l = alter a (·.map f) l := by induction l · rfl - · next ih => simp only [modify, alter, Option.map_some, ih] + next ih => simp only [modify, alter, Option.map_some, ih] end Const diff --git a/src/Std/Data/DHashMap/Internal/Model.lean b/src/Std/Data/DHashMap/Internal/Model.lean index e16e3703b6..d8c9f6ba68 100644 --- a/src/Std/Data/DHashMap/Internal/Model.lean +++ b/src/Std/Data/DHashMap/Internal/Model.lean @@ -216,7 +216,7 @@ theorem toListModel_updateAllBuckets {m : Raw₀ α β} {f : AssocList α β → rintro l l' l'' h induction l generalizing l' l'' · simpa using h.symm - · next l t ih => + next l t ih => simp only [List.foldl_cons] apply ih exact hg.trans (Perm.append h hfg.symm) @@ -241,7 +241,7 @@ theorem uset [BEq α] [Hashable α] {m : Array (AssocList α β)} {i : USize} {h refine ⟨fun j hj => ?_⟩ simp only [Array.uset, Array.getElem_set, Array.size_set] split - · next hij => exact hij ▸ (hd (hm.hashes_to _ _)) + next hij => exact hij ▸ (hd (hm.hashes_to _ _)) · exact hm.hashes_to j (by simpa using hj) /-- This is the general theorem to show that modification operations preserve well-formedness of @@ -493,7 +493,7 @@ theorem modify_eq_alter [BEq α] [Hashable α] [LawfulBEq α] (m : Raw₀ α β) split · dsimp split - · next h => + next h => simp only [AssocList.contains_eq] at h simp only [AssocList.modify_eq_alter, AssocList.contains_eq, containsKey_of_perm AssocList.toList_alter, ← modifyKey_eq_alterKey, @@ -523,7 +523,7 @@ theorem modify_eq_alter [BEq α] [Hashable α] [EquivBEq α] (m : Raw₀ α (fun split · dsimp split - · next h => + next h => simp only [AssocList.contains_eq] at h simp only [AssocList.Const.modify_eq_alter, AssocList.contains_eq, containsKey_of_perm AssocList.Const.toList_alter, ← Const.modifyKey_eq_alterKey, diff --git a/src/Std/Data/DHashMap/Internal/WF.lean b/src/Std/Data/DHashMap/Internal/WF.lean index 5bb3826ed2..e036d6a7ad 100644 --- a/src/Std/Data/DHashMap/Internal/WF.lean +++ b/src/Std/Data/DHashMap/Internal/WF.lean @@ -59,7 +59,7 @@ theorem computeSize_eq {buckets : Array (AssocList α β)} : intro l l' induction l generalizing l' · simp - · next l₂ t ih => rw [foldl_cons, ← List.length_append, ih, foldl_cons] + next l₂ t ih => rw [foldl_cons, ← List.length_append, ih, foldl_cons] namespace Raw @@ -267,7 +267,7 @@ theorem isHashSelf_foldl_reinsertAux [BEq α] [Hashable α] [EquivBEq α] [Lawfu IsHashSelf (l.foldl (fun acc p => reinsertAux hash acc p.1 p.2) target).1 := by induction l generalizing target · simp - · next k v _ ih => exact fun h => ih _ (isHashSelf_reinsertAux _ _ _ h) + next k v _ ih => exact fun h => ih _ (isHashSelf_reinsertAux _ _ _ h) theorem toListModel_foldl_reinsertAux [BEq α] [Hashable α] [PartialEquivBEq α] (l : List ((a : α) × β a)) (target : { d : Array (AssocList α β) // 0 < d.size }) : @@ -275,7 +275,7 @@ theorem toListModel_foldl_reinsertAux [BEq α] [Hashable α] [PartialEquivBEq α (l ++ toListModel target.1) := by induction l generalizing target · simp - · next k v t ih => + next k v t ih => simp only [foldl_cons, cons_append] refine (ih _).trans ?_ refine ((toListModel_reinsertAux _ _ _).append_left _).trans perm_middle @@ -302,14 +302,14 @@ theorem expand.go_eq [BEq α] [Hashable α] [PartialEquivBEq α] (source : Array simpa using this 0 intro i induction i, source, target using expand.go.induct - · next i source target _ hi es newSource newTarget ih => + next i source target _ hi es newSource newTarget ih => simp only [newSource, newTarget, es] at * rw [expand.go_pos hi] refine ih.trans ?_ simp only [AssocList.foldl_eq, Array.toList_set] rw [List.drop_eq_getElem_cons hi, List.flatMap_cons, List.foldl_append, List.drop_set_of_lt (by omega), Array.getElem_toList] - · next i source target hi => + next i source target hi => rw [expand.go_neg hi, List.drop_eq_nil_of_le, flatMap_nil, foldl_nil] rwa [Array.size_eq_length_toList, Nat.not_lt] at hi @@ -546,11 +546,11 @@ theorem toListModel_insertₘ [BEq α] [Hashable α] [EquivBEq α] [LawfulHashab Perm (toListModel (m.insertₘ a b).1.2) (insertEntry a b (toListModel m.1.2)) := by rw [insertₘ] split - · next h' => + next h' => rw [containsₘ_eq_containsKey h] at h' rw [insertEntry_of_containsKey h'] exact toListModel_replaceₘ _ h _ _ - · next h' => + next h' => rw [containsₘ_eq_containsKey h, Bool.not_eq_true] at h' rw [insertEntry_of_containsKey_eq_false h'] refine (Raw₀.toListModel_expandIfNecessary _).trans ?_ @@ -608,7 +608,7 @@ theorem isHashSelf_alterₘ [BEq α] [Hashable α] [LawfulBEq α] (m : Raw₀ α dsimp only [alterₘ, withComputedSize] split · exact isHashSelf_updateBucket_alter h - · next hc => + next hc => split · exact h.buckets_hash_self · refine (wfImp_expandIfNecessary _ (wfImp_consₘ _ h _ _ ?_)).buckets_hash_self @@ -620,15 +620,15 @@ theorem toListModel_alterₘ [BEq α] [Hashable α] [LawfulBEq α] {m : Raw₀ rw [alterₘ] split · exact toListModel_updateBucket_alter h - · next hc => + next hc => rw [Bool.not_eq_true, containsₘ_eq_containsKey h] at hc rw [alterKey, getValueCast?_eq_none hc] split - · next hn => + next hn => simp only [hn] rw [eraseKey_of_containsKey_eq_false] exact hc - · next hs => + next hs => simp only [hs] refine Perm.trans (toListModel_expandIfNecessary _) ?_ refine Perm.trans (toListModel_consₘ m h _ _) ?_ @@ -648,7 +648,7 @@ theorem wfImp_alterₘ [BEq α] [Hashable α] [LawfulBEq α] {m : Raw₀ α β} size_eq := by rw [← Perm.length_eq (toListModel_alterₘ h).symm, alterₘ] split - · next h₁ => + next h₁ => rw [containsₘ_eq_containsKey h] at h₁ simp only [length_alterKey, h.size_eq, dif_pos h₁] rw [containsₘ_eq_containsKey (by apply wfImp_updateBucket_alter h)] @@ -656,14 +656,14 @@ theorem wfImp_alterₘ [BEq α] [Hashable α] [LawfulBEq α] {m : Raw₀ α β} simp only [containsKey_of_perm <| toListModel_updateBucket_alter h] rw [← getValueCast?_eq_some_getValueCast h₁] conv => lhs; congr; rw [containsKey_alterKey_self h.distinct] - · next h₁ => + next h₁ => rw [containsₘ_eq_containsKey h] at h₁ rw [alterKey] rw [getValueCast?_eq_none <| Bool.not_eq_true _ ▸ h₁] split - · next heq => + next heq => rw [heq, h.size_eq, length_eraseKey, if_neg h₁] - · next heq => + next heq => rw [heq, size_expandIfNecessary, consₘ, length_insertEntry, if_neg h₁, h.size_eq] theorem wfImp_alter [BEq α] [Hashable α] [LawfulBEq α] {m : Raw₀ α β} @@ -706,7 +706,7 @@ theorem isHashSelf_alterₘ [BEq α] [EquivBEq α] [Hashable α] [LawfulHashable dsimp only [alterₘ, withComputedSize] split · exact isHashSelf_updateBucket_alter h - · next hc => + next hc => split · exact h.buckets_hash_self · refine (wfImp_expandIfNecessary _ (wfImp_consₘ _ h _ _ ?_)).buckets_hash_self @@ -718,15 +718,15 @@ theorem toListModel_alterₘ [BEq α] [EquivBEq α] [Hashable α] [LawfulHashabl rw [Const.alterₘ] split · exact toListModel_updateBucket_alter h - · next hc => + next hc => rw [Bool.not_eq_true, containsₘ_eq_containsKey h] at hc rw [Const.alterKey, getValue?_eq_none.mpr hc] split - · next hn => + next hn => simp only [hn] rw [eraseKey_of_containsKey_eq_false] exact hc - · next hs => + next hs => simp only [hs] refine Perm.trans (toListModel_expandIfNecessary _) ?_ refine Perm.trans (toListModel_consₘ m h _ _) ?_ @@ -746,7 +746,7 @@ theorem wfImp_alterₘ [BEq α] [EquivBEq α] [Hashable α] [LawfulHashable α] size_eq := by rw [← Perm.length_eq (toListModel_alterₘ h).symm, alterₘ] split - · next h₁ => + next h₁ => rw [containsₘ_eq_containsKey h] at h₁ simp only [Const.length_alterKey, h.size_eq, dif_pos h₁] rw [containsₘ_eq_containsKey (by apply wfImp_updateBucket_alter h)] @@ -754,14 +754,14 @@ theorem wfImp_alterₘ [BEq α] [EquivBEq α] [Hashable α] [LawfulHashable α] simp only [containsKey_of_perm <| toListModel_updateBucket_alter h] rw [← getValue?_eq_some_getValue h₁] conv => lhs; congr; rw [Const.containsKey_alterKey_self h.distinct] - · next h₁ => + next h₁ => rw [containsₘ_eq_containsKey h] at h₁ rw [Const.alterKey] rw [getValue?_eq_none.mpr <| Bool.not_eq_true _ ▸ h₁] split - · next heq => + next heq => rw [heq, h.size_eq, length_eraseKey, if_neg h₁] - · next heq => + next heq => rw [heq, size_expandIfNecessary, consₘ, length_insertEntry, if_neg h₁, h.size_eq] theorem wfImp_alter [BEq α] [EquivBEq α] [Hashable α] [LawfulHashable α] {m : Raw₀ α (fun _ => β)} @@ -829,8 +829,8 @@ theorem toListModel_insertIfNewₘ [BEq α] [Hashable α] [EquivBEq α] [LawfulH (insertEntryIfNew a b (toListModel m.1.buckets)) := by rw [insertIfNewₘ, insertEntryIfNew, containsₘ_eq_containsKey h, cond_eq_if] split - · next h' => exact Perm.refl _ - · next h' => exact (toListModel_expandIfNecessary _).trans (toListModel_consₘ m h a b) + next h' => exact Perm.refl _ + next h' => exact (toListModel_expandIfNecessary _).trans (toListModel_consₘ m h a b) theorem wfImp_insertIfNewₘ [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] {m : Raw₀ α β} (h : Raw.WFImp m.1) {a : α} {b : β a} : Raw.WFImp (m.insertIfNewₘ a b).1 := by @@ -933,14 +933,14 @@ theorem toListModel_eraseₘ [BEq α] [Hashable α] [EquivBEq α] [LawfulHashabl rw [eraseₘ] split · exact toListModel_eraseₘaux m a h - · next h' => + next h' => exact toListModel_perm_eraseKey_of_containsₘ_eq_false _ _ h (eq_false_of_ne_true h') theorem wfImp_eraseₘ [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] {m : Raw₀ α β} {a : α} (h : Raw.WFImp m.1) : Raw.WFImp (m.eraseₘ a).1 := by rw [eraseₘ] split - · next h' => exact wfImp_eraseₘaux m a h h' + next h' => exact wfImp_eraseₘaux m a h h' · exact h /-! # `erase` -/ @@ -1010,20 +1010,20 @@ namespace Raw theorem WF.out [BEq α] [Hashable α] [i₁ : EquivBEq α] [i₂ : LawfulHashable α] {m : Raw α β} (h : m.WF) : Raw.WFImp m := by induction h generalizing i₁ i₂ - · next h => apply h + next h => apply h · exact Raw₀.wfImp_emptyWithCapacity - · next h => exact Raw₀.wfImp_insert (by apply h) - · next h => exact Raw₀.wfImp_containsThenInsert (by apply h) - · next h => exact Raw₀.wfImp_containsThenInsertIfNew (by apply h) - · next h => exact Raw₀.wfImp_erase (by apply h) - · next h => exact Raw₀.wfImp_insertIfNew (by apply h) - · next h => exact Raw₀.wfImp_getThenInsertIfNew? (by apply h) - · next h => exact Raw₀.wfImp_filter (by apply h) - · next h => exact Raw₀.Const.wfImp_getThenInsertIfNew? (by apply h) - · next h => exact Raw₀.wfImp_modify (by apply h) - · next h => exact Raw₀.Const.wfImp_modify (by apply h) - · next h => exact Raw₀.wfImp_alter (by apply h) - · next h => exact Raw₀.Const.wfImp_alter (by apply h) + next h => exact Raw₀.wfImp_insert (by apply h) + next h => exact Raw₀.wfImp_containsThenInsert (by apply h) + next h => exact Raw₀.wfImp_containsThenInsertIfNew (by apply h) + next h => exact Raw₀.wfImp_erase (by apply h) + next h => exact Raw₀.wfImp_insertIfNew (by apply h) + next h => exact Raw₀.wfImp_getThenInsertIfNew? (by apply h) + next h => exact Raw₀.wfImp_filter (by apply h) + next h => exact Raw₀.Const.wfImp_getThenInsertIfNew? (by apply h) + next h => exact Raw₀.wfImp_modify (by apply h) + next h => exact Raw₀.Const.wfImp_modify (by apply h) + next h => exact Raw₀.wfImp_alter (by apply h) + next h => exact Raw₀.Const.wfImp_alter (by apply h) end Raw diff --git a/src/Std/Data/DHashMap/Lemmas.lean b/src/Std/Data/DHashMap/Lemmas.lean index e0b8f28a93..ee72f4af83 100644 --- a/src/Std/Data/DHashMap/Lemmas.lean +++ b/src/Std/Data/DHashMap/Lemmas.lean @@ -2587,9 +2587,9 @@ theorem getKey!_alter [LawfulBEq α] [Inhabited α] {k k' : α} {f : Option (β m.getKey! k' := by simp only [getKey!_eq_get!_getKey?, getKey?_alter, beq_iff_eq] split - · next heq => + next heq => split <;> rfl - · next heq => + next heq => rfl theorem getKey!_alter_self [LawfulBEq α] [Inhabited α] {k : α} {f : Option (β k) → Option (β k)} : diff --git a/src/Std/Data/DTreeMap/Internal/Balanced.lean b/src/Std/Data/DTreeMap/Internal/Balanced.lean index b287fe21cc..2f8967695b 100644 --- a/src/Std/Data/DTreeMap/Internal/Balanced.lean +++ b/src/Std/Data/DTreeMap/Internal/Balanced.lean @@ -108,7 +108,7 @@ theorem Balanced.at_root {sz k v l r} : (Impl.inner sz k v l r : Impl α β).Bal theorem BalancedAtRoot.symm {l r : Nat} (h : BalancedAtRoot l r) : BalancedAtRoot r l := by cases h - · next h => exact Or.inl <| Nat.add_comm _ _ ▸ h - · next h => exact Or.inr h.symm + next h => exact Or.inl <| Nat.add_comm _ _ ▸ h + next h => exact Or.inr h.symm end Std.DTreeMap.Internal.Impl diff --git a/src/Std/Data/DTreeMap/Internal/Balancing.lean b/src/Std/Data/DTreeMap/Internal/Balancing.lean index 9c315a31bc..29965f21b1 100644 --- a/src/Std/Data/DTreeMap/Internal/Balancing.lean +++ b/src/Std/Data/DTreeMap/Internal/Balancing.lean @@ -542,7 +542,7 @@ theorem balance!_eq_balanceₘ {k v} {l r : Impl α β} (hlb : l.Balanced) (hrb · rw [dif_pos (by omega)] simp only [rotateL, Std.Internal.tree_tac, ite_self] omega - · next l r => + next l r => simp only [Std.Internal.tree_tac, rotateL] at * suffices h : l.size = 0 ∧ r.size = 0 by simp only [h.1, h.2, reduceDIte, Nat.not_lt_zero] @@ -556,9 +556,9 @@ theorem balance!_eq_balanceₘ {k v} {l r : Impl α β} (hlb : l.Balanced) (hrb simp only [Std.Internal.tree_tac] at * omega · simp_all [Std.Internal.tree_tac] - · simp_all only [Std.Internal.tree_tac] + next l r => + simp_all only [Std.Internal.tree_tac] rw [if_neg (by omega)] - next l r _ => rw [dif_neg (by omega), dif_pos (by omega), rotateR] suffices h : l.size = 0 ∧ r.size = 0 by simp only [h.1, h.2] diff --git a/src/Std/Data/DTreeMap/Internal/Operations.lean b/src/Std/Data/DTreeMap/Internal/Operations.lean index 6a5ed83d33..e40fce1d98 100644 --- a/src/Std/Data/DTreeMap/Internal/Operations.lean +++ b/src/Std/Data/DTreeMap/Internal/Operations.lean @@ -73,10 +73,11 @@ def minView (k : α) (v : β k) (l r : Impl α β) (hl : l.Balanced) (hr : r.Bal | leaf => ⟨k, v, ⟨r, hr, ✓⟩⟩ | inner _ k' v' l' r' => let ⟨dk, dv, ⟨dt, hdt, hdt'⟩⟩ := minView k' v' l' r' ✓ ✓ ✓ - ⟨dk, dv, ⟨balanceRErase k v dt r ✓ ✓ (by as_aux_lemma => - exact hlr.erase_left - (by simp only [hdt', hl.eq, size_inner]; omega) - (by simp only [hdt', hl.eq, size_inner]; omega)), ✓, ✓⟩⟩ + ⟨dk, dv, ⟨balanceRErase k v dt r ✓ ✓ (by + as_aux_lemma => + exact hlr.erase_left + (by simp only [hdt', hl.eq, size_inner]; omega) + (by simp only [hdt', hl.eq, size_inner]; omega)), ✓, ✓⟩⟩ /-- Slower version of `minView` which can be used in the absence of balance information but still @@ -96,9 +97,10 @@ def maxView (k : α) (v : β k) (l r : Impl α β) (hl : l.Balanced) (hr : r.Bal | leaf => ⟨k, v, ⟨l, hl, ✓⟩⟩ | inner _ k' v' l' r' => let ⟨dk, dv, ⟨dt, hdt, hdt'⟩⟩ := maxView k' v' l' r' ✓ ✓ ✓ - ⟨dk, dv, ⟨balanceLErase k v l dt ✓ ✓ (by as_aux_lemma => - simp only [hdt', size_inner, hr.eq] at * - apply hlr.erase_right <;> omega), ✓, ✓⟩⟩ + ⟨dk, dv, ⟨balanceLErase k v l dt ✓ ✓ (by + as_aux_lemma => + simp only [hdt', size_inner, hr.eq] at * + apply hlr.erase_right <;> omega), ✓, ✓⟩⟩ /-- Slower version of `maxView` which can be used in the absence of balance information but still @@ -129,14 +131,14 @@ def glue (l r : Impl α β) (hl : l.Balanced) (hr : r.Balanced) (hlr : BalancedA let ⟨dk, dv, ⟨dt, hdt, hdt'⟩⟩ := minView k' v' l'' r'' ✓ ✓ ✓ balanceLErase dk dv (.inner sz k v l' r') dt hl ✓ (by as_aux_lemma => - simp only [hdt', size_inner, hr.eq] at * - apply hlr.erase_right <;> omega) + simp only [hdt', size_inner, hr.eq] at * + apply hlr.erase_right <;> omega) else let ⟨dk, dv, ⟨dt, hdt, hdt'⟩⟩ := maxView k v l' r' ✓ ✓ ✓ balanceRErase dk dv dt (.inner sz' k' v' l'' r'') ✓ hr (by as_aux_lemma => - simp only [hdt', size_inner, hl.eq] at * - apply hlr.erase_left <;> omega) + simp only [hdt', size_inner, hl.eq] at * + apply hlr.erase_left <;> omega) @[Std.Internal.tree_tac] theorem size_glue {l r : Impl α β} {hl hr hlr} : (glue l r hl hr hlr).size = l.size + r.size := by diff --git a/src/Std/Data/DTreeMap/Internal/WF/Lemmas.lean b/src/Std/Data/DTreeMap/Internal/WF/Lemmas.lean index f6eb34b3ca..6e93b80362 100644 --- a/src/Std/Data/DTreeMap/Internal/WF/Lemmas.lean +++ b/src/Std/Data/DTreeMap/Internal/WF/Lemmas.lean @@ -1475,7 +1475,7 @@ end Const theorem WF.ordered [Ord α] [TransOrd α] {l : Impl α β} (h : WF l) : l.Ordered := by induction h - · next h => exact h + next h => exact h · exact ordered_empty · exact ordered_insert ‹_› ‹_› · exact ordered_insertIfNew ‹_› ‹_› @@ -1810,7 +1810,7 @@ theorem WF.filter! {_ : Ord α} {t : Impl α β} {f : (a : α) → β a → Bool theorem toListModel_map [Ord α] {t : Impl α β} {f : (a : α) → β a → γ a} : (t.map f).toListModel = t.toListModel.map fun x => ⟨x.1, f x.1 x.2⟩ := by induction t - · next ihl ihr => + next ihl ihr => simp [map, ihl, ihr] · rfl diff --git a/src/Std/Data/Internal/List/Associative.lean b/src/Std/Data/Internal/List/Associative.lean index 57bfd99aac..b25790682e 100644 --- a/src/Std/Data/Internal/List/Associative.lean +++ b/src/Std/Data/Internal/List/Associative.lean @@ -79,7 +79,7 @@ theorem beq_of_getEntry?_eq_some [BEq α] {l : List ((a : α) × β a)} {a : α} (h : getEntry? a l = some p) : p.1 == a := by induction l using assoc_induction · simp at h - · next k' v' t ih => + next k' v' t ih => cases h' : k' == a · rw [getEntry?_cons_of_false h'] at h exact ih h @@ -91,7 +91,7 @@ theorem getEntry?_congr [BEq α] [PartialEquivBEq α] {l : List ((a : α) × β (h : a == b) : getEntry? a l = getEntry? b l := by induction l using assoc_induction · simp - · next k v l ih => + next k v l ih => cases h' : k == a · have h₂ : (k == b) = false := BEq.neq_of_neq_of_beq h' h rw [getEntry?_cons_of_false h', getEntry?_cons_of_false h₂, ih] @@ -171,7 +171,7 @@ theorem getValue?_eq_getEntry? [BEq α] {l : List ((_ : α) × β)} {a : α} : getValue? a l = (getEntry? a l).map (·.2) := by induction l using assoc_induction · simp - · next k v l ih => + next k v l ih => cases h : k == a · rw [getEntry?_cons_of_false h, getValue?_cons_of_false h, ih] · rw [getEntry?_cons_of_true h, getValue?_cons_of_true h, Option.map_some] @@ -260,7 +260,7 @@ private theorem getValueCast?_eq_getEntry? [BEq α] [LawfulBEq α] {l : List ((a (fun p h => cast (congrArg β (eq_of_beq (beq_of_getEntry?_eq_some h))) p.2) := by induction l using assoc_induction · simp - · next k v t ih => + next k v t ih => cases h : k == a · simp only [getValueCast?_cons_of_false h, ih, getEntry?_cons_of_false h] · simp only [getValueCast?_cons_of_true h, getEntry?_cons_of_true h, Option.dmap_some] @@ -311,7 +311,7 @@ theorem containsKey_eq_isSome_getEntry? [BEq α] {l : List ((a : α) × β a)} { containsKey a l = (getEntry? a l).isSome := by induction l using assoc_induction · simp - · next k v l ih => + next k v l ih => cases h : k == a · simp [getEntry?_cons_of_false h, h, ih] · simp [getEntry?_cons_of_true h, h] @@ -347,7 +347,7 @@ theorem containsKey_eq_keys_contains [BEq α] [PartialEquivBEq α] {l : List ((a {a : α} : containsKey a l = (keys l).contains a := by induction l using assoc_induction · rfl - · next k _ l ih => simp [ih, BEq.comm] + next k _ l ih => simp [ih, BEq.comm] theorem containsKey_of_mem_keys [BEq α] [EquivBEq α] {l : List ((a : α) × β a)} {a : α} (h : a ∈ keys l) : containsKey a l := @@ -804,7 +804,7 @@ theorem getKey?_eq_getEntry? [BEq α] {l : List ((a : α) × β a)} {a : α} : getKey? a l = (getEntry? a l).map (·.1) := by induction l using assoc_induction · simp - · next k v l ih => + next k v l ih => cases h : k == a · rw [getEntry?_cons_of_false h, getKey?_cons_of_false h, ih] · rw [getEntry?_cons_of_true h, getKey?_cons_of_true h, Option.map_some] @@ -1094,7 +1094,7 @@ theorem replaceEntry_of_containsKey_eq_false [BEq α] {l : List ((a : α) × β (h : containsKey k l = false) : replaceEntry k v l = l := by induction l · simp - · next k v l ih => + next k v l ih => rw [containsKey_cons_eq_false] at h rw [replaceEntry_cons_of_false h.1, ih h.2] @@ -1111,10 +1111,10 @@ theorem mem_replaceEntry_of_beq_eq_false [BEq α] [EquivBEq α] {a : α} {b : β p ∈ replaceEntry a b l ↔ p ∈ l := by induction l · simp only [replaceEntry_nil] - · next ih => + next ih => simp only [replaceEntry, cond_eq_if] split - · next h => + next h => simp only [List.mem_cons, Sigma.ext_iff] apply Iff.intro <;> exact fun | Or.inr y => Or.inr y @@ -1136,7 +1136,7 @@ theorem getEntry?_replaceEntry_of_false [BEq α] [PartialEquivBEq α] {l : List getEntry? a (replaceEntry k v l) = getEntry? a l := by induction l using assoc_induction · simp - · next k' v' l ih => + next k' v' l ih => cases h' : k' == k · rw [replaceEntry_cons_of_false h', getEntry?_cons, getEntry?_cons, ih] · rw [replaceEntry_cons_of_true h'] @@ -1148,7 +1148,7 @@ theorem getEntry?_replaceEntry_of_true [BEq α] [PartialEquivBEq α] {l : List ( getEntry? a (replaceEntry k v l) = some ⟨k, v⟩ := by induction l using assoc_induction · simp at hl - · next k' v' l ih => + next k' v' l ih => cases hk'a : k' == k · rw [replaceEntry_cons_of_false hk'a] have hk'k : (k' == a) = false := BEq.neq_of_neq_of_beq hk'a h @@ -1186,7 +1186,7 @@ theorem mem_getEntry [BEq α] {l : List ((a : α) × β a)} {k : α} (hl : conta getEntry k l hl ∈ l := by induction l using assoc_induction · simp at hl - · next k' v' l ih => + next k' v' l ih => simp [getEntry, getEntry?_cons, cond_eq_if] split · simp @@ -1198,7 +1198,7 @@ theorem mem_replaceEntry_of_true [BEq α] [PartialEquivBEq α] {l : List ((a : ⟨k, v⟩ ∈ replaceEntry k v l := by induction l using assoc_induction · simp at hl - · next k' v' l ih => + next k' v' l ih => cases h : k' == k <;> simp_all [replaceEntry_cons] @[simp] @@ -1232,9 +1232,9 @@ theorem getValueCast?_replaceEntry [BEq α] [LawfulBEq α] {l : List ((a : α) else getValueCast? a l := by rw [getValueCast?_eq_getEntry?] split - · next h => + next h => simp only [getEntry?_replaceEntry_of_true h.1 h.2, Option.dmap_some] - · next h => + next h => simp only [Decidable.not_and_iff_not_or_not] at h rcases h with h|h · simp only [getEntry?_replaceEntry_of_containsKey_eq_false (Bool.eq_false_iff.2 h), @@ -1247,8 +1247,8 @@ theorem getKey?_replaceEntry [BEq α] [PartialEquivBEq α] {l : List ((a : α) if containsKey k l ∧ k == a then some k else getKey? a l := by rw [getKey?_eq_getEntry?] split - · next h => simp [getEntry?_replaceEntry_of_true h.1 h.2] - · next h => + next h => simp [getEntry?_replaceEntry_of_true h.1 h.2] + next h => simp only [Decidable.not_and_iff_not_or_not] at h rcases h with h|h · rw [getEntry?_replaceEntry_of_containsKey_eq_false (Bool.eq_false_iff.2 h), getKey?_eq_getEntry?] @@ -1281,7 +1281,7 @@ theorem eraseKey_of_containsKey_eq_false [BEq α] {l : List ((a : α) × β a)} (h : containsKey k l = false) : eraseKey k l = l := by induction l using assoc_induction · simp - · next k' v' t ih => + next k' v' t ih => simp only [containsKey_cons, Bool.or_eq_false_iff] at h rw [eraseKey_cons_of_false h.1, ih h.2] @@ -1290,16 +1290,16 @@ theorem mem_eraseKey_of_key_beq_eq_false [BEq α] {a : α} p ∈ eraseKey a l ↔ p ∈ l := by induction l · simp only [eraseKey_nil] - · next ih => + next ih => simp only [eraseKey, List.mem_cons] rw [cond_eq_if] split - · next h => + next h => rw [iff_or_self, Sigma.ext_iff] intro ⟨h₁, h₂⟩ rw [h₁, h] at hne contradiction - · next h => + next h => simp only [List.mem_cons, ih] theorem mem_eraseKey_of_key_ne [BEq α] [LawfulBEq α] {a : α} @@ -1310,7 +1310,7 @@ theorem sublist_eraseKey [BEq α] {l : List ((a : α) × β a)} {k : α} : Sublist (eraseKey k l) l := by induction l using assoc_induction · simp - · next k' v' t ih => + next k' v' t ih => rw [eraseKey_cons] cases k' == k · simpa @@ -1320,7 +1320,7 @@ theorem length_eraseKey [BEq α] {l : List ((a : α) × β a)} {k : α} : (eraseKey k l).length = if containsKey k l then l.length - 1 else l.length := by induction l using assoc_induction · simp - · next k' v' t ih => + next k' v' t ih => rw [eraseKey_cons, containsKey_cons] cases k' == k · rw [cond_false, Bool.false_or, List.length_cons, ih] @@ -1353,7 +1353,7 @@ theorem DistinctKeys.replaceEntry [BEq α] [PartialEquivBEq α] {l : List ((a : {v : β k} (h : DistinctKeys l) : DistinctKeys (replaceEntry k v l) := by induction l using assoc_induction · simp - · next k' v' l ih => + next k' v' l ih => rw [distinctKeys_cons_iff] at h cases hk'k : k' == k · rw [replaceEntry_cons_of_false hk'k, distinctKeys_cons_iff] @@ -1802,7 +1802,7 @@ theorem keys_eraseKey [BEq α] [PartialEquivBEq α] {l : List ((a : α) × β a) keys (eraseKey k l) = (keys l).erase k := by induction l using assoc_induction · rfl - · next k' v' l ih => + next k' v' l ih => simp only [eraseKey_cons, keys_cons, List.erase_cons] rw [BEq.comm] cases k == k' <;> simp [ih] @@ -1815,7 +1815,7 @@ theorem getEntry?_eraseKey_self [BEq α] [PartialEquivBEq α] {l : List ((a : α (h : DistinctKeys l) : getEntry? k (eraseKey k l) = none := by induction l using assoc_induction · simp - · next k' v' t ih => + next k' v' t ih => cases h' : k' == k · rw [eraseKey_cons_of_false h', getEntry?_cons_of_false h'] exact ih h.tail @@ -1831,7 +1831,7 @@ theorem getEntry?_eraseKey_of_false [BEq α] [PartialEquivBEq α] {l : List ((a {k a : α} (hka : (k == a) = false) : getEntry? a (eraseKey k l) = getEntry? a l := by induction l using assoc_induction · simp - · next k' v' t ih => + next k' v' t ih => cases h' : k' == k · rw [eraseKey_cons_of_false h'] cases h'' : k' == a @@ -1853,7 +1853,7 @@ theorem keys_filterMap' {l : List ((a : α) × β a)} {f : (a : α) → β a → keys (l.filter fun p => (f p.1 p.2).isSome) := by induction l using assoc_induction · simp - · next k v t ih => + next k v t ih => simp only [List.filterMap_cons, List.filter_cons] cases f k v <;> simp [ih] @@ -1861,7 +1861,7 @@ theorem mem_keys_iff_contains [BEq α] [LawfulBEq α] {l : List ((a : α) × β k ∈ keys l ↔ containsKey k l = true := by induction l using assoc_induction · simp - · next k' v t ih => + next k' v t ih => simp only [keys_cons, List.mem_cons, containsKey_cons, Bool.or_eq_true, beq_iff_eq] rw [ih, Eq.comm] @@ -2101,27 +2101,27 @@ theorem getEntry?_of_perm [BEq α] [PartialEquivBEq α] {l l' : List ((a : α) (hl : DistinctKeys l) (h : Perm l l') : getEntry? a l = getEntry? a l' := by induction h · simp - · next p t₁ t₂ _ ih₂ => + next p t₁ t₂ _ ih₂ => rcases p with ⟨k', v'⟩ simp only [getEntry?_cons, ih₂ hl.tail] - · next p p' _ => + next p p' _ => rcases p with ⟨k₁, v₁⟩ rcases p' with ⟨k₂, v₂⟩ simp only [getEntry?_cons] cases h₂ : k₂ == a <;> cases h₁ : k₁ == a <;> try simp; done simp only [distinctKeys_cons_iff, containsKey_cons, Bool.or_eq_false_iff] at hl exact ((Bool.eq_false_iff.1 hl.2.1).elim (BEq.trans h₁ (BEq.symm h₂))).elim - · next l₁ l₂ l₃ hl₁₂ _ ih₁ ih₂ => exact (ih₁ hl).trans (ih₂ (hl.perm (hl₁₂.symm))) + next l₁ l₂ l₃ hl₁₂ _ ih₁ ih₂ => exact (ih₁ hl).trans (ih₂ (hl.perm (hl₁₂.symm))) theorem containsKey_of_perm [BEq α] [PartialEquivBEq α] {l l' : List ((a : α) × β a)} {k : α} (h : Perm l l') : containsKey k l = containsKey k l' := by induction h · simp - · next p t₁ t₂ _ ih₂ => rw [containsKey_cons, containsKey_cons, ih₂] - · next p p' _ => + next p t₁ t₂ _ ih₂ => rw [containsKey_cons, containsKey_cons, ih₂] + next p p' _ => rw [containsKey_cons, containsKey_cons, containsKey_cons, containsKey_cons] simp only [← Bool.or_assoc, Bool.or_comm] - · next _ _ _ _ _ ih₁ ih₂ => exact ih₁.trans ih₂ + next _ _ _ _ _ ih₁ ih₂ => exact ih₁.trans ih₂ theorem getValueCast?_of_perm [BEq α] [LawfulBEq α] {l l' : List ((a : α) × β a)} {a : α} (hl : DistinctKeys l) (h : Perm l l') : getValueCast? a l = getValueCast? a l' := by @@ -2192,7 +2192,7 @@ theorem perm_cons_getEntry [BEq α] {l : List ((a : α) × β a)} {a : α} (h : ∃ l', Perm l (getEntry a l h :: l') := by induction l using assoc_induction · simp at h - · next k' v' t ih => + next k' v' t ih => simp only [containsKey_cons, Bool.or_eq_true] at h cases hk : k' == a · obtain ⟨l', hl'⟩ := ih (h.resolve_left (Bool.not_eq_true _ ▸ hk)) @@ -2206,8 +2206,8 @@ theorem getEntry?_ext [BEq α] [EquivBEq α] {l l' : List ((a : α) × β a)} (h induction l using assoc_induction generalizing l' · induction l' using assoc_induction · exact Perm.refl _ - · next k _ _ _ => simpa using h k - · next k v t ih => + next k _ _ _ => simpa using h k + next k v t ih => have hl'k₁ : getEntry? k l' = some ⟨k, v⟩ := by rw [← h, getEntry?_cons_self] have hl'k₂ : containsKey k l' := by rw [containsKey_eq_isSome_getEntry?, hl'k₁, Option.isSome_some] @@ -2302,7 +2302,7 @@ theorem getEntry?_append [BEq α] {l l' : List ((a : α) × β a)} {a : α} : getEntry? a (l ++ l') = (getEntry? a l).or (getEntry? a l') := by induction l using assoc_induction · simp - · next k' v' t ih => cases h : k' == a <;> simp_all [getEntry?_cons] + next k' v' t ih => cases h : k' == a <;> simp_all [getEntry?_cons] theorem getEntry?_append_of_containsKey_eq_false [BEq α] {l l' : List ((a : α) × β a)} {a : α} (h : containsKey a l' = false) : getEntry? a (l ++ l') = getEntry? a l := by @@ -2318,7 +2318,7 @@ theorem containsKey_flatMap_eq_false [BEq α] {γ : Type w} {l : List γ} {f : containsKey a (l.flatMap f) = false := by induction l · simp - · next g t ih => + next g t ih => simp only [List.flatMap_cons, containsKey_append, Bool.or_eq_false_iff] refine ⟨?_, ?_⟩ · simpa using h 0 (by simp) @@ -2373,7 +2373,7 @@ theorem replaceEntry_append_of_containsKey_left [BEq α] {l l' : List ((a : α) {v : β k} (h : containsKey k l) : replaceEntry k v (l ++ l') = replaceEntry k v l ++ l' := by induction l using assoc_induction · simp at h - · next k' v' t ih => + next k' v' t ih => simp only [containsKey_cons, Bool.or_eq_true] at h cases h' : k' == k · simpa [replaceEntry_cons, h'] using ih (h.resolve_left (Bool.not_eq_true _ ▸ h')) @@ -2384,7 +2384,7 @@ theorem replaceEntry_append_of_containsKey_left_eq_false [BEq α] {l l' : List ( replaceEntry k v (l ++ l') = l ++ replaceEntry k v l' := by induction l using assoc_induction · simp - · next k' v' t ih => + next k' v' t ih => simp only [containsKey_cons, Bool.or_eq_false_iff] at h simpa [replaceEntry_cons, h.1] using ih h.2 @@ -2407,7 +2407,7 @@ theorem eraseKey_append_of_containsKey_right_eq_false [BEq α] {l l' : List ((a (h : containsKey k l' = false) : eraseKey k (l ++ l') = eraseKey k l ++ l' := by induction l using assoc_induction · simp [eraseKey_of_containsKey_eq_false h] - · next k' v' t ih => + next k' v' t ih => rw [List.cons_append, eraseKey_cons, eraseKey_cons] cases k' == k · rw [cond_false, cond_false, ih, List.cons_append] @@ -3611,9 +3611,9 @@ theorem containsKey_alterKey {k k' : α} {f : Option (β k) → Option (β k)} else containsKey k' l := by split - · next h => + next h => rw [← containsKey_congr h, containsKey_alterKey_self hl] - · next h => + next h => rw [alterKey] cases f (getValueCast? k l) · simp [containsKey_eraseKey_of_false (Bool.not_eq_true _ ▸ h)] @@ -3639,22 +3639,22 @@ theorem getValueCast?_alterKey (k k' : α) (f : Option (β k) → Option (β k)) else getValueCast? k' l := by split - · next heq => + next heq => cases eq_of_beq heq simp only [Function.comp_apply, cast_eq] rw [alterKey] split - · next hnone => + next hnone => simp only [getValueCast?_eraseKey_self hl, hnone] - · next hsome => + next hsome => rw [hsome, getValueCast?_insertEntry_self] - · next heq => + next heq => rw [alterKey] split - · next hnone => + next hnone => simp only [heq, hl, getValueCast?_eraseKey, ite_false, Bool.false_eq_true, ] - · next hsome => + next hsome => simp only [getValueCast?_insertEntry, dite_false, heq, Bool.false_eq_true] theorem getValueCast_alterKey (k k' : α) (f : Option (β k) → Option (β k)) @@ -3670,11 +3670,11 @@ theorem getValueCast_alterKey (k k' : α) (f : Option (β k) → Option (β k)) have := getValueCast?_alterKey k k' f l hl rw [getValueCast?_eq_some_getValueCast hc] at this split - · next heq => + next heq => cases eq_of_beq heq apply Option.some_inj.mp simp_all - · next heq => + next heq => apply Option.some_inj.mp simp_all only [Bool.false_eq_true, Function.comp_apply, dite_false] rw [getValueCast?_eq_some_getValueCast] @@ -3696,7 +3696,7 @@ theorem getValueCast!_alterKey {k k' : α} [Inhabited (β k')] {f : Option (β k simp only [hl, getValueCast!_eq_getValueCast?, getValueCast?_alterKey, beq_iff_eq, Function.comp_apply] split - · next heq => + next heq => simp only [Option.map_cast_apply] · rfl @@ -3728,9 +3728,9 @@ theorem getKey!_alterKey [Inhabited α] {k k' : α} {f : Option (β k) → Optio getKey! k' l := by simp only [getKey!_eq_getKey?, hl, getKey?_alterKey, beq_iff_eq] split - · next heq => + next heq => split <;> rfl - · next heq => + next heq => rfl theorem getKey_alterKey {k k' : α} {f : Option (β k) → Option (β k)} @@ -3744,11 +3744,11 @@ theorem getKey_alterKey {k k' : α} {f : Option (β k) → Option (β k)} have := getKey?_alterKey (f := f) (k' := k') _ hl rw [getKey?_eq_some_getKey hc] at this split - · next heq => + next heq => cases eq_of_beq heq apply Option.some_inj.mp simp_all - · next heq => + next heq => apply Option.some_inj.mp simp_all only [Bool.false_eq_true, ite_false] rw [getKey?_eq_some_getKey] @@ -3762,7 +3762,7 @@ theorem getKeyD_alterKey {k k' fallback : α} {f : Option (β k) → Option (β getKeyD k' l fallback := by simp only [hl, getKeyD_eq_getKey?, getKey?_alterKey, beq_iff_eq] split - · next heq => + next heq => split <;> rfl · rfl @@ -3886,9 +3886,9 @@ theorem containsKey_alterKey_self [EquivBEq α] {a : α} {f : Option β → Opti | x :: xs => simp only [alterKey] split - · next heq => + next heq => simp only [hl, heq, Option.isSome_none, containsKey_eraseKey_self] - · next heq => + next heq => simp only [containsKey_insertEntry, BEq.rfl, Bool.true_or, heq, Option.isSome_some] theorem mem_alterKey_of_key_not_beq [EquivBEq α] {β : Type v} {a : α} {f : Option β → Option β} @@ -3906,15 +3906,15 @@ theorem containsKey_alterKey [EquivBEq α] {k k' : α} {f : Option β → Option else containsKey k' l := by split - · next h => + next h => rw [← containsKey_congr h] exact containsKey_alterKey_self hl - · next h => + next h => rw [alterKey] split - · next heq => + next heq => simp only [containsKey_eraseKey_of_false (Bool.not_eq_true _ ▸ h)] - · next heq => + next heq => simp_all only [Bool.not_eq_true, containsKey_insertEntry, Bool.false_or] theorem getValue?_alterKey [EquivBEq α] (k k' : α) (f : Option β → Option β) @@ -3924,20 +3924,20 @@ theorem getValue?_alterKey [EquivBEq α] (k k' : α) (f : Option β → Option else getValue? k' l := by split - · next heq => + next heq => rw [alterKey] split - · next hnone => + next hnone => simp only [getValue?_eraseKey_of_beq hl heq, hnone] - · next hsome => + next hsome => rw [hsome, getValue?_insertEntry_of_beq heq] - · next heq => + next heq => rw [alterKey] split - · next hnone => + next hnone => simp only [heq, hl, getValue?_eraseKey, ite_false, Bool.false_eq_true, ] - · next hsome => + next hsome => simp only [getValue?_insertEntry, heq, Bool.false_eq_true, reduceIte] theorem getValue_alterKey [EquivBEq α] (k k' : α) (f : Option β → Option β) (l : List ((_ : α) × β)) @@ -3952,10 +3952,10 @@ theorem getValue_alterKey [EquivBEq α] (k k' : α) (f : Option β → Option β have := getValue?_alterKey k k' f l hl rw [getValue?_eq_some_getValue hc] at this split - · next heq => + next heq => apply Option.some_inj.mp simp_all - · next heq => + next heq => apply Option.some_inj.mp simp_all only [Bool.false_eq_true, ite_false] rw [getValue?_eq_some_getValue] @@ -4017,10 +4017,10 @@ theorem getKey_alterKey [EquivBEq α] {k k' : α} {f : Option β → Option β} have := getKey?_alterKey (f := f) (k := k) (k' := k') _ hl rw [getKey?_eq_some_getKey hc] at this split - · next heq => + next heq => apply Option.some_inj.mp simp_all - · next heq => + next heq => apply Option.some_inj.mp simp_all only [Bool.false_eq_true, ite_false] rw [getKey?_eq_some_getKey] @@ -4034,7 +4034,7 @@ theorem getKeyD_alterKey [EquivBEq α] {k k' fallback : α} {f : Option β → O getKeyD k' l fallback := by simp only [hl, getKeyD_eq_getKey?, getKey?_alterKey] split - · next heq => + next heq => split <;> rfl · rfl @@ -4076,7 +4076,7 @@ theorem length_modifyKey [BEq α] [LawfulBEq α] (k : α) (f : β k → β k) (l (modifyKey k f l).length = l.length := by induction l · rfl - · next ih => + next ih => simp only [modifyKey] split <;> next h => simp only [length_replaceEntry, List.length_cons] @@ -4130,7 +4130,7 @@ theorem getValueCast_modifyKey [BEq α] [LawfulBEq α] {k k' : α} {f : β k → getValueCast k' l h' := by simp only [modifyKey_eq_alterKey, getValueCast_alterKey, hl] split - · next heq => + next heq => cases eq_of_beq heq haveI h' : containsKey k l := by rwa [containsKey_modifyKey, ← eq_of_beq heq] at h simp [getValueCast?_eq_some_getValueCast, h'] @@ -4265,7 +4265,7 @@ theorem length_modifyKey (k : α) (f : β → β) (l : List ((_ : α) × β)) : (modifyKey k f l).length = l.length := by induction l · rfl - · next ih => + next ih => simp only [modifyKey] split <;> next h => simp only [length_replaceEntry, List.length_cons] @@ -4303,7 +4303,7 @@ theorem getValue_modifyKey [EquivBEq α] {k k' : α} {f : β → β} (l : List ( getValue k' l h' := by simp only [modifyKey_eq_alterKey, getValue_alterKey, hl] split - · next heq => + next heq => haveI h' : containsKey k l := by rwa [containsKey_modifyKey, ← containsKey_congr heq] at h simp [getValue?_eq_some_getValue, h'] · rfl diff --git a/src/Std/Data/Iterators/Lemmas/Combinators/Drop.lean b/src/Std/Data/Iterators/Lemmas/Combinators/Drop.lean index b9a2eb1a01..d7f5400f9a 100644 --- a/src/Std/Data/Iterators/Lemmas/Combinators/Drop.lean +++ b/src/Std/Data/Iterators/Lemmas/Combinators/Drop.lean @@ -41,7 +41,7 @@ theorem Iter.atIdxSlow?_drop {α β} (it.drop k).atIdxSlow? l = it.atIdxSlow? (l + k) := by induction k generalizing it <;> induction l generalizing it all_goals - induction it using Iter.inductSkips with | step it ih => + induction it using Iter.inductSkips with | step it ih rw [atIdxSlow?.eq_def, atIdxSlow?.eq_def, step_drop] cases it.step using PlausibleIterStep.casesOn <;> simp [*] diff --git a/src/Std/Data/Iterators/Lemmas/Combinators/DropWhile.lean b/src/Std/Data/Iterators/Lemmas/Combinators/DropWhile.lean index 4533b34d85..d17493d212 100644 --- a/src/Std/Data/Iterators/Lemmas/Combinators/DropWhile.lean +++ b/src/Std/Data/Iterators/Lemmas/Combinators/DropWhile.lean @@ -82,7 +82,7 @@ theorem Iter.toList_intermediateDropWhile_of_finite {α β} [Iterator α Id β] {it : Iter (α := α) β} : (Intermediate.dropWhile P dropping it).toList = if dropping = true then it.toList.dropWhile P else it.toList := by - induction it using Iter.inductSteps generalizing dropping with | step it ihy ihs => + induction it using Iter.inductSteps generalizing dropping with | step it ihy ihs rw [toList_eq_match_step, toList_eq_match_step, step_intermediateDropWhile] cases it.step using PlausibleIterStep.casesOn · rename_i hp diff --git a/src/Std/Data/Iterators/Lemmas/Combinators/Take.lean b/src/Std/Data/Iterators/Lemmas/Combinators/Take.lean index 1196ff3584..2c1f1e052c 100644 --- a/src/Std/Data/Iterators/Lemmas/Combinators/Take.lean +++ b/src/Std/Data/Iterators/Lemmas/Combinators/Take.lean @@ -61,7 +61,7 @@ theorem Iter.toList_take_of_finite {α β} [Iterator α Id β] {n : Nat} [Finite α Id] [IteratorCollect α Id Id] [LawfulIteratorCollect α Id Id] {it : Iter (α := α) β} : (it.take n).toList = it.toList.take n := by - induction it using Iter.inductSteps generalizing n with | step it ihy ihs => + induction it using Iter.inductSteps generalizing n with | step it ihy ihs rw [Iter.toList_eq_match_step, Iter.toList_eq_match_step, Iter.step_take] cases n case zero => simp diff --git a/src/Std/Data/Iterators/Lemmas/Consumers/Monadic/Collect.lean b/src/Std/Data/Iterators/Lemmas/Consumers/Monadic/Collect.lean index 5bfbed9305..79c94a2d8a 100644 --- a/src/Std/Data/Iterators/Lemmas/Consumers/Monadic/Collect.lean +++ b/src/Std/Data/Iterators/Lemmas/Consumers/Monadic/Collect.lean @@ -20,7 +20,7 @@ theorem IterM.Equiv.toListRev_eq [Monad m] [LawfulMonad m] [Iterator α₁ m β] [Iterator α₂ m β] [Finite α₁ m] [Finite α₂ m] {ita : IterM (α := α₁) m β} {itb : IterM (α := α₂) m β} (h : IterM.Equiv ita itb) : ita.toListRev = itb.toListRev := by - induction ita using IterM.inductSteps generalizing itb with | step ita ihy ihs => + induction ita using IterM.inductSteps generalizing itb with | step ita ihy ihs rw [IterM.toListRev_eq_match_step, IterM.toListRev_eq_match_step] apply h.lift_step_bind_congr intro s₁ s₂ h diff --git a/src/Std/Do/SPred/Laws.lean b/src/Std/Do/SPred/Laws.lean index 691ba69732..20b32ce1d6 100644 --- a/src/Std/Do/SPred/Laws.lean +++ b/src/Std/Do/SPred/Laws.lean @@ -46,7 +46,7 @@ instance : Trans (@entails σs) entails entails where theorem bientails.iff {P Q : SPred σs} : P ⊣⊢ₛ Q ↔ (P ⊢ₛ Q) ∧ (Q ⊢ₛ P) := by induction σs with | nil => exact Iff.intro (fun h => ⟨h.mp, h.mpr⟩) (fun h => ⟨h.1, h.2⟩) - | cons σ σs ih => + | cons σ σs ih apply Iff.intro · exact fun h => ⟨fun s => (ih.mp (h s)).1, fun s => (ih.mp (h s)).2⟩ · intro h s; exact ih.mpr ⟨h.1 s, h.2 s⟩ diff --git a/src/Std/Sat/AIG/Basic.lean b/src/Std/Sat/AIG/Basic.lean index 0438897a17..db2c8c0b39 100644 --- a/src/Std/Sat/AIG/Basic.lean +++ b/src/Std/Sat/AIG/Basic.lean @@ -198,7 +198,7 @@ theorem Cache.get?_property {decls : Array (Decl α)} {idx : Nat} (c : Cache α split · apply ih simp [hfound] - · next hbounds => + next hbounds => exfalso apply hbounds specialize ih _ hfound @@ -217,7 +217,7 @@ theorem Cache.get?_property {decls : Array (Decl α)} {idx : Nat} (c : Cache α | false => apply ih simpa [BEq.symm_false heq] using hfound - · next hbounds => + next hbounds => simp only [HashMap.getElem?_insert] at hfound match heq : decl == decl' with | true => diff --git a/src/Std/Sat/AIG/CNF.lean b/src/Std/Sat/AIG/CNF.lean index c75190edc5..d38766a8da 100644 --- a/src/Std/Sat/AIG/CNF.lean +++ b/src/Std/Sat/AIG/CNF.lean @@ -268,11 +268,11 @@ def Cache.addFalse (cache : Cache aig cnf) (idx : Nat) (h : idx < aig.decls.size intro assign heval idx hbound hmarked rw [Array.getElem_set] at hmarked split at hmarked - · next heq => + next heq => simp only [heq, CNF.eval_append, Decl.falseToCNF_eval, Bool.and_eq_true, beq_iff_eq] at htip heval simp [denote_idx_false htip, projectRightAssign_property, heval] - · next heq => + next heq => simp only [CNF.eval_append, Decl.falseToCNF_eval, Bool.and_eq_true, beq_iff_eq] at heval have := cache.inv assign heval.right idx hbound hmarked rw [this] @@ -298,10 +298,10 @@ def Cache.addAtom (cache : Cache aig cnf) (idx : Nat) (h : idx < aig.decls.size) intro assign heval idx hbound hmarked rw [Array.getElem_set] at hmarked split at hmarked - · next heq => + next heq => simp only [heq, CNF.eval_append, Decl.atomToCNF_eval, Bool.and_eq_true, beq_iff_eq] at htip heval simp [heval, denote_idx_atom htip] - · next heq => + next heq => simp only [CNF.eval_append, Decl.atomToCNF_eval, Bool.and_eq_true, beq_iff_eq] at heval have := cache.inv assign heval.right idx hbound hmarked rw [this] @@ -337,7 +337,7 @@ def Cache.addGate (cache : Cache aig cnf) {hlb} {hrb} (idx : Nat) (h : idx < aig intro assign heval idx hbound hmarked rw [Array.getElem_set] at hmarked split at hmarked - · next heq => + next heq => simp only [heq, CNF.eval_append, Decl.gateToCNF_eval, Bool.and_eq_true, beq_iff_eq] at htip heval have hleval := cache.inv assign heval.right lhs.gate (by omega) hl @@ -346,7 +346,7 @@ def Cache.addGate (cache : Cache aig cnf) {hlb} {hrb} (idx : Nat) (h : idx < aig generalize lhs.invert = linv generalize rhs.invert = rinv cases linv <;> cases rinv <;> simp [hleval, hreval] - · next heq => + next heq => simp only [CNF.eval_append, Decl.gateToCNF_eval, Bool.and_eq_true, beq_iff_eq] at heval have := cache.inv assign heval.right idx hbound hmarked rw [this] diff --git a/src/Std/Sat/AIG/CachedLemmas.lean b/src/Std/Sat/AIG/CachedLemmas.lean index 1ed31ccfe7..77133cbc5a 100644 --- a/src/Std/Sat/AIG/CachedLemmas.lean +++ b/src/Std/Sat/AIG/CachedLemmas.lean @@ -91,7 +91,7 @@ theorem mkAtomCached_eval_eq_mkAtom_eval {aig : AIG α} : ⟦aig.mkAtomCached var, assign⟧ = ⟦aig.mkAtom var, assign⟧ := by simp only [mkAtomCached] split - · next heq1 => + next heq1 => rw [denote_mkAtom_cached heq1] · simp [mkAtom, denote] @@ -105,8 +105,8 @@ theorem denote_mkConstCached {aig : AIG α} : unfold denote denote.go split · simp - · next heq => simp [aig.hconst] at heq - · next heq => simp [aig.hconst] at heq + next heq => simp [aig.hconst] at heq + next heq => simp [aig.hconst] at heq /-- If we find a cached gate declaration in the AIG, denoting it is equivalent to denoting `AIG.mkGate`. @@ -204,7 +204,7 @@ theorem mkGateCached.go_eval_eq_mkGate_eval {aig : AIG α} {input : BinaryInput ⟦go aig input, assign⟧ = ⟦aig.mkGate input, assign⟧ := by simp only [go] split - · next heq1 => + next heq1 => rw [denote_mkGate_cached heq1] · split · simp_all [denote_getConstant] @@ -215,7 +215,7 @@ theorem mkGateCached.go_eval_eq_mkGate_eval {aig : AIG α} {input : BinaryInput split · split · simp_all - · next hif => + next hif => simp_all have := Bool.eq_not_of_ne hif simp_all diff --git a/src/Std/Sat/AIG/LawfulOperator.lean b/src/Std/Sat/AIG/LawfulOperator.lean index 3da14d1297..719d9a94fd 100644 --- a/src/Std/Sat/AIG/LawfulOperator.lean +++ b/src/Std/Sat/AIG/LawfulOperator.lean @@ -58,13 +58,13 @@ theorem denote.go_eq_of_isPrefix (decls1 decls2 : Array (Decl α)) (start : Nat) unfold denote.go have hidx1 := hprefix.idx_eq start hbounds1 split - · next heq => + next heq => rw [hidx1] at heq split <;> simp_all - · next heq => + next heq => rw [hidx1] at heq split <;> simp_all - · next lhs rhs heq => + next lhs rhs heq => rw [hidx1] at heq have := hdag1 hbounds1 heq have hidx2 := hprefix.idx_eq lhs.gate (by omega) diff --git a/src/Std/Sat/AIG/Lemmas.lean b/src/Std/Sat/AIG/Lemmas.lean index 3a83a57edc..e1428e6bec 100644 --- a/src/Std/Sat/AIG/Lemmas.lean +++ b/src/Std/Sat/AIG/Lemmas.lean @@ -125,13 +125,13 @@ theorem denote_mkGate {aig : AIG α} {input : BinaryInput aig} : lhs unfold denote denote.go split - · next heq => + next heq => rw [mkGate, Array.getElem_push_eq] at heq contradiction - · next heq => + next heq => rw [mkGate, Array.getElem_push_eq] at heq contradiction - · next heq => + next heq => rw [mkGate, Array.getElem_push_eq] at heq injection heq with hl hr simp only [← hl, Fanin.gate_mk, mkGate, Fanin.invert_mk, ← hr, Bool.bne_false] @@ -168,14 +168,14 @@ theorem denote_mkAtom {aig : AIG α} : ⟦(aig.mkAtom var), assign⟧ = assign var := by unfold denote denote.go split - · next heq => + next heq => rw [mkAtom, Array.getElem_push_eq] at heq contradiction - · next heq => + next heq => rw [mkAtom, Array.getElem_push_eq] at heq injection heq with heq simp [heq, mkAtom] - · next heq => + next heq => rw [mkAtom, Array.getElem_push_eq] at heq contradiction @@ -207,13 +207,13 @@ instance : LawfulOperator α (fun _ => Bool) mkConst where theorem denote_mkConst {aig : AIG α} : ⟦(aig.mkConst val), assign⟧ = val := by unfold denote denote.go split - · next heq => + next heq => rw [mkConst, Array.getElem_push_eq] at heq simp [mkConst] - · next heq => + next heq => rw [mkConst, Array.getElem_push_eq] at heq contradiction - · next heq => + next heq => rw [mkConst, Array.getElem_push_eq] at heq contradiction @@ -251,7 +251,7 @@ theorem denote_idx_gate {aig : AIG α} {hstart} (h : aig.decls[start] = .gate lh split · simp_all · simp_all - · next heq => + next heq => rw [h] at heq simp_all @@ -306,7 +306,7 @@ theorem of_isConstant {aig : AIG α} {assign : α → Bool} {ref : Ref aig} {b : unfold isConstant at h dsimp only at h split at h - · next heq => + next heq => rw [denote_idx_false heq] cases invert <;> simp_all · contradiction @@ -318,7 +318,7 @@ theorem denote_getConstant {aig : AIG α} {assign : α → Bool} {ref : Ref aig} unfold getConstant at h dsimp only at h split at h - · next heq => + next heq => rw [denote_idx_false heq] cases invert <;> simp_all · contradiction diff --git a/src/Std/Sat/AIG/RefVecOperator/Fold.lean b/src/Std/Sat/AIG/RefVecOperator/Fold.lean index 036ff09d7e..997bad8374 100644 --- a/src/Std/Sat/AIG/RefVecOperator/Fold.lean +++ b/src/Std/Sat/AIG/RefVecOperator/Fold.lean @@ -48,7 +48,7 @@ theorem fold.go_le_size {aig : AIG α} (acc : Ref aig) (idx : Nat) (s : RefVec a aig.decls.size ≤ (go aig acc idx len s f).1.decls.size := by unfold go split - · next h => + next h => dsimp only refine Nat.le_trans ?_ (by apply fold.go_le_size) apply LawfulOperator.le_size diff --git a/src/Std/Sat/AIG/RefVecOperator/Map.lean b/src/Std/Sat/AIG/RefVecOperator/Map.lean index a2e19e3103..2826d86994 100644 --- a/src/Std/Sat/AIG/RefVecOperator/Map.lean +++ b/src/Std/Sat/AIG/RefVecOperator/Map.lean @@ -86,7 +86,7 @@ theorem map.go_le_size {aig : AIG α} (idx : Nat) (hidx) (s : RefVec aig idx) aig.decls.size ≤ (go aig idx hidx s input f).aig.decls.size := by unfold go split - · next h => + next h => dsimp only refine Nat.le_trans ?_ (by apply map.go_le_size) apply LawfulOperator.le_size diff --git a/src/Std/Sat/AIG/Relabel.lean b/src/Std/Sat/AIG/Relabel.lean index d1e96be38c..d694a392c9 100644 --- a/src/Std/Sat/AIG/Relabel.lean +++ b/src/Std/Sat/AIG/Relabel.lean @@ -44,7 +44,7 @@ theorem relabel_atom {decls : Array (Decl α)} {r : α → β} {hidx : idx < dec unfold relabel at h split at h · contradiction - · next x heq => + next x heq => injection h with h exists x simp [heq, h] @@ -162,11 +162,11 @@ theorem relabel_unsat_iff_of_Nonempty [Nonempty α] {aig : AIG α} {r : α → · intro a hmem simp only [Function.comp_apply, g] split - · next h => + next h => rcases Exists.choose_spec h with ⟨_, heq⟩ specialize hinj _ _ (by assumption) (by assumption) heq simp [hinj] - · next h => + next h => simp only [not_exists, not_and] at h specialize h a hmem contradiction diff --git a/src/Std/Sat/AIG/RelabelNat.lean b/src/Std/Sat/AIG/RelabelNat.lean index 276817c4f0..aaf1749e1d 100644 --- a/src/Std/Sat/AIG/RelabelNat.lean +++ b/src/Std/Sat/AIG/RelabelNat.lean @@ -113,7 +113,7 @@ theorem Inv2.property (decls : Array (Decl α)) (idx upper : Nat) (map : HashMap induction hinv with | empty => omega | newAtom ih1 ih2 ih3 ih4 ih5 => - next idx' _ a' _ => + rename_i idx' _ a' _ replace hidx : idx ≤ idx' := by omega rw [HashMap.getElem?_insert] match heq2 : a' == a with @@ -129,7 +129,7 @@ theorem Inv2.property (decls : Array (Decl α)) (idx upper : Nat) (map : HashMap exact Option.isSome_iff_exists.mp rfl | oldAtom ih1 ih2 ih3 ih4 ih5 => simp_all only [true_implies] - next idx' _ _ _ => + rename_i idx' _ _ _ replace hidx : idx ≤ idx' := by omega cases Nat.eq_or_lt_of_le hidx with | inl hidxeq => @@ -139,13 +139,13 @@ theorem Inv2.property (decls : Array (Decl α)) (idx upper : Nat) (map : HashMap assumption | inr hlt => apply ih5 <;> assumption | false ih1 ih2 ih3 ih4 => - next idx' _ => + rename_i idx' _ replace hidx : idx ≤ idx' := by omega cases Nat.eq_or_lt_of_le hidx with | inl hidxeq => simp [hidxeq, ih3] at heq | inr hlt => apply ih4 <;> assumption | gate ih1 ih2 ih3 ih4 => - next idx' _ _ _ => + rename_i idx' _ _ _ replace hidx : idx ≤ idx' := by omega cases Nat.eq_or_lt_of_le hidx with | inl hidxeq => simp [hidxeq, ih3] at heq @@ -335,18 +335,18 @@ theorem relabelNat_unsat_iff_of_NonEmpty [Nonempty α] {aig : AIG α} {hidx1} {h rw [relabel_unsat_iff] intro x y hx hy heq split at heq - · next hcase1 => + next hcase1 => split at heq - · next hcase2 => + next hcase2 => apply RelabelNat.State.ofAIG_find_unique · assumption · rw [heq] assumption - · next hcase2 => + next hcase2 => exfalso rcases RelabelNat.State.ofAIG_find_some y hy with ⟨n, hn⟩ simp [hcase2] at hn - · next hcase => + next hcase => exfalso rcases RelabelNat.State.ofAIG_find_some x hx with ⟨n, hn⟩ simp [hcase] at hn diff --git a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Basic.lean b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Basic.lean index 95a16665f3..12490f55fb 100644 --- a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Basic.lean +++ b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Basic.lean @@ -438,7 +438,7 @@ def eval (assign : Assignment) : BVExpr w → BitVec w theorem eval_var : eval assign ((.var idx) : BVExpr w) = (assign.get idx).bv.truncate w := by rw [eval] split - · next h => + next h => subst h simp · rfl diff --git a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Expr.lean b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Expr.lean index 0538b616d4..82b38302c0 100644 --- a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Expr.lean +++ b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Expr.lean @@ -62,7 +62,7 @@ def Cache.insert (cache : Cache aig) (expr : BVExpr w) (refs : AIG.RefVec aig w) intro i k hk h2 rw [Std.DHashMap.get_insert] split - · next heq => + next heq => rcases k with ⟨w, expr⟩ simp only [beq_iff_eq, Key.mk.injEq] at heq rcases heq with ⟨heq1, heq2⟩ @@ -326,7 +326,7 @@ theorem go_decl_eq (aig : AIG BVBit) (expr : BVExpr w) (cache : Cache aig) : split · rw [AIG.LawfulVecOperator.decl_eq (f := blastVar)] · simp - · next op lhsExpr rhsExpr => + next op lhsExpr rhsExpr => have hl := (goCache aig lhsExpr cache).result.property have hr := (goCache (goCache aig lhsExpr cache).1.1.aig rhsExpr (goCache aig lhsExpr cache).cache).result.property match op with @@ -344,14 +344,14 @@ theorem go_decl_eq (aig : AIG BVBit) (expr : BVExpr w) (cache : Cache aig) : · apply Nat.lt_of_lt_of_le · exact h1 · apply Nat.le_trans <;> assumption - · next op expr => + next op expr => match op with | .not | .rotateLeft .. | .rotateRight .. | .arithShiftRightConst .. | .reverse | .clz => rw [AIG.LawfulVecOperator.decl_eq] rw [goCache_decl_eq] have := (goCache aig expr cache).result.property omega - · next lhsExpr rhsExpr h => + next lhsExpr rhsExpr h => have hl := (goCache aig lhsExpr cache).result.property have hr := (goCache (goCache aig lhsExpr cache).1.1.aig rhsExpr (goCache aig lhsExpr cache).cache).result.property rw [AIG.LawfulVecOperator.decl_eq] @@ -360,17 +360,17 @@ theorem go_decl_eq (aig : AIG BVBit) (expr : BVExpr w) (cache : Cache aig) : · apply Nat.lt_of_lt_of_le · exact h1 · apply Nat.le_trans <;> assumption - · next inner _ => + next inner _ => rw [AIG.LawfulVecOperator.decl_eq (f := blastReplicate)] rw [goCache_decl_eq] have := (goCache aig inner cache).result.property omega - · next hi lo inner => + next hi lo inner => rw [AIG.LawfulVecOperator.decl_eq (f := blastExtract)] rw [goCache_decl_eq] have := (goCache aig inner cache).result.property omega - · next rhsExpr lhsExpr => + next rhsExpr lhsExpr => have hl := (goCache aig lhsExpr cache).result.property have hr := (goCache (goCache aig lhsExpr cache).1.1.aig rhsExpr (goCache aig lhsExpr cache).cache).result.property rw [AIG.LawfulVecOperator.decl_eq (f := blastShiftLeft)] @@ -379,7 +379,7 @@ theorem go_decl_eq (aig : AIG BVBit) (expr : BVExpr w) (cache : Cache aig) : · apply Nat.lt_of_lt_of_le · exact h1 · apply Nat.le_trans <;> assumption - · next rhsExpr lhsExpr => + next rhsExpr lhsExpr => have hl := (goCache aig lhsExpr cache).result.property have hr := (goCache (goCache aig lhsExpr cache).1.1.aig rhsExpr (goCache aig lhsExpr cache).cache).result.property rw [AIG.LawfulVecOperator.decl_eq (f := blastShiftRight)] @@ -388,7 +388,7 @@ theorem go_decl_eq (aig : AIG BVBit) (expr : BVExpr w) (cache : Cache aig) : · apply Nat.lt_of_lt_of_le · exact h1 · apply Nat.le_trans <;> assumption - · next rhsExpr lhsExpr => + next rhsExpr lhsExpr => have hl := (goCache aig lhsExpr cache).result.property have hr := (goCache (goCache aig lhsExpr cache).1.1.aig rhsExpr (goCache aig lhsExpr cache).cache).result.property rw [AIG.LawfulVecOperator.decl_eq (f := blastArithShiftRight)] diff --git a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Expr.lean b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Expr.lean index cd5bf4745e..4d27259e15 100644 --- a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Expr.lean +++ b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Expr.lean @@ -202,7 +202,7 @@ theorem go_Inv_of_Inv (cache : Cache aig) (hinv : Cache.Inv assign aig cache) : apply Cache.Inv_cast · apply IsPrefix.rfl · exact hinv - · next op lhsExpr rhsExpr => + next op lhsExpr rhsExpr => dsimp only at hres match op with | .and | .or | .xor => @@ -282,7 +282,7 @@ theorem goCache_denote_eq (aig : AIG BVBit) (expr : BVExpr w) (assign : Assignme generalize hres : goCache aig expr cache = res unfold goCache at hres split at hres - · next heq => + next heq => rw [← hres] apply Cache.denote_eq_eval_of_get?_eq_some_of_Inv · exact heq @@ -404,7 +404,7 @@ theorem go_denote_eq (aig : AIG BVBit) (expr : BVExpr w) (assign : Assignment) BitVec.getLsbD_eq_getElem, BitVec.getElem_rotateLeft] split all_goals - · rw [goCache_denote_eq] + rw [goCache_denote_eq] · apply BitVec.getLsbD_eq_getElem · exact hinv · rw [← hres] @@ -412,7 +412,7 @@ theorem go_denote_eq (aig : AIG BVBit) (expr : BVExpr w) (assign : Assignment) BitVec.getLsbD_eq_getElem, BitVec.getElem_rotateRight] split all_goals - · rw [goCache_denote_eq] + rw [goCache_denote_eq] · apply BitVec.getLsbD_eq_getElem · exact hinv · rw [← hres] @@ -436,7 +436,7 @@ theorem go_denote_eq (aig : AIG BVBit) (expr : BVExpr w) (assign : Assignment) intro idx hidx rw [goCache_denote_eq] exact hinv - · next h => + next h => subst h rw [← hres] simp only [denote_blastAppend, RefVec.get_cast, Ref.cast_eq, eval_append, BitVec.getLsbD_append] @@ -447,13 +447,13 @@ theorem go_denote_eq (aig : AIG BVBit) (expr : BVExpr w) (assign : Assignment) · rw [goCache_denote_mem_prefix] rw [goCache_denote_eq] exact hinv - · next h => + next h => subst h rw [← hres] simp only [denote_blastReplicate, eval_replicate, hidx, BitVec.getLsbD_eq_getElem, BitVec.getElem_replicate] split - · next h => + next h => simp only [h, Nat.zero_mul, Nat.not_lt_zero] at hidx · rw [goCache_denote_eq] · apply BitVec.getLsbD_eq_getElem diff --git a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/Add.lean b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/Add.lean index 1a6a2c6b9a..52f67b9797 100644 --- a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/Add.lean +++ b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/Add.lean @@ -162,7 +162,7 @@ theorem go_denote_eq (aig : AIG α) (curr : Nat) (hcurr : curr ≤ w) (cin : Ref unfold go at hgo dsimp only at hgo split at hgo - · next hlt => + next hlt => cases Nat.eq_or_lt_of_le hidx2 with | inl heq => rw [← hgo] diff --git a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/Clz.lean b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/Clz.lean index 9dca0b8280..561291e727 100644 --- a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/Clz.lean +++ b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/Clz.lean @@ -53,38 +53,38 @@ theorem go_denote_eq {w : Nat} (aig : AIG α) generalize hgo: go aig xc curr acc = res unfold go at hgo split at hgo - · case isTrue h => - simp only [BitVec.natCast_eq_ofNat, BitVec.ofNat_eq_ofNat] at hgo - rw [← hgo, go_denote_eq] - · intro idx hidx - rw [AIG.LawfulVecOperator.denote_mem_prefix (f := RefVec.ite)] - · simp [hx] - · simp [Ref.hgate] - · intro idx hidx - simp only [Nat.add_eq_zero, Nat.succ_ne_self, and_false, reduceIte, - Nat.add_one_sub_one] - rw [RefVec.denote_ite] - split - · next h => - rw [hx] at h - have : 1 < 2 ^ w := by exact Nat.one_lt_two_pow_iff.mpr (by omega) - rcases curr with _|curr - · simp [denote_blastConst, BitVec.clzAuxRec_zero, h, BitVec.ofNat_sub_ofNat_of_le (x := w) (y := 1) (by omega) (by omega)] - · have := Nat.lt_pow_self (n := curr + 1) (a := 2) (by omega) - have := Nat.pow_lt_pow_of_lt (a := 2) (n := curr + 1) (m := w) (by omega) (by omega) - simp only [denote_blastConst, BitVec.clzAuxRec_succ, h, reduceIte] - rw [BitVec.ofNat_sub_ofNat_of_le (x := w) (y := 1) (by omega) (by omega), - BitVec.ofNat_sub_ofNat_of_le (x := w - 1) (y := curr + 1) (by omega) (by omega)] - · split at hacc - · next h1 h2 => - have hxc : x.getLsbD 0 = false := by rw [hx] at h1; simp [h2] at h1; exact h1 - simp [hacc, h2, BitVec.clzAuxRec_zero, hxc] - · next h1 h2 => - obtain ⟨curr, hcurr⟩ : ∃ curr', curr = curr' + 1 := by apply Nat.exists_eq_add_one.mpr (by omega) - subst hcurr - have hxc : x.getLsbD (curr + 1) = false := by rw [hx] at h1; simp at h1; exact h1 - simp [hacc, BitVec.clzAuxRec_succ, hxc] - · case isFalse h => + case isTrue h => + simp only [BitVec.natCast_eq_ofNat, BitVec.ofNat_eq_ofNat] at hgo + rw [← hgo, go_denote_eq] + · intro idx hidx + rw [AIG.LawfulVecOperator.denote_mem_prefix (f := RefVec.ite)] + · simp [hx] + · simp [Ref.hgate] + · intro idx hidx + simp only [Nat.add_eq_zero, Nat.succ_ne_self, and_false, reduceIte, + Nat.add_one_sub_one] + rw [RefVec.denote_ite] + split + next h => + rw [hx] at h + have : 1 < 2 ^ w := by exact Nat.one_lt_two_pow_iff.mpr (by omega) + rcases curr with _|curr + · simp [denote_blastConst, BitVec.clzAuxRec_zero, h, BitVec.ofNat_sub_ofNat_of_le (x := w) (y := 1) (by omega) (by omega)] + · have := Nat.lt_pow_self (n := curr + 1) (a := 2) (by omega) + have := Nat.pow_lt_pow_of_lt (a := 2) (n := curr + 1) (m := w) (by omega) (by omega) + simp only [denote_blastConst, BitVec.clzAuxRec_succ, h, reduceIte] + rw [BitVec.ofNat_sub_ofNat_of_le (x := w) (y := 1) (by omega) (by omega), + BitVec.ofNat_sub_ofNat_of_le (x := w - 1) (y := curr + 1) (by omega) (by omega)] + · split at hacc + next h1 h2 => + have hxc : x.getLsbD 0 = false := by rw [hx] at h1; simp [h2] at h1; exact h1 + simp [hacc, h2, BitVec.clzAuxRec_zero, hxc] + next h1 h2 => + obtain ⟨curr, hcurr⟩ : ∃ curr', curr = curr' + 1 := by apply Nat.exists_eq_add_one.mpr (by omega) + subst hcurr + have hxc : x.getLsbD (curr + 1) = false := by rw [hx] at h1; simp at h1; exact h1 + simp [hacc, BitVec.clzAuxRec_succ, hxc] + case isFalse h => rw [← hgo] simp only [show ¬curr = 0 by omega, reduceIte] at hacc simp only [hacc, BitVec.clzAuxRec_eq_clzAuxRec_of_le (x := x) (n := curr - 1) (by omega)] diff --git a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/Mul.lean b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/Mul.lean index bdd8939b57..7bfebb9856 100644 --- a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/Mul.lean +++ b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/Mul.lean @@ -52,7 +52,7 @@ theorem go_denote_eq {w : Nat} (aig : AIG α) (curr : Nat) (hcurr : curr + 1 ≤ unfold go at hgo split at hgo · split at hgo - · next hconstant => + next hconstant => rw [← hgo] rw [go_denote_eq] · omega @@ -84,7 +84,7 @@ theorem go_denote_eq {w : Nat} (aig : AIG α) (curr : Nat) (hcurr : curr + 1 ≤ rw [BitVec.mulRec_succ_eq] simp only [RefVec.denote_ite, RefVec.get_cast, Ref.cast_eq, BitVec.ofNat_eq_ofNat] split - · next hdiscr => + next hdiscr => have : rexpr.getLsbD (curr + 1) = true := by rw [AIG.LawfulVecOperator.denote_mem_prefix (f := blastAdd)] at hdiscr rw [AIG.LawfulVecOperator.denote_mem_prefix (f := blastShiftLeftConst)] at hdiscr @@ -99,11 +99,11 @@ theorem go_denote_eq {w : Nat} (aig : AIG α) (curr : Nat) (hcurr : curr + 1 ≤ · intros simp only [denote_blastShiftLeftConst, BitVec.getLsbD_shiftLeft] split - · next hdiscr => simp [hdiscr] - · next hidx hdiscr => + next hdiscr => simp [hdiscr] + next hidx hdiscr => rw [hleft] simp [hdiscr, hidx] - · next hdiscr => + next hdiscr => have : rexpr.getLsbD (curr + 1) = false := by rw [AIG.LawfulVecOperator.denote_mem_prefix (f := blastAdd)] at hdiscr rw [AIG.LawfulVecOperator.denote_mem_prefix (f := blastShiftLeftConst)] at hdiscr @@ -139,7 +139,7 @@ theorem denote_blast (aig : AIG α) (lhs rhs : BitVec w) (assign : α → Bool) dsimp only at hb split at hb · omega - · next hne => + next hne => have := Nat.exists_eq_succ_of_ne_zero hne rcases this with ⟨w, hw⟩ subst hw @@ -161,11 +161,11 @@ theorem denote_blast (aig : AIG α) (lhs rhs : BitVec w) (assign : α → Bool) BitVec.ofNat_eq_ofNat, BitVec.getLsbD_zero, Bool.if_false_right, Bool.decide_eq_true] split - · next heq => + next heq => rw [← hright] at heq · simp [heq, hleft] · omega - · next heq => + next heq => simp only [Bool.not_eq_true] at heq rw [← hright] at heq · simp [heq] diff --git a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/ShiftLeft.lean b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/ShiftLeft.lean index 9ad9d014f8..8ef4025859 100644 --- a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/ShiftLeft.lean +++ b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/ShiftLeft.lean @@ -127,19 +127,19 @@ theorem go_denote_eq (aig : AIG α) (distance : Nat) (input : AIG.RefVec aig w) | inr => split at hgo · split - · next hidx => + next hidx => rw [← hgo] rw [go_denote_eq] · simp [hidx] · omega - · next hidx => + next hidx => rw [← hgo] rw [go_denote_eq] · simp [hidx] · omega · split · omega - · next hidx => + next hidx => rw [← hgo] rw [go_denote_eq] · simp [hidx] @@ -191,7 +191,7 @@ theorem twoPowShift_eq (aig : AIG α) (target : TwoPowShiftTarget aig w) (lhs : dsimp only at hg split at hg · split - · next hif1 => + next hif1 => rw [← hg] simp only [RefVec.denote_ite, RefVec.get_cast, Ref.cast_eq, denote_blastShiftLeftConst] @@ -213,7 +213,7 @@ theorem twoPowShift_eq (aig : AIG α) (target : TwoPowShiftTarget aig w) (lhs : decide_true, Bool.true_and, Bool.eq_and_self, Bool.not_eq_true', decide_eq_false_iff_not, Nat.not_lt] omega - · next hif1 => + next hif1 => simp only [Bool.not_eq_true] at hif1 rw [← hg] simp only [RefVec.denote_ite, RefVec.get_cast, Ref.cast_eq, @@ -289,7 +289,7 @@ theorem denote_blastShiftLeft (aig : AIG α) (target : ArbitraryShiftTarget aig unfold blastShiftLeft at hg dsimp only at hg split at hg - · next hzero => + next hzero => dsimp only subst hzero rw [← hg] diff --git a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/ShiftRight.lean b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/ShiftRight.lean index c5551db63c..91e36f8801 100644 --- a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/ShiftRight.lean +++ b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/ShiftRight.lean @@ -135,7 +135,7 @@ theorem go_denote_eq (aig : AIG α) (distance : Nat) (input : AIG.RefVec aig w) · omega · split · omega - · next hidx => + next hidx => rw [← hgo] rw [go_denote_eq] · simp [hidx] @@ -208,7 +208,7 @@ theorem go_denote_eq (aig : AIG α) (distance : Nat) (input : AIG.RefVec aig w) · cases Nat.eq_or_lt_of_le hidx2 with | inl heq => split at hgo - · next hlt => + next hlt => rw [heq] at hlt simp only [hlt, ↓reduceDIte] dsimp only at hgo @@ -217,7 +217,7 @@ theorem go_denote_eq (aig : AIG α) (distance : Nat) (input : AIG.RefVec aig w) rw [AIG.RefVec.get_push_ref_eq'] · simp [heq] · omega - · next hlt => + next hlt => rw [heq] at hlt simp only [hlt, ↓reduceDIte] dsimp only at hgo @@ -281,7 +281,7 @@ theorem twoPowShift_eq (aig : AIG α) (target : TwoPowShiftTarget aig w) (lhs : dsimp only at hg split at hg · split - · next hif1 => + next hif1 => rw [← hg] simp only [RefVec.denote_ite, RefVec.get_cast, Ref.cast_eq, denote_blastShiftRightConst] @@ -298,7 +298,7 @@ theorem twoPowShift_eq (aig : AIG α) (target : TwoPowShiftTarget aig w) (lhs : Bool.false_eq] apply BitVec.getLsbD_of_ge omega - · next hif1 => + next hif1 => simp only [Bool.not_eq_true] at hif1 rw [← hg] simp only [RefVec.denote_ite, RefVec.get_cast, Ref.cast_eq, @@ -374,7 +374,7 @@ theorem denote_blastShiftRight (aig : AIG α) (target : ArbitraryShiftTarget aig unfold blastShiftRight at hres dsimp only at hres split at hres - · next hzero => + next hzero => dsimp only subst hzero rw [← hres] @@ -414,7 +414,7 @@ theorem twoPowShift_eq (aig : AIG α) (target : TwoPowShiftTarget aig w) (lhs : dsimp only at hg split at hg · split - · next hif1 => + next hif1 => rw [← hg] simp only [RefVec.denote_ite, RefVec.get_cast, Ref.cast_eq, denote_blastArithShiftRightConst] @@ -425,13 +425,13 @@ theorem twoPowShift_eq (aig : AIG α) (target : TwoPowShiftTarget aig w) (lhs : apply Nat.mod_eq_of_lt apply Nat.pow_lt_pow_of_lt <;> omega split - · next hlt => + next hlt => rw [hleft] simp [hmod, BitVec.getElem_sshiftRight, hlt, hidx] - · next hlt => + next hlt => rw [hleft] simp [BitVec.getElem_sshiftRight, hmod, hlt, hidx, BitVec.msb_eq_getLsbD_last] - · next hif1 => + next hif1 => simp only [Bool.not_eq_true] at hif1 rw [← hg] simp only [RefVec.denote_ite, RefVec.get_cast, Ref.cast_eq, @@ -507,7 +507,7 @@ theorem denote_blastArithShiftRight (aig : AIG α) (target : ArbitraryShiftTarge unfold blastArithShiftRight at hres dsimp only at hres split at hres - · next hzero => + next hzero => dsimp only subst hzero rw [← hres] diff --git a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/Udiv.lean b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/Udiv.lean index 50e673aaea..9864f47499 100644 --- a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/Udiv.lean +++ b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/Udiv.lean @@ -169,7 +169,7 @@ theorem denote_blastDivSubtractShift_r (aig : AIG α) (assign : α → Bool) (lh simp only [RefVec.denote_ite, LawfulVecOperator.denote_cast_entry, RefVec.get_cast] rw [BVPred.mkUlt_denote_eq (lhs := rbv.shiftConcat (lhs.getLsbD (wn - 1))) (rhs := rhs)] · split - · next hdiscr => + next hdiscr => rw [← Normalize.BitVec.lt_ult] at hdiscr simp only [Ref.cast_eq, hdiscr, ↓reduceIte] rw [AIG.LawfulVecOperator.denote_mem_prefix (f := AIG.RefVec.ite)] @@ -183,7 +183,7 @@ theorem denote_blastDivSubtractShift_r (aig : AIG α) (assign : α → Bool) (lh · rw [BVPred.denote_getD_eq_getLsbD] · exact hleft · simp - · next hdiscr => + next hdiscr => rw [← Normalize.BitVec.lt_ult] at hdiscr simp only [Ref.cast_eq, hdiscr, ↓reduceIte] rw [AIG.LawfulVecOperator.denote_mem_prefix (f := AIG.RefVec.ite)] @@ -271,7 +271,7 @@ theorem denote_go_eq_divRec_q (aig : AIG α) (assign : α → Bool) (curr : Nat) intro idx hidx rw [go, BitVec.divRec_succ, BitVec.divSubtractShift] split - · next hdiscr => + next hdiscr => rw [ih] · rfl · intro idx hidx @@ -297,7 +297,7 @@ theorem denote_go_eq_divRec_q (aig : AIG α) (assign : α → Bool) (curr : Nat) · exact hleft · exact hright · exact hr - · next hdiscr => + next hdiscr => rw [ih] · rfl · intro idx hidx @@ -380,7 +380,7 @@ theorem denote_blastUdiv (aig : AIG α) (lhs rhs : BitVec w) (assign : α → Bo simp only [Ref.cast_eq, RefVec.denote_ite, RefVec.get_cast] split - · next hdiscr => + next hdiscr => rw [blastUdiv.go_denote_mem_prefix] at hdiscr rw [BVPred.mkEq_denote_eq (lhs := rhs) (rhs := 0#w)] at hdiscr · simp only [beq_iff_eq] at hdiscr @@ -393,7 +393,7 @@ theorem denote_blastUdiv (aig : AIG α) (lhs rhs : BitVec w) (assign : α → Bo simp [hright] · intro idx hidx simp - · next hdiscr => + next hdiscr => rw [blastUdiv.go_denote_mem_prefix] at hdiscr rw [BVPred.mkEq_denote_eq (lhs := rhs) (rhs := 0#w)] at hdiscr · have hzero : 0#w < rhs := by diff --git a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/Umod.lean b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/Umod.lean index 4ec1d9b155..221539fa63 100644 --- a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/Umod.lean +++ b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/Umod.lean @@ -53,7 +53,7 @@ theorem denote_go_eq_divRec_r (aig : AIG α) (assign : α → Bool) (curr : Nat) intro idx hidx rw [go, BitVec.divRec_succ, BitVec.divSubtractShift] split - · next hdiscr => + next hdiscr => rw [ih] · rfl · intro idx hidx @@ -79,7 +79,7 @@ theorem denote_go_eq_divRec_r (aig : AIG α) (assign : α → Bool) (curr : Nat) · exact hleft · exact hright · exact hr - · next hdiscr => + next hdiscr => rw [ih] · rfl · intro idx hidx @@ -146,7 +146,7 @@ theorem denote_blastUmod (aig : AIG α) (lhs rhs : BitVec w) (assign : α → Bo simp only [Ref.cast_eq, RefVec.denote_ite, RefVec.get_cast] split - · next hdiscr => + next hdiscr => rw [blastUdiv.go_denote_mem_prefix] at hdiscr rw [BVPred.mkEq_denote_eq (lhs := rhs) (rhs := 0#w)] at hdiscr · simp only [beq_iff_eq] at hdiscr @@ -161,7 +161,7 @@ theorem denote_blastUmod (aig : AIG α) (lhs rhs : BitVec w) (assign : α → Bo simp only [BitVec.getLsbD_zero] rw [denote_blastConst] simp - · next hdiscr => + next hdiscr => rw [blastUdiv.go_denote_mem_prefix] at hdiscr rw [BVPred.mkEq_denote_eq (lhs := rhs) (rhs := 0#w)] at hdiscr · have hzero : 0#w < rhs := by diff --git a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/ZeroExtend.lean b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/ZeroExtend.lean index d61ef2efca..b4b2f61a93 100644 --- a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/ZeroExtend.lean +++ b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/ZeroExtend.lean @@ -104,7 +104,7 @@ theorem go_denote_eq (aig : AIG α) (w : Nat) (input : AIG.RefVec aig w) (newWid cases Nat.eq_or_lt_of_le hidx2 with | inl heq => split at hgo - · next hsplit => + next hsplit => rw [heq] at hsplit simp only [hsplit, ↓reduceDIte] rw [← hgo] @@ -114,7 +114,7 @@ theorem go_denote_eq (aig : AIG α) (w : Nat) (input : AIG.RefVec aig w) (newWid · simp [heq] · simp [Ref.hgate] · omega - · next hsplit => + next hsplit => rw [heq] at hsplit simp only [hsplit, ↓reduceDIte] rw [← hgo] diff --git a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Pred.lean b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Pred.lean index 588b6c6249..d7a8d2829f 100644 --- a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Pred.lean +++ b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Pred.lean @@ -52,7 +52,7 @@ theorem bitblast_Inv_of_Inv (input : BVExpr.WithCache BVPred aig) unfold bitblast dsimp only split - · next op _ _ => + next op _ _ => cases op · dsimp only apply BVExpr.Cache.Inv_cast diff --git a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Var.lean b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Var.lean index 359cc60d7c..a24a5e5a27 100644 --- a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Var.lean +++ b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Var.lean @@ -94,7 +94,7 @@ theorem go_denote_eq (aig : AIG BVBit) (a : Nat) (assign : Assignment) (curr : N generalize hgo : go aig w a curr s hcurr = res unfold go at hgo split at hgo - · next hlt => + next hlt => dsimp only at hgo cases Nat.eq_or_lt_of_le hidx2 with | inl heq => diff --git a/src/Std/Tactic/BVDecide/LRAT/Internal/Convert.lean b/src/Std/Tactic/BVDecide/LRAT/Internal/Convert.lean index 8928b669ee..878ae761c9 100644 --- a/src/Std/Tactic/BVDecide/LRAT/Internal/Convert.lean +++ b/src/Std/Tactic/BVDecide/LRAT/Internal/Convert.lean @@ -137,7 +137,7 @@ theorem CNF.unsat_of_convertLRAT_unsat (cnf : CNF Nat) : rcases hlclause with ⟨reflectClause, ⟨hrclause1, hrclause2⟩⟩ simp only [CNF.eval, List.all_eq_true] at h2 split at hrclause2 - · next heq => + next heq => rw [← heq] at hrclause2 simp only [Option.some.injEq] at hrclause2 simp [CNF.Clause.convertLRAT_sat_of_sat reflectClause hrclause2, h2 reflectClause hrclause1] diff --git a/src/Std/Tactic/BVDecide/LRAT/Internal/Entails.lean b/src/Std/Tactic/BVDecide/LRAT/Internal/Entails.lean index ccba00b160..fc215f16b1 100644 --- a/src/Std/Tactic/BVDecide/LRAT/Internal/Entails.lean +++ b/src/Std/Tactic/BVDecide/LRAT/Internal/Entails.lean @@ -112,9 +112,9 @@ theorem unsat_of_limplies_and_incompatible (α : Type u) {σ1 : Type v} {σ2 : T Limplies α f1 f2 → Incompatible α f1 f2 → Unsatisfiable α f1 := by intro h1 h2 a af1 cases h2 a - · next h2 => + next h2 => exact h2 af1 - · next h2 => + next h2 => exact h2 <| h1 a af1 protected theorem Incompatible.symm {α : Type u} {σ1 : Type v} {σ2 : Type w} [Entails α σ1] diff --git a/src/Std/Tactic/BVDecide/LRAT/Internal/Formula/Lemmas.lean b/src/Std/Tactic/BVDecide/LRAT/Internal/Formula/Lemmas.lean index 448672c4ff..84ff1baf1f 100644 --- a/src/Std/Tactic/BVDecide/LRAT/Internal/Formula/Lemmas.lean +++ b/src/Std/Tactic/BVDecide/LRAT/Internal/Formula/Lemmas.lean @@ -72,10 +72,10 @@ theorem limplies_of_assignmentsInvariant {n : Nat} (f : DefaultFormula n) intro i specialize f_AssignmentsInvariant i (decide (p i = false)) by_cases hasAssignment (decide (p i = false)) (f.assignments[i.1]'(by rw [hsize]; exact i.2.2)) - · next h => + next h => specialize f_AssignmentsInvariant h p pf by_cases hpi : p i <;> simp [hpi, Entails.eval] at f_AssignmentsInvariant - · next h => simp_all [i.2.2] + next h => simp_all [i.2.2] /-- performRupAdd adds to f.rupUnits and then clears f.rupUnits. If f begins with some units in f.rupUnits, @@ -133,7 +133,7 @@ theorem readyForRupAdd_ofArray {n : Nat} (arr : Array (Option (DefaultClause n)) simp only [ofArray_fold_fn] at h split at h · exact ih.2 i b h - · next cOpt c => + next cOpt c => match heq : isUnit c with | none => simp only [heq] at h @@ -142,10 +142,10 @@ theorem readyForRupAdd_ofArray {n : Nat} (arr : Array (Option (DefaultClause n)) simp only [heq] at h rcases ih with ⟨hsize, ih⟩ by_cases i = l.1 - · next i_eq_l => + next i_eq_l => simp only [i_eq_l, Array.getElem_modify_self] at h by_cases b - · next b_eq_true => + next b_eq_true => rw [isUnit_iff, DefaultClause.toList] at heq simp only [toList, ofArray, List.map, List.append_nil, List.mem_filterMap, id_eq, exists_eq_right] have i_eq_l : i = l := Subtype.ext i_eq_l @@ -153,28 +153,28 @@ theorem readyForRupAdd_ofArray {n : Nat} (arr : Array (Option (DefaultClause n)) have c_def : c = ⟨c.clause, c.nodupkey, c.nodup⟩ := rfl simp only [heq] at c_def grind - · next b_eq_false => + next b_eq_false => simp only [Bool.not_eq_true] at b_eq_false simp only [hasAssignment, b_eq_false, ite_false, hasNeg_addPos, reduceCtorEq] at h specialize ih l false simp only [hasAssignment] at ih rw [b_eq_false, Subtype.ext i_eq_l] exact ih h - · next i_ne_l => grind + next i_ne_l => grind | some (l, false) => simp only [heq] at h rcases ih with ⟨hsize, ih⟩ by_cases i = l.1 - · next i_eq_l => + next i_eq_l => simp only [i_eq_l, Array.getElem_modify_self] at h by_cases b - · next b_eq_true => + next b_eq_true => simp only [hasAssignment, b_eq_true, ite_true, hasPos_addNeg] at h specialize ih l true simp only [hasAssignment] at ih rw [b_eq_true, Subtype.ext i_eq_l] grind - · next b_eq_false => + next b_eq_false => rw [isUnit_iff, DefaultClause.toList] at heq simp only [toList, ofArray, List.map, List.append_nil, List.mem_filterMap, id_eq, exists_eq_right] have i_eq_l : i = l := Subtype.ext i_eq_l @@ -182,7 +182,7 @@ theorem readyForRupAdd_ofArray {n : Nat} (arr : Array (Option (DefaultClause n)) have c_def : c = ⟨c.clause, c.nodupkey, c.nodup⟩ := rfl simp only [heq] at c_def grind - · next i_ne_l => grind + next i_ne_l => grind rcases List.foldlRecOn arr.toList ofArray_fold_fn hb hl with ⟨_h_size, h'⟩ grind [ofArray] @@ -218,7 +218,7 @@ theorem readyForRupAdd_insert {n : Nat} (f : DefaultFormula n) (c : DefaultClaus have hf := f_readyForRupAdd.2.2 i b hb simp only [toList] at hf ⊢ grind - · next l hc => + next l hc => have hsize : (Array.modify f.assignments l.1 addPosAssignment).size = n := by rw [Array.size_modify, f_readyForRupAdd.2.1] refine ⟨f_readyForRupAdd.1, hsize, ?_⟩ @@ -227,29 +227,29 @@ theorem readyForRupAdd_insert {n : Nat} (f : DefaultFormula n) (c : DefaultClaus have i_in_bounds : i.1 < f.assignments.size := by rw [f_readyForRupAdd.2.1]; exact i.2.2 simp only at hb by_cases (i, b) = (l, true) - · next ib_eq_c => + next ib_eq_c => simp only [toList, Array.toList_push, List.append_assoc, List.mem_append, List.mem_filterMap, List.mem_singleton, id_eq, exists_eq_right, Option.some.injEq, List.mem_map, Prod.exists, Bool.exists_bool] apply Or.inl ∘ Or.inr rw [isUnit_iff, DefaultClause.toList, ← ib_eq_c] at hc apply DefaultClause.ext simp only [unit, hc] - · next ib_ne_c => + next ib_ne_c => have hb' : hasAssignment b f.assignments[i.1] := by by_cases l.1 = i.1 - · next l_eq_i => + next l_eq_i => have b_eq_false : b = false := by by_cases b = true - · next b_eq_true => + next b_eq_true => simp only [b_eq_true, Subtype.ext l_eq_i, not_true] at ib_ne_c - · next b_eq_false => grind + next b_eq_false => grind simp only [hasAssignment, b_eq_false, l_eq_i, Array.getElem_modify_self, ite_false, hasNeg_addPos, reduceCtorEq] at hb grind [hasAssignment] - · next l_ne_i => grind + next l_ne_i => grind specialize hf hb' simp only [toList] at hf ⊢ grind - · next l hc => + next l hc => have hsize : (Array.modify f.assignments l.1 addNegAssignment).size = n := by rw [Array.size_modify, f_readyForRupAdd.2.1] refine ⟨f_readyForRupAdd.1, hsize, ?_⟩ @@ -258,24 +258,24 @@ theorem readyForRupAdd_insert {n : Nat} (f : DefaultFormula n) (c : DefaultClaus have i_in_bounds : i.1 < f.assignments.size := by rw [f_readyForRupAdd.2.1]; exact i.2.2 simp only at hb by_cases (i, b) = (l, false) - · next ib_eq_c => + next ib_eq_c => simp only [toList, Array.toList_push, List.append_assoc, List.mem_append, List.mem_filterMap, List.mem_singleton, id_eq, exists_eq_right, Option.some.injEq, List.mem_map, Prod.exists, Bool.exists_bool] apply Or.inl ∘ Or.inr rw [isUnit_iff, DefaultClause.toList, ← ib_eq_c] at hc apply DefaultClause.ext simp only [unit, hc] - · next ib_ne_c => + next ib_ne_c => have hb' : hasAssignment b f.assignments[i.1] := by by_cases l.1 = i.1 - · next l_eq_i => + next l_eq_i => have b_eq_false : b = true := by by_cases b = true · assumption - · next b_eq_false => + next b_eq_false => simp only [b_eq_false, Subtype.ext l_eq_i, not_true] at ib_ne_c grind [hasAssignment, hasPos_addNeg] - · next l_ne_i => grind + next l_ne_i => grind specialize hf hb' simp only [toList] at hf ⊢ grind @@ -376,7 +376,7 @@ theorem deleteOne_preserves_strongAssignmentsInvariant {n : Nat} (f : DefaultFor simp only [hl] simp only [deleteOne, heq, hl] at hb by_cases l.1.1 = i.1 - · next l_eq_i => + next l_eq_i => simp only [l_eq_i, Array.getElem_modify_self] at hb have l_ne_b : l.2 ≠ b := by grind [not_has_remove] replace l_ne_b := Bool.eq_not_of_ne l_ne_b @@ -398,7 +398,7 @@ theorem deleteOne_preserves_strongAssignmentsInvariant {n : Nat} (f : DefaultFor grind [unit] · exact hf · exact Or.inr hf - · next l_ne_i => + next l_ne_i => simp only [Array.getElem_modify_of_ne l_ne_i] at hb specialize hf i b hb simp only [toList, List.append_assoc, List.mem_append, List.mem_filterMap, id_eq, @@ -418,8 +418,8 @@ theorem deleteOne_preserves_strongAssignmentsInvariant {n : Nat} (f : DefaultFor · exact Or.inr hf · simp only [Prod.exists, Bool.exists_bool, not_exists, not_or, unit] at hl split - · next some_eq_none => grind - · next l _ _ heq => grind [cases Bool] + next some_eq_none => grind + next l _ _ heq => grind [cases Bool] · have deleteOne_f_rw : deleteOne f id = ⟨Array.set! f.clauses id none, f.rupUnits, f.ratUnits, f.assignments⟩ := by simp only [deleteOne] grind diff --git a/src/Std/Tactic/BVDecide/LRAT/Internal/Formula/RatAddResult.lean b/src/Std/Tactic/BVDecide/LRAT/Internal/Formula/RatAddResult.lean index 4b14d68c44..610d35a70f 100644 --- a/src/Std/Tactic/BVDecide/LRAT/Internal/Formula/RatAddResult.lean +++ b/src/Std/Tactic/BVDecide/LRAT/Internal/Formula/RatAddResult.lean @@ -105,7 +105,7 @@ theorem formula_performRatCheck {n : Nat} (f : DefaultFormula n) (performRatCheck f p ratHint).1 = f := by simp only [performRatCheck, Bool.or_eq_true, Bool.not_eq_true'] split - · next c _ => + next c _ => split · rw [clear_insertRat f hf] · let fc := (insertRatUnits f (negate (DefaultClause.delete c p))).1 @@ -154,7 +154,7 @@ theorem ratAdd_result {n : Nat} (f : DefaultFormula n) (c : DefaultClause n) (p · grind · split at ratAddSuccess · grind - · next performRatCheck_fold_success => + next performRatCheck_fold_success => simp only [Bool.not_eq_false] at performRatCheck_fold_success let fc := (insertRupUnits f (negate c)).1 have fc_assignments_size : (insertRupUnits f (negate c)).1.assignments.size = n := by diff --git a/src/Std/Tactic/BVDecide/LRAT/Internal/Formula/RatAddSound.lean b/src/Std/Tactic/BVDecide/LRAT/Internal/Formula/RatAddSound.lean index 4df379c75c..0d9f26d8e4 100644 --- a/src/Std/Tactic/BVDecide/LRAT/Internal/Formula/RatAddSound.lean +++ b/src/Std/Tactic/BVDecide/LRAT/Internal/Formula/RatAddSound.lean @@ -35,14 +35,14 @@ theorem mem_of_necessary_assignment {n : Nat} {p : (PosFin n) → Bool} {c : Def have h := p'_not_entails_c.1 v_in_c simp only [Bool.not_eq_false] at h split at h - · next heq => simp [Literal.negate, ← heq, h, v_in_c] - · next hne => simp [h] at pv + next heq => simp [Literal.negate, ← heq, h, v_in_c] + next hne => simp [h] at pv · specialize p'_not_entails_c v have h := p'_not_entails_c.2 v_in_c simp only at h split at h - · next heq => simp [Literal.negate, ← heq, h, v_in_c] - · next hne => simp [h] at pv + next heq => simp [Literal.negate, ← heq, h, v_in_c] + next hne => simp [h] at pv theorem entails_of_irrelevant_assignment {n : Nat} {p : (PosFin n) → Bool} {c : DefaultClause n} {l : Literal (PosFin n)} (p_entails_cl : p ⊨ c.delete (Literal.negate l)) : @@ -90,7 +90,7 @@ theorem assignmentsInvariant_insertRatUnits {n : Nat} (f : DefaultFormula n) exact hf.2.2 i b hb p pf · rw [h2] at hb by_cases b = b' - · next b_eq_b' => + next b_eq_b' => let j_unit := unit (insertRatUnits f units).1.ratUnits[j] have j_unit_def : j_unit = unit (insertRatUnits f units).1.ratUnits[j] := rfl have j_unit_in_insertRatUnits_res : @@ -133,7 +133,7 @@ theorem assignmentsInvariant_insertRatUnits {n : Nat} (f : DefaultFormula n) · simp only [b_eq_b', ← hp1.2, (· ⊨ ·)] rw [hp1.1] at hp2 exact hp2 - · next b_ne_b' => + next b_ne_b' => apply hf.2.2 i b _ p pf have b'_def : b' = (decide ¬b = true) := by cases b <;> cases b' <;> simp at * rw [has_iff_has_add_complement, ← b'_def, hb] @@ -282,13 +282,13 @@ theorem sat_of_insertRat {n : Nat} (f : DefaultFormula n) simp only [addAssignment, ← b_eq_true, addPosAssignment, ite_true] at h2 split at h2 · simp at h2 - · next heq => + next heq => have hasNegAssignment_fi : hasAssignment false (f.assignments[i.1]'i_in_bounds) := by simp +decide only [hasAssignment, hasPosAssignment, heq] have p_entails_i := hf.2.2 i false hasNegAssignment_fi p pf simp only [(· ⊨ ·)] at p_entails_i simp only [p_entails_i, decide_true] - · next heq => + next heq => exfalso rw [heq] at h3 exact h3 (has_both b) @@ -298,14 +298,14 @@ theorem sat_of_insertRat {n : Nat} (f : DefaultFormula n) apply And.intro i_true_in_c simp only [addAssignment, ← b_eq_false, addNegAssignment, ite_false, reduceCtorEq] at h2 split at h2 - · next heq => + next heq => have hasPosAssignment_fi : hasAssignment true (f.assignments[i.1]'i_in_bounds) := by simp only [hasAssignment, hasPosAssignment, ite_true, heq] have p_entails_i := hf.2.2 i true hasPosAssignment_fi p pf simp only [(· ⊨ ·)] at p_entails_i exact p_entails_i · simp at h2 - · next heq => + next heq => exfalso rw [heq] at h3 exact h3 (has_both b) @@ -388,11 +388,11 @@ theorem c_without_negPivot_of_performRatCheck_success {n : Nat} (f : DefaultForm intro hc p pf simp only [performRatCheck, hc, Bool.or_eq_true, Bool.not_eq_true'] at performRatCheck_success split at performRatCheck_success - · next h => + next h => exact sat_of_insertRat f hf (c.delete negPivot) p pf h · split at performRatCheck_success · simp at performRatCheck_success - · next h => + next h => simp only [not_or, Bool.not_eq_true, Bool.not_eq_false] at h have pfc : p ⊨ f.insert (c.delete negPivot) := safe_insert_of_performRupCheck_insertRat f hf (c.delete negPivot) ratHint.2 h.2 p pf @@ -457,7 +457,7 @@ theorem performRatCheck_success_of_performRatCheck_fold_success {n : Nat} (f : D · intro h i rw [fold_fn_def] at h split at h - · next acc_eq_true => + next acc_eq_true => have i_lt_or_eq_idx : i.1 < idx.1 ∨ i.1 = idx.1 := by omega -- FIXME: why can't `grind` to this? rcases i_lt_or_eq_idx with i_lt_idx | i_eq_idx @@ -581,7 +581,7 @@ theorem ratAdd_sound {n : Nat} (f : DefaultFormula n) (c : DefaultClause n) rw [performRatAdd] at ratAddSuccess simp only [Bool.not_eq_true'] at ratAddSuccess split at ratAddSuccess - · next ratHintsExhaustive_eq_true => + next ratHintsExhaustive_eq_true => split at ratAddSuccess · simp at ratAddSuccess · split at ratAddSuccess @@ -590,7 +590,7 @@ theorem ratAdd_sound {n : Nat} (f : DefaultFormula n) (c : DefaultClause n) · simp at ratAddSuccess · split at ratAddSuccess · simp at ratAddSuccess - · next performRatCheck_fold_success => + next performRatCheck_fold_success => simp only [Bool.not_eq_false] at performRatCheck_fold_success rw [f'_def] exact safe_insert_of_performRatCheck_fold_success f f_readyForRatAdd c pivot rupHints ratHints pivot_in_c diff --git a/src/Std/Tactic/BVDecide/LRAT/Internal/Formula/RupAddResult.lean b/src/Std/Tactic/BVDecide/LRAT/Internal/Formula/RupAddResult.lean index ef6dc0ef7c..a335a1abab 100644 --- a/src/Std/Tactic/BVDecide/LRAT/Internal/Formula/RupAddResult.lean +++ b/src/Std/Tactic/BVDecide/LRAT/Internal/Formula/RupAddResult.lean @@ -85,7 +85,7 @@ theorem insertUnitInvariant_insertUnit {n : Nat} (assignments0 : Array Assignmen have l_in_bounds : l.1.1 < assignments.size := by rw [assignments_size]; exact l.1.2.2 rcases h with ⟨h1, h2⟩ | ⟨j, b, i_gt_zero, h1, h2, h3, h4⟩ | ⟨j1, j2, i_gt_zero, h1, h2, h3, h4, h5⟩ · by_cases hasAssignment l.2 assignments[l.1.1]! - · next h3 => + next h3 => apply Or.inl simp only [insertUnit, h3, ite_true] constructor @@ -95,9 +95,9 @@ theorem insertUnitInvariant_insertUnit {n : Nat} (assignments0 : Array Assignmen simp [insertUnit, h3] let j' : Fin (Array.size units) := ⟨j.1, by rw [← hsize]; exact j.2⟩ exact h2 j' - · next h3 => + next h3 => by_cases i.1 = l.1.1 - · next i_eq_l => + next i_eq_l => apply Or.inr ∘ Or.inl have units_size_lt_updatedUnits_size : units.size < (insertUnit (units, assignments, foundContradiction) l).1.size := by simp only [insertUnit] @@ -123,7 +123,7 @@ theorem insertUnitInvariant_insertUnit {n : Nat} (assignments0 : Array Assignmen rw [Array.getElem_push_lt k_in_bounds] rw [i_eq_l] at h2 exact h2 ⟨k.1, k_in_bounds⟩ - · next i_ne_l => + next i_ne_l => apply Or.inl simp only [insertUnit, h3, ite_false, reduceCtorEq] rw [Array.getElem_modify_of_ne (Ne.symm i_ne_l)] @@ -136,7 +136,7 @@ theorem insertUnitInvariant_insertUnit {n : Nat} (assignments0 : Array Assignmen exact h2 ⟨j.1, h⟩ · grind · by_cases hasAssignment l.2 assignments[l.1.1]! - · next h5 => + next h5 => apply Or.inr ∘ Or.inl have j_lt_updatedUnits_size : j.1 < (insertUnit (units, assignments, foundContradiction) l).1.size := by simp only [insertUnit, h5, ite_true] @@ -152,9 +152,9 @@ theorem insertUnitInvariant_insertUnit {n : Nat} (assignments0 : Array Assignmen intro k_eq_j simp only [← Fin.val_eq_of_eq k_eq_j, not_true] at k_ne_j exact h4 ⟨k.1, k_size⟩ k_ne_j - · next h5 => + next h5 => by_cases i.1 = l.1.1 - · next i_eq_l => + next i_eq_l => apply Or.inr ∘ Or.inr have units_size_lt_updatedUnits_size : units.size < (insertUnit (units, assignments, foundContradiction) l).1.size := by simp only [insertUnit] @@ -250,7 +250,7 @@ theorem insertUnitInvariant_insertUnit {n : Nat} (assignments0 : Array Assignmen simp [i_in_bounds] rw [hl, ← i_eq_l, assignments_i_rw, h2] at h5 exact h5 (has_add _ false) - · next i_ne_l => + next i_ne_l => apply Or.inr ∘ Or.inl have j_lt_updatedUnits_size : j.1 < (insertUnit (units, assignments, foundContradiction) l).1.size := by simp only [insertUnit, h5, ite_false, Array.size_push, reduceCtorEq] @@ -300,16 +300,16 @@ theorem insertUnitInvariant_insertUnit {n : Nat} (assignments0 : Array Assignmen · exact h3 · simp only by_cases i.1 = l.1.1 - · next i_eq_l => + next i_eq_l => simp only [i_eq_l] rw [Array.getElem_modify_self] simp only [← i_eq_l, h3, add_both_eq_both] - · next i_ne_l => grind + next i_ne_l => grind · constructor · exact h4 · intro k k_ne_j1 k_ne_j2 by_cases k.1 < units.size - · next k_in_bounds => + next k_in_bounds => have k_ne_j1 : ⟨k.1, k_in_bounds⟩ ≠ j1 := by intro k_eq_j1 simp only [← k_eq_j1, not_true] at k_ne_j1 @@ -322,12 +322,12 @@ theorem insertUnitInvariant_insertUnit {n : Nat} (assignments0 : Array Assignmen rw [Array.getElem_push] simp only [k_in_bounds, dite_true] exact h5 ⟨k.1, k_in_bounds⟩ k_ne_j1 k_ne_j2 - · next k_not_lt_units_size => + next k_not_lt_units_size => split - · next h => + next h => have k_property := k.2 grind - · next h => + next h => simp only have k_eq_units_size : k.1 = units.size := by have k_property := k.2 @@ -347,7 +347,7 @@ theorem insertUnitInvariant_insertUnit_fold {n : Nat} (assignments0 : Array Assi InsertUnitInvariant assignments0 assignments0_size update_res.1 update_res.2.1 update_res_size := by induction units generalizing rupUnits assignments assignments_size b · simp only [List.foldl, imp_self] - · next hd tl ih => + next hd tl ih => simp only [List.foldl] intro h0 let update_res := insertUnit (rupUnits, assignments, b) hd @@ -467,7 +467,7 @@ theorem clear_insert_inductive_case {n : Nat} (f : DefaultFormula n) (f_assignme · intro j j_ge_idx_add_one exact ih2 j (Nat.le_of_succ_le j_ge_idx_add_one) · by_cases idx = j - · next idx_eq_j => + next idx_eq_j => apply Or.inl constructor · simp only [clearUnit, idx_eq_j, Array.getInternal_eq_getElem, ih1] @@ -477,7 +477,7 @@ theorem clear_insert_inductive_case {n : Nat} (f : DefaultFormula n) (f_assignme have k_ge_idx : k.val ≥ idx.val := by grind have k_ne_j : k ≠ j := by grind exact ih4 k k_ge_idx k_ne_j - · next idx_ne_j => + next idx_ne_j => refine Or.inr <| Or.inl <| ⟨j,b,i_gt_zero,?_⟩ constructor · grind @@ -491,7 +491,7 @@ theorem clear_insert_inductive_case {n : Nat} (f : DefaultFormula n) (f_assignme · intro k k_ge_idx_add_one k_ne_j exact ih4 k (Nat.le_of_succ_le k_ge_idx_add_one) k_ne_j · by_cases idx = j1 - · next idx_eq_j1 => + next idx_eq_j1 => have idx_ne_j2 : idx ≠ j2 := by grind refine Or.inr <| Or.inl <| ⟨j2, false, i_gt_zero, ?_⟩ constructor @@ -512,19 +512,19 @@ theorem clear_insert_inductive_case {n : Nat} (f : DefaultFormula n) (f_assignme · intro k k_ge_idx_add_one k_ne_j2 intro h1 by_cases units[k.1].2 - · next h2 => + next h2 => have k_ne_j1 : k ≠ j1 := by grind have h3 := units_nodup k j1 k_ne_j1 simp only [Fin.getElem_fin, ih1, ← h1, ← h2, ne_eq] at h3 exact h3 rfl - · next h2 => + next h2 => have h3 := units_nodup k j2 k_ne_j2 simp only [Bool.not_eq_true] at h2 simp only [Fin.getElem_fin, ih2, ← h1, ← h2, ne_eq] at h3 exact h3 rfl - · next idx_ne_j1 => + next idx_ne_j1 => by_cases idx = j2 - · next idx_eq_j2 => + next idx_eq_j2 => refine Or.inr <| Or.inl <| ⟨j1, true, i_gt_zero, ?_⟩ constructor · apply Nat.le_of_lt_succ @@ -545,17 +545,17 @@ theorem clear_insert_inductive_case {n : Nat} (f : DefaultFormula n) (f_assignme · intro k k_ge_idx_add_one k_ne_j1 intro h1 by_cases units[k.1].2 - · next h2 => + next h2 => have h3 := units_nodup k j1 k_ne_j1 simp only [Fin.getElem_fin, ih1, ← h1, ← h2, ne_eq] at h3 exact h3 rfl - · next h2 => + next h2 => have k_ne_j2 : k ≠ j2 := by grind have h3 := units_nodup k j2 k_ne_j2 simp only [Bool.not_eq_true] at h2 simp only [Fin.getElem_fin, ih2, ← h1, ← h2, ne_eq] at h3 exact h3 rfl - · next idx_ne_j2 => + next idx_ne_j2 => refine Or.inr <| Or.inr <| ⟨j1, j2,i_gt_zero, ?_⟩ constructor · grind @@ -663,7 +663,7 @@ theorem confirmRupHint_preserves_invariant_helper {n : Nat} (f : DefaultFormula have l_in_bounds : l.1.1 < acc.1.size := by rw [hsize]; exact l.1.2.2 rcases ih i with ⟨h1, h2⟩ | ⟨j, j_eq_i, h1, h2, h3⟩ | ⟨j1, j2, j1_eq_i, j2_eq_i, j1_eq_true, j2_eq_false, h1, h2, h3⟩ · by_cases l.1.1 = i.1 - · next l_eq_i => + next l_eq_i => have zero_lt_length_list : 0 < (l :: acc.snd.fst).length := by simp only [List.length_cons] exact Nat.zero_lt_succ (List.length acc.snd.fst) @@ -692,18 +692,18 @@ theorem confirmRupHint_preserves_invariant_helper {n : Nat} (f : DefaultFormula rw [k_eq_succ, List.get_cons_succ] have k'_in_bounds : k' < acc.2.1.length := by grind exact h2 (acc.2.1.get ⟨k', k'_in_bounds⟩) (by grind) - · next l_ne_i => grind + next l_ne_i => grind · let l' := acc.2.1.get j have zero_in_bounds : 0 < (l :: acc.2.1).length := by grind have j_succ_in_bounds : j.1 + 1 < (l :: acc.2.1).length := by simp only [List.length_cons] exact Nat.succ_lt_succ j.2 by_cases l.1.1 = i.1 - · next l_eq_i => + next l_eq_i => apply Or.inr ∘ Or.inr have l_ne_l' : l.2 ≠ l'.2 := by grind [has_add] by_cases l.2 - · next l_eq_true => + next l_eq_true => rw [l_eq_true] at l_ne_l' have l'_eq_false : l'.2 = false := by rw [← Bool.not_eq_true]; exact Ne.symm l_ne_l' apply Exists.intro ⟨0, zero_in_bounds⟩ @@ -743,7 +743,7 @@ theorem confirmRupHint_preserves_invariant_helper {n : Nat} (f : DefaultFormula have k'_in_bounds : k' < acc.2.1.length := by grind have k'_ne_j : ⟨k', k'_in_bounds⟩ ≠ j := by grind exact h3 ⟨k', k'_in_bounds⟩ k'_ne_j - · next l_eq_false => + next l_eq_false => simp only [Bool.not_eq_true] at l_eq_false rw [l_eq_false] at l_ne_l' have l'_eq_true : l'.2 = true := by grind @@ -783,7 +783,7 @@ theorem confirmRupHint_preserves_invariant_helper {n : Nat} (f : DefaultFormula have k'_in_bounds : k' < acc.2.1.length := by grind have k'_ne_j : ⟨k', k'_in_bounds⟩ ≠ j := by grind exact h3 ⟨k', k'_in_bounds⟩ k'_ne_j - · next l_ne_i => + next l_ne_i => apply Or.inr ∘ Or.inl ∘ Exists.intro ⟨j.1 + 1, j_succ_in_bounds⟩ simp only [List.get] constructor @@ -793,14 +793,14 @@ theorem confirmRupHint_preserves_invariant_helper {n : Nat} (f : DefaultFormula · apply And.intro h2 intro k k_ne_j_succ by_cases k.1 = 0 - · next k_eq_zero => + next k_eq_zero => have k_eq_zero : k = ⟨0, zero_in_bounds⟩ := by apply Fin.eq_of_val_eq simp only [List.length_cons] exact k_eq_zero simp only [k_eq_zero, List.length_cons, List.get, ne_eq] exact l_ne_i - · next k_ne_zero => + next k_ne_zero => have k_eq_succ : ∃ k' : Nat, ∃ k'_succ_in_bounds : k' + 1 < (l :: acc.2.1).length, k = ⟨k' + 1, k'_succ_in_bounds⟩ := by have k_val_ne_zero : k.1 ≠ 0 := by grind rcases Nat.exists_eq_succ_of_ne_zero k_val_ne_zero with ⟨k', k_eq_k'_succ⟩ @@ -839,8 +839,8 @@ theorem confirmRupHint_preserves_invariant_helper {n : Nat} (f : DefaultFormula · intro k k_ne_j1_succ k_ne_j2_succ have zero_in_bounds : 0 < (l :: acc.2.1).length := by grind by_cases k = ⟨0, zero_in_bounds⟩ - · next k_eq_zero => grind - · next k_ne_zero => + next k_eq_zero => grind + next k_ne_zero => have k_eq_succ : ∃ k' : Nat, ∃ k'_succ_in_bounds : k' + 1 < (l :: acc.2.1).length, k = ⟨k' + 1, k'_succ_in_bounds⟩ := by have k_val_ne_zero : k.1 ≠ 0 := by intro k_eq_zero @@ -936,7 +936,7 @@ theorem nodup_derivedLits {n : Nat} (f : DefaultFormula n) ⟨k1, k2, _, _, k1_eq_true, k2_eq_false, _, _, h3⟩ · exact h2 li li_in_derivedLits rfl · by_cases k.1 = i.1 - · next k_eq_i => + next k_eq_i => have j_ne_k : ⟨j.1, j_in_bounds⟩ ≠ k := by intro j_eq_k simp only [← j_eq_k] at k_eq_i @@ -945,12 +945,12 @@ theorem nodup_derivedLits {n : Nat} (f : DefaultFormula n) simp only [derivedLits_arr_def, Fin.getElem_fin] at li_eq_lj simp only [Fin.getElem_fin, derivedLits_arr_def, ne_eq, li, li_eq_lj] at h3 simp only [List.get_eq_getElem, ← Array.getElem_toList, not_true_eq_false] at h3 - · next k_ne_i => + next k_ne_i => have i_ne_k : ⟨i.1, i_in_bounds⟩ ≠ k := by intro i_eq_k; simp only [← i_eq_k, not_true] at k_ne_i specialize h3 ⟨i.1, i_in_bounds⟩ i_ne_k grind [Fin.getElem_fin] · by_cases li.2 = true - · next li_eq_true => + next li_eq_true => have i_ne_k2 : ⟨i.1, i_in_bounds⟩ ≠ k2 := by intro i_eq_k2 rw [← i_eq_k2] at k2_eq_false @@ -963,7 +963,7 @@ theorem nodup_derivedLits {n : Nat} (f : DefaultFormula n) simp only [derivedLits_arr_def, Fin.getElem_fin] at li_eq_lj simp [derivedLits_arr_def, k2_eq_false, li_eq_lj, li] at li_eq_true by_cases ⟨i.1, i_in_bounds⟩ = k1 - · next i_eq_k1 => + next i_eq_k1 => have j_ne_k1 : ⟨j.1, j_in_bounds⟩ ≠ k1 := by intro j_eq_k1 rw [← j_eq_k1] at i_eq_k1 @@ -971,12 +971,12 @@ theorem nodup_derivedLits {n : Nat} (f : DefaultFormula n) exact i_ne_j (Fin.eq_of_val_eq i_eq_k1) specialize h3 ⟨j.1, j_in_bounds⟩ j_ne_k1 j_ne_k2 simp [li, li_eq_lj, derivedLits_arr_def] at h3 - · next i_ne_k1 => + next i_ne_k1 => specialize h3 ⟨i.1, i_in_bounds⟩ i_ne_k1 i_ne_k2 apply h3 simp +decide only [Fin.getElem_fin, derivedLits_arr_def, li] rfl - · next li_eq_false => + next li_eq_false => simp only [Bool.not_eq_true] at li_eq_false have i_ne_k1 : ⟨i.1, i_in_bounds⟩ ≠ k1 := by intro i_eq_k1 @@ -990,7 +990,7 @@ theorem nodup_derivedLits {n : Nat} (f : DefaultFormula n) simp only [derivedLits_arr_def, Fin.getElem_fin] at li_eq_lj simp [derivedLits_arr_def, k1_eq_true, li_eq_lj, li] at li_eq_false by_cases ⟨i.1, i_in_bounds⟩ = k2 - · next i_eq_k2 => + next i_eq_k2 => have j_ne_k2 : ⟨j.1, j_in_bounds⟩ ≠ k2 := by intro j_eq_k2 rw [← j_eq_k2] at i_eq_k2 @@ -998,7 +998,7 @@ theorem nodup_derivedLits {n : Nat} (f : DefaultFormula n) exact i_ne_j (Fin.eq_of_val_eq i_eq_k2) specialize h3 ⟨j.1, j_in_bounds⟩ j_ne_k1 j_ne_k2 simp [li, li_eq_lj, derivedLits_arr_def] at h3 - · next i_ne_k2 => + next i_ne_k2 => specialize h3 ⟨i.1, i_in_bounds⟩ i_ne_k1 i_ne_k2 simp +decide [derivedLits_arr_def, li] at h3 diff --git a/src/Std/Tactic/BVDecide/LRAT/Internal/Formula/RupAddSound.lean b/src/Std/Tactic/BVDecide/LRAT/Internal/Formula/RupAddSound.lean index 15ae9c58b0..841f2744d2 100644 --- a/src/Std/Tactic/BVDecide/LRAT/Internal/Formula/RupAddSound.lean +++ b/src/Std/Tactic/BVDecide/LRAT/Internal/Formula/RupAddSound.lean @@ -35,33 +35,33 @@ theorem contradiction_of_insertUnit_success {n : Nat} (assignments : Array Assig simp only [insertUnit] at insertUnit_success have l_in_bounds : l.1.1 < assignments.size := by rw [assignments_size]; exact l.1.2.2 split at insertUnit_success - · next hl => + next hl => simp only [insertUnit, hl, ite_true] exact h insertUnit_success - · next hl => + next hl => simp only [Bool.or_eq_true] at insertUnit_success rcases insertUnit_success with foundContradiction_eq_true | assignments_l_ne_unassigned · simp only [insertUnit, hl] rcases h foundContradiction_eq_true with ⟨i, h⟩ apply Exists.intro i by_cases l.1.1 = i.1 - · next l_eq_i => + next l_eq_i => simp only [Bool.false_eq_true, ↓reduceIte, l_eq_i, Array.getElem_modify_self, h, ] exact add_both_eq_both l.2 - · next l_ne_i => + next l_ne_i => simpa [Array.getElem_modify_of_ne l_ne_i] using h · apply Exists.intro l.1 simp only [insertUnit, hl, ite_false, Array.getElem_modify_self, reduceCtorEq] simp only [getElem!_def, l_in_bounds, Array.getElem?_eq_getElem, ] at assignments_l_ne_unassigned by_cases l.2 - · next l_eq_true => + next l_eq_true => simp only [l_eq_true] simp only [hasAssignment, l_eq_true, getElem!_def, l_in_bounds, Array.getElem?_eq_getElem, ite_true, hasPosAssignment, Bool.not_eq_true] at hl split at hl <;> simp_all +decide - · next l_eq_false => + next l_eq_false => simp only [Bool.not_eq_true] at l_eq_false simp only [l_eq_false] simp only [hasAssignment, l_eq_false, Bool.false_eq_true, ↓reduceIte, hasNegAssignment, @@ -164,14 +164,14 @@ theorem sat_of_insertRup {n : Nat} (f : DefaultFormula n) (f_readyForRupAdd : Re simp only [addAssignment, ← b_eq_true, addPosAssignment, ite_true] at h2 split at h2 · simp at h2 - · next heq => + next heq => have hasNegAssignment_fi : hasAssignment false (f.assignments[i.1]'i_in_bounds) := by simp only [hasAssignment, hasPosAssignment, heq] decide have p_entails_i := (assignmentsInvariant_of_strongAssignmentsInvariant f f_readyForRupAdd.2).2 i false hasNegAssignment_fi p pf simp only [(· ⊨ ·)] at p_entails_i simp only [p_entails_i, decide_true] - · next heq => + next heq => exfalso rw [heq] at h3 exact h3 (has_both b) @@ -181,14 +181,14 @@ theorem sat_of_insertRup {n : Nat} (f : DefaultFormula n) (f_readyForRupAdd : Re apply And.intro i_true_in_c simp only [addAssignment, ← b_eq_false, addNegAssignment, ite_false, reduceCtorEq] at h2 split at h2 - · next heq => + next heq => have hasPosAssignment_fi : hasAssignment true (f.assignments[i.1]'i_in_bounds) := by simp only [hasAssignment, hasPosAssignment, ite_true, heq] have p_entails_i := (assignmentsInvariant_of_strongAssignmentsInvariant f f_readyForRupAdd.2).2 i true hasPosAssignment_fi p pf simp only [(· ⊨ ·)] at p_entails_i exact p_entails_i · simp at h2 - · next heq => + next heq => exfalso rw [heq] at h3 exact h3 (has_both b) @@ -254,7 +254,7 @@ theorem assignmentsInvariant_insertRupUnits_of_assignmentsInvariant {n : Nat} (f exact (assignmentsInvariant_of_strongAssignmentsInvariant f f_readyForRupAdd.2).2 i b hb p pf · rw [h2] at hb by_cases b = b' - · next b_eq_b' => + next b_eq_b' => let j_unit := unit (insertRupUnits f units).1.rupUnits[j] have j_unit_def : j_unit = unit (insertRupUnits f units).1.rupUnits[j] := rfl have j_unit_in_insertRupUnits_res : @@ -300,7 +300,7 @@ theorem assignmentsInvariant_insertRupUnits_of_assignmentsInvariant {n : Nat} (f · simp only [b_eq_b', ← hp1.2, Entails.eval] rw [hp1.1] at hp2 exact hp2 - · next b_ne_b' => + next b_ne_b' => apply (assignmentsInvariant_of_strongAssignmentsInvariant f f_readyForRupAdd.2).2 i b _ p pf have b'_def : b' = (decide ¬b = true) := by cases b <;> cases b' <;> simp at * @@ -371,7 +371,7 @@ theorem unsat_of_encounteredBoth {n : Nat} (c : DefaultClause n) · split at h · grind · grind - · next heq => + next heq => intro p hp simp only [(· ⊨ ·), Bool.not_eq_true] at hp specialize hp l.1 @@ -380,7 +380,7 @@ theorem unsat_of_encounteredBoth {n : Nat} (c : DefaultClause n) · split at h · grind · grind - · next heq => + next heq => intro p hp simp only [(· ⊨ ·), Bool.not_eq_true] at hp specialize hp l.1 @@ -408,14 +408,14 @@ theorem reduce_fold_fn_preserves_induction_motive {c_arr : Array (Literal (PosFi split at h · grind · split at h - · next heq => + next heq => split at h · grind - · next c_arr_idx_eq_false => + next c_arr_idx_eq_false => simp only [Bool.not_eq_true] at c_arr_idx_eq_false rcases ih.1 rfl p with ih1 | ih1 · by_cases p ⊨ assignment - · next p_entails_assignment => + next p_entails_assignment => apply Or.inl intro i i_lt_idx_add_one p_entails_c_arr_i rcases Nat.lt_or_eq_of_le <| Nat.le_of_lt_succ i_lt_idx_add_one with i_lt_idx | i_eq_idx @@ -424,17 +424,17 @@ theorem reduce_fold_fn_preserves_induction_motive {c_arr : Array (Literal (PosFi simp only [(· ⊨ ·), Bool.not_eq_true] at p_entails_assignment specialize p_entails_assignment c_arr[idx.1].1 simp +decide only [p_entails_c_arr_i, decide_true, heq] at p_entails_assignment - · next h => + next h => exact Or.inr h · exact Or.inr ih1 - · next heq => + next heq => split at h · simp at h - · next c_arr_idx_eq_false => + next c_arr_idx_eq_false => simp only [Bool.not_eq_true', Bool.not_eq_false] at c_arr_idx_eq_false rcases ih.1 rfl p with ih1 | ih1 · by_cases p ⊨ assignment - · next p_entails_assignment => + next p_entails_assignment => apply Or.inl intro i i_lt_idx_add_one p_entails_c_arr_i rcases Nat.lt_or_eq_of_le <| Nat.le_of_lt_succ i_lt_idx_add_one with i_lt_idx | i_eq_idx @@ -443,7 +443,7 @@ theorem reduce_fold_fn_preserves_induction_motive {c_arr : Array (Literal (PosFi simp only [(· ⊨ ·), Bool.not_eq_true] at p_entails_assignment specialize p_entails_assignment c_arr[idx.1].1 simp +decide only [p_entails_c_arr_i, heq] at p_entails_assignment - · next h => + next h => exact Or.inr h · exact Or.inr ih1 · grind @@ -455,35 +455,35 @@ theorem reduce_fold_fn_preserves_induction_motive {c_arr : Array (Literal (PosFi split at h · grind · split at h - · next heq => + next heq => split at h - · next c_arr_idx_eq_true => + next c_arr_idx_eq_true => simp only [reducedToUnit.injEq] at h simp only [h] at c_arr_idx_eq_true simp only [(· ⊨ ·), Bool.not_eq_true] at hp specialize hp c_arr[idx.val].1 rw [heq] at hp by_cases p c_arr[idx.val].1 - · next p_c_arr_idx_eq_true => + next p_c_arr_idx_eq_true => simp only [h] at p_c_arr_idx_eq_true simp only [(· ⊨ ·), c_arr_idx_eq_true, p_c_arr_idx_eq_true] - · next p_c_arr_idx_eq_false => + next p_c_arr_idx_eq_false => simp only [h, Bool.not_eq_true] at p_c_arr_idx_eq_false simp +decide only [h, p_c_arr_idx_eq_false] at hp · grind - · next heq => + next heq => split at h - · next c_arr_idx_eq_true => + next c_arr_idx_eq_true => simp only [reducedToUnit.injEq] at h simp only [h, Bool.not_eq_true'] at c_arr_idx_eq_true simp only [(· ⊨ ·), Bool.not_eq_true] at hp specialize hp c_arr[idx.val].1 rw [heq] at hp by_cases p c_arr[idx.val].1 - · next p_c_arr_idx_eq_true => + next p_c_arr_idx_eq_true => simp only [h] at p_c_arr_idx_eq_true simp +decide only [h, p_c_arr_idx_eq_true] at hp - · next p_c_arr_idx_eq_false => + next p_c_arr_idx_eq_false => simp only [h] at p_c_arr_idx_eq_false simp only [(· ⊨ ·), c_arr_idx_eq_true, p_c_arr_idx_eq_false] · grind @@ -496,12 +496,12 @@ theorem reduce_fold_fn_preserves_induction_motive {c_arr : Array (Literal (PosFi · exact ih1 j j_lt_idx p_entails_c_arr_j · exact ih1 hp · grind - · next l => + next l => split at h - · next heq => + next heq => split at h · grind - · next c_arr_idx_eq_false => + next c_arr_idx_eq_false => simp only [Bool.not_eq_true] at c_arr_idx_eq_false simp only [reducedToUnit.injEq] at h rcases Nat.lt_or_eq_of_le <| Nat.le_of_lt_succ j_lt_idx_add_one with j_lt_idx | j_eq_idx @@ -513,10 +513,10 @@ theorem reduce_fold_fn_preserves_induction_motive {c_arr : Array (Literal (PosFi simp only [(· ⊨ ·), Bool.not_eq_true] at hp specialize hp c_arr[idx.1].1 simp +decide only [p_entails_c_arr_j, decide_true, heq] at hp - · next heq => + next heq => split at h · grind - · next c_arr_idx_eq_true => + next c_arr_idx_eq_true => simp only [Bool.not_eq_true', Bool.not_eq_false] at c_arr_idx_eq_true simp only [reducedToUnit.injEq] at h rcases Nat.lt_or_eq_of_le <| Nat.le_of_lt_succ j_lt_idx_add_one with j_lt_idx | j_eq_idx @@ -618,25 +618,25 @@ theorem confirmRupHint_preserves_motive {n : Nat} (f : DefaultFormula n) (rupHin simp only [confirmRupHint, Bool.or_eq_true, Fin.getElem_fin] split · exact ⟨hsize, h1, h2⟩ - · next acc2_eq_false => + next acc2_eq_false => simp only [not_or, Bool.not_eq_true] at acc2_eq_false split - · next c hc => + next c hc => have c_in_f : c ∈ toList f := by simp only [toList, List.mem_append, List.mem_filterMap, id_eq, exists_eq_right] grind split - · next heq => + next heq => simp only [ConfirmRupHintFoldEntailsMotive, h1, imp_self, and_self, hsize, incompatible_of_unsat (PosFin n) acc.1 f (unsat_of_encounteredBoth c acc.1 heq)] - · next heq => + next heq => simp only [ConfirmRupHintFoldEntailsMotive, h1, hsize, forall_const, true_and] intro p rcases incompatible_of_reducedToEmpty c acc.1 heq p with pc | pacc · simp only [(· ⊨ ·)] at pc ⊢ grind · exact Or.inl pacc - · next l b heq => + next l b heq => simp only [ConfirmRupHintFoldEntailsMotive] split · simp [h1, hsize] @@ -653,7 +653,7 @@ theorem confirmRupHint_preserves_motive {n : Nat} (f : DefaultFormula n) (rupHin simp only [Bool.not_eq_true] at pacc have i_in_bounds : i.1 < acc.1.size := by rw [hsize]; exact i.2.2 by_cases l.1 = i.1 - · next l_eq_i => + next l_eq_i => simp only [l_eq_i, getElem!_def, Array.size_modify, i_in_bounds, Array.getElem?_eq_getElem, Array.getElem_modify_self (addAssignment b)] simp only [getElem!_def, i_in_bounds, Array.getElem?_eq_getElem] at pacc @@ -670,7 +670,7 @@ theorem confirmRupHint_preserves_motive {n : Nat} (f : DefaultFormula n) (rupHin by_cases hb : b · simp [(· ⊨ ·), hb, Subtype.ext l_eq_i, pi] at plb · grind [hasAssignment, addAssignment, hasPos_addNeg] - · next l_ne_i => grind + next l_ne_i => grind · apply And.intro hsize ∘ And.intro h1 simp · apply And.intro hsize ∘ And.intro h1 @@ -766,7 +766,7 @@ theorem rupAdd_sound {n : Nat} (f : DefaultFormula n) (c : DefaultClause n) (rup rw [performRupAdd] at rupAddSuccess simp only [Bool.not_eq_true'] at rupAddSuccess split at rupAddSuccess - · next insertRupContradiction => + next insertRupContradiction => intro p have f_limplies_fc := safe_insert_of_insertRup f f_readyForRupAdd c insertRupContradiction p rw [f'_def] @@ -777,7 +777,7 @@ theorem rupAdd_sound {n : Nat} (f : DefaultFormula n) (c : DefaultClause n) (rup · grind · split at rupAddSuccess · grind - · next performRupCheck_success => + next performRupCheck_success => rw [Bool.not_eq_false] at performRupCheck_success have f_limplies_fc := safe_insert_of_performRupCheck_insertRup f f_readyForRupAdd c rupHints performRupCheck_success rw [liff_iff_limplies_and_limplies f f', f'_def] diff --git a/tests/lean/grind/experiments/bitvec.lean b/tests/lean/grind/experiments/bitvec.lean index 254130ce69..dde6ba0cf1 100644 --- a/tests/lean/grind/experiments/bitvec.lean +++ b/tests/lean/grind/experiments/bitvec.lean @@ -646,7 +646,7 @@ theorem eq_zero_or_eq_one (a : BitVec 1) : a = 0#1 ∨ a = 1#1 := by have acases : a = 0 ∨ a = 1 := by omega rcases acases with ⟨rfl | rfl⟩ · simp - · case inr h => + case inr h => subst h simp @@ -4142,8 +4142,8 @@ theorem neg_one_ediv_toInt_eq {w : Nat} {y : BitVec w} : rcases w with _|_|w · simp [of_length_zero] · cases eq_zero_or_eq_one y - · case _ h => simp [h] - · case _ h => simp [h] + case _ h => simp [h] + case _ h => simp [h] · by_cases 0 < y.toInt · simp [Int.sign_eq_one_of_pos (a := y.toInt) (by omega), Int.neg_one_ediv] omega diff --git a/tests/lean/grind/experiments/list.lean b/tests/lean/grind/experiments/list.lean index ca3da8bf71..921613c4f7 100644 --- a/tests/lean/grind/experiments/list.lean +++ b/tests/lean/grind/experiments/list.lean @@ -872,7 +872,7 @@ theorem flatMap_eq_foldl {f : α → List β} {l : List α} : intro l' induction l generalizing l' · grind - · next ih => rw [flatMap_cons, ← append_assoc, ih, foldl_cons] + next ih => rw [flatMap_cons, ← append_assoc, ih, foldl_cons] /-! ### replicate -/ diff --git a/tests/lean/run/1017.lean b/tests/lean/run/1017.lean index 408e5d4530..a7d3b0bcca 100644 --- a/tests/lean/run/1017.lean +++ b/tests/lean/run/1017.lean @@ -27,17 +27,17 @@ instance hasNextWF : WellFoundedRelation {s : ρ // isFinite s} where rel := λ s1 s2 => hasNext s2.val s1.val wf := ⟨λ ⟨s,h⟩ => ⟨Subtype.mk s h, by simp only [Subtype.forall] - cases h; case intro w h => + cases h with | intro w h induction w generalizing s case zero => intro s' h' h_next simp [hasNext] at h_next - cases h_next; case intro x h_next => + cases h_next with | intro x h_next simp [lengthBoundedBy, isEmpty, Option.isNone, take, h_next] at h case succ n ih => intro s' h' h_next simp [hasNext] at h_next - cases h_next; case intro x h_next => + cases h_next with | intro x h_next simp [lengthBoundedBy, take, h_next] at h have := ih s' h exact Acc.intro (⟨s',h'⟩ : {s : ρ // isFinite s}) (by simpa only [Subtype.forall]) diff --git a/tests/lean/run/1337.lean b/tests/lean/run/1337.lean index 8e6a2a2068..336bc66e3a 100644 --- a/tests/lean/run/1337.lean +++ b/tests/lean/run/1337.lean @@ -2,9 +2,9 @@ theorem n_minus_one_le_n {n : Nat} : n > 0 → n - 1 < n := by cases n with | zero => simp [] | succ n => - intros - rw [Nat.add_sub_cancel] - apply Nat.le.refl + intros + rw [Nat.add_sub_cancel] + apply Nat.le.refl partial def foo : Array Int → Int | arr => Id.run do diff --git a/tests/lean/run/1711.lean b/tests/lean/run/1711.lean index 91b090fa1b..2e87b7b208 100644 --- a/tests/lean/run/1711.lean +++ b/tests/lean/run/1711.lean @@ -6,15 +6,15 @@ theorem MulOneClass.ext {M : Type u} : ∀ ⦃m₁ m₂ : MulOneClass M⦄, m₁ intro m₁ m₂ cases m₁ with | @mk one₁ mul₁ one_mul₁ mul_one₁ => - cases one₁ with | mk one₁ => - cases mul₁ with | mk mul₁ => + cases one₁ with | mk one₁ + cases mul₁ with | mk mul₁ cases m₂ with | @mk one₂ mul₂ one_mul₂ mul_one₂ => - cases one₂ with | mk one₂ => - cases mul₂ with | mk mul₂ => - simp - intro h - cases h - have := (one_mul₂ one₁).symm.trans (mul_one₁ one₂) -- TODO: make sure we can apply after congr - subst this - congr + cases one₂ with | mk one₂ + cases mul₂ with | mk mul₂ + simp + intro h + cases h + have := (one_mul₂ one₁).symm.trans (mul_one₁ one₂) -- TODO: make sure we can apply after congr + subst this + congr diff --git a/tests/lean/run/1841.lean b/tests/lean/run/1841.lean index 94a898f27a..ef6ed01d57 100644 --- a/tests/lean/run/1841.lean +++ b/tests/lean/run/1841.lean @@ -18,8 +18,8 @@ theorem head_induction_on {P : ∀ a : α, ReflTransGen r a b → Prop} {a : α} induction h case refl => exact refl case tail b c _ hbc ih => - apply ih - { exact head hbc _ refl } - { exact fun h1 h2 => head h1 (h2.tail hbc) } + apply ih + { exact head hbc _ refl } + { exact fun h1 h2 => head h1 (h2.tail hbc) } end ReflTransGen diff --git a/tests/lean/run/andCasesOnBug.lean b/tests/lean/run/andCasesOnBug.lean index 9c610f68ae..e4b69c2ca0 100644 --- a/tests/lean/run/andCasesOnBug.lean +++ b/tests/lean/run/andCasesOnBug.lean @@ -15,8 +15,7 @@ def makePair?: (n m: (sz: Nat) × FinInt sz) → Option Pair | ⟨sz, lhs⟩, ⟨sz', rhs⟩ => if EQ: true /\ sz = sz' then have rhs' : FinInt sz := by { - cases EQ; - case intro left right => + cases EQ with | intro left right simp [right]; exact rhs; }; diff --git a/tests/lean/run/as_aux_lemma.lean b/tests/lean/run/as_aux_lemma.lean index 0dd9dc05b6..9505b5ab0a 100644 --- a/tests/lean/run/as_aux_lemma.lean +++ b/tests/lean/run/as_aux_lemma.lean @@ -11,18 +11,19 @@ open Lean Meta abbrev testProp := ∀ n : Nat, n = 0 + n -def thmUsingTactic : testProp := by as_aux_lemma => - intro n - induction n - · rfl - · next ih => - rw [← Nat.succ_eq_add_one, Nat.add_succ, ← ih] +def thmUsingTactic : testProp := by + as_aux_lemma => + intro n + induction n + · rfl + next ih => + rw [← Nat.succ_eq_add_one, Nat.add_succ, ← ih] def thmWithoutTactic : testProp := by intro n induction n · rfl - · next ih => + next ih => rw [← Nat.succ_eq_add_one, Nat.add_succ, ← ih] open Lean diff --git a/tests/lean/run/doLogicTests.lean b/tests/lean/run/doLogicTests.lean index 7bd6b40744..23ea9e2ce7 100644 --- a/tests/lean/run/doLogicTests.lean +++ b/tests/lean/run/doLogicTests.lean @@ -287,7 +287,6 @@ theorem fib_triple : ⦃⌜True⌝⦄ fib_impl n ⦃⇓ r => ⌜r = fib_spec n theorem fib_triple_cases : ⦃⌜True⌝⦄ fib_impl n ⦃⇓ r => ⌜r = fib_spec n⌝⦄ := by apply fib_impl.fun_cases n _ ?case1 ?case2 case case1 => rintro rfl; mintro -; simp only [fib_impl, ↓reduceIte]; mspec - case case2 => intro h mintro - simp only [fib_impl, h, reduceIte] @@ -308,7 +307,6 @@ theorem fib_impl_vcs : ⊢ₛ wp⟦fib_impl n⟧ (Q n) := by apply fib_impl.fun_cases n _ ?case1 ?case2 case case1 => intro h; simp only [fib_impl, h, ↓reduceIte]; mstart; mspec - case case2 => intro hn simp only [fib_impl, hn, ↓reduceIte] mstart diff --git a/tests/lean/run/grind_bitvec2.lean b/tests/lean/run/grind_bitvec2.lean index 36465ff62a..26bf1d54b8 100644 --- a/tests/lean/run/grind_bitvec2.lean +++ b/tests/lean/run/grind_bitvec2.lean @@ -559,7 +559,7 @@ theorem eq_zero_or_eq_one (a : BitVec 1) : a = 0#1 ∨ a = 1#1 := by have acases : a = 0 ∨ a = 1 := by grind rcases acases with ⟨rfl | rfl⟩ · grind - · case inr h => + case inr h => -- TODO: why can't `grind` do this? subst h grind @@ -3418,8 +3418,8 @@ theorem neg_one_ediv_toInt_eq {w : Nat} {y : BitVec w} : rcases w with _|_|w · simp [of_length_zero] · cases eq_zero_or_eq_one y - · case _ h => simp [h] - · case _ h => simp [h] + case _ h => simp [h] + case _ h => simp [h] · by_cases 0 < y.toInt · simp [Int.sign_eq_one_of_pos (a := y.toInt) (by omega), Int.neg_one_ediv] omega @@ -4564,8 +4564,8 @@ theorem clzAuxRec_eq_clzAuxRec_of_le (x : BitVec w) (h : w - 1 ≤ n) : let k := n - (w - 1) rw [show n = (w - 1) + k by omega] induction k - · case zero => simp - · case succ k ihk => + case zero => simp + case succ k ihk => simp [show w - 1 + (k + 1) = (w - 1 + k) + 1 by omega, clzAuxRec_succ, ihk, show x.getLsbD (w - 1 + k + 1) = false by simp only [show w ≤ w - 1 + k + 1 by omega, getLsbD_of_ge]] diff --git a/tests/lean/run/issue2982.lean b/tests/lean/run/issue2982.lean index 6bca320f31..ed2c9ebafd 100644 --- a/tests/lean/run/issue2982.lean +++ b/tests/lean/run/issue2982.lean @@ -17,7 +17,7 @@ def foo : (n : Nat) → ∃ m, m > n | 0 => ⟨1, Nat.zero_lt_one⟩ | n+1 => by cases foo n - · case _ m hm => exact ⟨m+1, Nat.succ_lt_succ hm⟩ + case _ m hm => exact ⟨m+1, Nat.succ_lt_succ hm⟩ decreasing_by -- trace_state diff --git a/tests/lean/run/nomatch_regression.lean b/tests/lean/run/nomatch_regression.lean index cb012c8f36..afbb311676 100644 --- a/tests/lean/run/nomatch_regression.lean +++ b/tests/lean/run/nomatch_regression.lean @@ -100,7 +100,7 @@ protected theorem RedRed.balance2 {l : RBNode α} {v : α} {r : RBNode α} unfold balance2; split · have .redred _ (.red ha hb) hc := hr; exact ⟨_, .red (.black hl ha) (.black hb hc)⟩ · have .redred _ ha (.red hb hc) := hr; exact ⟨_, .red (.black hl ha) (.black hb hc)⟩ - · next H1 H2 => match hr with + next H1 H2 => match hr with | .balanced hr => exact ⟨_, .black hl hr⟩ | .redred _ (c₁ := black) (c₂ := black) ha hb => exact ⟨_, .black hl (.red ha hb)⟩ | .redred _ (c₁ := red) (.red ..) _ => cases H1 _ _ _ _ _ rfl @@ -111,7 +111,7 @@ protected theorem RedRed.balance1 {l : RBNode α} {v : α} {r : RBNode α} unfold balance1; split · have .redred _ (.red ha hb) hc := hl; exact ⟨_, .red (.black ha hb) (.black hc hr)⟩ · have .redred _ ha (.red hb hc) := hl; exact ⟨_, .red (.black ha hb) (.black hc hr)⟩ - · next H1 H2 => match hl with + next H1 H2 => match hl with | .balanced hl => exact ⟨_, .black hl hr⟩ | .redred _ (c₁ := black) (c₂ := black) ha hb => exact ⟨_, .black (.red ha hb) hr⟩ | .redred _ (c₁ := red) (.red ..) _ => cases H1 _ _ _ _ _ rfl @@ -120,12 +120,12 @@ protected theorem RedRed.balance1 {l : RBNode α} {v : α} {r : RBNode α} protected theorem Balanced.balRight (hl : l.Balanced cl (n + 1)) (hr : r.RedRed True n) : (balRight l v r).RedRed (cl = red) (n + 1) := by unfold balRight; split - · next b y c => exact + next b y c => exact let ⟨cb, cc, hb, hc⟩ := hr.of_red match cl with | red => .redred rfl hl (.black hb hc) | black => .balanced (.red hl (.black hb hc)) - · next H => exact match hr with + next H => exact match hr with | .redred .. => nomatch H _ _ _ rfl | .balanced hr => match hl with | .black hb hc => @@ -136,12 +136,12 @@ protected theorem Balanced.balRight (hl : l.Balanced cl (n + 1)) (hr : r.RedRed protected theorem Balanced.balLeft (hl : l.RedRed True n) (hr : r.Balanced cr (n + 1)) : (balLeft l v r).RedRed (cr = red) (n + 1) := by unfold balLeft; split - · next a x b => exact + next a x b => exact let ⟨ca, cb, ha, hb⟩ := hl.of_red match cr with | red => .redred rfl (.black ha hb) hr | black => .balanced (.red (.black ha hb) hr) - · next H => exact match hl with + next H => exact match hl with | .redred .. => nomatch H _ _ _ rfl | .balanced hl => match hr with | .black ha hb => @@ -163,23 +163,23 @@ protected theorem Balanced.append {l r : RBNode α} unfold append; split · exact .balanced hr · exact .balanced hl - · next b c _ _ => + next b c _ _ => have .red ha hb := hl; have .red hc hd := hr have ⟨_, IH⟩ := (hb.append hc).of_false (· rfl rfl); split - · next e => + next e => have .red hb' hc' := e ▸ IH exact .redred (nofun) (.red ha hb') (.red hc' hd) - · next bcc _ H => + next bcc _ H => match bcc, append b c, IH, H with | black, _, IH, _ => exact .redred (nofun) ha (.red IH hd) | red, _, .red .., H => cases H _ _ _ rfl - · next b c _ _ => + next b c _ _ => have .black ha hb := hl; have .black hc hd := hr have IH := hb.append hc; split - · next e => match e ▸ IH with + next e => match e ▸ IH with | .balanced (.red hb' hc') | .redred _ hb' hc' => exact .balanced (.red (.black ha hb') (.black hc' hd)) - · next H => + next H => match append b c, IH, H with | bc, .balanced hbc, _ => unfold balLeft; split