Gabriel's challenge

Stream: general

[Kevin Buzzard]

Can you do Gabriel's exercise?

[Kevin Buzzard]

https://leanprover.zulipchat.com/#narrow/stream/113488-general/subject/elaborator

[Kevin Buzzard]

theorem very_easy : unit = unit := by do exact $ ???

[Kevin Buzzard]

Can you make an expr which corresponds to eq.refl unit?

[Kevin Buzzard]

Talking of tactics reminded me of this.

[Kevin Buzzard]

I could only make a tactic expr

[Simon Hudon]

Is that against the rules of the game?

[Kevin Buzzard]

I wasn't sure.

[Kevin Buzzard]

because I know absolutely nothing about exprs

[Kevin Buzzard]

or whether it's possible to make them

[Kevin Buzzard]

I thought that eq.refl unit was an expression in Lean

[Kevin Buzzard]

but I don't think it has type expr

[Simon Hudon]

For unit, you could do: do exact $ expr.const ``unit.star []

[Kevin Buzzard]

stop at that one

[Kevin Buzzard]

that one works

[Kevin Buzzard]

were you having a backtick nightmare? ;-)

[Simon Hudon]

Yeah and I don't have an anti-tick shampoo!

[Simon Hudon]

How do you escape ticks?

[Kevin Buzzard]

open tactic expr
definition  very_easy : unit :=
by  do exact $ expr.const ``unit.star []

[Kevin Buzzard]

result!

[Simon Hudon]

There should be only one tick before unit.star though

[Kevin Buzzard]

expr.const wants a name

[Kevin Buzzard]

oh we are doing the bad thing which Patrick complained about

[Kevin Buzzard]

he wants us to buzz off to another thread

[Simon Hudon]

Co-opting a channel?

[Kevin Buzzard]

topic

[Kevin Buzzard]

Oh that was clever. I didn't know you could change in the middle

[Kevin Buzzard]

So a constructor is a const?

[Simon Hudon]

:grin: There's an option to change the topic of everything that comes after a certain post

[Simon Hudon]

Yes, that's correct

[Kevin Buzzard]

so how to change something like eq.refl into an expr?

[Simon Hudon]

Lean compiles inductive types into constants and axioms

[Simon Hudon]

Same thing const `eq.refl [`u] ... with the exception of the universe level

[Kevin Buzzard]

because then you could use expr.app to apply the function

[Simon Hudon]

Yes, you would first apply it to a Sort u and then to whatever term you want prove equal to itself

[Kevin Buzzard]

infer type failed, incorrect number of universe levels

[Kevin Buzzard]

woo, new error messages

[Simon Hudon]

That's curious! I'm pretty sure there should be only one

[Kevin Buzzard]

I honestly think that playing around with this sort of thing would be a good introduction to tactics.

[Kevin Buzzard]

because it gives you the idea of what an expr really is and begins to introduce stuff like the backtick hell before going meta

[Simon Hudon]

What you can do to see what's wrong is:

do c <- mk_const `eq.refl`,
   trace (c.to_raw_fmt)

[Simon Hudon]

Interesting! Thanks for the suggestion. I'll add some of that to my tutorial

[Kevin Buzzard]

Am I right in thinking that tactics could really be said to be acting on the exprs

[Kevin Buzzard]

and that you really have to have some sort of clear idea of what an expr is before moving on to tactics?

[Simon Hudon]

Yes, that's really the main data structure

[Kevin Buzzard]

so everyone has an informal idea of what one is

[Simon Hudon]

Completely

[Kevin Buzzard]

because they have written some Lean code

[Kevin Buzzard]

and they are told that they are constructing expressions of certain types

[Simon Hudon]

And maybe an explanation of what a proof goal is would also help

[Kevin Buzzard]

but actually they are not constructing the exprs themselves

[Kevin Buzzard]

What is a proof goal?

[Kevin Buzzard]

There is some "interesting" comment in PIL

[Kevin Buzzard]

there it is, p38

[Kevin Buzzard]

8.5 Metavariables and Unification [This section is still under construction. It will discuss the notion of a metavariable and its local context, with the interesting bit of information that goals in the tactic state are nothing more than metavariables. So the goal list is really just a list of metavariables, which can help us make sense of the get_goals and set_goals tactics. It will also discuss the unify tactic.]

[Simon Hudon]

A proof goal is basically an unassigned meta variable. It has no special status. You can think of a proof in tactic mode as creating one metavariable, saying that it's the proof of the main goal and then telling you to assign a value to that metavariable v by calling set_goals [v]

[Simon Hudon]

But you can set any list of unassigned metavariables as the goals in a proof even if they are not relevant.

[Simon Hudon]

Does that make sense?

[Kevin Buzzard]

set_goals doesn't make sense, but I can guess what it means.

[Kevin Buzzard]

so it makes some sort of sense

[Mario Carneiro]

@Kevin Buzzard To construct an expr, you can use the `(...) syntax

[Kevin Buzzard]

There is one backtick and two backticks and three backticks and none of them really make much sense to me

[Kevin Buzzard]

I can read the definitions but they don't stick yet

[Kevin Buzzard]

I am wondering if playing with exprs like this without thinking about tactics would be a better way to explain how all the backticks work

[Simon Hudon]

If you want to implement have for example, you could do it this way:

meta def my_have (h : name) (p : expr) : tactic unit :=
do (g :: gs) <- get_goals,
   prf <- mk_meta_var p, -- the side goal
   g' <- mk_mvar, -- not giving a type, we'll let `unify` guess it
   let prove_g := expr.app (expr.lam h binder_info.default p g') prf,
   unify prove_g g,
   set_goals (prf :: g' :: gs)

[Kevin Buzzard]

aah but now you're in tactic mode

[Kevin Buzzard]

I was wondering whether one could write something about creating raw exprs without ever mentioning the tactic monad

[Kevin Buzzard]

as an introduction to the backtick notation and to exprs

[Simon Hudon]

Yes, for two reasons: so that we can set and get the goals and so that we can create metavariables that are valid within the scope of the current proof

[Kevin Buzzard]

without having to introduce them at the same time as introducing all the tactic monad stuff

[Simon Hudon]

Oh ... and for unification. Since a meta variable is meaningful only in the context of a specific proof, you need the proof state when you assign a value to one.

[Mario Carneiro]

open tactic
theorem very_easy : unit = unit :=
by do exact `(eq.refl unit)

theorem very_easy₂ : unit = unit :=
by do mk_eq_refl `(unit) >>= exact

theorem very_easy₃ : unit = unit :=
by do exact $
  (expr.const ``eq.refl [level.of_nat 2] : expr)
  (expr.sort $ level.of_nat 1)
  (expr.const ``unit [])

[Simon Hudon]

But we're not discharging a goal completely here

[Kevin Buzzard]

it was level.of_nat 1 I was missing

[Kevin Buzzard]

Thanks Mario.

[Mario Carneiro]

you can also write level.succ level.zero

[Kevin Buzzard]

oh wow there is mk_eq_refl

[Simon Hudon]

Ah! That's the part I didn't think of! you were trying to prove unit = unit

[Kevin Buzzard]

I was trying to learn basic stuff about how to build exprs without going into tactic mode

[Kevin Buzzard]

no expr.app in version 3?

[Kevin Buzzard]

what's going on there?

[Mario Carneiro]

The last example is a bit artifical though, since usually you will not construct a complete expr by hand like that. Here's a half-tactic way to construct it:

theorem very_easy₄ : unit = unit :=
by do
  u ← mk_const ``unit,
  e ← mk_app ``eq.refl [u],
  exact e

[Kevin Buzzard]

I thought Lean was expecting one expr after the dollar sign and you passed three?

[Simon Hudon]

It's because of:

meta instance : has_coe_to_fun (expr elab) :=
{ F := λ e, expr elab → expr elab, coe := λ e, expr.app e }

[Mario Carneiro]

expr has a lovely coe_fn instance that allows you to write applications like that

[Mario Carneiro]

theorem very_easy₃' : unit = unit :=
by do exact $
  expr.app (expr.app
    (expr.const ``eq.refl [level.of_nat 2])
    (expr.sort $ level.of_nat 1))
  (expr.const ``unit [])