Constructor elimination under HEq

Stream: new members

[Alex Mobius]

Good day,
I'm trying to prove equivalence between type arguments and constructor used for my type family Path. It has two numeric arguments x, y, and if x < y, then you can only construct a point; likewise, if x < y, then you can only construct a cons. I'm trying to express that constraint through HEq.
Here's my unfinished program:

variable {N: Nat} (x y: Fin N)

structure DAG (N: Nat) where
  adj: (x y: Fin N) -> x < y -> Prop

namespace DAG
variable (G: DAG N)

-- DAG.adj plus x < y
def Adj := exists h, G.adj x y h

inductive Path (G: DAG N): (x y: Fin N) -> Type where
| point : {x: _} -> G.Path x x
| cons : {x y: _} -> (z: _) -> G.Adj x z -> G.Path z y -> G.Path x y

variable {G} {x y}

theorem Adj.to_lt (rel: DAG.Adj G x y): x < y := by
  cases rel
  assumption

namespace Path
  variable (p: G.Path x y)

  theorem point_is_eq (h: HEq p (@point N G x)): (x = y) := by
    cases p
    rfl
    -- `h` is HEq (cons ? ? ?) (point)

If I could name second argument to cons subexpression in h, then I would be able to use Adj.to_lt and arrive at a contradiction. But I don't know how to do that.

[Kyle Miller]

I think this is not provable, unfortunately.

[Kyle Miller]

The proof for non-provability is that if G is the path DAG (where only G.Adj n (n + 1) for each n < N), then Path G x y has cardinality 1 iff x <= y. This means that each such Path G x y type could in principle be equal to each other (according to the cardinality model of Lean in Mario's thesis), so you can't conclude anything about x and y.

[Kyle Miller]

Incidentally, trying to work with paths in graphs is how I learned about this issue.

docs#SimpleGraph.Walk.copy is a way to work around the issue. You have to keep track of index equalities somehow.

[Alex Mobius]

Interesting! A very categorical way of thinking about it, but alas. I suppose I should go back to strict path construction, then, if I want to be able to distinguish these cases.
Relatedly, why does conv only allow me to extract the G.Path z y part from the cons constructor?

[Alex Mobius]

Your link is the reverse direction, that's pretty easy to prove :)

[Kyle Miller]

That's not a theorem, it's a definition

[Kyle Miller]

The idea is to avoid HEq entirely for paths, and instead only consider equalities, making use of this copy function to "cast" the paths

[Kyle Miller]

re conv: I'm not sure exactly, but this means that somehow the congruence lemma it's generating is deficient. I don't see why it would be, since you can in principle rewrite the Adj and Path arguments independently just fine... Constraints arise when there's dependence — that's why z can't be rewritten for example.

[Alex Mobius]

HEq is rightly confusing me:

You should avoid using this type if you can. Heterogeneous equality does not have all the same properties as Eq, because the assumption that the types of a and b are equal is often too weak to prove theorems of interest. One important non-theorem is the analogue of congr: If HEq f g and HEq x y and f x and g y are well typed it does not follow that HEq (f x) (g y). (This does follow if you have f = g instead.) However if a and b have the same type then a = b and HEq a b are equivalent.

but then:

theorem congr_heq {α : Sort u_2} {β : Sort u_2} {γ : Sort u_3} {f : α → γ} {g : β → γ} {x : α} {y : β} (h₁ : HEq f g) (h₂ : HEq x y) :
f x = g y

What gives?

[Mario Carneiro]

this is provable, the version that is not provable is when f and g have different codomains γ, γ' (and you don't otherwise have an equality of these types in scope)