match

Stream: general

[Johan Commelin]

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]

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]

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]

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]

But.....

[Johan Commelin]

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

[Johan Commelin]

But apparently those defeqs aren't working anyways.

[Johan Commelin]

Anyway, thank you so much for that dsimp trick!

[Eric Rodriguez]

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]

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]

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