## Stream: general

### Topic: avoiding heq

#### Peter Nelson (Jan 27 2023 at 13:33):

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 (Jan 27 2023 at 13:47):

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 (Jan 27 2023 at 13:49):

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.

Last updated: Aug 03 2023 at 10:10 UTC