Tactic failure in a class

Stream: metaprogramming / tactics

[Andre Hernandez-Espiet (Rutgers)]

Hi all, I'm trying to write my first tactics. I'm trying to do this in a class called incidence_geometry and for some reason the test tactics I write don't transfer over, as I get the error failed to add declaration to environment, it contains local constants when I try to use a tactic on a lemma trivi2'. What is it that I'm not understanding? Here is the code:

import tactic.interactive

universes u1
class incidence_geometry :=
(point : Type u1)

open incidence_geometry

variables[AxA: incidence_geometry]

include AxA

lemma trivi'  : 1=1 := by refl

meta def dumbest' : tactic unit:=
do
tactic.applyc ``trivi'

lemma trivi2' : 1=1:=
begin
  dumbest',
end

[Kevin Buzzard]

Does it make any difference if you put dumbest' in the tactic.interactive namespace?

[Andre Hernandez-Espiet (Rutgers)]

I don't think I quite know what you mean

[Andre Hernandez-Espiet (Rutgers)]

Like if I put the tactic code before the universes u1 line, then it works. But I would like to write tactics about points, which I wouldn't be able to do if I had to write the tactics before I define a point? Unless I'm misunderstanding something.

[Kevin Buzzard]

Oh I see, you know the problem? Then it's not what I was suggesting. Your problem is then surely the include. Just remove that, because it has nothing to do with the tactic.

[Kevin Buzzard]

include is only used rarely, it means "I'm too lazy to write [AxA: incidence_geometry] lots of times in situations where Lean can't guess that it should be there". But Lean can usually guess what to include. Right now you're demanding that your tactics all include a variable which Lean has no idea what it is or what to do with.

[Andre Hernandez-Espiet (Rutgers)]

I see, but then what do I add to make things about points work? As in, how would I repair the following code?

import tactic.interactive

universes u1
class incidence_geometry :=
(point : Type u1)

open incidence_geometry

variables[AxA: incidence_geometry]


lemma trivi'  (a: point): a=a := by refl

meta def dumbest' : tactic unit:=
do
tactic.applyc ``trivi'

lemma trivi2' : a=a:=
begin
  dumbest',
end

[Patrick Massot]

I think you need to learn much more about regular use of Lean before trying to write tactics.

[Heather Macbeth]

@Andre Hernandez-Espiet (Rutgers) Am I guessing correctly that you're setting up some situation like, you have (point : Type) and (line : Type) and various axiomatic relations lies_on : point → line → Prop, between : point → point → point → Prop?

[Andre Hernandez-Espiet (Rutgers)]

Yes, that is exactly correct @Heather Macbeth

[Heather Macbeth]

Then I think you will fight the typeclass system less if you make incidence_geometry a class which takes point and line as parameters, like

class incidence_geometry (point : Type*) (line : Type*) :=
(lies_on : point → line → Prop)
(between : point → point → point → Prop)

etc

[Andre Hernandez-Espiet (Rutgers)]

What parts of Lean @Patrick Massot ? I've written about 2000 lines formalizing things in synthetic geometry (so I'm comfortable in this sense), but my setup is quite simple. There are a lot of repetitive routines I have to do over and over again, and was thinking I could write some tactics to simplify this.

[Heather Macbeth]

You can then work with a standing typeclass assumption

variables (point : Type*) (line : Type*) [incidence_geometry point line]

[Andre Hernandez-Espiet (Rutgers)]

Thanks a lot! That worked

[Patrick Massot]

Andre, my comment was purely based on the code snippet right above it that is very far away from compiling even if you remove the tactic attempt.

[Patrick Massot]

Did you try actually pasting that code into an empty Lean file?