Difference in `simp` behaviour

Stream: mathlib4

[Chris Hughes]

The following proof works in Lean3 but not Lean4. I'm a bit surprised that it does work in Lean3, but the fact that it doesn't work breaks a bunch of proofs in Data.Set.Basic. What's the best fix to this?

import logic.basic

example (p : Prop) (q : p → Prop) (h : p) :
  (∀ (h2 : p), q h2) ↔ q h :=
by simp only [h, forall_true_left]

[Kevin Buzzard]

The problem seems to be the following:

import logic.basic

example (p : Prop) (q : p → Prop) (h : p) :
    (∀ (h2 : p), q h2) ↔ q h :=
begin
  have foo : p = true := by simp only [h],
  simp only [foo], -- `⊢ (∀ (h : true), q _) ↔ q h`
  simp only [iff_self, forall_true_left],
end

The simp only [foo] line works in Lean 3, but does nothing in Lean 4:

import Mathlib.Logic.Basic

example (p : Prop) (q : p → Prop) (h : p) :
    (∀ (h2 : p), q h2) ↔ q h := by
  have foo : p = True := by simp only [h]
  simp only [foo] -- no change in goal in Lean 4
  -- rw [foo] -- motive not type correct :-/
  subst foo
  simp -- works fine now

[David Renshaw]

This vaguely reminds me of https://github.com/leanprover/lean4/issues/1549

[David Renshaw]

I wonder if there's a way to add a type annotation to make it work (like this workaround).

[Scott Morrison]

Can we #mwe this for an issue on the Lean 4 repo?

[Jakob von Raumer]

slightly shorter but not much

example (q : p → Prop) (h : p = True)
  (h' : ∀(q : True → Prop), (∀ x, q x) ↔ q True.intro) : (∀ h', q h') ↔ q (h.symm ▸ trivial) := by
  simp only [h, h'] -- no change in goal in Lean 4
  -- rw [h] -- motive not type correct :-/
  subst h
  simp [h'] -- works fine now

[Jakob von Raumer]

I'll file it. I noticed this a few months ago as well but thought it was just a lack of @[simp]s

[Scott Morrison]

It would be best if you can minimise this so it doesn't include Mathlib at all

[Scott Morrison]

Just copy-paste anything needed from Logic.Basic. The Lean 4 devs will need a test case.

[Jakob von Raumer]

Right, edited

[Scott Morrison]

Just adding the link to Jakob's issue here: https://github.com/leanprover/lean4/issues/1926

[Heather Macbeth]

In #903 I encountered a bug which I think is related. If someone can sanity-check this then I'll add it to the issue Jakob opened. The following fails in Lean 4 but works in Lean 3:

example (P Q R : Prop) (hQ : Q = False) (hR : R = False) : P ∨ Q ↔ P ∨ R :=
by simp only [hQ, hR]

[Yakov Pechersky]

Does adding docs#iff_self to the list help?

[Heather Macbeth]

It does, but that doesn't seem to explain the difference between the Lean 3 and Lean 4 behaviour?

[Kevin Buzzard]

Lean 3:

set_option trace.simplify.rewrite true

example (P Q R : Prop) (hQ : Q = false) (hR : R = false) : P ∨ Q ↔ P ∨ R :=
by simp only [hQ, hR] -- works
/-
debugging output:

0. [simplify.rewrite] [hQ]: Q ==> false
0. [simplify.rewrite] [hR]: R ==> false
-/

-- but
example (P : Prop) : P ∨ false ↔ P ∨ false := by simp only -- fails

Lean 3 simp is doing some kind of magic. Is it trying refl if a rewrite succeeds or something?

[Heather Macbeth]

It's strange because P ∨ false ↔ P ∨ false isn't even true by refl!

[Heather Macbeth]

Or more precisely, it's true by refl but not with rfl. Maybe that's an important difference.

[Yaël Dillies]

It's true by docs#iff.rfl

[Yaël Dillies]

Maybe a missing @[refl] tag on Iff.rfl?

[Yaël Dillies]

Oh i guess not, because refl works here. Sorry, got Lean 3 and Lean 4 confused.

[Kevin Buzzard]

I think that lean 3 rw tries tactic refl if it succeeds.

[Heather Macbeth]

example (P : Prop) : P ∨ False ↔ P ∨ False := by rfl

fails in Lean 4, but

example (P : Prop) : P ∨ false ↔ P ∨ false := by refl

succeeds in Lean 3.

[Kevin Buzzard]

Regarding the initial issue of rewriting under binders: the minimised example in the github issue doesn't work in lean 3 either without imports. In fact it seems that import logic.basic changes the behaviour of simp only. This surprised me! Lean 3 code:

import logic.basic

example (p : Prop) (q : p → Prop) (h : p) :
    (∀ (h2 : p), q h2) ↔ q h := by {
  have foo : p = true := by simp only [h],
                   -- goal currently  `⊢ (∀ (h2 : p), q h2) ↔ q h`
  simp only [foo], -- goal changes to `⊢ (∀ (h : true), q _) ↔ q h`
  sorry,
    }

If you comment out the mathlib3 import, simp only [foo] fails to make progress. So the mathlib import is changing the behaviour of simp only. How?? Note that this means that the original issue in this conversation might not be a Lean 4 issue at all, perhaps mathlib3 is doing something clever which mathlib4 isn't doing. Note in particular that the claim in the lean 4 issue that lean 3 does something different is incorrect as it stands, and also the original issue Chris posted is behaving the same way in bare lean 3 and bare lean 4; it's only when mathlib gets involved that simp only becomes more powerful in lean 3.

[Kevin Buzzard]

Got it: (again this is Lean 3 code)

-- comment out this lemma to make `simp only [foo]` fail below
@[congr] lemma forall_prop_congr' {p p' : Prop} {q q' : p → Prop}
  (hq : ∀ h, q h ↔ q' h) (hp : p ↔ p') : (∀ h, q h) = ∀ h : p', q' (hp.2 h) :=
sorry

example (p : Prop) (q : p → Prop) (h : p) :
    (∀ (h2 : p), q h2) ↔ q h := by {
  have foo : p = true := by simp only [h],
                   -- goal currently  `⊢ (∀ (h2 : p), q h2) ↔ q h`
  simp only [foo], -- goal changes to `⊢ (∀ (h : true), q _) ↔ q h`
  sorry,
    }

So adding a congr lemma can change the behaviour of simp only in Lean 3 and this is perhaps the real cause of the original issue.

[Heather Macbeth]

Nice detective work. Inter alia, you're saying that my issue is not related to Jakob's issue, right?

[Kevin Buzzard]

Tactic rfl in Lean 4 only tries eq.refl because it was written before the @[refl] attribute. I haven't got back to your issue yet but I'll get there :-)

[Kevin Buzzard]

Chris' original issue in Lean 3:

@[simp] lemma forall_true_left (p : true → Prop) : (∀ x, p x) ↔ p true.intro :=
sorry

example (p : Prop) (q : p → Prop) (h : p) :
  (∀ (h2 : p), q h2) ↔ q h :=
by simp only [h, forall_true_left] -- fails


@[congr] lemma forall_prop_congr' {p p' : Prop} {q q' : p → Prop}
  (hq : ∀ h, q h ↔ q' h) (hp : p ↔ p') : (∀ h, q h) = ∀ h : p', q' (hp.2 h) :=
sorry

example (p : Prop) (q : p → Prop) (h : p) :
  (∀ (h2 : p), q h2) ↔ q h :=
by simp only [h, forall_true_left] -- works

[Notification Bot]

16 messages were moved here from #mathlib4 > Difference in simp behaviour by Heather Macbeth.

[Notification Bot]

16 messages were moved from this topic to #mathlib4 > simp (or refl?) difference Lean 3/4 by Heather Macbeth.

[Heather Macbeth]

OK, I think I disaggregated the messages :)

[Heather Macbeth]

So do we want to be tagging every congr lemma in mathlib4 with simp? Or is there a better fix?

[Kevin Buzzard]

What is weirding me out is that this congr lemma is changing the behaviour of simp only!

[Kevin Buzzard]

From mathlib4:

-- Porting note: `@[congr]` commented out for now.
-- @[congr]
theorem forall_prop_congr' {p p' : Prop} {q q' : p → Prop} (hq : ∀ h, q h ↔ q' h) (hp : p ↔ p') :
    (∀ h, q h) = ∀ h : p', q' (hp.2 h) :=
  propext (forall_prop_congr hq hp)

;-)

attribute [congr] forall_prop_congr'
/-
invalid 'congr' theorem, equality left/right-hand sides must be applications of the same function
  (∀ (h : ?p), ?q h) = ∀ (h : ?p'), ?q' (_ : ?p)
-/

:-(

[Mario Carneiro]

congr lemmas are not selected by simp only, it always uses all of them

[Kevin Buzzard]

Do you have any idea why we can't tag forall_prop_congr' with @[congr] in Lean 4 whereas we could in Lean 3? Are we doomed to a life of simp [...] with lean_3_congr_simps_which_arent_congr_in_lean_4?

[Mario Carneiro]

because no one has filed a bug report for this yet

[Kevin Buzzard]

-- lean 3

@[simp] lemma forall_true_left (p : true → Prop) : (∀ x, p x) ↔ p true.intro :=
sorry

@[simp] lemma forall_prop_congr' {p p' : Prop} {q q' : p → Prop}
  (hq : ∀ h, q h ↔ q' h) (hp : p ↔ p') : (∀ h, q h) = ∀ h : p', q' (hp.2 h) :=
sorry

-- uncomment to fix
-- attribute [congr] forall_prop_congr'

example (p : Prop) (q : p → Prop) (h : p) :
  (∀ (h2 : p), q h2) ↔ q h :=
by simp only [h, forall_true_left, forall_prop_congr'] -- still fails

[Kevin Buzzard]

It's more than "just add this as a simp lemma"

[Mario Carneiro]

yeah simp doesn't take congr lemmas as input at all

[Kevin Buzzard]

Mario Carneiro said:

because no one has filed a bug report for this yet

I added some comments at https://github.com/leanprover/lean4/issues/1926 -- does that count as filing a bug report?

[Mario Carneiro]

if you put them in the simp list they will be treated as simp lemmas, not congr lemmas

[Mario Carneiro]

I think so... you just have to make sure that the issue being solved implies this problem is also solved

[Mario Carneiro]

because leo likes closing issues :)

[Patrick Massot]

Who doesn't?

[Jakob von Raumer]

As soon as I find the time I'll try to see what happens if one just disables the check here which prevents forall_prop_congr' to be marked as [congr]...

[Scott Morrison]

@Jakob von Raumer, I disabled it in a branch: https://github.com/leanprover/lean4/compare/master...semorrison:lean4:disable_congr_check?expand=1

We would need to include a test including @[congr] theorem forall_prop_congr` .

[Jakob von Raumer]

It's funny that for most purposes, ∀ behaves like a normal function Forall : (α : Type) → (α → Prop) → Prop

[Scott Morrison]

I added the test, which failed:

[Scott Morrison]

https://github.com/leanprover/lean4/pull/1942

[Scott Morrison]

Oh, that's unfortunate, closing the PR deleted the CI outputs?

[Scott Morrison]

Ah, here it is:

[Scott Morrison]

https://github.com/leanprover/lean4/actions/runs/3671852401/jobs/6207473096#step:11:1914

[Scott Morrison]

[02:15 (00.050441)] lean-test-stage1>  664/1623 Test  #664: leanruntest_1926.lean .....................................***Failed    0.13 sec
[02:15 (00.000713)] lean-test-stage1> Unexpected return code 1 executing 'lean -j 0 -Dlinter.all=false 1926.lean'; expected 0. Output:
[02:15 (00.000481)] lean-test-stage1> 1926.lean:1:8: warning: declaration uses 'sorry'
[02:15 (00.000441)] lean-test-stage1> 1926.lean:3:8: warning: declaration uses 'sorry'
[02:15 (00.000451)] lean-test-stage1> 1926.lean:7:11: error: invalid 'congr' theorem, argument #1 of parameter #5 contains unresolved parameter
[02:15 (00.000655)] lean-test-stage1>   ?p
[02:15 (00.000768)] lean-test-stage1> 1926.lean:11:0: error: unsolved goals
[02:15 (00.000384)] lean-test-stage1> p : Prop
[02:15 (00.000408)] lean-test-stage1> q : p → Prop
[02:15 (00.000429)] lean-test-stage1> h : p
[02:15 (00.000446)] lean-test-stage1> ⊢ (∀ (h2 : p), q h2) ↔ q h

[Scott Morrison]

So there's still a later step where this lemma would be rejected by @[congr].

[Jakob von Raumer]

Would this not be a way around it?

def propForall {p : Prop} (q : p → Prop) : Prop := ∀ x, q x

@[simp] theorem forall_eq_forall_iff {p p' : Prop} {q : p → Prop} {q' : p' → Prop} :
  ((∀ x, q x) = (∀ x, q' x)) ↔ propForall q = propForall q' :=
⟨(·), (·)⟩

@[congr] theorem propForall_prop_congr' {p p' : Prop} {q q' : p → Prop}
  (hq : ∀ h, q h ↔ q' h) (hp : p ↔ p') :
    propForall q = propForall (fun h => q' (hp.2 h)) :=
sorry --propext (forall_prop_congr hq hp)

[Scott Morrison]

I'm out of time for now: would you mind editing my PR to use that test?

[Jakob von Raumer]

Will do

[Jakob von Raumer]

So this works:

def propForall {p : Prop} (q : p → Prop) : Prop := ∀ x, q x

@[simp] theorem forall_eq_propForall {p : Prop} (q : p → Prop) : (∀ x, q x) ↔ propForall q :=
Iff.rfl

@[simp] theorem propForall_true_left : ∀ (p : True → Prop), propForall p ↔ p True.intro :=
sorry

@[congr] theorem propForall_prop_congr' {p p' : Prop} {q q' : p → Prop}
  (hq : ∀ h, q h ↔ q' h) (hp : p ↔ p') :
    propForall q = propForall (fun h => q' (hp.2 h)) :=
sorry --propext (forall_prop_congr hq hp)

example (p : Prop) (q : p → Prop) (h : p) :
  (∀ (h2 : p), q h2) ↔ q h :=
by simp only [forall_eq_propForall, h, propForall_true_left, iff_self]

[Jakob von Raumer]

So maybe this is better than tweaking SimpCongrTheorems.lean? I don't know :thinking:

[Chris Hughes]

Then you're leaving propForall in people's goal after non-terminal simp. I know non-terminal simp is bad but it's still not ideal.

[Jakob von Raumer]

Yea, would be better if we could engineer it in a way that only triggers the [simp] if the [congr] is applicable

[Chris Hughes]

As a temporary hack for when these come up, I've been using the lemmas forall_prop_of_true and forall_prop_of_false