## Stream: metaprogramming / tactics

### Topic: Linear algebra tactic

#### Heather Macbeth (Oct 15 2020 at 15:34):

Do other formalization languages have a tactic to do linear algebra -- taking linear combinations of several given equalities to produce a goal equality? Could linarith be adapted to do this (over a general rather than ordered field)?

I just had to do the following:

example {x y a : ℂ} :
(∃ (k : ℤ), y - a / 2 = 2 * k * a + (x - a / 2) ∨ y - a / 2 = 2 * k * a - (x - a / 2)) ↔
(∃ (k : ℤ), y = 2 * k * a + x ∨ y = (2 * k + 1) * a - x) :=
begin
refine exists_congr (λ k, or_congr ⟨_, _⟩ ⟨_, _⟩),
{ intros h,
field_simp,
ring },
{ rintros rfl,
field_simp,
ring },
{ intros h,
field_simp,
ring },
{ rintros rfl,
field_simp,
ring },
end


and was wishing I was working over the reals, where I could have done

example {x y a : ℝ} :
(∃ (k : ℤ), y - a / 2 = 2 * k * a + (x - a / 2) ∨ y - a / 2 = 2 * k * a - (x - a / 2)) ↔
(∃ (k : ℤ), y = 2 * k * a + x ∨ y = (2 * k + 1) * a - x) :=
begin
refine exists_congr (λ k, or_congr ⟨_, _⟩ ⟨_, _⟩);
exact λ _, by linarith
end


#### Heather Macbeth (Oct 15 2020 at 15:36):

aah, I refined my example so much it no longer makes sense, one sec fixed

#### Yury G. Kudryashov (Oct 15 2020 at 16:13):

If someone will write this tactic, it would be nice to make it handle add_torsors automatically. E.g., by turning every equality in the affine space into an equality in the tangent space. This can be done by subtracting classical.choice point whenever needed.

#### Heather Macbeth (Oct 18 2020 at 17:14):

@Rob Lewis I am still a little curious about this (pinging you because I see you are online). Would this imaginary tactic effectively amount to re-implementing Matlab in Lean? Is it the kind of thing which (at least) should wait til Lean 4?

#### Yury G. Kudryashov (Oct 18 2020 at 17:28):

I guess Lean already has linear programming in linarith, so this should not be (much) harder.

#### Rob Lewis (Oct 18 2020 at 17:29):

This could be done with fairly large modifications to linarith. You need different preprocessing, different certificate generation, a different verification method.

#### Yury G. Kudryashov (Oct 18 2020 at 17:30):

I meant that writing this tactic shouldn't be harder than writing linarith.

#### Rob Lewis (Oct 18 2020 at 17:30):

At a certain point it does start to feel like it's moving toward a computational linear algebra package.

#### Rob Lewis (Oct 18 2020 at 17:31):

Yury G. Kudryashov said:

I meant that writing this tactic shouldn't be harder than writing linarith.

Oh, I wasn't actually responding to your message there, hah. But you're right, it's not much harder and it does share some cod.e

#### Heather Macbeth (Oct 18 2020 at 17:59):

Rob Lewis said:

At a certain point it does start to feel like it's moving toward a computational linear algebra package.

OK, thanks! Would the ideal solution in your mind (not taking into account the amount of work required) for this kind of thing be to outsource to an actual computational linear algebra package (Sage or similar)?

#### Yury G. Kudryashov (Oct 18 2020 at 18:01):

There are much smaller linear algebra packages.

#### Heather Macbeth (Oct 18 2020 at 18:02):

Or numpy, whatever.

#### Heather Macbeth (Oct 18 2020 at 18:02):

Although, I guess what one needs for formal verification is linear algebra over $\mathbb{Q}$?

#### Yury G. Kudryashov (Oct 18 2020 at 18:05):

If we implement linear algebra in Lean, then we can use a custom test for a = 0. E.g., it may work differently in [char_zero] and [char_p] scenarios.

#### Heather Macbeth (Oct 18 2020 at 18:29):

Do Isabelle or Coq have a tactic to do this?

#### Patrick Massot (Oct 18 2020 at 18:54):

I think proof assistants won't be seriously used as long as they are less good at computation than computational linear algebra packages (here I'm talking about small computation, not huge linear algebra needed in numerical analysis). So "moving toward a computational linear algebra package" certainly feels like a good idea.

#### Rob Lewis (Oct 18 2020 at 21:11):

When I said a "computational linear algebra package" I had in mind something like CoqEAL. The idea is, you don't want every algebraic computation to be handled by a one-off tactic with its own method and own data structures. You want to base as much as possible on the same core representations and algorithms. Offloading certifiable stuff to untrusted CAS is one way to partially do this, but you still need to deal with a lot of glue for setting up the problems and verifying the certificates. In principle I think something like CoqEAL can minimize that glue. I'm not sure how much is built on top of it right now.

#### Rob Lewis (Oct 18 2020 at 21:13):

AFAIK CoqEAL does Gaussian elimination/matrix rank computations, which is the core of this problem, but again I don't know off the top of my head whether it's immediately applicable.

#### Rob Lewis (Oct 18 2020 at 21:14):

And there are various other approaches to certified computer algebra out there. I wouldn't be surprised if this particular thing were doable in Isabelle or Coq.

#### Heather Macbeth (Oct 20 2020 at 14:36):

In the medium term, maybe there could be a tactic linear_combination where you provide the coefficients yourself? (Idea borrowed from Mario.) With syntax like this:

import tactic.ring

variables {K : Type*} [field K] [char_zero K]

/-- Desired syntax -/
example {a b : K} (h1 : 2 * a = 4) (h2 : 2 * b = a - b) :
b = 2 / 3 :=
by linear_combination [⟨h1, 1/6⟩, ⟨h2, 1/3⟩]

/-- What it should do -/
example {a b : K} (h1 : 2 * a = 4) (h2 : 2 * b = a - b) :
b = 2 / 3 :=
begin
rw ← sub_eq_zero at h1 h2 ⊢,
rw ← mul_right_inj' (by norm_num : (1:K)/6 ≠ 0) at h1,
rw ← mul_right_inj' (by norm_num : (1:K)/3 ≠ 0) at h2,
{ field_simp,
ring },
{ simp }
end


#### Mario Carneiro (Oct 20 2020 at 15:44):

See also an earlier conversation about this where I propose a ring_rw tactic with similar semantics

#### Heather Macbeth (Oct 20 2020 at 16:21):

Cool! Yes, this ring_rw is very similar to what I am imagining, and would be great. On the other hand, I think the linear-algebra version would be easier than the full ring-theory version, because you really only need equations and coefficients.

#### Mario Carneiro (Oct 20 2020 at 16:23):

the implementation is the same, though, it's not really any easier or harder

#### Mario Carneiro (Oct 20 2020 at 16:23):

the only difference is that the coefficients are variables instead of constants

#### Mario Carneiro (Oct 20 2020 at 16:24):

in fact, as I mention in that thread, you could even substitute into arbitrary functions, not just + and *

#### Mario Carneiro (Oct 20 2020 at 16:25):

I think the hard problem with such generalization is the input grammar for the tactic though

Last updated: May 09 2021 at 22:13 UTC