What tactics to use when goal contains term can be unify?

Stream: new members

[Alissa Tung]

Consider the case

def what_typ : ℤ -> Type
  | .ofNat   _ => ℤ × ℤ
  | .negSucc _ => ℕ × ℤ

def my_go (n : ℤ) : what_typ (n + 1) -> what_typ n := by exact match n with
  | .ofNat   n => by
      dsimp
      sorry
  | .negSucc n => sorry

before the sorry:

n✝: ℤ
n: ℕ
⊢ what_typ (↑n + 1) → what_typ ↑n

where the goal can be transform to show ℤ × ℤ -> ℤ × ℤ .

Partial show can also be used like show ℤ × ℤ -> _ to ⊢ what_typ (↑n + 1) → what_typ ↑n.

But some cases partial show does not work, and the goal is too complex.

Is there a way to do this task more idiomatically?

[Kyle Miller]

You could do dsimp [what_type] to unfold the definition

[Alissa Tung]

[Quoting…]

Yes. But some more complicated situations the definition will be unfold to match (ofNat x) + 1 with …, which still not reduce to the ofNat branch. I thought there should have some mechanics to push the match operand into constructor form by definitional equality, and reduce to the branch it should be.

[Alissa Tung]

A more concrete goal I am facing is

⊢ CategoryTheory.CategoryStruct.comp
    (match ↑a✝ + 1 with
    | Int.ofNat a =>
      { toAddHom := { toFun := fun x => 4 * x, map_add' := (_ : ∀ (x y : ZMod 8), 4 * (x + y) = 4 * x + 4 * y) },
        map_smul' := (_ : ∀ (r : ℤ) (x : ZMod 8), 4 * r • x = r • (4 * x)) }
    | Int.negSucc n => 0)
    { toAddHom := { toFun := fun x => 4 * x, map_add' := (_ : ∀ (x y : ZMod 8), 4 * (x + y) = 4 * x + 4 * y) },
      map_smul' := (_ : ∀ (r : ℤ) (x : ZMod 8), 4 * r • x = r • (4 * x)) } =
  0

[Kyle Miller]

It could be that you need simp [what_type] instead, since it might not be a definitional equality, but that adds Eq.recs into your term.

Another tactic you can use is split, which is for case splitting on match and if statements that appear in the goal. But again this might give you some gross terms if that matters to you.

[Alissa Tung]

Oh thx, that helps a lot. But I am still confusing at my code, which is actually

import Mathlib.Tactic

import Mathlib.Algebra.Ring.Basic
import Mathlib.Algebra.Module.Basic
import Mathlib.Algebra.Category.ModuleCat.Basic
import Mathlib.Algebra.Homology.HomologicalComplex


def z_mod_8_c : ChainComplex (ModuleCat ℤ) ℤ := by
  refine ChainComplex.of ?X ?d ?d_comp_d'
  · exact fun n => match n with
      | .ofNat   _ => ModuleCat.mk $ ZMod 8
      | .negSucc _ => ModuleCat.of ℤ PUnit
  · exact fun n => match n with
      | .ofNat   _ => by
          show ModuleCat.mk (ZMod 8) ⟶ ModuleCat.mk (ZMod 8)
          refine LinearMap.mk ?_ ?_
          · constructor; swap
            · intro x
              exact 4 * x
            intro x y
            ring
          dsimp
          intro r x
          ring_nf
          exact smul_mul_assoc r x 4
      | .negSucc n => 0
  intro n
  exact match n with
    | .ofNat   n => by
        dsimp
        sorry

    | .negSucc _ => sorry

in the sorry after dsimp, which can not use those methods since there is no named function

[Alissa Tung]

Seems that this works

    | .ofNat   n => by
        dsimp
        show CategoryTheory.CategoryStruct.comp
                (match ((↑n + 1) : ℤ) with
                | Int.ofNat a => _
                | Int.negSucc n => 0)
                _ =
              0
        show CategoryTheory.CategoryStruct.comp
                (match ((Nat.succ n) : ℤ) with
                | Int.ofNat a => _
                | Int.negSucc n => 0)
                _ =
              0
        simp