tactic

Stream: general

[orlando]

Hello,

in this post : here Kevin & Patrick show how to create a tactic.

The example of the post is :

meta def AGL_ring : tactic unit :=
`[simp only [one_a, one_b, a_comp, b_comp], ring]

run_cmd add_interactive [`AGL_ring]

In the same post " make a group " there is also a question of tag : @ext and @simp !

So my question : is it possible to create a tactic (my_tactic) and a new tag and add gradually new lemma in my tactic ?

For example : add a new tag AGL_ring and gradualy add new lemma to my tactic !

Thx,

[Patrick Massot]

In this case you could use the builtin simp set feature.

[Rob Lewis]

The easiest way to do this would be with a custom simp attribute. https://leanprover-community.github.io/mathlib_docs/commands.html#mk_simp_attribute

[Patrick Massot]

Oh nice, I was searching for this link and Rob posted it.

[Rob Lewis]

You write run_cmd mk_simp_attribute AGL.

[orlando]

Perhaps my question is not clear :innocent:

I give my example :

import tactic
variables (R : Type)[comm_ring R]
structure R_exp :=
(a_0 : R)
(a_e : R)

namespace R_exp
@[ext] lemma ext : ∀ {g1 g2 : R_exp R}, g1.a_0 = g2.a_0 →  g1.a_e = g2.a_e  → g1 = g2 := λ g1 g2,
        begin
            intros h1,
            intros h2,
            cases g1,
            cases g2,
            congr ; try { assumption },   ---
        end
local notation R`[ε]` := R_exp R

def mod_ε (a : R[ε]) : R := a.a_0

instance has_coe :  has_coe(R[ε]) R := ⟨mod_ε(R)⟩  -- ? bof
/-
a ↦ a+ 0 ε
-/
def of(r : R) : R[ε] := {a_0 := r, a_e := 0}
lemma of_ext_0 (r : R) : ((of R r).a_0 = r)  := rfl
lemma of_ext_e (r : R) : ((of R r).a_e = 0)  := rfl
lemma coe_of (r : R) : ((of R r) : R) = r := rfl

/-
element : ε qui va vérifier :   ε^2 = 0
-/
def ε : R[ε]  := {a_0 := (0 : R), a_e := (1 : R)}
lemma ε_ext_0 : (ε R).a_0 = 0  := rfl
lemma ε_ext_e : (ε R).a_e = 1  := rfl
/-
Element : one !
-/
def one  : R[ε] := of R (1 : R)

instance : has_one (R[ε] ) := ⟨one R⟩
lemma one_ext_0 : (1 : R[ε]).a_0 = 1  := rfl
lemma one_ext_e : (1 : R[ε]).a_e = 0  := rfl

/-
Element !: 0
-/
def zero : R[ε] := of R (0 : R)
instance : has_zero (R[ε] ) := ⟨zero R⟩

lemma zero_ext_0 : (0 : R[ε]).a_0 = 0  := rfl
lemma zero_ext_e : (0 : R[ε]).a_e = 0  := rfl

/-
Addition :
-/
def add' :  (R[ε]) → (R[ε]) →  (R[ε]) := λ a b,  {a_0 := a.a_0+b.a_0, a_e := a.a_e +b.a_e}
instance : has_add (R[ε]) := ⟨add' R⟩
lemma add_ext_0 (a b : R[ε]) : (a+b).a_0 = a.a_0+ b.a_0 := rfl
lemma add_ext_e (a b : R[ε]) : (a+b).a_e = a.a_e+ b.a_e := rfl
/-
We want to show that add' give to R[ε] abelian group structure
we print the axiom !
-/
#print add_group
/-
There is a lot of axiom
-/
def neg' :  (R[ε]) → (R[ε]) := λ a, {a_0 := - a.a_0, a_e := -a.a_e}
instance : has_neg(R[ε]) := ⟨neg' R⟩
lemma neg_ext_0 (a : R[ε]) : (-a).a_0 = -a.a_0  := rfl
lemma neg_ext_e (a : R[ε]) : (-a).a_e = -a.a_e  := rfl

meta def add_ring : tactic unit :=
`[simp only [neg_ext_0, neg_ext_e, add_ext_0,of_ext_0,of_ext_e, add_ext_e,zero_ext_0,zero_ext_e,one_ext_0,one_ext_e], ring]

run_cmd add_interactive [`add_ring]
lemma add_assoc' (a b c : R[ε]) : a + b + c = a+(b+c) := begin
ext,
add_ring,
add_ring,
end

The problem is : i want next to define multiplication and there is new lemma to add to my tatic !

[Rob Lewis]

Then you can tag lemmas with @[AGL] lemma foo ...

[orlando]

Ah i don't see the answers ! Thx i read !

[Rob Lewis]

and your tactic can say simp only with AGL

[Patrick Massot]

He also wanted to tack ring at the end, hence the Kevin-style tactic.

[Rob Lewis]

Note, I misread my own documentation. You should write mk_simp_attribute AGL "describe what these rules are here"

[orlando]

Rob : i thinck i understand i add ring as Patrick mention !

import tactic
variables (R : Type)[comm_ring R]
structure R_exp :=
(a_0 : R)
(a_e : R)

namespace R_exp
run_cmd mk_simp_attr `AGL
meta def AGL_ring : tactic unit :=
`[simp only with AGL, ring]

run_cmd add_interactive [`AGL_ring]
@[ext] lemma ext : ∀ {g1 g2 : R_exp R}, g1.a_0 = g2.a_0 →  g1.a_e = g2.a_e  → g1 = g2 := λ g1 g2,
        begin
            intros h1,
            intros h2,
            cases g1,
            cases g2,
            congr ; try { assumption },   ---
        end
local notation R`[ε]` := R_exp R

def mod_ε (a : R[ε]) : R := a.a_0

instance has_coe :  has_coe(R[ε]) R := ⟨mod_ε(R)⟩  -- ? bof
/-
a ↦ a+ 0 ε
-/
def of(r : R) : R[ε] := {a_0 := r, a_e := 0}
@[AGL]lemma of_ext_0 (r : R) : ((of R r).a_0 = r)  := rfl
@[AGL]lemma of_ext_e (r : R) : ((of R r).a_e = 0)  := rfl
@[AGL]lemma coe_of (r : R) : ((of R r) : R) = r := rfl

/-
element : ε qui va vérifier :   ε^2 = 0
-/
def ε : R[ε]  := {a_0 := (0 : R), a_e := (1 : R)}
@[AGL]lemma ε_ext_0 : (ε R).a_0 = 0  := rfl
@[AGL]lemma ε_ext_e : (ε R).a_e = 1  := rfl
/-
Element : one !
-/
def one  : R[ε] := of R (1 : R)

instance : has_one (R[ε] ) := ⟨one R⟩
@[AGL]lemma one_ext_0 : (1 : R[ε]).a_0 = 1  := rfl
@[AGL]lemma one_ext_e : (1 : R[ε]).a_e = 0  := rfl

/-
Element !: 0
-/
def zero : R[ε] := of R (0 : R)
instance : has_zero (R[ε] ) := ⟨zero R⟩

@[AGL]lemma zero_ext_0 : (0 : R[ε]).a_0 = 0  := rfl
@[AGL]lemma zero_ext_e : (0 : R[ε]).a_e = 0  := rfl

/-
Addition :
-/
def add' :  (R[ε]) → (R[ε]) →  (R[ε]) := λ a b,  {a_0 := a.a_0+b.a_0, a_e := a.a_e +b.a_e}
instance : has_add (R[ε]) := ⟨add' R⟩
@[AGL]lemma add_ext_0 (a b : R[ε]) : (a+b).a_0 = a.a_0+ b.a_0 := rfl
@[AGL]lemma add_ext_e (a b : R[ε]) : (a+b).a_e = a.a_e+ b.a_e := rfl
/-
We want to show that add' give to R[ε] abelian group structure
we print the axiom !
-/
#print add_group
/-
There is a lot of axiom
-/
def neg' :  (R[ε]) → (R[ε]) := λ a, {a_0 := - a.a_0, a_e := -a.a_e}
instance : has_neg(R[ε]) := ⟨neg' R⟩
@[AGL]lemma neg_ext_0 (a : R[ε]) : (-a).a_0 = -a.a_0  := rfl
@[AGL]lemma neg_ext_e (a : R[ε]) : (-a).a_e = -a.a_e  := rfl


lemma add_assoc' (a b c : R[ε]) : a + b + c = a+(b+c) := begin
ext,
AGL_ring,
AGL_ring,
end


instance has_repr [has_repr R] : has_repr(R[ε])  := begin sorry, end


end R_exp

[Rob Lewis]

Looks good! But it's better style if you replace the line

run_cmd mk_simp_attr `AGL

with

mk_simp_attribute AGL "description"

where you describe what the set of AGL rules are supposed to do.

[Rob Lewis]

This isn't very important though. :)

[orlando]

Hum little change ! Thx Rob ! That's very good !

mk_simp_attribute R_exp_ "trivial simplification"
meta def R_exp__ring : tactic unit :=
`[iterate 2 { simp only with R_exp_, ring}]

[orlando]

Another little question : it's possible to simplify all this stuff ! I mean all the axiom result from the same command begin ext, R_exp__ring, end Is it possible to " factorise " all ?

import tactic
variables (R : Type)[comm_ring R]
structure R_exp :=
(a_0 : R)
(a_e : R)

namespace R_exp
mk_simp_attribute R_exp_ "trivial simplification"
meta def R_exp__ring : tactic unit :=
`[iterate 2 { simp only with R_exp_, ring}]

run_cmd add_interactive [`R_exp__ring]
@[ext] lemma ext : ∀ {g1 g2 : R_exp R}, g1.a_0 = g2.a_0 →  g1.a_e = g2.a_e  → g1 = g2 := λ g1 g2,
        begin
            intros h1,
            intros h2,
            cases g1,
            cases g2,
            congr ; try { assumption },   ---
        end
local notation R`[ε]` := R_exp R

def mod_ε (a : R[ε]) : R := a.a_0

instance has_coe :  has_coe(R[ε]) R := ⟨mod_ε(R)⟩  -- ? bof
/-
a ↦ a+ 0 ε
-/
def of(r : R) : R[ε] := {a_0 := r, a_e := 0}
@[R_exp_]lemma of_ext_0 (r : R) : ((of R r).a_0 = r)  := rfl
@[R_exp_]lemma of_ext_e (r : R) : ((of R r).a_e = 0)  := rfl
@[R_exp_]lemma coe_of (r : R) : ((of R r) : R) = r := rfl

/-
element : ε qui va vérifier :   ε^2 = 0
-/
def ε : R[ε]  := {a_0 := (0 : R), a_e := (1 : R)}
@[R_exp_]lemma ε_ext_0 : (ε R).a_0 = 0  := rfl
@[R_exp_]lemma ε_ext_e : (ε R).a_e = 1  := rfl

/-
Element !: 0
-/
def zero : R[ε] := of R (0 : R)
instance : has_zero (R[ε] ) := ⟨zero R⟩

@[R_exp_]lemma zero_ext_0 : (0 : R[ε]).a_0 = 0  := rfl
@[R_exp_]lemma zero_ext_e : (0 : R[ε]).a_e = 0  := rfl

/-
Addition :
-/
def add' :  (R[ε]) → (R[ε]) →  (R[ε]) := λ a b,  {a_0 := a.a_0+b.a_0, a_e := a.a_e +b.a_e}
instance : has_add (R[ε]) := ⟨add' R⟩
@[R_exp_]lemma add_ext_0 (a b : R[ε]) : (a+b).a_0 = a.a_0+ b.a_0 := rfl
@[R_exp_]lemma add_ext_e (a b : R[ε]) : (a+b).a_e = a.a_e+ b.a_e := rfl
/-
We want to show that add' give to R[ε] abelian group structure
we print the axiom !
-/
#print add_comm_group
/-
There is a lot of axiom
add_comm_group.add : Π {α : Type u} [c : add_comm_group α], α → α → α
add_comm_group.add_assoc : ∀ {α : Type u} [c : add_comm_group α] (a b c_1 : α), a + b + c_1 = a + (b + c_1)
add_comm_group.zero : Π (α : Type u) [c : add_comm_group α], α
add_comm_group.zero_add : ∀ {α : Type u} [c : add_comm_group α] (a : α), 0 + a = a
add_comm_group.add_zero : ∀ {α : Type u} [c : add_comm_group α] (a : α), a + 0 = a
add_comm_group.neg : Π {α : Type u} [c : add_comm_group α], α → α
add_comm_group.add_left_neg : ∀ {α : Type u} [c : add_comm_group α] (a : α), -a + a = 0
add_comm_group.add_comm : ∀ {α : Type u} [c : add_comm_group α] (a b : α), a + b = b + a
-/
def neg' :  (R[ε]) → (R[ε]) := λ a, {a_0 := - a.a_0, a_e := -a.a_e}
instance : has_neg(R[ε]) := ⟨neg' R⟩
@[R_exp_]lemma neg_ext_0 (a : R[ε]) : (-a).a_0 = -a.a_0  := rfl
@[R_exp_]lemma neg_ext_e (a : R[ε]) : (-a).a_e = -a.a_e  := rfl


lemma add_assoc' (a b c : R[ε]) : a + b + c = a+(b+c) := begin ext, R_exp__ring, end
lemma zero_add' (a : R[ε]) : 0 + a = a:= begin ext, R_exp__ring, end
lemma add_zero' (a : R[ε]) : a+ 0 = a:= begin ext, R_exp__ring, end
lemma add_left_neg'  (a : R[ε]) :  -a + a = 0 := begin ext,R_exp__ring, end
lemma add_comm'   (a b : R[ε]) :  a + b = b + a :=begin ext,R_exp__ring,end

#print comm_ring
/-
structure comm_ring : Type u → Type u
fields:
comm_ring.add : Π {α : Type u} [c : comm_ring α], α → α → α
comm_ring.add_assoc : ∀ {α : Type u} [c : comm_ring α] (a b c_1 : α), a + b + c_1 = a + (b + c_1)
comm_ring.zero : Π (α : Type u) [c : comm_ring α], α
comm_ring.zero_add : ∀ {α : Type u} [c : comm_ring α] (a : α), 0 + a = a
comm_ring.add_zero : ∀ {α : Type u} [c : comm_ring α] (a : α), a + 0 = a
comm_ring.neg : Π {α : Type u} [c : comm_ring α], α → α
comm_ring.add_left_neg : ∀ {α : Type u} [c : comm_ring α] (a : α), -a + a = 0
comm_ring.add_comm : ∀ {α : Type u} [c : comm_ring α] (a b : α), a + b = b + a
comm_ring.mul : Π {α : Type u} [c : comm_ring α], α → α → α
comm_ring.mul_assoc : ∀ {α : Type u} [c : comm_ring α] (a b c_1 : α), a * b * c_1 = a * (b * c_1)
comm_ring.one : Π (α : Type u) [c : comm_ring α], α
comm_ring.one_mul : ∀ {α : Type u} [c : comm_ring α] (a : α), 1 * a = a
comm_ring.mul_one : ∀ {α : Type u} [c : comm_ring α] (a : α), a * 1 = a
comm_ring.left_distrib : ∀ {α : Type u} [c : comm_ring α] (a b c_1 : α), a * (b + c_1) = a * b + a * c_1
comm_ring.right_distrib : ∀ {α : Type u} [c : comm_ring α] (a b c_1 : α), (a + b) * c_1 = a * c_1 + b * c_1
comm_ring.mul_comm : ∀ {α : Type u} [c : comm_ring α] (a b : α), a * b = b * a
-/
def mul'  : (R[ε]) → (R[ε]) →  (R[ε]) := λ a b,begin exact
{a_0 := a.a_0 * b.a_0, a_e := a.a_0 * b.a_e+ a.a_e * b.a_0}
end
instance : has_mul (R[ε]) := ⟨mul' R⟩
@[R_exp_]lemma mul_ext_0 (a b : R[ε]) : (a * b).a_0 = a.a_0 * b.a_0 := rfl
@[R_exp_]lemma mul_ext_e (a b : R[ε]) : (a*b).a_e =a.a_0 * b.a_e+ a.a_e * b.a_0 := rfl
lemma mul_assoc' ( a b c : R[ε]) : a * b * c = a * (b * c) := begin ext, R_exp__ring, end

def one  : R[ε] := of R (1 : R)

instance : has_one (R[ε] ) := ⟨one R⟩
@[R_exp_]lemma one_ext_0 : (1 : R[ε]).a_0 = 1  := rfl
@[R_exp_]lemma one_ext_e : (1 : R[ε]).a_e = 0  := rfl

lemma one_mul' (a : R[ε]) : 1 * a = a := begin ext, R_exp__ring,end
lemma mul_one' (a : R[ε]) : a * 1 = a := begin ext, R_exp__ring,end
lemma left_distrib' (a b c :  R[ε]) :  a * (b + c) = a * b + a * c := begin ext, R_exp__ring,end
lemma right_distrib' (a b c :  R[ε]) :  (a + b) *c = a * c + b * c := begin ext, R_exp__ring,end

lemma mul_comm' (a b : R[ε]) :  a * b = b * a := begin ext, R_exp__ring, end

instance : comm_ring (R[ε]) :=
  { add                  := add' R,
    add_assoc            := add_assoc' R,
    zero                 := 0,
    zero_add             := zero_add' R,
    add_zero             := add_zero' R,
    neg                  := neg' R,
    add_left_neg         := add_left_neg' R,
    add_comm             := add_comm' R,
    mul                  := mul' R,
    mul_assoc            := mul_assoc' R,
    one                  := 1,
    one_mul              := one_mul' R,
    mul_one              := mul_one' R,
    left_distrib         := left_distrib' R,
    right_distrib        := right_distrib' R,
    mul_comm             := mul_comm' R,
    }

instance has_repr [has_repr R] : has_repr(R[ε])  := begin sorry, end


end R_exp

[Kevin Buzzard]

These proofs look fine, but probably in mathlib you would not see it done like this; they would make the comm_ring structure by something like refine_struct (something); by ext; R_exp__ring and it would try this proof on all of the fields at once

[orlando]

i mean i would write

instance : comm_ring (R[ε]) := by ext, R_exp__ring,

Or something like that, without writing all the lemma just defining mul add one zero :yum:

[Kevin Buzzard]

For example see

instance to_complex.is_ring_hom : is_ring_hom to_complex :=
by refine_struct {..}; intros; apply complex.ext; simp [sub_eq_add_neg, to_complex]

in data.zsqrtd.gaussian_int

[orlando]

ok Kevin !!! thx i take a look :wink:

[Kevin Buzzard]

It is the same as your situation: they need to check 10 things, but it's always the same proof -- "ext, then automation"

[Kevin Buzzard]

so they do not even name the lemmas, they use this semicolon ; trick

[Patrick Massot]

Why don't you use a quotient ring?

[orlando]

hum good question Patrick, because i don't understand how to deal with 'mathlib quotient ring', i try to use but i think i loose all the control ! Probably i miss-understand something :confused:

[Patrick Massot]

In the long run I think you'll be much better with mathlib quotient rings.

[Kevin Buzzard]

I think it's a good exercise to do it like this, but of course quotient rings would be a much quicker way. But quotients are quite intimidating for beginners.

[Yury G. Kudryashov]

Also quotient ring won't give you a nice structure with two fields.

[orlando]

I explain my problem with mathlib tool : For example the next step with my $R[ \varepsilon ]$ is to create a functor $CommRing \to CommRing$ sendind $R \mapsto R[\varepsilon]$, with my construction if $\psi : R \to R'$, the action on $(a,b)$ is $( \psi(a),\psi(b))$ . If i use, quotient, the problem is that i spent hours dealing with 'mathlib construction' quotient map etc , tensor product etc !

Is that i mean by : i loose control. But i thinck i don't use mathlib in a good maner for the moment :confused:

[Kevin Buzzard]

If you don't define it as a quotient, then you will probably at some stage have to prove that given $f:R[X]\to A$ such that $f(X^2)=0$, there is an induced map $R[\epsilon]\to A$.

[Kevin Buzzard]

With the quotient definition you get this for free. But I agree, your approach has the advantage of being more concrete.

[orlando]

Yes Kevin ! The good stuff is to use the concret description and the mathlib construction via quotient ! Also, it's a good exercice for beginner, as you tell :grinning:

[orlando]

I add i little thing :

instance has_repr [has_repr R] : has_repr(R[ε])  := ⟨λ x,   repr x.a_0 ++ "+" ++ repr x.a_e ++ "ε"⟩
#eval (8+ε ℤ)^7 -- result  : 2097152+1835008ε

Is It possible to do the calculus with 'mathlib quotient' ?

[Kenny Lau]

no

[Kenny Lau]

Mario would say don't use quotient

[Kenny Lau]

Kevin would say use pari/gp for computations not Lean

[orlando]

yes !