Tutorial Tests

👍 001_basicDef

Basic definition

def basicDef : Type :=
  Prop

✋ 002_badDef

Mismatched types

def badDef : Prop :=
  Type

👍 003_arrowType

Arrow type (function type)

def arrowType : Type :=
  Prop → Prop

👍 004_dependentType

Dependent type (forall)

def dependentType : Prop :=
  ∀ (p : Prop), p

👍 005_constType

Lambda expression

def constType : Type → Type → Type :=
  fun (x y : Type) => x

👍 006_betaReduction

Lambda reduction

Includes: constType

def betaReduction : constType Prop (Prop → Prop) :=
  ∀ (p : Prop), p

👍 007_betaReduction2

Lambda reduction under binder

Includes: constType

def betaReduction2 : (p : Prop) → constType Prop (Prop → Prop) :=
  fun (p : Prop) => p

👍 008_forallSortWhnf

The binding domain of a forall may need to be reduce before it is a sort

def id.{u} : {α : Sort u} → (a : α) → α :=
  fun {α : Sort u} (a : α) => a
def forallSortWhnf : Prop :=
  ∀ (p : @id.{2} Type Prop) (a : p), p

✋ 009_forallSortBad

The binding domain of a forall has to be a sort

Includes: id

def forallSortBad : Prop :=
  (x : @id.{2} Type Prop) → (x : x) → (a : x) → x

✋ 010_nonTypeType

The type of a declaration has to be a type, not some other expression

Includes: constType

def nonTypeType : constType :=
  Prop

✋ 011_nonTypeAxiom

This applies to axioms as well, which are easy to overlook because they have no value to check the type against. Letting one through is not merely untidy: an axiom whose type is an arbitrary term inhabits whatever that term is later found definitionally equal to, and the eta and proof irrelevance rules are happy to equate a term like this with a great many things.

Includes: constType

axiom nonTypeAxiom : constType

✋ 012_nonPropThm

The type of a theorem has to be a proposition

theorem nonPropThm : Prop :=
  ∀ (x : Prop), x

👍 013_levelComp1

Some level computation

def levelComp1 : Type :=
  Sort (imax 1 0)

👍 014_levelComp2

Some level computation

def levelComp2 : Type 1 :=
  Sort (imax 0 1)

👍 015_levelComp3

Some level computation

def levelComp3 : Type 2 :=
  Type (max 1 0)

👍 016_levelParams

Level parameters

def levelParamF.{u} : Sort u → Sort u → Sort u :=
  fun (α β : Sort u) => α
def levelParams : levelParamF.{1} Prop (Prop → Prop) :=
  ∀ (p : Prop), p

✋ 017_tut06_bad01

Duplicate universe parameters

def tut06_bad01.{u, u} : Type :=
  Prop

👍 018_levelComp4

Some level computation

def levelComp4.{u} : Type :=
  Prop

👍 019_levelComp5

Some level computation

def levelComp5.{u} : Type u :=
  Sort u

👍 020_imax1

Type inference for forall using imax

def imax1 : (p : Prop) → Prop :=
  fun (p : Prop) => ∀ (a : Type), p

👍 021_imax2

Type inference for forall using imax

def imax2 : (α : Type) → Type 1 :=
  fun (α : Type) => Type → α

👍 022_levelMaxComm

Level equality: max is commutative (max u v ≈ max v u).

def levelMaxComm.{u, v} : Type (max v u) :=
  Sort (max u v)

👍 023_levelMaxAssoc

Level equality: max is associative (max (max u v) w ≈ max u (max v w)).

def levelMaxAssoc.{u, v, w} : Type (max u v w) :=
  Sort (max (max u v) w)

👍 024_levelMaxIdem

Level equality: max is idempotent (max u u ≈ u).

def levelMaxIdem.{u} : Type u :=
  Sort (max u u)

👍 025_levelMaxAbsorb

Level equality: max absorption (max u (max u v) ≈ max u v).

def levelMaxAbsorb.{u, v} : Type (max u v) :=
  Sort (max u u v)

👍 026_inferVar

Type inference of local variables

def inferVar : ∀ (f : Prop) (g : f), f :=
  fun (f : Prop) (g : f) => g

👍 027_defEqLambda

Definitional equality between lambdas

def defEqLambda :
    ∀ (f : (Prop → Prop) → Prop) (g : ∀ (a : Prop → Prop), f a),
      f fun (p : Prop) => p → p :=
  fun (f : (Prop → Prop) → Prop) (g : ∀ (a : Prop → Prop), f a) =>
    g fun (p : Prop) => p → p

👍 028_peano1

Peano arithmetic: 2 = 2

def PN.{u_1} : Sort (imax (u_1 + 1) u_1) :=
  (α : Sort u_1) → (α → α) → α → α
def PN.succ.{u_1} : PN.{u_1} → PN.{u_1} :=
  fun (n : PN.{u_1}) (α : Sort u_1) (s : α → α) (z : α) => s (n α s z)
def PN.zero.{u_1} : PN.{u_1} :=
  fun (α : Sort u_1) (s : α → α) (z : α) => z
def PN.lit0.{u_1} : PN.{u_1} :=
  PN.zero.{u_1}
def PN.lit1.{u_1} : PN.{u_1} :=
  PN.succ.{u_1} PN.lit0.{u_1}
def PN.lit2.{u_1} : PN.{u_1} :=
  PN.succ.{u_1} PN.lit1.{u_1}
theorem peano1.{u} :
    ∀ (t : PN.{u} → Prop) (v : ∀ (n : PN.{u}), t n), t PN.lit2.{u} :=
  fun (t : PN.{u} → Prop) (v : ∀ (n : PN.{u}), t n) => v PN.lit2.{u}

👍 029_peano2

Peano arithmetic: 1 + 1 = 2

Includes: PN, PN.succ, PN.zero, PN.lit0, PN.lit1, PN.lit2

def PN.add.{u_1} : PN.{u_1} → PN.{u_1} → PN.{u_1} :=
  fun (n m : PN.{u_1}) (α : Sort u_1) (s : α → α) (z : α) => n α s (m α s z)
theorem peano2.{u} :
    ∀ (t : PN.{u} → Prop) (v : ∀ (n : PN.{u}), t n), t PN.lit2.{u} :=
  fun (t : PN.{u} → Prop) (v : ∀ (n : PN.{u}), t n) =>
    v (PN.add.{u} PN.lit1.{u} PN.lit1.{u})

👍 030_peano3

Peano arithmetic: 2 * 2 = 4

Includes: PN, PN.succ, PN.zero, PN.lit0, PN.lit1, PN.lit2

def PN.lit3.{u_1} : PN.{u_1} :=
  PN.succ.{u_1} PN.lit2.{u_1}
def PN.lit4.{u_1} : PN.{u_1} :=
  PN.succ.{u_1} PN.lit3.{u_1}
def PN.mul.{u_1} : PN.{u_1} → PN.{u_1} → PN.{u_1} :=
  fun (n m : PN.{u_1}) (α : Sort u_1) (s : α → α) (z : α) => n α (m α s) z
theorem peano3.{u} :
    ∀ (t : PN.{u} → Prop) (v : ∀ (n : PN.{u}), t n), t PN.lit4.{u} :=
  fun (t : PN.{u} → Prop) (v : ∀ (n : PN.{u}), t n) =>
    v (PN.mul.{u} PN.lit2.{u} PN.lit2.{u})

👍 031_letType

Type checking a non-dependent let

def letType : Type :=
  let x : Type := Prop;
  x

👍 032_letTypeDep

Type checking a dependent let

axiom aDepProp : Type → Prop
axiom mkADepProp : ∀ (t : Type), aDepProp t
def letTypeDep : aDepProp Prop :=
  let x : Type := Prop;
  mkADepProp x

👍 033_letRed

Reducing a let

axiom aProp : Prop
def letRed :
    let x : Type := Prop;
    x :=
  aProp

👍 034_empty

A simple empty inductive type

inductive Empty : Type
def empty : Type :=
  Empty

👍 035_boolType

A simple enumeration inductive type

inductive Bool : Type
constructor Bool.false : Bool
constructor Bool.true : Bool
def boolType : Type :=
  Bool

👍 036_twoBool

A simple product type

Includes: Bool, Bool.false, Bool.true

inductive TwoBool : Type
constructor TwoBool.mk : (b1 b2 : Bool) → TwoBool
def twoBool : Type :=
  TwoBool

👍 037_andType

A parametrized product type (no level parameters)

inductive And (a : Prop) (b : Prop) : Prop
constructor And.intro : ∀ {a b : Prop} (left : a) (right : b), And a b
def andType : (a b : Prop) → Prop :=
  And

👍 038_prodType

A parametrized product type (with level parameters)

inductive Prod.{u, v} (α : Type u) (β : Type v) : Type (max u v)
constructor Prod.mk.{u, v} :
    {α : Type u} → {β : Type v} → (fst : α) → (snd : β) → Prod.{u, v} α β
def prodType : Type → Type → Type :=
  Prod.{0, 0}

👍 039_pprodType

A parametrized product type (with more general level parameters)

inductive PProd.{u, v} (α : Sort u) (β : Sort v) : Sort (max (max 1 u) v)
constructor PProd.mk.{u, v} :
    {α : Sort u} → {β : Sort v} → (fst : α) → (snd : β) → PProd.{u, v} α β
def pprodType : Type → Type → Type :=
  PProd.{1, 1}

👍 040_pUnitType

Level-polymorphic unit type

inductive PUnit.{u} : Sort u
constructor PUnit.unit.{u} : PUnit.{u}
def pUnitType : Type :=
  PUnit.{1}

👍 041_eqType

Equality, as an important indexed non-recursive data type

inductive Eq.{u_1} {α : Sort u_1} (a._@._internal._hyg.0 : α) : α → Prop
constructor Eq.refl.{u_1} : ∀ {α : Sort u_1} (a : α), @Eq.{u_1} α a a
def eqType.{u_1} : {α : Sort u_1} → α → α → Prop :=
  @Eq.{u_1}

👍 042_natDef

A recursive inductive data type

inductive N : Type
constructor N.zero : N
constructor N.succ : N → N
def natDef : Type :=
  N

👍 043_rbTreeDef

A recursive indexed data type

Includes: N, N.zero, N.succ

inductive Color : Type
constructor Color.r : Color
constructor Color.b : Color
inductive RBTree.{u} (α : Type u) : Color → N → Type u
constructor RBTree.leaf.{u} : {α : Type u} → RBTree.{u} α Color.b N.zero
constructor RBTree.red.{u} :
    {α : Type u} →
      {n : N} →
        RBTree.{u} α Color.b n →
          α → RBTree.{u} α Color.b n → RBTree.{u} α Color.r n
constructor RBTree.black.{u} :
    {α : Type u} →
      {c1 c2 : Color} →
        {n : N} →
          RBTree.{u} α c1 n →
            α → RBTree.{u} α c2 n → RBTree.{u} α Color.b (N.succ n)
def rbTreeDef.{u} : (α : Type u) → Color → N → Type u :=
  RBTree.{u}

✋ 044_inductBadNonSort

An inductive type with a non-sort type

Includes: constType

inductive inductBadNonSort : constType

✋ 045_inductBadNonSort2

Another inductive type with a non-sort type

axiom aType : Type
inductive inductBadNonSort2 : aType

✋ 046_inductLevelParam

An inductive with duplicate level params

inductive inductLevelParam.{u, u} : Type

✋ 047_inductTooFewParams

An inductive with too few parameters in the type

inductive inductTooFewParams (x : Prop) : Prop

✋ 048_inductWrongCtorParams

An inductive with a constructor with wrong parameters

Includes: aProp

inductive inductWrongCtorParams (x : Prop) : Type
constructor inductWrongCtorParams.mk : (x : Type) → inductWrongCtorParams aProp

✋ 049_inductWrongCtorResParams

An inductive with a constructor with wrong parameters in result (they are swapped)

inductive inductWrongCtorResParams (x : Prop) (y : Prop) : Type
constructor inductWrongCtorResParams.mk :
    (x y : Prop) → inductWrongCtorResParams y x

✋ 050_inductWrongCtorResLevel

An inductive with a constructor with wrong level parameters in result (they are swapped)

inductive inductWrongCtorResLevel.{u1, u2} (x : Prop) (y : Prop) : Type
constructor inductWrongCtorResLevel.mk.{u1, u2} :
    (x y : Prop) → inductWrongCtorResLevel.{u2, u1} x y

✋ 051_inductInIndex

A constructor with an unexpected occurrence of the type in index position of a return type.

Includes: aProp

inductive inductInIndex : (x : Prop) → Prop
constructor inductInIndex.mk : inductInIndex (inductInIndex aProp)

✋ 052_indNeg

The classic example of an inductive with negative recursive occurrence

inductive indNeg : Type
constructor indNeg.mk : (x : (x : indNeg) → indNeg) → indNeg

👍 053_reduceCtorParam.mk

When checking inductives, we expect the kernel to reduce the types of constructor arguments.

Includes: id, constType

inductive reduceCtorParam (a._@._internal._hyg.0 : Type) : Type
constructor reduceCtorParam.mk :
    (α : @id.{3} (Type 1) Type) →
      (x : constType (reduceCtorParam α) (reduceCtorParam α)) →
        reduceCtorParam α

✋ 054_reduceCtorType.mk

When checking inductives, we expect the kernel to not reduce the type of the constructor itself; that should be all manifest foralls

Includes: id

inductive reduceCtorType : Type
constructor reduceCtorType.mk : @id.{2} Type reduceCtorType

✋ 055_indNegReducible

When checking inductives, we expect the kernel to not reduce the type of the constructor parameters further than head normal form. Recursive occurrences nested inside the head normal form are considered negative occurrences, even if they could be reduced to disappear.

Includes: constType, aType

inductive indNegReducible : Type
constructor indNegReducible.mk :
    (x : (x : constType aType indNegReducible) → indNegReducible) →
      indNegReducible

👍 056_predWithTypeField

An inductive proposition can have constructors with fields of arbitrary level.

inductive PredWithTypeField : Prop
constructor PredWithTypeField.mk : ∀ (α : Type), PredWithTypeField
def predWithTypeField : Prop :=
  PredWithTypeField

👍 057_typeWithTypeField

An inductive type can have fields of level up to that of the inductive.

inductive TypeWithTypeField : Type 1
constructor TypeWithTypeField.mk : (α : Type) → TypeWithTypeField
def typeWithTypeField : Type 1 :=
  TypeWithTypeField

👍 058_typeWithTypeFieldPoly

An inductive type can have fields of level up to that of the inductive (polymorphic variant).

inductive TypeWithTypeFieldPoly.{u} : Type (u + 1)
constructor TypeWithTypeFieldPoly.mk.{u} :
    (α : Type u) → TypeWithTypeFieldPoly.{u}
def typeWithTypeFieldPoly.{u} : Type (u + 1) :=
  TypeWithTypeFieldPoly.{u}