Zulip Chat Archive

Stream: general

Topic: so what is eq.rec?


view this post on Zulip Kenny Lau (Apr 16 2018 at 04:35):

I'm stuck in this state:

A : orbits G X,
x : X,
hx : ⟦x⟧ = A,
z : ↥(stab G X ↑⟨x, hx⟩)
⊢ ((eq.rec ⟨⟨x, rfl ⟦x⟧⟩, z⟩ hx).fst).val = x

view this post on Zulip Kenny Lau (Apr 16 2018 at 04:35):

I don't see any way to destruct eq.rec

view this post on Zulip Kenny Lau (Apr 16 2018 at 04:35):

⟨⟨x, rfl ⟦x⟧⟩, z⟩ is subtype inside sigma

view this post on Zulip Mario Carneiro (Apr 16 2018 at 04:36):

pp.all?

view this post on Zulip Mario Carneiro (Apr 16 2018 at 04:37):

You should probably subst A

view this post on Zulip Kenny Lau (Apr 16 2018 at 04:37):

@eq.{v+1} X
    (@subtype.val.{v+1} X
       (λ (x : X),
          @eq.{v+1} (@quotient.{v+1} X (@group_action.orbit_rel.{u v} G _inst_1 X _inst_2))
            (@quotient.mk.{v+1} X (@group_action.orbit_rel.{u v} G _inst_1 X _inst_2) x)
            A)
       (@sigma.fst.{v u}
          (@subtype.{v+1} X
             (λ (x : X),
                @eq.{v+1} (@quotient.{v+1} X (@group_action.orbit_rel.{u v} G _inst_1 X _inst_2))
                  (@quotient.mk.{v+1} X (@group_action.orbit_rel.{u v} G _inst_1 X _inst_2) x)
                  A))
          (λ
           (a :
             @subtype.{v+1} X
               (λ (x : X),
                  @eq.{v+1} (@quotient.{v+1} X (@group_action.orbit_rel.{u v} G _inst_1 X _inst_2))
                    (@quotient.mk.{v+1} X (@group_action.orbit_rel.{u v} G _inst_1 X _inst_2) x)
                    A)),
             @subtype.{u+1} G
               (λ (x : G),
                  @has_mem.mem.{u u} G (set.{u} G) (@set.has_mem.{u} G) x
                    (@group_action.stab.{u v} G _inst_1 X _inst_2
                       (@coe.{(max 1 (v+1)) v+1}
                          (@subtype.{v+1} X
                             (λ (x : X),
                                @eq.{v+1} (@quotient.{v+1} X (@group_action.orbit_rel.{u v} G _inst_1 X _inst_2))
                                  (@quotient.mk.{v+1} X (@group_action.orbit_rel.{u v} G _inst_1 X _inst_2) x)
                                  A))
                          X
                          (@coe_to_lift.{(max 1 (v+1)) v+1}
                             (@subtype.{v+1} X
                                (λ (x : X),
                                   @eq.{v+1} (@quotient.{v+1} X (@group_action.orbit_rel.{u v} G _inst_1 X _inst_2))
                                     (@quotient.mk.{v+1} X (@group_action.orbit_rel.{u v} G _inst_1 X _inst_2) x)
                                     A))
                             X
                             (@coe_base.{(max 1 (v+1)) v+1}
                                (@subtype.{v+1} X
                                   (λ (x : X),
                                      @eq.{v+1} (@quotient.{v+1} X (@group_action.orbit_rel.{u v} G _inst_1 X _inst_2))
                                        (@quotient.mk.{v+1} X (@group_action.orbit_rel.{u v} G _inst_1 X _inst_2) x)
                                        A))
                                X
                                (@coe_subtype.{v+1} X
                                   (λ (x : X),
                                      @eq.{v+1} (@quotient.{v+1} X (@group_action.orbit_rel.{u v} G _inst_1 X _inst_2))
                                        (@quotient.mk.{v+1} X (@group_action.orbit_rel.{u v} G _inst_1 X _inst_2) x)
                                        A))))
                          a))))
          (@eq.rec.{(max v u)+1 v+1} (@group_action.orbits.{u v} G _inst_1 X _inst_2)
             (@quotient.mk.{v+1} X (@group_action.orbit_rel.{u v} G _inst_1 X _inst_2) x)
             (λ (_x : @group_action.orbits.{u v} G _inst_1 X _inst_2),
                @sigma.{v u}
                  (@subtype.{v+1} X
                     (λ (x : X),
                        @eq.{v+1} (@quotient.{v+1} X (@group_action.orbit_rel.{u v} G _inst_1 X _inst_2))
                          (@quotient.mk.{v+1} X (@group_action.orbit_rel.{u v} G _inst_1 X _inst_2) x)
                          _x))
                  (λ
                   (x :
                     @subtype.{v+1} X
                       (λ (x : X),
                          @eq.{v+1} (@quotient.{v+1} X (@group_action.orbit_rel.{u v} G _inst_1 X _inst_2))
                            (@quotient.mk.{v+1} X (@group_action.orbit_rel.{u v} G _inst_1 X _inst_2) x)
                            _x)),
                     @subtype.{u+1} G
                       (λ (x_1 : G),
                          @has_mem.mem.{u u} G (set.{u} G) (@set.has_mem.{u} G) x_1
                            (@group_action.stab.{u v} G _inst_1 X _inst_2
                               (@coe.{(max 1 (v+1)) v+1}
                                  (@subtype.{v+1} X
                                     (λ (x : X),
                                        @eq.{v+1}
                                          (@quotient.{v+1} X (@group_action.orbit_rel.{u v} G _inst_1 X _inst_2))
                                          (@quotient.mk.{v+1} X (@group_action.orbit_rel.{u v} G _inst_1 X _inst_2) x)
                                          _x))
                                  X
                                  (@coe_to_lift.{(max 1 (v+1)) v+1}
                                     (@subtype.{v+1} X
                                        (λ (x : X),
                                           @eq.{v+1}
                                             (@quotient.{v+1} X (@group_action.orbit_rel.{u v} G _inst_1 X _inst_2))
                                             (@quotient.mk.{v+1} X (@group_action.orbit_rel.{u v} G _inst_1 X _inst_2)
                                                x)
                                             _x))
                                     X
                                     (@coe_base.{(max 1 (v+1)) v+1}
                                        (@subtype.{v+1} X
                                           (λ (x : X),
                                              @eq.{v+1}
                                                (@quotient.{v+1} X (@group_action.orbit_rel.{u v} G _inst_1 X _inst_2))
                                                (@quotient.mk.{v+1} X
                                                   (@group_action.orbit_rel.{u v} G _inst_1 X _inst_2)
                                                   x)
                                                _x))
                                        X
                                        (@coe_subtype.{v+1} X
                                           (λ (x : X),
                                              @eq.{v+1}
                                                (@quotient.{v+1} X (@group_action.orbit_rel.{u v} G _inst_1 X _inst_2))
                                                (@quotient.mk.{v+1} X
                                                   (@group_action.orbit_rel.{u v} G _inst_1 X _inst_2)
                                                   x)
                                                _x))))
                                  x)))))
             (@sigma.mk.{v u}
                (@subtype.{v+1} X
                   (λ (x_1 : X),
                      @eq.{v+1} (@quotient.{v+1} X (@group_action.orbit_rel.{u v} G _inst_1 X _inst_2))
                        (@quotient.mk.{v+1} X (@group_action.orbit_rel.{u v} G _inst_1 X _inst_2) x_1)
                        (@quotient.mk.{v+1} X (@group_action.orbit_rel.{u v} G _inst_1 X _inst_2) x)))
                (λ
                 (x_1 :
                   @subtype.{v+1} X
                     (λ (x_1 : X),
                        @eq.{v+1} (@quotient.{v+1} X (@group_action.orbit_rel.{u v} G _inst_1 X _inst_2))
                          (@quotient.mk.{v+1} X (@group_action.orbit_rel.{u v} G _inst_1 X _inst_2) x_1)
                          (@quotient.mk.{v+1} X (@group_action.orbit_rel.{u v} G _inst_1 X _inst_2) x))),
                   @subtype.{u+1} G
                     (λ (x_2 : G),
                        @has_mem.mem.{u u} G (set.{u} G) (@set.has_mem.{u} G) x_2
                          (@group_action.stab.{u v} G _inst_1 X _inst_2
                             (@coe.{(max 1 (v+1)) v+1}
                                (@subtype.{v+1} X
                                   (λ (x_1 : X),
                                      @eq.{v+1} (@quotient.{v+1} X (@group_action.orbit_rel.{u v} G _inst_1 X _inst_2))
                                        (@quotient.mk.{v+1} X (@group_action.orbit_rel.{u v} G _inst_1 X _inst_2) x_1)
                                        (@quotient.mk.{v+1} X (@group_action.orbit_rel.{u v} G _inst_1 X _inst_2) x)))
                                X
                                (@coe_to_lift.{(max 1 (v+1)) v+1}
                                   (@subtype.{v+1} X
                                      (λ (x_1 : X),
                                         @eq.{v+1}
                                           (@quotient.{v+1} X (@group_action.orbit_rel.{u v} G _inst_1 X _inst_2))
                                           (@quotient.mk.{v+1} X (@group_action.orbit_rel.{u v} G _inst_1 X _inst_2)
                                              x_1)
                                           (@quotient.mk.{v+1} X (@group_action.orbit_rel.{u v} G _inst_1 X _inst_2)
                                              x)))
                                   X
                                   (@coe_base.{(max 1 (v+1)) v+1}
                                      (@subtype.{v+1} X
                                         (λ (x_1 : X),
                                            @eq.{v+1}
                                              (@quotient.{v+1} X (@group_action.orbit_rel.{u v} G _inst_1 X _inst_2))
                                              (@quotient.mk.{v+1} X (@group_action.orbit_rel.{u v} G _inst_1 X _inst_2)
                                                 x_1)
                                              (@quotient.mk.{v+1} X (@group_action.orbit_rel.{u v} G _inst_1 X _inst_2)
                                                 x)))
                                      X
                                      (@coe_subtype.{v+1} X
                                         (λ (x_1 : X),
                                            @eq.{v+1}
                                              (@quotient.{v+1} X (@group_action.orbit_rel.{u v} G _inst_1 X _inst_2))
                                              (@quotient.mk.{v+1} X (@group_action.orbit_rel.{u v} G _inst_1 X _inst_2)
                                                 x_1)
                                              (@quotien

view this post on Zulip Kenny Lau (Apr 16 2018 at 04:37):

lol too long

view this post on Zulip Kenny Lau (Apr 16 2018 at 04:38):

oh, lol, subst did the job

view this post on Zulip Kenny Lau (Apr 16 2018 at 04:38):

how does it work?

view this post on Zulip Mario Carneiro (Apr 16 2018 at 04:38):

You have an equality assumption [[x]] = A, and a bunch of complicated stuff that depends on it

view this post on Zulip Mario Carneiro (Apr 16 2018 at 04:39):

to reduce an eq.rec you need the major premise to become refl somehow

view this post on Zulip Mario Carneiro (Apr 16 2018 at 04:39):

that usually means finding the appropriate equality in the context and generalizing it until one side is a variable, and then subst, which is to say use eq.rec in the proof term

view this post on Zulip Kenny Lau (Apr 16 2018 at 04:43):

eq.rec ⟨⟨x, rfl ⟦x⟧⟩, z⟩ hx = ⟨⟨x, hx⟩, z⟩

is cleared by:

(eq.drec
   (λ (z : ↥(stab G X ↑⟨snd_fst_val, eq.refl ⟦snd_fst_val⟧⟩)),
      eq.refl
        (eq.rec_on (eq.refl ⟦snd_fst_val⟧)
           (((λ (z : Σ (x : X), ↥(stab G X x)),
             ⟨⟦z.fst⟧, ⟨⟨z.fst, rfl ⟦z.fst⟧⟩, z.snd⟩⟩)
            ((λ
              (z :
                Σ (A : orbits G X) (x : ↥{x : X | ⟦x⟧ = A}), ↥(stab G X ↑x)),
                ⟨((z.snd).fst).val, (z.snd).snd⟩)
               ⟨⟦snd_fst_val⟧, ⟨⟨snd_fst_val, eq.refl ⟦snd_fst_val⟧⟩, z⟩⟩)).snd)))
   snd_fst_property
   snd_snd)

view this post on Zulip Kenny Lau (Apr 16 2018 at 04:43):

I printed to look at the proof term

view this post on Zulip Kenny Lau (Apr 16 2018 at 04:44):

so maybe drec would have worked?

view this post on Zulip Mario Carneiro (Apr 16 2018 at 04:44):

I guess it uses eq.drec since you also need to replace hx in the term with eq.refl, but it's not necessary provided you generalize hx by proof irrelevance


Last updated: May 14 2021 at 03:27 UTC