max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

chore: library style cleanup (#9654)

Browse source 
This PR cleans up the style of the library in anticipation of a future
PR that requires strict indentation for tactic sequences.
This commit is contained in:
Kyle Miller 2025-07-31 14:28:59 -07:00 • committed by GitHub
parent 271c8ab9cb
commit 4575799f8e
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
84 changed files with 698 additions and 749 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

12
src/Init/Data/Array/Lemmas.lean
View file

@ -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)

4
src/Init/Data/Array/Mem.lean
View file

@ -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) :

18
src/Init/Data/BitVec/Lemmas.lean
View file

@ -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

10
src/Init/Data/Int/Compare.lean
View file

@ -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

104
src/Init/Data/Int/Linear.lean
View file

@ -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₂

2
src/Init/Data/Iterators/Lemmas/Combinators/Monadic/FilterMap.lean
View file

@ -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]

4
src/Init/Data/Iterators/Lemmas/Consumers/Collect.lean
View file

@ -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 =>

6
src/Init/Data/Iterators/Lemmas/Consumers/Loop.lean
View file

@ -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

6
src/Init/Data/Iterators/Lemmas/Consumers/Monadic/Collect.lean
View file

@ -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

4
src/Init/Data/Iterators/Lemmas/Consumers/Monadic/Loop.lean
View file

@ -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

2
src/Init/Data/List/Erase.lean
View file

@ -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]

2
src/Init/Data/List/FinRange.lean
View file

@ -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

2
src/Init/Data/List/Lemmas.lean
View file

@ -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 -/

8
src/Init/Data/List/Nat/TakeDrop.lean
View file

@ -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'

2
src/Init/Data/List/Zip.lean
View file

@ -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 :

17
src/Init/Data/Nat/Bitwise/Lemmas.lean
View file

@ -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

10
src/Init/Data/Nat/Compare.lean
View file

@ -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

5
src/Init/Data/Nat/Lemmas.lean
View file

@ -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) :=

2
src/Init/Data/Nat/Log2.lean
View file

@ -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

2
src/Init/Data/Range/Polymorphic/Lemmas.lean
View file

@ -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 _ _

10
src/Init/Data/SInt/Lemmas.lean
View file

@ -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

4
src/Init/Data/UInt/Lemmas.lean
View file

@ -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:

4
src/Init/Data/Vector/Lemmas.lean
View file

@ -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

63
src/Init/Grind/Module/Envelope.lean
View file

@ -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

122
src/Init/Grind/Ring/Envelope.lean
View file

@ -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

6
src/Init/Grind/Ring/Field.lean
View file

@ -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

40
src/Init/Grind/Ring/OfSemiring.lean
View file

@ -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

12
src/Init/Grind/Ring/Poly.lean
View file

@ -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]

4
src/Init/GrindInstances/Ring/Fin.lean
View file

@ -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)]

26
src/Std/Data/DHashMap/Internal/AssocList/Lemmas.lean
View file

@ -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

8
src/Std/Data/DHashMap/Internal/Model.lean
View file

@ -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,

80
src/Std/Data/DHashMap/Internal/WF.lean
View file

@ -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

4
src/Std/Data/DHashMap/Lemmas.lean
View file

@ -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)} :

4
src/Std/Data/DTreeMap/Internal/Balanced.lean
View file

@ -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

6
src/Std/Data/DTreeMap/Internal/Balancing.lean
View file

@ -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]

24
src/Std/Data/DTreeMap/Internal/Operations.lean
View file

@ -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

4
src/Std/Data/DTreeMap/Internal/WF/Lemmas.lean
View file

@ -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

162
src/Std/Data/Internal/List/Associative.lean
View file

@ -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

2
src/Std/Data/Iterators/Lemmas/Combinators/Drop.lean
View file

@ -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 [*]

2
src/Std/Data/Iterators/Lemmas/Combinators/DropWhile.lean
View file

@ -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

2
src/Std/Data/Iterators/Lemmas/Combinators/Take.lean
View file

@ -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

2
src/Std/Data/Iterators/Lemmas/Consumers/Monadic/Collect.lean
View file

@ -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

2
src/Std/Do/SPred/Laws.lean
View file

@ -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⟩

4
src/Std/Sat/AIG/Basic.lean
View file

@ -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 =>

12
src/Std/Sat/AIG/CNF.lean
View file

@ -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]

10
src/Std/Sat/AIG/CachedLemmas.lean
View file

@ -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

6
src/Std/Sat/AIG/LawfulOperator.lean
View file

@ -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)

24
src/Std/Sat/AIG/Lemmas.lean
View file

@ -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

2
src/Std/Sat/AIG/RefVecOperator/Fold.lean
View file

@ -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

2
src/Std/Sat/AIG/RefVecOperator/Map.lean
View file

@ -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

6
src/Std/Sat/AIG/Relabel.lean
View file

@ -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

16
src/Std/Sat/AIG/RelabelNat.lean
View file

@ -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

2
src/Std/Tactic/BVDecide/Bitblast/BVExpr/Basic.lean
View file

@ -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

18
src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Expr.lean
View file

@ -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)]

14
src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Expr.lean
View file

@ -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

2
src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/Add.lean
View file

@ -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]

64
src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/Clz.lean
View file

@ -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)]

16
src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/Mul.lean
View file

@ -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]

12
src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/ShiftLeft.lean
View file

@ -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]

22
src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/ShiftRight.lean
View file

@ -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]

12
src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/Udiv.lean
View file

@ -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

8
src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/Umod.lean
View file

@ -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

4
src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/ZeroExtend.lean
View file

@ -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]

2
src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Pred.lean
View file

@ -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

2
src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Var.lean
View file

@ -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 =>

2
src/Std/Tactic/BVDecide/LRAT/Internal/Convert.lean
View file

@ -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]

4
src/Std/Tactic/BVDecide/LRAT/Internal/Entails.lean
View file

@ -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]

56
src/Std/Tactic/BVDecide/LRAT/Internal/Formula/Lemmas.lean
View file

@ -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

4
src/Std/Tactic/BVDecide/LRAT/Internal/Formula/RatAddResult.lean
View file

@ -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

30
src/Std/Tactic/BVDecide/LRAT/Internal/Formula/RatAddSound.lean
View file

@ -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

86
src/Std/Tactic/BVDecide/LRAT/Internal/Formula/RupAddResult.lean
View file

@ -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

88
src/Std/Tactic/BVDecide/LRAT/Internal/Formula/RupAddSound.lean
View file

@ -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]

6
tests/lean/grind/experiments/bitvec.lean
View file

@ -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

2
tests/lean/grind/experiments/list.lean
View file

@ -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 -/

6
tests/lean/run/1017.lean
View file

@ -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])

6
tests/lean/run/1337.lean
View file

@ -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

20
tests/lean/run/1711.lean
View file

@ -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

6
tests/lean/run/1841.lean
View file

@ -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

3
tests/lean/run/andCasesOnBug.lean
View file

@ -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;
};

15
tests/lean/run/as_aux_lemma.lean
View file

@ -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

2
tests/lean/run/doLogicTests.lean
View file

@ -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

10
tests/lean/run/grind_bitvec2.lean
View file

@ -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]]

2
tests/lean/run/issue2982.lean
View file

@ -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

24
tests/lean/run/nomatch_regression.lean
View file

@ -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