Skip to content

[Merged by Bors] - feat: port Archive.Wiedijk100Theorems.BallotProblem #5204

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Closed
int-y1 wants to merge 9 commits into from
Closed

[Merged by Bors] - feat: port Archive.Wiedijk100Theorems.BallotProblem #5204

Changes from 1 commit
Commits
Show all changes
9 commits
Select commit Hold shift + click to select a range
66ca83b
feat: port Archive.Wiedijk100Theorems.BallotProblem
int-y1 Jun 18, 2023
aeb5c52
Initial file copy from mathport
int-y1 Jun 18, 2023
7a31728
automated fixes
int-y1 Jun 18, 2023
908e6c3
fix
int-y1 Jun 18, 2023
883328d
small fix
int-y1 Jun 18, 2023
07505c9
fix list stuff
mo271 Jun 21, 2023
fbb3434
Merge branch 'master' into port/Archive.Wiedijk100Theorems.BallotProblem
mo271 Jun 21, 2023
c6a926f
small golf
int-y1 Jun 21, 2023
fced86d
golf 2
int-y1 Jun 21, 2023
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
Prev Previous commit
Next Next commit
fix list stuff
  • Loading branch information
@mo271
mo271 committed Jun 21, 2023
commit 07505c970dd73cfb8924d9ffe50271ef08fca2e4
34 changes: 23 additions & 11 deletions Archive/Wiedijk100Theorems/BallotProblem.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -125,23 +125,35 @@ theorem counted_succ_succ (p q : ℕ) :
· intro hl
have hlnil := counted_ne_nil_left (Nat.succ_ne_zero p) hl
obtain ⟨hl₀, hl₁, hl₂⟩ := hl
obtain hlast | hlast := hl₂ l.head (List.head!_mem_self hlnil)
obtain hlast | hlast := hl₂ l.head! (List.head!_mem_self hlnil)
· refine' Or.inl ⟨l.tail, ⟨_, _, _⟩, _⟩
· rw [List.count_tail l 1 (List.length_pos_of_ne_nil hlnil), hl₀, if_pos,
Nat.add_succ_sub_one, add_zero]
rw [List.nthLe_zero, hlast]
· rw [List.count_tail l 1 (List.length_pos_of_ne_nil hlnil)]
rw [hl₀, if_pos]
rw [Nat.add_succ_sub_one, add_zero]
cases l
· tauto
· simp only [List.head!_cons] at hlast
simp only [List.get]
exact hlast.symm
· rw [List.count_tail l (-1) (List.length_pos_of_ne_nil hlnil), hl₁, if_neg, Nat.sub_zero]
rw [List.nthLe_zero, hlast]
norm_num
cases l
· tauto
· simp only [List.head!_cons] at hlast
simp only [List.get, hlast]
· exact fun x hx => hl₂ x (List.mem_of_mem_tail hx)
· rw [← hlast, List.cons_head!_tail hlnil]
· refine' Or.inr ⟨l.tail, ⟨_, _, _⟩, _⟩
· rw [List.count_tail l 1 (List.length_pos_of_ne_nil hlnil), hl₀, if_neg, Nat.sub_zero]
rw [List.nthLe_zero, hlast]
norm_num
cases l
· tauto
· simp only [List.head!_cons] at hlast
simp only [List.get, hlast]
· rw [List.count_tail l (-1) (List.length_pos_of_ne_nil hlnil), hl₁, if_pos,
Nat.add_succ_sub_one, add_zero]
rw [List.nthLe_zero, hlast]
cases l
· tauto
· simp only [List.head!_cons] at hlast
simp only [List.get, hlast]
· exact fun x hx => hl₂ x (List.mem_of_mem_tail hx)
· rw [← hlast, List.cons_head!_tail hlnil]
· rintro (⟨t, ⟨ht₀, ht₁, ht₂⟩, rfl⟩ | ⟨t, ⟨ht₀, ht₁, ht₂⟩, rfl⟩)
Expand All @@ -150,13 +162,13 @@ theorem counted_succ_succ (p q : ℕ) :
· rw [List.count_cons, if_neg, ht₁]
norm_num
· rintro x (_ | _)
exacts [Or.inl rfl, ht₂ x _]
exacts [Or.inl rfl, ht₂ x (by tauto)]
· refine' ⟨_, _, _⟩
· rw [List.count_cons, if_neg, ht₀]
norm_num
· rw [List.count_cons, if_pos rfl, ht₁]
· rintro x (_ | _)
exacts [Or.inr rfl, ht₂ x _]
exacts [Or.inr rfl, ht₂ x (by tauto)]
#align ballot.counted_succ_succ Ballot.counted_succ_succ

theorem countedSequence_finite : ∀ p q : ℕ, (countedSequence p q).Finite
Expand Down