Lean 4 tactic writing tutorial

Stream: general

[Patrick Massot]

Nice series of blog posts! I think you should make it clear that this is not about using tactics but about writing tactics. Otherwise it is a bit strange to read you complain about documentation only to realize later you are talking about super advanced usage (tactic writing) documentation.

[Patrick Massot]

It would be even nicer if you could find less artificial examples. All the issues you face in those examples come from stating lemmas in a very unusable way. I mean unusable first when proving them but mostly when using them. Did you notice you almost never see conjunctions as conclusions of lemmas in mathlib? And I think you would have a very hard time finding a lemma in mathlib whose conclusion is ten conjunctions like your example. Trying to use such a lemma would be a nightmare because accessing the individual pieces would be very difficult.

[Patrick Massot]

Here is a slightly cleanup version of your file anyway (since each post ends with a request for improvement suggestions).

import Mathlib.Data.Real.Basic

universe u1 u2 u3
class incidence_geometry :=
(point : Type u1)
(line : Type u2)
(circle : Type u3)

(length : point → point → ℝ)
(B : point → point → point → Prop) -- Betweenness

(length_nonneg : ∀ (a b : point), 0 ≤ length a b)
(length_symm : ∀ (a b : point), length a b = length b a)
(length_eq_zero_iff : ∀ {a b : point}, length a b = 0 ↔ a = b)
(length_sum_of_B : ∀ {a b c : point},
   B a b c → length a b + length b c = length a c)
(ne_12_of_B : ∀ {a b c : point}, B a b c → a ≠ b )
(ne_13_of_B : ∀ {a b c : point}, B a b c → a ≠ c )
(ne_23_of_B : ∀ {a b c : point}, B a b c → b ≠ c )

variable [incidence_geometry]
open incidence_geometry

lemma len_pos_of_neq (ab : a ≠ b) : 0 < length a b :=
  Ne.lt_of_le' (length_eq_zero_iff.not.mpr ab) (length_nonneg a b)

theorem incidence_geometry.B.length_pos (Babc : B a b c) :
      0 < length a b :=
  len_pos_of_neq (ne_12_of_B Babc)

theorem incidence_geometry.B.ne_12 (Babc : B a b c) : a ≠ b := ne_12_of_B Babc

theorem incidence_geometry.B.ne_23 (Babc : B a b c) : b ≠ c := ne_23_of_B Babc

theorem incidence_geometry.B.ne_13 (Babc : B a b c) : a ≠ c := ne_13_of_B Babc

theorem length_sum_perm_of_B' (Babc : B a b c) :
      0 < length a b ∧ 0 < length b a := by
   simp [length_symm b, Babc.length_pos]

theorem length_sum_perm_of_B (Babc : B a b c) :
      0 < length a b ∧ 0 < length b a ∧ 0 < length b c ∧
      0 < length c b ∧ 0 < length a c ∧ 0 < length c a ∧
      length a b + length b c = length a c ∧
      length b a + length b c = length a c ∧
      length b a + length c b = length a c ∧
      length b a + length b c = length c a ∧
      length b a + length c b = length c a ∧
      length a b + length c b = length a c ∧
      length a b + length b c = length c a ∧
      length a b + length c b = length c a
   := by
  simp [length_sum_of_B Babc, B.length_pos, Babc.ne_12, Babc.ne_13, Babc.ne_23,
        len_pos_of_neq, length_symm b a, length_symm c a, length_symm c b]

[Patrick Massot]

For completeness I should make sure you know about @Julien Narboux's work on formalization of synthetic Euclidean geometry, see https://dpt-info.u-strasbg.fr/~narboux/publications.html. In particular https://inria.hal.science/hal-00989781/file/small-scale-automation-Tarski-proceedings.pdf for less naive tactics handling permutation (your tactic will only work if you have a betweenness assumption miraculously listing the point in the order you enforce in your tactic).

[Patrick Massot]

@Ian Jauslin those blog post refer to your project, but this line makes it impossible to use. Mathlib is moving too fast, you can't simply to tell people to install the latest mathlib and hope for the best. The best will never happen here.

[Patrick Massot]

You need to put a specific mathlib commit, just as with André's project two lines below.

[Sebastian Ullrich]

This is the role of lake-manifest.json, which needs to be committed as well for this reason

[Notification Bot]

7 messages were moved here from #announce > Lean 4 tactics tutorial by Sebastian Ullrich.

[Vláďa Sedláček]

Patrick Massot said:

For completeness I should make sure you know about Julien Narboux's work on formalization of synthetic Euclidean geometry, see https://dpt-info.u-strasbg.fr/~narboux/publications.html. In particular https://inria.hal.science/hal-00989781/file/small-scale-automation-Tarski-proceedings.pdf for less naive tactics handling permutation (your tactic will only work if you have a betweenness assumption miraculously listing the point in the order you enforce in your tactic).

Thanks a lot! I'll definitely check this out and try to think about improving the tactics as well as finding more natural examples (ideally unsolvable by simp alone). I've incorporated your other points.

[Mario Carneiro]

@Vladimír Sedláček you can simplify your example in part 3 to:

import Lean

namespace Lean.Elab.Tactic

def getFVars (e : Expr) : Array FVarId :=
  (Lean.collectFVars {} e).fvarIds

elab "length_nf" : conv => withMainContext do
  let tgt ← instantiateMVars (← Conv.getLhs)
  let n1 ← ((getFVars (Lean.Expr.getArg! tgt 1)).get! 0).getUserName
  let n2 ← ((getFVars (Lean.Expr.getArg! tgt 2)).get! 0).getUserName
  if n2.lt n1 then
    evalTactic (← `(tactic| rw [@length_symm _ _] ))

end Lean.Elab.Tactic

[Mario Carneiro]

An alternative to the splitAll tactic you wrote is repeat' constructor, repeat' is like repeat but it recurses on all subgoals generated by the tactic instead of just the first one

[Mario Carneiro]

The fact that you had to implement perm at * separately seems like a bug in conv, conv at * => ... should work

[Ian Jauslin]

@Patrick Massot Thanks. I guess I'm too much of an optimist...

[Vláďa Sedláček]

@Mario Carneiro Thanks! I've finally incorporated your comments. conv at * => ... doesn't seem to work (throws expected identifier) even in other contexts though, do you have any idea what could be wrong with it?

[Mario Carneiro]

"It should work" in the sense "someone should write a PR to make it work"

[Utensil Song]

In case anyone found this thread but not the posts (like me), the 4 great posts are here: https://www.vladasedlacek.cz/en/posts/lean-01-intro ( found here )