Zulip Chat Archive

Stream: general

Topic: Using propext for heq on metavariables


Izzy Meckler (May 22 2020 at 20:46):

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 (May 22 2020 at 20:47):

#mwe

Bhavik Mehta (May 22 2020 at 20:47):

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

Izzy Meckler (May 22 2020 at 20:48):

Bryan Gin-ge Chen said:

#mwe

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

Reid Barton (May 22 2020 at 20:49):

At a guess, you have two different subtypes

Bryan Gin-ge Chen (May 22 2020 at 20:51):

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 (May 22 2020 at 20:52):

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

Izzy Meckler (May 22 2020 at 20:55):

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 (May 22 2020 at 20:58):

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 (May 22 2020 at 21:07):

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 (May 22 2020 at 21:09):

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

Bhavik Mehta (May 22 2020 at 21:09):

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 (May 22 2020 at 21:09):

oh, there is another heq goal after that

Bhavik Mehta (May 22 2020 at 21:11):

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 (May 22 2020 at 21:14):

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

Mario Carneiro (May 22 2020 at 21:14):

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 (May 22 2020 at 21:15):

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 (May 22 2020 at 21:16):

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 (May 22 2020 at 21:16):

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

Mario Carneiro (May 22 2020 at 21:16):

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 (May 22 2020 at 21:17):

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

Mario Carneiro (May 22 2020 at 21:17):

= is not defined specially on any type

Mario Carneiro (May 22 2020 at 21:17):

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 (May 22 2020 at 21:17):

simp does not use only defeq, that would be dsimp

Izzy Meckler (May 22 2020 at 21:18):

ah! thank you mario

Mario Carneiro (May 22 2020 at 21:18):

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

Kevin Buzzard (May 22 2020 at 22:39):

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 (May 22 2020 at 23:32):

and you can even prove it in HoTT

Kevin Buzzard (May 22 2020 at 23:35):

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


Last updated: Dec 20 2023 at 11:08 UTC