From 17ba0a95736208172767a24d513f8b4220185c6a Mon Sep 17 00:00:00 2001 From: ChihChengLiang Date: Thu, 26 Mar 2026 18:59:03 +0800 Subject: [PATCH 1/3] extract prefer ifs simp more --- Arrow/Basic.lean | 112 +++++++++++++++++------------------------------ 1 file changed, 40 insertions(+), 72 deletions(-) diff --git a/Arrow/Basic.lean b/Arrow/Basic.lean index 3bc3b7a..f8eedbc 100644 --- a/Arrow/Basic.lean +++ b/Arrow/Basic.lean @@ -103,43 +103,32 @@ Given three alternatives, `prefer a₀ a₁ a₂ tie` ranks them with optional t /-- Where ties occur in a 3-element preference ranking -/ inductive Tie | Not | Top | Bot +abbrev prefer_ifs (x y a₀ _a₁ a₂ : α) (tie : Tie): Prop := + match tie with + | .Not => + if x = a₂ then True -- a₂ is bottom + else if y = a₀ then True -- a₀ is top + else if x = a₀ then y = a₀ -- only a₀ ≤ a₀ + else if y = a₂ then x = a₂ -- only a₂ ≥ a₂ + else True + | .Top => + if y = a₂ then x = a₂ -- only a₂ ≥ a₂ (a₂ is bottom) + else if x = a₂ then True -- a₂ ≤ everything else + else True -- a₀ ~ a₁: both directions + | .Bot => + if x = a₀ then y = a₀ -- only a₀ ≤ a₀ (a₀ is top) + else if y = a₀ then True -- everything else ≤ a₀ + else True -- a₁ ~ a₂: both directions + /-- Construct a preference ordering with optional ties: - `Tie.Not`: a₀ > a₁ > a₂ (strict ranking) - `Tie.Top`: a₀ ~ a₁ > a₂ (top two tied) - `Tie.Bot`: a₀ > a₁ ~ a₂ (bottom two tied) -/ def prefer (a₀ _a₁ a₂ : α) (tie : Tie) (h02 : a₀ ≠ a₂) : Preorder' α where - le x y := match tie with - | .Not => - if x = a₂ then True -- a₂ is bottom - else if y = a₀ then True -- a₀ is top - else if x = a₀ then y = a₀ -- only a₀ ≤ a₀ - else if y = a₂ then x = a₂ -- only a₂ ≥ a₂ - else True - | .Top => - if y = a₂ then x = a₂ -- only a₂ ≥ a₂ (a₂ is bottom) - else if x = a₂ then True -- a₂ ≤ everything else - else True -- a₀ ~ a₁: both directions - | .Bot => - if x = a₀ then y = a₀ -- only a₀ ≤ a₀ (a₀ is top) - else if y = a₀ then True -- everything else ≤ a₀ - else True -- a₁ ~ a₂: both directions + le x y := prefer_ifs x y a₀ _a₁ a₂ tie refl := by intro x; cases tie <;> simp - trans := by intro a b c ha hb; split <;> split_ifs <;> simp_all - total := by intro a b; split <;> by_cases a = a₂ <;> by_cases b = a₀ <;> simp_all - -lemma prefer_expand - (top mid bot: α)(tie: Tie := Tie.Not)(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) - ) - := by - intro p; unfold p prefer; simp; refine ⟨?_, ?_, ?_, ?_, ?_⟩ - all_goals split <;> try simp_all [Ne.symm htb] <;> intro h <;> exact Ne.symm h + trans := by intro a b c ha hb; unfold prefer_ifs at *; split <;> split_ifs <;> simp_all + total := by intro a b; unfold prefer_ifs at *; split <;> by_cases a = a₂ <;> by_cases b = a₀ <;> simp_all /-! ## Pivotal Voter @@ -172,7 +161,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 .Not (Ne.symm hab) )] a := by - apply hu; intro _; simp [prefer_expand b b a] + apply hu; intro _; unfold prefer prefer_ifs; simp [hab, Ne.symm hab] intro _; exact this.1 /-- The pivotal voter for `(a, b)`: the minimum `k` where society flips from `a ≻ b` to `b ≻ a`. -/ @@ -216,7 +205,7 @@ lemma nab_dictate_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 _; simp [mg1, hn, prefer_expand a b c, hab] + intro _; simp [mg1, hn, prefer, prefer_ifs, hac, hba] exact hu _ _ _ h . -- Case n_ab ≠ 0: Use no_flip let k := n_ab - 1 @@ -226,16 +215,13 @@ lemma nab_dictate_bc (a b c: α) have hk : k.val < n_ab := by omega have hp : AgreeOn mg1 (canonicalSwap a b hab k.succ) a b := by intro i; unfold mg1 - by_cases hi : i.val < n_ab.val <;> simp [hk_succ, hi] - . simp [prefer_expand b b a, prefer_expand b c a] - . simp [prefer_expand a b b, prefer_expand a b c, hab] - + by_cases hi : i.val < n_ab.val <;> simp [hk_succ, hi, prefer, prefer_ifs, hac, hab] simp [hAIIA _ _ _ _ hp] exact no_flip a b k hk -- b ≻ c by unanimity . have h: ∀ i: Fin N, b ≻[mg1 i] c := by intro _; unfold mg1; split_ifs - all_goals simp [prefer_expand b c a, prefer_expand a b c, hbc] + all_goals simp [prefer, prefer_ifs, hbc, hba, hcb, hca] exact hu _ _ _ h -- `pp` has arbitrary preference on (b,c), except n_ab @@ -260,19 +246,13 @@ lemma nab_dictate_bc (a b c: α) | .Indiff _ _ => prefer a b c .Bot hac -- a ≻ b ~ c have h_agree: AgreeOn pp mg2 b c := by - simp [mg2]; intro i; split_ifs + simp [mg2]; intro i; split_ifs <;> simp_all [prefer, prefer_ifs] . -- i < n_ab - cases (pp i).cmp b c with - | LT h hn => simp [ h, hn, prefer_expand c b a, hcb] - | GT hn h => simp [ h, hn, prefer_expand b c a, hbc] - | Indiff h1 h2 => simp [h1, h2, prefer_expand b c a .Top hba, hca] + split <;> simp_all . -- i = n_ab - subst i n_ab; simp [h_pp_bc.1, h_pp_bc.2, prefer_expand b a c .Not hbc] + subst i n_ab; simp [h_pp_bc.1, h_pp_bc.2] . -- i > n_ab - cases (pp i).cmp b c with - | LT h hn => simp [ h, hn, prefer_expand a c b, hcb] - | GT hn h => simp [ h, hn, prefer_expand a b c, hbc] - | Indiff h1 h2 => simp [h1, h2, prefer_expand a b c .Bot hac, hab] + split <;> simp_all have hbac: b ≽[R mg2] a ≻ c := by constructor @@ -281,38 +261,26 @@ lemma nab_dictate_bc (a b c: α) unfold 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] - split - . simp [prefer_expand c b a, hba] - . simp [prefer_expand b c a] - . simp [prefer_expand b c a .Top hba] + simp [hi, this, prefer, prefer_ifs] + split <;> simp[hab, hba, hac] . by_cases hi2: i = n_ab - . simp [hi2, prefer_expand b b a, prefer_expand b a c, hba] + . simp [hi2, prefer, prefer_ifs, hbc, hba] . have :¬ (i.val < n_ab +1 ):= by omega - simp [hi, hi2, this, prefer_expand a b b] - split - . simp [prefer_expand a c b] - . simp [prefer_expand a b c, hab] - . simp [prefer_expand a b c .Bot hac, hab] + simp [hi, hi2, this, prefer, prefer_ifs] + split <;> simp [hac, hab] simp only [hAIIA _ _ _ _ h_agree_ba] exact flipped a b -- By AIIA . have h_agree_ac: AgreeOn mg2 mg1 a c := by simp [mg2, mg1]; intro i; split_ifs . -- i < n_ab - simp [prefer_expand b c a, hca] - split - . simp [prefer_expand c b a] - . simp [prefer_expand b c a, hca] - . simp [prefer_expand b c a .Top hba, hca] + simp [prefer, prefer_ifs] + split <;> simp [hca, hac, hab] . -- i = n_ab - simp [prefer_expand a b c, prefer_expand b a c, hac] + simp [prefer, prefer_ifs, hac, hcb, hca] . -- i > n_ab - simp [prefer_expand a b c] - split - . simp [prefer_expand a c b, hac] - . simp [prefer_expand a b c] - . simp [prefer_expand a b c .Bot hac] + simp [prefer, prefer_ifs] + split <;> simp [hac, hab] simp [hAIIA _ _ _ _ h_agree_ac] exact (R mg1).lt_trans habc.2 habc.1 @@ -329,7 +297,7 @@ lemma nab_le_nbc (a b c: α) by_contra h; push_neg at h; let cs := canonicalSwap b c hbc (pivoter b c hbc hu).succ have h_pref : b ≻[cs (pivoter a b hab hu)] c := by - simp [cs]; split_ifs with hh <;> simp_all [prefer_expand b c c]; omega + simp [cs]; split_ifs with hh <;> simp_all [prefer, prefer_ifs, Ne.symm hbc]; omega exact absurd (nab_dictate_bc a b c hab hac hbc hu hAIIA cs h_pref) -- n_ab still dictates b over c (flipped b c |> Preorder'.not_lt.mpr) -- but n_bc flipped, so society should prefer c over b @@ -342,7 +310,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, prefer_expand b b c] + have: b ≻[cs n_ab] c := by simp [cs, prefer, prefer_ifs, hbc, Ne.symm hbc] exact absurd (nab_dictate_bc a b c hab hac hbc hu hAIIA cs this) -- n_ab prefer b over c, so is society (no_flip c b n_ab h |> Preorder'.lt_asymm) -- n_ab before pivoter, so b c shouldn't flip From b6eac453dc5455a91aa685ba5290a6ac874c6589 Mon Sep 17 00:00:00 2001 From: ChihChengLiang Date: Thu, 26 Mar 2026 19:26:24 +0800 Subject: [PATCH 2/3] reduce cases --- Arrow/Basic.lean | 35 ++++++++++++----------------------- 1 file changed, 12 insertions(+), 23 deletions(-) diff --git a/Arrow/Basic.lean b/Arrow/Basic.lean index f8eedbc..03432d6 100644 --- a/Arrow/Basic.lean +++ b/Arrow/Basic.lean @@ -161,7 +161,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 .Not (Ne.symm hab) )] a := by - apply hu; intro _; unfold prefer prefer_ifs; simp [hab, Ne.symm hab] + apply hu; intro _; simp [prefer, prefer_ifs, hab, Ne.symm hab] intro _; exact this.1 /-- The pivotal voter for `(a, b)`: the minimum `k` where society flips from `a ≻ b` to `b ≻ a`. -/ @@ -214,14 +214,12 @@ lemma nab_dictate_bc (a b c: α) exact Nat.sub_add_cancel (Nat.one_le_iff_ne_zero.mpr (Fin.val_ne_of_ne hn)) have hk : k.val < n_ab := by omega have hp : AgreeOn mg1 (canonicalSwap a b hab k.succ) a b := by - intro i; unfold mg1 - by_cases hi : i.val < n_ab.val <;> simp [hk_succ, hi, prefer, prefer_ifs, hac, hab] + intro i; unfold mg1; split_ifs with hi <;> simp [hk_succ, hi, prefer, prefer_ifs, hac, hab] simp [hAIIA _ _ _ _ hp] exact no_flip a b k hk -- b ≻ c by unanimity . have h: ∀ i: Fin N, b ≻[mg1 i] c := by - intro _; unfold mg1; split_ifs - all_goals simp [prefer, prefer_ifs, hbc, hba, hcb, hca] + intro _; unfold mg1; split_ifs <;> simp [prefer, prefer_ifs, hbc, hba, hcb, hca] exact hu _ _ _ h -- `pp` has arbitrary preference on (b,c), except n_ab @@ -246,11 +244,11 @@ lemma nab_dictate_bc (a b c: α) | .Indiff _ _ => prefer a b c .Bot hac -- a ≻ b ~ c have h_agree: AgreeOn pp mg2 b c := by - simp [mg2]; intro i; split_ifs <;> simp_all [prefer, prefer_ifs] + simp [mg2]; intro i; split_ifs <;> simp [prefer, prefer_ifs] . -- i < n_ab split <;> simp_all . -- i = n_ab - subst i n_ab; simp [h_pp_bc.1, h_pp_bc.2] + subst i n_ab; simp [h_pp_bc.1, h_pp_bc.2, hbc, hcb] . -- i > n_ab split <;> simp_all @@ -258,29 +256,20 @@ lemma nab_dictate_bc (a b c: α) constructor -- By AIIA on nab pivoting defintion . have h_agree_ba: AgreeOn mg2 (canonicalSwap a b hab n_ab.succ) b a := by - unfold mg2; intro i; + simp [mg2, prefer, prefer_ifs]; intro i; by_cases hi: i < n_ab . have :i.val < n_ab +1 := by omega - simp [hi, this, prefer, prefer_ifs] - split <;> simp[hab, hba, hac] + simp [hi, this]; split <;> simp[hab, hba, hac] . by_cases hi2: i = n_ab - . simp [hi2, prefer, prefer_ifs, hbc, hba] + . simp [hi2, hbc, hba] . have :¬ (i.val < n_ab +1 ):= by omega - simp [hi, hi2, this, prefer, prefer_ifs] - split <;> simp [hac, hab] + simp [hi, hi2, this]; split <;> simp [hac, hab] simp only [hAIIA _ _ _ _ h_agree_ba] exact flipped a b -- By AIIA . have h_agree_ac: AgreeOn mg2 mg1 a c := by - simp [mg2, mg1]; intro i; split_ifs - . -- i < n_ab - simp [prefer, prefer_ifs] - split <;> simp [hca, hac, hab] - . -- i = n_ab - simp [prefer, prefer_ifs, hac, hcb, hca] - . -- i > n_ab - simp [prefer, prefer_ifs] - split <;> simp [hac, hab] + simp [mg2, mg1, prefer, prefer_ifs]; intro _; split_ifs <;> try split + all_goals simp [hca, hac, hab, hcb] simp [hAIIA _ _ _ _ h_agree_ac] exact (R mg1).lt_trans habc.2 habc.1 @@ -297,7 +286,7 @@ lemma nab_le_nbc (a b c: α) by_contra h; push_neg at h; let cs := canonicalSwap b c hbc (pivoter b c hbc hu).succ have h_pref : b ≻[cs (pivoter a b hab hu)] c := by - simp [cs]; split_ifs with hh <;> simp_all [prefer, prefer_ifs, Ne.symm hbc]; omega + simp [cs]; split_ifs <;> simp [prefer, prefer_ifs, Ne.symm hbc, hbc]; omega exact absurd (nab_dictate_bc a b c hab hac hbc hu hAIIA cs h_pref) -- n_ab still dictates b over c (flipped b c |> Preorder'.not_lt.mpr) -- but n_bc flipped, so society should prefer c over b From cf0b13766b211ede0b8af3a52ce05232ae9c429e Mon Sep 17 00:00:00 2001 From: ChihChengLiang Date: Thu, 26 Mar 2026 20:18:34 +0800 Subject: [PATCH 3/3] make prefer_ifs @simp --- Arrow/Basic.lean | 23 ++++++++++++----------- 1 file changed, 12 insertions(+), 11 deletions(-) diff --git a/Arrow/Basic.lean b/Arrow/Basic.lean index 03432d6..eec7e6e 100644 --- a/Arrow/Basic.lean +++ b/Arrow/Basic.lean @@ -103,7 +103,8 @@ Given three alternatives, `prefer a₀ a₁ a₂ tie` ranks them with optional t /-- Where ties occur in a 3-element preference ranking -/ inductive Tie | Not | Top | Bot -abbrev prefer_ifs (x y a₀ _a₁ a₂ : α) (tie : Tie): Prop := +@[simp] +def prefer_ifs (x y a₀ _a₁ a₂ : α) (tie : Tie): Prop := match tie with | .Not => if x = a₂ then True -- a₂ is bottom @@ -160,8 +161,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 .Not (Ne.symm hab) )] a := by - apply hu; intro _; simp [prefer, prefer_ifs, hab, Ne.symm hab] + have : b ≻[R (fun _ => prefer b b a .Not (Ne.symm hab) )] a := by + apply hu; intro _; simp [prefer, hab, Ne.symm hab] intro _; exact this.1 /-- The pivotal voter for `(a, b)`: the minimum `k` where society flips from `a ≻ b` to `b ≻ a`. -/ @@ -205,7 +206,7 @@ lemma nab_dictate_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 _; simp [mg1, hn, prefer, prefer_ifs, hac, hba] + intro _; simp [mg1, hn, prefer, hac, hba] exact hu _ _ _ h . -- Case n_ab ≠ 0: Use no_flip let k := n_ab - 1 @@ -214,12 +215,12 @@ lemma nab_dictate_bc (a b c: α) exact Nat.sub_add_cancel (Nat.one_le_iff_ne_zero.mpr (Fin.val_ne_of_ne hn)) have hk : k.val < n_ab := by omega have hp : AgreeOn mg1 (canonicalSwap a b hab k.succ) a b := by - intro i; unfold mg1; split_ifs with hi <;> simp [hk_succ, hi, prefer, prefer_ifs, hac, hab] + intro i; unfold mg1; split_ifs with hi <;> simp [hk_succ, hi, prefer, hac, hab] simp [hAIIA _ _ _ _ hp] exact no_flip a b k hk -- b ≻ c by unanimity . have h: ∀ i: Fin N, b ≻[mg1 i] c := by - intro _; unfold mg1; split_ifs <;> simp [prefer, prefer_ifs, hbc, hba, hcb, hca] + intro _; unfold mg1; split_ifs <;> simp [prefer, hbc, hba, hcb, hca] exact hu _ _ _ h -- `pp` has arbitrary preference on (b,c), except n_ab @@ -244,7 +245,7 @@ lemma nab_dictate_bc (a b c: α) | .Indiff _ _ => prefer a b c .Bot hac -- a ≻ b ~ c have h_agree: AgreeOn pp mg2 b c := by - simp [mg2]; intro i; split_ifs <;> simp [prefer, prefer_ifs] + simp [mg2, prefer]; intro i; split_ifs . -- i < n_ab split <;> simp_all . -- i = n_ab @@ -256,7 +257,7 @@ lemma nab_dictate_bc (a b c: α) constructor -- By AIIA on nab pivoting defintion . have h_agree_ba: AgreeOn mg2 (canonicalSwap a b hab n_ab.succ) b a := by - simp [mg2, prefer, prefer_ifs]; intro i; + simp [mg2, prefer]; intro i; by_cases hi: i < n_ab . have :i.val < n_ab +1 := by omega simp [hi, this]; split <;> simp[hab, hba, hac] @@ -268,7 +269,7 @@ lemma nab_dictate_bc (a b c: α) exact flipped a b -- By AIIA . have h_agree_ac: AgreeOn mg2 mg1 a c := by - simp [mg2, mg1, prefer, prefer_ifs]; intro _; split_ifs <;> try split + simp [mg2, mg1, prefer]; intro _; split_ifs <;> try split all_goals simp [hca, hac, hab, hcb] simp [hAIIA _ _ _ _ h_agree_ac] exact (R mg1).lt_trans habc.2 habc.1 @@ -286,7 +287,7 @@ lemma nab_le_nbc (a b c: α) by_contra h; push_neg at h; let cs := canonicalSwap b c hbc (pivoter b c hbc hu).succ have h_pref : b ≻[cs (pivoter a b hab hu)] c := by - simp [cs]; split_ifs <;> simp [prefer, prefer_ifs, Ne.symm hbc, hbc]; omega + simp [cs, prefer]; split_ifs <;> simp [Ne.symm hbc, hbc]; omega exact absurd (nab_dictate_bc a b c hab hac hbc hu hAIIA cs h_pref) -- n_ab still dictates b over c (flipped b c |> Preorder'.not_lt.mpr) -- but n_bc flipped, so society should prefer c over b @@ -299,7 +300,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, prefer, prefer_ifs, hbc, Ne.symm hbc] + have: b ≻[cs n_ab] c := by simp [cs, prefer, hbc, Ne.symm hbc] exact absurd (nab_dictate_bc a b c hab hac hbc hu hAIIA cs this) -- n_ab prefer b over c, so is society (no_flip c b n_ab h |> Preorder'.lt_asymm) -- n_ab before pivoter, so b c shouldn't flip