hypotheses of the form A → B → C and A

Stream: new members

[rzeta0]

In Lean I am new to (i) forall quantifiers, and (ii) hypotheses of the form $$A \implies B \imples C$$ .

Consider the following about which I have two questions:

import Mathlib.Tactic

example (ha : m > 5) (hb : ∀ m : ℕ, m > 5 → m > 4 → m > 3) : m > 3 := by
  have h1 : m > 5 → m > 4 → m > 3 := by apply hb
  apply ha at h1 -- < -- doesn't work

Question 1: Do I need to "instantiate" the forall hb into h1 as I have done above, to make it into a form that's usable like most hypotheses without quantifiers?

Quastion 2: I have ha which fulfulls the antecedent of h1 but I don't know how to apply it. My attempt above failed, as have other variations I tried at random.

[Julian Berman]

The simplest way of thinking about forall quantifiers, unless you already are "ingrained" into them from logic and can't shake that off, is to actually pretend they don't exist at all. Specifically, read every forall as simply being a function from one thing to another.

[Julian Berman]

Here you have hb which is a function -- you give it some m : \N and it gives you a proof that m > 5 → m > 4 → m > 3.

[Julian Berman]

Your variables are a bit confusingly named, which might not be helping you -- but the proof that m > 5 → m > 4 → m > 3 should be "that's just hb applied to m"

[Julian Berman]

Here's one proof that starts as you have it:

example (ha : m > 5) (hb : ∀ m : ℕ, m > 5 → m > 4 → m > 3) : m > 3 := by
  have h1 : m > 5 → m > 4 → m > 3 := by apply hb -- but equivalently, this is `hb m`!
  apply h1   -- let's prove h1 instead, which implies the goal
  · exact ha  -- m > 5, that's just ha
  · exact?  -- exact Nat.lt_of_succ_lt ha

[rzeta0]

Thanks - I will study your example.

The Mechanics of Proof teaches us the pattern for "for all" is to apply them eg have h1 : m > 5 → m > 4 → m > 3 := by apply hb but your example of hb m is useful to think about too.

The key was your apply h1 to the current goal which I had missed and should have known already.

[Julian Berman]

Ah. I haven't read it but I'm sure it's great, so yeah I'd fully trust whatever mental model it gives you as well.

[Dan Velleman]

@rzeta0 , returning to your original example, you were confused that apply ha at h1 didn't work. The reason it didn't work is that you should have written apply h1 at ha. That would give you ha : m > 4 → m > 3.

An alternative would be: have h2 : m > 4 → m > 3 := h1 ha. This would leave ha unchanged, but add h2 : m > 4 → m > 3 to the tactic state.

[Dan Velleman]

An alternative to your step

have h1 : m > 5 → m > 4 → m > 3 := by apply hb

would have been

have h1 : m > 5 → m > 4 → m > 3 := hb m

This is using Julian Berman's point that hb is a function, and when you apply that function to m, you get a proof of m > 5 → m > 4 → m > 3. (I disagree with Julian's suggestion that you should pretend that forall quantifiers don't exist. They are important, and you have to use them correctly. But it is helpful to know that, in Lean, a proof of a "for all" statement is a function.) Similarly, h1 is a function, and when you apply it to a proof of m > 5 you get a proof of m > 4 → m > 3. That explains my earlier example have h2 : m > 4 → m > 3 := h1 ha.

To understand all of this, it would be helpful to know about the difference between term-mode proofs and tactic-mode proofs. When you write h : P :=, Lean is expecting a term-mode proof of P. In the examples above, h1 ha and hb m are term-mode proofs. The keyword by tells Lean to switch to tactic mode. In your have h1 line, apply hb is a tactic-mode proof.

Most proofs you write will be in tactic mode. That's why they start with by. But sometimes it is helpful to know how to write very simply term-mode proofs, as in the have examples above. Also, what goes after exact is a term-mode proof. What goes inside the brackets in rw [...] is a term-mode proof. So even if you're mostly going to write tactic-mode proofs, it is helpful to know a little bit about term-mode proofs.

[rzeta0]

Hi Dan - I've been avoiding the tactic-mode vs term-mode discussion as it seemed like an unnecessary rabbit hole. Perhaps I should start looking at it next.

Thanks for your helpful reply.

Sadly I still don't understand why

apply ha at h1

doesn't work. Is there a reasoning that I could get my head around?

In my head applying ha : m > 5 to h1 should fulfil the leftmost antecedent leaving the remainder as a true hypothesis: m > 4 → m > 3.

---

I'm comparing it to a known good example:

import Mathlib.Tactic

example {n : ℕ} (h : n < 5) : n ≠ 5 := by
  apply ne_of_lt at h
  exact h

[Ruben Van de Velde]

That's the wrong way around. Compare the three pairs of equivalent proofs:

import Mathlib.Tactic

example {n : ℕ} (h : n < 5) : n ≠ 5 := by
  apply ne_of_lt at h
  exact h

example {n : ℕ} (h : n < 5) : n ≠ 5 := by
  have h := ne_of_lt h
  exact h

example (ha : m > 5) (hb : ∀ m : ℕ, m > 5 → m > 4 → m > 3) : m > 3 := by
  have h1 : m > 5 → m > 4 → m > 3 := by apply hb
  apply ha at h1 -- < -- doesn't work

example (ha : m > 5) (hb : ∀ m : ℕ, m > 5 → m > 4 → m > 3) : m > 3 := by
  have h1 : m > 5 → m > 4 → m > 3 := by apply hb
  have h1 := ha h1

example (ha : m > 5) (hb : ∀ m : ℕ, m > 5 → m > 4 → m > 3) : m > 3 := by
  have h1 : m > 5 → m > 4 → m > 3 := by apply hb
  apply h1 at ha
  sorry

example (ha : m > 5) (hb : ∀ m : ℕ, m > 5 → m > 4 → m > 3) : m > 3 := by
  have h1 : m > 5 → m > 4 → m > 3 := by apply hb
  have ha := h1 ha
  sorry

[Matt Diamond]

In my head applying ha : m > 5 to h1 should fulfil the leftmost antecedent leaving the remainder as a true hypothesis: m > 4 → m > 3.

FYI there's a tactic called specialize that does what you're describing here

import Mathlib.Tactic

example (ha : m > 5) (hb : ∀ m : ℕ, m > 5 → m > 4 → m > 3) : m > 3 := by
  have h1 : m > 5 → m > 4 → m > 3 := by apply hb
  specialize h1 ha

[Kevin Buzzard]

rzeta0 said:

In my head applying ha : m > 5 to h1 should fulfil the leftmost antecedent leaving the remainder as a true hypothesis: m > 4 → m > 3.

I think the moral of that story is that you are thinking of the word "apply" as a fluid concept, the way it's used as an English word, and not as a precise concept which does exactly two things and only these two things, as it's used in Lean.

If h : P -> Q then apply h turns a goal of Q into a goal of P

If h : P -> Q thenapply h at h2 turns h2 : P into h2 : Q

And that's it. That's what the apply tactic does.

Any other English uses of the word "apply" do not translate into the Lean apply tactic. For example, even though you might be able to "apply" any old fact to anything in English and get another fact via some completely valid logical reasoning, you can never apply h if h isn't of the form P -> Q. This is not like informal reasoning. There are precise rules and you must obey these rules and that's the end of it. You might be able to apply the fact that m > 5 to some informal argument and make a deduction, but you cannot apply it. Ever.

[Dan Velleman]

rzeta0 said:

Sadly I still don't understand why

apply ha at h1

doesn't work. Is there a reasoning that I could get my head around?

This is where it may be helpful to remember that h1 : m > 5 → m > 4 → m > 3 means that h1 is a function, and if you apply the function h1 to a proof of m > 5, then you get a proof of m > 4 → m > 3 . In your situation you also have ha : m > 5, so h1 ha is a proof of m > 4 → m > 3. You always apply a function to an argument; you wouldn't say that you were apply an argument to a function. So in this case you are applying h1 to ha, not the other way around.

This is all an attempt to make what Kevin said easier to remember. If you have h : P -> Q and h2 : P, then h is a function that can be applied to h2 to give you a proof of Q. So it makes sense to apply h to h2, but not the other way around. So you can say apply h at h2, but not apply h2 at h.

[rzeta0]

thanks everyone for the replies - very much appreciated. I will read again in the morning with a coffee.

[rzeta0]

and thanks also @Ruben Van de Velde for your very useful illustrative examples