Linear algebra tactic

Stream: metaprogramming / tactics

[Heather Macbeth]

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,
    rw eq_add_of_sub_eq h,
    field_simp,
    ring },
  { rintros rfl,
    field_simp,
    ring },
  { intros h,
    rw eq_add_of_sub_eq 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]

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

[Yury G. Kudryashov]

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]

@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]

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

[Rob Lewis]

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

[Yury G. Kudryashov]

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

[Rob Lewis]

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

[Rob Lewis]

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]

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]

There are much smaller linear algebra packages.

[Heather Macbeth]

Or numpy, whatever.

[Heather Macbeth]

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

[Yury G. Kudryashov]

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]

Do Isabelle or Coq have a tactic to do this?

[Patrick Massot]

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]

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]

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]

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]

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,
  convert congr (congr_arg has_add.add h2) h1,
  { field_simp,
    ring },
  { simp }
end

[Mario Carneiro]

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

[Heather Macbeth]

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]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Mario Carneiro]

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