Zulip Chat Archive

Stream: general

Topic: Gabriel's challenge


Kevin Buzzard (Apr 01 2018 at 23:20):

Can you do Gabriel's exercise?

Kevin Buzzard (Apr 01 2018 at 23:20):

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

Kevin Buzzard (Apr 01 2018 at 23:21):

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

Kevin Buzzard (Apr 01 2018 at 23:21):

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

Kevin Buzzard (Apr 01 2018 at 23:22):

Talking of tactics reminded me of this.

Kevin Buzzard (Apr 01 2018 at 23:22):

I could only make a tactic expr

Simon Hudon (Apr 01 2018 at 23:23):

Is that against the rules of the game?

Kevin Buzzard (Apr 01 2018 at 23:24):

I wasn't sure.

Kevin Buzzard (Apr 01 2018 at 23:24):

because I know absolutely nothing about exprs

Kevin Buzzard (Apr 01 2018 at 23:24):

or whether it's possible to make them

Kevin Buzzard (Apr 01 2018 at 23:25):

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

Kevin Buzzard (Apr 01 2018 at 23:25):

but I don't think it has type expr

Simon Hudon (Apr 01 2018 at 23:25):

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

Kevin Buzzard (Apr 01 2018 at 23:26):

stop at that one

Kevin Buzzard (Apr 01 2018 at 23:26):

that one works

Kevin Buzzard (Apr 01 2018 at 23:27):

were you having a backtick nightmare? ;-)

Simon Hudon (Apr 01 2018 at 23:27):

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

Simon Hudon (Apr 01 2018 at 23:27):

How do you escape ticks?

Kevin Buzzard (Apr 01 2018 at 23:27):

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

Kevin Buzzard (Apr 01 2018 at 23:27):

result!

Simon Hudon (Apr 01 2018 at 23:28):

There should be only one tick before unit.star though

Kevin Buzzard (Apr 01 2018 at 23:28):

expr.const wants a name

Kevin Buzzard (Apr 01 2018 at 23:28):

oh we are doing the bad thing which Patrick complained about

Kevin Buzzard (Apr 01 2018 at 23:28):

he wants us to buzz off to another thread

Simon Hudon (Apr 01 2018 at 23:29):

Co-opting a channel?

Kevin Buzzard (Apr 01 2018 at 23:29):

topic

Kevin Buzzard (Apr 01 2018 at 23:30):

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

Kevin Buzzard (Apr 01 2018 at 23:31):

So a constructor is a const?

Simon Hudon (Apr 01 2018 at 23:31):

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

Simon Hudon (Apr 01 2018 at 23:31):

Yes, that's correct

Kevin Buzzard (Apr 01 2018 at 23:32):

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

Simon Hudon (Apr 01 2018 at 23:32):

Lean compiles inductive types into constants and axioms

Simon Hudon (Apr 01 2018 at 23:33):

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

Kevin Buzzard (Apr 01 2018 at 23:33):

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

Simon Hudon (Apr 01 2018 at 23:34):

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

Kevin Buzzard (Apr 01 2018 at 23:35):

infer type failed, incorrect number of universe levels

Kevin Buzzard (Apr 01 2018 at 23:35):

woo, new error messages

Simon Hudon (Apr 01 2018 at 23:36):

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

Kevin Buzzard (Apr 01 2018 at 23:36):

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

Kevin Buzzard (Apr 01 2018 at 23:37):

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 (Apr 01 2018 at 23:37):

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

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

Simon Hudon (Apr 01 2018 at 23:38):

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

Kevin Buzzard (Apr 01 2018 at 23:39):

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

Kevin Buzzard (Apr 01 2018 at 23:39):

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

Simon Hudon (Apr 01 2018 at 23:39):

Yes, that's really the main data structure

Kevin Buzzard (Apr 01 2018 at 23:39):

so everyone has an informal idea of what one is

Simon Hudon (Apr 01 2018 at 23:39):

Completely

Kevin Buzzard (Apr 01 2018 at 23:39):

because they have written some Lean code

Kevin Buzzard (Apr 01 2018 at 23:40):

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

Simon Hudon (Apr 01 2018 at 23:40):

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

Kevin Buzzard (Apr 01 2018 at 23:40):

but actually they are not constructing the exprs themselves

Kevin Buzzard (Apr 01 2018 at 23:40):

What is a proof goal?

Kevin Buzzard (Apr 01 2018 at 23:40):

There is some "interesting" comment in PIL

Kevin Buzzard (Apr 01 2018 at 23:42):

there it is, p38

Kevin Buzzard (Apr 01 2018 at 23:42):

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 (Apr 01 2018 at 23:45):

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 (Apr 01 2018 at 23:46):

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

Simon Hudon (Apr 01 2018 at 23:48):

Does that make sense?

Kevin Buzzard (Apr 01 2018 at 23:51):

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

Kevin Buzzard (Apr 01 2018 at 23:51):

so it makes some sort of sense

Mario Carneiro (Apr 02 2018 at 00:00):

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

Kevin Buzzard (Apr 02 2018 at 00:01):

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

Kevin Buzzard (Apr 02 2018 at 00:01):

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

Kevin Buzzard (Apr 02 2018 at 00:01):

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 (Apr 02 2018 at 00:03):

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 (Apr 02 2018 at 00:04):

aah but now you're in tactic mode

Kevin Buzzard (Apr 02 2018 at 00:04):

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

Kevin Buzzard (Apr 02 2018 at 00:04):

as an introduction to the backtick notation and to exprs

Simon Hudon (Apr 02 2018 at 00:04):

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 (Apr 02 2018 at 00:04):

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

Simon Hudon (Apr 02 2018 at 00:05):

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 (Apr 02 2018 at 00:06):

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 (Apr 02 2018 at 00:06):

But we're not discharging a goal completely here

Kevin Buzzard (Apr 02 2018 at 00:06):

it was level.of_nat 1 I was missing

Kevin Buzzard (Apr 02 2018 at 00:06):

Thanks Mario.

Mario Carneiro (Apr 02 2018 at 00:07):

you can also write level.succ level.zero

Kevin Buzzard (Apr 02 2018 at 00:07):

oh wow there is mk_eq_refl

Simon Hudon (Apr 02 2018 at 00:08):

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

Kevin Buzzard (Apr 02 2018 at 00:08):

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

Kevin Buzzard (Apr 02 2018 at 00:09):

no expr.app in version 3?

Kevin Buzzard (Apr 02 2018 at 00:09):

what's going on there?

Mario Carneiro (Apr 02 2018 at 00:09):

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 (Apr 02 2018 at 00:10):

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

Simon Hudon (Apr 02 2018 at 00:10):

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 (Apr 02 2018 at 00:10):

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

Mario Carneiro (Apr 02 2018 at 00:12):

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 [])

Last updated: Dec 20 2023 at 11:08 UTC