Trouble with rw/subst

Stream: lean4

[sgcs]

I have the following MWE:

inductive Foo where
  | foo₁ : Foo
  | foo₂ : Foo
  | foo₃ : Foo

inductive Baz : Foo → Type where
  | baz1 : Baz Foo.foo₁
  | baz2 : Baz Foo.foo₂

inductive Bar : Foo → Foo → Type where

axiom Bar.deterministic {f₁ f₂ f₃ : Foo} (bar₁ : Bar f₁ f₂) (bar₂ : Bar f₁ f₃) : f₂ = f₃

inductive Barᵣₜ : Foo → Foo → Type where
  | refl : (f : Foo) → Barᵣₜ f f
  | trans (f₁ : Foo) {f₂ f₃ : Foo} : (Bar f₁ f₂) → Barᵣₜ f₂ f₃ → Barᵣₜ f₁ f₃

def Barᵣₜ.length {f f' : Foo} : (Barᵣₜ f f') → Nat
  | .refl _ => 0
  | .trans _ _ mtr => 1 + length mtr

axiom Barᵣₜ.deterministic {f₁ f₂ f₃ : Foo} (barᵣₜ₁ : Barᵣₜ f₁ f₂) (barᵣₜ₂ : Barᵣₜ f₁ f₃) (baz₁ : Baz f₂) (baz₂ : Baz f₃) : f₂ = f₃

axiom Foo.barᵣₜ (f : Foo) : Σ f' : Foo, Baz f' × Barᵣₜ f f'

theorem Foo.count (f : Foo) : Nat := (Foo.barᵣₜ f).2.2.length

theorem foo
  {f₁ f₂ : Foo} (bar₁ : Bar f₁ f₂) :
  1 + f₂.count = f₁.count := by
  unfold Foo.count

  let ⟨_, baz₁, barᵣₜ₁⟩ := f₁.barᵣₜ
  rename_i f₃

  let ⟨_, baz₂, barᵣₜ₂⟩ := f₂.barᵣₜ
  rename_i f₃'

  cases barᵣₜ₁ with
  | refl => sorry -- this is not important
  | trans _ bar₁' barᵣₜ₂' =>
      rename_i fₘ
      simp only
      conv => rhs; unfold Barᵣₜ.length

      -- Had the same problem below as I did here, but was able to resolve by reverting
      revert barᵣₜ₂ barᵣₜ₂'
      rw [Bar.deterministic bar₁ bar₁'] at *
      intro barᵣₜ₂' barᵣₜ₂

      -- If I try the following, I get:
      -- ```
      -- application type mismatch
      --   Barᵣₜ.deterministic barᵣₜ₂ barᵣₜ₂' baz₁
      -- argument
      --   baz₁
      -- has type
      --   Baz f₃ : Type
      -- but is expected to have type
      --   Baz f₃' : Type
      -- ```
      -- rw [Barᵣₜ.deterministic barᵣₜ₂ barᵣₜ₂' baz₁ baz₂] at *

      -- Which I don't understand since this works by itself:
      -- let eq := Barᵣₜ.deterministic barᵣₜ₂ barᵣₜ₂' baz₁ baz₂

      -- But if I try to subst `eq`, I get:
      -- `failed to create binder due to failure when reverting variable dependencies`
      -- subst eq
      sorry

I have an equality Barᵣₜ.deterministic barᵣₜ₂ barᵣₜ₂' baz₁ baz₂ that I want to rewrite with, but can't seem to figure out how to do so. I have some comments above showing what I've tried and what errors I've gotten.

[Kevin Buzzard]

If I put set_option autoImplicit false at the top of your file it indicates an error in the definition of Baz, meaning that your definition of Baz might not say what you think it says (foo₁ ≠ Foo.foo₁, in fact foo₁ is just a variable here). Does this help?

[sgcs]

Oh, thank you, I didn't notice that. Unfortunately, that was just a mistake in making the MWE. Changing it to be Foo.foo₁ and Foo.foo₂ doesn't change the error I'm getting.

[sgcs]

Another example where I run into the same problems is (in the context of the above code) is:

axiom Bar.irrelevant {f f' : Foo} (bar bar' : Bar f f') : bar = bar'

theorem thm {f₁ f₂ : Foo} (barᵣₜ barᵣₜ' : Barᵣₜ f₁ f₂) (baz : Baz f₂) : barᵣₜ = barᵣₜ' :=
  match barᵣₜ, barᵣₜ' with
  | .refl _, .refl _ => rfl
  | .refl _, .trans _ _ _ => sorry -- not important
  | .trans _ _ _, .refl _ => sorry -- not important
  | .trans _ bar barᵣₜ, .trans _ bar' barᵣₜ' => by
      -- Want to:
      -- 1. rewrite using `Bar.deterministic bar bar'`
      -- 2. rewrite using `Bar.irrelevant bar bar'`
      -- 3. rewrite using `thm barᵣₜ barᵣₜ' baz`
      rw [Bar.deterministic bar bar'] at *
      rw [Bar.irrelevant bar bar'] at *
      rw [thm barᵣₜ barᵣₜ' baz] at *

      sorry

When I try to rw [Bar.deterministic bar bar'] at *, it remove the old hypotheses which makes the following rewrites fail. I get the same failed to create binder due to failure when reverting variable dependencies error if I try to use subst instead.

[Kevin Buzzard]

I'm a bit confused by exactly what you're asking. Can you just post one question? Give an example of a rewrite which you think should work, but which fails, for example. The error you get with rw [Barᵣₜ.deterministic barᵣₜ₂ barᵣₜ₂' baz₁ baz₂] at * seems to be exactly the error one would expect, for example.

[Kyle Miller]

Using cases instead of subst works here:

theorem thm {f₁ f₂ : Foo} (barᵣₜ barᵣₜ' : Barᵣₜ f₁ f₂) (baz : Baz f₂) : barᵣₜ = barᵣₜ' :=
  match barᵣₜ, barᵣₜ' with
  | .refl _, .refl _ => rfl
  | .refl _, .trans _ _ _ => sorry -- not important
  | .trans _ _ _, .refl _ => sorry -- not important
  | .trans _ bar barᵣₜ, .trans _ bar' barᵣₜ' => by
      cases Bar.deterministic bar bar'
      cases Bar.irrelevant bar bar'
      cases thm barᵣₜ barᵣₜ' baz

      sorry

[Kyle Miller]

cases is more low-level than subst

[Kyle Miller]

I didn't check to what extent it carried out the full substitution however.

[sgcs]

Kyle Miller said:

Using cases instead of subst works here:

theorem thm {f₁ f₂ : Foo} (barᵣₜ barᵣₜ' : Barᵣₜ f₁ f₂) (baz : Baz f₂) : barᵣₜ = barᵣₜ' :=
  match barᵣₜ, barᵣₜ' with
  | .refl _, .refl _ => rfl
  | .refl _, .trans _ _ _ => sorry -- not important
  | .trans _ _ _, .refl _ => sorry -- not important
  | .trans _ bar barᵣₜ, .trans _ bar' barᵣₜ' => by
      cases Bar.deterministic bar bar'
      cases Bar.irrelevant bar bar'
      cases thm barᵣₜ barᵣₜ' baz

      sorry

Thank you! That solves all of the rewrite problems I was having, though I don't understand why rw and subst fail while cases works.

[Kyle Miller]

I don't know why subst fails, but rw at * is usually not good for global substitutions. It uses a different algorithm to do the rewrite.

[sgcs]

Kevin Buzzard said:

I'm a bit confused by exactly what you're asking. Can you just post one question? Give an example of a rewrite which you think should work, but which fails, for example. The error you get with rw [Barᵣₜ.deterministic barᵣₜ₂ barᵣₜ₂' baz₁ baz₂] at * seems to be exactly the error one would expect, for example.

I'm not sure what you mean about the error being expected, at least it doesn't seem obvious to me. Changing it to use cases makes it work which is what I would have expected with rw.

[sgcs]

For example, the final code with finished proofs (excluding some other cases that needed additional lemmas outside of the MWE):

inductive Foo where
  | foo₁ : Foo
  | foo₂ : Foo
  | foo₃ : Foo

inductive Baz : Foo → Type where
  | baz1 : Baz Foo.foo₁
  | baz2 : Baz Foo.foo₂

inductive Bar : Foo → Foo → Type where

axiom Bar.deterministic {f₁ f₂ f₃ : Foo} (bar₁ : Bar f₁ f₂) (bar₂ : Bar f₁ f₃) : f₂ = f₃

inductive Barᵣₜ : Foo → Foo → Type where
  | refl : (f : Foo) → Barᵣₜ f f
  | trans (f₁ : Foo) {f₂ f₃ : Foo} : (Bar f₁ f₂) → Barᵣₜ f₂ f₃ → Barᵣₜ f₁ f₃

def Barᵣₜ.length {f f' : Foo} : (Barᵣₜ f f') → Nat
  | .refl _ => 0
  | .trans _ _ mtr => 1 + length mtr

axiom Barᵣₜ.deterministic {f₁ f₂ f₃ : Foo} (barᵣₜ₁ : Barᵣₜ f₁ f₂) (barᵣₜ₂ : Barᵣₜ f₁ f₃) (baz₁ : Baz f₂) (baz₂ : Baz f₃) : f₂ = f₃

axiom Foo.barᵣₜ (f : Foo) : Σ f' : Foo, Baz f' × Barᵣₜ f f'

theorem Foo.count (f : Foo) : Nat := (Foo.barᵣₜ f).2.2.length

axiom Bar.irrelevant {f f' : Foo} (bar bar' : Bar f f') : bar = bar'

theorem thm {f₁ f₂ : Foo} (barᵣₜ barᵣₜ' : Barᵣₜ f₁ f₂) (baz : Baz f₂) : barᵣₜ = barᵣₜ' :=
  match barᵣₜ, barᵣₜ' with
  | .refl _, .refl _ => rfl
  | .refl _, .trans _ _ _ => sorry -- not important
  | .trans _ _ _, .refl _ => sorry -- not important
  | .trans _ bar barᵣₜ, .trans _ bar' barᵣₜ' => by
      cases Bar.deterministic bar bar'
      cases Bar.irrelevant bar bar'
      cases thm barᵣₜ barᵣₜ' baz
      rfl

theorem foo
  {f₁ f₂ : Foo} (bar₁ : Bar f₁ f₂) :
  1 + f₂.count = f₁.count := by
  unfold Foo.count

  let ⟨_, baz₁, barᵣₜ₁⟩ := f₁.barᵣₜ
  rename_i f₃

  let ⟨_, baz₂, barᵣₜ₂⟩ := f₂.barᵣₜ
  rename_i f₃'

  cases barᵣₜ₁ with
  | refl => sorry -- this is not important
  | trans _ bar₁' barᵣₜ₂' =>
      rename_i fₘ
      simp only
      conv => rhs; unfold Barᵣₜ.length

      revert barᵣₜ₂ barᵣₜ₂'
      rw [Bar.deterministic bar₁ bar₁'] at *
      intro barᵣₜ₂' barᵣₜ₂

      cases Barᵣₜ.deterministic barᵣₜ₂ barᵣₜ₂' baz₁ baz₂
      cases thm barᵣₜ₂ barᵣₜ₂' baz₁
      rfl

[Kyle Miller]

I'm not actually able to reproduce that subst fails:

theorem foo
  {f₁ f₂ : Foo} (bar₁ : Bar f₁ f₂) :
  1 + f₂.count = f₁.count := by
  unfold Foo.count

  let ⟨_, baz₁, barᵣₜ₁⟩ := f₁.barᵣₜ
  rename_i f₃

  let ⟨_, baz₂, barᵣₜ₂⟩ := f₂.barᵣₜ
  rename_i f₃'

  cases barᵣₜ₁ with
  | refl => sorry -- this is not important
  | trans _ bar₁' barᵣₜ₂' =>
      rename_i fₘ
      simp only
      conv => rhs; unfold Barᵣₜ.length

      revert barᵣₜ₂ barᵣₜ₂'
      have := Bar.deterministic bar₁ bar₁'
      subst this
      intro barᵣₜ₂' barᵣₜ₂

      have := Barᵣₜ.deterministic barᵣₜ₂ barᵣₜ₂' baz₁ baz₂
      subst this
      have := thm barᵣₜ₂ barᵣₜ₂' baz₁
      subst this
      rfl

[sgcs]

Really? When I have:

theorem foo
  {f₁ f₂ : Foo} (bar₁ : Bar f₁ f₂) :
  1 + f₂.count = f₁.count := by
  unfold Foo.count

  let ⟨_, baz₁, barᵣₜ₁⟩ := f₁.barᵣₜ
  rename_i f₃

  let ⟨_, baz₂, barᵣₜ₂⟩ := f₂.barᵣₜ
  rename_i f₃'

  cases barᵣₜ₁ with
  | refl => sorry -- this is not important
  | trans _ bar₁' barᵣₜ₂' =>
      rename_i fₘ
      simp only
      conv => rhs; unfold Barᵣₜ.length

      -- Had the same problem below as I did here, but was able to resolve by reverting
      revert barᵣₜ₂ barᵣₜ₂'
      rw [Bar.deterministic bar₁ bar₁'] at *
      intro barᵣₜ₂' barᵣₜ₂

      let eq := Barᵣₜ.deterministic barᵣₜ₂ barᵣₜ₂' baz₁ baz₂
      subst eq
      sorry

I get: failed to create binder due to failure when reverting variable dependencies Let me try yours

[sgcs]

But, you're right, yours works. Am I using subst incorrectly?

[Kyle Miller]

Yeah, don't use let for propositions, use have.

[sgcs]

Oh, ok, I wasn't aware there was even a difference between using let and have in tactics, I thought they were the same

[Kyle Miller]

They general difference between let and have (both inside and outside tactics) is that with let the defined variable is definitionally equal to its value, but with have the defined variable isn't, and it can't be unfolded to its value (it's been forgotten, so to speak).

[Kyle Miller]

With propositions, you don't generally want the value, and many tactics assume any local proofs are created with have, like apparently subst.

[Kyle Miller]

Maybe subst should detect this and report an error, rather than giving a cryptic second-order error

[sgcs]

Thanks, that clarifies a lot for me. I think part of the problem is that I've used (or recall doing so) subst successfully with let bindings previously in simpler proofs so wasn't aware that was a problem.