2 ms·

Thank you thau! Your example is pretty interesting! I avoid using any advanved Mathlib tactic to make the comparison fairer. We are comparing Lean and Litex und

Thank you thau! Your example is pretty interesting! I avoid using any advanved Mathlib tactic to make the comparison fairer. We are comparing Lean and Litex under conditions where they don’t rely too much on external packages, which makes the comparison a bit fairer. (since Lean does have a very rich set of libraries, but building libraries is itself a challenge. Litex really needs to learn from Lean on how to build a successful library!).)(afterall, Litex can also abstract all proofs here and give it a name linear_combination, right?)

thaumasiotes 1y ago
> Your example is pretty interesting! I avoid using any advanved Mathlib tactic to make the comparison fairer. I learned about the `linear_combination` tactic from your example. Other than that, I use `have` and `exact`, which (a) are not advanced, and (b) are also used in your example. Before that, my first attempt at the lean proof looked like this: example (x y : ℝ) (h₁ : 2 * x + 3 * y = 10) (h₂ : 4 * x + 5 * y = 14) : x = -4 ∧ y = 6 := by -- double h₁ to cancel the x term have h₃ : 2 * (2 * x + 3 * y) = 2 * 10 := by rw [h₁] conv at h₃ => ring_nf -- "ring normal form" -- subtract h₂ from h₃ have h₄ : (x * 4 + y * 6) - (4 * x + 5 * y) = 20 - 14 := by rw [h₂, h₃] conv at h₄ => ring_nf conv at h₁ => -- substitute y = 6 into h₁ rw [h₄] ring_nf -- solve for x have h₅ : ((18 + x * 2) - 18) / 2 = (10 - 18) / 2 := by rw [h₁] conv at h₅ => ring_nf apply And.intro h₅ h₄ > We are comparing Lean and Litex under conditions where they don’t rely too much on external packages This proof does have the advantage of not needing to import Mathlib.Tactic. Although again, that's something your proof does.

thaumasiotes 1y ago

> Your example is pretty interesting! I avoid using any advanved Mathlib tactic to make the comparison fairer. I learned about the `linear_combination` tactic from your example. Other than that, I use `have` and `exact`, which (a) are not advanced, and (b) are also used in your example. Before that, my first attempt at the lean proof looked like this: example (x y : ℝ) (h₁ : 2 * x + 3 * y = 10) (h₂ : 4 * x + 5 * y = 14) : x = -4 ∧ y = 6 := by -- double h₁ to cancel the x term have h₃ : 2 * (2 * x + 3 * y) = 2 * 10 := by rw [h₁] conv at h₃ => ring_nf -- "ring normal form" -- subtract h₂ from h₃ have h₄ : (x * 4 + y * 6) - (4 * x + 5 * y) = 20 - 14 := by rw [h₂, h₃] conv at h₄ => ring_nf conv at h₁ => -- substitute y = 6 into h₁ rw [h₄] ring_nf -- solve for x have h₅ : ((18 + x * 2) - 18) / 2 = (10 - 18) / 2 := by rw [h₁] conv at h₅ => ring_nf apply And.intro h₅ h₄ > We are comparing Lean and Litex under conditions where they don’t rely too much on external packages This proof does have the advantage of not needing to import Mathlib.Tactic. Although again, that's something your proof does.