Zulip Chat Archive

Stream: general

Topic: Gabriel's challenge


view this post on Zulip Kevin Buzzard (Apr 01 2018 at 23:20):

Can you do Gabriel's exercise?

view this post on Zulip Kevin Buzzard (Apr 01 2018 at 23:20):

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

view this post on Zulip Kevin Buzzard (Apr 01 2018 at 23:21):

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

view this post on Zulip Kevin Buzzard (Apr 01 2018 at 23:21):

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

view this post on Zulip Kevin Buzzard (Apr 01 2018 at 23:22):

Talking of tactics reminded me of this.

view this post on Zulip Kevin Buzzard (Apr 01 2018 at 23:22):

I could only make a tactic expr

view this post on Zulip Simon Hudon (Apr 01 2018 at 23:23):

Is that against the rules of the game?

view this post on Zulip Kevin Buzzard (Apr 01 2018 at 23:24):

I wasn't sure.

view this post on Zulip Kevin Buzzard (Apr 01 2018 at 23:24):

because I know absolutely nothing about exprs

view this post on Zulip Kevin Buzzard (Apr 01 2018 at 23:24):

or whether it's possible to make them

view this post on Zulip Kevin Buzzard (Apr 01 2018 at 23:25):

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

view this post on Zulip Kevin Buzzard (Apr 01 2018 at 23:25):

but I don't think it has type expr

view this post on Zulip Simon Hudon (Apr 01 2018 at 23:25):

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

view this post on Zulip Kevin Buzzard (Apr 01 2018 at 23:26):

stop at that one

view this post on Zulip Kevin Buzzard (Apr 01 2018 at 23:26):

that one works

view this post on Zulip Kevin Buzzard (Apr 01 2018 at 23:27):

were you having a backtick nightmare? ;-)

view this post on Zulip Simon Hudon (Apr 01 2018 at 23:27):

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

view this post on Zulip Simon Hudon (Apr 01 2018 at 23:27):

How do you escape ticks?

view this post on Zulip Kevin Buzzard (Apr 01 2018 at 23:27):

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

view this post on Zulip Kevin Buzzard (Apr 01 2018 at 23:27):

result!

view this post on Zulip Simon Hudon (Apr 01 2018 at 23:28):

There should be only one tick before unit.star though

view this post on Zulip Kevin Buzzard (Apr 01 2018 at 23:28):

expr.const wants a name

view this post on Zulip Kevin Buzzard (Apr 01 2018 at 23:28):

oh we are doing the bad thing which Patrick complained about

view this post on Zulip Kevin Buzzard (Apr 01 2018 at 23:28):

he wants us to buzz off to another thread

view this post on Zulip Simon Hudon (Apr 01 2018 at 23:29):

Co-opting a channel?

view this post on Zulip Kevin Buzzard (Apr 01 2018 at 23:29):

topic

view this post on Zulip Kevin Buzzard (Apr 01 2018 at 23:30):

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

view this post on Zulip Kevin Buzzard (Apr 01 2018 at 23:31):

So a constructor is a const?

view this post on Zulip 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

view this post on Zulip Simon Hudon (Apr 01 2018 at 23:31):

Yes, that's correct

view this post on Zulip Kevin Buzzard (Apr 01 2018 at 23:32):

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

view this post on Zulip Simon Hudon (Apr 01 2018 at 23:32):

Lean compiles inductive types into constants and axioms

view this post on Zulip Simon Hudon (Apr 01 2018 at 23:33):

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

view this post on Zulip Kevin Buzzard (Apr 01 2018 at 23:33):

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

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Apr 01 2018 at 23:35):

infer type failed, incorrect number of universe levels

view this post on Zulip Kevin Buzzard (Apr 01 2018 at 23:35):

woo, new error messages

view this post on Zulip Simon Hudon (Apr 01 2018 at 23:36):

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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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)

view this post on Zulip Simon Hudon (Apr 01 2018 at 23:38):

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

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip Simon Hudon (Apr 01 2018 at 23:39):

Yes, that's really the main data structure

view this post on Zulip Kevin Buzzard (Apr 01 2018 at 23:39):

so everyone has an informal idea of what one is

view this post on Zulip Simon Hudon (Apr 01 2018 at 23:39):

Completely

view this post on Zulip Kevin Buzzard (Apr 01 2018 at 23:39):

because they have written some Lean code

view this post on Zulip Kevin Buzzard (Apr 01 2018 at 23:40):

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

view this post on Zulip Simon Hudon (Apr 01 2018 at 23:40):

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

view this post on Zulip Kevin Buzzard (Apr 01 2018 at 23:40):

but actually they are not constructing the exprs themselves

view this post on Zulip Kevin Buzzard (Apr 01 2018 at 23:40):

What is a proof goal?

view this post on Zulip Kevin Buzzard (Apr 01 2018 at 23:40):

There is some "interesting" comment in PIL

view this post on Zulip Kevin Buzzard (Apr 01 2018 at 23:42):

there it is, p38

view this post on Zulip 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.]

view this post on Zulip 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]

view this post on Zulip 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.

view this post on Zulip Simon Hudon (Apr 01 2018 at 23:48):

Does that make sense?

view this post on Zulip Kevin Buzzard (Apr 01 2018 at 23:51):

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

view this post on Zulip Kevin Buzzard (Apr 01 2018 at 23:51):

so it makes some sort of sense

view this post on Zulip Mario Carneiro (Apr 02 2018 at 00:00):

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

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Apr 02 2018 at 00:01):

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

view this post on Zulip 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

view this post on Zulip 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)

view this post on Zulip Kevin Buzzard (Apr 02 2018 at 00:04):

aah but now you're in tactic mode

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Apr 02 2018 at 00:04):

as an introduction to the backtick notation and to exprs

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Apr 02 2018 at 00:04):

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

view this post on Zulip 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.

view this post on Zulip 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 [])

view this post on Zulip Simon Hudon (Apr 02 2018 at 00:06):

But we're not discharging a goal completely here

view this post on Zulip Kevin Buzzard (Apr 02 2018 at 00:06):

it was level.of_nat 1 I was missing

view this post on Zulip Kevin Buzzard (Apr 02 2018 at 00:06):

Thanks Mario.

view this post on Zulip Mario Carneiro (Apr 02 2018 at 00:07):

you can also write level.succ level.zero

view this post on Zulip Kevin Buzzard (Apr 02 2018 at 00:07):

oh wow there is mk_eq_refl

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Apr 02 2018 at 00:09):

no expr.app in version 3?

view this post on Zulip Kevin Buzzard (Apr 02 2018 at 00:09):

what's going on there?

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Apr 02 2018 at 00:10):

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

view this post on Zulip 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 }

view this post on Zulip Mario Carneiro (Apr 02 2018 at 00:10):

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

view this post on Zulip 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: May 12 2021 at 05:19 UTC