# Zulip Chat Archive

## 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 `heq`

s naturally become `eq`

s.

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