rw vs simp | default arguments for hypothesis

Stream: new members

[Tobias Grosser]

I am currently playing with the following code:

lemma pow_pred_mul {x y : Nat } (h : 0 < y := by omega) :
    x ^ (y - 1) * x = x ^ y := by
  simp only [← pow_succ, gt_iff_lt, ne_eq, not_false_eq_true]
  rw [Nat.sub_add_cancel]
  omega

theorem this_works {y : Nat} (h : 0 < y) :
    2 ^ (y - 1) * 2 = 2 ^ y := by
  simp [pow_pred_mul h] -- This works

theorem this_does_not_work {x y : Nat} (h : 0 < y) :
    2 ^ (y - 1) * 2 = 2 ^ y := by
  simp [pow_pred_mul] -- This does not work

theorem this_also_works {x y : Nat} (h : 0 < y) :
    2 ^ (y - 1) * 2 = 2 ^ y := by
  rw [pow_pred_mul] -- this_also_works

I would like for the this_does_not_work example to work the same way as the this_also_works example. Meaning, i would have hoped that simp could automatically pick up the correct hypothesis. I guess there is a reason it does not do this. Could someone help me with some background here?

[Julian Berman]

I don't know enough to provide said context (I assume you're asking why using simp doesn't try to fill in the hypothesis needed using your default discharger that you wrote in pow_pred_mul, if I recall the terminology correctly) -- just to note though, simp [h, pow_pred_mul] works as well, if that happens to suit you.

[Tobias Grosser]

Ah, this is interesting, Therefore simp [h, pow_pred_mul] as well as simp_all [pow_pred_mul] also work.

[Tobias Grosser]

I guess my conclusion is then that it is not best-practice to include the := omega in the @[simp] theorem, as simp can add h automatically as long as its part of the simp set. To get it there I should use one of the three, simp [h], simp [*], or simp_all.

[Tobias Grosser]

Thank you, this input was quite useful.

[Julian Berman]

I think that sounds right based on what I've seen, though I suspect it's still an interesting question to ask from someone who knows more about how the simplifier works as to why simp -- when it encounters a lemma which has a default discharger -- can't try applying the lemma and seeing whether it type checks after the default argument gets filled in. The answer seems like it may be "performance" I guess?, but I'd still be curious to hear.

[Julian Berman]

Maybe it's not too nice considering whatever tactic is there can potentially do arbitrarily slow amounts of work?

[Tomas Skrivan]

You can specify custom discharger i.e. a tactic that tries to close assumptions of simp theorems. In this example it is sufficient to use assumption

theorem works_with_assumption {x y : Nat} (h : 0 < y) :
    2 ^ (y - 1) * 2 = 2 ^ y := by
  simp (disch:=assumption) [pow_pred_mul]

you can also directly call apply h

theorem works_with_apply {x y : Nat} (h : 0 < y) :
    2 ^ (y - 1) * 2 = 2 ^ y := by
  simp (disch:=apply h) [pow_pred_mul]

When the hypothesis h does not fit the exactly the assumption you might have to use more powerful tactic like aesop

theorem works_with_aesop {x y : Nat} (h : 0 < y) :
    2 ^ (y^2 - 1) * 2 = 2 ^ (y^2) := by
  simp (disch:=aesop) [pow_pred_mul]

To diagnose this kind of problem it is useful to use option

set_option trace.Meta.Tactic.simp.discharge true

which on this_does_not_work produces this trace:

trace

[Meta.Tactic.simp.discharge] tsub_eq_zero_of_le discharge ❌
      y ≤ 1 ▶

[Meta.Tactic.simp.discharge] Nat.sub_eq_zero_of_le discharge ❌
      y ≤ 1 ▶

[Meta.Tactic.simp.discharge] pow_pred_mul discharge ❌
      autoParam (0 < y) _auto✝

[Julian Berman]

But that discharger in simp's config is "global" to all the lemmas simp tries to use obviously right? In theory might each lemma not know best as to what tactics are best suited to discharging their hypotheses automatically?

[Tomas Skrivan]

Yes it is a global discharger for all lemmas.

On my to-do list is to write a tactic/discharger that executes the tactic provided by auto parameter which would exactly run the most appropriate tactic for a particular argument of a particular theorem.

[Tomas Skrivan]

This would of course require to go over all the theorems and add appropriate auto parameters.

[Tobias Grosser]

I wonder if one could somehow do this using some kind of matching machinery? Or somehow derive these from data than doing it all manually.

[Tobias Grosser]

Or maybe a mix. This sounds definitely interesting.

[Tomas Skrivan]

I often run (disch:=aesop) and just rely that aesop is smart enough to pick what ever strategy it thinks is the best.