From 14bf7c026da18d607ee76c62ae1065ae1e521b32 Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Tue, 30 Jul 2024 00:02:52 +1000 Subject: [PATCH] fixes in Archive --- Archive/MiuLanguage/DecisionNec.lean | 6 ++++-- Archive/MiuLanguage/DecisionSuf.lean | 6 ++++-- Archive/Wiedijk100Theorems/BallotProblem.lean | 9 +++++---- 3 files changed, 13 insertions(+), 8 deletions(-) diff --git a/Archive/MiuLanguage/DecisionNec.lean b/Archive/MiuLanguage/DecisionNec.lean index 088a4d5867bf9..ba3cc0bc34669 100644 --- a/Archive/MiuLanguage/DecisionNec.lean +++ b/Archive/MiuLanguage/DecisionNec.lean @@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Gihan Marasingha -/ import Archive.MiuLanguage.Basic +import Mathlib.Data.List.Basic import Mathlib.Data.List.Count import Mathlib.Data.Nat.ModEq import Mathlib.Tactic.Ring @@ -71,9 +72,10 @@ theorem count_equiv_one_or_two_mod3_of_derivable (en : Miustr) : any_goals apply mod3_eq_1_or_mod3_eq_2 h_ih -- Porting note: `simp_rw [count_append]` usually doesn't work · left; rw [count_append, count_append]; rfl - · right; simp_rw [count_append, count_cons, if_false, two_mul]; simp + · right; simp_rw [count_append, count_cons, beq_iff_eq, ite_false, add_zero, two_mul] · left; rw [count_append, count_append, count_append] - simp_rw [count_cons_self, count_nil, count_cons, ite_false, add_right_comm, add_mod_right] + simp_rw [count_cons_self, count_nil, count_cons, beq_iff_eq, ite_false, add_right_comm, + add_mod_right] simp · left; rw [count_append, count_append, count_append] simp only [ne_eq, not_false_eq_true, count_cons_of_ne, count_nil, add_zero] diff --git a/Archive/MiuLanguage/DecisionSuf.lean b/Archive/MiuLanguage/DecisionSuf.lean index 4e460e9939ba2..10eaa8e26942b 100644 --- a/Archive/MiuLanguage/DecisionSuf.lean +++ b/Archive/MiuLanguage/DecisionSuf.lean @@ -251,7 +251,7 @@ theorem count_I_eq_length_of_count_U_zero_and_neg_mem {ys : Miustr} (hu : count · -- case `x = M` gives a contradiction. exfalso; exact hm (mem_cons_self M xs) · -- case `x = I` - rw [count_cons, if_pos rfl, length, succ_inj'] + rw [count_cons, beq_self_eq_true, if_pos rfl, length, succ_inj'] apply hxs · simpa only [count] · rw [mem_cons, not_or] at hm; exact hm.2 @@ -307,7 +307,9 @@ theorem ind_hyp_suf (k : ℕ) (ys : Miustr) (hu : count U ys = succ k) (hdec : D use as, bs refine ⟨rfl, ?_, ?_, ?_⟩ · -- Porting note: `simp_rw [count_append]` didn't work - rw [count_append] at hu; simp_rw [count_cons, if_true, add_succ, succ_inj'] at hu + rw [count_append] at hu + simp_rw [count_cons, beq_self_eq_true, if_true, add_succ, beq_iff_eq, reduceIte, add_zero, + succ_inj'] at hu rwa [count_append, count_append] · apply And.intro rfl rw [cons_append, cons_append] diff --git a/Archive/Wiedijk100Theorems/BallotProblem.lean b/Archive/Wiedijk100Theorems/BallotProblem.lean index b037dd8fab914..8b45732a49ddb 100644 --- a/Archive/Wiedijk100Theorems/BallotProblem.lean +++ b/Archive/Wiedijk100Theorems/BallotProblem.lean @@ -115,18 +115,19 @@ theorem counted_succ_succ (p q : ℕ) : obtain ⟨hl₀, hl₁, hl₂⟩ := hl obtain hlast | hlast := hl₂ (l.head hlnil) (List.head_mem hlnil) · refine Or.inl ⟨l.tail, ⟨?_, ?_, ?_⟩, ?_⟩ - · rw [List.count_tail l 1 hlnil, hl₀, hlast, if_pos rfl, Nat.add_sub_cancel] + · rw [List.count_tail l 1 hlnil, hl₀, hlast, beq_self_eq_true, if_pos rfl, Nat.add_sub_cancel] · rw [List.count_tail l (-1) hlnil, hl₁, hlast, if_neg (by decide), Nat.sub_zero] · exact fun x hx => hl₂ x (List.mem_of_mem_tail hx) · rw [← hlast, List.head_cons_tail] · refine Or.inr ⟨l.tail, ⟨?_, ?_, ?_⟩, ?_⟩ · rw [List.count_tail l 1 hlnil, hl₀, hlast, if_neg (by decide), Nat.sub_zero] - · rw [List.count_tail l (-1) hlnil, hl₁, hlast, if_pos rfl, Nat.add_sub_cancel] + · rw [List.count_tail l (-1) hlnil, hl₁, hlast, beq_self_eq_true, if_pos rfl, + Nat.add_sub_cancel] · exact fun x hx => hl₂ x (List.mem_of_mem_tail hx) · rw [← hlast, List.head_cons_tail] · rintro (⟨t, ⟨ht₀, ht₁, ht₂⟩, rfl⟩ | ⟨t, ⟨ht₀, ht₁, ht₂⟩, rfl⟩) · refine ⟨?_, ?_, ?_⟩ - · rw [List.count_cons, if_pos rfl, ht₀] + · rw [List.count_cons, beq_self_eq_true, if_pos rfl, ht₀] · rw [List.count_cons, if_neg, ht₁] norm_num · rintro x (_ | _) @@ -134,7 +135,7 @@ theorem counted_succ_succ (p q : ℕ) : · refine ⟨?_, ?_, ?_⟩ · rw [List.count_cons, if_neg, ht₀] norm_num - · rw [List.count_cons, if_pos rfl, ht₁] + · rw [List.count_cons, beq_self_eq_true, if_pos rfl, ht₁] · rintro x (_ | _) exacts [Or.inr rfl, ht₂ x (by tauto)]