Zulip Chat Archive

Stream: new members

Topic: structure default for proof fields


Julian Berman (Sep 09 2020 at 21:34):

If I write some (silly for example purposes) structure like:

structure thing := (value : ) (h :  i : , i = value  i  value)

where I have a structure with a field and then a proof of something about that field, then I can instantiate that structure via e.g.:

#check {thing . value := 12, h := by tauto}

and that will compile. According to https://leanprover.github.io/reference/declarations.html#structures-and-records I should also be able to set defaults for fields within a structure. Can that default be a tactic somehow? I.e. this does not work:

structure thing := (value : ) (h :  i : , i = value  i  value := by tauto)

where I wanted that tactic to be applied when instances are created, saving having to pass it, but I get an interesting type error if I do that and then try #check {thing . value := 12}:

src/chess/board.lean:47:1 Error [lean] type mismatch at field 'h'  rfl.mpr ?hhas type   (i : ), i = 12  i  12but is expected to have type   (i : ), i = 12  i  12

Julian Berman (Sep 09 2020 at 21:35):

(in my "real code" for transparency, which is here: https://github.com/Julian/lean-across-the-board/blob/main/src/chess/board.lean#L24-L31, the thing I wanted to default was dec_trivial rather than tauto in case that's relevant, but the error seems similar)

Kenny Lau (Sep 09 2020 at 21:37):

structure thing := (value : ) (h :  i : , i = value  i  value . tauto)

Julian Berman (Sep 09 2020 at 21:39):

hm, that gives me... invalid auto_param, 'tauto' must have type (tactic unit)

Yakov Pechersky (Sep 09 2020 at 21:46):

Is tauto imported?

Kyle Miller (Sep 09 2020 at 21:51):

The category theory library uses obviously, which for now refers to tidy:

structure thing := (value : ) (h :  i : , i = value  i  value . obviously)

Julian Berman (Sep 09 2020 at 21:52):

Yakov Pechersky said:

Is tauto imported?

ah interesting, indeed it wasn't, I didn't realize it was transitively imported by the original place I extracted my code from

Julian Berman (Sep 09 2020 at 21:52):

(I still don't know that I can tell which import imports it? it's not import tactic.tauto seemingly?)

Kyle Miller (Sep 09 2020 at 21:52):

The error you're seeing might be that it's tactic.interactive.tauto, since you likely haven't used open for tactic.interactive.

Kyle Miller (Sep 09 2020 at 21:53):

But once you solve that, you might run into the issue that tauto is not a tactic unit, it's

interactive.tactic : interactive.parse (optional (lean.parser.tk "!"))  tactic unit

Julian Berman (Sep 09 2020 at 21:54):

@Kyle Miller I'm reading to make sure I understand what tidy means

Kevin Buzzard (Sep 09 2020 at 21:54):

It's just a "kitchen sink" tactic which tries simp and ext and induction and...

Julian Berman (Sep 09 2020 at 21:54):

It looks like it's basically an (annotation?) for a bunch of stuff that's useful to "make structures tidy" when instantiating yeah?

Julian Berman (Sep 09 2020 at 21:55):

got it, cool

Julian Berman (Sep 09 2020 at 21:55):

ok will try obviously.

Kevin Buzzard (Sep 09 2020 at 21:55):

That does the same as tidy

Julian Berman (Sep 09 2020 at 21:57):

Kevin Buzzard said:

That does the same as tidy

and which doesn't solve the goal from my silly example seemingly, if I did this correctly

Julian Berman (Sep 09 2020 at 21:57):

structure thing := (value : ) (h :  i : , i = value  i  value . obviously)
#check {thing . value := 12}

that says "tactic failed, there are unsolved goals"

Kyle Miller (Sep 09 2020 at 21:57):

If you want tauto, it looks like this works:

meta def my_tauto := tactic.tautology tt

structure thing := (value : ) (h :  i : , i = value  i  value . my_tauto)

Kyle Miller (Sep 09 2020 at 21:58):

the tt means "allow classical reasoning." Set it to ff if you don't want that

Julian Berman (Sep 09 2020 at 21:58):

interesting

Kyle Miller (Sep 09 2020 at 21:59):

For some reason, you cannot use tactics that have optional arguments, which is why I defined my_tauto

Julian Berman (Sep 09 2020 at 21:59):

yeah basically that's defining whether it's tauto with or without the !?

Kyle Miller (Sep 09 2020 at 22:00):

Yeah. tactic.interactive.tauto ultimately uses tactic.tautology and passes it tt or ff depending on whether or not a ! follows it.

Julian Berman (Sep 09 2020 at 22:01):

got it, thanks. is there a place to read about the auto_param syntax itself y'all just showed me?

Julian Berman (Sep 09 2020 at 22:01):

I don't see it in that reference manual page unless I'm missing it

Kyle Miller (Sep 09 2020 at 22:02):

I've only picked it up by osmosis. I have the same question :smile:

Julian Berman (Sep 09 2020 at 22:17):

Cool! After "unwrapping" dec_trivial this works in my real code too, though I seem to not need meta def since I found a tactic (exact_def_trivial) that I think I get to use directly already.

Julian Berman (Sep 09 2020 at 22:19):

I get a new error now if I try to use record updating though -- when I do {foo with value := 46} I guess the auto_param isn't reevaluated again (i.e. the proof isn't rerun on the new value, it takes the proof from the original record as-is, and type-errors)? Will have to put together a small example there to show what I mean.

Julian Berman (Sep 09 2020 at 22:50):

So if I have this:

import data.matrix.notation
structure thing :=
(elements : (fin 2)  )
(contents : matrix (fin 2) (fin 2) )
(contains_elements :
   ix: (fin 2),  x y: (fin 2), contents x y = ix . tactic.exact_dec_trivial)
def t : thing := {thing . elements := ![0, 1], contents := ![![0, 0], ![1, 1]]}

then it appears I can happily do #check {t with elements := ![2, 3]} but I cannot do #check {t with contents := ![![1, 1], ![0, 0]]}

Julian Berman (Sep 09 2020 at 22:52):

The error being:

type mismatch at field 'contains_elements'
  t.contains_elements
has type
  auto_param ( (ix : fin 2),  (x y : fin 2), t.contents x y = ix)
    (name.mk_string "exact_dec_trivial" (name.mk_string "tactic" name.anonymous))
but is expected to have type
  auto_param ( (ix : fin 2),  (x y : fin 2), ![![1, 1], ![0, 0]] x y = ix)
    (name.mk_string "exact_dec_trivial" (name.mk_string "tactic" name.anonymous))

which I guess I interpret as "the auto_param didn't get re-run again". Which I guess makes sense retrospectively, but I assume I can't get it to re-run in that situation (as part of defining the structure) can I?

Julian Berman (Oct 09 2020 at 22:27):

Julian Berman said:

I don't see it in that reference manual page unless I'm missing it

(again in case anyone searches and finds this thread... I found this :) -- it's covered in https://leanprover.github.io/reference/expressions.html#implicit-arguments as the last form there)


Last updated: Dec 20 2023 at 11:08 UTC