Working with HEq statements

Stream: general

[Frederick Pu]

Hey, I'm trying to prove the following statement of about HEq using HEq.subst but I can't seem to get it to work.

inductive DiffTree (α : Type u) (β : Type v) : List Nat → Type (max u v)
| mk
    (outShape : List Nat)
    (parents : Array (Σ shape, DiffTree α β shape))
    : DiffTree α β outShape


inductive DiffTree.valid {α : Type u} {β : Type v} : ∀ (shape : List Nat), DiffTree α β shape → Prop
| mk (outShape : List Nat) (parents : Array (Σ shape, DiffTree α β shape)) : (DiffTree.mk outShape parents).valid

example (shapeX : List Nat)
    (X : DiffTree α β shapeX)
    (shapeP : List Nat)
    (P : DiffTree α β shapeP)
    (H : HEq P X)
    (hv : P.valid) : X.valid := by
    exact HEq.subst H.symm hv
/-
application type mismatch
  HEq.subst (HEq.symm H) hv
argument
  hv
has type
  DiffTree.valid shapeP P : Prop
but is expected to have type
  ?m.1805 (DiffTree α β shapeX) X : Prop
-/

[Andrés Goens]

(deleted)

[Andrés Goens]

I think the issue seems to be with the argument p to HEq.subst, I'm not sure what it would be because in your case there's another layer of dependence: The type T is DiffTree α β shape, but your valid type has this ∀ (shape : List Nat), part that doesn't match the form of p. Maybe if you don't use HEq.subst but either build something similar to take into account your ∀ shape or prove it directly using something similar to the proof of HEq.subst?

[Andrés Goens]

(which seems to be just HEq.ndrecOn h₁ h₂)

[Frederick Pu]

wait what is motive anyways?

[Frederick Pu]

i tried smth like this

inductive DiffTree (α : Type u) (β : Type v) : List Nat → Type (max u v)
| mk
    (outShape : List Nat)
    (parents : Array (Σ shape, DiffTree α β shape))
    : DiffTree α β outShape


inductive DiffTree.valid {α : Type u} {β : Type v} : ∀ (shape : List Nat), DiffTree α β shape → Prop
| mk (outShape : List Nat) (parents : Array (Σ shape, DiffTree α β shape)) : (DiffTree.mk outShape parents).valid
example (shapeX : List Nat)
    (X : DiffTree α β shapeX)
    (shapeP : List Nat)
    (P : DiffTree α β shapeP)
    (H : HEq P X)
    (hv : P.valid) : X.valid := by
  -- Use `HEq.ndrecOn` to transport `P.valid` to `X.valid` along `H`.
  exact HEq.ndrecOn H (hv : (fun (β : Σ s, DiffTree α β s) => fun x : β => x.2.valid) X)

but it's very hard to parametrize DiffTree over a sort. Is there any way to have ndrec but over type families instead?

[Violeta Hernández]

I'm not entirely convinced this is provable. HEq is very badly behaved, since type equality is badly behaved. For instance, it's entirely possible DiffTree a b shapeX = DiffTree a b shapeP even for shapeX ≠ shapeP, and in that case it's hard to tell what a = b implies.

[Violeta Hernández]

Note that your result is easy to prove if you further assume shapeX = shapeP.

[𝚠𝚘𝚓𝚌𝚒𝚎𝚌𝚑 𝚗𝚊𝚠𝚛𝚘𝚌𝚔𝚒]

Violeta Hernández said:

it's entirely possible DiffTree a b shapeX = DiffTree a b shapeP even for shapeX ≠ shapeP

That sounds right. This paper from Chung-Kil Hur explains that you don't actually want to work with HEq, you want to package up shapeP = shapeX ∧ HEq P X into a single proof, and one way to do that is to use a Sigma type. I recommend looking at the paper.

[Frederick Pu]

So ig the general approach would be to casst from DiffTree a b shapeX to DiffTree a b ShapeP and then using
cast_eq_iff_heq

[Frederick Pu]

is this what kevin buzzard meant by setoid hell?

[Kevin Buzzard]

I think "setoid hell" was a term in existence long before I foolishly mentioned it in 2019! But that's about trying to work with quotients without using Lean's quotient axiom. Sounds like what you're talking about is "DTT hell"?

[Frederick Pu]

So is setoid hell $$\subeteq$$ DTT hell?

[Frederick Pu]

so i managed to get to here but now im stuck

import Batteries.Logic

inductive DiffTree (α : Type u) (β : Type v) : List Nat → Type (max u v)
| mk
    (outShape : List Nat)
    (parents : Array (Σ shape, DiffTree α β shape))
    : DiffTree α β outShape


inductive DiffTree.valid {α : Type u} {β : Type v} : ∀ (shape : List Nat), DiffTree α β shape → Prop
| mk (outShape : List Nat) (parents : Array (Σ shape, DiffTree α β shape)) : (DiffTree.mk outShape parents).valid

example (shapeX : List Nat)
    (X : DiffTree α β shapeX)
    (shapeP : List Nat)
    (P : DiffTree α β shapeP)
    (H : shapeX = shapeP ∧ HEq P X)
    (hv : P.valid) : X.valid := by
    let temp : DiffTree α β shapeX := cast (by rw [H.1]) P
    have : temp = X :=
      cast_eq_iff_heq.mpr H.2
    rw [← this]
    simp [temp]
/-
  α : Type u_1
β : Type u_2
shapeX : List Nat
X : DiffTree α β shapeX
shapeP : List Nat
P : DiffTree α β shapeP
H : shapeX = shapeP ∧ HEq P X
hv : DiffTree.valid shapeP P
temp : DiffTree α β shapeX := cast ⋯ P
this : temp = X
⊢ DiffTree.valid shapeX (cast ⋯ P)
-/

[Kyle Miller]

example (shapeX : List Nat)
    (X : DiffTree α β shapeX)
    (shapeP : List Nat)
    (P : DiffTree α β shapeP)
    (H1 : shapeX = shapeP)
    (H2 : HEq P X)
    (hv : P.valid) : X.valid := by
  cases H1
  cases H2
  exact hv

[Frederick Pu]

mb no gifs were harmed in the making of this post

[Kyle Miller]

You can also use subst_vars in place of the cases lines.