How does one actually construct proofs without using "by"?

Stream: new members

[Ching-Tsun Chou]

In #mil there are many proofs without using "by". Some good examples can be found in:

https://leanprover-community.github.io/mathematics_in_lean/C10_Topology.html#convergence-and-continuity

But I can never understand how one actually construct such proofs. When one does a tactic proof using "by", one can look at the tactic state to know where one stands and the tactic state often suggests what one should do next. But when one does not use tactics, how does one get such feedbacks? Personally I find that the only non-tactic proof step I am capable of doing is to apply modus ponens or specialize a universal quantifier (which of course are the same thing in Lean). Even when doing so, I find that I have to use the "have" tactic so that I can keep the proof result in the tactic state to look at. Furthermore, when I read a tactic proof, I can move my cursor around in the proof and look at the tactic states to get an idea of how the proof progresses. Is there any such feedback in a non-tactic proof?

[Riccardo Brasca]

At the beginning I suggest to just write tactic proofs. With some experience you will be able to write term proofs more and more complicated. And of course one can always "cheat" writing a tactic mode proof and later realizing that it can be written in term mode.

[Riccardo Brasca]

But there is nothing better with term mode proofs (unless you are writing a definition, then things are a little different)

[Kevin Buzzard]

The way I usually construct a non-tactic proof is that I construct a tactic proof, realise that the tactic proof has no rw or simp and is just refine, apply, exact, use etc, and then I just refactor the proof into a term mode proof making liberal use of "holes" (i.e. _, which gives an error, and clicking on the error tells you the goal which is supposed to go in the hole).

[Michael Stoll]

(And in some cases, rw can be replaced by a term with ▸.)

[Kevin Buzzard]

Here's the first example in the link above:

import Mathlib

open Filter Topology

variable (X : Type) [MetricSpace X]

-- step 1: search the library
example {u : ℕ → X} {a : X} :
    Tendsto u atTop (𝓝 a) ↔ ∀ ε > 0, ∃ N, ∀ n ≥ N, dist (u n) a < ε := by
  exact? -- surely this is in the library

-- step 2: click on the output of `exact?`
example {u : ℕ → X} {a : X} :
    Tendsto u atTop (𝓝 a) ↔ ∀ ε > 0, ∃ N, ∀ n ≥ N, dist (u n) a < ε := by
  exact Metric.tendsto_atTop -- That's a tactic proof

-- step 3: "by" switches from term mode to tactic mode, and `exact` switches from
-- tactic mode to term mode, so `by exact` just cancel each other out
example {u : ℕ → X} {a : X} :
    Tendsto u atTop (𝓝 a) ↔ ∀ ε > 0, ∃ N, ∀ n ≥ N, dist (u n) a < ε :=
  Metric.tendsto_atTop -- term mode proof

[Kevin Buzzard]

import Mathlib

-- tactic proof
example : ∃ n : ℕ, n = 4 := by
  use 4

-- but `use x` is just `refine ⟨x, ?_⟩`
example : ∃ n : ℕ, n = 4 := by
  refine ⟨4, ?_⟩
  -- ⊢ 4 = 4
  rfl

-- but `?_` left a hole, and `rfl` filled it, so just slot it in
example : ∃ n : ℕ, n = 4 := by
  refine ⟨4, rfl⟩

-- `refine` with no holes is `exact`
example : ∃ n : ℕ, n = 4 := by
  exact ⟨4, rfl⟩

-- `by` and `exact` cancel out

example : ∃ n : ℕ, n = 4 := ⟨4, rfl⟩

[Ted Hwa]

To me, it doesn't seem like there's much point in trying to construct complicated term-mode proofs. As others have said, almost certainly you start with a tactic proof first, and then "golf" it into a term-mode proof to minimize the length of the proof. This doesn't seem very interesting to me, but people seem to like to do it with Lean.

[Kevin Buzzard]

In early parts of the library if there's a one-line term proof people will use it: it costs some time to enter tactic mode, and why pay that time thousands of times per day with CI on github? We're paying for the machines which are compiling the code. In later parts of the library you'll find many tactic mode proofs, because things get more complicated. Typically you get a definition, some cute one-liners in the basic API, and then tactic mode for the more complex stuff.

[Kevin Buzzard]

But I agree, there's not much point in making complex term-mode proofs. Sometimes I start a proof in term mode, and only switch to tactic mode at the point where I need a high-powered tactic like simp, norm_num, linarith, ring etc.

[Kevin Buzzard]

e.g.

example : ∃ x : ℝ, x ^ 2 - 3 * x + 2 = 0 := ⟨2, by norm_num⟩

[Kevin Buzzard]

import Mathlib

example (P Q R : Prop) (h1 : P → Q → R) (h2 : P → Q) : P → R := by
  intro hP
  apply h1
  · exact hP
  · apply h2
    exact hP

example (P Q R : Prop) (h1 : P → Q → R) (h2 : P → Q) : P → R := by
  intro hP
  refine h1 ?_ ?_
  · exact hP
  · refine h2 ?_
    exact hP

example (P Q R : Prop) (h1 : P → Q → R) (h2 : P → Q) : P → R := by
  intro hP
  refine h1 ?_ ?_
  · exact hP
  · exact h2 hP

example (P Q R : Prop) (h1 : P → Q → R) (h2 : P → Q) : P → R := by
  intro hP
  refine h1 hP (h2 hP)

example (P Q R : Prop) (h1 : P → Q → R) (h2 : P → Q) : P → R := by
  intro hP
  exact h1 hP <| h2 hP

example (P Q R : Prop) (h1 : P → Q → R) (h2 : P → Q) : P → R :=
  fun hP ↦ h1 hP <| h2 hP

[Ching-Tsun Chou]

For Kevin's last example, I would just write "by tauto". Once I know the goal follows by purely propositional reasoning from the premises, I cease to be interested in the details of the reasoning.

[Kevin Buzzard]

Sure, but I was answering the question "how do you turn a tactic proof into a term proof" and with high-powered tactics the answer is "that's pretty tricky"

[Kevin Buzzard]

import Mathlib

example (P Q R : Prop) (h1 : P → Q → R) (h2 : P → Q) : P → R := by show_term tauto

example (P Q R : Prop) (h1 : P → Q → R) (h2 : P → Q) : P → R := fun a =>
  have := Classical.propDecidable
  Or.casesOn (Decidable.not_or_of_imp h1)
    (fun h => Or.casesOn (Decidable.not_or_of_imp h2) (fun h_1 => absurd a h) fun h_1 => absurd a h)
    fun h =>
    Or.casesOn (Decidable.not_or_of_imp h2) (fun h => absurd a h) fun h_1 =>
      Or.casesOn (Decidable.not_or_of_imp h) (fun h => absurd h_1 h) fun h => h

[Notification Bot]

This topic was moved here from #maths > How does one actually construct proofs without using "by"? by Patrick Massot.

[Patrick Massot]

All this is true, but we should also answer the original question. You can write term mode proofs interactively without using tactic mode by simply using underscores and reading Lean’s messages.

[Patrick Massot]

@Ching-Tsun Chou note I moved your message that had nothing to do with the channel where you originally posted it.

[Patrick Massot]

In Kevin’s example, you would start with example : ∃ n : ℕ, n = 4 := ⟨_, _⟩, look at what Lean wants on the first underscore, fill-in the 4, then look at the message on the second underscore, fill in the rfl.

[Ching-Tsun Chou]

Thanks for pointing out the "_" technique. However, I'm not sure how well it works in practice. Consider the following example from #mil sec.10.2.1:

example {X Y : Type*} [MetricSpace X] [MetricSpace Y] {f : X → Y} (hf : Continuous f) :
    Continuous fun p : X × X ↦ dist (f p.1) (f p.2) :=
  Continuous.comp continuous_dist _

When I put my cursor on the "_", I see the following message:

type mismatch
Continuous.comp continuous_dist ?m.33228
has type
Continuous ((fun p ↦ dist p.1 p.2) ∘ ?m.32923) : Prop
but is expected to have type
Continuous fun p ↦ dist (f p.1) (f p.2) : Prop

It seems that I am none the wiser.

[Kevin Buzzard]

Well then hop into tactic mode and try refine Continuous.comp continuous_dist ?_ and see if you get luckier.

[Kevin Buzzard]

Unfortunately higher order unification is undecidable, so you can't expect it to work every time :-)

[Kyle Miller]

If you read the type mismatch, it says that it can't see how the function is a composition. You could try giving _ a type ascription to help it out, or you could start with a show term to change the expected type to display a composition.

[Kyle Miller]

example {X Y : Type*} [MetricSpace X] [MetricSpace Y] {f : X → Y} (hf : Continuous f) :
    Continuous fun p : X × X ↦ dist (f p.1) (f p.2) :=
  show Continuous ((fun q : Y × Y ↦ dist q.1 q.2) ∘ fun p : X × X ↦ (f p.1, f p.2)) from
  Continuous.comp continuous_dist _

[Kyle Miller]

example {X Y : Type*} [MetricSpace X] [MetricSpace Y] {f : X → Y} (hf : Continuous f) :
    Continuous fun p : X × X ↦ dist (f p.1) (f p.2) :=
  Continuous.comp continuous_dist (_ : Continuous fun p : X × X ↦ (f p.1, f p.2))

[Ching-Tsun Chou]

I'm afraid that the conclusion I draw from this discussion is that I should stick to tactic proofs. The term proofs are just too hard for me and I'm not sure what is to be gained from not using tactics.

[Ruben Van de Velde]

That's absolutely fine!

[Kyle Miller]

As an exercise, it would be worth writing a tactic proof for this example. (I think you happened to choose an example that's challenging to do step-by-step no matter what modality you choose to use!)

[Michael Rothgang]

Kevin Buzzard said:

In early parts of the library if there's a one-line term proof people will use it: it costs some time to enter tactic mode, and why pay that time thousands of times per day with CI on github? We're paying for the machines which are compiling the code. In later parts of the library you'll find many tactic mode proofs, because things get more complicated. Typically you get a definition, some cute one-liners in the basic API, and then tactic mode for the more complex stuff.

One addition about golfing: as I've understood it, the point of golfing is not "as short as possible", but rather "if nothing mathematically interesting happens, you can golf it". If a proof was interesting, it's nicer to keep it readable, so it's easier to change or fix in the future.

[Ching-Tsun Chou]

Kyle Miller said:

As an exercise, it would be worth writing a tactic proof for this example. (I think you happened to choose an example that's challenging to do step-by-step no matter what modality you choose to use!)

The example is taken from #mil sec.10.2.1 where a tactic proof is also given:

https://leanprover-community.github.io/mathematics_in_lean/C10_Topology.html#convergence-and-continuity

Unsurprisingly, the tactic proof is more transparent and I can move my cursor in the proof to see all the intermediate proof states. But I thought I should learn how the non-tactic proofs could be constructed.

[Mario Carneiro]

Kevin Buzzard said:

example (P Q R : Prop) (h1 : P → Q → R) (h2 : P → Q) : P → R := by show_term tauto

By the way, by show_term has a shorthand which is by?

[Kyle Miller]

Ching-Tsun Chou said:

I can move my cursor in the proof to see all the intermediate proof states

That's not unique to tactic proofs. In terms, you can move your cursor around and see expected types.

The tactic proof that's given by the way is analogous to the term proof that immediately follows it. Continuous.dist has much better properties for this particular proof than Continuous.comp.

[Ching-Tsun Chou]

Thanks for pointing out expected types.

I used Continuous.comp because the first term proof given is:

example {X Y : Type*} [MetricSpace X] [MetricSpace Y] {f : X → Y} (hf : Continuous f) :
    Continuous fun p : X × X ↦ dist (f p.1) (f p.2) :=
  continuous_dist.comp ((hf.comp continuous_fst).prod_mk (hf.comp continuous_snd))

Removing the first anonymous projection notation, the proof term becomes:

  Continuous.comp continuous_dist ((hf.comp continuous_fst).prod_mk (hf.comp continuous_snd))

Right?

[Kyle Miller]

Yes, that is the first proof term given, and that is equivalent. I'm just saying that this proof term is particularly delicate, and it's no wonder that the tactic proof uses a completely different approach.

[Daniel Weber]

If you want to practice term-mode proofs the first few chapters of #tpil have many exercises

[Patrick Massot]

You chose a complicated example for reasons explained by others here. If you want to try some more I recommend trying:

import Mathlib.Topology.MetricSpace.Basic

def continuous_function_at (f : ℝ → ℝ) (x₀ : ℝ) :=
∀ ε > 0, ∃ δ > 0, ∀ x, |x - x₀| ≤ δ → |f x - f x₀| ≤ ε

def sequence_tendsto (u : ℕ → ℝ) (l : ℝ) :=
∀ ε > 0, ∃ N, ∀ n ≥ N, |u n - l| ≤ ε

example (f : ℝ → ℝ) (u : ℕ → ℝ) (x₀ : ℝ)
    (hf : continuous_function_at f x₀) (hu : sequence_tendsto u x₀) :
    sequence_tendsto (f ∘ u) (f x₀) :=
  fun ε ε_pos ↦ (sorry)

Put your cursor before the sorry and Lean will tell you the context and what is expected here. Then replace sorry with (hf sorry sorry).elim (sorry) and start thinking about what to put instead of those three new sorries. And continue until the proof is complete.

[Patrick Massot]

Solution

example (f : ℝ → ℝ) (u : ℕ → ℝ) (x₀ : ℝ)
    (hf : continuous_function_at f x₀) (hu : sequence_tendsto u x₀) :
    sequence_tendsto (f ∘ u) (f x₀) :=
  fun ε ε_pos ↦ (hf ε ε_pos).elim
   fun δ ⟨δ_pos, hδ⟩ ↦ (hu δ δ_pos).elim
     fun N hN ↦ ⟨N, fun n n_ge ↦ hδ (u n) <| hN n n_ge⟩

[Michael Stoll]

(You need to use "```lean4" in the spoiler block to get correct code formatting.)

[Ching-Tsun Chou]

I can't really do it. The only way I could come up with a proof term is by doing a tactic proof first and then translating it into a proof term:

example (f : ℝ → ℝ) (u : ℕ → ℝ) (x₀ : ℝ)
    (hf : continuous_function_at f x₀) (hu : sequence_tendsto u x₀) :
    sequence_tendsto (f ∘ u) (f x₀) := by
  intro ε ε_pos
  have ⟨δ, δ_pos, hf'⟩ := hf ε ε_pos
  have ⟨N, hu'⟩ := hu δ δ_pos
  use N
  intro n n_N
  have h1 := hu' n n_N
  exact hf' (u n) h1

example (f : ℝ → ℝ) (u : ℕ → ℝ) (x₀ : ℝ)
    (hf : continuous_function_at f x₀) (hu : sequence_tendsto u x₀) :
    sequence_tendsto (f ∘ u) (f x₀) :=
  fun ε ε_pos ↦ (
    have ⟨δ, δ_pos, hf'⟩ := hf ε ε_pos
    have ⟨N, hu'⟩ := hu δ δ_pos
    ⟨N, fun n n_N ↦ (
      have h1 := hu' n n_N
      have h2 := hf' (u n) h1
      show |(f ∘ u) n - f x₀| ≤ ε from h2
      )
    ⟩
  )

I still have no idea how you could come up with your solution without a known tactical proof to guide you.

[Mario Carneiro]

Here's a proof I just did of this example, pausing at each step where I had to look at the goal view (usually at the holes, but also paging around the lines like one does in a tactic proof as well):

variable (f : ℝ → ℝ) (u : ℕ → ℝ) (x₀ : ℝ)
  (hf : continuous_function_at f x₀) (hu : sequence_tendsto u x₀)
include hf hu

example : sequence_tendsto (f ∘ u) (f x₀) :=
  fun ε ε_pos ↦
    have := hf _ _
    sorry

example : sequence_tendsto (f ∘ u) (f x₀) :=
  fun ε ε_pos ↦
    have := hf _ ε_pos
    _

example : sequence_tendsto (f ∘ u) (f x₀) :=
  fun ε ε_pos ↦
    have ⟨δ, δ_pos, hδ⟩ := hf _ ε_pos
    _

example : sequence_tendsto (f ∘ u) (f x₀) :=
  fun ε ε_pos ↦
    have ⟨δ, δ_pos, hδ⟩ := hf _ ε_pos
    have := hδ _ _
    _

example : sequence_tendsto (f ∘ u) (f x₀) :=
  fun ε ε_pos ↦
    have ⟨δ, δ_pos, hδ⟩ := hf _ ε_pos
    have : |f (u x) - _| ≤ _ := hδ _ _
    _

example : sequence_tendsto (f ∘ u) (f x₀) :=
  fun ε ε_pos ↦
    have ⟨δ, δ_pos, hδ⟩ := hf _ ε_pos
    have (x) : |f (u x) - _| ≤ _ := hδ _ _
    _

example : sequence_tendsto (f ∘ u) (f x₀) :=
  fun ε ε_pos ↦
    have ⟨δ, δ_pos, hδ⟩ := hf _ ε_pos
    have := hu _ _
    have (n) : |f (u n) - _| ≤ _ := hδ _ _
    _

example : sequence_tendsto (f ∘ u) (f x₀) :=
  fun ε ε_pos ↦
    have ⟨δ, δ_pos, hδ⟩ := hf _ ε_pos
    have ⟨N, hN⟩ := hu _ δ_pos
    have (n) : |f (u n) - _| ≤ _ := hδ _ _
    _

example : sequence_tendsto (f ∘ u) (f x₀) :=
  fun ε ε_pos ↦
    have ⟨δ, δ_pos, hδ⟩ := hf _ ε_pos
    have ⟨N, hN⟩ := hu _ δ_pos
    have (n) : |f (u n) - _| ≤ _ := hδ _ _
    ⟨N, fun n hn => _⟩

example : sequence_tendsto (f ∘ u) (f x₀) :=
  fun ε ε_pos ↦
    have ⟨δ, δ_pos, hδ⟩ := hf _ ε_pos
    have ⟨N, hN⟩ := hu _ δ_pos
    ⟨N, fun n hn =>
      hδ _ _⟩

example : sequence_tendsto (f ∘ u) (f x₀) :=
  fun ε ε_pos ↦
    have ⟨δ, δ_pos, hδ⟩ := hf _ ε_pos
    have ⟨N, hN⟩ := hu _ δ_pos
    ⟨N, fun n hn =>
      hδ _ (hN _ _)⟩

example : sequence_tendsto (f ∘ u) (f x₀) :=
  fun ε ε_pos ↦
    have ⟨δ, δ_pos, hδ⟩ := hf _ ε_pos
    have ⟨N, hN⟩ := hu _ δ_pos
    ⟨N, fun n hn =>
      hδ _ (hN _ hn)⟩

example : sequence_tendsto (f ∘ u) (f x₀) :=
  fun _ ε_pos ↦
    have ⟨_, δ_pos, hδ⟩ := hf _ ε_pos
    have ⟨N, hN⟩ := hu _ δ_pos
    ⟨N, fun _ hn => hδ _ (hN _ hn)⟩

[Mario Carneiro]

(I also resisted the urge to golf the last line to ⟨N, fun _ => hδ _ ∘ hN _⟩)

[Mario Carneiro]

Another golf available in the final state is to use Exists.imp since the proof has a subterm of the form have ⟨N, hN⟩ := ...; ⟨N, ...⟩

[Mario Carneiro]

so a possible one-liner version of this proof is

example : sequence_tendsto (f ∘ u) (f x₀) := fun _ ε_pos ↦
  have ⟨_, δ_pos, hδ⟩ := hf _ ε_pos; (hu _ δ_pos).imp fun _ hN _ ↦ hδ _ ∘ hN _

[Ching-Tsun Chou]

After staring at Patrick's solution, I see that his proof is actually the same as mine. (Indeed, it would be very surprising if such a simple proof can be done in two essentially different ways.) This is shown in the following examples, where the same variable names are used in both to highlight the correspondences:

example (f : ℝ → ℝ) (u : ℕ → ℝ) (x₀ : ℝ)
    (hf : continuous_function_at f x₀) (hu : sequence_tendsto u x₀) :
    sequence_tendsto (f ∘ u) (f x₀) :=
  fun ε ε_pos ↦ (
    have ⟨δ, δ_pos, hf'⟩ := hf ε ε_pos
    have ⟨N, hu'⟩ := hu δ δ_pos
    ⟨N, fun n n_N ↦ (
      have h1 := hu' n n_N
      have h2 := hf' (u n) h1
      h2
      )
    ⟩
  )

example (f : ℝ → ℝ) (u : ℕ → ℝ) (x₀ : ℝ)
    (hf : continuous_function_at f x₀) (hu : sequence_tendsto u x₀) :
    sequence_tendsto (f ∘ u) (f x₀) :=
  fun ε ε_pos ↦ (hf ε ε_pos).elim
   fun δ ⟨δ_pos, hf'⟩ ↦ (hu δ δ_pos).elim
     fun N hu' ↦ ⟨N, fun n n_N ↦ hf' (u n) <| hu' n n_N⟩

[Mario Carneiro]

it is also the same as my proof, because pattern matching on existentials like have ⟨_, δ_pos, hδ⟩ := hf _ ε_pos is syntactic sugar for application of Exists.elim, i.e. (hf ε ε_pos).elim fun _ ⟨δ_pos, hδ⟩ =>

[Mario Carneiro]

(Ditto for the pattern matching on ⟨δ_pos, hδ⟩ here, which is syntax sugar for using And.elim)

[Dominic Steinitz]

This is a great thread - I've been slowly (re-) inventing these sort of tricks for myself - thanks very much everyone contributing :grinning_face_with_smiling_eyes:

[Ching-Tsun Chou]

I would also like to thank all experienced users who answered my questions.