avoiding heq

Stream: general

[Peter Nelson]

I would like to consider the type of all functions f from the subsets of {1, ... ,n} (for some n) to a set A; in other words, the type Σ n, set (fin n) → α There is a natural partial order on this type, where f ≤ g if and only if f.1 ≤ g.1, and f.2 is a 'restriction' of g.2 to set (fin f.1) in the natural way.

I can't seem to do this, however, without running into heterogeneous equality. Here is a MWE.

import tactic

def col (α : Type*) := Σ n, set (fin n) → α

instance {α : Type*} : partial_order (col α) :=
{ le := λ c c', ∃ (h : c.1 ≤ c'.1), ∀ s, c.2 s = c'.2 (fin.cast_le h '' s),
  le_refl := λ c, ⟨rfl.le, λ s, by {congr, rw fin.cast_le_of_eq rfl, simp}⟩,
  le_trans := begin
    rintros _ _ _ ⟨h1,h1'⟩ ⟨h2,h2'⟩,
    refine ⟨h1.trans h2, λ s, _⟩,
    rw [h1',h2'],
    convert rfl using 2,
    rw [←fin.cast_le_comp_cast_le],
    apply set.image_comp ,
  end,
  le_antisymm := begin

    rintros c c' ⟨hle, h⟩ ⟨hle', h'⟩,
    have h_eq := hle.antisymm hle',
    ext, rw h_eq, rw h_eq,
    sorry,

    /-
    ⊢ ∀ (a : set (fin c.fst)) (a' : set (fin c'.fst)), a == a' → c.snd a == c'.snd a'
    -/
  end  }

I did figure out how to resolve this goal, but from what I gather, it is preferable to avoid == altogether. Is there a design route that does this? I'm not fussy as long as it captures the (simple) mathematical object I'm considering.

[Kyle Miller]

I think it's fine having heq in proofs, though sometimes eliminating it actually makes things simpler -- this is because sometimes the steps following a heq showing up are just to turn that heq back into an eq.

The strategy I usually try to go for is to do cases/subst on relevant equalities from left-to-right so that heqs naturally become eqs.

Here's a heq-free proof of le_antisymm:

instance {α : Type*} : partial_order (col α) :=
{ le := λ c c', ∃ (h : c.1 ≤ c'.1), ∀ s, c.2 s = c'.2 (fin.cast_le h '' s),
  le_refl := λ c, ⟨rfl.le, λ s, by {congr, rw fin.cast_le_of_eq rfl, simp}⟩,
  le_trans := begin
    rintros _ _ _ ⟨h1,h1'⟩ ⟨h2,h2'⟩,
    refine ⟨h1.trans h2, λ s, _⟩,
    rw [h1',h2'],
    convert rfl using 2,
    rw [←fin.cast_le_comp_cast_le],
    apply set.image_comp ,
  end,
  le_antisymm := begin
    rintros ⟨c, sc⟩ ⟨c', sc'⟩ ⟨hle, h⟩ ⟨hle', h'⟩,
    cases hle.antisymm hle',
    simp only [true_and, eq_self_iff_true, heq_iff_eq, sigma.mk.inj_iff],
    ext s,
    refine (h _).trans _,
    rw fin.cast_le_of_eq rfl,
    simp only [fin.cast_refl, order_iso.refl_apply, set.image_id'],
  end }

[Kyle Miller]

I forgot to mention that part of the strategy is also to split open structures so that you get enough equalities between plain variables, which you need for cases/subst to work.