Zulip Chat Archive

Stream: metaprogramming / tactics

Topic: Linear algebra tactic


view this post on Zulip 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,
    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

view this post on Zulip Heather Macbeth (Oct 15 2020 at 15:36):

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

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Yury G. Kudryashov (Oct 18 2020 at 17:30):

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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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)?

view this post on Zulip Yury G. Kudryashov (Oct 18 2020 at 18:01):

There are much smaller linear algebra packages.

view this post on Zulip Heather Macbeth (Oct 18 2020 at 18:02):

Or numpy, whatever.

view this post on Zulip Heather Macbeth (Oct 18 2020 at 18:02):

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

view this post on Zulip 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.

view this post on Zulip Heather Macbeth (Oct 18 2020 at 18:29):

Do Isabelle or Coq have a tactic to do this?

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Mario Carneiro (Oct 20 2020 at 16:23):

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

view this post on Zulip Mario Carneiro (Oct 20 2020 at 16:23):

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

view this post on Zulip 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 *

view this post on Zulip 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