|
| 1 | +/- |
| 2 | +Copyright (c) 2025 Vasilii Nesterov. All rights reserved. |
| 3 | +Released under Apache 2.0 license as described in the file LICENSE. |
| 4 | +Authors: Vasilii Nesterov |
| 5 | +-/ |
| 6 | +import Batteries.Data.List.Pairwise |
| 7 | +import Mathlib.Tactic.Order.CollectFacts |
| 8 | +import Batteries.Tactic.GeneralizeProofs |
| 9 | +import Mathlib.Util.Qq |
| 10 | + |
| 11 | +/-! |
| 12 | +# Translating linear orders to ℤ |
| 13 | +
|
| 14 | +In this file we implement the translation of a problem in any linearly ordered type to a problem in |
| 15 | +`ℤ`. This allows us to use the `omega` tactic to solve it. |
| 16 | +
|
| 17 | +While the core algorithm of the `order` tactic is complete for the theory of linear orders in the |
| 18 | +signature (`<`, `≤`), |
| 19 | +it becomes incomplete in the signature with lattice operations `⊓` and `⊔`. With these operations, |
| 20 | +the problem becomes NP-hard, and the idea is to reuse a smart and efficient procedure, such as |
| 21 | +`omega`. |
| 22 | +
|
| 23 | +## TODO |
| 24 | +
|
| 25 | +Migrate to `grind` when it is ready. |
| 26 | +-/ |
| 27 | + |
| 28 | +namespace Mathlib.Tactic.Order.ToInt |
| 29 | + |
| 30 | +variable {α : Type*} [LinearOrder α] {n : ℕ} (val : Fin n → α) |
| 31 | + |
| 32 | +/-- The main theorem asserting the existence of a translation. |
| 33 | +We use `Classical.chooose` to turn this into a value for use in the `order` tactic, |
| 34 | +see `toInt`. |
| 35 | +-/ |
| 36 | +theorem exists_translation : ∃ tr : Fin n → ℤ, ∀ i j, val i ≤ val j ↔ tr i ≤ tr j := by |
| 37 | + let li := List.ofFn val |
| 38 | + let sli := li.mergeSort |
| 39 | + have (i : Fin n) : ∃ j : Fin sli.length, sli[j] = val i := by |
| 40 | + apply List.get_of_mem |
| 41 | + rw [List.Perm.mem_iff (List.mergeSort_perm _ _)] |
| 42 | + simp [li] |
| 43 | + use fun i ↦ (this i).choose |
| 44 | + intro i j |
| 45 | + simp only [Fin.getElem_fin, Int.ofNat_le] |
| 46 | + by_cases h_eq : val i = val j |
| 47 | + · simp [h_eq] |
| 48 | + generalize_proofs _ hi hj |
| 49 | + rw [← hi.choose_spec, ← hj.choose_spec] at h_eq |
| 50 | + conv_lhs => rw [← hi.choose_spec, ← hj.choose_spec] |
| 51 | + have := List.sorted_mergeSort (l := li) (le := fun a b ↦ decide (a ≤ b)) |
| 52 | + (by simpa using Preorder.le_trans) (by simpa using LinearOrder.le_total) |
| 53 | + rw [List.pairwise_iff_get] at this |
| 54 | + refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩ |
| 55 | + · contrapose! h |
| 56 | + exact lt_of_le_of_ne (by simpa using (this hj.choose hi.choose (by simpa))) |
| 57 | + (fun h ↦ h_eq (h.symm)) |
| 58 | + · simpa using this hi.choose hj.choose (by apply lt_of_le_of_ne h; contrapose! h_eq; simp [h_eq]) |
| 59 | + |
| 60 | +/-- Auxiliary definition used by the `order` tactic to transfer facts in a linear order to `ℤ`. -/ |
| 61 | +noncomputable def toInt (k : Fin n) : ℤ := |
| 62 | + (exists_translation val).choose k |
| 63 | + |
| 64 | +variable (i j k : Fin n) |
| 65 | + |
| 66 | +theorem toInt_le_toInt : toInt val i ≤ toInt val j ↔ val i ≤ val j := by |
| 67 | + simp [toInt, (exists_translation val).choose_spec] |
| 68 | + |
| 69 | +theorem toInt_lt_toInt : toInt val i < toInt val j ↔ val i < val j := by |
| 70 | + simpa using (toInt_le_toInt val j i).not |
| 71 | + |
| 72 | +theorem toInt_eq_toInt : toInt val i = toInt val j ↔ val i = val j := by |
| 73 | + simp [toInt_le_toInt, le_antisymm_iff] |
| 74 | + |
| 75 | +theorem toInt_ne_toInt : toInt val i ≠ toInt val j ↔ val i ≠ val j := by |
| 76 | + simpa using (toInt_eq_toInt val i j).not |
| 77 | + |
| 78 | +theorem toInt_nle_toInt : ¬toInt val i ≤ toInt val j ↔ ¬val i ≤ val j := by |
| 79 | + simpa using toInt_lt_toInt val j i |
| 80 | + |
| 81 | +theorem toInt_nlt_toInt : ¬toInt val i < toInt val j ↔ ¬val i < val j := by |
| 82 | + simpa using toInt_le_toInt val j i |
| 83 | + |
| 84 | +theorem toInt_sup_toInt_eq_toInt : |
| 85 | + toInt val i ⊔ toInt val j = toInt val k ↔ val i ⊔ val j = val k := by |
| 86 | + simp [le_antisymm_iff, sup_le_iff, le_sup_iff, toInt_le_toInt] |
| 87 | + |
| 88 | +theorem toInt_inf_toInt_eq_toInt : |
| 89 | + toInt val i ⊓ toInt val j = toInt val k ↔ val i ⊓ val j = val k := by |
| 90 | + simp [le_antisymm_iff, inf_le_iff, le_inf_iff, toInt_le_toInt] |
| 91 | + |
| 92 | +open Lean Meta Qq |
| 93 | + |
| 94 | +/-- Given an array `atoms : Array α`, create an expression representing a function |
| 95 | +`f : Fin atoms.size → α` such that `f n` is defeq to `atoms[n]` for `n : Fin atoms.size`. -/ |
| 96 | +def mkFinFun {u : Level} {α : Q(Type $u)} (atoms : Array Q($α)) : MetaM Expr := do |
| 97 | + if h : atoms.isEmpty then |
| 98 | + return q(Fin.elim0 : Fin 0 → $α) |
| 99 | + else |
| 100 | + let rarray := RArray.ofArray atoms (by simpa [Array.size_pos_iff] using h) |
| 101 | + let rarrayExpr : Q(RArray $α) ← rarray.toExpr α (fun x ↦ x) |
| 102 | + haveI m : Q(ℕ) := mkNatLit atoms.size |
| 103 | + return q(fun (x : Fin $m) ↦ ($rarrayExpr).get x.val) |
| 104 | + |
| 105 | +/-- Translates a set of values in a linear ordered type to `ℤ`, |
| 106 | +preserving all the facts except for `.isTop` and `.isBot`. These facts are filtered at the |
| 107 | +preprocessing step. -/ |
| 108 | +def translateToInt {u : Lean.Level} (type : Q(Type u)) (inst : Q(LinearOrder $type)) |
| 109 | + (idxToAtom : Std.HashMap ℕ Q($type)) |
| 110 | + (facts : Array AtomicFact) : |
| 111 | + MetaM <| Std.HashMap ℕ Q(ℤ) × Array AtomicFact := do |
| 112 | + haveI nE : Q(ℕ) := mkNatLitQ idxToAtom.size |
| 113 | + haveI finFun : Q(Fin $nE → $type) := |
| 114 | + ← mkFinFun (Array.ofFn fun (n : Fin idxToAtom.size) => idxToAtom[n]!) |
| 115 | + let toFinUnsafe : ℕ → Q(Fin $nE) := fun k => |
| 116 | + haveI kE := mkNatLitQ k |
| 117 | + haveI heq : decide ($kE < $nE) =Q true := ⟨⟩ |
| 118 | + q(⟨$kE, of_decide_eq_true $heq⟩) |
| 119 | + return Prod.snd <| facts.foldl (fun (curr, map, facts) fact => |
| 120 | + match fact with |
| 121 | + | .eq lhs rhs prf => |
| 122 | + (curr, map, facts.push ( |
| 123 | + haveI lhsFin := toFinUnsafe lhs |
| 124 | + haveI rhsFin := toFinUnsafe rhs |
| 125 | + haveI prfQ : Q($finFun $lhsFin = $finFun $rhsFin) := prf |
| 126 | + .eq lhs rhs q((toInt_eq_toInt $finFun $lhsFin $rhsFin).mpr $prfQ) |
| 127 | + )) |
| 128 | + | .ne lhs rhs prf => |
| 129 | + (curr, map, facts.push ( |
| 130 | + haveI lhsFin := toFinUnsafe lhs |
| 131 | + haveI rhsFin := toFinUnsafe rhs |
| 132 | + haveI prfQ : Q($finFun $lhsFin ≠ $finFun $rhsFin) := prf |
| 133 | + .ne lhs rhs q((toInt_ne_toInt $finFun $lhsFin $rhsFin).mpr $prfQ) |
| 134 | + )) |
| 135 | + | .le lhs rhs prf => |
| 136 | + (curr, map, facts.push ( |
| 137 | + haveI lhsFin := toFinUnsafe lhs |
| 138 | + haveI rhsFin := toFinUnsafe rhs |
| 139 | + haveI prfQ : Q($finFun $lhsFin ≤ $finFun $rhsFin) := prf |
| 140 | + .le lhs rhs q((toInt_le_toInt $finFun $lhsFin $rhsFin).mpr $prfQ) |
| 141 | + )) |
| 142 | + | .lt lhs rhs prf => |
| 143 | + (curr, map, facts.push ( |
| 144 | + haveI lhsFin := toFinUnsafe lhs |
| 145 | + haveI rhsFin := toFinUnsafe rhs |
| 146 | + haveI prfQ : Q($finFun $lhsFin < $finFun $rhsFin) := prf |
| 147 | + .lt lhs rhs q((toInt_lt_toInt $finFun $lhsFin $rhsFin).mpr $prfQ) |
| 148 | + )) |
| 149 | + | .nle lhs rhs prf => |
| 150 | + (curr, map, facts.push ( |
| 151 | + haveI lhsFin := toFinUnsafe lhs |
| 152 | + haveI rhsFin := toFinUnsafe rhs |
| 153 | + haveI prfQ : Q(¬$finFun $lhsFin ≤ $finFun $rhsFin) := prf |
| 154 | + .nle lhs rhs q((toInt_nle_toInt $finFun $lhsFin $rhsFin).mpr $prfQ) |
| 155 | + )) |
| 156 | + | .nlt lhs rhs prf => |
| 157 | + (curr, map, facts.push ( |
| 158 | + haveI lhsFin := toFinUnsafe lhs |
| 159 | + haveI rhsFin := toFinUnsafe rhs |
| 160 | + haveI prfQ : Q(¬$finFun $lhsFin < $finFun $rhsFin) := prf |
| 161 | + .nlt lhs rhs q((toInt_nlt_toInt $finFun $lhsFin $rhsFin).mpr $prfQ) |
| 162 | + )) |
| 163 | + | .isBot _ |
| 164 | + | .isTop _ => (curr, map, facts) |
| 165 | + | .isSup lhs rhs val => |
| 166 | + haveI lhsFin := toFinUnsafe lhs |
| 167 | + haveI rhsFin := toFinUnsafe rhs |
| 168 | + haveI valFin := toFinUnsafe val |
| 169 | + haveI heq : max («$finFun» «$lhsFin») («$finFun» «$rhsFin») =Q «$finFun» «$valFin» := ⟨⟩ |
| 170 | + (curr + 1, map.insert curr q(toInt $finFun $lhsFin ⊔ toInt $finFun $rhsFin), |
| 171 | + (facts.push (.isSup lhs rhs curr)).push (.eq curr val |
| 172 | + q((toInt_sup_toInt_eq_toInt $finFun $lhsFin $rhsFin $valFin).mpr $heq) |
| 173 | + ) |
| 174 | + ) |
| 175 | + | .isInf lhs rhs val => |
| 176 | + haveI lhsFin := toFinUnsafe lhs |
| 177 | + haveI rhsFin := toFinUnsafe rhs |
| 178 | + haveI valFin := toFinUnsafe val |
| 179 | + haveI heq : min («$finFun» «$lhsFin») («$finFun» «$rhsFin») =Q «$finFun» «$valFin» := ⟨⟩ |
| 180 | + (curr + 1, map.insert curr q(toInt $finFun $lhsFin ⊓ toInt $finFun $rhsFin), |
| 181 | + (facts.push (.isInf lhs rhs curr)).push (.eq curr val |
| 182 | + q((toInt_inf_toInt_eq_toInt $finFun $lhsFin $rhsFin $valFin).mpr $heq) |
| 183 | + ) |
| 184 | + )) |
| 185 | + (idxToAtom.size, idxToAtom.map fun k _ => |
| 186 | + haveI kFin := toFinUnsafe k |
| 187 | + q(toInt $finFun $kFin), Array.emptyWithCapacity idxToAtom.size) |
| 188 | + |
| 189 | +end Mathlib.Tactic.Order.ToInt |
| 190 | + |
| 191 | +export Mathlib.Tactic.Order.ToInt (translateToInt) |
0 commit comments