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

chore: cleanup #5167 workarounds after update stage0 (#5175)

Browse source 
PR #5167 implemented RFC #5046, but it required several workarounds due
to staging issues. This PR cleans up these workarounds.
This commit is contained in:
Leonardo de Moura 2024-08-26 19:53:30 +02:00 • committed by GitHub
parent 3c687df6d5
commit f917f811c8
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
16 changed files with 42 additions and 53 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

3
src/Init/ByCases.lean
View file

@ -57,8 +57,7 @@ theorem apply_ite (f : α → β) (P : Prop) [Decidable P] (x y : α) :
-- We don't mark this as `simp` as it is already handled by `ite_eq_right_iff`.
theorem ite_some_none_eq_none [Decidable P] :
(if P then some x else none) = none ↔ ¬ P := by
have : some x ≠ none := Option.noConfusion
simp only [ite_eq_right_iff, this]
simp only [ite_eq_right_iff, reduceCtorEq]
rfl
@[simp] theorem ite_some_none_eq_some [Decidable P] :

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

@ -993,9 +993,8 @@ theorem signExtend_eq_not_zeroExtend_not_of_msb_false {x : BitVec w} {v : Nat} (
x.signExtend v = x.zeroExtend v := by
ext i
by_cases hv : i < v
· have : (false = true) = False := by simp
simp only [signExtend, getLsb, getLsb_zeroExtend, hv, decide_True, Bool.true_and, toNat_ofInt,
BitVec.toInt_eq_msb_cond, hmsb, ↓reduceIte, this]
· simp only [signExtend, getLsb, getLsb_zeroExtend, hv, decide_True, Bool.true_and, toNat_ofInt,
BitVec.toInt_eq_msb_cond, hmsb, ↓reduceIte, reduceCtorEq]
rw [Int.ofNat_mod_ofNat, Int.toNat_ofNat, Nat.testBit_mod_two_pow]
simp [BitVec.testBit_toNat]
· simp only [getLsb_zeroExtend, hv, decide_False, Bool.false_and]

6
src/Init/Data/List/Count.lean
View file

@ -47,11 +47,11 @@ theorem length_eq_countP_add_countP (l) : length l = countP p l + countP (fun a
if h : p x then
rw [countP_cons_of_pos _ _ h, countP_cons_of_neg _ _ _, length, ih]
· rw [Nat.add_assoc, Nat.add_comm _ 1, Nat.add_assoc]
· simp [h, not_true_eq_false, decide_False, not_false_eq_true]
· simp [h]
else
rw [countP_cons_of_pos (fun a => ¬p a) _ _, countP_cons_of_neg _ _ h, length, ih]
· rfl
· simp [h, not_false_eq_true, decide_True]
· simp [h]
theorem countP_eq_length_filter (l) : countP p l = length (filter p l) := by
induction l with
@ -234,7 +234,7 @@ theorem count_erase (a b : α) :
rw [if_pos hc_beq, hc, count_cons, Nat.add_sub_cancel]
else
have hc_beq := beq_false_of_ne hc
simp [hc_beq, if_false, count_cons, count_cons, count_erase a b l]
simp only [hc_beq, if_false, count_cons, count_cons, count_erase a b l, reduceCtorEq]
if ha : b = a then
rw [ha, eq_comm] at hc
rw [if_pos ((beq_iff_eq _ _).2 ha), if_neg (by simpa using Ne.symm hc), Nat.add_zero, Nat.add_zero]

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

@ -39,13 +39,13 @@ theorem eraseP_of_forall_not {l : List α} (h : ∀ a, a ∈ l → ¬p a) : l.er
| cons x xs ih =>
simp only [eraseP_cons, cond_eq_if]
split <;> rename_i h
· simp
· simp only [reduceCtorEq, cons.injEq, false_or]
constructor
· rintro rfl
simpa
· rintro ⟨_, _, rfl, rfl⟩
rfl
· simp
· simp only [reduceCtorEq, cons.injEq, false_or, false_iff, not_exists, not_and]
rintro x h' rfl
simp_all

4
src/Init/Data/List/Find.lean
View file

@ -737,10 +737,10 @@ theorem findIdx?_eq_enum_findSome? {xs : List α} {p : α → Bool} :
induction xs with
| nil => simp
| cons x xs ih =>
simp [findIdx?_cons, Nat.zero_add, findIdx?_succ, enum]
simp only [findIdx?_cons, Nat.zero_add, findIdx?_succ, enum]
split
· simp_all
· simp_all [enumFrom_cons, ite_false, Option.isNone_none, findSome?_cons_of_isNone]
· simp_all only [enumFrom_cons, ite_false, Option.isNone_none, findSome?_cons_of_isNone, reduceCtorEq]
simp [Function.comp_def, ← map_fst_add_enum_eq_enumFrom, findSome?_map]
theorem Sublist.findIdx?_isSome {l₁ l₂ : List α} (h : l₁ <+ l₂) :

2
src/Init/Data/List/Nat/Range.lean
View file

@ -200,7 +200,7 @@ theorem range'_eq_append_iff : range' s n = xs ++ ys ↔ ∃ k, k ≤ n ∧ xs =
cases k with
| zero => simp [range'_succ]
| succ k =>
simp [range'_succ, ih, exists_eq_left']
simp only [range'_succ, reduceCtorEq, false_and, cons.injEq, true_and, ih, range'_inj, exists_eq_left', or_true, and_true, false_or]
refine ⟨k, ?_⟩
simp_all
omega

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

@ -123,7 +123,7 @@ theorem pairwise_filterMap (f : β → Option α) {l : List β} :
match e : f a with
| none =>
rw [filterMap_cons_none e, pairwise_cons]
simp [e, false_implies, implies_true, true_and, IH]
simp only [e, false_implies, implies_true, true_and, IH, reduceCtorEq]
| some b =>
rw [filterMap_cons_some e]
simpa [IH, e] using fun _ =>

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

@ -136,7 +136,7 @@ theorem merge_stable : ∀ (xs ys) (_ : ∀ x y, x ∈ xs → y ∈ ys → x.1
simp only [map_cons, cons.injEq, true_and]
rw [merge_stable, map_cons]
exact fun x' y' mx my => h x' y' (mem_cons_of_mem (i, x) mx) my
· simp [↓reduceIte, map_cons, cons.injEq, true_and]
· simp only [↓reduceIte, map_cons, cons.injEq, true_and, reduceCtorEq]
rw [merge_stable, map_cons]
exact fun x' y' mx my => h x' y' mx (mem_cons_of_mem (j, y) my)

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

@ -123,7 +123,7 @@ theorem ne_zero_implies_bit_true {x : Nat} (xnz : x ≠ 0) : ∃ i, testBit x i
match mod_two_eq_zero_or_one x with
| Or.inl mod2_eq =>
rw [←div_add_mod x 2] at xnz
simp [mod2_eq, ne_eq, Nat.mul_eq_zero, Nat.add_zero, false_or] at xnz
simp only [mod2_eq, ne_eq, Nat.mul_eq_zero, Nat.add_zero, false_or, reduceCtorEq] at xnz
have ⟨d, dif⟩ := hyp x_pos xnz
apply Exists.intro (d+1)
simp_all

2
src/Init/WFTactics.lean
View file

@ -26,7 +26,7 @@ macro "clean_wf" : tactic =>
`(tactic| simp
(config := { unfoldPartialApp := true, zetaDelta := true, failIfUnchanged := false })
only [invImage, InvImage, Prod.lex, sizeOfWFRel, measure, Nat.lt_wfRel,
WellFoundedRelation.rel, sizeOf_nat])
WellFoundedRelation.rel, sizeOf_nat, reduceCtorEq])
/-- Extensible helper tactic for `decreasing_tactic`. This handles the "base case"
reasoning after applying lexicographic order lemmas.

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

@ -155,7 +155,7 @@ theorem isUnit_iff (c : DefaultClause n) (l : Literal (PosFin n)) :
split
· next l' heq => simp [heq]
· next hne =>
simp [false_iff]
simp
apply hne
def negate (c : DefaultClause n) : CNF.Clause (PosFin n) := c.clause.map Literal.negate

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

@ -154,9 +154,9 @@ theorem readyForRupAdd_ofArray {n : Nat} (arr : Array (Option (DefaultClause n))
exact cOpt_in_arr
· next b_eq_false =>
simp only [Bool.not_eq_true] at b_eq_false
simp [hasAssignment, b_eq_false, ite_false, hasNeg_addPos] at h
simp only [hasAssignment, b_eq_false, ite_false, hasNeg_addPos, reduceCtorEq] at h
specialize ih l false
simp [hasAssignment, ite_false] at ih
simp only [hasAssignment, ite_false] at ih
rw [b_eq_false, Subtype.ext i_eq_l]
exact ih h
· next i_ne_l =>
@ -302,8 +302,8 @@ theorem readyForRupAdd_insert {n : Nat} (f : DefaultFormula n) (c : DefaultClaus
· next b_eq_false =>
simp only [Bool.not_eq_true] at b_eq_false
exact b_eq_false
simp [hasAssignment, b_eq_false, l_eq_i, Array.getElem_modify_self i_in_bounds, ite_false, hasNeg_addPos] at hb
simp [hasAssignment, b_eq_false, ite_false, hb]
simp only [hasAssignment, b_eq_false, l_eq_i, Array.getElem_modify_self i_in_bounds, ite_false, hasNeg_addPos, reduceCtorEq] at hb
simp only [hasAssignment, b_eq_false, ite_false, hb, reduceCtorEq]
· next l_ne_i =>
simp only [Array.getElem_modify_of_ne i_in_bounds _ l_ne_i] at hb
exact hb

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

@ -17,9 +17,6 @@ namespace Internal
namespace DefaultFormula
-- TODO: remove aux lemma after update-stage0
private theorem false_ne_true : (false = true) = False := by simp
open Std.Sat
open DefaultClause DefaultFormula Assignment ReduceResult
@ -318,7 +315,7 @@ theorem sat_of_insertRat {n : Nat} (f : DefaultFormula n)
· apply Or.inr
rw [i'_eq_i] at i_true_in_c
apply And.intro i_true_in_c
simp only [addAssignment, ← b_eq_false, addNegAssignment, ite_false, false_ne_true] at h2
simp only [addAssignment, ← b_eq_false, addNegAssignment, ite_false, reduceCtorEq] at h2
split at h2
· next heq =>
have hasPosAssignment_fi : hasAssignment true (f.assignments[i.1]'i_in_bounds) := by
@ -408,8 +405,8 @@ theorem assignmentsInvariant_performRupCheck_of_assignmentsInvariant {n : Nat} (
rw [hb] at h
by_cases pi : p i
· exact pi
· simp at pi
simp [pi, decide_True, h] at h1
· simp only at pi
simp [pi, h] at h1
· simp only [Bool.not_eq_true] at hb
rw [hb]
rw [hb] at h

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

@ -20,9 +20,6 @@ namespace DefaultFormula
open Std.Sat
open DefaultClause DefaultFormula Assignment
-- TODO: remove aux lemma after update-stage0
private theorem false_ne_true : (false = true) = False := by simp
theorem size_insertUnit {n : Nat} (units : Array (Literal (PosFin n)))
(assignments : Array Assignment) (b : Bool) (l : Literal (PosFin n)) :
(insertUnit (units, assignments, b) l).2.1.size = assignments.size := by
@ -114,7 +111,7 @@ theorem insertUnitInvariant_insertUnit {n : Nat} (assignments0 : Array Assignmen
⟨units.size, units_size_lt_updatedUnits_size⟩
have i_gt_zero : i.1 > 0 := by rw [i_eq_l]; exact l.1.2.1
refine ⟨mostRecentUnitIdx, l.2, i_gt_zero, ?_⟩
simp [insertUnit, h3, ite_false, Array.get_push_eq, i_eq_l]
simp only [insertUnit, h3, ite_false, Array.get_push_eq, i_eq_l, reduceCtorEq]
constructor
· rfl
· constructor
@ -130,7 +127,7 @@ theorem insertUnitInvariant_insertUnit {n : Nat} (assignments0 : Array Assignmen
apply Nat.lt_of_le_of_ne
· apply Nat.le_of_lt_succ
have k_property := k.2
simp [insertUnit, h3, ite_false, Array.size_push] at k_property
simp only [insertUnit, h3, ite_false, Array.size_push, reduceCtorEq] at k_property
exact k_property
· intro h
simp only [← h, not_true, mostRecentUnitIdx] at hk
@ -140,7 +137,7 @@ theorem insertUnitInvariant_insertUnit {n : Nat} (assignments0 : Array Assignmen
exact h2 ⟨k.1, k_in_bounds⟩
· next i_ne_l =>
apply Or.inl
simp [insertUnit, h3, ite_false]
simp only [insertUnit, h3, ite_false, reduceCtorEq]
rw [Array.getElem_modify_of_ne i_in_bounds _ (Ne.symm i_ne_l)]
constructor
· exact h1
@ -192,7 +189,7 @@ theorem insertUnitInvariant_insertUnit {n : Nat} (assignments0 : Array Assignmen
exact h5 (has_add _ true)
| true, false =>
refine ⟨⟨j.1, j_lt_updatedUnits_size⟩, mostRecentUnitIdx, i_gt_zero, ?_⟩
simp [insertUnit, h5, ite_false, Array.get_push_eq, ne_eq]
simp only [insertUnit, h5, ite_false, Array.get_push_eq, ne_eq, reduceCtorEq]
constructor
· rw [Array.get_push_lt units l j.1 j.2, h1]
· constructor
@ -222,7 +219,7 @@ theorem insertUnitInvariant_insertUnit {n : Nat} (assignments0 : Array Assignmen
exact h4 ⟨k.1, h⟩ k_ne_j
· exfalso
have k_property := k.2
simp [insertUnit, h5, ite_false, Array.size_push] at k_property
simp only [insertUnit, h5, ite_false, Array.size_push, reduceCtorEq] at k_property
rcases Nat.lt_or_eq_of_le <| Nat.le_of_lt_succ k_property with k_lt_units_size | k_eq_units_size
· exact h k_lt_units_size
· simp only [← k_eq_units_size, not_true, mostRecentUnitIdx] at k_ne_l
@ -244,8 +241,8 @@ theorem insertUnitInvariant_insertUnit {n : Nat} (assignments0 : Array Assignmen
· match h : assignments0[i.val]'_ with
| unassigned => rfl
| pos =>
simp [addAssignment, h, ite_false, addNegAssignment] at h2
simp [i_eq_l] at h2
simp only [addAssignment, h, ite_false, addNegAssignment, reduceCtorEq] at h2
simp only [i_eq_l] at h2
simp [hasAssignment, hl, getElem!, l_in_bounds, h2, hasPosAssignment, decidableGetElem?] at h5
| neg => simp (config := {decide := true}) only [h] at h3
| both => simp (config := {decide := true}) only [h] at h3
@ -259,7 +256,7 @@ theorem insertUnitInvariant_insertUnit {n : Nat} (assignments0 : Array Assignmen
exact h4 ⟨k.1, h⟩ k_ne_j
· exfalso
have k_property := k.2
simp [insertUnit, h5, ite_false, Array.size_push] at k_property
simp only [insertUnit, h5, ite_false, Array.size_push, reduceCtorEq] at k_property
rcases Nat.lt_or_eq_of_le <| Nat.le_of_lt_succ k_property with k_lt_units_size | k_eq_units_size
· exact h k_lt_units_size
· simp only [← k_eq_units_size, not_true, mostRecentUnitIdx] at k_ne_l
@ -273,10 +270,10 @@ theorem insertUnitInvariant_insertUnit {n : Nat} (assignments0 : Array Assignmen
· 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 [insertUnit, h5, ite_false, Array.size_push]
simp only [insertUnit, h5, ite_false, Array.size_push, reduceCtorEq]
exact Nat.lt_trans j.2 (Nat.lt_succ_self units.size)
refine ⟨⟨j.1, j_lt_updatedUnits_size⟩, b,i_gt_zero, ?_⟩
simp [insertUnit, h5, ite_false]
simp only [insertUnit, h5, ite_false, reduceCtorEq]
constructor
· rw [Array.get_push_lt units l j.1 j.2, h1]
· constructor
@ -353,7 +350,7 @@ theorem insertUnitInvariant_insertUnit {n : Nat} (assignments0 : Array Assignmen
simp only
have k_eq_units_size : k.1 = units.size := by
have k_property := k.2
simp [insertUnit, h, ite_false, Array.size_push] at k_property
simp only [insertUnit, h, ite_false, Array.size_push, reduceCtorEq] at k_property
rcases Nat.lt_or_eq_of_le <| Nat.le_of_lt_succ k_property with k_lt_units_size | k_eq_units_size
· exfalso; exact k_not_lt_units_size k_lt_units_size
· exact k_eq_units_size
@ -876,7 +873,7 @@ theorem confirmRupHint_preserves_invariant_helper {n : Nat} (f : DefaultFormula
simp only [l'_eq_false, hasAssignment, ite_false] at h2
simp only [hasAssignment, l_eq_true, getElem!, l_eq_i, i_in_bounds,
Array.get_eq_getElem, ↓reduceIte, ↓reduceDIte, h1, addAssignment, l'_eq_false,
hasPos_addNeg, decidableGetElem?, false_ne_true] at h
hasPos_addNeg, decidableGetElem?, reduceCtorEq] at h
exact unassigned_of_has_neither _ h h2
· intro k k_ne_zero k_ne_j_succ
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
@ -924,7 +921,7 @@ theorem confirmRupHint_preserves_invariant_helper {n : Nat} (f : DefaultFormula
· simp only [l'] at l'_eq_true
simp only [hasAssignment, l'_eq_true, ite_true] at h2
simp only [hasAssignment, l_eq_false, ↓reduceIte, getElem!, l_eq_i, i_in_bounds,
Array.get_eq_getElem, h1, addAssignment, l'_eq_true, hasNeg_addPos, decidableGetElem?, false_ne_true] at h
Array.get_eq_getElem, h1, addAssignment, l'_eq_true, hasNeg_addPos, decidableGetElem?, reduceCtorEq] at h
exact unassigned_of_has_neither _ h2 h
· intro k k_ne_j_succ 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

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

@ -17,9 +17,6 @@ namespace Internal
namespace DefaultFormula
-- TODO: remove aux lemma after update-stage0
private theorem false_ne_true : (false = true) = False := by simp
open Std.Sat
open DefaultClause DefaultFormula Assignment ReduceResult
@ -52,7 +49,7 @@ theorem contradiction_of_insertUnit_success {n : Nat} (assignments : Array Assig
simp [Array.getElem_modify_of_ne i_in_bounds _ l_ne_i]
exact h
· apply Exists.intro l.1
simp only [insertUnit, hl, ite_false, Array.getElem_modify_self l_in_bounds, false_ne_true]
simp only [insertUnit, hl, ite_false, Array.getElem_modify_self l_in_bounds, reduceCtorEq]
simp only [getElem!, l_in_bounds, dite_true, decidableGetElem?] at assignments_l_ne_unassigned
by_cases l.2
· next l_eq_true =>
@ -184,7 +181,7 @@ theorem sat_of_insertRup {n : Nat} (f : DefaultFormula n) (f_readyForRupAdd : Re
· apply Or.inr
rw [i'_eq_i] at i_true_in_c
apply And.intro i_true_in_c
simp only [addAssignment, ← b_eq_false, addNegAssignment, ite_false, false_ne_true] at h2
simp only [addAssignment, ← b_eq_false, addNegAssignment, ite_false, reduceCtorEq] at h2
split at h2
· next heq =>
have hasPosAssignment_fi : hasAssignment true (f.assignments[i.1]'i_in_bounds) := by
@ -669,7 +666,7 @@ theorem confirmRupHint_preserves_motive {n : Nat} (f : DefaultFormula n) (rupHin
simp only [ConfirmRupHintFoldEntailsMotive]
split
· simp [h1, hsize]
· simp [Array.size_modify, hsize]
· simp only [Array.size_modify, hsize, Bool.false_eq_true, false_implies, and_true, true_and]
intro p pf
have pacc := h1 p pf
have pc : p ⊨ c := by
@ -703,7 +700,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
· simp only [Bool.not_eq_true] at hb
simp only [hasAssignment, addAssignment, hb, ite_false, ite_true, hasPos_addNeg, false_ne_true]
simp only [hasAssignment, addAssignment, hb, ite_false, ite_true, hasPos_addNeg, reduceCtorEq]
simp only [hasAssignment, ite_true] at pacc
exact pacc
· next l_ne_i =>

4
tests/lean/mutwf1.lean
View file

@ -6,8 +6,8 @@ mutual
| n, false => n + g n
termination_by n b => (n, if b then 2 else 1)
decreasing_by
· apply Prod.Lex.right; simp -- decide TODO: add `reduceCtorEq` at `clean_wf` after update-stage0
· apply Prod.Lex.right; simp -- decide
· apply Prod.Lex.right; decide
· apply Prod.Lex.right; decide
def g (n : Nat) : Nat :=
if h : n ≠ 0 then