heq alternative

Stream: general

[Reid Barton]

I found the following technique useful recently and thought it might be interesting to others.
Sometimes in a dependently-typed situation we have two expressions which are morally equal but we cannot directly state their equality because the types of the two sides are only propositionally equal. For my example I'll take associativity of append on vector:

variables {α : Type} {i j k : ℕ} (x : vector α i) (y : vector α j) (z : vector α k)

-- doesn't typecheck
-- lemma bad_append : (x.append y).append z = x.append (y.append z) := ...
/-
error: type mismatch at application
  (x.append y).append z = x.append (y.append z)
term
  x.append (y.append z)
has type
  vector α (i + (j + k))
but is expected to have type
  vector α (i + j + k)
-/

[Reid Barton]

There are a couple of ways to deal with this, including using heterogeneous equality or inserting a cast of some kind. Here is another one. Often in the situation where you'd like to apply this equality, the term (x.append y).append z appears in a context that could accept a vector of any length. Then, you can apply a lemma of the following form:

import data.subtype
import data.vector
import tactic.basic

variables {α : Type} {i j k : ℕ} (x : vector α i) (y : vector α j) (z : vector α k)

lemma good_append {ι : Sort*} {C : Π {n : ℕ}, vector α n → ι} :
  C ((x.append y).append z) = C (x.append (y.append z)) :=
begin
  have A : (i + j) + k = i + (j + k) := nat.add_assoc i j k,
  congr' 1, { exact A },
  have : ∀ {n m : ℕ} (h : n = m) (v : vector α n) (w : vector α m),
    v == w ↔ v.to_list = w.to_list,
  { rintros _ _ rfl v w,
    rw heq_iff_eq,
    exact subtype.ext_iff },
  rw this A,
  simp only [vector.to_list_append],
  apply list.append_assoc
end

[Reid Barton]

For example C might be something like is_palindrome : Π {n : ℕ}, vector α n → Prop. Or in other situations, C might be some general property like continuity. Then you can rewrite under C using something like refine (good_append x y z).mpr _. (rw gets confused by the form of the lemma, and couldn't know where to rewrite.)

[Johan Commelin]

Could we have some sort of hrw (heterogenous rw) that could make using any of these tricks easier?

[Kevin Buzzard]

Is that heq have thing just missing API? I avoid heq like the plague.

[Mario Carneiro]

I think this is equivalent to the statement that if you tuple a vector with its length you get something you can state an equality about

[Adam Topaz]

Is there a similar trick that can be done where \iota is a family of types that depends on a vector? It seems that heq would still cause issues in that case.

[Mario Carneiro]

that is, ⟨(i + j) + k, (x.append y).append z⟩ = ⟨i + (j + k), x.append (y.append z)⟩ is an equality in Σ n, vector A n

[Mario Carneiro]

whch is of course true because that's equivalent to list.append_assoc

[Adam Topaz]

Well... it's a combination of list.append and add_assoc right?

[Mario Carneiro]

I mean that Σ n, vector A n is isomorphic to list A, and the two sides of that are mapped by the isomorphism to (x ++ y) ++ z and x ++ (y ++ z)

[Adam Topaz]

Oh I see.

[Reid Barton]

Right, and one way to look at it is that sigma.mk is the universal possible choice for C--but when you want to apply this lemma you probably don't have a sigma.mk in the term waiting to be rewritten, so it's more convenient to use in the form with C.

[Reid Barton]

Adam Topaz said:

Is there a similar trick that can be done where \iota is a family of types that depends on a vector? It seems that heq would still cause issues in that case.

Yeah, I actually tried to do this when I wrote down the type of the lemma for the first time, and then Lean told me it wouldn't work--the purpose of C is to hide the problematic type index, so it can't appear in the result type of C.

[Reid Barton]

In my case the type doesn't change (as some might guess my real C is the property of a subset of $R^n$ being definable in some structure, which is a Prop), so I didn't think about what one could do if it does change.

[Floris van Doorn]

Nice trick!
I still feel like the lemma should be with heq, and that there should be tooling to make it easy to go from the heq statement to the lemma good_append.

[Reid Barton]

Here's yet another alternative which I haven't really tried to use for anything, but seems sensible for theoretical reasons:

import tactic.basic

/-
dependent equality / dependent path / "pathover" from HoTT/cubical type theory
-/

inductive deq {α : Sort*} {C : α → Sort*} :
  Π {a a' : α} (e : a = a') (x : C a) (x' : C a'), Prop
| refl {a : α} (x : C a) : deq (eq.refl a) x x

attribute [refl] deq.refl

notation x ` =[`:50 e:50 `] `:50 x':50 := deq e x x'

variables {α : Sort*} {C : α → Sort*}

@[symm] lemma deq.symm {a a' : α} (e : a = a') (x : C a) (x' : C a') :
  x =[e] x' → x' =[e.symm] x :=
begin
  rintro ⟨⟩,
  refl
end

@[trans] lemma deq.trans {a a' a'' : α} (e : a = a') (e' : a' = a'')
  (x : C a) (x' : C a') (x'' : C a'') :
  x =[e] x' → x' =[e'] x'' → x =[e.trans e'] x'' :=
begin
  rintros ⟨⟩ ⟨⟩,
  refl
end

[Adam Topaz]

Cool. I guess the rinto is necessary to see past the constructor of the inductive type?

[Reid Barton]

yes, it's just short for cases

[Adam Topaz]

But to really make this cubical, we would need deq over deq, etc...

[Reid Barton]

deq over deq is not really any more cubical, but it is a separate issue I'm a bit confused about

[Adam Topaz]

Isn't it a path dependent on a path?

[Reid Barton]

A path dependent on a path is still a path

[Reid Barton]

I think you're thinking of a path in a path type

[Reid Barton]

(I'm assuming by deq over deq you meant something like e : a = a', f : x =[e] x', then you want some kind of y =[f] y')

[Reid Barton]

that just corresponds to a longer telescope/context

[Reid Barton]

like a path \I -> Sigma (a : A) (b : B a), C a b (where \I is the interval)

[Reid Barton]

while a higher cube is \I -> \I -> A

[Reid Barton]

er, Pi wasn't right--something more like Sigma, but really more like a : A, b : B a |- \I -> C a b

[Reid Barton]

ok even this is wrong

[Reid Barton]

a and b should also depend on an interval variable... but hopefully you get the idea

[Reid Barton]

Explicitly, this is the next entry in the sequence

inductive ddeq {α : Sort*} {C : α → Sort*} {D : Π (a : α), C a → Sort*} :
  Π {a a' : α} {e : a = a'} {x : C a} {x' : C a'} (f : x =[e] x') (y : D a x) (y' : D a' x'), Prop
| refl {a : α} {x : C a} (y : D a x) : ddeq (deq.refl x) y y

[Adam Topaz]

I'm just being naive and thinking of a path of paths as a cube.

[Adam Topaz]

But yes I get the idea

[Reid Barton]

Right, this one isn't a path of paths, it's a path whose image under the fibration/display map corresponding to C is the given path e

[Adam Topaz]

Forgetting cubical stuff, it seems that to really make this behave like equality we would need the ddeq you defined, and a dddeq and a ddddeq and ...

[Reid Barton]

or in the ddeq, three paths, each one lying over the next (previous?)

[Adam Topaz]

Oh you mean like the Kan filling condition for cubes? (I don't remember the actual name)

[Reid Barton]

Amusingly, this is (at least spiritually) related to the other conversation about the topology on an sigma type

[Floris van Doorn]

I built the pathover library for Lean 2 HoTT, and I was also worried about needing ddeq, dddeq, etc. (and in HoTT it's worse because then you also need square, dsquare, ddsquare, ..., cube, dcube, ..., ...). However, if you defined ddeq, depending on a path p : x = x' and a pathover q : y =[p] y' and write it as something as z =[p][q] z', then you can prove that it's equivalent to z =[(p, q)] z', where (p, q) is a path (x, y) = (x', y') in the sigma-type, built from p and q. And then it's easier to just use z =[(p, q)] z' in the first place, and then you never have to define deq.

[Kyle Miller]

Is deq different from equality of sigma types? I was experimenting with this, and you can at least implement the recursor for @Reid Barton's deq with it.

import tactic

def deq {α : Sort*} {C : α → Sort*} {a a' : α} (x : C a) (x' : C a') : Prop :=
psigma.mk a x = psigma.mk a' x'

infix ` === `:50 := deq

variables {α : Sort*} {C : α → Sort*}

@[refl] lemma deq.refl {a : α} {x : C a} : x === x := by exact rfl  -- "not a rfl lemma"
@[symm] lemma deq.symm {a a' : α} (x : C a) (x' : C a') : x === x' → x' === x :=
by { rintro ⟨⟩, refl, }
@[trans] lemma deq.trans {a a' a'' : α} (x : C a) (x' : C a') (x'' : C a'') :
  x === x' → x' === x'' → x === x'' :=
by { rintro ⟨⟩ ⟨⟩, refl, }

lemma deq.index_eq {a a' : α} (x : C a) (x' : C a') :
  x === x' → a = a' :=
by { rintro ⟨⟩, refl }

lemma deq.value_eq {a : α} (x x' : C a) :
  x === x' → x = x' :=
by { rintro ⟨⟩, refl }

lemma deq.value_eq' {a a' : α} (x : C a) (x' : C a') (e : a = a') :
  x === x' → (eq.rec x e : C a') = x' :=
by { rintro ⟨⟩, refl }

lemma deq.to_heq {a a' : α} (x : C a) (x' : C a') :
  x === x' → x == x' :=
by simp [deq]

def deq.rec {C' : Π {a a' : α}, a = a' → C a → C a' → Sort*}
  (f : Π {a : α} (x : C a), C' rfl x x)
  {a a' : α} {e : a = a'} {x : C a} {x' : C a'} :
  x === x' → C' e x x' :=
by { subst e, rintro ⟨⟩, apply f }

lemma deq.rec_rule {C' : Π {a a' : α}, a = a' → C a → C a' → Sort*}
  (f : Π {a : α} (x : C a), C' rfl x x)
  {a a' : α} {e : a = a'} {x : C a} {x' : C a'} :
  @deq.rec α C @C' @f a a rfl x x deq.refl = f x := rfl

[Floris van Doorn]

If you have proof irrelevance like in Lean 3 they are the same.
In HoTT they are not quite the same, but closely related:
https://github.com/leanprover/lean2/blob/8072fdf9a0b31abb9d43ab894d7a858639e20ed7/hott/types/sigma.hlean#L109-L110
A path is in a sigma type consists of a path between the first components and then a path between the second components over the first path.

[Mario Carneiro]

I like Kyle's version of deq, it looks strictly more useful than heq

[Floris van Doorn]

I think the type of deq is less convenient to work with than heq: the elaborator will not always be able to figure out what C is from the types of x and x'. In the hott3 library we had to make the family of pathovers explicit, because the elaborator of Lean 3 too often couldn't figure out the type family (in Lean 2 this was not necessary).

[Mario Carneiro]

That's probably true. I often use sigma type equalities in lieu of deq (as mentioned earlier in this thread), but you can almost never avoid writing the type family

[Floris van Doorn]

Why do you think deq is more useful than heq? Isn't deq just a special case of heq, and you can prove all lemmas about deq for heq?

[Mario Carneiro]

heq is a special case of deq (with the identity C), not the other way around afaict

[Floris van Doorn]

Oh, you're right. From deq x x' you get that a = a', which you don't get from x == x'. Yeah, that sounds pretty useful.

[Reid Barton]

The difference between my original deq and Kyle's version is indexing vs bundling--in Lean, everything in sight is a Prop and so there seems to be no disadvantage to Kyle's bundled version.