Simp prefer ifs

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