HEq

Stream: lean4

[Marcus Rossel]

Sorry I don't have an MWE for this, because the small examples I tried worked.
Hopefully the goal state is enough to explain my problem.

I have:

p₁ : IDPath σ₁ x y
p₂ : IDPath σ₂ x y
hσ : σ₁ = σ₂
h : HEq p₁.toRaw p₂.toRaw
hi : ∀ {p : IDPath σ₁ x y}, p₁.toRaw = p.toRaw → p₁ = p
⊢ ...

I'm trying to use hypothesis hi with p₂.
By h I know that p₁.toRaw = p₂.toRaw should hold in some sense, but I don't know how to obtain a proof of that.

---

Plainly using:

have h' := eq_of_heq h

gives:

application type mismatch
  eq_of_heq h
argument
  h
has type
  HEq p₁.toRaw p₂.toRaw : Prop
but is expected to have type
  HEq ?m.23467 ?m.23468 : Prop

---

Rewriting hσ on p₂ produces this goal state:

p₁ : IDPath σ₁ x y
p₂ : IDPath σ₁ x y
p₂✝ : IDPath σ₂ x y
hσ : σ₁ = σ₂
hi : ∀ {p : IDPath σ₁ x y}, p₁.toRaw = p.toRaw → p₁ = p
h : HEq p₁.toRaw p₂✝.toRaw

Thus, I can't use h anymore, as it is about p₂✝ instead of p₂.

---

Am I doing something stupid / missing something obvious here?
I feel like the information is there, but I can't use it.

[Sebastian Ullrich]

I think the common consensus is to avoid het equality wherever possible. Though, does cases hσ help anything in this case?

[Marcus Rossel]

Sebastian Ullrich said:

I think the common consensus is to avoid het equality wherever possible. Though, does cases hσ help anything in this case?

Yeah, the HEq arose from using simp [toRaw] on IDPath.toRaw <path 1> = IDPath.toRaw <path 2>.
The cases hσ doesn't work.
I'll try to change the definition of IDPath.

[Reid Barton]

What are σ₁ and σ₂? Variables?

[Reid Barton]

If neither is a variable then you can still do this by generalizing but it is just kicking the can down the road... since you will only be able to deduce HEq p₁ p₂

[Reid Barton]

But yeah, usually better to find another approach even if it is technically possible to plow ahead

[Marcus Rossel]

Reid Barton said:

What are σ₁ and σ₂? Variables?

I'm not exactly sure how to answer that, so perhaps for some context:

inductive Cmp
  | rtr | rcn | prt | stv

inductive Raw.Reactor (ι υ)
  | mk ...

structure Reactor (ι υ) where
  ...

variable {ι υ}

inductive Raw.IDPath : Raw.Reactor ι υ → ι → Cmp → Type _
  | rtr σ i : σ.nest i ≠ none → IDPath σ i Cmp.rtr
  | rcn σ i : σ.rcns i ≠ none → IDPath σ i Cmp.rcn
  | prt σ i : i ∈ σ.ports.ids → IDPath σ i Cmp.prt
  | stv σ i : i ∈ σ.state.ids → IDPath σ i Cmp.stv
  | nest (σ : Raw.Reactor ι υ) {σ'} (cmp i i') : (IDPath σ' i cmp) → (σ.nest i' = some σ') → IDPath σ i cmp

inductive IDPath : Reactor ι υ → ι → Cmp → Type _
  | rtr {σ i} : i ∈ σ.nest.ids  → IDPath σ i Cmp.rtr
  | rcn {σ i} : i ∈ σ.rcns.ids  → IDPath σ i Cmp.rcn
  | prt {σ i} : i ∈ σ.ports.ids → IDPath σ i Cmp.prt
  | stv {σ i} : i ∈ σ.state.ids → IDPath σ i Cmp.stv
  | nest (σ σ' : Reactor ι υ) (cmp i i') : (IDPath σ' i cmp) → (σ.nest i' = some σ') → IDPath σ i cmp

private def IDPath.toRaw {σ : Reactor ι υ} {i} : {cmp : Cmp} → (IDPath σ i cmp) → Raw.IDPath σ.raw i cmp
  | Cmp.prt, IDPath.prt h => Raw.IDPath.prt σ.raw i h
  | Cmp.stv, IDPath.stv h => Raw.IDPath.stv σ.raw i h
  | Cmp.rcn, IDPath.rcn h => Raw.IDPath.rcn σ.raw i $ ((rcns_rawEquiv σ).eqIDs i).mp h
  | Cmp.rtr, IDPath.rtr h => Raw.IDPath.rtr σ.raw i $ ((nest_rawEquiv σ).eqIDs i).mp h
  | cmp, IDPath.nest _ _ _ _ i' p hn => Raw.IDPath.nest σ.raw cmp i i' (toRaw p) (nest_rawEquiv' hn)

private theorem IDPath.eq_if_toRaw_eq {σ : Reactor ι υ} {i cmp} {p₁ p₂ : IDPath σ i cmp} (h : p₁.toRaw = p₂.toRaw) : p₁ = p₂ := by
  induction p₁
  case nest σ₁ σ₂ cmp i₁ i₂ p hn hi =>
    cases p₂
    case nest σ' i' hn' p' =>
      cases cmp
      all_goals {
        simp [toRaw] at h
        have hσ : σ₂ = σ' := by ext; exact h.left
        sorry
      }
    all_goals { simp [toRaw] at * }
  all_goals { cases p₂ <;> simp [toRaw] at * }

---

So HEq p₁ p₂ would be perfect, as it would allow me to finish the proof.

[Reid Barton]

Well it looks like they are variables. In Lean 3 I would use subst hσ, maybe it will work the same way in Lean 4?