Basic building block tactics

Stream: new members

[Lucas Allen]

I'm interested in learning about the basic building blocks of proofs in Lean. To this end I've read section 2 of Mario's masters thesis, but I don't have a CS background and didn't understand everything. From what I did understand the tactics, intro, apply, induction, and rw, relate to typing judgements, the basic building blocks of proofs.

Is there a list of tactics for which it's theoretically possible to prove any statement in Lean using only tactics on the list? Or is there a tactic for each typing judgement? And if so, what's the list? Or where can I learn more?

Thanks.

[Mario Carneiro]

exact does everything by itself

[Mario Carneiro]

or refine

[Mario Carneiro]

You can probably get away with intro and apply, since that covers application and lambda

[Mario Carneiro]

change is important for triggering definitional conversion

[Mario Carneiro]

but induction and rw are just fancy ways to apply functions

[Kevin Buzzard]

I guess it's theoretically possible to prove any statement in lean without using any tactics at all, because you can just use term mode. I think Agda might look like this?

[Lucas Allen]

Mario Carneiro said:

You can probably get away with intro and apply, since that covers application and lambda

change is important for triggering definitional conversion

I see, thanks.

If solve_by_elim was extended so that it could also do intro and change, would it then be a proof search? I.e. if max_reps := nwould it always find a proof of length less than or equal to n if one exists?

Kevin Buzzard said:

I guess it's theoretically possible to prove any statement in lean without using any tactics at all, because you can just use term mode. I think Agda might look like this?

I guess this is why exact does everything. But that's no fun. :)

[Scott Morrison]

No. Remember solve_by_elim only applies local hypotheses.

[Scott Morrison]

Also, change requires an explicit user provided argument, so I don't know what you're hoping it would do for you automatically.

[Lucas Allen]

Scott Morrison said:

No. Remember solve_by_elim only applies local hypotheses.

Right, but I thought if something can be proved then it can be proved only using local hypotheses, you just take the proof of lemma or theorem you'd normally use and insert in into the correct spot in your proof. Is that wrong?

Scott Morrison said:

Also, change requires an explicit user provided argument, so I don't know what you're hoping it would do for you automatically.

I have no experience with change, and it's not in tactics.md. I'm going to spend a bit of time seeing what I can find out.

[Kevin Buzzard]

Change = show

[Jasmin Blanchette]

If one is interested in minimalism, one can easily avoid the "change" (or "show") tactic. Say the goal is ⊢ half_empty and I wish it were ⊢ half_full. I can write

    apply (begin ... end : half_full)

If you allow yourself have, you can write

    have hhf : half_full := ...,
    apply hhf

[Lucas Allen]

I'm interested in learning about the fundamental building blocks of proofs in Lean. In order to do this do I need to learn some CS stuff to the point I completely understand section 2 of Mario's thesis, or is it possible to understand what the basic building blocks are from existing tactics? I.e. are there tactics that emulate the various typing judgements, such as intro for example? Or am I way off base about how Lean works?

[Mario Carneiro]

I think a good place to start is by understanding term proofs, and how tactics are just mechanisms for building particular terms (which you can see with #print)

[Mario Carneiro]

In a tactic proof, each goal corresponds to an _ (a hole to be filled) in the corresponding term proof, and each tactic replaces that hole with a term, usually containing more holes inside it. For example, intro x will replace the hole with \lam x, _.

[Mario Carneiro]

and apply f replaces the hole with f _ _ _ (depending on how many arguments f has)

[Mario Carneiro]

It also might help to look at the definition of the expr type in lean, which shows all the kind of things that can appear in a term

[Lucas Allen]

Ok, I think I'm pretty comfortable with the idea of metavariables, but I'm might go through theorem proving in Lean again to pick up some of the things I missed the first time as well as understand what specifically different tactics are doing to the terms.

I'm not so comfortable with exprs, however, but I'll put some time into learning.

I'd still like to understand how a proof search tactic might work. Maybe I'll ask again after I've learned these things.

Thanks.

[Mario Carneiro]

A quick overview:

• intro x replaces the goal with \lam x, _
• apply f replaces the goal with f _ _ _
• refine e1 (e2 _) (e3 _) replaces the goal with e1 (e2 _) (e3 _) (which should make it clear why I say sometimes that refine is the "universal" tactic, capable of playing the role of all others)
• exact e replaces the goal with e
• change foo replaces the goal with (_ : foo)
• rw foo replaces the goal with eq.rec_on foo _
• induction foo replaces the goal with T.rec_on foo _ _ where T is the type of foo
• cases foo replaces the goal with T.cases_on foo _ _ where T is the type of foo
• split replaces the goal with and.intro _ _
• have x := t replaces the goal with (\lam x, _) t
• let x := t replaces the goal with let x := t in _
• revert x replaces the goal with _ x

[Mario Carneiro]

simp, norm_num, ring, omega, library_search, tidy, rcases, rintro do more complicated or iterative things to the goal, but fundamentally they all have the same form as the above tactics: they look at the current type of the target hole and use that to determine some term, possibly with more holes in it, to fill the target

[Lucas Allen]

Awesome!

[Lucas Allen]

Can induction be used instead of rw? For example, given h : a = b, can we always use induction h instead of rw h? Or are there some cases where funny things happen with exprs?

[Mario Carneiro]

Yep!

[Mario Carneiro]

However it usually won't be able to calculate the "motive", a hidden extra argument to eq.rec_on, correctly if you use induction h

[Mario Carneiro]

However if one side of the equality is a variable, induction h, cases h, and subst h all act more or less the same way

[Lucas Allen]

Also, are there situations where cases works, but induction doesn't? This might be covered in theorem proving in Lean.

[Mario Carneiro]

Yes. The reason is that unlike induction, cases is able to make use of the equality between the input and the values in the cases to eliminate some of the constructors. (If you were to do this in induction, the inductive hypothesis would end up being useless in most cases)

[Mario Carneiro]

Internally, cases actually first reverts the input variable and adds an equality

[Lucas Allen]

Oh, so eq.rec_on is different somehow to other rec_on's for inductive types?

[Mario Carneiro]

No, it is just that rw uses an algorithm which is different from the generic one that is more useful for equalities

[Lucas Allen]

Right, because induction rewrites everything it can everywhere.

[Mario Carneiro]

You can always specify the motive yourself, but it's a pain. eq.rec_on says that from a = b and C a derive C b, so if you are faced with a goal that has b's in it you want to reverse engineer what C should be so that C b evaluates to the goal and C a evaluates to something more useful

[Lucas Allen]

Ok, so rewrite is a convenience thing, built for humans.

[Mario Carneiro]

yep, most tactics are like that

[Lucas Allen]

Yeah, what about Ext? can that be broken down into simpler tactics?

[Mario Carneiro]

you could write the term if you wanted to, but you don't want to

[Mario Carneiro]

ext is just try {apply f} for every f that has been marked @[ext]

[Mario Carneiro]

in practice, these lemmas tend to be about extensionality

[Lucas Allen]

Yeah, makes sense.

[Lucas Allen]

I have a bit to think about now. Thanks.

[Lucas Allen]

Is unfold just another version of change? I looked at the code and unfold uses the simplifier, which is complex and confusing.

[Lucas Allen]

Does simp use change?

[Mario Carneiro]

dsimp and dunfold act like change, which is to say, they don't add anything to the term but rather just assert a new type for the term and let the kernel figure it out. (Actually that's a lie. In order to keep up performance in the kernel, the goal is actually replaced with @id foo _ instead so that the kernel also gets the same definitional reduction hint as the elaborator. If you have @id foo (@id bar x), lean's kernel is forced to prove that foo and bar are definitionally equal so that the term is well typed.)

[Mario Carneiro]

simp and unfold actually insert equality theorems. It's kind of like rw but instead of using a single eq.rec term with a complicated motive, it is a cast applied to a bunch of congruence lemmas with types like x = y -> z = w -> x + z = y + w.

[Mario Carneiro]

This approach allows you to do extra things in the course of those lemmas, like for example ignoring equalities of arguments that are known to be in subsingleton types, as well as generally using equality proofs that are not definitional

[Lucas Allen]

I see, Thanks. I had a look at dunfold but it's just a meta constant, so I guess it's more fundamental than unfold. tactic.change is a meta constant as well.

I've been rereading chapter 2 of theorem proving in Lean, and decided to have a go at reducing the proof term for succ_add.

#reduce λ (n m : ℕ),
  nat.brec_on m
    (λ (m : ℕ) (_F : nat.below (λ (m : ℕ), ∀ (n : ℕ), succ n + m = succ (n + m)) m) (n : ℕ),
       (λ (n m : ℕ) (_F : nat.below (λ (m : ℕ), ∀ (n : ℕ), succ n + m = succ (n + m)) m),
          nat.cases_on m
            (λ (_F : nat.below (λ (m : ℕ), ∀ (n : ℕ), succ n + m = succ (n + m)) 0),
               id_rhs (succ n + 0 = succ n + 0) rfl)
            (λ (m : ℕ) (_F : nat.below (λ (m : ℕ), ∀ (n : ℕ), succ n + m = succ (n + m)) (succ m)),
               id_rhs (succ (succ n + m) = succ (succ (n + m))) (congr_arg succ (_F.fst.fst n)))
            _F) n m _F) n

It gives me λ (n m : ℕ), ⁇ and red sqiggle under nat.brec_on with the error message "invalid 'nat.brec_on' application, elaborator has special support for this kind of application (it is handled as an "eliminator"), but the expected type must be known."

Does it want know the type of succ_add? And is there some way to reduce a proof term to the type it's proving?

[Reid Barton]

The term displayed by Lean might not contain enough information to reconstruct the original term, as implicit arguments (here the motive for nat.brec_on) may not be inferable, or at least not by the algorithm Lean uses. Here maybe it would help to add a type ascription (... : succ n + m = succ (n + m)) or whatever the correct type is to the body of the lambda.

[Reid Barton]

But in this case, you might as well just write #reduce nat.succ_add.

[Reid Barton]

(I'm assuming you did something like #print succ_add, and then copy and pasted the result into #reduce.)

[Lucas Allen]

I couldn't get the type ascription to work.

I had a go at turn implicit arguments off and reducing the larger proof term, but now I get a "type mismatch at application" under @nat.rec.

But the red squiggle under @nat.brec_on is gone.

[Lucas Allen]

Reid Barton said:

(I'm assuming you did something like #print succ_add, and then copy and pasted the result into #reduce.)

Yes, exactly. :)

[Reid Barton]

Using pp.all would increase the chances of this working, but it would be better not to do this at all and just use #reduce succ_add directly

[Kevin Buzzard]

I never understand why these terms have brec_on and below in. When we prove this in the natural number game we just use an easy induction on m so I would just expect a much simpler term with rec

[Kevin Buzzard]

Is this the fault of the equation compiler or something?

[Mario Carneiro]

It is a rather unfortunate limitation of the current equation compiler that it cannot handle structural recursion, that is, creating definitions using rec_on directly. It always compiles everything using "bounded recursion", which is needed to handle more complex structural recursions like:

def fib : nat -> nat
| 0 := 0
| 1 := 1
| (n+2) := fib n + fib (n+1)

(Actually, the bounded recursion technique is not necessary here because you don't need to tuple up the entire history of the function, only the last two values. To take full advantage of the bounded recursion technique you would need to have references out some arbitrary amount, like f n depending on f(n/2), but in fact this is exactly the case where the equation compiler can't use this method and falls back on well founded recursion.)

While the use of structural recursion in place of bounded recursion is a "mere optimization", allowing functions like

def add (m : nat) : nat -> nat
| 0 := m
| (n+1) := add n + 1

to be compiled to the obvious nat.rec_on term instead of the current monstrosity, in some cases it is actually the only available method because bounded recursion method is blocked, and in those cases you will get an error if you try to use the equation compiler even though it should be able to compile in principle.

[Mario Carneiro]

Here's an example of a structural recursive definition that is rejected because the equation compiler can't handle it. (The error message you get is because the failure of bounded recursion falls over to well founded recursion, which fails at some obscure step.)

inductive foo : ℕ → Prop
| mk {n} : foo (n+1) → foo n

def no_foo : ∀ n, foo n → false
| n (foo.mk h) := no_foo (n+1) h
-- failed to prove recursive application is decreasing
-- |- 0 < 0

[Mario Carneiro]

Here's the obvious structural recursion proof:

def no_foo' : ∀ n, foo n → false :=
λ n h, foo.rec_on h (λ n h ih, ih)

[Reid Barton]

Would it be feasible to add an option to the equation compiler to disable this brec stuff? While it managed to cause fewer problems than it seems like it ought to, it's also virtually never the case that I actually want it

[Mario Carneiro]

The problem is that the rec stuff is not implemented

[Mario Carneiro]

so it's brec or nothing

[Mario Carneiro]

(well, well founded recursion, but that's much worse of an option)

[Mario Carneiro]

It's ironic because it's the most basic primitive so you would expect it to be supported, but no, the fancy brec is there but not the humble rec

[Reid Barton]

Oh huh I never realized that. So even when I use complicated inductive types with extra indices, constructors of infinite arity etc it always translates into brec?

[Mario Carneiro]

Yep. The brec method works as long as the inductive type is not a Prop

[Lucas Allen]

Is there some function in Lean that eats a proof term and gives the proposition proved by the input?

For example, is there a function F, say, such that F (λ hp : p, λ hq : q, hp) gives p → q → p?

And if not, is such a function possible?

[Mario Carneiro]

infer_type is a tactic that will do that. But it doesn't make any sense for a lean function to do that, as it would be one of the inputs to the function. That is:

def get_type {A : Sort*} (a : A) := A

[Lucas Allen]

Oh right, of course.

[Lucas Allen]

I got it working, I'm very happy. :)