How to write proofs without knowing conclusions in advance?

Stream: Is there code for X?

[Terence Tao]

In informal proofs there is a proof style that looks something like this

Assume that proposition P is true.
(run a complicated argument using P as a hypothesis)
We conclude that complicated_conclusion_Q is true.
To summarize, we have shown that P implies complicated_conclusion_Q.
(continue the argument)

In many cases, it is not immediately clear in advance what complicated_conclusion_Q will be; it is something that comes out of the complicated argument.

One way to formalize this sort of thing in Lean is to do something like

have h : P \imp complicated_conclusion_Q by
  intro hp : P
  -- apply a complicated argument
-- continue the argument

but this requires one to know what complicated_conclusion_Q is in advance, or at least to go back and state it early in the proof.

Is there a style of writing in Lean that more closely resembles the informal style mentioned above? Something like this:

  assume hp : P
      -- this introduces hp : P as a hypothesis, and creates a new goal that is something like `_ assuming hp`
      -- run a complicated argument that produces a conclusion hc : complicated_conclusion_Q
     conclude hc -- this closes the assumption goal and inserts a new hypothesis hc : P \imp complicated_conclusion_Q
  -- continuation of the argument

although this proposal would presumably require a major reworking of how Lean manages goals and is not feasible. But is there some other Lean-compatible syntax that could achieve something like this?

[Alex J. Best]

The closest thing I can think of is that you can write a have statement with a named metavariable for your Q
for example

import Mathlib.Tactic
example (h : 50 < x) : 1 < x := by
  have : 10 < x → ?Q := by
    intro h
    -- complicated argument that proves something that will become Q
    have : 5 ≤ 10 := by norm_num
    exact this.trans_lt h
  -- now I have 10 < x → 5 < x in context without having spelt out ahead of time what I was proving

It still requires some knowing in advance what sort of structure you have, and isn't particularly reminiscent of the stream of conciousness style you are after, but if the statement of Q is annoying enough it may be a solution.

[Jireh Loreaux]

The biggest issue with this is that without a goal, many tactics won't work very well or at all (e.g., apply and refine are useless). However, one place where this is certainly relevant is in calculations, and with those it would be extremely simple to support this framework. Note, that there isn't really a need for named metavariables necessarily. The reason this works is that in a calc proof, you are incrementally providing the new goals to Lean, so it never has to guess. For an oversimplified toy example:

import Mathlib.Data.Real.Basic

example (x : ℝ) : 0 ≤ 1 + x ^ 2 := by
  have key₁ := fun hx : 0 ≤ x ↦ calc
    0 ≤ x * x     := mul_nonneg hx hx
    _ ≤ 0 + x ^ 2 := by simp [sq]
    _ ≤ 1 + x ^ 2 := by gcongr; norm_num
  have key₂ := fun hx : x ≤ 0 ↦ calc
    0 ≤ x * x     := mul_nonneg_of_nonpos_of_nonpos hx hx
    _ ≤ 0 + x ^ 2 := by simp [sq]
    _ ≤ 1 + x ^ 2 := by gcongr; norm_num
  by_cases h : 0 ≤ x
  · exact key₁ h
  · push_neg at h
    exact key₂ h.le

In these calc proofs above, you can just keep adding lines, and the type of the established key₁ or key₂ is updated accordingly (although of course that would break the remainder of the proof I have provided, but that's irrelevant).

[Terence Tao]

Alex J. Best said:

The closest thing I can think of is that you can write a have statement with a named metavariable for your Q
for example

Thanks, this basically does what I wanted! in general, the syntax would be

have hPQ: P →  ?Q := by
  intro hP
  -- run a complicated argument to conclude a conclusion hQ : Q
  exact hQ

and this will add a hypothesis hPQ: P → Q without having to ever write down Q explicitly. The only additional thing perhaps is to add some syntactic sugar to replace the first two lines have hPQ: P → ?Q := by and intro hP by something shorter such as suppose P (given that assume is already taken), but otherwise this feels like a satisfactory solution.

[Terence Tao]

There is also the variant

have h : ?Q := by
  -- run a complicated argument to conclude a conclusion hQ : Q
  exact hQ

where one starts a stream-of-consciousness argument, perhaps not knowing in advance exactly where one will end up, until one reaches a satisfactory conclusion and declares victory, producing a new hypothesis h:Q as a result. (The point being that any intermediate facts produced in the course of establishing hQ pass out of scope when closing the have h block, so that the tactic state is conceptually cleaner.)

[Heather Macbeth]

Jireh Loreaux said:

The biggest issue with this is that without a goal, many tactics won't work very well or at all (e.g., apply and refine are useless).

I think a closely related issue, if not actually the same issue, is that the tactic language definitely has a preference for backward reasoning over forward reasoning. Maybe it's worth thinking through what tactics do work purely on hypotheses:

• rw [...] at h
• normalization tactics like ring_nf at h, norm_num at h, norm_cast at h, ...
• have := congr(1 + $h1 + $h2 * $h3)
• specialize, obtain/rcases, ...

[Heather Macbeth]

There are other forward-reasoning tactics which you could imagine existing:

• @Alex J. Best weren't you working on a "factor" tactic?
• for teaching I have a hacky "cancel" tactic which e.g. simplifies a hypothesis $(x ^ 2 + 3)a<(x^2+3)b$ to $a<b$

[Heather Macbeth]

• @Scott Morrison has proposed an "isolate x" tactic which takes an equation whose LHS is a complicated expression involving x and reorganizes it so that x is alone on the LHS

[Jireh Loreaux]

@Adam Topaz just wrote apply ... at h, but it hasn't been merged yet: #7527

[Vincent Beffara]

One can always combine the first two lines have and intro into one:

example : True := by
  have key_step {n : Nat} (hP : n < 1) : ?Q := by
    rw [Nat.lt_one_iff] at hP
    exact hP
  tauto

[Terence Tao]

Heather Macbeth said:

I think a closely related issue, if not actually the same issue, is that the tactic language definitely has a preference for backward reasoning over forward reasoning. Maybe it's worth thinking through what tactics do work purely on hypotheses:

A preference is fine, so long as contrary preferences are supported by the software, with only mild aesthetic and logistical costs. But it seems Lean4 is in fact expressive enough to support forward reasoning as well as backwards (or various combinations of the two); it's just that the tools for doing so are not as well documented or developed always.

[Alex J. Best]

Heather Macbeth said:

• Alex J. Best weren't you working on a "factor" tactic?

Yes I think there is a lot of potential for "put this element in a form with X property" tactics, I just got a bit interrupted by the Lean 4 switch but hope to get back to them, one could imagine e.g. factoring polynomials, some matrix decompositions / normal forms, sums of squares for proving positivity etc. etc. One thing that one also needs doing for most proofs using these forms though is also introducing the properties they have, there is no point factoring polynomials if there is no good way to prove those factors irreducible. This seems to require some more domain specific thought to find and verify good certificates of such properties though.

[Patrick Massot]

If you work on sos then you should coordinate with Rob who may have a student working on this.

[Miguel Marco]

Alex J. Best said:

One thing that one also needs doing for most proofs using these forms though is also introducing the properties they have, there is no point factoring polynomials if there is no good way to prove those factors irreducible.

Automatically factoring expressions can be very useful even if you don't have the proof that the factors are irreducible. For example, for proving (in)equalities. A toy example could be:

example (a b c : ℤ  ) :  0 ≤  16 * a ^ 2 * c ^ 2 - 48 * a * c ^ 3 + 36 * c ^ 4 + 8 * a * c ^ 2 - 12 * c ^ 3  + c ^ 2:= by
  factor
  -- goal becomes  0 ≤ (6 * c ^ 2 - 4 * a * c - c) ^ 2
  apply sq_nonneg

[Kevin Buzzard]

I suspect that the least painful way to make this kind of tactic is to go down the polyrith route -- farm the polynomial out to SageMath, ask it nicely to factor it, and then check its answer using ring. @Eric Wieser or @Mario Carneiro -- how easy is such a tactic to write, given that we must already have a bunch of machinery needed to make the bridge?

[Eric Wieser]

The polyrith route isn't ideal because it isn't something we can actually commit to mathlib (as it needs a network connection)

[Kevin Buzzard]

I mean "write a new tactic like polyrith which factors stuff". That should be OK, right?

[Eric Wieser]

Yes, that ought to be very doable

[Eric Wieser]

Probably it would make sense to adapt the existing polyrith infrastructure rather than try to write a new copy from scratch

[Miguel Marco]

Maybe some partial factorizations can be done inside Lean without too much pain. For example, the squarefree factorization for univariate polynomials requires only to compute derivatives and extended euclidean algorithm. For the multivariate case, you have to reduce to one variable and then do Hensel lifting (which basically involves linear algebra).

If you want to go farther, you have to reduce modulo a prime, factor there and then do Hensel lifting again and rational reconstruction. That can be a bit tricky.

Another option would be to use a local installation of Sage (or your favourite CAS).

[Kevin Buzzard]

yeah you could definitely do some stuff in Lean, but I imagine it would be quite a challenging project. I suspect that the "use the internet" approach would be much easier in practice (but attach a low significance to my imagining because I know essentially nothing about writing tactics).

[Kevin Buzzard]

One has to look at the practicalities here, and basically when am I using Lean and not connected to the internet? "between stations on the Picadilly line" was the answer to this a year or two ago, but now they're talking about WiFi between stations so even that won't be happening soon.