structure default for proof fields

Stream: new members

[Julian Berman]

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]

(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]

structure thing := (value : ℕ) (h : ∀ i : ℕ, i = value ∨ i ≠ value . tauto)

[Julian Berman]

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

[Yakov Pechersky]

Is tauto imported?

[Kyle Miller]

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

structure thing := (value : ℕ) (h : ∀ i : ℕ, i = value ∨ i ≠ value . obviously)

[Julian Berman]

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]

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

[Kyle Miller]

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]

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]

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

[Kevin Buzzard]

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

[Julian Berman]

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]

got it, cool

[Julian Berman]

ok will try obviously.

[Kevin Buzzard]

That does the same as tidy

[Julian Berman]

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]

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

that says "tactic failed, there are unsolved goals"

[Kyle Miller]

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]

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

[Julian Berman]

interesting

[Kyle Miller]

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

[Julian Berman]

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

[Kyle Miller]

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

[Julian Berman]

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

[Julian Berman]

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

[Kyle Miller]

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

[Julian Berman]

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]

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]

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]

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]

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)