|
| 1 | +/- |
| 2 | +Copyright (c) 2022 Abby J. Goldberg. All rights reserved. |
| 3 | +Released under Apache 2.0 license as described in the file LICENSE. |
| 4 | +Authors: Abby J. Goldberg, Mario Carneiro |
| 5 | +-/ |
| 6 | +import Mathlib.Tactic.Ring |
| 7 | + |
| 8 | +/-! |
| 9 | +# linear_combination' Tactic |
| 10 | +
|
| 11 | +In this file, the `linear_combination'` tactic is created. This tactic, which |
| 12 | +works over `CommRing`s, attempts to simplify the target by creating a linear combination |
| 13 | +of a list of equalities and subtracting it from the target. A `Syntax.Tactic` |
| 14 | +object can also be passed into the tactic, allowing the user to specify a |
| 15 | +normalization tactic. |
| 16 | +
|
| 17 | +## Implementation Notes |
| 18 | +
|
| 19 | +This tactic works by creating a weighted sum of the given equations with the |
| 20 | +given coefficients. Then, it subtracts the right side of the weighted sum |
| 21 | +from the left side so that the right side equals 0, and it does the same with |
| 22 | +the target. Afterwards, it sets the goal to be the equality between the |
| 23 | +lefthand side of the new goal and the lefthand side of the new weighted sum. |
| 24 | +Lastly, calls a normalization tactic on this target. |
| 25 | +
|
| 26 | +This file contains the `linear_combination'` tactic (note the '): the original |
| 27 | +Lean 4 implementation of the "linear combination" idea, written at the time of |
| 28 | +the port from Lean 3. Notably, its scope includes certain *nonlinear* |
| 29 | +operations. The `linear_combination` tactic (in a separate file) is a variant |
| 30 | +implementation, but this version is provided for backward-compatibility. |
| 31 | +
|
| 32 | +## References |
| 33 | +
|
| 34 | +* <https://leanprover.zulipchat.com/#narrow/stream/239415-metaprogramming-.2F.20tactics/topic/Linear.20algebra.20tactic/near/213928196> |
| 35 | +
|
| 36 | +-/ |
| 37 | + |
| 38 | +namespace Mathlib.Tactic.LinearCombination' |
| 39 | +open Lean hiding Rat |
| 40 | +open Elab Meta Term |
| 41 | + |
| 42 | +variable {α : Type*} {a a' a₁ a₂ b b' b₁ b₂ c : α} |
| 43 | + |
| 44 | +theorem pf_add_c [Add α] (p : a = b) (c : α) : a + c = b + c := p ▸ rfl |
| 45 | +theorem c_add_pf [Add α] (p : b = c) (a : α) : a + b = a + c := p ▸ rfl |
| 46 | +theorem add_pf [Add α] (p₁ : (a₁:α) = b₁) (p₂ : a₂ = b₂) : a₁ + a₂ = b₁ + b₂ := p₁ ▸ p₂ ▸ rfl |
| 47 | +theorem pf_sub_c [Sub α] (p : a = b) (c : α) : a - c = b - c := p ▸ rfl |
| 48 | +theorem c_sub_pf [Sub α] (p : b = c) (a : α) : a - b = a - c := p ▸ rfl |
| 49 | +theorem sub_pf [Sub α] (p₁ : (a₁:α) = b₁) (p₂ : a₂ = b₂) : a₁ - a₂ = b₁ - b₂ := p₁ ▸ p₂ ▸ rfl |
| 50 | +theorem neg_pf [Neg α] (p : (a:α) = b) : -a = -b := p ▸ rfl |
| 51 | +theorem pf_mul_c [Mul α] (p : a = b) (c : α) : a * c = b * c := p ▸ rfl |
| 52 | +theorem c_mul_pf [Mul α] (p : b = c) (a : α) : a * b = a * c := p ▸ rfl |
| 53 | +theorem mul_pf [Mul α] (p₁ : (a₁:α) = b₁) (p₂ : a₂ = b₂) : a₁ * a₂ = b₁ * b₂ := p₁ ▸ p₂ ▸ rfl |
| 54 | +theorem inv_pf [Inv α] (p : (a:α) = b) : a⁻¹ = b⁻¹ := p ▸ rfl |
| 55 | +theorem pf_div_c [Div α] (p : a = b) (c : α) : a / c = b / c := p ▸ rfl |
| 56 | +theorem c_div_pf [Div α] (p : b = c) (a : α) : a / b = a / c := p ▸ rfl |
| 57 | +theorem div_pf [Div α] (p₁ : (a₁:α) = b₁) (p₂ : a₂ = b₂) : a₁ / a₂ = b₁ / b₂ := p₁ ▸ p₂ ▸ rfl |
| 58 | + |
| 59 | +/-- Result of `expandLinearCombo`, either an equality proof or a value. -/ |
| 60 | +inductive Expanded |
| 61 | + /-- A proof of `a = b`. -/ |
| 62 | + | proof (pf : Syntax.Term) |
| 63 | + /-- A value, equivalently a proof of `c = c`. -/ |
| 64 | + | const (c : Syntax.Term) |
| 65 | + |
| 66 | +/-- |
| 67 | +Performs macro expansion of a linear combination expression, |
| 68 | +using `+`/`-`/`*`/`/` on equations and values. |
| 69 | +* `.proof p` means that `p` is a syntax corresponding to a proof of an equation. |
| 70 | + For example, if `h : a = b` then `expandLinearCombo (2 * h)` returns `.proof (c_add_pf 2 h)` |
| 71 | + which is a proof of `2 * a = 2 * b`. |
| 72 | +* `.const c` means that the input expression is not an equation but a value. |
| 73 | +-/ |
| 74 | +partial def expandLinearCombo (ty : Expr) (stx : Syntax.Term) : TermElabM Expanded := withRef stx do |
| 75 | + match stx with |
| 76 | + | `(($e)) => expandLinearCombo ty e |
| 77 | + | `($e₁ + $e₂) => do |
| 78 | + match ← expandLinearCombo ty e₁, ← expandLinearCombo ty e₂ with |
| 79 | + | .const c₁, .const c₂ => .const <$> ``($c₁ + $c₂) |
| 80 | + | .proof p₁, .const c₂ => .proof <$> ``(pf_add_c $p₁ $c₂) |
| 81 | + | .const c₁, .proof p₂ => .proof <$> ``(c_add_pf $p₂ $c₁) |
| 82 | + | .proof p₁, .proof p₂ => .proof <$> ``(add_pf $p₁ $p₂) |
| 83 | + | `($e₁ - $e₂) => do |
| 84 | + match ← expandLinearCombo ty e₁, ← expandLinearCombo ty e₂ with |
| 85 | + | .const c₁, .const c₂ => .const <$> ``($c₁ - $c₂) |
| 86 | + | .proof p₁, .const c₂ => .proof <$> ``(pf_sub_c $p₁ $c₂) |
| 87 | + | .const c₁, .proof p₂ => .proof <$> ``(c_sub_pf $p₂ $c₁) |
| 88 | + | .proof p₁, .proof p₂ => .proof <$> ``(sub_pf $p₁ $p₂) |
| 89 | + | `(-$e) => do |
| 90 | + match ← expandLinearCombo ty e with |
| 91 | + | .const c => .const <$> `(-$c) |
| 92 | + | .proof p => .proof <$> ``(neg_pf $p) |
| 93 | + | `(← $e) => do |
| 94 | + match ← expandLinearCombo ty e with |
| 95 | + | .const c => return .const c |
| 96 | + | .proof p => .proof <$> ``(Eq.symm $p) |
| 97 | + | `($e₁ * $e₂) => do |
| 98 | + match ← expandLinearCombo ty e₁, ← expandLinearCombo ty e₂ with |
| 99 | + | .const c₁, .const c₂ => .const <$> ``($c₁ * $c₂) |
| 100 | + | .proof p₁, .const c₂ => .proof <$> ``(pf_mul_c $p₁ $c₂) |
| 101 | + | .const c₁, .proof p₂ => .proof <$> ``(c_mul_pf $p₂ $c₁) |
| 102 | + | .proof p₁, .proof p₂ => .proof <$> ``(mul_pf $p₁ $p₂) |
| 103 | + | `($e⁻¹) => do |
| 104 | + match ← expandLinearCombo ty e with |
| 105 | + | .const c => .const <$> `($c⁻¹) |
| 106 | + | .proof p => .proof <$> ``(inv_pf $p) |
| 107 | + | `($e₁ / $e₂) => do |
| 108 | + match ← expandLinearCombo ty e₁, ← expandLinearCombo ty e₂ with |
| 109 | + | .const c₁, .const c₂ => .const <$> ``($c₁ / $c₂) |
| 110 | + | .proof p₁, .const c₂ => .proof <$> ``(pf_div_c $p₁ $c₂) |
| 111 | + | .const c₁, .proof p₂ => .proof <$> ``(c_div_pf $p₂ $c₁) |
| 112 | + | .proof p₁, .proof p₂ => .proof <$> ``(div_pf $p₁ $p₂) |
| 113 | + | e => |
| 114 | + -- We have the expected type from the goal, so we can fully synthesize this leaf node. |
| 115 | + withSynthesize do |
| 116 | + -- It is OK to use `ty` as the expected type even if `e` is a proof. |
| 117 | + -- The expected type is just a hint. |
| 118 | + let c ← withSynthesizeLight <| Term.elabTerm e ty |
| 119 | + if (← whnfR (← inferType c)).isEq then |
| 120 | + .proof <$> c.toSyntax |
| 121 | + else |
| 122 | + .const <$> c.toSyntax |
| 123 | + |
| 124 | +theorem eq_trans₃ (p : (a:α) = b) (p₁ : a = a') (p₂ : b = b') : a' = b' := p₁ ▸ p₂ ▸ p |
| 125 | + |
| 126 | +theorem eq_of_add [AddGroup α] (p : (a:α) = b) (H : (a' - b') - (a - b) = 0) : a' = b' := by |
| 127 | + rw [← sub_eq_zero] at p ⊢; rwa [sub_eq_zero, p] at H |
| 128 | + |
| 129 | +theorem eq_of_add_pow [Ring α] [NoZeroDivisors α] (n : ℕ) (p : (a:α) = b) |
| 130 | + (H : (a' - b')^n - (a - b) = 0) : a' = b' := by |
| 131 | + rw [← sub_eq_zero] at p ⊢; apply pow_eq_zero (n := n); rwa [sub_eq_zero, p] at H |
| 132 | + |
| 133 | +/-- Implementation of `linear_combination'` and `linear_combination2`. -/ |
| 134 | +def elabLinearCombination' (tk : Syntax) |
| 135 | + (norm? : Option Syntax.Tactic) (exp? : Option Syntax.NumLit) (input : Option Syntax.Term) |
| 136 | + (twoGoals := false) : Tactic.TacticM Unit := Tactic.withMainContext do |
| 137 | + let some (ty, _) := (← (← Tactic.getMainGoal).getType').eq? | |
| 138 | + throwError "'linear_combination'' only proves equalities" |
| 139 | + let p ← match input with |
| 140 | + | none => `(Eq.refl 0) |
| 141 | + | some e => |
| 142 | + match ← expandLinearCombo ty e with |
| 143 | + | .const c => `(Eq.refl $c) |
| 144 | + | .proof p => pure p |
| 145 | + let norm := norm?.getD (Unhygienic.run <| withRef tk `(tactic| ring1)) |
| 146 | + Term.withoutErrToSorry <| Tactic.evalTactic <| ← withFreshMacroScope <| |
| 147 | + if twoGoals then |
| 148 | + `(tactic| ( |
| 149 | + refine eq_trans₃ $p ?a ?b |
| 150 | + case' a => $norm:tactic |
| 151 | + case' b => $norm:tactic)) |
| 152 | + else |
| 153 | + match exp? with |
| 154 | + | some n => |
| 155 | + if n.getNat = 1 then `(tactic| (refine eq_of_add $p ?a; case' a => $norm:tactic)) |
| 156 | + else `(tactic| (refine eq_of_add_pow $n $p ?a; case' a => $norm:tactic)) |
| 157 | + | _ => `(tactic| (refine eq_of_add $p ?a; case' a => $norm:tactic)) |
| 158 | + |
| 159 | +/-- |
| 160 | +The `(norm := $tac)` syntax says to use `tac` as a normalization postprocessor for |
| 161 | +`linear_combination'`. The default normalizer is `ring1`, but you can override it with `ring_nf` |
| 162 | +to get subgoals from `linear_combination'` or with `skip` to disable normalization. |
| 163 | +-/ |
| 164 | +syntax normStx := atomic(" (" &"norm" " := ") withoutPosition(tactic) ")" |
| 165 | + |
| 166 | +/-- |
| 167 | +The `(exp := n)` syntax for `linear_combination'` says to take the goal to the `n`th power before |
| 168 | +subtracting the given combination of hypotheses. |
| 169 | +-/ |
| 170 | +syntax expStx := atomic(" (" &"exp" " := ") withoutPosition(num) ")" |
| 171 | + |
| 172 | +/-- |
| 173 | +`linear_combination'` attempts to simplify the target by creating a linear combination |
| 174 | + of a list of equalities and subtracting it from the target. |
| 175 | + The tactic will create a linear |
| 176 | + combination by adding the equalities together from left to right, so the order |
| 177 | + of the input hypotheses does matter. If the `normalize` field of the |
| 178 | + configuration is set to false, then the tactic will simply set the user up to |
| 179 | + prove their target using the linear combination instead of normalizing the subtraction. |
| 180 | +
|
| 181 | +Note: There is also a similar tactic `linear_combination` (no prime); this version is |
| 182 | +provided for backward compatibility. |
| 183 | +
|
| 184 | +Note: The left and right sides of all the equalities should have the same |
| 185 | + type, and the coefficients should also have this type. There must be |
| 186 | + instances of `Mul` and `AddGroup` for this type. |
| 187 | +
|
| 188 | +* The input `e` in `linear_combination' e` is a linear combination of proofs of equalities, |
| 189 | + given as a sum/difference of coefficients multiplied by expressions. |
| 190 | + The coefficients may be arbitrary expressions. |
| 191 | + The expressions can be arbitrary proof terms proving equalities. |
| 192 | + Most commonly they are hypothesis names `h1, h2, ...`. |
| 193 | +* `linear_combination' (norm := tac) e` runs the "normalization tactic" `tac` |
| 194 | + on the subgoal(s) after constructing the linear combination. |
| 195 | + * The default normalization tactic is `ring1`, which closes the goal or fails. |
| 196 | + * To get a subgoal in the case that it is not immediately provable, use |
| 197 | + `ring_nf` as the normalization tactic. |
| 198 | + * To avoid normalization entirely, use `skip` as the normalization tactic. |
| 199 | +* `linear_combination' (exp := n) e` will take the goal to the `n`th power before subtracting the |
| 200 | + combination `e`. In other words, if the goal is `t1 = t2`, `linear_combination' (exp := n) e` |
| 201 | + will change the goal to `(t1 - t2)^n = 0` before proceeding as above. |
| 202 | + This feature is not supported for `linear_combination2`. |
| 203 | +* `linear_combination2 e` is the same as `linear_combination' e` but it produces two |
| 204 | + subgoals instead of one: rather than proving that `(a - b) - (a' - b') = 0` where |
| 205 | + `a' = b'` is the linear combination from `e` and `a = b` is the goal, |
| 206 | + it instead attempts to prove `a = a'` and `b = b'`. |
| 207 | + Because it does not use subtraction, this form is applicable also to semirings. |
| 208 | + * Note that a goal which is provable by `linear_combination' e` may not be provable |
| 209 | + by `linear_combination2 e`; in general you may need to add a coefficient to `e` |
| 210 | + to make both sides match, as in `linear_combination2 e + c`. |
| 211 | + * You can also reverse equalities using `← h`, so for example if `h₁ : a = b` |
| 212 | + then `2 * (← h)` is a proof of `2 * b = 2 * a`. |
| 213 | +
|
| 214 | +Example Usage: |
| 215 | +``` |
| 216 | +example (x y : ℤ) (h1 : x*y + 2*x = 1) (h2 : x = y) : x*y = -2*y + 1 := by |
| 217 | + linear_combination' 1*h1 - 2*h2 |
| 218 | +
|
| 219 | +example (x y : ℤ) (h1 : x*y + 2*x = 1) (h2 : x = y) : x*y = -2*y + 1 := by |
| 220 | + linear_combination' h1 - 2*h2 |
| 221 | +
|
| 222 | +example (x y : ℤ) (h1 : x*y + 2*x = 1) (h2 : x = y) : x*y = -2*y + 1 := by |
| 223 | + linear_combination' (norm := ring_nf) -2*h2 |
| 224 | + /- Goal: x * y + x * 2 - 1 = 0 -/ |
| 225 | +
|
| 226 | +example (x y z : ℝ) (ha : x + 2*y - z = 4) (hb : 2*x + y + z = -2) |
| 227 | + (hc : x + 2*y + z = 2) : |
| 228 | + -3*x - 3*y - 4*z = 2 := by |
| 229 | + linear_combination' ha - hb - 2*hc |
| 230 | +
|
| 231 | +example (x y : ℚ) (h1 : x + y = 3) (h2 : 3*x = 7) : |
| 232 | + x*x*y + y*x*y + 6*x = 3*x*y + 14 := by |
| 233 | + linear_combination' x*y*h1 + 2*h2 |
| 234 | +
|
| 235 | +example (x y : ℤ) (h1 : x = -3) (h2 : y = 10) : 2*x = -6 := by |
| 236 | + linear_combination' (norm := skip) 2*h1 |
| 237 | + simp |
| 238 | +
|
| 239 | +axiom qc : ℚ |
| 240 | +axiom hqc : qc = 2*qc |
| 241 | +
|
| 242 | +example (a b : ℚ) (h : ∀ p q : ℚ, p = q) : 3*a + qc = 3*b + 2*qc := by |
| 243 | + linear_combination' 3 * h a b + hqc |
| 244 | +``` |
| 245 | +-/ |
| 246 | +syntax (name := linearCombination') "linear_combination'" |
| 247 | + (normStx)? (expStx)? (ppSpace colGt term)? : tactic |
| 248 | +elab_rules : tactic |
| 249 | + | `(tactic| linear_combination'%$tk $[(norm := $tac)]? $[(exp := $n)]? $(e)?) => |
| 250 | + elabLinearCombination' tk tac n e |
| 251 | + |
| 252 | +@[inherit_doc linearCombination'] |
| 253 | +syntax "linear_combination2" (normStx)? (ppSpace colGt term)? : tactic |
| 254 | +elab_rules : tactic |
| 255 | + | `(tactic| linear_combination2%$tk $[(norm := $tac)]? $(e)?) => |
| 256 | + elabLinearCombination' tk tac none e true |
| 257 | + |
| 258 | +end Mathlib.Tactic.LinearCombination' |
0 commit comments