term mode version of simple tactic proof

Stream: new members

[rzeta0]

I've been learning to do "tactic mode" proofs.

I'm curious as to what a "term mode" proof of the following very simple proof looks like:

-- 01 - First Proof

import Mathlib.Tactic

example {a : ℕ} (h1 : a = 4) : a > 1 := by
  calc
    a = 4 := by rw [h1]
    _ > 1 := by norm_num

My guess is that term mode proofs are more like "lambda calculus" in that we construct a function that is the proof, and here I can't think what we'd "apply" to h1 to get a>1.

example {a : ℕ} (h1 : a = 4) : a > 1 := h1 -- fails

[Riccardo Brasca]

import Mathlib.Tactic

example {a : ℕ} (h1 : a = 4) : a > 1 :=
  h1 ▸ (Nat.succ_lt_succ_iff.mpr <| Nat.zero_lt_succ _)

[Riccardo Brasca]

In general you can try by? to see a term mode proof, but it doesn't always work.

[Riccardo Brasca]

Here you have to avoid using rw, that is tricky, under th hood you need the recursor of equality. ▸ does this.

[Riccardo Brasca]

Here a version that avoids ▸ and uses Eq.subst explicitly.

example {a : Nat} (h1 : a = 4) : a > 1 :=
  Eq.subst (motive := fun n ↦ n > 1) h1.symm
    <| Nat.succ_lt_succ_iff.mpr <| Nat.zero_lt_succ _

[rzeta0]

yikes - that's a lot more complicated than I expected.

I'll try to come up with a simpler example where there is a simpler term mode proof.

I guess inequalities don't lend themselves to a simple mapping function.

[Aaron Liu]

Note that calc has a term version too:

import Mathlib.Tactic.NormNum

example {a : ℕ} (h1 : a = 4) : a > 1 :=
  calc
    a = 4 := h1
    _ > 1 := by norm_num

or maybe

example {a : Nat} (h1 : a = 4) : a > 1 :=
  calc
    a = 4 := h1
    _ > 1 := of_decide_eq_true rfl

[Riccardo Brasca]

Well, there are two things in the proof: first of all the rw part, that is not so easy to explain (it is done by Eq.subst). Then anyway you have to prove in some way that 4 > 1. Unravelling the definitions, a > b (that is b < a) is defined by b.succ ≤ a. Now, by definition of ≤, we have that 0 ≤ n and n ≤ m → n ≤ m.succ.

[Riccardo Brasca]

And one has somehow to use these facts to get to 1 < 4 (of course decide or something like that does it automatically)

[Damiano Testa]

As a general rule of thumb, if a tactic proof uses a tactic other than refine, apply, exact, constructor, intro (and possibly a couple more), the term mode proof will be "hard". In particular, rw, simp and tactics that internally use them (e.g. norm_num) are typically not so "term-mode friendly".

[Kevin Buzzard]

import Mathlib

theorem dontlook (a b : ℝ) : (a + b) * (a - b) = a^2 - b^2 := by ring

#print dontlook -- aaaargh