Using propext for heq on metavariables

Stream: general

[Izzy Meckler]

I am in the following proof state in lean (as part of proving a group decomposes into cosets)

G : Group,
H : subgroup G,
X : coset H,
x : ↥G,
x_in_X : x ∈ X.val
⊢ ⟨x, _⟩ == ⟨x, x_in_X⟩

and this should be true by the fact that membership is a Prop, but I can't figure out how to get that to work. i wrote a lemme analogous to subtype.eq for heterogeneous equality but it didn't unify when i applied it:

lemma subtype_triviality {A : Type u}
    { P : A → Prop }
    {x : A}
    {w1 w2 : P x}
    : @heq { a : A // P a } ⟨ x, w1 ⟩ { a : A // P a } ⟨ x, w2 ⟩
    := ...

applying this gives the error

invalid apply tactic, failed to unify
  ⟨x, _⟩ == ⟨x, x_in_X⟩
with
  ⟨?m_3, ?m_4⟩ == ⟨?m_3, ?m_5⟩

[Bryan Gin-ge Chen]

#mwe

[Bhavik Mehta]

Try using congr (or hcongr?) on your goal, maybe

[Izzy Meckler]

Bryan Gin-ge Chen said:

#mwe

the development is a few hundred lines... should i just post it here?

[Reid Barton]

At a guess, you have two different subtypes

[Bryan Gin-ge Chen]

You should minimize the code so that the same issue appears. I doubt that every single one of those lines is necessary to reproduce this.

[Reid Barton]

Also, it seems likely that you should not have done whatever caused == to appear

[Izzy Meckler]

Reid Barton said:

Also, it seems likely that you should not have done whatever caused == to appear

it appeared as a result of simping an equality in a sigma type... in any case, is it not possible to just give a name to the underscore variable and then just use propext to finish this off?

[Izzy Meckler]

Izzy Meckler said:

Bryan Gin-ge Chen said:

#mwe

the development is a few hundred lines... should i just post it here?

I am a Lean novice, so my apologies if there is stuff that could be done more nicely

import data.set.basic
import algebra.category.Group
import data.subtype
import category_theory.isomorphism
open set

def subgroup (G : Group) := { H : set G // is_subgroup H }

def shift { G : Group } (x : G) (H : set G) : set G := { g | H (x⁻¹ * g) }

def is_coset_of {G : Group} (H : subgroup G) (K : set G) : Prop :=
    exists (x : G), K = shift x H.val

def coset {G : Group} (H : subgroup G) := { K : set G // is_coset_of H K }

def shift_coset {G : Group} (x : G) (H : subgroup G) : coset H :=
    ⟨ shift x H.val , exists.intro x begin trivial end ⟩

def subgroup_property' {G : Group} (H : subgroup G)
    : forall x y, x ∈ H.val → ((y ∈ H.val) ↔ ((x*y) ∈ H.val)) :=
begin
intros,
induction H,
apply iff.intro,
apply H_property.mul_mem,
apply a,
intros,
have h : x⁻¹ * (x * y) ∈ H_val,
    apply H_property.mul_mem,
    apply H_property.inv_mem,
    apply a,
    apply a_1,
have e : x⁻¹ * (x * y) = y,
    apply inv_mul_cancel_left,
    rewrite <- e,
    apply h,
end

def subgroup_property {G : Group} (H : subgroup G)
    : forall x y, x ∈ H.val → ((y ∈ H.val) = ((x*y) ∈ H.val)) :=
    begin
    intros,
    apply propext,
    apply subgroup_property',
    apply a,
end

lemma mul_subgroup_property {G : Group} (H : subgroup G)
    : forall x y, H.val x → (H.val y ↔ H.val (x * y)) :=
begin
intros,
have h0 : (x ∈ H.val ↔ H.val x), apply mem_def,
rewrite <- h0 at a,
apply iff.intro,
intros,
have h1 : (y ∈ H.val ↔ H.val y), apply mem_def,
rewrite <- h1 at a_1,
apply H.property.mul_mem,
apply a, apply a_1,

intros,
have ai : x⁻¹ ∈ H.val,
apply H.property.inv_mem, apply a,
rewrite <- inv_mul_cancel_left x y,
have m : x⁻¹ * (x * y) ∈ H.val,
apply H.property.mul_mem, apply ai,
rewrite mem_def, apply a_1,
rewrite mem_def at m,
apply m,
end

lemma inv_subgroup_property {G : Group} (H : subgroup G)
    : forall x, H.val x ↔ H.val (x⁻¹) :=
begin
intros,
have h : (x ∈ H.val ↔ H.val x),
apply mem_def,
rewrite <- h,
have h : (x⁻¹ ∈ H.val ↔ H.val x⁻¹ ),
apply mem_def,
rewrite <- h,
apply iff.intro,
intros,
apply H.property.inv_mem, apply a,
intros,
have e : x = x⁻¹⁻¹, rewrite inv_inv,
rewrite e,
apply H.property.inv_mem,
apply a,
end

lemma coset_characterization
{G : Group} {H : subgroup G}
    (X : coset H) (g : G)
    : g ∈ X.val →  X.val = shift g H.val
    :=
begin
let H_val := H.val,
intros,
induction X,
apply ext,
intro y,
simp,
induction X_property,
rename X_property_w x,
simp at a,
rewrite X_property_h at a,
rewrite X_property_h,
rewrite mem_def, rewrite mem_def,
unfold shift,
rewrite set_of_app_iff,
rewrite set_of_app_iff,
unfold shift at a,
have h : (g⁻¹ * x) ∈ H.val, rewrite mem_def at a,
rewrite set_of_app_iff at a,
rewrite mem_def,
rewrite inv_subgroup_property,
rewrite mul_inv_rev,
rewrite inv_inv,
apply a,
have i : H.val (x⁻¹ * y) ↔ H.val ((g⁻¹ * x ) * (x⁻¹ * y)),
rewrite mul_subgroup_property, rewrite mem_def at h, apply h,
rewrite i,  rewrite mul_assoc,
rewrite mul_inv_cancel_left x y,
end

def cosets_disjoint {G: Group} {H : subgroup G}
    (X Y : coset H)
    : ∀ g, (g ∈ X.val) ∧ (g ∈ Y.val) → X = Y :=
begin
    intros,
    apply subtype.eq',
    induction a,
    have eX : (X.val = shift g H.val),
    apply coset_characterization, apply a_left,
    have eY : (Y.val = shift g H.val),
    apply coset_characterization, apply a_right,
    rewrite eX, rewrite eY,
end

def underlying_type (G : Group) : Type := G

universe u
universe v

def mem_def' {a : Type u} (X : set a) (x : a)
    : x ∈ X ↔ X x := begin
    intros,
    apply mem_def
end

lemma g_in_gH {G: Group} {H : subgroup G} (g : G)
    : g ∈ (shift_coset g H).val :=
begin
    intros,
    rewrite mem_def,
    unfold shift_coset,
    simp, unfold shift,
    rewrite set_of_app_iff,
    rewrite inv_mul_self,
    rewrite <- (mem_def' H.val 1),
    apply H.property.one_mem
end

lemma subtype_triviality {A : Type u}
    { P : A → Prop }
    {x : A}
    {w1 w2 : P x}
    : @heq { a : A // P a } ⟨ x, w1 ⟩ { a : A // P a } ⟨ x, w2 ⟩
    := begin
    intros,
    have e : w1 = w2,
    trivial,
    rewrite e,
end

def coset_decomposition {G: Group} (H : subgroup G)
: underlying_type G ≅ Σ (X : coset H), { x : G // x ∈ X.val }
:=
    { hom := λ g, sigma.mk (shift_coset g H) ⟨ g , g_in_gH g⟩
    , inv:= (λ ⟨ X, ⟨ g, _ ⟩ ⟩, g)
    , hom_inv_id' := begin
        apply funext,
        intros,
        simp, unfold coset_decomposition._match_1,
      end
    , inv_hom_id' := begin
        apply funext, intros, induction x,
        rename x_fst X,
        induction x_snd with x x_in_X,
        simp,
        unfold coset_decomposition._match_1,
        split, unfold shift_coset,
        have e : shift x H.val = X.val,
        rewrite <- coset_characterization, apply x_in_X,
        apply subtype.eq, simp, apply e,
        sorry, -- Here is where the goal is
    end
    }

[Bryan Gin-ge Chen]

You had a bunch of defs which should be theorem or lemma instead. All proofs of lemmas can be replaced with sorry when making a MWE. Then you can remove lemmas and defs which aren't referenced:

import data.set.basic
import algebra.category.Group
import data.subtype
import category_theory.isomorphism
open set

def subgroup (G : Group) := { H : set G // is_subgroup H }
def shift { G : Group } (x : G) (H : set G) : set G := { g | H (x⁻¹ * g) }
def is_coset_of {G : Group} (H : subgroup G) (K : set G) : Prop :=
    exists (x : G), K = shift x H.val
def coset {G : Group} (H : subgroup G) := { K : set G // is_coset_of H K }
def shift_coset {G : Group} (x : G) (H : subgroup G) : coset H :=
    ⟨ shift x H.val , exists.intro x begin trivial end ⟩

lemma coset_characterization
{G : Group} {H : subgroup G}
    (X : coset H) (g : G)
    : g ∈ X.val →  X.val = shift g H.val
    :=
sorry

def underlying_type (G : Group) : Type := G

universe u
universe v

lemma mem_def' {a : Type u} (X : set a) (x : a)
    : x ∈ X ↔ X x := sorry
lemma g_in_gH {G: Group} {H : subgroup G} (g : G)
    : g ∈ (shift_coset g H).val :=
sorry

def coset_decomposition {G: Group} (H : subgroup G)
: underlying_type G ≅ Σ (X : coset H), { x : G // x ∈ X.val }
:=
    { hom := λ g, sigma.mk (shift_coset g H) ⟨ g , g_in_gH g⟩
    , inv:= (λ ⟨ X, ⟨ g, _ ⟩ ⟩, g)
    , hom_inv_id' := begin
        apply funext,
        intros,
        simp, unfold coset_decomposition._match_1,
      end
    , inv_hom_id' := begin
        apply funext, intros, induction x,
        rename x_fst X,
        induction x_snd with x x_in_X,
        simp,
        unfold coset_decomposition._match_1,
        split, unfold shift_coset,
        have e : shift x H.val = X.val,
        rewrite <- coset_characterization, apply x_in_X,
        apply subtype.eq, simp, apply e,
        sorry, -- Here is where the goal is
    end
    }

[Mario Carneiro]

You can prove the lemma if you replace the apply subtype.eq line with cases X, cases e, refl,

[Bhavik Mehta]

I'm sure others can tell you better than I how to improve your code, but the immediate thing which stands out to me is that you're showing isomorphism between two types, so it's easier to use equiv instead. I finished your goal in this context:

def coset_decomposition {G: Group} (H : subgroup G)
: underlying_type G ≃ Σ (X : coset H), { x : G // x ∈ X.val }
:=
    { to_fun := λ g, sigma.mk (shift_coset g H) ⟨ g , g_in_gH g⟩
    , inv_fun := (λ ⟨ X, ⟨ g, _ ⟩ ⟩, g)
    , left_inv := begin
        intro x,
        intros,
        simp, unfold coset_decomposition._match_1,
      end
    , right_inv := λ x, begin
        intros, induction x,
        induction x_snd with x x_in_X,
        dsimp,
        congr,
        unfold coset_decomposition._match_1,
        unfold shift_coset,
        apply subtype.eq,
        exact (coset_characterization _ _ x_in_X).symm,
        funext t,
        dsimp [shift_coset, coset_decomposition._match_1],
        rw ← (coset_characterization _ _ x_in_X),
        apply proof_irrel_heq,
    end
    }

[Mario Carneiro]

oh, there is another heq goal after that

[Bhavik Mehta]

The key thing I did which made it work here was to use congr which broke up the constructor into nicer things, and then proof_irrel_heq to take care of the _. That said, I still agree that some design thing has gone wrong which is leading to this - the most obvious to me is that you want to define an extensionality property for cosets

[Izzy Meckler]

Thanks everyone for all the tips! Still confused what exactly what is going wrong or even why the heterogeneous equality goal appears

[Mario Carneiro]

This is a cleaned up version of Bhavik's proof

def coset_decomposition {G: Group} (H : subgroup G) :
  underlying_type G ≃ Σ (X : coset H), { x : G // x ∈ X.val } :=
{ to_fun := λ g, ⟨shift_coset g H, g, g_in_gH g⟩,
  inv_fun := λ x, x.2.1,
  left_inv := begin
    intro x,
    intros,
    simp,
  end,
  right_inv := begin
    rintro ⟨X, g, x_in_X⟩,
    dsimp,
    have : shift_coset g H = X,
    { unfold shift_coset,
      apply subtype.eq,
      exact (coset_characterization _ _ x_in_X).symm },
    subst X,
  end }

[Bhavik Mehta]

The heq goal appears because you're trying to show two cosets are equal, and the second argument of a coset depends on the first (and the second argument is a prop)

[Mario Carneiro]

The key step here is to replace the step that produced the heq, the congr on a dependent pair, with a have that the first components are equal followed by a subst

[Izzy Meckler]

right, makes sense -- but is = on sigma types defined in terms of heq?

[Mario Carneiro]

in this case, that's actually the end of the proof, but usually you would have to then follow up with a proof that the second components are equal (but since the first types are now the same this is a regular equal)

[Izzy Meckler]

my understanding was that simp just computes using the definitional equality, is this not the case?

[Mario Carneiro]

= is not defined specially on any type

[Mario Carneiro]

congr knows how to prove equality of sigma types (or more generally, dependent functions) by reducing to heq, but this is usually the wrong move

[Mario Carneiro]

simp does not use only defeq, that would be dsimp

[Izzy Meckler]

ah! thank you mario

[Mario Carneiro]

in particular simp has a rule that will rewrite <x, y> = <z, w> <-> x = y /\ z == w

[Kevin Buzzard]

Equality of dependent types is a bit of a thorny issue in dependent type theory. Equality of types in general is a bit weird. You apparently can't disprove nat = int in lean

[Mario Carneiro]

and you can even prove it in HoTT

[Kevin Buzzard]

https://twitter.com/XenaProject/status/1263841150009475073

"Mathematics is the art of giving the same name to different things." - Henri Poincaré. Dependent type theory's `=` doesn't prove R[1/fg]=R[1/f][1/g] and Homotopy Type Theory's = lets things be equal even if they're non-canonically isomorphic. Computers haven't mastered this art.

- The Xena Project (@XenaProject)