Making a tactic more efficient

Stream: metaprogramming / tactics

[Andre Hernandez-Espiet (Rutgers)]

Hi all, I wrote the following tactics:

import data.real.basic
universes u1 u2
class incidence_geometry :=
(point : Type u1)
(line : Type u2)
(online : point → line → Prop)
(sameside : point → point → line → Prop)
(not_online_of_sameside : ∀ {a b : point}, ∀ {L : line}, sameside a b L → ¬online a L)

open incidence_geometry

instance incidence_geometry_ℝ_ℝ : incidence_geometry :=
{ point := ℝ × ℝ, -- p = (x, y)
  line := ℝ × ℝ × ℝ, -- a x + b y = c ↔ (a, b, c)
  online := sorry,
  sameside := sorry,
  not_online_of_sameside := sorry,
   }

variables[i: incidence_geometry]

theorem neq_of_online_offline {a b : point} {L : line} (aL : online a L) (bL : ¬online b L) : a ≠ b :=
begin
  intro ab, rw ab at aL, exact bL aL,
end

theorem side {a b c: point} {L: line} (bL: online b L) (acL: sameside a c L) : a≠ b
:=(neq_of_online_offline bL (not_online_of_sameside acL)).symm

meta def exact_list : list expr →  tactic unit
| [] := tactic.fail "no matching expression found"
| (h :: hs) :=
do {
tactic.applyc ``neq_of_online_offline,
tactic.exact h,
tactic.assumption
}
<|> exact_list hs

meta def exact_list2 : list expr →  tactic unit
| [] := tactic.fail "no matching expression found"
| (h :: hs) :=
do {
tactic.applyc ``side,
tactic.exact h,
tactic.assumption
}
<|> exact_list2 hs

meta def neq: tactic unit :=
do
hs ←  tactic.local_context,
(exact_list hs <|> exact_list2 hs)

theorem neqtest {a b c: point} {L: line} (bL: online b L) (acL: sameside a c L)  : a ≠ b :=
begin
  neq,
end

theorem neqtest2 {a b : point } {L: line} (aL: online a L) (bL: ¬ online b L) : a≠ b :=by neq

Basically, I made a tactic that tries the theorems side and neq_of_online_offline consecutively. However, I had to write exact_list2 in addition to exact_list in order to try both theorems. I feel like I'm missing an easy way to try as many theorems as I want with just two meta programs. Is there a way to make this work more efficiently?

[Heather Macbeth]

Have you looked at tactic#apply_rules ?

[Heather Macbeth]

@Andre Hernandez-Espiet (Rutgers) I looked a little more at your use case and it seems like you need to backtrack, not just apply the first lemma that fits. So you want the generalization tactic#solve_by_elim of apply_rules. Here:

import tactic

class incidence_geometry :=
(point : Type*)
(line : Type*)
(online : point → line → Prop)
(sameside : point → point → line → Prop)
(not_online_of_sameside : ∀ {a b : point}, ∀ {L : line}, sameside a b L → ¬online a L)

export incidence_geometry (online sameside not_online_of_sameside)

variables [i : incidence_geometry] {a b c : i.point} {L : i.line}

theorem neq_of_online_offline (aL : online a L) (bL : ¬online b L) :   a ≠ b :=
begin
  intro ab, rw ab at aL, exact bL aL,
end

theorem side (bL: online b L) (acL: sameside a c L) : a ≠ b :=
(neq_of_online_offline bL (not_online_of_sameside acL)).symm

/-- Tactic for deducing disequalities among points. -/
meta def neq : tactic unit := `[solve_by_elim [neq_of_online_offline, side]]

example (bL: online b L) (acL: sameside a c L) : a ≠ b := by neq

example (aL: online a L) (bL: ¬ online b L) : a ≠ b := by neq

[Heather Macbeth]

(Note: work on asking questions with #mwe -- everything in your question involving the reals was irrelevant.)

[Heather Macbeth]

In practice, you probably want something extensible, to which you can add more relevant lemmas as they accumulate. You can do this using the solve_by_elim option which brings in all lemmas marked with a certain attribute:

@[user_attribute]
meta def point_neq : user_attribute :=
{ name := `point_neq,
  descr := "lemmas usable to prove disequalities of points" }

/-- Tactic for deducing disequalities among points. -/
meta def neq : tactic unit := `[solve_by_elim with point_neq]

[Heather Macbeth]

Now tag each relevant lemma with @[point_neq] as you prove it.

@[point_neq] theorem side (bL: online b L) (acL: sameside a c L) : a ≠ b :=
(neq_of_online_offline bL (not_online_of_sameside acL)).symm

[Notification Bot]

Andre Hernandez-Espiet (Rutgers) has marked this topic as unresolved.

[Andre Hernandez-Espiet (Rutgers)]

I am going more with the Euclidean side. Working with Euclid's elements.

[Andre Hernandez-Espiet (Rutgers)]

Also, I feel like I'm missing something very silly. Why doesn't the example get proven by neq?

import tactic

class incidence_geometry :=
(point : Type*)
(line : Type*)
(online : point → line → Prop)
(B : point → point → point → Prop) -- Betweenness
(online_2_of_B : ∀ {a b c : point}, ∀ {L : line}, B a b c → online a L → online c L → online b L)

export incidence_geometry (online B online_2_of_B)

variables [i : incidence_geometry] {a b c d: i.point} {L : i.line}

@[user_attribute]
meta def point_neq : user_attribute :=
{ name := `point_neq,
  descr := "lemmas usable to prove disequalities of points" }

meta def neq : tactic unit := `[solve_by_elim with point_neq]

@[point_neq] theorem neq_of_online_offline (aL : online a L) (bL : ¬online b L) :   a ≠ b :=
begin
  intro ab, rw ab at aL, exact bL aL,
end

@[point_neq] theorem bet_nq (aL: online a L) (bL: online b L) (cL: ¬ online c L) (Bet: B a d b) : c≠ d :=
(neq_of_online_offline (online_2_of_B Bet aL bL) cL).symm

example (aL: online a L) (bL: online b L) (cL: ¬ online c L) (Bet: B a d b) : c≠ d := by neq

[Heather Macbeth]

@Andre Hernandez-Espiet (Rutgers) Increasing the "max depth" seems to work:

meta def neq : tactic unit := `[solve_by_elim with point_neq { max_depth := 5 }]

[Andre Hernandez-Espiet (Rutgers)]

For this small example this works. However, for my longer code I then get the error excessive memory consumption detected at 'expression equality test' (potential solution: increase memory consumption threshold) Any ideas on how to increase the threshold?

[Andre Hernandez-Espiet (Rutgers)]

I went to vscode's settings and changed the memory limit from 2GB to 12GB and it still gives the same issue, so this doesn't seem to be it...

[Heather Macbeth]

@Andre Hernandez-Espiet (Rutgers) Maybe something is looping ... I don't know but in any case I don't think it's a metaprogramming-specific issue; you could isolate it and ask on #general.