New `solve_by_elim`

Stream: mathlib4

[Heather Macbeth]

@Scott Morrison I was experimenting with the refactored solve_by_elim, particularly with the new functionality to throw in symms of hypotheses. I expected the following to work; can you tell me if I am doing something wrong?

import Mathlib.Data.Int.ModEq

example {a : ℤ} (ha : a ≡ 2 [ZMOD 4]) : 2 ≡ a [ZMOD 4] := by
  apply_rules only [ha] -- doesn't resolve the goal

The goal state after this is

a : ℤ
ha : a ≡ 2 [ZMOD 4]
ha_symm : 2 ≡ a [ZMOD 4]
⊢ 2 ≡ a [ZMOD 4]

so at least it correctly formed the symm of ha.

[Heather Macbeth]

I'm also curious why this one doesn't work:

import Mathlib.Data.Int.ModEq

example {a b : ℤ} (ha : a ≡ 2 [ZMOD 4]) :
    a * b ^ 2 + a ^ 2 * b ≡ 2 * b ^ 2 + 2 ^ 2 * b [ZMOD 4] := by
  apply_rules only [ha, Int.ModEq.add, Int.ModEq.mul,
    Int.ModEq.pow, Int.ModEq.rfl] -- doesn't resolve the goal

After it runs there is one goal left which ought to be doable by Int.ModEq.rfl:

a b : ℤ
ha : a ≡ 2 [ZMOD 4]
ha_symm : 2 ≡ a [ZMOD 4]
⊢ b ≡ b [ZMOD 4]

and it's strange because presumably it already resolved another b ≡ b [ZMOD 4] goal.

[Scott Morrison]

The first one is presumably a bug/feature that only doesn't pick up the symm version of that named lemma. I'll have to think about how to allow that.

[Heather Macbeth]

If it would be easier, we could have the syntax apply_rules only [←ha]

[Scott Morrison]

apply_rules only [←ha] seems a bit superfluous given apply_rules only [ha.symm] works.

[Scott Morrison]

I can change the behaviour of only so it automatically includes all the symmetric versions, but then I worry someone will want only only.

[Scott Morrison]

Regarding the second example,

example {a b : ℤ} (ha : a ≡ 2 [ZMOD 4]) :
    a * b ^ 2 + a ^ 2 * b ≡ 2 * b ^ 2 + 2 ^ 2 * b [ZMOD 4] := by
  apply_rules (config := {maxDepth := 13}) only [ha, Int.ModEq.add, Int.ModEq.mul,
    Int.ModEq.pow, Int.ModEq.rfl]

suffices.

[Scott Morrison]

We should probably increase the default maxDepth for apply_rules.

[Scott Morrison]

Reordering the lemmas as

example {a b : ℤ} (ha : a ≡ 2 [ZMOD 4]) :
    a * b ^ 2 + a ^ 2 * b ≡ 2 * b ^ 2 + 2 ^ 2 * b [ZMOD 4] := by
  apply_rules only [ha, Int.ModEq.rfl, Int.ModEq.add, Int.ModEq.mul,
    Int.ModEq.pow]

also works.

[Scott Morrison]

i.e. so it tries rfl on things before decomposing products and powers that match to begin with. I'm not sure if there is a sensible way to make these tactics try to find better orderings themselves. That's probably out of scope for now.

[Heather Macbeth]

Is there a reason to have a maxDepth for apply_rules at all? It seems like with a sensible rule set (no symms) there's no way it would loop.

[Scott Morrison]

Actually, given that we already have the config := { symm := false } option, maybe apply_rules only [ha] could reasonably use ha.symm as well, and you have to write apply_rules (config := {symm := false}) only [ha] for the only only behaviour!

[Scott Morrison]

It would be nice if we could have different defaults: default to symm := true normally, but default to symm := false when called with only. Then users could call apply_rules (config := { symm := true }) only [ha] if they wanted the "weird" behaviour of only + symm.

[Scott Morrison]

Heather Macbeth said:

Is there a reason to have a maxDepth for apply_rules at all? It seems like with a sensible rule set (no symms) there's no way it would loop.

Well, at some point we need a maxDepth, if only for implementation reasons. mathlib#1580 changes the default to 50. @Heather Macbeth, feel free to merge as is or change the default to anything else that suits you.

[Heather Macbeth]

mathlib4#1580

[Heather Macbeth]

From the solve_by_elim source:

(In mathlib3 we could also pass attributes, and all declarations with that attribute were included. This has not been implemented here.)

@Scott Morrison Would it be difficult to implement that functionality? It was very convenient in mathlib3.

To #xy a bit, a typical use case for me would be to implement a tactic

mod_rw [h1, h2]

which is a wrapper for

apply_rules only [h1, h2] using mod_rules

where mod_rules is an attribute which I have tagged Int.ModEq.add, Int.ModEq.mul, Int.ModEq.pow ... with. I'm not sure how to do this without the attribute functionality.

[Scott Morrison]

It's the usual problem, that there isn't a "standard" for looking up everything with an attribute. Presumably it would suffice if this worked with something created via register_simp_attr?

[Scott Morrison]

(Or alternatively some relative of this, like register_apply_attr that we make up? It would also potentially be useful for aesop.)

[Heather Macbeth]

I don't think the lemmas I will be tagging are technically suitable as simp-lemmas. But I'm happy to "abuse" the functionality in this way if it will work.

[Heather Macbeth]

Actually, can we just re-use the declare_aesop_rule_sets [mod_rules] functionality?

[Heather Macbeth]

Presumably that sets up an attribute which has most of the code needed already written.

[Scott Morrison]

aesop rule sets are much more complicated

[Heather Macbeth]

Do you have any ideas for a hack that could make my desired syntax

mod_rw [h1, h2]

work without the attribute functionality? Some kind of mini-tactic that

• appends a hard-coded list of lemmas to [h1, h2]
• runs apply_rules only on the resulting list

?

[Scott Morrison]

I'm writing register_tag_attr, for attributes which have no function except being able to look up everything so tagged.

[Heather Macbeth]

Scott Morrison said:

Reordering the lemmas also works.

By the way, when it comes to using register_tag_attr in apply_rules, it sounds like there will be a question of the relative priority of attribute-tagged lemmas vs lemmas listed individually by the user -- the tactic tries the lemmas in a fixed order, only trying a given lemma if all the previous lemmas failed.

In my own use cases it is better that the attribute-tagged lemmas be given lower priority than the individually-listed lemmas. In fact I am going to be bold and claim that this is better in most use cases.

[Scott Morrison]

Happily, this is what I implemented before reading this message. :-)

[Scott Morrison]

mathlib4#1581

[Scott Morrison]

@Heather Macbeth, there's a very simple test case

@[dummy_tag_attr] axiom foo : 1 = 2

example : 1 = 2 := by
  fail_if_success solve_by_elim
  solve_by_elim using dummy_tag_attr

but I haven't tested it any beyond that. Please let me know how it goes. :-)

[Heather Macbeth]

As far as I can tell, the attribute setup is working correctly. Thank you @Scott Morrison!

I did discover a separate weird behaviour, which I suspect might be because the mathlib3 option for a transparency setting is not implemented yet.

import Mathlib.Init.Data.Int.Basic
import Mathlib.Tactic.SolveByElim

def Int.ModEq (n a b : ℤ) := a % n = b % n

notation:50 a " ≡ " b " [ZMOD " n "]" => Int.ModEq n a b

theorem Int.ModEq.add (h₁ : a ≡ b [ZMOD n]) (h₂ : c ≡ d [ZMOD n]) :
    a + c ≡ b + d [ZMOD n] :=
  sorry

example {a b : ℤ} : a + b ≡ a + a [ZMOD 4] := by
  apply_rules [Int.ModEq.add]

[Heather Macbeth]

In mathlib3, apply_rules does what I want here, which is to leave the following goal state:

2 goals
a b : ℤ
⊢ a ≡ a [ZMOD 4]

a b : ℤ
⊢ b ≡ a [ZMOD 4]

In the mathlib4 implementation the goal state after the apply_rules is

a b : ℤ
⊢ HAdd.hAdd = fun {a b} => a + a

However, if I mark def Int.ModEq as @[irreducible], then I get back the mathlib3 behaviour. So I'm guessing that if apply_rules { md := reducible } were implemented then the mathlib4 version would do what I want.

[Heather Macbeth]

(In the mathlib3 apply_rules I always set { md := reducible }.)

[Heather Macbeth]

Hmm, actually it can't just be transparency level, because the discrepancy in behaviour persists even without any definitions or notations. Compare mathlib4

import Mathlib.Init.Data.Int.Basic
import Mathlib.Tactic.SolveByElim

variable {a b c d n : ℤ}

theorem Int.ModEq.add (h₁ : a % n = b % n) (h₂ : c % n = d % n) :
    (a + c) % n = (b + d) % n :=
  sorry

example : (a + b) % 4 = (a + a) % 4 := by
  apply_rules [Int.ModEq.add]

with mathlib3

import tactic.interactive

variables {a b c d n : ℤ}

theorem Int.ModEq.add (h₁ : a % n = b % n) (h₂ : c % n = d % n) :
    (a + c) % n = (b + d) % n :=
  sorry

example {a b : ℤ} : (a + b) % 4 = (a + a) % 4 :=
begin
  apply_rules [Int.ModEq.add],

end

[Heather Macbeth]

Note that in this example apply_rules [Int.ModEq.add] actually produces a different goal list than apply Int.ModEq.add.

[Heather Macbeth]

@Scott Morrison Aha! I think the change in behaviour is that apply_rules now has the following feature, from being implemented on top of solve_by_elim: per the source,

mkAssumptionSet builds a collection of lemmas for use in the backtracking search in solve_by_elim.

• By default, it includes all local hypotheses, along with rfl, trivial, congrFun and congrArg.

[Heather Macbeth]

Indeed, the term proof produced by the version which makes the weird goals

example : (a + b) % 4 = (a + a) % 4 := by
  apply_rules [Int.ModEq.add]
  sorry

includes congrFun and congrArg:

congrFun (congrArg HMod.hMod (congrFun (congrFun (sorryAx (HAdd.hAdd = fun {a b} => a + a)) a) b)) 4

Whereas with the only flag (which your docs say will omit those default lemmas from the applyset), i.e. running

example : (a + b) % 4 = (a + a) % 4 := by
  apply_rules only [Int.ModEq.add]
  . sorry
  . sorry

I get the goals I expected, and the term proof indeed has no congrArg or congrFun:

Int.ModEq.add (sorryAx (a % 4 = a % 4)) (sorryAx (b % 4 = a % 4))

[Heather Macbeth]

What would you think about changing the order of the collection of lemmas built by mkAssumptionSet, so that the default lemmas rfl, trivial, congrFun and congrArg are tried last (after lemmas provided by the user, local hypotheses, and lemmas tagged with listed attributes)? It seems like that would prevent the behaviour I observed here.

[Scott Morrison]

This change will conflict slightly with mathlib4#1581 which hasn't been merged yet, so I propose making this change part of that PR.

[Scott Morrison]

Done.

[Heather Macbeth]

Thank you!

[Heather Macbeth]

Scott Morrison said:

Heather Macbeth, there's a very simple test case

@[dummy_tag_attr] axiom foo : 1 = 2

example : 1 = 2 := by
  fail_if_success solve_by_elim
  solve_by_elim using dummy_tag_attr

but I haven't tested it any beyond that. Please let me know how it goes. :-)

@Scott Morrison OK, testing the attribute functionality a little more. How would I use an attribute in a macro, like the last line of the apply_rules macro? I tried writing

liftMetaTactic fun g => solveByElim.processSyntax cfg true star add remove #[`mod_rules] [g]

but it complains that mod_rules is a Name, not an Ident.

[Heather Macbeth]

(I can provide the full macro if needed, but it's pretty close to the apply_rules macro except that I want to hard-code a choice of attribute.)

[Thomas Murrills]

Was scrolling through old messages and saw this, so it might be resolved by now, but if that's the error, does mkIdent `mod_rules work?

[Mario Carneiro]

it does (solved in PMs)