rw term depended on by other argument

Stream: lean4

[Max Nowak 🐉]

I have the following minified problem, where applying the equation h doesn't work, which is likely because D t depends on t as in the definition of S, but I have no idea how to work around this:

inductive D : Nat -> Type
def mwe (t : Nat) (f : Nat -> Nat) (h : f t = t)
  (d : D (f t))
  (P : (t : Nat) -> D t -> Prop)
  : P (f t) d
  := by
  rw [h] -- tactic 'rewrite' failed, motive is not type correct
  -- I want the goal to become `P t d`

[Kyle Miller]

What does your D type look like in the non-minified example? Is it a docs#Subsingleton ?

[Kevin Buzzard]

Try simp only [h] or simp_rw [h].(but I guess I'm not optimistic). Your diagnosis is correct but sometimes these hacks get around it. What do you expect the rewrite to turn d into?

[Kyle Miller]

Your goal definitely can't be P t d, but you can rewrite t if you're willing to insert an Eq.rec. Here's one way:

import Mathlib.Tactic

inductive D : Nat -> Type

def mwe (t : Nat) (f : Nat -> Nat) (h : f t = t)
  (d : D (f t))
  (P : (t : Nat) -> D t -> Prop)
  : P (f t) d
  := by
  convert_to P t (h ▸ d)
  · simp [heq_rec_iff_heq]
  -- ⊢ P t (h ▸ d)

[Max Nowak 🐉]

It is not a subsingleton, it can have many different values.

[Kyle Miller]

Ok, I asked about subsingletons because if it is you can write a congr lemma to deal with the issue and get simp to be able to rewrite the t argument (assuming P is an actual predicate you have somewhere, rather than an argument to a def)

[Kyle Miller]

Here's another way that does essentially the same thing as convert_to but it's more explicit.

def mwe (t : Nat) (f : Nat -> Nat) (h : f t = t)
  (d : D (f t))
  (P : (t : Nat) -> D t -> Prop)
  : P (f t) d
  := by
  have : P (f t) d = P t (h ▸ d) := congr(P $h $(heq_of_eq_rec_left h rfl))
  rw [this]
  -- ⊢ P t (h ▸ d)

[Kyle Miller]

(These "congr quotations" come from Mathlib.Tactic.TermCongr)

[Eric Wieser]

This should be a theorem not a def because P _ _ is a Prop

[Max Nowak 🐉]

I don't have mathlib set up right now unfortunately, but if none of the other approaches work I'll give it a try tomorrow at the latest.

[Max Nowak 🐉]

Ah they all need mathlib stuff :)

[Kyle Miller]

It's worth knowing how to do it by hand:

theorem mwe (t : Nat) (f : Nat -> Nat) (h : f t = t)
  (d : D (f t))
  (P : (t : Nat) -> D t -> Prop)
  : P (f t) d
  := by
  have : ∀ {x y : Nat} (h : x = y) (d : D x), P x d = P y (h ▸ d) := by
    intros x y h d
    subst h
    rfl
  rw [this h]
  -- ⊢ P t (h ▸ d)

[Kyle Miller]

The mathlib stuff automates this sort of thing.

[Kyle Miller]

The key here is that when there are complicated dependent types, you need to write a "congruence lemma", where everything that could be rewritten is a free variable, and the proof is just subst of all the equality hypotheses followed by rfl.

[Max Nowak 🐉]

That sounds like a good strategy, I'll definitely keep that in mind!

[Max Nowak 🐉]

(Some probably needless context: The original D type is the displayed algebra, i.e. the stuff you put into a recursor. I am trying to implement section 2.3.2, definition \iota^E, of https://andraskovacs.github.io/pdfs/phdthesis_compact.pdf .)

[Kyle Miller]

One design decision you might want to make is to create a D.cast operation that is for restricting the Eq.rec to just the type parameter/index. You can make better simp lemmas for D.cast than you can for unrestricted Eq.rec.

[Max Nowak 🐉]

That is a good idea! I hope I get that far to actually need simp lemmas.

[Max Nowak 🐉]

Your strategy worked, Kyle, and I managed to finally close my goal after half a day of confusion. Thank you so much!

[Max Nowak 🐉]

I'm definitely taking the "congruence lemma" trick away from this!