Documentation about tactic for default value in a structure

Stream: general

[Andrej Bauer]

Where can I read about the meaning of . obviously in

structure simple_graph (V : Type u) :=
(adj : V → V → Prop)
(sym : symmetric adj . obviously)
(loopless : irreflexive adj . obviously)

My guess is that it means "use the tactic obviously to construct a value if none given". What I am looking for is a way to construct such simple graphs, but I want to provide my custom tactics for the fields sym and loopless. (Or even better, convince the type class mechanism to unfold symmetric and irreflexive, as that would allow me to provide proof terms directly.)

[Scott Morrison]

You can put any tactic you like after the .. It just has to have type tactic unit, so sometime you need to make an auxiliary definition to wrap a tactic with a more complicated type.

[Scott Morrison]

e.g. meta def my_foo : tactic unit := `[foo] usually suffices to wrap an interactive tactic as a tactic unit.

[Andrej Bauer]

But I cannot change the definition of simple_graph in the standard library.

[Scott Morrison]

Ah!

[Scott Morrison]

Actually, obviously is an overridable tactic!

[Scott Morrison]

(Although we never really made use of this; it has constant meaning throughout mathlib.)

[Andrej Bauer]

I have a proof term that would work, if only symmetric and irreflexive were @[reducible] (I think), which they are not.

[Andrej Bauer]

It sounds like "overriding tactics" is the sort of thing that leads to a shotgun hole in the knee.

[Scott Morrison]

Yes. It was a bad idea, but it is still there to shoot yourself in the knee if you want to. :-)

[Scott Morrison]

It seems you just write

@[obviously] meta def my_obviously : tactic unit := ...

and from then on it has a new meaning.

[Scott Morrison]

You can just write a wrapper that uses your alternative tactics, I guess.

[Andrej Bauer]

To explain what I am after, it's a convenient way to generate simple graphs like this:

def my_adj := ....

example: simple_graph (fin 4) :=
 { adj := my_adj,
   sym := begin unfold symmetric, exact cow rfl end,
   loopless := begin unfold irreflexive, exact cow rfl end
 }

So I either have to get rid of the unfold and write just cow rfl for the proof terms, or write a little tactic-or-something that packages up the above snippet of code. What's the idiomatic way of doing this?

[Andrej Bauer]

Yes, I suppose I am asking how to write such a wrapper. (Or where to read about it, so that I don't have to bother you.)

[Andrej Bauer]

Oh my god, an interactive tactic can only have one argument. I so wish there were some documentation. Is there?

[Scott Morrison]

No, no, interactive tactics can have many arguments. Sorry, I'm about to head off for the night, but hopefully someone can step in.

[Scott Morrison]

There are some excellent video tutorials on metaprogramming by Rob Lewis.

[Scott Morrison]

There is a limited tutorial at https://leanprover-community.github.io/extras/tactic_writing.html

[Andrej Bauer]

We came up with this:

meta def tactic.interactive.foobar (adj : parse texpr) : tactic unit :=
do { t ← target,
     r ← i_to_expr_strict
                  ``(simple_graph.mk
                      (restrict (%%adj) _)
                      (begin unfold symmetric, exact cow rfl end)
                      (begin unfold irreflexive, exact cow rfl end) : %%t
                  ),
     exact r
}

Do we go to hell?

[Andrej Bauer]

Here's how an interactive tactic is not happy with two arguments:

meta def tactic.interactive.couple (a : parse texpr) (b : parse texpr) : tactic unit :=
do { r ← i_to_expr_strict ``((%%a, %%b)),
     exact r}

example: ℕ × ℕ := by couple 5 6

[Gabriel Ebner]

Lean parses 5 6 as an application here (and so never gets to b).

[Andrej Bauer]

Yes, I gather that much. How do I get around it?

[Gabriel Ebner]

The easiest fix is to add a separator between the two arguments:

import tactic.core
setup_tactic_parser
open tactic

meta def tactic.interactive.couple (a : parse texpr) (_ : parse $ tk ",") (b : parse texpr) : tactic unit :=
do { r ← i_to_expr_strict ``((%%a, %%b)),
       exact r}

example: ℕ × ℕ := by couple 5, 6

[Kyle Miller]

Andrej Bauer said:

But I cannot change the definition of simple_graph in the standard library.

One way around this is to define your own constructor, and you can replace the obviously with another tactic

structure simple_graph' (V : Type*) :=
(adj : V → V → Prop)
(sym : symmetric adj . obviouslier)
(loopless : irreflexive adj . obviouslier)

def simple_graph.create {V : Type*} (G : simple_graph' V) :
  simple_graph V :=
{ adj := G.adj,
  sym := G.sym,
  loopless := G.loopless }

-- example
def my_complete (V : Type*) : simple_graph V :=
simple_graph.create { adj := ne }

I would have expected the following to work too, but for some reason the tactics fail because their results have metavariables:

def simple_graph.mk' {V : Type*}
  (adj : V → V → Prop)
  (sym : symmetric adj . obviously)
  (loopless : irreflexive adj . obviously) :
  simple_graph V :=
{ adj := adj }

def my_complete (V : Type*) : simple_graph V :=
simple_graph.mk' ne

[Mario Carneiro]

Another way to make by couple 5 6 work is to parse 5 and 6 at application precedence, using pexpr 1025 instead of texpr