golfing help

Stream: new members

[Jack J Garzella]

Hi,

I'm struggling how to figure out how to write proofs that aren't super super long. In particular, my current workflow is to write a bunch of have statements and then rewrite using them. This matches my mental model of how I think about how I would prove something on paper--in particular the have statements seem to be nice for communicating a proof to a human. However, they get quite cumbersome and people who answer my questions here (thanks again, especially @Adam Topaz ) seem to be able to prove things more efficiently. Or at least, they know how to golf all of the have statements away.

A good example is the following lemma, part of proving that a monoid object in the category of types is a monoid:

import category_theory.closed.cartesian
import category_theory.limits.has_limits
import category_theory.monoidal.Mon_
import category_theory.limits.types
import category_theory.limits.shapes.types
import category_theory.types

-- set_option pp.universes true
-- set_option pp.implicit true
-- set_option trace.simplify.rewrite true


noncomputable theory

universes u v


open category_theory
open category_theory.limits.types
open category_theory.concrete_category

instance : monoidal_category (Type u) :=
  monoidal_of_has_finite_products (Type u)

instance has_one_of_Mon__Type (M : Mon_ (Type u)) : has_one M.X :=
{ one := ((terminal_iso.symm.hom ≫ M.one) punit.star) }

instance has_mul_of_Mon__Type (M : Mon_ (Type u)) : has_mul M.X :=
{ mul := (λ a b, ((binary_product_iso _ _).symm.hom ≫ M.mul) (a,b)) }

@[simp, reassoc]
lemma binary_product_iso_limits_fst_eq_fst (A B : Type u) :
  (binary_product_iso A B).inv ≫ limits.prod.fst = prod.fst :=
limits.prod.lift_fst _ _

@[simp, reassoc]
lemma binary_product_iso_limits_snd_eq_snd (A B : Type u) :
  (binary_product_iso A B).inv ≫ limits.prod.snd = prod.snd :=
limits.prod.lift_snd _ _

def punit_prod_iso (A : Type u) : (punit : (Type u)) × A ≅ A :=
  (binary_product_iso _ _).symm ≪≫
  tensor_iso terminal_iso.symm (iso.refl _) ≪≫
  (λ_ A)

def punit_morph_prod (M : Mon_ (Type u)) : (punit : Type u) × M.X ⟶ M.X × M.X :=
  (binary_product_iso _ _).symm.hom ≫
  (tensor_iso terminal_iso.symm (iso.refl _)).hom ≫
  (M.one ⊗ (𝟙 M.X)) ≫
  (binary_product_iso _ _).hom

lemma prod_map_bpo_commutes (A B C D : Type u) (f : A ⟶ C) (g : B ⟶ D) :
as_hom (prod.map f g) ≫
(binary_product_iso C D).inv =
(binary_product_iso A B).inv ≫
limits.prod.map f g :=
by { ext1; simpa }

lemma rearrange_comp (a b c d e : Type u) (f : a ⟶ b) (g : b ⟶ c) (h : c ⟶ d) (j : d ⟶ e) :
(f ≫ g) ≫ h ≫ j = (f ≫ (g ≫ h)) ≫ j :=
by simp

lemma rearrange_comp_2  (a b c d e : Type u) (f : a ⟶ b) (g : b ⟶ c) (h : c ⟶ d) (j : d ⟶ e) :
(f ≫ g ≫ h) ≫ j = (f ≫ g) ≫ h ≫ j :=
by simp

lemma one_mul_of_Mon__Type (M : Mon_ (Type u)) : ∀ (a : M.X), 1 * a = a :=
begin
  have mul := M.mul,
  let om := M.one_mul,

  intro a,
  have morph_one_a : (prod.map (terminal_iso.symm.hom ≫ M.one) (𝟙 M.X)) (punit.star,a) =
    ((terminal_iso.symm.hom ≫ M.one) punit.star, a),
    by simp,
  have morph_one_comp_a :
    (as_hom (prod.map terminal_iso.inv (𝟙 M.X)) ≫
    as_hom (prod.map M.one (𝟙 M.X))) (punit.star, a) =
    ((terminal_iso.symm.hom ≫ M.one) punit.star, a),
    begin
      simp only [category_theory.types_comp_apply, category_theory.iso.symm_hom],
      refl,
    end,

  have comm_rectangle_terminal_iso:
    as_hom (prod.map (terminal_iso.inv) (𝟙 M.X)) ≫
    (binary_product_iso _ _).symm.hom =
    (binary_product_iso _ _).symm.hom ≫
    ((terminal_iso.symm.hom) ⊗ (𝟙 M.X)), -- you have to have the outer parens
    by { simp, apply prod_map_bpo_commutes },

  have comm_rectangle_prod_map :
    as_hom (prod.map M.one (𝟙 M.X)) ≫
    (binary_product_iso _ _).symm.hom =
    (binary_product_iso _ _).symm.hom ≫
    (M.one ⊗ (𝟙 M.X)), -- you have to have the outer parens
    by { simp, apply prod_map_bpo_commutes },

  have rearrange_composition :
    (as_hom (prod.map terminal_iso.inv (𝟙 M.X)) ≫
    as_hom (prod.map M.one (𝟙 M.X))) ≫
    (binary_product_iso M.X M.X).symm.hom ≫
    M.mul =
    (as_hom (prod.map terminal_iso.inv (𝟙 M.X)) ≫
    (as_hom (prod.map M.one (𝟙 M.X)) ≫
    (binary_product_iso M.X M.X).symm.hom)) ≫
    M.mul,
    begin
      by apply rearrange_comp,
      -- simp,
      -- `simp` should work here, at the time of writing this comment it seems to time out
    end,

  have rearrange_composition_2 :
    ((as_hom (prod.map terminal_iso.inv (𝟙 M.X)) ≫
    (binary_product_iso (𝟙_ (Type u)) M.X).symm.hom ≫
    (M.one ⊗ 𝟙 M.X)) ≫
    M.mul) =
    (as_hom (prod.map terminal_iso.inv (𝟙 M.X)) ≫
    (binary_product_iso (𝟙_ (Type u)) M.X).symm.hom) ≫
    (M.one ⊗ 𝟙 M.X) ≫
    M.mul,
    by apply rearrange_comp_2,

  have same_morphism :
    (binary_product_iso (⊤_ Type u) M.X).symm.hom = (binary_product_iso (𝟙_ (Type u)) M.X).symm.hom,
    by refl,

  have ppo_equality :
    (((binary_product_iso punit M.X).symm.hom ≫ (terminal_iso.symm.hom ⊗ 𝟙 M.X)) ≫ (λ_ M.X).hom)
    = prod.snd,
    by simp,

  unfold has_mul.mul,
  unfold has_one.one,
  rw [←morph_one_comp_a],
  rw [←(types_comp_apply (as_hom (prod.map terminal_iso.inv (𝟙 M.X)) ≫
                         as_hom (prod.map M.one (𝟙 M.X)))
                         ((binary_product_iso M.X M.X).symm.hom ≫
                         M.mul))],

  rw [rearrange_composition],
  rw [comm_rectangle_prod_map],
  rw [rearrange_composition_2],
  rw [←same_morphism],
  rw [comm_rectangle_terminal_iso],
  rw [om],
  rw [ppo_equality],
end

Each of the have statements/auxillary lemmas pretty much comes down to simp. Does anyone have any tips and tricks on how one golfs such a proof?

[Andrew Yang]

This is how I would have approached this problem:

instance : monoidal_category (Type u) :=
  monoidal_of_has_finite_products (Type u)

instance has_one_of_Mon__Type (M : Mon_ (Type u)) : has_one M.X :=
{ one := ((terminal_iso.symm.hom ≫ M.one) punit.star) }

instance has_mul_of_Mon__Type (M : Mon_ (Type u)) : has_mul M.X :=
{ mul := (λ a b, ((binary_product_iso _ _).symm.hom ≫ M.mul) (a,b)) }

lemma one_mul_of_Mon__Type (M : Mon_ (Type u)) : ∀ (a : M.X), 1 * a = a :=
begin
  intro a,
  dsimp [has_mul.mul, has_one.one],
  have : (binary_product_iso _ _).inv ≫ (M.one ⊗ 𝟙 M.X) ≫ M.mul =
    (binary_product_iso _ _).inv ≫ (λ_ M.X).hom,
  { rw M.one_mul },
  convert _root_.congr_fun this (terminal_iso.inv punit.star, a),
  { have : function.injective (binary_product_iso M.X M.X).hom,
    { rw ← mono_iff_injective, apply_instance },
    apply this,
    ext; simp [elementwise_of (limits.prod.map_fst M.one (𝟙 M.X)),
      elementwise_of (limits.prod.map_snd M.one (𝟙 M.X))] },
  { simp }
end

This is roughly how I came up with this proof:

1. I know that the proof "is just M.one_mul", so I first applied a into M.one_mul (by composing with binary_product_iso and using congr_fun.
2. I applied simp on both the goal and the hypothesis obtained, and see what I have. In this case the hypothesis already looks like the goal, so I used convert.
3. In the lhs, the two elements (in limits.prod _ _) are equal since the components are (this is usually done by ext). I moved into prod since the extlemmas there looks better.
4. Apply simp again. The only barrier seems to be limits.prod.fst (limits.prod.map foo) so the elementwise_of versions of them are provided. simp then closes the goal.
5. The rhs can also be closed by simp.

[Jack J Garzella]

Ok, I have one question:

how would I "use congr_fun" without knowing that I already had to use the convert tactic? All of the tactics I use seem to give errors.

[Andrew Yang]

I would first have := _root_.congr_fun this (terminal_iso.inv punit.star, a)
And then I could simp at this ⊢.