1
$\begingroup$

I was wondering how can one reason backwards in Lean 4, starting from an existentially quantified conclusion.

I know that I can reason about an existentially quantified variable in a hypothesis using obtain as follows:

-- ...
have h : ∃ a : ℤ, a ^ 2 + 2 * a + 1 = 9 := by sorry
obtain ⟨x,hx⟩ := h
--  ...

But sometimes, I wanted to reason about an existential variable in the conclusion part of the property. For example,

example : ∃ a : ℤ, a ^ 2 + 2 * a + 1 = 9 := by
  sorry

I wanted to reason that assuming such an a exists, say it is x, then

(x + 1) ^ 2 = 9

and then ... x = 2.

Then, after all this backward reasoning, one could say:

-- ...
use 2
-- ...

So, how can I express the idea "assuming that the conclusion holds" or "assuming such a thing exists"?

-- Update --

@Jason Rute's answer helped. But I think I didn't express my intent clearly. I wanted to assume that the conclusion holds, then obtain some necessary (but not sufficient) conditions to help me make guesses in the proof assistant. So, if the such a thing exists, it must satisfy P. But I understand that the other direction of the implication doesn't hold.

So, all this is trying to writing down the guesswork in the PA. In a slightly modified example below, I tried to infer the necessary condition in a naive/incorrect way (as I am only beginning to learn lean 4). Hopefully, this expresses the intent: I assume the goal g holds by sorry, and then infer properties for making guesses. My naive example may have used some tactics from The Mechanics of Proof:

example : ∃ a : ℕ, a ^ 2 + 2 * a + 1 ≤ 9 := by
  have g : ∃ a : ℕ, a ^ 2 + 2 * a + 1 ≤ 9 := by sorry
  obtain ⟨x, hx⟩ := g
  have h1 : (x + 1) ^ 2 ≤ 3 ^ 2
  · calc (x + 1) ^ 2
      _ = x ^ 2 + 2 * x + 1  := by ring
      _ ≤ 9  := hx
      _ = 3 ^ 2 := by ring
  cancel 2 at h1
  -- h1 : x + 1 ≤ 3
  use 2
  numbers

So, the point is, I can infer that if the conclusion g holds, then $x+1 \leq 3$

This guesswork narrows down the solution space from N to {0,1,2}. And I understand that it's still guesswork. There is no guarantee that if I choose from {0,1,2}, the conclusion will hold. The only guarantee is that if I choose outside of {0,1,2}, it can't hold. And I still need to use 0, use 1 or use 2 and verify the conclusion.

So, how should one write down this kind of guesswork formally in Lean (instead of using paper and pencil)?

My naive way doesn't look very good, because it has a sorry in it, and is probably incomplete.

$\endgroup$

2 Answers 2

1
$\begingroup$

First, one needs to be careful with backwards reasoning. In general, it isn't valid to reason from a conclusion (despite how we often teach algebra and calculus). For a dumb example,

$$ \begin{align} x + 1 & = x \\ x (x+1) & = x^2 \qquad\text{(multiply both sides by $x$)}\\ x^2 + x &= x^2 \\ x &= 0 \qquad\text{(subtract $x^2$ from both sides)} \end{align} $$

The problem is that we actually need the implications to go from the bottom to the top, and that isn't true of $x(x+1) = x^2 \rightarrow x + 1 = x$. The other steps are ok since they are bidirectional implications.

Of course, Lean won't let you make mistakes like this. rewrite and simp are the way one normally does this sort of "backwards" reasoning since you have to use equality or iff rules which go both ways.

As for $\exists$, in theory, one should be able to get tactics to work under the $\exists$ binder. (Specifically, if $P(a) \rightarrow Q(a)$ then $(\exists a, P(a)) \rightarrow (\exists a, Q(a))$.) However, in practice, it seems more difficult to apply Lean tactics under a binder. I've found that simp (and its variants) work somewhat reliably (but not perfectly), while say rewrite doesn't work at all.

So here are some things you can do:

example : ∃ a : ℤ, a ^ 2 + 2 * a + 1 = 9 := by
  have h (x : ℤ) : x^2 + 2 * x + 1 = (x + 1)^2 := by ring
  -- rewrite (using simp) with an equality
  simp [h]
  have h2 (x : ℤ ) : x = 9 <-> x = 3^2 := by ring_nf
  -- rewrite (using simp) with an iff
  simp [h2]
  /-
  h : ∀ (x : ℤ), x ^ 2 + 2 * x + 1 = (x + 1) ^ 2
  h2 : ∀ (x : ℤ), x = 9 ↔ x = 3 ^ 2
  ⊢ ∃ a, (a + 1) ^ 2 = 3 ^ 2
  -/

Of course, it is also just possible to do the reasoning on pen and paper and then plug in the value (2 in this case) into Lean. By front-loading the witness use 2, you eliminate the challenges of working under a binder.

If you find that Lean helps you work through the problem, you could also work with the universally quantified version in tactic mode like follows to figure out the answer. Then you can plug that answer in upfront.

-- scratch work using the universally quantified version
example (a : ℤ) : a ^ 2 + 2 * a + 1 = 9 := by
  have h (x : ℤ) : x^2 + 2 * x + 1 = (x + 1)^2 := by ring
  rw [h]
  have h2 (x : ℤ ) : x = 9 <-> x = 3^2 := by ring_nf
  rw [h2]
  have h3 (x : ℤ) (y : ℤ) : x^2 = y^2 <-> (x = y ∨ x = -y) := sq_eq_sq_iff_eq_or_eq_neg
  rw [h3]
  /-
  a : ℤ
  h : ∀ (x : ℤ), x ^ 2 + 2 * x + 1 = (x + 1) ^ 2
  h2 : ∀ (x : ℤ), x = 9 ↔ x = 3 ^ 2
  h3 : ∀ (x y : ℤ), x ^ 2 = y ^ 2 ↔ x = y ∨ x = -y
  ⊢ a + 1 = 3 ∨ a + 1 = -3
  -/

Edit: The above scratch work is for finding sufficient conditions on a for a ^ 2 + 2 * a + 1 = 9 to hold. But if instead (like the OP is asking), you want to derive consequences of having such an a, then that is easy too. Just put that assumption on a in the hypotheses:

example (a : ℤ) (h : a ^ 2 + 2 * a + 1 = 9) : |a| <= 4 := by
  have h2 : (a + 1)^2 <= 3^2 := calc
    (a + 1)^2 = a ^ 2 + 2 * a + 1 := by ring
    _         = 9                 := h
    _        <= 3^2               := by simp
  have h3 : |a + 1| <= |3| := by
    rw [sq_le_sq] at h2
    assumption
  calc
    |a| <= |1| + |1+a| := by apply abs_add'
    _    = 1 + |a + 1| := by simp [Int.add_comm]
    _   <= 1 + |3|     := by exact Int.add_le_add_left h3 1
    _    = 4           := rfl

Of course, when you start, you may not know what you are proving. That is fine. Just make the conclusion False and use have to explore short-term consequences. I would strongly recommend that you avoid putting your scratch work inside the theorem you are trying to prove (by adding your conclusion as a hypothesis). At best it is confusing. At worst, you may assume your goal like the OP is doing above, and then accidentally prove it with a powerful tactic. If you really want to put the scratch work in the main theorem, I would say do it as a have-lemma like this:

example : ∃ a : ℤ, a ^ 2 + 2 * a + 1 = 9 := by
  have scratch (x : ℤ) (h : x ^ 2 + 2 * x + 1 = 9) : False := by
    -- scratch work goes here
  -- main proof here
$\endgroup$
2
  • $\begingroup$ Thanks a lot for your help. I understand that what the conclusion implied is only a necessary condition (not sufficient condition). I only wanted to use the necessary condition for guesswork for the evidence. Please see my update. $\endgroup$
    – tinlyx
    Commented Jun 13 at 16:54
  • $\begingroup$ @tinlyx I edited my answer. $\endgroup$
    – Jason Rute
    Commented Jun 13 at 20:49
1
$\begingroup$

If the goal is ∃ a, P a and you want to observe that any a's satisfying P a must also satisfy Q a, why not do precisely that? As follows:

have someObservation := ∀ a, P a → Q a := by ...

Here is how it applies to your example:

example: ∃ a : ℕ, a ^ 2 + 2 * a + 1 ≤ 9 := by
  -- tan abbreviation for the property in question
  let P (a : ℕ) := a ^ 2 + 2 * a + 1 ≤ 9
  -- any solution satisfies (a + 1) ^ 2 ≤ 3 ^ 2
  have h2 : ∀ a, P a → (a + 1) ^ 2 ≤ 3 ^ 2 := by
    intro x Px
    calc (x + 1) ^ 2
      _ = x ^ 2 + 2 * x + 1 := by ring
      _ ≤ 9 := Px
      _ = 3 ^ 2 := by rfl
  -- any solution satisfies (a + 1) ≤ 3
  have h3 : ∀ a, P a → (a + 1) ≤ 3 := by
    intro x Px
    apply (@Nat.pow_le_pow_iff_left (x + 1) 3 2 (by simp)).1
    apply h2 x Px
  -- by h3, if there is a solution, it is 0, 1, or 2
  use 2
  simp
$\endgroup$
3
  • $\begingroup$ Doesn't use 2; simp just work? What's the utility of the haves? $\endgroup$ Commented Jun 14 at 5:56
  • 1
    $\begingroup$ I am tempted to ask whether you read the question. The OP would like to know, given a goal ∃ a, P a, how to make observations of the sort "every solution a must satisfy Q a". Doing this with have is reasonable, and since they OP is already using them, I followed suit. (I do not necesarily think this is a useful way of formalizing things, and in fact Lean tells me I have unused haves.) $\endgroup$ Commented Jun 14 at 10:39
  • $\begingroup$ I had read the question. My understanding was that the OP wanted to gradually refine the conclusion to help reasoning. Schematically, instead of proving $P \to Q$, prove that $P \to Q \land R$ where it is known that $P \to R$. $\endgroup$ Commented Jun 20 at 16:39

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.