equality substitution

Stream: lean4

[Alice Laroche]

So, i have this :

import Mathlib.Logic.Basic

theorem not_forall_eq {s s' : α -> Prop} (h : ∀x, (¬s x) = s' x) : (¬ ∀x, s x) = (∃ x, s' x) :=
funext h ▸ propext not_forall
theorem not_exists_eq {s s' : α -> Prop} (h : ∀x, (¬s x) = s' x) : (¬ ∃x, s x) = (∀ x, s' x) :=
funext h ▸ propext not_exists

The first theorem work, but not the second one, does someone have an idea of why, and how to make it work

[Kevin Buzzard]

Independent of the question, are you sure you want to be talking about equality of propositions? Equality of types is a pretty hairy notion in type theory. What's wrong with ↔?

[Kevin Buzzard]

Normally when eq.subst fails it's just a matter of giving things more type ascriptions. The elaborator has a hard time solving these questions because higher order unification is undecidable and intermediate problems may have multiple solutions. But I'm not at lean right now and haven't tried to fix the code

[Alice Laroche]

For the use i have of it, yeah i'm pretty sure i need equality, because i'm relying heavily on Eq.congr , and i don't think there is an equivalent for Iff ?

[Kevin Buzzard]

The rw tactic works fine with iff

[Alice Laroche]

But i don't use rw actually

[Kevin Buzzard]

Yeah I can't get rw to work in tactic mode either -- in Lean 3 this wouldn't work either -- rw can't see under binders. In Lean 3 we use simp only and the same trick works here:

theorem not_exists_eq {s s' : α -> Prop} (h : ∀x, (¬s x) = s' x) : (¬ ∃x, s x) = (∀ x, s' x) :=
by
  have h1 : (¬ ∃x, s x) = (∀ x, (¬s x)) := propext not_exists
  simp only [h] at h1
  assumption

To be quite frank I'm more surprised that your first proof works than the second one fails :-) (eq.subst really seems to be rewriting under a binder). But I spend my life in tactic mode, I don't know the subtleties of eq.subst (although if you search for "stupid triangle" here I'm sure you'll find plenty of examples of me moaning about it).

What is Eq.congr? I still have this nagging worry that you shouldn't be doing things like this. Prop is not bool, it's a level higher; equality of terms is fine, but equality of types is not a good concept somehow.

[Alice Laroche]

congr is this : theorem congr {α : Sort u} {β : Sort v} {f₁ f₂ : α → β} {a₁ a₂ : α} (h₁ : Eq f₁ f₂) (h₂ : Eq a₁ a₂) : Eq (f₁ a₁) (f₂ a₂)

[Kevin Buzzard]

Oh in Lean 3 it's just the same, both in term mode and tactic mode. I would expect all four proofs to fail, and certainly the tactic proof of not_forall_eq because everyone knows that rw won't rewrite under a binder.

import tactic

variable (α : Type)

theorem not_forall_eq {s s' : α -> Prop} (h : ∀x, (¬s x) = s' x) : (¬ ∀x, s x) = (∃ x, s' x) :=
funext h ▸ propext not_forall -- works
theorem not_exists_eq {s s' : α -> Prop} (h : ∀x, (¬s x) = s' x) : (¬ ∃x, s x) = (∀ x, s' x) :=
funext h ▸ propext not_exists -- fails

theorem not_forall_eq' {s s' : α -> Prop} (h : ∀x, (¬s x) = s' x) : (¬ ∀x, s x) = (∃ x, s' x) :=
begin
  have h2 := funext h,
  have h3 : (¬∀ (x : α), s x) = ∃ (x : α), ¬s x := propext not_forall,
  rw h2 at h3, -- `rw` rewriting under a binder
  exact h3,
end

theorem not_exists_eq {s s' : α -> Prop} (h : ∀x, (¬s x) = s' x) : (¬ ∃x, s x) = (∀ x, s' x) :=
begin
  have h2 := funext h,
  have h3 : (¬∃ (x : α), s x) = ∀ (x : α), ¬s x := propext not_exists,
  rw h2 at h3, -- `rw` fails, as expected, because we all know it can't rewrite under binders
end

[Kevin Buzzard]

(deleted)

[Alice Laroche]

Yeah, i figured out
So i just #print your proof via tactic to see if I can somehow make a clean expression

[Alice Laroche]

And of course i can, so here it is :

theorem not_forall_eq {s s' : α -> Prop} (h : ∀x, (¬s x) = s' x) : (¬ ∀x, s x) = (∃ x, s' x) := funext h ▸ propext not_forall
theorem not_exists_eq {s s' : α -> Prop} (h : ∀x, (¬s x) = s' x) : (¬ ∃x, s x) = (∀ x, s' x) := forall_congr h ▸ propext not_exists

[Kevin Buzzard]

Nice! And thanks for your explanation on the thread in #general (I started it because many Lean 3 people don't read this stream, I should have just asked you here!). As for congr, what does iff.congr say? Whatever it says, can't you just prove it using propext?

[Alice Laroche]

Thanks to you too, because i figured that rewriting under binder was not a good thing

[Kevin Buzzard]

This is regarded as a "known limitation of rw" in Lean 3; the simp_rw command is basically (I think) a wrapper for simp only which will rewrite under binders (because simp will and rw won't). I had not understood before that it's also a limitation of eq.subst, I guess this is the reason why we can't rewrite under binders. Is there a type-theoretic reason for this behaviour I wonder or is it just because someone had to write a unifier for Lean at some point and because there's some theorem of logic saying there's no algorithm for higher order unification they had to instead write an algorithm which sometimes fails and they chose it to fail here.

[Kyle Miller]

Kevin Buzzard said:

rw can't see under binders

This is commonly stated, but it turns out not to be true. What rw can't do is rewrite subexpressions containing bound variables.

This is rw rewriting under binders in Lean 3:

example {α : Type*} (f : ℕ → ℕ → α) (h : f 1 = f 2) : ∀ (n : ℕ), f 1 n = f 2 n :=
begin
  rw h,
  exact λ _, rfl,
end

[Kyle Miller]

My understanding of this is that rw needs to do a "global" rewrite of the entire term, and if a subexpression to be rewritten contains a bound variable, you can't lift it outside that binder to do the global rewrite.

[Kyle Miller]

Here's an example of rw failing to rewrite under binders since it would need to refer to f (n + 1) 1 outside the binder for n.

example {α : Type*} (f : ℕ → ℕ → α) (h : ∀ (k : ℕ), f k 1 = f k 2) :
  ∀ (n : ℕ), f (n + 1) 1 = f (n + 1) 2 :=
begin
  rw h,  -- fails (and simp_rw [h] succeeds)
end

[Mario Carneiro]

Kevin Buzzard said:

This is regarded as a "known limitation of rw" in Lean 3; the simp_rw command is basically (I think) a wrapper for simp only which will rewrite under binders (because simp will and rw won't). I had not understood before that it's also a limitation of eq.subst, I guess this is the reason why we can't rewrite under binders. Is there a type-theoretic reason for this behaviour I wonder or is it just because someone had to write a unifier for Lean at some point and because there's some theorem of logic saying there's no algorithm for higher order unification they had to instead write an algorithm which sometimes fails and they chose it to fail here.

This is a fundamental limitation of eq.subst. It accepts an equality as input, that is, the assertion that two particular things are equal. If I know that ?x + ?y = ?y + ?x for some particular (to be determined) values ?x and ?y, there is no way I can prove (∀ n, P (x + n)) -> (∀ n, P (n + x))

[Kevin Buzzard]

In the example the equality it had was fun a, f a = fun a, g a and in that situation you could imagine it working somehow

[Reid Barton]

Which example?

[Reid Barton]

There is a difference between fun a, f a = fun a, g a and forall a, f a = g a

[Kevin Buzzard]

In the example at the top we have funext h ▸ ...

[Reid Barton]

So the type of funext h is something like (fun x => neg (s x)) = s', and the LHS of that doesn't look like anything in not_exists

[Reid Barton]

ah, trying to rewrite the RHS of not_exists?

[Reid Barton]

I guess in that case it probably could work with an explicitly provided motive

[Reid Barton]

and the first one works because the RHS is really notation for Exists (fun x => neg (s x)) already