# Zulip Chat Archive

## Stream: new members

### Topic: Basic building block tactics

#### Lucas Allen (Feb 26 2020 at 03:02):

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 (Feb 26 2020 at 03:38):

`exact`

does everything by itself

#### Mario Carneiro (Feb 26 2020 at 03:38):

or `refine`

#### Mario Carneiro (Feb 26 2020 at 03:39):

You can probably get away with `intro`

and `apply`

, since that covers application and lambda

#### Mario Carneiro (Feb 26 2020 at 03:40):

`change`

is important for triggering definitional conversion

#### Mario Carneiro (Feb 26 2020 at 03:40):

but `induction`

and `rw`

are just fancy ways to apply functions

#### Kevin Buzzard (Feb 26 2020 at 07:41):

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 (Feb 27 2020 at 01:05):

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 := n`

would 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 (Feb 27 2020 at 01:08):

No. Remember `solve_by_elim`

only applies local hypotheses.

#### Scott Morrison (Feb 27 2020 at 01:10):

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 (Feb 27 2020 at 01:48):

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 (Feb 27 2020 at 07:13):

Change = show

#### Jasmin Blanchette (Feb 27 2020 at 08:59):

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 (Feb 28 2020 at 00:16):

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 (Feb 28 2020 at 00:46):

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 (Feb 28 2020 at 00:48):

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 (Feb 28 2020 at 00:49):

and `apply f`

replaces the hole with `f _ _ _`

(depending on how many arguments `f`

has)

#### Mario Carneiro (Feb 28 2020 at 00:50):

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 (Feb 28 2020 at 01:07):

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 `expr`

s, 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 (Feb 28 2020 at 01:13):

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 (Feb 28 2020 at 01:22):

`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 (Feb 28 2020 at 01:24):

Awesome!

#### Lucas Allen (Feb 28 2020 at 01:26):

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 `expr`

s?

#### Mario Carneiro (Feb 28 2020 at 01:26):

Yep!

#### Mario Carneiro (Feb 28 2020 at 01:27):

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 (Feb 28 2020 at 01:27):

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 (Feb 28 2020 at 01:28):

Also, are there situations where `cases`

works, but induction doesn't? This might be covered in theorem proving in Lean.

#### Mario Carneiro (Feb 28 2020 at 01:29):

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 (Feb 28 2020 at 01:30):

Internally, `cases`

actually first reverts the input variable and adds an equality

#### Lucas Allen (Feb 28 2020 at 01:30):

Oh, so `eq.rec_on`

is different somehow to other `rec_on`

's for inductive types?

#### Mario Carneiro (Feb 28 2020 at 01:30):

No, it is just that `rw`

uses an algorithm which is different from the generic one that is more useful for equalities

#### Lucas Allen (Feb 28 2020 at 01:32):

Right, because `induction`

rewrites everything it can everywhere.

#### Mario Carneiro (Feb 28 2020 at 01:32):

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 (Feb 28 2020 at 01:36):

Ok, so `rewrite`

is a convenience thing, built for humans.

#### Mario Carneiro (Feb 28 2020 at 01:36):

yep, most tactics are like that

#### Lucas Allen (Feb 28 2020 at 01:36):

Yeah, what about `Ext`

? can that be broken down into simpler tactics?

#### Mario Carneiro (Feb 28 2020 at 01:36):

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

#### Mario Carneiro (Feb 28 2020 at 01:37):

`ext`

is just `try {apply f}`

for every `f`

that has been marked `@[ext]`

#### Mario Carneiro (Feb 28 2020 at 01:37):

in practice, these lemmas tend to be about extensionality

#### Lucas Allen (Feb 28 2020 at 01:37):

Yeah, makes sense.

#### Lucas Allen (Feb 28 2020 at 01:41):

I have a bit to think about now. Thanks.

#### Lucas Allen (Feb 28 2020 at 02:06):

Is `unfold`

just another version of `change`

? I looked at the code and `unfold`

uses the simplifier, which is complex and confusing.

#### Lucas Allen (Feb 28 2020 at 02:07):

Does `simp`

use `change`

?

#### Mario Carneiro (Feb 28 2020 at 02:26):

`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 (Feb 28 2020 at 02:28):

`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 (Feb 28 2020 at 02:29):

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 (Feb 29 2020 at 00:22):

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 (Feb 29 2020 at 01:07):

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 (Feb 29 2020 at 01:08):

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

.

#### Reid Barton (Feb 29 2020 at 01:09):

(I'm assuming you did something like `#print succ_add`

, and then copy and pasted the result into `#reduce`

.)

#### Lucas Allen (Feb 29 2020 at 01:22):

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 (Feb 29 2020 at 01:22):

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 (Feb 29 2020 at 02:30):

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 (Feb 29 2020 at 08:16):

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 (Feb 29 2020 at 08:16):

Is this the fault of the equation compiler or something?

#### Mario Carneiro (Feb 29 2020 at 08:54):

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 (Feb 29 2020 at 08:59):

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 (Feb 29 2020 at 09:00):

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 (Feb 29 2020 at 14:24):

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 (Feb 29 2020 at 15:33):

The problem is that the `rec`

stuff is *not implemented*

#### Mario Carneiro (Feb 29 2020 at 15:33):

so it's `brec`

or nothing

#### Mario Carneiro (Feb 29 2020 at 15:33):

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

#### Mario Carneiro (Feb 29 2020 at 15:34):

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 (Feb 29 2020 at 16:59):

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 (Feb 29 2020 at 16:59):

Yep. The `brec`

method works as long as the inductive type is not a `Prop`

#### Lucas Allen (Mar 02 2020 at 02:23):

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 (Mar 02 2020 at 02:26):

`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 (Mar 02 2020 at 02:28):

Oh right, of course.

#### Lucas Allen (Mar 02 2020 at 02:36):

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

Last updated: May 15 2021 at 23:13 UTC