diff --git a/Arrow/Basic.lean b/Arrow/Basic.lean index 3bc3b7a..eec7e6e 100644 --- a/Arrow/Basic.lean +++ b/Arrow/Basic.lean @@ -103,43 +103,33 @@ 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 +@[simp] +def 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 @@ -171,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_expand b b a] + 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`. -/ @@ -216,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_expand a b c, hab] + intro _; simp [mg1, hn, prefer, hac, hba] exact hu _ _ _ h . -- Case n_ab ≠ 0: Use no_flip let k := n_ab - 1 @@ -225,17 +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 - 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] - + 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 - all_goals simp [prefer_expand b c a, prefer_expand a b c, hbc] + intro _; unfold mg1; split_ifs <;> simp [prefer, hbc, hba, hcb, hca] exact hu _ _ _ h -- `pp` has arbitrary preference on (b,c), except n_ab @@ -260,59 +245,32 @@ 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, prefer]; intro i; split_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, hbc, hcb] . -- 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 -- 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]; 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]; 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, 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]; 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] - . -- i = n_ab - simp [prefer_expand a b c, prefer_expand b a c, hac] - . -- 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 [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 @@ -329,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 with hh <;> simp_all [prefer_expand b c c]; 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 @@ -342,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_expand b b c] + 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