Type mismatch error

Stream: new members

[VayusElytra]

Hello, I'm having a small issue with making type mismatches that really do not feel like type mismatches.

abbrev PersistenceModule (C K : Type*) [PartialOrder C] [DivisionRing K]
  := (C ⥤ (ModuleCat K))

def ZeroModule (C K : Type*) [PartialOrder C] [DivisionRing K] : PersistenceModule C K where
  obj := fun (x : C) ↦ PUnit --type mismatch
  map := fun (U V : C) (f : ULift (PLift (U ≤ V))) ↦ fun (x : PUnit) ↦ PUnit.unit

This code defines a structure of "persistence module" for a partial order C and a field K, which is the category of functors from C to the category of modules over K. This structure has a 0 object, which is obtained by sending every element in C to the trivial K module; this is the ZeroModule def.

However Lean throws an error, saying that PUnit does not have type ModuleCat K. This is really weird to me because PUnit is a K-module; this is established in this file for instance.

Even replacing PUnit by some variable E : ModuleCat K, Lean still finds a type mismatch.
image.png

What is going on here?

[Kevin Buzzard]

Can you please edit your question to make a it a #mwe ? Your question might depend on what you have imported, for example.

[Ryan Kennelly]

Hello,

I've been doing theorem proving for a bit (in Agda), but I'm new to lean, and am having some trouble with the type checking. Specifically I'm trying to define Strong Normalization for Simply Typed Lambda Calculus, and I'm having some trouble with pattern matching. Below is my code with the problematic part in the substvar function commented.

--- Type
inductive Ty : Type where
  | bool : Ty
  | func : Ty → Ty → Ty

 -- Term
inductive Tm : List Ty → Ty → Type where
  | tr : Tm l Ty.bool
  | fl : Tm l Ty.bool
  | var : List.Mem ty l → Tm l ty
  | lam : Tm (e :: l) ty → Tm l (Ty.func e ty)
  | app : Tm l (Ty.func s t) → Tm l s → Tm l t

-- Substitution on context
inductive Subst : List Ty → List Ty → Type where
  | zero : Tm l s → Subst (s :: l) l
  | suc : Subst l l' → Subst (s :: l) (s :: l')

-- Substitute variable
def substvar : Subst l l' → List.Mem t l → Tm l' t
| Subst.zero t', List.Mem.head a => t'  --- This line has  the error:
/- type mismatch
  Subst.zero t'
has type
  Subst (?m.2143 :: ?m.2142) ?m.2142 : Type
but is expected to have type
  Subst l l' : Type -/
| Subst.zero t', List.Mem.tail _ m => Tm.var m
| Subst.suc s', List.Mem.head _ => Tm.var (List.Mem.head _)
| Subst.suc s', List.Mem.tail _ m => weaken (substvar s' m)

-- substitute
def subst : Subst l l' → Tm l t → Tm l' t
  | _, Tm.tr => Tm.tr
  | _, Tm.fl => Tm.fl
  | s, (Tm.var m) => substvar s m
  | s, (Tm.lam t) => Tm.lam (subst (Subst.suc s) t)
  | s, (Tm.app a b) => Tm.app (subst s a) (subst s b)

-- step function
inductive Step : Tm l t → Tm l t → Type where
  | lam : Step t t' → Step (Tm.lam t) (Tm.lam t')
  | app1 : Step f f' → Step (Tm.app f t) (Tm.app f' t)
  | app2 : Step t t' → Step (Tm.app f t) (Tm.app f t')
  | βred : Step (Tm.app (Tm.lam t) s) (subst (Subst.zero s) t)

-- strong normalization
inductive SN : Tm l t → Type where
  | sn : (∀ tm, Step tm tm' → SN tm') → SN tm

It would be really helpful to know what is causing this 'type mismatch', and any pointers on how to avoid this.
Thanks for any help.

[Mario Carneiro]

you need to include l and l' in the pattern match, although they can just be _, _, in each branch

[Kyle Miller]

def substvar : {l l' : List Ty} → Subst l l' → List.Mem t l → Tm l' t
| _, _, Subst.zero t', List.Mem.head _ => t'
| _, _, Subst.zero t', List.Mem.tail _ m => Tm.var m
| _, _, Subst.suc s', List.Mem.head _ => Tm.var (List.Mem.head _)
| _, _, Subst.suc s', List.Mem.tail _ m => weaken (substvar s' m)

/-
tactic 'cases' failed, nested error:
tactic 'induction' failed, recursor 'List.Mem.casesOn' can only eliminate into Prop
-/

[Kyle Miller]

Though there's a limitation that you can't do pattern matching on List.Mem, since it's a proposition.

[Ryan Kennelly]

Oh, that makes sense. I was wondering why List.Mem was so hard to work with. Thanks for the help!