Proving equality of sigma types

Stream: general

[Sabrina Jewson]

Hi, so I’m still trying to implement finmap β ≃ Σ (keys : finset α), (Π (key ∈ keys), β key), and I’ve made some progress but now I’m completely stuck in heq hell. I need to prove equality of two sigma types to show that pair → map → pair is an identity (my goal is roughly of the form f (g x) = x where x : sigma β) — the trouble is that nearly every attempt to break apart that equality to prove it results in heq because of the nature of the sigma type. My code so far looks like this:

import data.finmap
import data.finset.image
import data.fintype.basic
import data.list.sigma

universes u v

private lemma option.heq_some_iff_get_heq {α : Type*} {β : Type*} {o : option α} {a : β} :
  o == some a ↔ ∃ h : o.is_some, option.get h == a :=
begin
  sorry
end

private def list.pmap_eq_self {α : Type*} {p : α → Prop}
  {f : Π a, p a → α} {l : list α} {prover : ∀ (a ∈ l), p a}
  (h : ∀ (x ∈ l), f x (prover x H) = x)
  : list.pmap f l prover = l
:= begin
  induction l,
  refl,
  rw list.pmap,
  rw h l_hd (or.inl rfl),
  rw l_ih (λ x H, h x (or.inr H)),
end

private def make_entries {α : Type*} {β : α → Type*} [decidable_eq α]
  (keys : finset α) (value : Π (key ∈ keys), β key)
  : multiset (sigma β)
:= keys.val.pmap
  (λ (elem : α) (elem_mem : elem ∈ keys.val), ⟨elem, value elem elem_mem⟩)
  (λ (elem : α), id)

def finmap.equiv_finset_fun {α : Type*} {β : α → Type*} [decidable_eq α] :
  finmap β ≃ Σ (keys : finset α), (Π (key ∈ keys), β key)
:= {
  to_fun := λ map, {
    fst := map.keys,
    snd := λ x x_mem, option.get (finmap.lookup_is_some.mpr x_mem),
  },
  inv_fun := λ pair, {
    entries := make_entries pair.1 pair.2,
    nodupkeys := @quot.ind _ _
      (λ (keys : multiset α),
        Π (keys_nodup : keys.nodup) (value : Π (key ∈ keys), β key),
          (make_entries ⟨keys, keys_nodup⟩ value).nodupkeys)
      (λ (keys : list α) (keys_nodup : keys.nodup) value,
        by simp [make_entries, list.nodupkeys, list.keys, list.map_pmap, keys_nodup])
      pair.1.val
      pair.1.nodup
      pair.2,
  },
  -- map → pair → map is an identity (not a pretty proof but I’ll come back to this later)
  left_inv := λ map, begin
    cases map,
    dsimp only [finmap.keys],
    apply finmap.ext,
    dsimp only,
    rw make_entries,
    dsimp only,
    simp only [multiset.keys],
    induction map_entries,
    simp,
    rw [list.pmap_map],
    convert ← list.perm.refl _,
    apply list.pmap_eq_self,
    intros x x_mem,
    cases x,
    simp,
    dsimp at map_nodupkeys,
    apply (@exists_prop_of_true _ (λ h, option.get h = x_snd) _).mp,
    apply option.eq_some_iff_get_eq.mp,
    dsimp only,
    apply @finmap.induction_on _ _
      (λ f, sigma.mk x_fst x_snd ∈ f.entries → finmap.lookup x_fst f = some x_snd) _
      (λ _, alist.mem_lookup_iff.mpr),
    exact x_mem,
    refl,
  end,
  -- pair → map → pair is an identity
  right_inv := λ pair, begin
    cases pair with keys val,
    cases keys,
    induction keys_val,

    -- STRATEGY 1: Don’t break the sigma
    dsimp only,
    dsimp only [make_entries],
    dsimp only [multiset.quot_mk_to_coe''],
    dsimp only [multiset.coe_pmap],
    dsimp only [finmap.keys],
    dsimp only [multiset.coe_keys],
    dsimp only [list.keys],
    have h :
      list.map sigma.fst (list.pmap (λ (elem : α) (elem_mem : elem ∈ ↑keys_val), ⟨ elem, val elem elem_mem ⟩) keys_val _)
      = list.pmap (λ (elem : α) (elem_mem : elem ∈ ↑keys_val), sigma.fst ⟨ elem, val elem elem_mem ⟩) keys_val _,
    { apply list.map_pmap },
    dsimp only [h],
    -- ^ errors, for some reason; `rw` and `simp` also fail, hence all the dsimps

    -- STRATEGY 2: Break the sigma
    fapply sigma.eq,
    simp [finmap.keys, make_entries, multiset.keys, list.map_pmap, list.map_id''],
    -- What now? How do I prove a goal of the form `_.rec_on (…) = …`?

    -- STRATEGY 3: Embrace the heq
    simp,
    constructor,
    { simp [finmap.keys, make_entries, multiset.keys, list.map_pmap, list.map_id''], },
    dsimp only,
    apply function.hfunext, refl, intros a b a_heq_b,
    have a_eq_b : a = b, from eq_of_heq a_heq_b,
    apply function.hfunext,
    { simp [finmap.keys, make_entries, multiset.keys, a_eq_b], },
    intros a_mem b_mem a_mem_eq_b_mem,
    apply (@exists_prop_of_true _ (λ h, option.get h == val b b_mem) _).mp,
    apply option.heq_some_iff_get_heq.mp,
    dsimp only [make_entries, multiset.quot_mk_to_coe'', multiset.coe_pmap],
    -- What now? I have no ideä how to simplify or prove this goal because it uses `heq`…
  end,
}

You can see the three different strategies I’ve tried, but with each one I encountered a dead end somehow. Any ideäs on this?

[Yury G. Kudryashov]

Do you mean "equality of 2 elements of a sigma type"? Because equality of types is something different.

[Yury G. Kudryashov]

Here is a complete proof with some auxiliary lemmas that should go to other files. The main trick I used was to use a subtype of a product type as an intermediate type. Probably, one can golf the last equivalence using existing equiv.*_congr constructions.

Code

import data.finmap
import data.finset.sigma

variables {ι : Type*} {α : ι → Type*}

namespace multiset

instance can_lift_finset {α} : can_lift (multiset α) (finset α) finset.val multiset.nodup :=
⟨λ m hm, ⟨⟨m, hm⟩, rfl⟩⟩

lemma nodup_keys {m : multiset (Σ i, α i)} : m.keys.nodup ↔ m.nodupkeys :=
by { rcases m with ⟨l⟩, refl }

lemma nodupkeys.nodup {m : multiset (Σ i, α i)} (h : m.nodupkeys) : m.nodup :=
(nodup_keys.2 h).of_map _

end multiset

@[simp] lemma part.to_option_is_some {α} (o : part α) [decidable o.dom] :
  o.to_option.is_some ↔ o.dom :=
by by_cases o.dom; simp [h, part.to_option]

namespace option

lemma get_eq_iff {α} {o : option α} {a : α} (h : o.is_some) :
  get h = a ↔ a ∈ o :=
by { rcases is_some_iff_exists.1 h with ⟨b, rfl⟩, rw [mem_def, get_some, some_inj] }

end option

namespace finmap

lemma lookup_eq_some_iff [decidable_eq ι] {f : finmap α} {i : ι} {x : α i} :
  f.lookup i = some x ↔ sigma.mk i x ∈ f.entries :=
by { rcases f with ⟨⟨l⟩, hl⟩, exact list.mem_lookup_iff hl }

protected lemma nodup (f : finmap α) : f.entries.nodup := f.nodupkeys.nodup

@[simp] lemma sigma_keys_lookup [decidable_eq ι] (f : finmap α) :
  f.keys.sigma (λ i, (f.lookup i).to_finset) = ⟨f.entries, f.nodup⟩ :=
begin
  ext x,
  have : x ∈ f.entries → x.fst ∈ f.keys, from multiset.mem_map_of_mem _,
  simpa [lookup_eq_some_iff]
end

variables [decidable_eq ι]

def keys_lookup_equiv :
  finmap α ≃ {f : finset ι × (Π i, option (α i)) // ∀ i, (f.2 i).is_some ↔ i ∈ f.1} :=
{ to_fun := λ f, ⟨(f.keys, λ i, f.lookup i), λ i, lookup_is_some⟩,
  inv_fun := λ f, ⟨(f.1.1.sigma $ λ i, (f.1.2 i).to_finset).val,
    begin
      refine multiset.nodup_keys.1 ((finset.nodup _).map_on _),
      simp only [finset.mem_val, finset.mem_sigma, option.mem_to_finset, option.mem_def],
      rintro ⟨i, x⟩ ⟨hi, hx⟩ ⟨j, y⟩ ⟨hj, hy⟩ (rfl : i = j),
      obtain rfl : x = y, from option.some.inj (hx.symm.trans hy),
      refl
    end⟩,
  left_inv := λ f, ext $ by simp,
  right_inv := λ ⟨⟨s, f⟩, hf⟩,
    begin
      ext : 2; dsimp [keys],
      { ext1 i,
        have : i ∈ s → (∃ x, f i = some x),
          from λ hi, ⟨option.get _, option.get_mem $ (hf i).2 hi⟩,
        simpa [multiset.keys] },
      { ext i x : 2,
        simp only [option.mem_def, lookup_eq_some_iff, finset.mem_val, finset.mem_sigma,
          option.mem_to_finset, and_iff_right_iff_imp, ← hf],
        exact λ h, option.is_some_iff_exists.2 ⟨_, h⟩ }
    end }

def finmap_equiv_sigma [decidable_eq ι] :
  finmap α ≃ Σ keys : finset ι, Π k ∈ keys, α k :=
keys_lookup_equiv.trans
{ to_fun := λ f, ⟨f.1.1, λ i hi, option.get $ (f.2 i).2 hi⟩,
  inv_fun := λ f, ⟨(f.1, λ i, part.to_option ⟨i ∈ f.1, f.2 i⟩),
    λ i, by simp⟩,
  left_inv := λ ⟨⟨s, f⟩, hf⟩,
    begin
      dsimp,
      congr' with i x,
      have : f i = some x → (f i).is_some, from λ h, option.is_some_iff_exists.2 ⟨_, h⟩,
      simpa [option.get_eq_iff, ← hf]
    end,
  right_inv := λ ⟨s, f⟩,
    begin
      dsimp,
      congr' with i hi,
      rw [option.get_eq_iff, part.mem_to_option],
      exact ⟨hi, rfl⟩
    end }

end finmap

[Sabrina Jewson]

Thank you very much! I’ll have to spend a while studying that :D

[Yury G. Kudryashov]

It's hard to work with equality of x y : Σ i, α i unless x.1 = y.1 is a definitional equality. So, it helps to isolate "actual work" from wrapping in convenient types.

[Yury G. Kudryashov]

BTW, I don't know which of the equivalences is more useful in practice.

[Yaël Dillies]

The trick to work with sigma types is to make x.1 = y.1 an equality of at least one free variable, then subst it. Then x.2 == y.2 becomes x.2 = y.2.

[Yury G. Kudryashov]

PRd non-sigma version: #18151. I'm not sure that we need the sigma version in mathlib because the math content is there but it's easier to deal with a subtype of a product than with a sigma type.