Skip to content

Simp final step #8

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

Merged
ChihChengLiang merged 6 commits into from
Mar 16, 2026
Merged

Simp final step #8

Changes from all commits
Commits
Show all changes
6 commits
Select commit Hold shift + click to select a range
55c42a9
less branching in final step
ChihChengLiang Mar 16, 2026
f5cc832
claude improvement
ChihChengLiang Mar 16, 2026
55cd1b9
unesting with b ≠ x
ChihChengLiang Mar 16, 2026
b18e9b8
all subst gone, add comments
ChihChengLiang Mar 16, 2026
790d294
cleanup proof direction
ChihChengLiang Mar 16, 2026
c432605
OCD picks
ChihChengLiang Mar 16, 2026
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
67 changes: 28 additions & 39 deletions Arrow/Basic.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -91,14 +91,14 @@ def AIIA (R : SWF α N) : Prop :=
∀ (p q: Profile α N) (a b: α),
AgreeOn p q a b → ((a ≽[R p] b) ↔ a ≽[R q] b) ∧ ((b ≽[R p] a) ↔ b ≽[R q] a)

lemma strict_aiia {R: SWF α N}
{p q: Profile α N} {a b: α} (hagree: AgreeOn p q a b) (hAIIA: AIIA R):
(a ≻[R p] b) ↔ a ≻[R q] b := by simp [Preorder'.lt, hAIIA _ _ _ _ hagree]

/-- **Non-Dictatorship**: No single voter dictates the outcome for all pairs. -/
def NonDictatorship (R : SWF α N): Prop :=
¬ (∃ i: Fin N, ∀ (a b: α), (a ≠ b) → Dictates R i a b)

lemma strict_aiia {R: SWF α N}
{p q: Profile α N} {a b: α} (hagree: AgreeOn p q a b) (hAIIA: AIIA R):
(a ≻[R p] b) ↔ a ≻[R q] b := by simp [Preorder'.lt, hAIIA _ _ _ _ hagree]

/-! ## Preference Construction

We construct concrete preference orderings to build test profiles for the proof.
Expand Down Expand Up @@ -233,9 +233,9 @@ lemma nab_pivotal_bc (a b c: α)
have hba := Ne.symm hab; have hca := Ne.symm hac; have hcb := Ne.symm hbc

-- Magic profile 1
-- 0 ... k-1 prefer b > c > a
-- k ... N-1 prefer a > b > c
-- Result: Society prefers a > b > c
-- 0 ... k-1 prefer b ≻ c ≻ a
-- k ... N-1 prefer a ≻ b ≻ c
-- Result: Society prefers a ≻ b ≻ c
let mg1: Profile α N := fun i: Fin N =>
if i < n_ab.val
then prefer b c a .Not hba
Expand Down Expand Up @@ -418,38 +418,27 @@ lemma n_ab_dictate_xy (a b c x y: α)
(hab : a ≠ b) (hac : a ≠ c) (hbc : b ≠ c) (hxy : x ≠ y)
(hu: Unanimity R) (hAIIA: AIIA R):
Dictates R (pivoter a b hab hu) x y := by
-- Collect pivotal voter equalities for {a,b,c}
obtain ⟨h_nbc_eq_ncb, h_ncb_eq_nab⟩ := n_ab_pivotal_bc_cb a b c hab hac hbc hu hAIIA
obtain ⟨h_nab_eq_nba, h_nba_eq_nca⟩ := n_ab_pivotal_bc_cb c a b (Ne.symm hac) (Ne.symm hbc) hab hu hAIIA
obtain ⟨_, h_nbc_eq_nac⟩ := n_ab_pivotal_bc_cb a c b hac hab (Ne.symm hbc) hu hAIIA
by_cases hxa : x = a; subst x
. by_cases hyb : y = b; subst y
. simpa [← h_nba_eq_nca, ← h_nab_eq_nba] using nab_pivotal_bc c a b (Ne.symm hac) (Ne.symm hbc) hab hu hAIIA
. by_cases hyc : y = c; subst y
. simpa [← h_nab_eq_nba] using nab_pivotal_bc b a c (Ne.symm hab) hbc hac hu hAIIA
. simpa [← h_nab_eq_nba] using nab_pivotal_bc b a y (Ne.symm hab) (Ne.symm hyb) hxy hu hAIIA
. by_cases hxb : x = b; subst x
. by_cases hya : y = a; subst y
. simpa [h_ncb_eq_nab] using nab_pivotal_bc c b a (Ne.symm hbc) (Ne.symm hac) (Ne.symm hab) hu hAIIA
. by_cases hyc : y = c; subst y
. exact nab_pivotal_bc a b c hab hac hbc hu hAIIA
. exact nab_pivotal_bc a b y hab (Ne.symm hya) hxy hu hAIIA
. by_cases hxc : x = c; subst x
. by_cases hya : y = a; subst y
. simpa [h_nbc_eq_ncb, h_ncb_eq_nab] using nab_pivotal_bc b c a hbc (Ne.symm hab) (Ne.symm hac) hu hAIIA
. by_cases hyb : y = b; subst y
. simpa [← h_nbc_eq_nac, h_nbc_eq_ncb, h_ncb_eq_nab] using nab_pivotal_bc a c b hac hab (Ne.symm hbc) hu hAIIA
. simpa [h_nbc_eq_ncb, h_ncb_eq_nab] using nab_pivotal_bc b c y hbc (Ne.symm hyb) hxy hu hAIIA
. -- x ∉ {a,b,c}
obtain ⟨h_nbx_eq_nxb, h_nxb_eq_nab⟩ := n_ab_pivotal_bc_cb a b x hab (Ne.symm hxa) (Ne.symm hxb) hu hAIIA
obtain ⟨_, h_nbx_eq_nax⟩ := n_ab_pivotal_bc_cb a x b (Ne.symm hxa) hab hxb hu hAIIA
by_cases hya : y = a; subst y
. simpa [h_nbx_eq_nxb, h_nxb_eq_nab] using nab_pivotal_bc b x a (Ne.symm hxb) (Ne.symm hab) hxa hu hAIIA
. by_cases hyb : y = b; subst y
. simpa [← h_nbx_eq_nax, h_nbx_eq_nxb, h_nxb_eq_nab] using nab_pivotal_bc a x b (Ne.symm hxa) hab hxb hu hAIIA
. by_cases hyc : y = c; subst y
. simpa [← h_nbx_eq_nax, h_nbx_eq_nxb, h_nxb_eq_nab] using nab_pivotal_bc a x c (Ne.symm hxa) hac hxc hu hAIIA
. simpa [h_nbx_eq_nxb, h_nxb_eq_nab] using nab_pivotal_bc b x y (Ne.symm hxb) (Ne.symm hyb) hxy hu hAIIA
have := nab_pivotal_bc a b c hab hac hbc hu hAIIA
have := n_ab_pivotal_bc_cb a b c hab hac hbc hu hAIIA
have := n_ab_pivotal_bc_cb a c b hac hab (Ne.symm hbc) hu hAIIA
by_cases hxb: x ≠ b <;> by_cases hxc: x ≠ c <;> by_cases hyc: y ≠ c <;> simp_all <;> try subst x y
-- x ∉ {b, c}, y ≠ c
. have := nab_pivotal_bc c x y (Ne.symm hxc) (Ne.symm hyc) hxy hu hAIIA
have := n_ab_pivotal_bc_cb b c x hbc (Ne.symm hxb) (Ne.symm hxc) hu hAIIA
simp_all
-- x ∉ {b, c}, y = c
. have := nab_pivotal_bc b x c (Ne.symm hxb) hbc hxc hu hAIIA
have := n_ab_pivotal_bc_cb c b x (Ne.symm hbc) (Ne.symm hxc) (Ne.symm hxb) hu hAIIA
simp_all
-- x = c, y ≠ c
. by_cases hyb: y ≠ b
. have := nab_pivotal_bc b c y hbc (Ne.symm hyb) (Ne.symm hyc) hu hAIIA
simp_all
. have := nab_pivotal_bc a c b hac hab (Ne.symm hbc) hu hAIIA
simp_all
-- x = b, y ≠ c
. have := nab_pivotal_bc c b y (Ne.symm hbc) (Ne.symm hyc) hxy hu hAIIA
simp_all

/-- **Arrow's Impossibility Theorem**: No SWF with ≥3 alternatives and ≥1 voters
can satisfy Unanimity, IIA, and Non-Dictatorship simultaneously. -/
Expand Down
Loading