Term mode vs tactic mode

Stream: Lean for teaching

[Patrick Massot]

Frédéric Tran Minh said:

We used proof-term style in Lean.

Can you comment on why you chose to use proof-terms? This seems very counter-intuitive for a math course.

[Frédéric Tran Minh]

Hi Patrick and thanks for sharing. As you know I'm quite new is the universe of PA (we saw each other in Paris about 1 year ago... remember?) . Sorry in advance for the quite long reply. Good question....

In preamble: I made this choice without any background knowledge of how usually people use PA for teaching.
This was even one of the reasons for which I chose Lean over Coq, because at that time I didn't know that Coq could use proof term style as well, introduced by exact tactic (and even it seems less 'native').
(Aside from that I would probably be interested in opening a topic about why people here chose Lean over Coq for teaching, maybe this topic already exists).

To try to actually answer the question, I had the feeling that proof term style emphasizes the structured / hierarchical aspect of a proof. Terms being functionnally nested, the proof does not appear as sequence of imperative instructions. The scope of symbols is naturally highlighted by the structure of the term.
(Also I try to teach a very 'decorated' term style , with all the types made redundantly apparent : assume (h:P), ..., which is if I'm not mistaking something you're sort of forcing in your "Lean-Verbose" package -- but I could do that also in tactic-style)
In tactic mode to prove P \and Q you ask, say, 'split', and you have to mentally keep track of the following structure in 2 blocks, and the interactive display of tactic state helps you.
In proof term you write 'and.intro (...) (...)' which in a sense is identical, but the structure is imposed by the syntax of the langage.
I have a slightly different feeling between 'the proof is unfinished because there's a goal left to prove' and 'the term is syntaxically incorrect because I gave only 1 argument to function and.intro which expects 2'.
I must add that my students are and will keep studying CS during 5 years (algorithmics, langages, theory of langages: grammars...) and are supposed to be gradually sensitized to formal syntaxics issues. (and I'm myself a former dev engineer reconverted in teaching maths & CS...)
I don't know what is really intuitive or counter intuitive for 1st year students with quasi no proof practice. But the tactic style kind of mixes the "necessary condition" direction (work on hypothesis) and the "sufficient condition" direction (work on the goal) and to me, this seems confusing for students that do not clearly distinguish forward and backward reasoning.
Finally, even if the use of tactics is 'in fine' inevitable in practice, the sense that you could develop the whole term using lemmas gives, I find, sort of confidence in a proof, as opposed to the quite 'opaque' 'black box' philosophy of tactics. If you #print the term produced by 'simp' or 'finish' you often get a term the no normal human would write, nor easily reads. (I would be interested to know if it's possible to write tactics the produces human-readable terms....).

I admit that the difference could be tiny and also I may have made a mistake. Still hesitating for next time.
May I ask you why you chose tactic-style for teaching ?

[Kevin Buzzard]

Because ring represents how mathematicians think much better than rw add_assoc, and linarith much better than refine lt_of_le_of_lt h _

[Patrick Massot]

The question simply does not apply in a course involving actual math. Term mode is good enough only for pure logic or micro proofs combining known facts.

[Patrick Massot]

About structuring, there is nothing enforced by tactic mode. It all depends on the tactics you choose to use and how you choose to use them.

[Siddhartha Gadgil]

I do however give a few term mode proofs and also some in both modes and/or print the ones in tactic mode so that students know what is going on in tactics.

[Frédéric Tran Minh]

Thank you for your clear-cut answer! I'll think about it.

[suhr]

A great feature of Lean 4 is an ability to combine both style easily. In term mode you can write something like add.intro (by ring) (...), while in the proof mode you can do refine add_intro ?_ ?_ to get the goals you need.

I prefer term mode for a simple reason: I prefer to embrace type theory rather than hide it under tactics and pretend it's a some kind of set theory.

As an example of a style, consider mul_left_cancel from Natural Number Game:

theorem mul_left_cancel {n k p: Nat}(pn: n ≠ 0): (n * k = n * p) → k = p := by
  suffices h: ∀k, (n * k = n * p) → k = p from h k
  refine p.recOn ?_ ?_
  · intro k (nk: n * k = 0)
    exact (mul_eq_zero nk).elim (λz: n = 0 => (pn z).elim) id
  · intro p h
    show ∀k, (n * k = n * p.succ) → k = p.succ
    refine λk => k.casesOn ?_ ?_
    · intro (e: 0 = n * p + n)
      exact (pn $ add_eq_zero_right e.symm).elim
    · intro k (e: n * Nat.succ k = n * Nat.succ p)
      exact congrArg Nat.succ $ h k (add_right_cancel e)

Compared to a proof in NNG it has the following features:

1. You can actually read it without starting Lean
2. The reason why it's possible to read is because of sufficient amount of type annotations
3. Only structuring tactics are used. No tactics like split or induction, since there are functions for that
4. And I would argue it's closer to both a human proof and a proof term than the proof in NNG

[Jireh Loreaux]

suhr said:

I prefer term mode for a simple reason: I prefer to embrace type theory rather than hide it under tactics and pretend it's a some kind of set theory.

I don't understand what tactics have to do with pretending type theory is set theory (except potentially tactic#lift).

I'm also not sure why you think p.recOn ?_ ?_ is more readable than some version using the induction tactic, or how using Or.elim hidden behind dot notation is more readable than a proof with cases. I'm not saying the NNG proof you linked is the ideal in terms of readability, but certainly there are cases where sophisticated tactics (beyond intro, exact or refine) truly aid in readability of a proof, especially when you get past things as simple as natural numbers.

[suhr]

Nat is an inductive type, defined by its constructors and eliminated by its recursor. So p.recOn emphasis that induction is not some kind of special thing in type theory, it's literally just using the recursor of an inductive type.

Same for Or.elim: reasoning by cases is not some kind of special rule, but simply applying a function to the value of the Or type. And Or is again just an inductive type.

but certainly there are cases where sophisticated tactics (beyond intro, exact or refine) truly aid in readability of a proof

True. But in this cases you need simp, ring or aesop rather than cases.

[Petur Vetle]

I'm rather new to Lean so I can't comment on the benefits that tactic mode may give you over term mode. That being said, from a beginner's perspective, comparatively I like term mode over tactics (although both are quite difficult to read).

Tactics hide a lot of information that you only see when the lean server is running, which makes understanding a proof very difficult. While the kernel checks the correctness of the proof, a lot of the times the thing I am more interested in is the strategy the user took to develop the proof. Which means being able to easily read a proof is a priority for me.

[Yury G. Kudryashov]

If you want to write a mathematically non-trivial proof, then it's really hard without tactics.

[Yury G. Kudryashov]

Also, simp only [inter_univ] is more readable than some complicated expression with congr_arg and congr_fun.

[Kevin Buzzard]

I think you must mean a different thing to me when you say "understanding a proof". The term corresponding to a proof of $(x+y)^2=x^2+2xy+y^2$ is incomprehensible to me, whereas the tactic ring is highly comprehensible as an explanation of what is actually going on.

[Petur Vetle]

Tactics are definitely better in situations where the details of the proof are a burden to the reader (and hence the writer). But the link that @suhr gave to the mul_left_cancel proof in the natural number game is good example of why I don't like tactics. For me, its very difficult to parse the proof, even with vs code open and running the lean server. I'm sure that'll change as I learn more about lean. On the other hand, term mode isn't much better, but at least all of the details involved in the proof are visible. To me at least, its easier to see the structure and motivation behind a proof when its written in term mode.

[Yury G. Kudryashov]

That's because it's better to write this proof with some abstractions.

[Yury G. Kudryashov]

E.g., if you use docs4#Function.Injective.eq_iff, then you need to prove only one implication.

[Yury G. Kudryashov]

The other is in fact some congr_arg

[Yury G. Kudryashov]

Then it may be useful to prove that (a * ·) is strictly monotone, not just injective.

[Yury G. Kudryashov]

(of course in the NNG you're not building a library, you're heading for a goal)

[Kevin Buzzard]

For results that basic I guess my instinct would be that I had no desire to actually see the details of the proof :-) The term behind that tactic mode proof will be much worse than the tactic, because it uses the rw tactic which generates horrible terms.

Here's my attempt to read that proof without VS Code (disclaimer: I wrote the proof).

Every variable is a natural. Fix $a\not=0$. Let $P(c)$ denote the statement that for all $b$, $ab=ac\implies b=c$. We prove it by induction. Base case: we need to check that $0=ac$ implies $0=c$ given $0\not=a$, but $ac=0$ implies $a=0$ or $c=0$ (that's what eq_zero_or_eq_zero_of_mul_eq_zero is going to say) so we're done.

Inductive step: we assume "for all $b$, $ab=ad\implies b=d$" and we want "for all $b$, $ab=a(d+1)\implies b=(d+1)$". So let $b$ be arbitrary. If $b=0$ then $a(d+1)=0$ and this is a contradiction because neither $a$ nor $d+1$ are zero. If $b\not=0$ then we can write $b=c+1$ (sorry for reusing $c$!) and now our goal is $a(c+1)=a(d+1)\implies c+1=d+1$ and expanding out the brackets (mul_succ) and cancelling $a$ (add_right_cancel) means that we need to prove $ac=ad\implies c+1=d+1$, which follows from the inductive hypothesis.

Note that I just read the tactic proof and I could guess what the lemmas were saying because of Lean's super-cool naming convention.

[Shreyas Srinivas]

The experts have already weighed in. However, since this is about teaching and learning, I'll try to offer the perspective of someone who started with lean recently, and has also dabbled in other provers. That is to say, a learner and beginner.

TL DR: Term mode is worth it for basic stuff and understanding what to do and what tactics mean. It has some pedagogical value. However, once you get past basic propositions and start dabbling in predicates involving other data types, it quickly becomes tedious with messy details that distract from the actual proof. Sticking with term mode can be very boring for students.

Very Long Response:
Firstly, I understand where you are coming from. When I started with tpil, I too was enthusiastic about using term mode and retained that enthusiasm for a few months. Why? I had tried Coq before (Software Foundations) and dabbled a bit in Isabelle (although back then I gave it up very quickly). In both of them, the tactic language confused me a lot because every tactic seemed to be doing its own thing and the only handle the teaching materials gave to me was the intuitive idea of what they did. This might be fine for pen and paper proofs where one can work out the details in one's mind or scribble them in enough detail to understand things. But when you are writing something in a theorem prover (which is an exercise in programming and, at sufficient scale engineering, no matter what mathematicians say), you know you need to formulate something precise. At that point the vague intuition about tactics that tutorials provide is not sufficient. How does one reason about what's going on? What's really happening under the hood for some tactic code to be considered a proof? What even is a proof, and what is the prover checking? How does one debug the proof if something doesn't work? In contrast, lean's #tpil starts out with two chapters on term mode proofs of propositions and predicates. This is a minimal simple programming language and with practice, one can learn to program proofs for almost any propositional statement. Suddenly proof assistants feel less like unwieldy magic and more like a systematic, comprehensible programming exercise. I wouldn't be surprised if subconsciously this was the factor that made me stick with lean, although my normal response to such questions includes other factors. Since then I have taken another shot at Coq and Isabelle and got through the learning material and exercises much more quickly. So there is clearly some pedagogical value in understanding the term language

However, having sung the glories of term mode, I have to admit that I very quickly hit a wall. As soon as I hit some "real" math (read : simple things involving numbers, equalities, inequalities etc), the proving process very quickly degenerated into long and tedious sequences of using Nat, Eq's, LTs constructors and recursors. Any high level structure in the proof got drowned in a morass of irrelevant details. This is when I warmed to chapter 5. The term mode chapters definitely helped me better structure my understanding of what these tactics were doing. I am guessing I am not the only one who went through this experience.

Additionally, I have known quite a few students who went through theorem prover courses in a CS context. Many of these courses focus mostly on how to work with logic and never touch upon any serious math. The students came out these courses scarred. One of them, doesn't want to see a theorem prover again for a few years. This is not some statistically representative sample. But it is not hard to guess why someone might say this.