From f9eb3f33d2222b3451e90afdb383d0fe67c197a7 Mon Sep 17 00:00:00 2001 From: ChihChengLiang Date: Sun, 15 Mar 2026 22:34:00 +0800 Subject: [PATCH 01/20] add prefer expand --- Arrow/Basic.lean | 26 ++++++++++++++++++++++++++ 1 file changed, 26 insertions(+) diff --git a/Arrow/Basic.lean b/Arrow/Basic.lean index 823dffb..4b36d3f 100644 --- a/Arrow/Basic.lean +++ b/Arrow/Basic.lean @@ -168,6 +168,32 @@ def prefer (a₀ _a₁ a₂ : α) (tie : Tie) (h02 : a₀ ≠ a₂) : Preorder' · simp only; by_cases hxa : a = a₂ <;> by_cases hya : b = a₂ <;> simp_all · simp only; by_cases hxa : a = a₀ <;> by_cases hya : b = a₀ <;> simp_all +lemma prefer_expand + (top mid bot: α)(tie: Tie) + (htm: top ≠ mid)(hmb: mid≠ bot)(htb: top ≠ bot) + :let p:= prefer top mid bot tie htb + (top ≽[p] mid) ∧ (mid ≽[p] bot) ∧ (top ≽[p] bot) ∧ (¬ bot ≽[p] top) ∧ + (match tie with + | .Not => (¬ mid ≽[p] top) ∧ (¬ bot ≽[p] mid) + | .Top => ( mid ≽[p] top) ∧ (¬ bot ≽[p] mid) + | .Bot => (¬ mid ≽[p] top) ∧ ( bot ≽[p] mid) + ) + := by + intro p + unfold p prefer + simp + refine ⟨?_, ?_, ?_, ?_, ?_⟩ + . split <;> simp_all + . split <;> try trivial + intro h; exact absurd h (Ne.symm htb) + . split <;> trivial + . split <;> simp_all <;> push_neg <;> exact Ne.symm htb + . split <;> simp_all <;> push_neg + . exact ⟨ Ne.symm htm, Ne.symm htb⟩ + . constructor + . exact Ne.symm htm + . intro h; exact absurd h (Ne.symm htm) + /-! ### Lemmas for Tie.Not (strict ranking a₀ > a₁ > a₂) -/ /-- In `prefer a₀ a₁ a₂ .Not`, we have `a₀ > a₁`. -/ From 2e92f91e8b90eb6aa2408ef9cc3d1d21f236d44f Mon Sep 17 00:00:00 2001 From: ChihChengLiang Date: Sun, 15 Mar 2026 23:47:24 +0800 Subject: [PATCH 02/20] fixed some existing broken proofs --- Arrow/Basic.lean | 93 ++++++++++++++++++++---------------------------- 1 file changed, 39 insertions(+), 54 deletions(-) diff --git a/Arrow/Basic.lean b/Arrow/Basic.lean index 4b36d3f..68b329a 100644 --- a/Arrow/Basic.lean +++ b/Arrow/Basic.lean @@ -169,14 +169,13 @@ def prefer (a₀ _a₁ a₂ : α) (tie : Tie) (h02 : a₀ ≠ a₂) : Preorder' · simp only; by_cases hxa : a = a₀ <;> by_cases hya : b = a₀ <;> simp_all lemma prefer_expand - (top mid bot: α)(tie: Tie) - (htm: top ≠ mid)(hmb: mid≠ bot)(htb: top ≠ bot) + (top mid bot: α)(tie: Tie)(htb: top ≠ bot) :let p:= prefer top mid bot tie htb (top ≽[p] mid) ∧ (mid ≽[p] bot) ∧ (top ≽[p] bot) ∧ (¬ bot ≽[p] top) ∧ (match tie with - | .Not => (¬ mid ≽[p] top) ∧ (¬ bot ≽[p] mid) - | .Top => ( mid ≽[p] top) ∧ (¬ bot ≽[p] mid) - | .Bot => (¬ mid ≽[p] top) ∧ ( bot ≽[p] mid) + | .Not => (mid≠top → ¬ mid ≽[p] top) ∧ (bot≠ mid → ¬ bot ≽[p] mid) + | .Top => bot≠mid → ((mid ≽[p] top) ∧ (¬ bot ≽[p] mid)) + | .Bot => mid≠top → ((¬ mid ≽[p] top) ∧ (bot ≽[p] mid)) ) := by intro p @@ -187,12 +186,11 @@ lemma prefer_expand . split <;> try trivial intro h; exact absurd h (Ne.symm htb) . split <;> trivial - . split <;> simp_all <;> push_neg <;> exact Ne.symm htb - . split <;> simp_all <;> push_neg - . exact ⟨ Ne.symm htm, Ne.symm htb⟩ - . constructor - . exact Ne.symm htm - . intro h; exact absurd h (Ne.symm htm) + . split <;> try simp_all <;> push_neg <;> exact Ne.symm htb + push_neg; exact Ne.symm htb + . split <;> simp_all + . intro h; exact ⟨ Ne.symm h, Ne.symm htb⟩ ; + . intro h; exact Ne.symm h /-! ### Lemmas for Tie.Not (strict ranking a₀ > a₁ > a₂) -/ @@ -288,8 +286,8 @@ variable [NeZero N] {R : SWF α N} def canonicalSwap (a b : α) (hab : a ≠ b) : Fin (N+1) → Profile α N := fun k: Fin (N+1) => fun i: Fin N => if i < k.val - then prefer b b a .Not (Ne.symm hab) -- b on top - else prefer a b b .Not hab -- a on top + then prefer b b a .Top (Ne.symm hab) -- b on top + else prefer a b b .Bot hab -- a on top /-- `flipping R a b hab k` holds iff society prefers `b ≻ a` when voters `0..k` prefer `b ≻ a`. -/ def flipping (R : SWF α N) (a b : α) (hab : a ≠ b) := @@ -302,8 +300,10 @@ lemma flip_exists (R : SWF α N) (a b : α) (hab : a ≠ b) (hu : Unanimity R): unfold flipping canonicalSwap have: 0 < N := Nat.pos_of_ne_zero (NeZero.ne N) simp [Nat.sub_add_cancel this] - have: b ≻[R (fun i => prefer b b a .Not (Ne.symm hab) )] a := by - apply hu; intro i; simp [prefer_lt_02 b _ a (Ne.symm hab)] + have: b ≻[R (fun i => prefer b b a .Top (Ne.symm hab) )] a := by + apply hu; intro i; + have := prefer_expand b b a .Top (Ne.symm hab) + exact ⟨this.2.1, this.2.2.2.1⟩ exact this.1 /-- The pivotal voter for `(a, b)`: the minimum `k` where society flips from `a ≻ b` to `b ≻ a`. -/ @@ -358,14 +358,9 @@ lemma nab_pivotal_bc (a b c: α) have hp : AgreeOn mg1 (canonicalSwap a b hab k.succ) a b := by intro i; simp only [mg1, canonicalSwap] by_cases hi : i.val < n_ab.val <;> simp [hk_succ, hi] - . constructor - . rw[← not_iff_not] - simp only [(prefer_lt_02 b c a (Ne.symm hab)).2, (prefer_lt_02 b b a (Ne.symm hab)).2] - . simp only [prefer_le_02 b c a (Ne.symm hab), prefer_le_02 b b a (Ne.symm hab)] - . constructor - . simp only [prefer_le_01 a b c hac, prefer_le_01 a b b hab] - . rw[← not_iff_not] - simp only [(prefer_lt_01 a b c hab hac).2, (prefer_lt_01 a b b hab hab).2] + . simp [prefer_expand b c a .Not (Ne.symm hab), prefer_expand b b a .Top] + . have := prefer_expand a b c .Not hac + simp [this, prefer_expand a b b .Bot, this.2.2.2.2.1 (Ne.symm hab)] apply (strict_aiia hp hAIIA).mpr exact no_flip a b k hk @@ -428,37 +423,23 @@ lemma nab_pivotal_bc (a b c: α) unfold AgreeOn canonicalSwap mg2; intro i; by_cases hi: i < n_ab . have :i.val < n_ab +1 := by omega - simp [hi, this] - constructor - . simp only [prefer_le_02 b b a (Ne.symm hab)] - cases (pp i).cmp b c with - | LT _ _ => simp only [prefer_le_12 c b a (Ne.symm hac)] - | GT _ _ => simp only [prefer_le_02 b c a (Ne.symm hab)] - | Indiff _ _ => simp only [prefer_top_le_02 b c a (Ne.symm hab)] - . rw[← not_iff_not] - simp [(prefer_lt_02 b b a (Ne.symm hab)).2] - cases (pp i).cmp b c with - | LT _ _ => simp [(prefer_lt_12 c b a (Ne.symm hab) (Ne.symm hac)).2] - | GT _ _ => simp [(prefer_lt_02 b c a (Ne.symm hab)).2] - | Indiff _ _ => simp [(prefer_top_lt_02 b c a (Ne.symm hab)).2] + simp [hi, this, prefer_expand b b a .Top] + split + . have := prefer_expand c b a .Not (Ne.symm hac) + simp [this, this.2.2.2.2.2 hab] + . simp [prefer_expand b c a .Not (Ne.symm hab)] + . simp [prefer_expand b c a .Top (Ne.symm hab)] . by_cases hi2: i = n_ab - . simp [hi2, prefer_le_01 b a c hbc, prefer_le_02 b b a (Ne.symm hab)] - rw[← not_iff_not] - simp [(prefer_lt_01 b a c (Ne.symm hab) hbc).2, (prefer_lt_02 b b a (Ne.symm hab)).2] + . have := prefer_expand b a c .Not hbc + simp [hi2, prefer_expand b b a .Top, this, this.2.2.2.2.1 hab] . have :¬ (i.val < n_ab +1 ):= by omega - simp [hi, hi2, this] - constructor - . rw[← not_iff_not] - simp [(prefer_lt_02 a b b hab).2] - cases (pp i).cmp b c with - | LT _ _ => simp [(prefer_lt_02 a c b hab).2] - | GT _ _ => simp [(prefer_lt_01 a b c hab hac).2] - | Indiff _ _ => simp [(prefer_bot_lt_01 a b c hac hab).2] - . simp only [(prefer_lt_02 a b b hab).1] - cases (pp i).cmp b c with - | LT _ _ => simp [(prefer_lt_02 a c b hab).1] - | GT _ _ => simp [(prefer_lt_01 a b c hab hac).1] - | Indiff _ _ => simp [(prefer_bot_lt_01 a b c hac hab).1] + simp [hi, hi2, this, prefer_expand a b b .Bot] + split + . simp [prefer_expand a c b .Not hab] + . have := prefer_expand a b c .Not hac + simp [this, this.2.2.2.2.1 (Ne.symm hab)] + . have := prefer_expand a b c .Bot hac + simp [this, (this.2.2.2.2 (Ne.symm hab)).1] apply (hAIIA _ _ _ _ h_agree_ba).1.mpr exact flipped a b -- By AIIA @@ -515,7 +496,8 @@ lemma nab_le_nbc (a b c: α) simp only [cs, canonicalSwap] split_ifs with hh . simp at hh; omega - . exact prefer_lt_02 b _ c hbc + . have := prefer_expand b c c .Bot hbc + exact ⟨this.1, (this.2.2.2.2 (Ne.symm hbc)).1 ⟩ exact absurd (nab_pivotal_bc a b c hab hac hbc hu hAIIA cs h_pref) -- n_ab still dictates b over c ((Preorder'.not_lt _ _ _).mpr (flipped b c)) -- but n_bc flipped, so society should prefer c over b @@ -528,7 +510,10 @@ lemma ncb_le_nab (a b c: α) by_contra h; push_neg at h let n_ab := pivoter a b hab hu let cs := canonicalSwap c b (Ne.symm hbc) n_ab.succ - have: b ≻[cs n_ab] c := by simp [cs, canonicalSwap, prefer_lt_02 b _ c hbc] + have: b ≻[cs n_ab] c := by + simp [cs, canonicalSwap] + have := prefer_expand b b c .Top hbc + exact ⟨ this.2.1, (this.2.2.2.2 (Ne.symm hbc)).2⟩ exact absurd (nab_pivotal_bc a b c hab hac hbc hu hAIIA cs this) -- n_ab prefer b over c, so is society (Preorder'.lt_asymm _ _ _ (no_flip c b n_ab h)) -- n_ab before pivoter, so b c shouldn't flip From d39515fe9f320b6c2a044880899f88622ebcadef Mon Sep 17 00:00:00 2001 From: ChihChengLiang Date: Mon, 16 Mar 2026 00:51:58 +0800 Subject: [PATCH 03/20] one helper lemma to rule them all --- Arrow/Basic.lean | 184 ++++++++++++++--------------------------------- 1 file changed, 52 insertions(+), 132 deletions(-) diff --git a/Arrow/Basic.lean b/Arrow/Basic.lean index 68b329a..b4a7549 100644 --- a/Arrow/Basic.lean +++ b/Arrow/Basic.lean @@ -192,86 +192,6 @@ lemma prefer_expand . intro h; exact ⟨ Ne.symm h, Ne.symm htb⟩ ; . intro h; exact Ne.symm h -/-! ### Lemmas for Tie.Not (strict ranking a₀ > a₁ > a₂) -/ - -/-- In `prefer a₀ a₁ a₂ .Not`, we have `a₀ > a₁`. -/ -lemma prefer_lt_01 (a₀ a₁ a₂ : α) (h01 : a₀ ≠ a₁) (h02 : a₀ ≠ a₂) : - (prefer a₀ a₁ a₂ .Not h02).lt a₁ a₀ := by - simp [Preorder'.lt, prefer, h02, Ne.symm h01] - -lemma prefer_le_01 (a₀ a₁ a₂ : α) (h02 : a₀ ≠ a₂) : - (prefer a₀ a₁ a₂ .Not h02).le a₁ a₀ := by simp [prefer] - -lemma prefer_lt_12 (a₀ a₁ a₂ : α) (h12 : a₁ ≠ a₂) (h02 : a₀ ≠ a₂) : - (prefer a₀ a₁ a₂ .Not h02).lt a₂ a₁ := by - simp [Preorder'.lt, prefer, h12, Ne.symm h02] - -lemma prefer_le_12 (a₀ a₁ a₂ : α) (h02 : a₀ ≠ a₂) : - (prefer a₀ a₁ a₂ .Not h02).le a₂ a₁ := by simp [prefer] - -lemma prefer_lt_02 (a₀ a₁ a₂ : α) (h02 : a₀ ≠ a₂) : - (prefer a₀ a₁ a₂ .Not h02).lt a₂ a₀ := by - simp [Preorder'.lt, prefer, h02, Ne.symm h02] - -lemma prefer_le_02 (a₀ a₁ a₂ : α) (h02 : a₀ ≠ a₂) : - (prefer a₀ a₁ a₂ .Not h02).le a₂ a₀ := by simp [prefer] - -/-! ### Lemmas for Tie.Top (a₀ ~ a₁ > a₂) -/ - -/-- In `prefer a₀ a₁ a₂ .Top`, we have a₀ > a₂ -/ -lemma prefer_top_lt_02 (a₀ a₁ a₂ : α) (h02 : a₀ ≠ a₂) : - (prefer a₀ a₁ a₂ .Top h02).lt a₂ a₀ := by - simp [Preorder'.lt, prefer, h02] - -/-- In `prefer a₀ a₁ a₂ .Top`, we have a₁ > a₂ -/ -lemma prefer_top_lt_12 (a₀ a₁ a₂ : α) (h02 : a₀ ≠ a₂) (h12 : a₁ ≠ a₂) : - (prefer a₀ a₁ a₂ .Top h02).lt a₂ a₁ := by - simp [Preorder'.lt, prefer, h12] - -/-- In `prefer a₀ a₁ a₂ .Top`, a₀ and a₁ are indifferent: a₀ ≤ a₁ -/ -lemma prefer_top_le_01 (a₀ a₁ a₂ : α) (h02 : a₀ ≠ a₂) (h12 : a₁ ≠ a₂) : - (prefer a₀ a₁ a₂ .Top h02).le a₀ a₁ := by - simp [prefer, h02, h12] - -/-- In `prefer a₀ a₁ a₂ .Top`, a₀ and a₁ are indifferent: a₁ ≤ a₀ -/ -lemma prefer_top_le_10 (a₀ a₁ a₂ : α) (h02 : a₀ ≠ a₂): - (prefer a₀ a₁ a₂ .Top h02).le a₁ a₀ := by - simp [prefer, h02] - -lemma prefer_top_le_02 (a₀ a₁ a₂ : α) (h02 : a₀ ≠ a₂) : - (prefer a₀ a₁ a₂ .Top h02).le a₂ a₀ := by simp [prefer] - -lemma prefer_top_le_12 (a₀ a₁ a₂ : α) (h02 : a₀ ≠ a₂) : - (prefer a₀ a₁ a₂ .Top h02).le a₂ a₁ := by simp [prefer] - -/-! ### Lemmas for Tie.Bot (a₀ > a₁ ~ a₂) -/ - -/-- In `prefer a₀ a₁ a₂ .Bot`, we have a₀ > a₁ -/ -lemma prefer_bot_lt_01 (a₀ a₁ a₂ : α) (h02 : a₀ ≠ a₂) (h01 : a₀ ≠ a₁) : - (prefer a₀ a₁ a₂ .Bot h02).lt a₁ a₀ := by - simp [Preorder'.lt, prefer, Ne.symm h01] - -/-- In `prefer a₀ a₁ a₂ .Bot`, we have a₀ > a₂ -/ -lemma prefer_bot_lt_02 (a₀ a₁ a₂ : α) (h02 : a₀ ≠ a₂) : - (prefer a₀ a₁ a₂ .Bot h02).lt a₂ a₀ := by - simp [Preorder'.lt, prefer, Ne.symm h02] - -/-- In `prefer a₀ a₁ a₂ .Bot`, a₁ and a₂ are indifferent: a₁ ≤ a₂ -/ -lemma prefer_bot_le_12 (a₀ a₁ a₂ : α) (h02 : a₀ ≠ a₂) (h01 : a₀ ≠ a₁) : - (prefer a₀ a₁ a₂ .Bot h02).le a₁ a₂ := by - simp [prefer, Ne.symm h02, Ne.symm h01] - -/-- In `prefer a₀ a₁ a₂ .Bot`, a₁ and a₂ are indifferent: a₂ ≤ a₁ -/ -lemma prefer_bot_le_21 (a₀ a₁ a₂ : α) (h02 : a₀ ≠ a₂) (h01 : a₀ ≠ a₁) : - (prefer a₀ a₁ a₂ .Bot h02).le a₂ a₁ := by - simp [prefer, Ne.symm h01, Ne.symm h02] - -lemma prefer_bot_le_01 (a₀ a₁ a₂ : α) (h02 : a₀ ≠ a₂) (h01 : a₀ ≠ a₁) : - (prefer a₀ a₁ a₂ .Bot h02).le a₁ a₀ := by simp [prefer, Ne.symm h01] - -lemma prefer_bot_le_02 (a₀ a₁ a₂ : α) (h02 : a₀ ≠ a₂) : - (prefer a₀ a₁ a₂ .Bot h02).le a₂ a₀ := by simp [prefer, Ne.symm h02] - /-! ## Pivotal Voter The key construction: we find the "pivotal voter" who flips society's preference. @@ -347,7 +267,8 @@ lemma nab_pivotal_bc (a b c: α) . -- Case n_ab = 0: All voters prefer a > b, use unanimity have h : ∀ i : Fin N, a ≻[mg1 i] b := by intro i; simp [mg1, hn] - exact prefer_lt_01 a b c hab hac + have := prefer_expand a b c .Not hac + exact ⟨ this.1, this.2.2.2.2.1 (Ne.symm hab)⟩ exact hu _ _ _ h . -- Case n_ab ≠ 0: Use no_flip let k := n_ab - 1 @@ -367,8 +288,10 @@ lemma nab_pivotal_bc (a b c: α) -- b > c by unanimity . have h: ∀ i: Fin N, b ≻[mg1 i] c := by intro i; unfold mg1; split_ifs - . exact prefer_lt_01 b c a hbc (Ne.symm hab) - . exact prefer_lt_12 a b c hbc hac + . have := prefer_expand b c a .Not (Ne.symm hab) + exact ⟨ this.1, this.2.2.2.2.1 (Ne.symm hbc)⟩ + . have := prefer_expand a b c .Not hac + exact ⟨this.2.1, this.2.2.2.2.2 (Ne.symm hbc)⟩ exact hu _ _ _ h intro pp h @@ -393,28 +316,31 @@ lemma nab_pivotal_bc (a b c: α) have h_agree: AgreeOn pp mg2 b c := by unfold AgreeOn mg2; intro i split_ifs with hiltnab hieqnab - . constructor -- i < n_ab - . cases (pp i).cmp b c with - | LT _ hn=> rw[← not_iff_not]; simp [hn, (prefer_lt_01 c b a (Ne.symm hbc) (Ne.symm hac)).2] - | GT _ h => simp only [h, prefer_le_01 b c a (Ne.symm hab)] - | Indiff _ h2 => simp only [h2, prefer_top_le_10 b c a (Ne.symm hab)] - . cases (pp i).cmp b c with - | LT h _=> simp [h, (prefer_lt_01 c b a (Ne.symm hbc) (Ne.symm hac)).1] - | GT hn _ => rw[← not_iff_not]; simp [hn, (prefer_lt_01 b c a hbc (Ne.symm hab)).2] - | Indiff h1 _ => simp only [h1, prefer_top_le_01 b c a (Ne.symm hab) (Ne.symm hac)] + . -- i < n_ab + cases (pp i).cmp b c with + | LT h hn => + have := prefer_expand c b a .Not (Ne.symm hac) + simp [h, hn, this, this.2.2.2.2.1 hbc] + | GT hn h => + have := prefer_expand b c a .Not (Ne.symm hab) + simp [h, hn, this, this.2.2.2.2.1 (Ne.symm hbc)] + | Indiff h1 h2 => + have := prefer_expand b c a .Top (Ne.symm hab) + simp [h1, h2, this, this.2.2.2.2 hac] . -- i = n_ab - subst i n_ab; constructor - . simp only [h.1, prefer_le_02 b a c hbc] - . rw[← not_iff_not]; simp [h.2, (prefer_lt_02 b a c hbc).2] - . constructor -- i > n_ab - . cases (pp i).cmp b c with - | LT _ hn => rw[← not_iff_not]; simp [hn, (prefer_lt_12 a c b (Ne.symm hbc) hab).2] - | GT _ h => simp only [h, prefer_le_12 a b c hac] - | Indiff _ h2 => simp only [h2, prefer_bot_le_21 a b c hac hab] - . cases (pp i).cmp b c with - | LT h _=> simp [h, prefer_le_12 a c b hab] - | GT hn _ => rw[← not_iff_not]; simp [hn, (prefer_lt_12 a b c hbc hac).2] - | Indiff h1 _ => simp only [h1, prefer_bot_le_12 a b c hac hab] + subst i n_ab + simp [h.1, h.2, prefer_expand b a c .Not hbc] + . -- i > n_ab + cases (pp i).cmp b c with + | LT h hn => + have := prefer_expand a c b .Not hab + simp [h, hn, this, this.2.2.2.2.2 hbc] + | GT hn h => + have := prefer_expand a b c .Not hac + simp [h, hn, this, this.2.2.2.2.2 (Ne.symm hbc)] + | Indiff h1 h2 => + have := prefer_expand a b c .Bot hac + simp [h1, h2, this, this.2.2.2.2 (Ne.symm hab)] have hbac: b ≽[R mg2] a ≻ c := by constructor @@ -445,34 +371,28 @@ lemma nab_pivotal_bc (a b c: α) -- By AIIA . have h_agree_ac: AgreeOn mg2 mg1 a c := by unfold AgreeOn mg2 mg1; intro i; simp; split_ifs - . constructor - . rw[← not_iff_not] - simp [(prefer_lt_12 b c a (Ne.symm hac) (Ne.symm hab)).2] - cases (pp i).cmp b c with - | LT _ _ => simp [(prefer_lt_02 c b a (Ne.symm hac)).2] - | GT _ _ => simp [(prefer_lt_12 b c a (Ne.symm hac) (Ne.symm hab)).2] - | Indiff _ _ => simp [(prefer_top_lt_12 b c a (Ne.symm hab) (Ne.symm hac)).2] - . simp [prefer_le_12 b c a (Ne.symm hab)] - cases (pp i).cmp b c with - | LT _ _ => simp [prefer_le_02 c b a (Ne.symm hac)] - | GT _ _ => simp [prefer_le_12 b c a (Ne.symm hab)] - | Indiff _ _ => simp [prefer_top_le_12 b c a (Ne.symm hab)] - . constructor - . simp only [prefer_le_12 b a c hbc, prefer_le_02 a b c hac] - . rw[← not_iff_not] - simp [(prefer_lt_12 b a c hac hbc).2, (prefer_lt_02 a b c hac).2] - . constructor - . simp only [prefer_le_02 a b c hac] - cases (pp i).cmp b c with - | LT _ _ => simp [prefer_le_01 a c b hab] - | GT _ _ => simp [prefer_le_02 a b c hac] - | Indiff _ _ => simp [prefer_bot_le_02 a b c hac] - . rw[← not_iff_not] - simp [(prefer_lt_02 a b c hac).2] - cases (pp i).cmp b c with - | LT _ _ => simp [(prefer_lt_01 a c b hac hab).2] - | GT _ _ => simp [(prefer_lt_02 a b c hac).2] - | Indiff _ _ => simp [(prefer_bot_lt_02 a b c hac).2] + . -- i < n_ab + have := prefer_expand b c a .Not (Ne.symm hab) + simp [this, this.2.2.2.2.2 hac] + cases (pp i).cmp b c with + | LT _ _ => simp [prefer_expand c b a .Not (Ne.symm hac)] + | GT hn h => + have := prefer_expand b c a .Not (Ne.symm hab) + simp [this, this.2.2.2.2.2 hac] + | Indiff _ _ => + have := prefer_expand b c a .Top (Ne.symm hab) + simp [ this, this.2.2.2.2 hac] + . -- i = n_ab + have := prefer_expand b a c .Not hbc + simp [prefer_expand a b c .Not hac, this, this.2.2.2.2.2 (Ne.symm hac)] + . -- i > n_ab + simp [prefer_expand a b c .Not hac] + cases (pp i).cmp b c with + | LT _ _ => + have := prefer_expand a c b .Not hab + simp [this, this.2.2.2.2.1 (Ne.symm hac)] + | GT hn h => simp [prefer_expand a b c .Not hac] + | Indiff _ _ => simp [ prefer_expand a b c .Bot hac] exact (strict_aiia h_agree_ac hAIIA).mpr ((R mg1).lt_trans habc.2 habc.1) -- transitivity from b ≽ a ≻ c From 6dc035d441adac80d9a8d41168a47aeaccaa6dbd Mon Sep 17 00:00:00 2001 From: ChihChengLiang Date: Mon, 16 Mar 2026 01:08:27 +0800 Subject: [PATCH 04/20] sweep trivial lines --- Arrow/Basic.lean | 11 ++++------- 1 file changed, 4 insertions(+), 7 deletions(-) diff --git a/Arrow/Basic.lean b/Arrow/Basic.lean index b4a7549..acd000e 100644 --- a/Arrow/Basic.lean +++ b/Arrow/Basic.lean @@ -178,19 +178,16 @@ lemma prefer_expand | .Bot => mid≠top → ((¬ mid ≽[p] top) ∧ (bot ≽[p] mid)) ) := by - intro p - unfold p prefer - simp - refine ⟨?_, ?_, ?_, ?_, ?_⟩ + intro p; unfold p prefer; simp; refine ⟨?_, ?_, ?_, ?_, ?_⟩ . split <;> simp_all . split <;> try trivial intro h; exact absurd h (Ne.symm htb) . split <;> trivial . split <;> try simp_all <;> push_neg <;> exact Ne.symm htb push_neg; exact Ne.symm htb - . split <;> simp_all - . intro h; exact ⟨ Ne.symm h, Ne.symm htb⟩ ; - . intro h; exact Ne.symm h + . split <;> simp_all <;> intro h + . exact ⟨ Ne.symm h, Ne.symm htb⟩ + . exact Ne.symm h /-! ## Pivotal Voter From 73d8b03c3880547f445660faaa6ca0852283db4c Mon Sep 17 00:00:00 2001 From: ChihChengLiang Date: Mon, 16 Mar 2026 02:29:00 +0800 Subject: [PATCH 05/20] two more helper lemma, consider a win --- Arrow/Basic.lean | 90 +++++++++++++++++++++--------------------------- 1 file changed, 40 insertions(+), 50 deletions(-) diff --git a/Arrow/Basic.lean b/Arrow/Basic.lean index acd000e..ba6a3c1 100644 --- a/Arrow/Basic.lean +++ b/Arrow/Basic.lean @@ -173,9 +173,9 @@ lemma prefer_expand :let p:= prefer top mid bot tie htb (top ≽[p] mid) ∧ (mid ≽[p] bot) ∧ (top ≽[p] bot) ∧ (¬ bot ≽[p] top) ∧ (match tie with - | .Not => (mid≠top → ¬ mid ≽[p] top) ∧ (bot≠ mid → ¬ bot ≽[p] mid) - | .Top => bot≠mid → ((mid ≽[p] top) ∧ (¬ bot ≽[p] mid)) - | .Bot => mid≠top → ((¬ mid ≽[p] top) ∧ (bot ≽[p] mid)) + | .Not => (top ≠ mid → ¬ mid ≽[p] top) ∧ (mid ≠ bot → ¬ bot ≽[p] mid) + | .Top => mid ≠ bot → ((mid ≽[p] top) ∧ (¬ bot ≽[p] mid)) + | .Bot => top ≠ mid → ((¬ mid ≽[p] top) ∧ (bot ≽[p] mid)) ) := by intro p; unfold p prefer; simp; refine ⟨?_, ?_, ?_, ?_, ?_⟩ @@ -183,11 +183,21 @@ lemma prefer_expand . split <;> try trivial intro h; exact absurd h (Ne.symm htb) . split <;> trivial - . split <;> try simp_all <;> push_neg <;> exact Ne.symm htb - push_neg; exact Ne.symm htb - . split <;> simp_all <;> intro h - . exact ⟨ Ne.symm h, Ne.symm htb⟩ - . exact Ne.symm h + . split <;> try simp_all <;> exact Ne.symm htb + exact Ne.symm htb + . split <;> simp_all <;> tauto + +lemma prefer_gt_top_mid (top mid bot: α)(htb: top ≠ bot)(htm: top ≠ mid) + :let p:= prefer top mid bot .Not htb + (top ≻[p] mid) := by + have := prefer_expand top mid bot .Not htb + exact ⟨ this.1, this.2.2.2.2.1 htm⟩ + +lemma prefer_gt_mid_bot (top mid bot: α)(htb: top ≠ bot)(hmb: mid ≠ bot) + :let p:= prefer top mid bot .Not htb + (mid ≻[p] bot) := by + have := prefer_expand top mid bot .Not htb + exact ⟨ this.2.1, this.2.2.2.2.2 hmb⟩ /-! ## Pivotal Voter @@ -263,9 +273,7 @@ lemma nab_pivotal_bc (a b c: α) . by_cases hn : n_ab = 0 . -- Case n_ab = 0: All voters prefer a > b, use unanimity have h : ∀ i : Fin N, a ≻[mg1 i] b := by - intro i; simp [mg1, hn] - have := prefer_expand a b c .Not hac - exact ⟨ this.1, this.2.2.2.2.1 (Ne.symm hab)⟩ + intro i; simp [mg1, hn]; exact prefer_gt_top_mid a b c hac hab exact hu _ _ _ h . -- Case n_ab ≠ 0: Use no_flip let k := n_ab - 1 @@ -277,18 +285,15 @@ lemma nab_pivotal_bc (a b c: α) intro i; simp only [mg1, canonicalSwap] by_cases hi : i.val < n_ab.val <;> simp [hk_succ, hi] . simp [prefer_expand b c a .Not (Ne.symm hab), prefer_expand b b a .Top] - . have := prefer_expand a b c .Not hac - simp [this, prefer_expand a b b .Bot, this.2.2.2.2.1 (Ne.symm hab)] + . simp [prefer_expand a b b .Bot]; exact prefer_gt_top_mid a b c hac hab apply (strict_aiia hp hAIIA).mpr exact no_flip a b k hk -- b > c by unanimity . have h: ∀ i: Fin N, b ≻[mg1 i] c := by intro i; unfold mg1; split_ifs - . have := prefer_expand b c a .Not (Ne.symm hab) - exact ⟨ this.1, this.2.2.2.2.1 (Ne.symm hbc)⟩ - . have := prefer_expand a b c .Not hac - exact ⟨this.2.1, this.2.2.2.2.2 (Ne.symm hbc)⟩ + . exact prefer_gt_top_mid b c a (Ne.symm hab) hbc + . exact prefer_gt_mid_bot a b c hac hbc exact hu _ _ _ h intro pp h @@ -315,29 +320,21 @@ lemma nab_pivotal_bc (a b c: α) split_ifs with hiltnab hieqnab . -- i < n_ab cases (pp i).cmp b c with - | LT h hn => - have := prefer_expand c b a .Not (Ne.symm hac) - simp [h, hn, this, this.2.2.2.2.1 hbc] - | GT hn h => - have := prefer_expand b c a .Not (Ne.symm hab) - simp [h, hn, this, this.2.2.2.2.1 (Ne.symm hbc)] + | LT h hn => simp [h, hn, And.comm]; exact prefer_gt_top_mid c b a (Ne.symm hac) (Ne.symm hbc) + | GT hn h => simp [h, hn]; exact prefer_gt_top_mid b c a (Ne.symm hab) hbc | Indiff h1 h2 => have := prefer_expand b c a .Top (Ne.symm hab) - simp [h1, h2, this, this.2.2.2.2 hac] + simp [h1, h2, this, this.2.2.2.2 (Ne.symm hac)] . -- i = n_ab subst i n_ab simp [h.1, h.2, prefer_expand b a c .Not hbc] . -- i > n_ab cases (pp i).cmp b c with - | LT h hn => - have := prefer_expand a c b .Not hab - simp [h, hn, this, this.2.2.2.2.2 hbc] - | GT hn h => - have := prefer_expand a b c .Not hac - simp [h, hn, this, this.2.2.2.2.2 (Ne.symm hbc)] + | LT h hn => simp [h, hn, And.comm]; exact prefer_gt_mid_bot a c b hab (Ne.symm hbc) + | GT hn h => simp [h, hn]; exact prefer_gt_mid_bot a b c hac hbc | Indiff h1 h2 => have := prefer_expand a b c .Bot hac - simp [h1, h2, this, this.2.2.2.2 (Ne.symm hab)] + simp [h1, h2, this, this.2.2.2.2 hab] have hbac: b ≽[R mg2] a ≻ c := by constructor @@ -348,21 +345,19 @@ lemma nab_pivotal_bc (a b c: α) . have :i.val < n_ab +1 := by omega simp [hi, this, prefer_expand b b a .Top] split - . have := prefer_expand c b a .Not (Ne.symm hac) - simp [this, this.2.2.2.2.2 hab] + . exact prefer_gt_mid_bot c b a (Ne.symm hac) (Ne.symm hab) . simp [prefer_expand b c a .Not (Ne.symm hab)] . simp [prefer_expand b c a .Top (Ne.symm hab)] . by_cases hi2: i = n_ab - . have := prefer_expand b a c .Not hbc - simp [hi2, prefer_expand b b a .Top, this, this.2.2.2.2.1 hab] + . simp [hi2, prefer_expand b b a .Top] + exact prefer_gt_top_mid b a c hbc (Ne.symm hab) . have :¬ (i.val < n_ab +1 ):= by omega simp [hi, hi2, this, prefer_expand a b b .Bot] split . simp [prefer_expand a c b .Not hab] - . have := prefer_expand a b c .Not hac - simp [this, this.2.2.2.2.1 (Ne.symm hab)] + . rw [And.comm]; exact prefer_gt_top_mid a b c hac hab . have := prefer_expand a b c .Bot hac - simp [this, (this.2.2.2.2 (Ne.symm hab)).1] + simp [this, (this.2.2.2.2 hab).1] apply (hAIIA _ _ _ _ h_agree_ba).1.mpr exact flipped a b -- By AIIA @@ -370,24 +365,19 @@ lemma nab_pivotal_bc (a b c: α) unfold AgreeOn mg2 mg1; intro i; simp; split_ifs . -- i < n_ab have := prefer_expand b c a .Not (Ne.symm hab) - simp [this, this.2.2.2.2.2 hac] + simp [this, this.2.2.2.2.2 (Ne.symm hac)] cases (pp i).cmp b c with | LT _ _ => simp [prefer_expand c b a .Not (Ne.symm hac)] - | GT hn h => - have := prefer_expand b c a .Not (Ne.symm hab) - simp [this, this.2.2.2.2.2 hac] + | GT _ _ => rw[And.comm]; exact prefer_gt_mid_bot b c a (Ne.symm hab) (Ne.symm hac) | Indiff _ _ => have := prefer_expand b c a .Top (Ne.symm hab) - simp [ this, this.2.2.2.2 hac] + simp [ this, this.2.2.2.2 (Ne.symm hac)] . -- i = n_ab - have := prefer_expand b a c .Not hbc - simp [prefer_expand a b c .Not hac, this, this.2.2.2.2.2 (Ne.symm hac)] + simp [prefer_expand a b c .Not hac]; exact prefer_gt_mid_bot b a c hbc hac . -- i > n_ab simp [prefer_expand a b c .Not hac] cases (pp i).cmp b c with - | LT _ _ => - have := prefer_expand a c b .Not hab - simp [this, this.2.2.2.2.1 (Ne.symm hac)] + | LT _ _ => exact prefer_gt_top_mid a c b hab hac | GT hn h => simp [prefer_expand a b c .Not hac] | Indiff _ _ => simp [ prefer_expand a b c .Bot hac] exact (strict_aiia h_agree_ac hAIIA).mpr ((R mg1).lt_trans habc.2 habc.1) @@ -414,7 +404,7 @@ lemma nab_le_nbc (a b c: α) split_ifs with hh . simp at hh; omega . have := prefer_expand b c c .Bot hbc - exact ⟨this.1, (this.2.2.2.2 (Ne.symm hbc)).1 ⟩ + exact ⟨this.1, (this.2.2.2.2 hbc).1 ⟩ exact absurd (nab_pivotal_bc a b c hab hac hbc hu hAIIA cs h_pref) -- n_ab still dictates b over c ((Preorder'.not_lt _ _ _).mpr (flipped b c)) -- but n_bc flipped, so society should prefer c over b @@ -430,7 +420,7 @@ lemma ncb_le_nab (a b c: α) have: b ≻[cs n_ab] c := by simp [cs, canonicalSwap] have := prefer_expand b b c .Top hbc - exact ⟨ this.2.1, (this.2.2.2.2 (Ne.symm hbc)).2⟩ + exact ⟨ this.2.1, (this.2.2.2.2 hbc).2⟩ exact absurd (nab_pivotal_bc a b c hab hac hbc hu hAIIA cs this) -- n_ab prefer b over c, so is society (Preorder'.lt_asymm _ _ _ (no_flip c b n_ab h)) -- n_ab before pivoter, so b c shouldn't flip From fe20f278e8688f6e60f772337ab56ca511fe9f7a Mon Sep 17 00:00:00 2001 From: ChihChengLiang Date: Mon, 16 Mar 2026 02:40:30 +0800 Subject: [PATCH 06/20] writing in weak pref allows simp --- Arrow/Basic.lean | 33 ++++++++++++++++----------------- 1 file changed, 16 insertions(+), 17 deletions(-) diff --git a/Arrow/Basic.lean b/Arrow/Basic.lean index ba6a3c1..73792b2 100644 --- a/Arrow/Basic.lean +++ b/Arrow/Basic.lean @@ -187,15 +187,16 @@ lemma prefer_expand exact Ne.symm htb . split <;> simp_all <;> tauto +/-- Writing in weak preference form allows simplification -/ lemma prefer_gt_top_mid (top mid bot: α)(htb: top ≠ bot)(htm: top ≠ mid) :let p:= prefer top mid bot .Not htb - (top ≻[p] mid) := by + (top ≽[p] mid) ∧ ¬ mid ≽[p] top := by have := prefer_expand top mid bot .Not htb exact ⟨ this.1, this.2.2.2.2.1 htm⟩ lemma prefer_gt_mid_bot (top mid bot: α)(htb: top ≠ bot)(hmb: mid ≠ bot) :let p:= prefer top mid bot .Not htb - (mid ≻[p] bot) := by + (mid ≽[p] bot) ∧ ¬ bot ≽[p] mid:= by have := prefer_expand top mid bot .Not htb exact ⟨ this.2.1, this.2.2.2.2.2 hmb⟩ @@ -285,7 +286,7 @@ lemma nab_pivotal_bc (a b c: α) intro i; simp only [mg1, canonicalSwap] by_cases hi : i.val < n_ab.val <;> simp [hk_succ, hi] . simp [prefer_expand b c a .Not (Ne.symm hab), prefer_expand b b a .Top] - . simp [prefer_expand a b b .Bot]; exact prefer_gt_top_mid a b c hac hab + . simp [prefer_expand a b b .Bot, prefer_gt_top_mid a b c hac hab] apply (strict_aiia hp hAIIA).mpr exact no_flip a b k hk @@ -320,8 +321,8 @@ lemma nab_pivotal_bc (a b c: α) split_ifs with hiltnab hieqnab . -- i < n_ab cases (pp i).cmp b c with - | LT h hn => simp [h, hn, And.comm]; exact prefer_gt_top_mid c b a (Ne.symm hac) (Ne.symm hbc) - | GT hn h => simp [h, hn]; exact prefer_gt_top_mid b c a (Ne.symm hab) hbc + | LT h hn => simp [h, hn, prefer_gt_top_mid c b a (Ne.symm hac) (Ne.symm hbc)] + | GT hn h => simp [h, hn, prefer_gt_top_mid b c a (Ne.symm hab) hbc] | Indiff h1 h2 => have := prefer_expand b c a .Top (Ne.symm hab) simp [h1, h2, this, this.2.2.2.2 (Ne.symm hac)] @@ -330,8 +331,8 @@ lemma nab_pivotal_bc (a b c: α) simp [h.1, h.2, prefer_expand b a c .Not hbc] . -- i > n_ab cases (pp i).cmp b c with - | LT h hn => simp [h, hn, And.comm]; exact prefer_gt_mid_bot a c b hab (Ne.symm hbc) - | GT hn h => simp [h, hn]; exact prefer_gt_mid_bot a b c hac hbc + | LT h hn => simp [h, hn, prefer_gt_mid_bot a c b hab (Ne.symm hbc)] + | GT hn h => simp [h, hn, prefer_gt_mid_bot a b c hac hbc] | Indiff h1 h2 => have := prefer_expand a b c .Bot hac simp [h1, h2, this, this.2.2.2.2 hab] @@ -345,17 +346,16 @@ lemma nab_pivotal_bc (a b c: α) . have :i.val < n_ab +1 := by omega simp [hi, this, prefer_expand b b a .Top] split - . exact prefer_gt_mid_bot c b a (Ne.symm hac) (Ne.symm hab) + . simp [prefer_gt_mid_bot c b a (Ne.symm hac) (Ne.symm hab)] . simp [prefer_expand b c a .Not (Ne.symm hab)] . simp [prefer_expand b c a .Top (Ne.symm hab)] . by_cases hi2: i = n_ab - . simp [hi2, prefer_expand b b a .Top] - exact prefer_gt_top_mid b a c hbc (Ne.symm hab) + . simp [hi2, prefer_expand b b a .Top, prefer_gt_top_mid b a c hbc (Ne.symm hab)] . have :¬ (i.val < n_ab +1 ):= by omega simp [hi, hi2, this, prefer_expand a b b .Bot] split . simp [prefer_expand a c b .Not hab] - . rw [And.comm]; exact prefer_gt_top_mid a b c hac hab + . simp [prefer_gt_top_mid a b c hac hab] . have := prefer_expand a b c .Bot hac simp [this, (this.2.2.2.2 hab).1] apply (hAIIA _ _ _ _ h_agree_ba).1.mpr @@ -364,21 +364,20 @@ lemma nab_pivotal_bc (a b c: α) . have h_agree_ac: AgreeOn mg2 mg1 a c := by unfold AgreeOn mg2 mg1; intro i; simp; split_ifs . -- i < n_ab - have := prefer_expand b c a .Not (Ne.symm hab) - simp [this, this.2.2.2.2.2 (Ne.symm hac)] + simp [prefer_gt_mid_bot b c a (Ne.symm hab) (Ne.symm hac)] cases (pp i).cmp b c with | LT _ _ => simp [prefer_expand c b a .Not (Ne.symm hac)] - | GT _ _ => rw[And.comm]; exact prefer_gt_mid_bot b c a (Ne.symm hab) (Ne.symm hac) + | GT _ _ => simp [prefer_gt_mid_bot b c a (Ne.symm hab) (Ne.symm hac)] | Indiff _ _ => have := prefer_expand b c a .Top (Ne.symm hab) simp [ this, this.2.2.2.2 (Ne.symm hac)] . -- i = n_ab - simp [prefer_expand a b c .Not hac]; exact prefer_gt_mid_bot b a c hbc hac + simp [prefer_expand a b c .Not hac, prefer_gt_mid_bot b a c hbc hac] . -- i > n_ab simp [prefer_expand a b c .Not hac] cases (pp i).cmp b c with - | LT _ _ => exact prefer_gt_top_mid a c b hab hac - | GT hn h => simp [prefer_expand a b c .Not hac] + | LT _ _ => simp [prefer_gt_top_mid a c b hab hac] + | GT _ _ => simp [prefer_expand a b c .Not hac] | Indiff _ _ => simp [ prefer_expand a b c .Bot hac] exact (strict_aiia h_agree_ac hAIIA).mpr ((R mg1).lt_trans habc.2 habc.1) From 6c571d5c3ae9671205c6cc014c6fc2ef3b4d1986 Mon Sep 17 00:00:00 2001 From: ChihChengLiang Date: Mon, 16 Mar 2026 02:53:51 +0800 Subject: [PATCH 07/20] nitpick --- Arrow/Basic.lean | 7 ++----- 1 file changed, 2 insertions(+), 5 deletions(-) diff --git a/Arrow/Basic.lean b/Arrow/Basic.lean index 73792b2..5080bbe 100644 --- a/Arrow/Basic.lean +++ b/Arrow/Basic.lean @@ -383,12 +383,9 @@ lemma nab_pivotal_bc (a b c: α) -- transitivity from b ≽ a ≻ c have hRmg2bc : b ≻[R mg2] c := by - simp [Preorder'.lt] - constructor + simp [Preorder'.lt]; constructor . exact (R mg2).trans c a b hbac.2.1 hbac.1 - . intro h - have := (R mg2).trans a b c hbac.1 h - exact absurd this hbac.2.2 + . intro h; exact absurd ((R mg2).trans a b c hbac.1 h) hbac.2.2 exact (strict_aiia h_agree hAIIA).mpr hRmg2bc /-- The pivotal voter for `(a, b)` comes no later than the one for `(b, c)`. -/ From 23375c7f544a22161c2af3c905a7946d8cd60779 Mon Sep 17 00:00:00 2001 From: ChihChengLiang Date: Mon, 16 Mar 2026 03:20:29 +0800 Subject: [PATCH 08/20] fixed crazy 2.2.2.2 with obtain --- Arrow/Basic.lean | 34 +++++++++++++++------------------- 1 file changed, 15 insertions(+), 19 deletions(-) diff --git a/Arrow/Basic.lean b/Arrow/Basic.lean index 5080bbe..e758505 100644 --- a/Arrow/Basic.lean +++ b/Arrow/Basic.lean @@ -191,14 +191,14 @@ lemma prefer_expand lemma prefer_gt_top_mid (top mid bot: α)(htb: top ≠ bot)(htm: top ≠ mid) :let p:= prefer top mid bot .Not htb (top ≽[p] mid) ∧ ¬ mid ≽[p] top := by - have := prefer_expand top mid bot .Not htb - exact ⟨ this.1, this.2.2.2.2.1 htm⟩ + obtain ⟨h, _, _, _, hn⟩ := prefer_expand top mid bot .Not htb + exact ⟨ h, hn.1 htm⟩ lemma prefer_gt_mid_bot (top mid bot: α)(htb: top ≠ bot)(hmb: mid ≠ bot) :let p:= prefer top mid bot .Not htb (mid ≽[p] bot) ∧ ¬ bot ≽[p] mid:= by - have := prefer_expand top mid bot .Not htb - exact ⟨ this.2.1, this.2.2.2.2.2 hmb⟩ + obtain ⟨_, h, _, _, hn⟩ := prefer_expand top mid bot .Not htb + exact ⟨ h, hn.2 hmb⟩ /-! ## Pivotal Voter @@ -229,9 +229,7 @@ lemma flip_exists (R : SWF α N) (a b : α) (hab : a ≠ b) (hu : Unanimity R): have: 0 < N := Nat.pos_of_ne_zero (NeZero.ne N) simp [Nat.sub_add_cancel this] have: b ≻[R (fun i => prefer b b a .Top (Ne.symm hab) )] a := by - apply hu; intro i; - have := prefer_expand b b a .Top (Ne.symm hab) - exact ⟨this.2.1, this.2.2.2.1⟩ + apply hu; intro i; simp [Preorder'.lt, prefer_expand b b a .Top (Ne.symm hab)] exact this.1 /-- The pivotal voter for `(a, b)`: the minimum `k` where society flips from `a ≻ b` to `b ≻ a`. -/ @@ -324,8 +322,8 @@ lemma nab_pivotal_bc (a b c: α) | LT h hn => simp [h, hn, prefer_gt_top_mid c b a (Ne.symm hac) (Ne.symm hbc)] | GT hn h => simp [h, hn, prefer_gt_top_mid b c a (Ne.symm hab) hbc] | Indiff h1 h2 => - have := prefer_expand b c a .Top (Ne.symm hab) - simp [h1, h2, this, this.2.2.2.2 (Ne.symm hac)] + obtain ⟨h, _, _, _, hn⟩ := prefer_expand b c a .Top (Ne.symm hab) + simp [h1, h2, h, hn (Ne.symm hac)] . -- i = n_ab subst i n_ab simp [h.1, h.2, prefer_expand b a c .Not hbc] @@ -334,8 +332,8 @@ lemma nab_pivotal_bc (a b c: α) | LT h hn => simp [h, hn, prefer_gt_mid_bot a c b hab (Ne.symm hbc)] | GT hn h => simp [h, hn, prefer_gt_mid_bot a b c hac hbc] | Indiff h1 h2 => - have := prefer_expand a b c .Bot hac - simp [h1, h2, this, this.2.2.2.2 hab] + obtain ⟨_, h, _, _, hn⟩ := prefer_expand a b c .Bot hac + simp [h1, h2, h, hn hab] have hbac: b ≽[R mg2] a ≻ c := by constructor @@ -356,8 +354,7 @@ lemma nab_pivotal_bc (a b c: α) split . simp [prefer_expand a c b .Not hab] . simp [prefer_gt_top_mid a b c hac hab] - . have := prefer_expand a b c .Bot hac - simp [this, (this.2.2.2.2 hab).1] + . obtain ⟨h, _, _, _, hn ⟩ := prefer_expand a b c .Bot hac; simp [h, hn hab] apply (hAIIA _ _ _ _ h_agree_ba).1.mpr exact flipped a b -- By AIIA @@ -369,8 +366,8 @@ lemma nab_pivotal_bc (a b c: α) | LT _ _ => simp [prefer_expand c b a .Not (Ne.symm hac)] | GT _ _ => simp [prefer_gt_mid_bot b c a (Ne.symm hab) (Ne.symm hac)] | Indiff _ _ => - have := prefer_expand b c a .Top (Ne.symm hab) - simp [ this, this.2.2.2.2 (Ne.symm hac)] + obtain ⟨_, h, _, _, hn ⟩ := prefer_expand b c a .Top (Ne.symm hab) + simp [ h, hn (Ne.symm hac)] . -- i = n_ab simp [prefer_expand a b c .Not hac, prefer_gt_mid_bot b a c hbc hac] . -- i > n_ab @@ -399,8 +396,7 @@ lemma nab_le_nbc (a b c: α) simp only [cs, canonicalSwap] split_ifs with hh . simp at hh; omega - . have := prefer_expand b c c .Bot hbc - exact ⟨this.1, (this.2.2.2.2 hbc).1 ⟩ + . obtain ⟨h, _, _, _, hn⟩ := prefer_expand b c c .Bot hbc; exact ⟨h, (hn hbc).1⟩ exact absurd (nab_pivotal_bc a b c hab hac hbc hu hAIIA cs h_pref) -- n_ab still dictates b over c ((Preorder'.not_lt _ _ _).mpr (flipped b c)) -- but n_bc flipped, so society should prefer c over b @@ -415,8 +411,8 @@ lemma ncb_le_nab (a b c: α) let cs := canonicalSwap c b (Ne.symm hbc) n_ab.succ have: b ≻[cs n_ab] c := by simp [cs, canonicalSwap] - have := prefer_expand b b c .Top hbc - exact ⟨ this.2.1, (this.2.2.2.2 hbc).2⟩ + obtain ⟨_, h, _, _, hn⟩ := prefer_expand b b c .Top hbc + exact ⟨ h, (hn hbc).2⟩ exact absurd (nab_pivotal_bc a b c hab hac hbc hu hAIIA cs this) -- n_ab prefer b over c, so is society (Preorder'.lt_asymm _ _ _ (no_flip c b n_ab h)) -- n_ab before pivoter, so b c shouldn't flip From c24781736e0e94a5ec4defbff3ed6a6c17f3f3c6 Mon Sep 17 00:00:00 2001 From: ChihChengLiang Date: Mon, 16 Mar 2026 03:24:56 +0800 Subject: [PATCH 09/20] rm repetitive docs --- Arrow/Basic.lean | 10 ++-------- 1 file changed, 2 insertions(+), 8 deletions(-) diff --git a/Arrow/Basic.lean b/Arrow/Basic.lean index e758505..bcb7da9 100644 --- a/Arrow/Basic.lean +++ b/Arrow/Basic.lean @@ -117,18 +117,12 @@ def NonDictatorship (R : SWF α N): Prop := /-! ## Preference Construction We construct concrete preference orderings to build test profiles for the proof. -Given three alternatives, `prefer a₀ a₁ a₂ tie` ranks them with optional ties: -- `Tie.Not`: a₀ > a₁ > a₂ -- `Tie.Top`: a₀ ~ a₁ > a₂ -- `Tie.Bot`: a₀ > a₁ ~ a₂ +Given three alternatives, `prefer a₀ a₁ a₂ tie` ranks them with optional ties. -/ variable [LinearOrder α] /-- Where ties occur in a 3-element preference ranking -/ -inductive Tie - | Not -- No ties: a₀ > a₁ > a₂ - | Top -- Top two tied: a₀ ~ a₁ > a₂ - | Bot -- Bottom two tied: a₀ > a₁ ~ a₂ +inductive Tie | Not | Top | Bot /-- Construct a preference ordering with optional ties: - `Tie.Not`: a₀ > a₁ > a₂ (strict ranking) From 4993880726053ad7db610e2833b50c1fbfcae947 Mon Sep 17 00:00:00 2001 From: ChihChengLiang Date: Mon, 16 Mar 2026 03:32:38 +0800 Subject: [PATCH 10/20] reduce noise with split --- Arrow/Basic.lean | 17 ++++++++--------- 1 file changed, 8 insertions(+), 9 deletions(-) diff --git a/Arrow/Basic.lean b/Arrow/Basic.lean index bcb7da9..d91bed7 100644 --- a/Arrow/Basic.lean +++ b/Arrow/Basic.lean @@ -356,20 +356,19 @@ lemma nab_pivotal_bc (a b c: α) unfold AgreeOn mg2 mg1; intro i; simp; split_ifs . -- i < n_ab simp [prefer_gt_mid_bot b c a (Ne.symm hab) (Ne.symm hac)] - cases (pp i).cmp b c with - | LT _ _ => simp [prefer_expand c b a .Not (Ne.symm hac)] - | GT _ _ => simp [prefer_gt_mid_bot b c a (Ne.symm hab) (Ne.symm hac)] - | Indiff _ _ => - obtain ⟨_, h, _, _, hn ⟩ := prefer_expand b c a .Top (Ne.symm hab) + split + . simp [prefer_expand c b a .Not (Ne.symm hac)] + . simp [prefer_gt_mid_bot b c a (Ne.symm hab) (Ne.symm hac)] + . obtain ⟨_, h, _, _, hn ⟩ := prefer_expand b c a .Top (Ne.symm hab) simp [ h, hn (Ne.symm hac)] . -- i = n_ab simp [prefer_expand a b c .Not hac, prefer_gt_mid_bot b a c hbc hac] . -- i > n_ab simp [prefer_expand a b c .Not hac] - cases (pp i).cmp b c with - | LT _ _ => simp [prefer_gt_top_mid a c b hab hac] - | GT _ _ => simp [prefer_expand a b c .Not hac] - | Indiff _ _ => simp [ prefer_expand a b c .Bot hac] + split + . simp [prefer_gt_top_mid a c b hab hac] + . simp [prefer_expand a b c .Not hac] + . simp [prefer_expand a b c .Bot hac] exact (strict_aiia h_agree_ac hAIIA).mpr ((R mg1).lt_trans habc.2 habc.1) -- transitivity from b ≽ a ≻ c From 59620f5515a1dad9668672553555da27092c07f8 Mon Sep 17 00:00:00 2001 From: ChihChengLiang Date: Mon, 16 Mar 2026 03:35:15 +0800 Subject: [PATCH 11/20] unused variable --- Arrow/Basic.lean | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/Arrow/Basic.lean b/Arrow/Basic.lean index d91bed7..4a7a7ed 100644 --- a/Arrow/Basic.lean +++ b/Arrow/Basic.lean @@ -309,8 +309,7 @@ lemma nab_pivotal_bc (a b c: α) | .Indiff _ _ => prefer a b c .Bot hac -- a > b ~ c have h_agree: AgreeOn pp mg2 b c := by - unfold AgreeOn mg2; intro i - split_ifs with hiltnab hieqnab + unfold AgreeOn mg2; intro i; split_ifs . -- i < n_ab cases (pp i).cmp b c with | LT h hn => simp [h, hn, prefer_gt_top_mid c b a (Ne.symm hac) (Ne.symm hbc)] From 7f8560b1d63fbe8936babc5529916f7c3c7ed47a Mon Sep 17 00:00:00 2001 From: ChihChengLiang Date: Mon, 16 Mar 2026 03:37:56 +0800 Subject: [PATCH 12/20] rename h_pp_bc --- Arrow/Basic.lean | 5 ++--- 1 file changed, 2 insertions(+), 3 deletions(-) diff --git a/Arrow/Basic.lean b/Arrow/Basic.lean index 4a7a7ed..f25d65f 100644 --- a/Arrow/Basic.lean +++ b/Arrow/Basic.lean @@ -288,7 +288,7 @@ lemma nab_pivotal_bc (a b c: α) . exact prefer_gt_top_mid b c a (Ne.symm hab) hbc . exact prefer_gt_mid_bot a b c hac hbc exact hu _ _ _ h - intro pp h + intro pp h_pp_bc -- Magic profile 2: match arbitrary profile `pp` on (b,c) -- For i < n_ab: (b ~ c) > a, or b > c > a, or c > b > a (matching pp) @@ -318,8 +318,7 @@ lemma nab_pivotal_bc (a b c: α) obtain ⟨h, _, _, _, hn⟩ := prefer_expand b c a .Top (Ne.symm hab) simp [h1, h2, h, hn (Ne.symm hac)] . -- i = n_ab - subst i n_ab - simp [h.1, h.2, prefer_expand b a c .Not hbc] + subst i n_ab; simp [h_pp_bc.1, h_pp_bc.2, prefer_expand b a c .Not hbc] . -- i > n_ab cases (pp i).cmp b c with | LT h hn => simp [h, hn, prefer_gt_mid_bot a c b hab (Ne.symm hbc)] From dfe6a730eee0bd875ec45cf6f0b22c3cbf07d619 Mon Sep 17 00:00:00 2001 From: ChihChengLiang Date: Mon, 16 Mar 2026 03:39:45 +0800 Subject: [PATCH 13/20] visual adjustment --- Arrow/Basic.lean | 20 ++++++++++---------- 1 file changed, 10 insertions(+), 10 deletions(-) diff --git a/Arrow/Basic.lean b/Arrow/Basic.lean index f25d65f..0667544 100644 --- a/Arrow/Basic.lean +++ b/Arrow/Basic.lean @@ -25,7 +25,6 @@ lemma Preorder'.lt_asymm (p : Preorder' α) (a b : α) : intro ⟨hab, hnba⟩ ⟨hba, _⟩ exact hnba hba -@[simp] lemma Preorder'.not_lt {α : Type} (p : Preorder' α) (a b : α) : ¬ p.lt a b ↔ p.le b a := by unfold Preorder'.lt @@ -166,10 +165,11 @@ lemma prefer_expand (top mid bot: α)(tie: Tie)(htb: top ≠ bot) :let p:= prefer top mid bot tie htb (top ≽[p] mid) ∧ (mid ≽[p] bot) ∧ (top ≽[p] bot) ∧ (¬ bot ≽[p] top) ∧ - (match tie with - | .Not => (top ≠ mid → ¬ mid ≽[p] top) ∧ (mid ≠ bot → ¬ bot ≽[p] mid) - | .Top => mid ≠ bot → ((mid ≽[p] top) ∧ (¬ bot ≽[p] mid)) - | .Bot => top ≠ mid → ((¬ mid ≽[p] top) ∧ (bot ≽[p] mid)) + ( + match tie with + | .Not => (top ≠ mid → ¬ mid ≽[p] top) ∧ (mid ≠ bot → ¬ bot ≽[p] mid) + | .Top => mid ≠ bot → ((mid ≽[p] top) ∧ ¬ bot ≽[p] mid) + | .Bot => top ≠ mid → ((¬ mid ≽[p] top) ∧ bot ≽[p] mid) ) := by intro p; unfold p prefer; simp; refine ⟨?_, ?_, ?_, ?_, ?_⟩ @@ -224,7 +224,7 @@ lemma flip_exists (R : SWF α N) (a b : α) (hab : a ≠ b) (hu : Unanimity R): simp [Nat.sub_add_cancel this] have: b ≻[R (fun i => prefer b b a .Top (Ne.symm hab) )] a := by apply hu; intro i; simp [Preorder'.lt, prefer_expand b b a .Top (Ne.symm hab)] - exact this.1 + exact Preorder'.lt_asymm _ _ _ this /-- The pivotal voter for `(a, b)`: the minimum `k` where society flips from `a ≻ b` to `b ≻ a`. -/ noncomputable def pivoter (a b : α) (hab : a ≠ b) (hu : Unanimity R) : Fin N := @@ -298,14 +298,14 @@ lemma nab_pivotal_bc (a b c: α) let mg2 : Profile α N := fun i: Fin N => if i < n_ab then match (pp i).cmp b c with - | .LT _ _ => prefer c b a .Not (Ne.symm hac) - | .GT _ _ => prefer b c a .Not (Ne.symm hab) + | .LT _ _ => prefer c b a .Not (Ne.symm hac) + | .GT _ _ => prefer b c a .Not (Ne.symm hab) | .Indiff _ _ => prefer b c a .Top (Ne.symm hab) -- b ~ c > a else if i = n_ab then prefer b a c .Not hbc else match (pp i).cmp b c with - | .LT _ _ => prefer a c b .Not hab - | .GT _ _ => prefer a b c .Not hac + | .LT _ _ => prefer a c b .Not hab + | .GT _ _ => prefer a b c .Not hac | .Indiff _ _ => prefer a b c .Bot hac -- a > b ~ c have h_agree: AgreeOn pp mg2 b c := by From 1fe5f2289a809894a4be1bf8349654f39660083a Mon Sep 17 00:00:00 2001 From: ChihChengLiang Date: Mon, 16 Mar 2026 04:20:49 +0800 Subject: [PATCH 14/20] reduce Ne.symm noise --- Arrow/Basic.lean | 46 ++++++++++++++++++++++------------------------ 1 file changed, 22 insertions(+), 24 deletions(-) diff --git a/Arrow/Basic.lean b/Arrow/Basic.lean index 0667544..e707306 100644 --- a/Arrow/Basic.lean +++ b/Arrow/Basic.lean @@ -248,6 +248,9 @@ lemma nab_pivotal_bc (a b c: α) (hu: Unanimity R) (hAIIA: AIIA R) : Dictates R (pivoter a b hab hu) b c := by let n_ab := pivoter a b hab hu + 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 @@ -255,7 +258,7 @@ lemma nab_pivotal_bc (a b c: α) -- result: socPrefer a > b > c let mg1: Profile α N := fun i: Fin N => if i < n_ab.val - then prefer b c a .Not (Ne.symm hab) + then prefer b c a .Not hba else prefer a b c .Not hac -- soc prefer a > b > c have habc: a ≻[R mg1] b ≻ c := by @@ -277,7 +280,7 @@ lemma nab_pivotal_bc (a b c: α) have hp : AgreeOn mg1 (canonicalSwap a b hab k.succ) a b := by intro i; simp only [mg1, canonicalSwap] by_cases hi : i.val < n_ab.val <;> simp [hk_succ, hi] - . simp [prefer_expand b c a .Not (Ne.symm hab), prefer_expand b b a .Top] + . simp [prefer_expand b c a .Not hba, prefer_expand b b a .Top] . simp [prefer_expand a b b .Bot, prefer_gt_top_mid a b c hac hab] apply (strict_aiia hp hAIIA).mpr @@ -285,7 +288,7 @@ lemma nab_pivotal_bc (a b c: α) -- b > c by unanimity . have h: ∀ i: Fin N, b ≻[mg1 i] c := by intro i; unfold mg1; split_ifs - . exact prefer_gt_top_mid b c a (Ne.symm hab) hbc + . exact prefer_gt_top_mid b c a hba hbc . exact prefer_gt_mid_bot a b c hac hbc exact hu _ _ _ h intro pp h_pp_bc @@ -298,9 +301,9 @@ lemma nab_pivotal_bc (a b c: α) let mg2 : Profile α N := fun i: Fin N => if i < n_ab then match (pp i).cmp b c with - | .LT _ _ => prefer c b a .Not (Ne.symm hac) - | .GT _ _ => prefer b c a .Not (Ne.symm hab) - | .Indiff _ _ => prefer b c a .Top (Ne.symm hab) -- b ~ c > a + | .LT _ _ => prefer c b a .Not hca + | .GT _ _ => prefer b c a .Not hba + | .Indiff _ _ => prefer b c a .Top hba -- b ~ c > a else if i = n_ab then prefer b a c .Not hbc else match (pp i).cmp b c with @@ -312,20 +315,16 @@ lemma nab_pivotal_bc (a b c: α) unfold AgreeOn mg2; intro i; split_ifs . -- i < n_ab cases (pp i).cmp b c with - | LT h hn => simp [h, hn, prefer_gt_top_mid c b a (Ne.symm hac) (Ne.symm hbc)] - | GT hn h => simp [h, hn, prefer_gt_top_mid b c a (Ne.symm hab) hbc] - | Indiff h1 h2 => - obtain ⟨h, _, _, _, hn⟩ := prefer_expand b c a .Top (Ne.symm hab) - simp [h1, h2, h, hn (Ne.symm hac)] + | LT h hn => simp [h, hn, prefer_gt_top_mid c b a hca hcb] + | GT hn h => simp [h, hn, prefer_gt_top_mid b c a hba hbc] + | Indiff h1 h2 => obtain ⟨h, _, _, _, hn⟩ := prefer_expand b c a .Top hba; simp [h1, h2, h, hn hca] . -- i = n_ab subst i n_ab; simp [h_pp_bc.1, h_pp_bc.2, prefer_expand b a c .Not hbc] . -- i > n_ab cases (pp i).cmp b c with - | LT h hn => simp [h, hn, prefer_gt_mid_bot a c b hab (Ne.symm hbc)] + | LT h hn => simp [h, hn, prefer_gt_mid_bot a c b hab hcb] | GT hn h => simp [h, hn, prefer_gt_mid_bot a b c hac hbc] - | Indiff h1 h2 => - obtain ⟨_, h, _, _, hn⟩ := prefer_expand a b c .Bot hac - simp [h1, h2, h, hn hab] + | Indiff h1 h2 => obtain ⟨_, h, _, _, hn⟩ := prefer_expand a b c .Bot hac; simp [h1, h2, h, hn hab] have hbac: b ≽[R mg2] a ≻ c := by constructor @@ -336,11 +335,11 @@ lemma nab_pivotal_bc (a b c: α) . have :i.val < n_ab +1 := by omega simp [hi, this, prefer_expand b b a .Top] split - . simp [prefer_gt_mid_bot c b a (Ne.symm hac) (Ne.symm hab)] - . simp [prefer_expand b c a .Not (Ne.symm hab)] - . simp [prefer_expand b c a .Top (Ne.symm hab)] + . simp [prefer_gt_mid_bot c b a hca hba] + . simp [prefer_expand b c a .Not hba] + . simp [prefer_expand b c a .Top hba] . by_cases hi2: i = n_ab - . simp [hi2, prefer_expand b b a .Top, prefer_gt_top_mid b a c hbc (Ne.symm hab)] + . simp [hi2, prefer_expand b b a .Top, prefer_gt_top_mid b a c hbc hba] . have :¬ (i.val < n_ab +1 ):= by omega simp [hi, hi2, this, prefer_expand a b b .Bot] split @@ -353,12 +352,11 @@ lemma nab_pivotal_bc (a b c: α) . have h_agree_ac: AgreeOn mg2 mg1 a c := by unfold AgreeOn mg2 mg1; intro i; simp; split_ifs . -- i < n_ab - simp [prefer_gt_mid_bot b c a (Ne.symm hab) (Ne.symm hac)] + simp [prefer_gt_mid_bot b c a hba hca] split - . simp [prefer_expand c b a .Not (Ne.symm hac)] - . simp [prefer_gt_mid_bot b c a (Ne.symm hab) (Ne.symm hac)] - . obtain ⟨_, h, _, _, hn ⟩ := prefer_expand b c a .Top (Ne.symm hab) - simp [ h, hn (Ne.symm hac)] + . simp [prefer_expand c b a .Not hca] + . simp [prefer_gt_mid_bot b c a hba hca] + . obtain ⟨_, h, _, _, hn ⟩ := prefer_expand b c a .Top hba; simp [ h, hn hca] . -- i = n_ab simp [prefer_expand a b c .Not hac, prefer_gt_mid_bot b a c hbc hac] . -- i > n_ab From c68f577b3b9a9164a738dd717eaf2b5ce1fc372e Mon Sep 17 00:00:00 2001 From: ChihChengLiang Date: Mon, 16 Mar 2026 04:27:18 +0800 Subject: [PATCH 15/20] visual 2 --- Arrow/Basic.lean | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/Arrow/Basic.lean b/Arrow/Basic.lean index e707306..b7982fe 100644 --- a/Arrow/Basic.lean +++ b/Arrow/Basic.lean @@ -301,14 +301,14 @@ lemma nab_pivotal_bc (a b c: α) let mg2 : Profile α N := fun i: Fin N => if i < n_ab then match (pp i).cmp b c with - | .LT _ _ => prefer c b a .Not hca - | .GT _ _ => prefer b c a .Not hba + | .LT _ _ => prefer c b a .Not hca + | .GT _ _ => prefer b c a .Not hba | .Indiff _ _ => prefer b c a .Top hba -- b ~ c > a else if i = n_ab then prefer b a c .Not hbc else match (pp i).cmp b c with - | .LT _ _ => prefer a c b .Not hab - | .GT _ _ => prefer a b c .Not hac + | .LT _ _ => prefer a c b .Not hab + | .GT _ _ => prefer a b c .Not hac | .Indiff _ _ => prefer a b c .Bot hac -- a > b ~ c have h_agree: AgreeOn pp mg2 b c := by From 41f056729cdd3b963433c5ec7303d858e196eb64 Mon Sep 17 00:00:00 2001 From: ChihChengLiang Date: Mon, 16 Mar 2026 04:34:05 +0800 Subject: [PATCH 16/20] more compression --- Arrow/Basic.lean | 14 ++++---------- 1 file changed, 4 insertions(+), 10 deletions(-) diff --git a/Arrow/Basic.lean b/Arrow/Basic.lean index b7982fe..1ba4e3e 100644 --- a/Arrow/Basic.lean +++ b/Arrow/Basic.lean @@ -21,9 +21,7 @@ def Preorder'.lt (p : Preorder' α) (a b : α) : Prop := p.le a b ∧ ¬p.le b a lemma Preorder'.lt_asymm (p : Preorder' α) (a b : α) : - p.lt a b → ¬ p.lt b a := by - intro ⟨hab, hnba⟩ ⟨hba, _⟩ - exact hnba hba + p.lt a b → ¬ p.lt b a := by intro ⟨_, hnba⟩ ⟨hba, _⟩; exact hnba hba lemma Preorder'.not_lt {α : Type} (p : Preorder' α) (a b : α) : ¬ p.lt a b ↔ p.le b a := by @@ -39,8 +37,7 @@ lemma Preorder'.lt_trans (p : Preorder' α) {a b c : α} (h1 : p.lt a b) (h2 : p.lt b c) : p.lt a c := by constructor . exact p.trans _ _ _ h1.1 h2.1 - . intro h - exact h1.2 (p.trans _ _ _ h2.1 h) + . intro h; exact h1.2 (p.trans _ _ _ h2.1 h) /-- The three possible outcomes when comparing two elements under a total preorder. -/ inductive Cmp (p : Preorder' α) (a b : α) : Type @@ -103,11 +100,8 @@ def AIIA (R : SWF α N) : Prop := 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 - have := hAIIA _ _ _ _ hagree - simp [Preorder'.lt, this.1, this.2] + {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 := From cfab0e6f328abd3fa4f09612d54c9f84ef57fb89 Mon Sep 17 00:00:00 2001 From: ChihChengLiang Date: Mon, 16 Mar 2026 04:38:37 +0800 Subject: [PATCH 17/20] dot style --- Arrow/Basic.lean | 16 ++++++++-------- 1 file changed, 8 insertions(+), 8 deletions(-) diff --git a/Arrow/Basic.lean b/Arrow/Basic.lean index 1ba4e3e..44e4a02 100644 --- a/Arrow/Basic.lean +++ b/Arrow/Basic.lean @@ -142,18 +142,18 @@ def prefer (a₀ _a₁ a₂ : α) (tie : Tie) (h02 : a₀ ≠ a₂) : Preorder' trans := by intro a b c ha hb cases tie <;> simp only at ha hb ⊢ - · split_ifs with haa2 hca0 haa0 hca2 <;> simp_all + . split_ifs with haa2 hca0 haa0 hca2 <;> simp_all by_cases hba0: b = a₀ - · simp_all - · simp_all; exact le_trans ha.2 hb - · split_ifs at ha hb ⊢; exact ha - · split_ifs at ha hb ⊢; exact hb + . simp_all + . simp_all; exact le_trans ha.2 hb + . split_ifs at ha hb ⊢; exact ha + . split_ifs at ha hb ⊢; exact hb total := by intro a b cases tie - · split_ifs <;> simp_all [le_total a b] - · simp only; by_cases hxa : a = a₂ <;> by_cases hya : b = a₂ <;> simp_all - · simp only; by_cases hxa : a = a₀ <;> by_cases hya : b = a₀ <;> simp_all + . split_ifs <;> simp_all [le_total a b] + . simp only; by_cases hxa : a = a₂ <;> by_cases hya : b = a₂ <;> simp_all + . simp only; by_cases hxa : a = a₀ <;> by_cases hya : b = a₀ <;> simp_all lemma prefer_expand (top mid bot: α)(tie: Tie)(htb: top ≠ bot) From 655652808e1a1ea7563b87b2848400680c9a1dee Mon Sep 17 00:00:00 2001 From: ChihChengLiang Date: Mon, 16 Mar 2026 04:56:45 +0800 Subject: [PATCH 18/20] ranking of two can be handled gracely --- Arrow/Basic.lean | 25 +++++++++++-------------- 1 file changed, 11 insertions(+), 14 deletions(-) diff --git a/Arrow/Basic.lean b/Arrow/Basic.lean index 44e4a02..2651e7c 100644 --- a/Arrow/Basic.lean +++ b/Arrow/Basic.lean @@ -202,8 +202,8 @@ variable [NeZero N] {R : SWF α N} def canonicalSwap (a b : α) (hab : a ≠ b) : Fin (N+1) → Profile α N := fun k: Fin (N+1) => fun i: Fin N => if i < k.val - then prefer b b a .Top (Ne.symm hab) -- b on top - else prefer a b b .Bot hab -- a on top + then prefer b b a .Not (Ne.symm hab) -- b on top + else prefer a b b .Not hab -- a on top /-- `flipping R a b hab k` holds iff society prefers `b ≻ a` when voters `0..k` prefer `b ≻ a`. -/ def flipping (R : SWF α N) (a b : α) (hab : a ≠ b) := @@ -216,8 +216,8 @@ lemma flip_exists (R : SWF α N) (a b : α) (hab : a ≠ b) (hu : Unanimity R): unfold flipping canonicalSwap have: 0 < N := Nat.pos_of_ne_zero (NeZero.ne N) simp [Nat.sub_add_cancel this] - have: b ≻[R (fun i => prefer b b a .Top (Ne.symm hab) )] a := by - apply hu; intro i; simp [Preorder'.lt, prefer_expand b b a .Top (Ne.symm hab)] + have: b ≻[R (fun i => prefer b b a .Not (Ne.symm hab) )] a := by + apply hu; intro i; exact prefer_gt_mid_bot b b a (Ne.symm hab) (Ne.symm hab) exact Preorder'.lt_asymm _ _ _ this /-- The pivotal voter for `(a, b)`: the minimum `k` where society flips from `a ≻ b` to `b ≻ a`. -/ @@ -274,8 +274,8 @@ lemma nab_pivotal_bc (a b c: α) have hp : AgreeOn mg1 (canonicalSwap a b hab k.succ) a b := by intro i; simp only [mg1, canonicalSwap] by_cases hi : i.val < n_ab.val <;> simp [hk_succ, hi] - . simp [prefer_expand b c a .Not hba, prefer_expand b b a .Top] - . simp [prefer_expand a b b .Bot, prefer_gt_top_mid a b c hac hab] + . simp [prefer_expand b c a .Not hba, prefer_expand b b a] + . simp [prefer_expand a b b, prefer_gt_top_mid a b c hac hab] apply (strict_aiia hp hAIIA).mpr exact no_flip a b k hk @@ -327,15 +327,15 @@ lemma nab_pivotal_bc (a b c: α) unfold AgreeOn canonicalSwap mg2; intro i; by_cases hi: i < n_ab . have :i.val < n_ab +1 := by omega - simp [hi, this, prefer_expand b b a .Top] + simp [hi, this, prefer_expand b b a] split . simp [prefer_gt_mid_bot c b a hca hba] . simp [prefer_expand b c a .Not hba] . simp [prefer_expand b c a .Top hba] . by_cases hi2: i = n_ab - . simp [hi2, prefer_expand b b a .Top, prefer_gt_top_mid b a c hbc hba] + . simp [hi2, prefer_expand b b a, prefer_gt_top_mid b a c hbc hba] . have :¬ (i.val < n_ab +1 ):= by omega - simp [hi, hi2, this, prefer_expand a b b .Bot] + simp [hi, hi2, this, prefer_expand a b b] split . simp [prefer_expand a c b .Not hab] . simp [prefer_gt_top_mid a b c hac hab] @@ -379,7 +379,7 @@ lemma nab_le_nbc (a b c: α) simp only [cs, canonicalSwap] split_ifs with hh . simp at hh; omega - . obtain ⟨h, _, _, _, hn⟩ := prefer_expand b c c .Bot hbc; exact ⟨h, (hn hbc).1⟩ + . exact prefer_gt_top_mid b c c hbc hbc exact absurd (nab_pivotal_bc a b c hab hac hbc hu hAIIA cs h_pref) -- n_ab still dictates b over c ((Preorder'.not_lt _ _ _).mpr (flipped b c)) -- but n_bc flipped, so society should prefer c over b @@ -392,10 +392,7 @@ lemma ncb_le_nab (a b c: α) by_contra h; push_neg at h let n_ab := pivoter a b hab hu let cs := canonicalSwap c b (Ne.symm hbc) n_ab.succ - have: b ≻[cs n_ab] c := by - simp [cs, canonicalSwap] - obtain ⟨_, h, _, _, hn⟩ := prefer_expand b b c .Top hbc - exact ⟨ h, (hn hbc).2⟩ + have: b ≻[cs n_ab] c := by simp [cs, canonicalSwap]; exact prefer_gt_mid_bot b b c hbc hbc exact absurd (nab_pivotal_bc a b c hab hac hbc hu hAIIA cs this) -- n_ab prefer b over c, so is society (Preorder'.lt_asymm _ _ _ (no_flip c b n_ab h)) -- n_ab before pivoter, so b c shouldn't flip From 449726a1b01dff1370e98cfc5110c073509bac99 Mon Sep 17 00:00:00 2001 From: ChihChengLiang Date: Mon, 16 Mar 2026 04:58:34 +0800 Subject: [PATCH 19/20] nitpick --- Arrow/Basic.lean | 4 +--- 1 file changed, 1 insertion(+), 3 deletions(-) diff --git a/Arrow/Basic.lean b/Arrow/Basic.lean index 2651e7c..32487f1 100644 --- a/Arrow/Basic.lean +++ b/Arrow/Basic.lean @@ -242,9 +242,7 @@ lemma nab_pivotal_bc (a b c: α) (hu: Unanimity R) (hAIIA: AIIA R) : Dictates R (pivoter a b hab hu) b c := by let n_ab := pivoter a b hab hu - have hba := Ne.symm hab - have hca := Ne.symm hac - have hcb := Ne.symm hbc + 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 From 2f7beeae29619947f1b9f4e10afb6d1f54f5e488 Mon Sep 17 00:00:00 2001 From: ChihChengLiang Date: Mon, 16 Mar 2026 05:04:05 +0800 Subject: [PATCH 20/20] comment --- Arrow/Basic.lean | 1 + 1 file changed, 1 insertion(+) diff --git a/Arrow/Basic.lean b/Arrow/Basic.lean index 32487f1..148cae5 100644 --- a/Arrow/Basic.lean +++ b/Arrow/Basic.lean @@ -202,6 +202,7 @@ variable [NeZero N] {R : SWF α N} def canonicalSwap (a b : α) (hab : a ≠ b) : Fin (N+1) → Profile α N := fun k: Fin (N+1) => fun i: Fin N => if i < k.val + -- `prefer` takes 3 items, we duplicate middle as a workaround then prefer b b a .Not (Ne.symm hab) -- b on top else prefer a b b .Not hab -- a on top