Zulip Chat Archive

Stream: general

Topic: match


Johan Commelin (Mar 11 2022 at 12:57):

How should one use match?

import algebra.homology.homotopy
import category_theory.abelian.basic

noncomputable theory

open category_theory

variables {ι₁ ι₂ : Type*}

namespace complex_shape

structure embedding (c₁ : complex_shape ι₁) (c₂ : complex_shape ι₂) :=
(f : ι₁  ι₂)
(r : ι₂  option ι₁)
(rf :  i, r (f i) = i)
(eq_none :  i, r i = none   i', f i'  i)
(c :  i j⦄, c₁.rel i j  c₂.rel (f i) (f j))

end complex_shape

variables {c₁ : complex_shape ι₁} {c₂ : complex_shape ι₂}
variables {C : Type*} [category C] [abelian C]

namespace homological_complex

open_locale zero_object

variables (e : c₁.embedding c₂)
variables (X : homological_complex C c₁)

@[reducible]
def embed.X : ι₂  C := λ i,
match e.r i with
| some i' := X.X i'
| none    := 0
end

def embed.d : Π (i j : ι₂), embed.X e X i  embed.X e X j := λ i j,
match e.r i, e.r j with
| some i', some j' := show X.X i'  X.X j', from X.d i' j' -- Lean is unhappy here
| some i', none    := 0
| none,    some j' := 0
| none,    none    := 0
end

end homological_complex

Johan Commelin (Mar 11 2022 at 12:59):

Context: I'm trying to build the functor from -indexed complexes to -indexed complexes. But there are actually two useful complex_shape on both and . So there are 4 potentially useful embeddings. Hence my attempt at abstracting the definition of this functor.
At the same time, I was trying to write this in such a way that we will have useful defeqs when specializing to one of these four ℕ → ℤ embeddings.

Johan Commelin (Mar 11 2022 at 13:00):

But Lean doesn't want to reduce embed.X in the match statement in embed.d. Is Lean throwing away too much information?

Eric Rodriguez (Mar 11 2022 at 13:04):

this is truly terrible, but compiles:

def embed.d : Π (i j : ι₂), embed.X e X i  embed.X e X j := λ i j,
begin
dsimp only [embed.X],
exact match e.r i, e.r j with
| some i', some j' := show X.X i'  X.X j', from X.d i' j'
| some i', none    := 0
| none,    some j' := 0
| none,    none    := 0
end
end

I think the "real" answer is "don't do this" somehow

Johan Commelin (Mar 11 2022 at 13:07):

But.....

Johan Commelin (Mar 11 2022 at 13:08):

That would mean giving up on really nice defeqs, presumably.

Johan Commelin (Mar 11 2022 at 13:08):

But apparently those defeqs aren't working anyways.

Johan Commelin (Mar 11 2022 at 13:08):

Anyway, thank you so much for that dsimp trick!

Eric Rodriguez (Mar 11 2022 at 13:19):

I feel like cases on constructor applications aren't really supported that well. People like Mario, etc, will likely know the "correct" way to do this

Johan Commelin (Mar 11 2022 at 13:43):

Here is a "do it this way instead" approach:

def embed.X : option ι₁  C
| (some i) := X.X i
| none     := 0

def embed.d : Π (i j : option ι₁), embed.X X i  embed.X X j
| (some i) (some j) := X.d i j
| (some i) none     := 0
| none     j        := 0

lemma embed.shape :  (i j : option ι₁)
  (h :  (i' j' : ι₁), i = some i'  j = some j'  ¬ c₁.rel i' j'),
  embed.d X i j = 0
| (some i) (some j) h := X.shape _ _ $ h i j rfl rfl
| (some i) none     h := rfl
| none     j        h := rfl

lemma embed.d_comp_d :  (i j k : option ι₁), embed.d X i j  embed.d X j k = 0
| (some i) (some j) (some k) := X.d_comp_d _ _ _
| (some i) (some j) none     := limits.comp_zero
| (some i) none     k        := limits.comp_zero
| none     j        k        := limits.zero_comp

def embed : homological_complex C c₂ :=
{ X := embed.X X  e.r,
  d := λ i j, embed.d X (e.r i) (e.r j),
  shape' := λ i j hij, embed.shape X _ _ begin
    simp only [e.eq_some],
    rintro i' j' rfl rfl h',
    exact hij (e.c h')
  end,
  d_comp_d' := λ i j k hij hjk, embed.d_comp_d X _ _ _ }

Johan Commelin (Mar 11 2022 at 14:24):

That worked really well! See https://github.com/leanprover-community/lean-liquid/blob/master/src/for_mathlib/complex_extend.lean for the result.


Last updated: Dec 20 2023 at 11:08 UTC