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: Dec 20 2023 at 11:08 UTC