tactic to contract equalities

Stream: lean4

[Jakob von Raumer]

Do we have a tactic which contracts equalities under various binders when possible? For example given h : ∃ a b c, a = b ∧ b = c ∧ foo c I want to simplify to h : ∃ a, foo a without performing any other simplifications.

[Ruben Van de Velde]

Does simp make progress? You could do something with simp only if it does

[Yaël Dillies]

Unfortunately this kind of goals isn't very simp-friendly. Try simp {contextual := true}, though.

[Jeremy Salwen]

theorem z (h : ∃ a b c, a = b ∧ b  = c ∧ f c): a := by
  simp  at h

works!

[Yaël Dillies]

Shouldn't the goal be f a rather than a?

[Jakob von Raumer]

@Jeremy Salwen Fails to simplify for (h : ∃ a b c, a = b ∧ b = c ∧ f c ∨ f a) though

[Jakob von Raumer]

@Yaël Dillies I'm getting an error on this, is this a fairly new addition to simp?

[Yaël Dillies]

No, it's an old one. I suspect the syntax has changed in Lean 4.

[Jakob von Raumer]

@Jeremy Salwen The issue is also that a pure simp does too much in other situations

[Jakob von Raumer]

@Yaël Dillies Ah, it's simp (config := { contextual := true}) now

[Yaël Dillies]

Ugh, that's a mouthful

[Jakob von Raumer]

Hm, so the result of that is not too bad, probably I can make it work if I find a good simp set. Some of the simp lemmas prevent equalities in nested existential quantifiers to be contracted further.

[Jeremy Salwen]

Adding the following lemma lets simp solve it:

theorem w (p: α -> Prop):  (∃ x, (p x) ∨ b) ↔  ((∃ x, p x) ∨ b) := sorry

This is similar to the exists_and_left lemma which simp uses to simplify the first expression, but pushing the extential quantifier in through an or expression instead of an and expression.

[Jakob von Raumer]

(deleted)

[Gabriel Ebner]

You might be interested in this talk: https://matryoshka-project.github.io/matryoshka2018/slides/Matryoskha-2018-Hoelzl-Generalising-the-One-Point-Rule.pdf

[Jakob von Raumer]

Thanks :blush:

[Jakob von Raumer]

Though this issue is simply about simps unification behaviour under ∃ :sweat_smile:

[Jakob von Raumer]

Maybe I'm just too tired, but now it simplifies

[Jakob von Raumer]

Ignore my last message :face_palm:

[Gabriel Ebner]

I should also warn you that foo is false.

[Jakob von Raumer]

(deleted)

[Jakob von Raumer]

(deleted)

[Jakob von Raumer]

Fixed the example:

theorem foo {α : Sort u} {P Q : α → Prop} {a : α} : (∃ b, Q a ∧ a = b ∧ P b) ↔ (Q a ∧ P a) := by
  constructor
  · rintro ⟨_, q, rfl, p⟩; exact ⟨q, p⟩
  · rintro ⟨q, p⟩; exact ⟨_, q, rfl, p⟩

example {a b c : ℕ} : ∃ d, c < 3 ∧ c = d ∧ d > a * a := by
  simp only [foo (Q := fun (c : ℕ ) => c < 3)]  -- fails to simplify without giving `Q`
  sorry