change in `simp` behaviour

Stream: lean4

[Kevin Buzzard]

I will be the first to admit that I know absolutely nothing about how simp works. Is it expected that this code

def foo (a b : Prop) : Prop := sorry

theorem foo.comm {a b : Prop} : foo a b ↔ foo b a := sorry

theorem foo.left_comm {a b c : Prop} : foo a (foo b c) ↔ foo b (foo a c) := sorry

theorem foo.right_comm {a b c : Prop} : foo (foo a b) c ↔ foo (foo a c) b :=
by simp only [foo.comm, foo.left_comm]

works in Lean 3 but not in Lean 4? Is telling simp about foo.comm basically a lottery? [PS foo:=and, this is a proof in logic.basic without the notation]

[Mario Carneiro]

it looks like it worked, the two sides are the same

[Mario Carneiro]

it's just missing iff.refl

[Mario Carneiro]

attribute [refl] iff.rfl

doesn't work because iff.rfl doesn't exist and neither does @[refl]

[Mario Carneiro]

the rfl tactic is also now simply exact rfl instead of looking up the refl lemma and so on

[Mario Carneiro]

this will probably need mathlib prelude work

[Ryan Lahfa]

Mario Carneiro said:

attribute [refl] iff.rfl

doesn't work because iff.rfl doesn't exist and neither does @[refl]

Doesn't Iff.rfl exist?

[Mario Carneiro]

silly me

[Ryan Lahfa]

I had to exact Iff.rfl on some a <=> aalas, but was wondering if there was a better way to do it

[Kevin Buzzard]

It's iff_self : a ↔ a ↔ true which is missing

[Mario Carneiro]

in lean 3, this is handled by the refl tactic, which is automatically called with reducible reducibility by simp and rw

[Mario Carneiro]

Adding iff_self_iff_true to the simp only list will also fix it in this case, although I guess exact Iff.rfl is shorter

[Kevin Buzzard]

I noticed today that rw will try Eq.refl when it finishes in Lean 4 but not Iff.refl.

[Ryan Lahfa]

Kevin Buzzard said:

I noticed today that rw will try Eq.refl when it finishes in Lean 4 but not Iff.refl.

Correct, I wished it would, is this also a simp-lemmas list thing?

[Mario Carneiro]

it uses

private def withCheapRefl (tac : Syntax) : MacroM Syntax :=
  `(tactic| $tac; try (withReducible rfl))

[Mario Carneiro]

where rfl is the tactic

macro "rfl" : tactic => `(exact rfl)

[Mario Carneiro]

so there really isn't anything fancy here

[Mario Carneiro]

It is not clear to me whether overriding the rfl tactic will make withCheapRefl change behavior

[Kevin Buzzard]

I think that in Lean 3 Lean tries refl after a rw, and refl will solve any R a a goal if R is tagged @[refl]. But we can't make user tags right now. I have

syntax "refl" : tactic

macro_rules
  | `(tactic| refl) => `(tactic| apply Eq.refl)

macro_rules
  | `(tactic| refl) => `(tactic| apply Iff.refl)

in git@github.com:kbuzzard/mathlib4_experiments.git

[Mario Carneiro]

you should try using rfl instead of refl and override the existing one

[Mario Carneiro]

There is a funny new way of adding dynamic lists to the environment using initialize though

[Mario Carneiro]

you might need special commands if we can't declare attributes though

[Sebastian Ullrich]

Mario Carneiro said:

It is not clear to me whether overriding the rfl tactic will make withCheapRefl change behavior

It should! Tactics are really just macros and can be extended/overridden in the same way (see also our macro paper). I'll leave it to you to evaluate whether that is a good idea in this case.

[Mario Carneiro]

I assume that this only applies to macro-based tactics, though. I expect most tactics will be written as actual metaprograms, similar to lean 3, unless they are really trivial, and I assume that if you make it a program then you are actually calling a specific function when you refer to a subroutine, not calling into a forward reference in the macro system

[Sebastian Ullrich]

You can make it a forward reference using evalTactic. You may want to avoid that in the hot part of the code, but at that point you're probably calling function that don't have a tactic syntax anyway.