## Stream: general

### Topic: tactic

#### orlando (Apr 07 2020 at 07:14):

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 (Apr 07 2020 at 07:41):

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

#### Rob Lewis (Apr 07 2020 at 07:41):

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 (Apr 07 2020 at 07:42):

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

#### Rob Lewis (Apr 07 2020 at 07:42):

You write run_cmd mk_simp_attribute AGL.

#### orlando (Apr 07 2020 at 07:42):

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

/-
-/
def add' :  (R[ε]) → (R[ε]) →  (R[ε]) := λ a b,  {a_0 := a.a_0+b.a_0, a_e := a.a_e +b.a_e}
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 !
-/
/-
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 :=

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


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

#### Rob Lewis (Apr 07 2020 at 07:42):

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

#### Rob Lewis (Apr 07 2020 at 07:43):

and your tactic can say simp only with AGL

#### Patrick Massot (Apr 07 2020 at 07:44):

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

#### Rob Lewis (Apr 07 2020 at 07:47):

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

#### orlando (Apr 07 2020 at 07:53):

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]

@[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

/-
-/
def add' :  (R[ε]) → (R[ε]) →  (R[ε]) := λ a b,  {a_0 := a.a_0+b.a_0, a_e := a.a_e +b.a_e}
@[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 !
-/
/-
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 (Apr 07 2020 at 07:57):

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 (Apr 07 2020 at 07:57):

This isn't very important though. :)

#### orlando (Apr 07 2020 at 08:06):

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 (Apr 07 2020 at 08:46):

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

@[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

/-
-/
def add' :  (R[ε]) → (R[ε]) →  (R[ε]) := λ a b,  {a_0 := a.a_0+b.a_0, a_e := a.a_e +b.a_e}
@[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 !
-/
/-
There is a lot of axiom
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[ε]) :=
zero                 := 0,
neg                  := neg' 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 (Apr 07 2020 at 08:49):

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 (Apr 07 2020 at 08:50):

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 (Apr 07 2020 at 08:51):

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 (Apr 07 2020 at 08:51):

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

#### Kevin Buzzard (Apr 07 2020 at 08:51):

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 (Apr 07 2020 at 08:52):

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

#### Patrick Massot (Apr 07 2020 at 09:15):

Why don't you use a quotient ring?

#### orlando (Apr 07 2020 at 09:19):

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 (Apr 07 2020 at 09:19):

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

#### Kevin Buzzard (Apr 07 2020 at 09:22):

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 (Apr 07 2020 at 09:23):

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

#### orlando (Apr 07 2020 at 09:28):

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 (Apr 07 2020 at 09:37):

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$.

#### orlando (Apr 07 2020 at 09:59):

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 (Apr 07 2020 at 10:10):

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' ?

no

#### Kenny Lau (Apr 07 2020 at 10:12):

Mario would say don't use quotient

#### Kenny Lau (Apr 07 2020 at 10:13):

Kevin would say use pari/gp for computations not Lean

#### orlando (Apr 07 2020 at 10:13):

yes !

Last updated: Aug 03 2023 at 10:10 UTC