Tutorial Test Cases

These are the test cases from the Lean Kernel Arena tutorial. Each test is a small Lean 4 environment exported via lean4export. Good tests (👍) should be accepted by a correct kernel implementation; bad tests (✋) should be rejected. Later tests build on declarations from earlier ones; shared declarations are listed under Includes.

👍 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_nonPropThm

The type of a theorem has to be a proposition

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

👍 012_levelComp1

Some level computation

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

👍 013_levelComp2

Some level computation

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

👍 014_levelComp3

Some level computation

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

👍 015_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

✋ 016_tut06_bad01

Duplicate universe parameters

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

👍 017_levelComp4

Some level computation

def levelComp4.{u} : Type :=
  Prop

👍 018_levelComp5

Some level computation

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

👍 019_imax1

Type inference for forall using imax

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

👍 020_imax2

Type inference for forall using imax

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

👍 021_inferVar

Type inference of local variables

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

👍 022_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

👍 023_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}

👍 024_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})

👍 025_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})

👍 026_letType

Type checking a non-dependent let

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

👍 027_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

👍 028_letRed

Reducing a let

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

👍 029_empty

A simple empty inductive type

inductive Empty : Type
def empty : Type :=
  Empty

👍 030_boolType

A simple enumeration inductive type

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

👍 031_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

👍 032_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

👍 033_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}

👍 034_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}

👍 035_pUnitType

Level-polymorphic unit type

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

👍 036_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}

👍 037_natDef

A recursive inductive data type

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

👍 038_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}

✋ 039_inductBadNonSort

An inductive type with a non-sort type

Includes: constType

inductive inductBadNonSort : constType

✋ 040_inductBadNonSort2

Another inductive type with a non-sort type

axiom aType : Type
inductive inductBadNonSort2 : aType

✋ 041_inductLevelParam

An inductive with duplicate level params

inductive inductLevelParam.{u, u} : Type

✋ 042_inductTooFewParams

An inductive with too few parameters in the type

inductive inductTooFewParams (x : Prop) : Prop

✋ 043_inductWrongCtorParams

An inductive with a constructor with wrong parameters

Includes: aProp

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

✋ 044_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

✋ 045_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

✋ 046_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)

✋ 047_indNeg

The classic example of an inductive with negative recursive occurrence

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

👍 048_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 α

✋ 049_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

✋ 050_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

👍 051_predWithTypeField

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

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

👍 052_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

👍 053_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}

✋ 054_typeWithTooHighTypeField.mk

An inductive type can have fields of from higher universes.

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

👍 055_emptyRec

Asserting the type of the generated recursor

Includes: Empty

def emptyRec.{u} : (motive : (t : Empty) → Sort u) → (t : Empty) → motive t :=
  Empty.rec.{u}

👍 056_boolRec

Asserting the type of the generated recursor

Includes: Bool, Bool.false, Bool.true

def boolRec.{u} :
    {motive : (t : Bool) → Sort u} →
      (false : motive Bool.false) →
        (true : motive Bool.true) → (t : Bool) → motive t :=
  fun {motive : (t : Bool) → Sort u} (false : motive Bool.false)
      (true : motive Bool.true) (t : Bool) =>
    @Bool.rec.{u} motive false true t

👍 057_twoBoolRec

Asserting the type of the generated recursor

Includes: Bool, Bool.false, Bool.true, TwoBool, TwoBool.mk

def twoBoolRec.{u} :
    {motive : (t : TwoBool) → Sort u} →
      (mk : (b1 b2 : Bool) → motive (TwoBool.mk b1 b2)) →
        (t : TwoBool) → motive t :=
  fun {motive : (t : TwoBool) → Sort u}
      (mk : (b1 b2 : Bool) → motive (TwoBool.mk b1 b2)) (t : TwoBool) =>
    @TwoBool.rec.{u} motive mk t

👍 058_andRec

Asserting the type of the generated recursor

Includes: And, And.intro

def andRec.{u} :
    {a b : Prop} →
      {motive : (t : And a b) → Sort u} →
        (intro :
            (left : a) → (right : b) → motive (@And.intro a b left right)) →
          (t : And a b) → motive t :=
  @And.rec.{u}

👍 059_prodRec

Asserting the type of the generated recursor

Includes: Prod, Prod.mk

def prodRec.{u, v, w} :
    (α : Type u) →
      (β : Type v) →
        {motive : Prod.{u, v} α β → Sort u} →
          (mk : (fst : α) → (snd : β) → motive (@Prod.mk.{u, v} α β fst snd)) →
            (t : Prod.{u, v} α β) → motive t :=
  @Prod.rec.{u, u, v}

👍 060_pprodRec

Asserting the type of the generated recursor

Includes: PProd, PProd.mk

def pprodRec.{u, v, w} :
    (α : Sort u) →
      (β : Sort v) →
        {motive : PProd.{u, v} α β → Sort u} →
          (mk : (fst : α) → (snd : β) → motive (@PProd.mk.{u, v} α β fst snd)) →
            (t : PProd.{u, v} α β) → motive t :=
  @PProd.rec.{u, u, v}

👍 061_punitRec

Asserting the type of the generated recursor

Includes: PUnit, PUnit.unit

def punitRec.{u, w} :
    {motive : PUnit.{u} → Sort w} →
      (unit : motive PUnit.unit.{u}) → (t : PUnit.{u}) → motive t :=
  @PUnit.rec.{w, u}

👍 062_eqRec

Asserting the type of the generated recursor

Includes: Eq, Eq.refl

def eqRec.{u, u_1} :
    {α : Sort u_1} →
      {a : α} →
        {motive : (a_1 : α) → (t : @Eq.{u_1} α a a_1) → Sort u} →
          (refl : motive a (@Eq.refl.{u_1} α a)) →
            {a_1 : α} → (t : @Eq.{u_1} α a a_1) → motive a_1 t :=
  @Eq.rec.{u, u_1}

👍 063_nRec

Asserting the type of the generated recursor

Includes: N, N.zero, N.succ

def nRec.{u} :
    {motive : (t : N) → Sort u} →
      (zero : motive N.zero) →
        (succ : (a : N) → motive a → motive (N.succ a)) → (t : N) → motive t :=
  @N.rec.{u}

👍 064_rbTreeRef

Asserting the type of the generated recursor

Includes: Color, Color.r, Color.b, N, N.zero, N.succ, RBTree, RBTree.leaf, RBTree.red, RBTree.black

def rbTreeRef.{u} :
    {α : Type u} →
      {motive : (a : Color) → (a_1 : N) → RBTree.{u} α a a_1 → Sort u} →
        (leaf : motive Color.b N.zero (@RBTree.leaf.{u} α)) →
          (red :
              {n : N} →
                (a : RBTree.{u} α Color.b n) →
                  (a_1 : α) →
                    (a_2 : RBTree.{u} α Color.b n) →
                      motive Color.b n a →
                        motive Color.b n a_2 →
                          motive Color.r n (@RBTree.red.{u} α n a a_1 a_2)) →
            (black :
                {c1 c2 : Color} →
                  {n : N} →
                    (a : RBTree.{u} α c1 n) →
                      (a_1 : α) →
                        (a_2 : RBTree.{u} α c2 n) →
                          motive c1 n a →
                            motive c2 n a_2 →
                              motive Color.b (N.succ n)
                                (@RBTree.black.{u} α c1 c2 n a a_1 a_2)) →
              {a : Color} →
                {a_1 : N} → (t : RBTree.{u} α a a_1) → motive a a_1 t :=
  @RBTree.rec.{u, u}

👍 065_boolPropRec

Inductive predicates eliminate into Prop if they have more than one constructor.

inductive BoolProp : Prop
constructor BoolProp.a : BoolProp
constructor BoolProp.b : BoolProp
def boolPropRec :
    ∀ {motive : (t : BoolProp) → Prop} (a : motive BoolProp.a)
      (b : motive BoolProp.b) (t : BoolProp), motive t :=
  @BoolProp.rec

👍 066_existsRec

Inductive predicates eliminate into Prop if they have one constructors and it carries data.

inductive Exists.{u} {α : Sort u} (p : α → Prop) : Prop
constructor Exists.intro.{u} :
    ∀ {α : Sort u} {p : α → Prop} (w : α) (h : p w), @Exists.{u} α p
def existsRec.{u} :
    ∀ {α : Sort u} {p : α → Prop} {motive : (t : @Exists.{u} α p) → Prop}
      (intro : ∀ (w : α) (h : p w), motive (@Exists.intro.{u} α p w h))
      (t : @Exists.{u} α p), motive t :=
  @Exists.rec.{u}

👍 067_sortElimPropRec

Inductive predicates eliminate into Sort if they have one constructors and it carries data, but the data is known from the type, e.g. a parameter or an index

Includes: Bool, Bool.false, Bool.true

inductive SortElimProp (b : Bool) : Bool → Bool → Prop
constructor SortElimProp.mk : ∀ {b : Bool} (b1 b2 : Bool), SortElimProp b b2 b1
def sortElimPropRec.{u} :
    {b : Bool} →
      {motive : (a a_1 : Bool) → (t : SortElimProp b a a_1) → Sort u} →
        (mk : (b1 b2 : Bool) → motive b2 b1 (@SortElimProp.mk b b1 b2)) →
          {a a_1 : Bool} → (t : SortElimProp b a a_1) → motive a a_1 t :=
  @SortElimProp.rec.{u}

👍 068_sortElimProp2Rec

Inductive predicates eliminate into Sort if they have one constructors and it carries data, but the data is known from the type, e.g. a parameter or an index. However, it must occur directly in the result type, with no intervening reduction.

Includes: Bool, Bool.false, Bool.true, id

inductive SortElimProp2 (b : Bool) : Bool → Bool → Prop
constructor SortElimProp2.mk :
    ∀ {b : Bool} (b1 b2 : Bool), SortElimProp2 b b2 (@id.{1} Bool b1)
def sortElimProp2Rec :
    ∀ {b : Bool} {motive : (a a_1 : Bool) → (t : SortElimProp2 b a a_1) → Prop}
      (mk : ∀ (b1 b2 : Bool), motive b2 b1 (@SortElimProp2.mk b b1 b2))
      {a a_1 : Bool} (t : SortElimProp2 b a a_1), motive a a_1 t :=
  @SortElimProp2.rec

👍 069_boolRecEqns

Reduction behavior of Bool.rec

Includes: And, And.intro, Bool, Bool.false, Bool.true, Eq, Eq.refl

theorem boolRecEqns.{u} :
    And
      (∀ {motive : (t : Bool) → Sort u} (falseVal : motive Bool.false)
        (trueVal : motive Bool.true),
        @Eq.{u} (motive Bool.false)
          (@Bool.rec.{u} (fun (x : Bool) => motive x) falseVal trueVal
            Bool.false)
          falseVal)
      (∀ {motive : (t : Bool) → Sort u} (falseVal : motive Bool.false)
        (trueVal : motive Bool.true),
        @Eq.{u} (motive Bool.true)
          (@Bool.rec.{u} (fun (x : Bool) => motive x) falseVal trueVal
            Bool.true)
          trueVal) :=
  @And.intro
    (∀ {motive : (t : Bool) → Sort u} (falseVal : motive Bool.false)
      (trueVal : motive Bool.true),
      @Eq.{u} (motive Bool.false)
        (@Bool.rec.{u} (fun (x : Bool) => motive x) falseVal trueVal Bool.false)
        falseVal)
    (∀ {motive : (t : Bool) → Sort u} (falseVal : motive Bool.false)
      (trueVal : motive Bool.true),
      @Eq.{u} (motive Bool.true)
        (@Bool.rec.{u} (fun (x : Bool) => motive x) falseVal trueVal Bool.true)
        trueVal)
    (fun {motive : (t : Bool) → Sort u} (falseVal : motive Bool.false)
        (trueVal : motive Bool.true) =>
      @Eq.refl.{u} (motive Bool.false)
        (@Bool.rec.{u} (fun (x : Bool) => motive x) falseVal trueVal
          Bool.false))
    fun {motive : (t : Bool) → Sort u} (falseVal : motive Bool.false)
      (trueVal : motive Bool.true) =>
    @Eq.refl.{u} (motive Bool.true)
      (@Bool.rec.{u} (fun (x : Bool) => motive x) falseVal trueVal Bool.true)

👍 070_prodRecEqns

Reduction behavior of Prod.rec

Includes: Prod, Prod.mk, Eq, Eq.refl

theorem prodRecEqns.{u} :
    ∀ {α β : Type} {motive : Prod.{0, 0} α β → Sort u}
      (f : (a : α) → (b : β) → motive (@Prod.mk.{0, 0} α β a b)) (a : α)
      (b : β),
      @Eq.{u} (motive (@Prod.mk.{0, 0} α β a b))
        (@Prod.rec.{u, 0, 0} α β (fun (x : Prod.{0, 0} α β) => motive x) f
          (@Prod.mk.{0, 0} α β a b))
        (f a b) :=
  fun {α β : Type} {motive : Prod.{0, 0} α β → Sort u}
      (f : (a : α) → (b : β) → motive (@Prod.mk.{0, 0} α β a b)) (a : α)
      (b : β) =>
    @Eq.refl.{u} (motive (@Prod.mk.{0, 0} α β a b))
      (@Prod.rec.{u, 0, 0} α β (fun (x : Prod.{0, 0} α β) => motive x) f
        (@Prod.mk.{0, 0} α β a b))

👍 071_nRecReduction

A proof relying on the reduction behavior of N.rec

Includes: And, And.intro, N, N.zero, N.succ, Eq, Eq.refl, id

def N.add : N → N → N :=
  fun (t : N) =>
    @N.rec.{1} (fun (x : N) => N → N) (fun (m : N) => m)
      (fun (n : N) (ih : N → N) (m : N) => N.succ (ih m)) t
theorem nRecReduction :
    And (∀ (m : N), @Eq.{1} N (N.add N.zero m) m)
      (∀ (n m : N), @Eq.{1} N (N.add (N.succ n) m) (N.succ (N.add n m))) :=
  @id.{0}
    (And (∀ (m : N), @Eq.{1} N (N.add N.zero m) m)
      (∀ (n m : N), @Eq.{1} N (N.add (N.succ n) m) (N.succ (N.add n m))))
    (@And.intro
      (∀ (m : N),
        @Eq.{1} N
          (@N.rec.{1} (fun (x : N) => N → N) (fun (m : N) => m)
            (fun (n : N) (ih : N → N) (m : N) => N.succ (ih m)) N.zero m)
          m)
      (∀ (n m : N),
        @Eq.{1} N
          (@N.rec.{1} (fun (x : N) => N → N) (fun (m : N) => m)
            (fun (n : N) (ih : N → N) (m : N) => N.succ (ih m)) (N.succ n) m)
          (N.succ
            (@N.rec.{1} (fun (x : N) => N → N) (fun (m : N) => m)
              (fun (n : N) (ih : N → N) (m : N) => N.succ (ih m)) n m)))
      (fun (m : N) =>
        @Eq.refl.{1} N
          (@N.rec.{1} (fun (x : N) => N → N) (fun (m : N) => m)
            (fun (n : N) (ih : N → N) (m : N) => N.succ (ih m)) N.zero m))
      fun (n m : N) =>
      @Eq.refl.{1} N
        (@N.rec.{1} (fun (x : N) => N → N) (fun (m : N) => m)
          (fun (n : N) (ih : N → N) (m : N) => N.succ (ih m)) (N.succ n) m))

👍 072_listRecReduction

Reduction behavior of List.rec

Includes: And, And.intro, Eq, Eq.refl, id

inductive List.{u} (α : Type u) : Type u
constructor List.nil.{u} : {α : Type u} → List.{u} α
constructor List.cons.{u} :
    {α : Type u} → (head : α) → (tail : List.{u} α) → List.{u} α
def List.recOn.{u_1, u} :
    {α : Type u} →
      {motive : (t : List.{u} α) → Sort u_1} →
        (t : List.{u} α) →
          (nil : motive (@List.nil.{u} α)) →
            (cons :
                (head : α) →
                  (tail : List.{u} α) →
                    (tail_ih : motive tail) →
                      motive (@List.cons.{u} α head tail)) →
              motive t :=
  fun {α : Type u} {motive : (t : List.{u} α) → Sort u_1} (t : List.{u} α)
      (nil : motive (@List.nil.{u} α))
      (cons :
        (head : α) →
          (tail : List.{u} α) →
            (tail_ih : motive tail) → motive (@List.cons.{u} α head tail)) =>
    @List.rec.{u_1, u} α motive nil cons t
def myListApped : {α : Type} → (xs ys : List.{0} α) → List.{0} α :=
  fun {α : Type} (xs ys : List.{0} α) =>
    @List.recOn.{1, 0} α (fun (x : List.{0} α) => List.{0} α) xs ys
      fun (x : α) (xs ih : List.{0} α) => @List.cons.{0} α x ih
theorem listRecReduction :
    ∀ {α : Type} (xs ys : List.{0} α),
      And (@Eq.{1} (List.{0} α) (@myListApped α (@List.nil.{0} α) ys) ys)
        (∀ (x : α) (xs : List.{0} α),
          @Eq.{1} (List.{0} α) (@myListApped α (@List.cons.{0} α x xs) ys)
            (@List.cons.{0} α x (@myListApped α xs ys))) :=
  fun {α : Type} (xs ys : List.{0} α) =>
    @id.{0}
      (And (@Eq.{1} (List.{0} α) (@myListApped α (@List.nil.{0} α) ys) ys)
        (∀ (x : α) (xs : List.{0} α),
          @Eq.{1} (List.{0} α) (@myListApped α (@List.cons.{0} α x xs) ys)
            (@List.cons.{0} α x (@myListApped α xs ys))))
      (@And.intro
        (@Eq.{1} (List.{0} α)
          (@List.recOn.{1, 0} α (fun (x : List.{0} α) => List.{0} α)
            (@List.nil.{0} α) ys fun (x : α) (xs ih : List.{0} α) =>
            @List.cons.{0} α x ih)
          ys)
        (∀ (x : α) (xs : List.{0} α),
          @Eq.{1} (List.{0} α)
            (@List.recOn.{1, 0} α (fun (x : List.{0} α) => List.{0} α)
              (@List.cons.{0} α x xs) ys fun (x : α) (xs ih : List.{0} α) =>
              @List.cons.{0} α x ih)
            (@List.cons.{0} α x
              (@List.recOn.{1, 0} α (fun (x : List.{0} α) => List.{0} α) xs ys
                fun (x : α) (xs ih : List.{0} α) => @List.cons.{0} α x ih)))
        (@Eq.refl.{1} (List.{0} α)
          (@List.recOn.{1, 0} α (fun (x : List.{0} α) => List.{0} α)
            (@List.nil.{0} α) ys fun (x : α) (xs ih : List.{0} α) =>
            @List.cons.{0} α x ih))
        fun (x : α) (xs : List.{0} α) =>
        @Eq.refl.{1} (List.{0} α)
          (@List.recOn.{1, 0} α (fun (x : List.{0} α) => List.{0} α)
            (@List.cons.{0} α x xs) ys fun (x : α) (xs ih : List.{0} α) =>
            @List.cons.{0} α x ih))

👍 073_RBTree.id_spec

Reduction behavior of RBTree.rec

Includes: Color, Color.r, Color.b, N, N.zero, N.succ, RBTree, RBTree.leaf, RBTree.red, RBTree.black, Eq, Eq.refl, id

def RBTree.id :
    {α : Type} →
      {c : Color} → {n : N} → (t : RBTree.{0} α c n) → RBTree.{0} α c n :=
  fun {α : Type} {c : Color} {n : N} (t : RBTree.{0} α c n) =>
    @RBTree.rec.{1, 0} α
      (fun (x : Color) (x_1 : N) (x_2 : RBTree.{0} α x x_1) =>
        RBTree.{0} α x x_1)
      (@RBTree.leaf.{0} α)
      (fun {n : N} (_t1 : RBTree.{0} α Color.b n) (a : α)
          (_t2 ih1 ih2 : RBTree.{0} α Color.b n) =>
        @RBTree.red.{0} α n ih1 a ih2)
      (fun {c1 c2 : Color} {n : N} (_t1 : RBTree.{0} α c1 n) (a : α)
          (_t2 : RBTree.{0} α c2 n) (ih1 : RBTree.{0} α c1 n)
          (ih2 : RBTree.{0} α c2 n) =>
        @RBTree.black.{0} α c1 c2 n ih1 a ih2)
      c n t
theorem RBTree.id_spec :
    ∀ {α : Type} {c : Color} {n : N} (t : RBTree.{0} α c n),
      @Eq.{1} (RBTree.{0} α c n) (@RBTree.id α c n t) t :=
  fun {α : Type} {c : Color} {n : N} (t : RBTree.{0} α c n) =>
    @RBTree.rec.{0, 0} α
      (fun {c : Color} {n : N} (t : RBTree.{0} α c n) =>
        @Eq.{1} (RBTree.{0} α c n) (@RBTree.id α c n t) t)
      (@Eq.refl.{1} (RBTree.{0} α Color.b N.zero)
        (@RBTree.id α Color.b N.zero (@RBTree.leaf.{0} α)))
      (fun {n : N} (a : RBTree.{0} α Color.b n) (a_1 : α)
          (a_2 : RBTree.{0} α Color.b n)
          (a_ih : @Eq.{1} (RBTree.{0} α Color.b n) (@RBTree.id α Color.b n a) a)
          (a_ih_1 :
            @Eq.{1} (RBTree.{0} α Color.b n) (@RBTree.id α Color.b n a_2)
              a_2) =>
        @id.{0}
          (@Eq.{1} (RBTree.{0} α Color.r n)
            (@RBTree.id α Color.r n (@RBTree.red.{0} α n a a_1 a_2))
            (@RBTree.red.{0} α n a a_1 a_2))
          ((@fun {α : Type} {n : N} (a a_3 : RBTree.{0} α Color.b n)
                (e_a : @Eq.{1} (RBTree.{0} α Color.b n) a a_3) =>
              @Eq.rec.{0, 1} (RBTree.{0} α Color.b n) a
                (fun (a_4 : RBTree.{0} α Color.b n)
                    (e_a : @Eq.{1} (RBTree.{0} α Color.b n) a a_4) =>
                  ∀ (a_5 a_6 : α),
                    @Eq.{1} α a_5 a_6 →
                      ∀ (a_7 a_8 : RBTree.{0} α Color.b n),
                        @Eq.{1} (RBTree.{0} α Color.b n) a_7 a_8 →
                          @Eq.{1} (RBTree.{0} α Color.r n)
                            (@RBTree.red.{0} α n a a_5 a_7)
                            (@RBTree.red.{0} α n a_4 a_6 a_8))
                (fun (a_4 a_5 : α) (e_a : @Eq.{1} α a_4 a_5) =>
                  @Eq.rec.{0, 1} α a_4
                    (fun (a_6 : α) (e_a : @Eq.{1} α a_4 a_6) =>
                      ∀ (a_7 a_8 : RBTree.{0} α Color.b n),
                        @Eq.{1} (RBTree.{0} α Color.b n) a_7 a_8 →
                          @Eq.{1} (RBTree.{0} α Color.r n)
                            (@RBTree.red.{0} α n a a_4 a_7)
                            (@RBTree.red.{0} α n a a_6 a_8))
                    (fun (a_6 a_7 : RBTree.{0} α Color.b n)
                        (e_a : @Eq.{1} (RBTree.{0} α Color.b n) a_6 a_7) =>
                      @Eq.rec.{0, 1} (RBTree.{0} α Color.b n) a_6
                        (fun (a_8 : RBTree.{0} α Color.b n)
                            (e_a : @Eq.{1} (RBTree.{0} α Color.b n) a_6 a_8) =>
                          @Eq.{1} (RBTree.{0} α Color.r n)
                            (@RBTree.red.{0} α n a a_4 a_6)
                            (@RBTree.red.{0} α n a a_4 a_8))
                        (@Eq.refl.{1} (RBTree.{0} α Color.r n)
                          (@RBTree.red.{0} α n a a_4 a_6))
                        a_7 e_a)
                    a_5 e_a)
                a_3 e_a)
            α n
            (@RBTree.rec.{1, 0} α
              (fun (x : Color) (x_1 : N) (x_2 : RBTree.{0} α x x_1) =>
                RBTree.{0} α x x_1)
              (@RBTree.leaf.{0} α)
              (fun {n : N} (_t1 : RBTree.{0} α Color.b n) (a : α)
                  (_t2 ih1 ih2 : RBTree.{0} α Color.b n) =>
                @RBTree.red.{0} α n ih1 a ih2)
              (fun {c1 c2 : Color} {n : N} (_t1 : RBTree.{0} α c1 n) (a : α)
                  (_t2 : RBTree.{0} α c2 n) (ih1 : RBTree.{0} α c1 n)
                  (ih2 : RBTree.{0} α c2 n) =>
                @RBTree.black.{0} α c1 c2 n ih1 a ih2)
              Color.b n a)
            a a_ih a_1 a_1 (@Eq.refl.{1} α a_1)
            (@RBTree.rec.{1, 0} α
              (fun (x : Color) (x_1 : N) (x_2 : RBTree.{0} α x x_1) =>
                RBTree.{0} α x x_1)
              (@RBTree.leaf.{0} α)
              (fun {n : N} (_t1 : RBTree.{0} α Color.b n) (a : α)
                  (_t2 ih1 ih2 : RBTree.{0} α Color.b n) =>
                @RBTree.red.{0} α n ih1 a ih2)
              (fun {c1 c2 : Color} {n : N} (_t1 : RBTree.{0} α c1 n) (a : α)
                  (_t2 : RBTree.{0} α c2 n) (ih1 : RBTree.{0} α c1 n)
                  (ih2 : RBTree.{0} α c2 n) =>
                @RBTree.black.{0} α c1 c2 n ih1 a ih2)
              Color.b n a_2)
            a_2 a_ih_1))
      (fun {c1 c2 : Color} {n : N} (a : RBTree.{0} α c1 n) (a_1 : α)
          (a_2 : RBTree.{0} α c2 n)
          (a_ih : @Eq.{1} (RBTree.{0} α c1 n) (@RBTree.id α c1 n a) a)
          (a_ih_1 : @Eq.{1} (RBTree.{0} α c2 n) (@RBTree.id α c2 n a_2) a_2) =>
        @id.{0}
          (@Eq.{1} (RBTree.{0} α Color.b (N.succ n))
            (@RBTree.id α Color.b (N.succ n)
              (@RBTree.black.{0} α c1 c2 n a a_1 a_2))
            (@RBTree.black.{0} α c1 c2 n a a_1 a_2))
          ((@fun {α : Type} {c1 c2 : Color} {n : N} (a a_3 : RBTree.{0} α c1 n)
                (e_a : @Eq.{1} (RBTree.{0} α c1 n) a a_3) =>
              @Eq.rec.{0, 1} (RBTree.{0} α c1 n) a
                (fun (a_4 : RBTree.{0} α c1 n)
                    (e_a : @Eq.{1} (RBTree.{0} α c1 n) a a_4) =>
                  ∀ (a_5 a_6 : α),
                    @Eq.{1} α a_5 a_6 →
                      ∀ (a_7 a_8 : RBTree.{0} α c2 n),
                        @Eq.{1} (RBTree.{0} α c2 n) a_7 a_8 →
                          @Eq.{1} (RBTree.{0} α Color.b (N.succ n))
                            (@RBTree.black.{0} α c1 c2 n a a_5 a_7)
                            (@RBTree.black.{0} α c1 c2 n a_4 a_6 a_8))
                (fun (a_4 a_5 : α) (e_a : @Eq.{1} α a_4 a_5) =>
                  @Eq.rec.{0, 1} α a_4
                    (fun (a_6 : α) (e_a : @Eq.{1} α a_4 a_6) =>
                      ∀ (a_7 a_8 : RBTree.{0} α c2 n),
                        @Eq.{1} (RBTree.{0} α c2 n) a_7 a_8 →
                          @Eq.{1} (RBTree.{0} α Color.b (N.succ n))
                            (@RBTree.black.{0} α c1 c2 n a a_4 a_7)
                            (@RBTree.black.{0} α c1 c2 n a a_6 a_8))
                    (fun (a_6 a_7 : RBTree.{0} α c2 n)
                        (e_a : @Eq.{1} (RBTree.{0} α c2 n) a_6 a_7) =>
                      @Eq.rec.{0, 1} (RBTree.{0} α c2 n) a_6
                        (fun (a_8 : RBTree.{0} α c2 n)
                            (e_a : @Eq.{1} (RBTree.{0} α c2 n) a_6 a_8) =>
                          @Eq.{1} (RBTree.{0} α Color.b (N.succ n))
                            (@RBTree.black.{0} α c1 c2 n a a_4 a_6)
                            (@RBTree.black.{0} α c1 c2 n a a_4 a_8))
                        (@Eq.refl.{1} (RBTree.{0} α Color.b (N.succ n))
                          (@RBTree.black.{0} α c1 c2 n a a_4 a_6))
                        a_7 e_a)
                    a_5 e_a)
                a_3 e_a)
            α c1 c2 n
            (@RBTree.rec.{1, 0} α
              (fun (x : Color) (x_1 : N) (x_2 : RBTree.{0} α x x_1) =>
                RBTree.{0} α x x_1)
              (@RBTree.leaf.{0} α)
              (fun {n : N} (_t1 : RBTree.{0} α Color.b n) (a : α)
                  (_t2 ih1 ih2 : RBTree.{0} α Color.b n) =>
                @RBTree.red.{0} α n ih1 a ih2)
              (fun {c1 c2 : Color} {n : N} (_t1 : RBTree.{0} α c1 n) (a : α)
                  (_t2 : RBTree.{0} α c2 n) (ih1 : RBTree.{0} α c1 n)
                  (ih2 : RBTree.{0} α c2 n) =>
                @RBTree.black.{0} α c1 c2 n ih1 a ih2)
              c1 n a)
            a a_ih a_1 a_1 (@Eq.refl.{1} α a_1)
            (@RBTree.rec.{1, 0} α
              (fun (x : Color) (x_1 : N) (x_2 : RBTree.{0} α x x_1) =>
                RBTree.{0} α x x_1)
              (@RBTree.leaf.{0} α)
              (fun {n : N} (_t1 : RBTree.{0} α Color.b n) (a : α)
                  (_t2 ih1 ih2 : RBTree.{0} α Color.b n) =>
                @RBTree.red.{0} α n ih1 a ih2)
              (fun {c1 c2 : Color} {n : N} (_t1 : RBTree.{0} α c1 n) (a : α)
                  (_t2 : RBTree.{0} α c2 n) (ih1 : RBTree.{0} α c1 n)
                  (ih2 : RBTree.{0} α c2 n) =>
                @RBTree.black.{0} α c1 c2 n ih1 a ih2)
              c2 n a_2)
            a_2 a_ih_1))
      c n t

👍 074_And.right

Type-checking simple projection functions

Includes: And, And.intro

theorem And.left : ∀ {a b : Prop} (self : And a b), a :=
  fun (a b : Prop) (self : And a b) => self.1
theorem And.right : ∀ {a b : Prop} (self : And a b), b :=
  fun (a b : Prop) (self : And a b) => self.2

👍 075_Prod.snd

Type-checking projection functions with parameters

Includes: Prod, Prod.mk

def Prod.fst.{u, v} : {α : Type u} → {β : Type v} → (self : Prod.{u, v} α β) → α :=
  fun (α : Type u) (β : Type v) (self : Prod.{u, v} α β) => self.1
def Prod.snd.{u, v} : {α : Type u} → {β : Type v} → (self : Prod.{u, v} α β) → β :=
  fun (α : Type u) (β : Type v) (self : Prod.{u, v} α β) => self.2

👍 076_PProd.snd

Type-checking projection functions

Includes: PProd, PProd.mk

def PProd.fst.{u, v} :
    {α : Sort u} → {β : Sort v} → (self : PProd.{u, v} α β) → α :=
  fun (α : Sort u) (β : Sort v) (self : PProd.{u, v} α β) => self.1
def PProd.snd.{u, v} :
    {α : Sort u} → {β : Sort v} → (self : PProd.{u, v} α β) → β :=
  fun (α : Sort u) (β : Sort v) (self : PProd.{u, v} α β) => self.2

👍 077_PSigma.snd

Type-checking dependent projection functions

inductive PSigma.{u, v} {α : Sort u} (β : α → Sort v) : Sort (max (max 1 u) v)
constructor PSigma.mk.{u, v} :
    {α : Sort u} →
      {β : α → Sort v} → (fst : α) → (snd : β fst) → @PSigma.{u, v} α β
def PSigma.fst.{u, v} :
    {α : Sort u} → {β : α → Sort v} → (self : @PSigma.{u, v} α β) → α :=
  fun (α : Sort u) (β : α → Sort v) (self : @PSigma.{u, v} α β) => self.1
def PSigma.snd.{u, v} :
    {α : Sort u} →
      {β : α → Sort v} →
        (self : @PSigma.{u, v} α β) → β (@PSigma.fst.{u, v} α β self) :=
  fun (α : Sort u) (β : α → Sort v) (self : @PSigma.{u, v} α β) => self.2

✋ 078_projOutOfRange

Out of range projection

Includes: And, And.intro

def projOutOfRange : ∀ (x x_1 : Prop) (x_2 : And x x_1), x :=
  fun (x y : Prop) (z : And x y) => z.3

✋ 079_projNotStruct

Projection out something that is not a structure

Includes: N, N.zero, N.succ

def projNotStruct : N → N :=
  fun (x : N) => x.1

👍 080_projProp1

Projecting out of a proposition

The lean kernel allows projections out of propositions if they precede all dependent data fields.

Includes: PUnit, PUnit.unit, Eq, Eq.refl

inductive PropStructure.{u, v} : Prop
constructor PropStructure.mk.{u, v} :
    ∀ (aProof : PUnit.{u}) (someData : PUnit.{v}) (aSecondProof : PUnit.{u})
      (someMoreData : PUnit.{v})
      (aProofAboutData : @Eq.{v} PUnit.{v} someMoreData someMoreData)
      (aFinalProof : PUnit.{u}), PropStructure.{u, v}
def projProp1 : ∀ (x : PropStructure.{0, 1}), PUnit.{0} :=
  fun (x : PropStructure.{0, 1}) => x.1

✋ 081_projProp2

Projecting out of a proposition

The lean kernel disallows data projections out of propositional structures.

Includes: PUnit, PUnit.unit, Eq, Eq.refl, PropStructure, PropStructure.mk

def projProp2 : (x : PropStructure.{0, 1}) → PUnit.{1} :=
  fun (x : PropStructure.{0, 1}) => x.2

👍 082_projProp3

Projecting out of a proposition

The lean kernel allows projections out of propositions if they precede all dependent data fields. Non-dependent data fields are not relevant.

Includes: PUnit, PUnit.unit, Eq, Eq.refl, PropStructure, PropStructure.mk

def projProp3 : ∀ (x : PropStructure.{0, 1}), PUnit.{0} :=
  fun (x : PropStructure.{0, 1}) => x.3

✋ 083_projProp4

Projecting out of a proposition

The lean kernel disallows data projections out of propositional structures.

Includes: PUnit, PUnit.unit, Eq, Eq.refl, PropStructure, PropStructure.mk

def projProp4 : (x : PropStructure.{0, 1}) → PUnit.{1} :=
  fun (x : PropStructure.{0, 1}) => x.4

✋ 084_projProp5

Projecting out of a proposition

The lean kernel disallows proof projections out of propositional structures that depend on data.

Includes: PUnit, PUnit.unit, Eq, Eq.refl, PropStructure, PropStructure.mk

def projProp5 : ∀ (x : PropStructure.{0, 1}), @Eq.{1} PUnit.{1} x.4 x.4 :=
  fun (x : PropStructure.{0, 1}) => x.5

✋ 085_projProp6

Projecting out of a proposition.

The lean kernel rejects any projections out of a proposition that come after a dependent data field, even if that is not used by the present projection.

Includes: PUnit, PUnit.unit, Eq, Eq.refl, PropStructure, PropStructure.mk

def projProp6 : ∀ (x : PropStructure.{0, 1}), PUnit.{0} :=
  fun (x : PropStructure.{0, 1}) => x.6

👍 086_projDataIndexRec

The recursor for ProjDataIndex allows elimination into sort.

Includes: N, N.zero, N.succ

inductive True : Prop
constructor True.intro : True
inductive ProjDataIndex (a._@._internal._hyg.0 : N) : Prop
constructor ProjDataIndex.mk : ∀ (n : N) (p : True), ProjDataIndex n
def projDataIndexRec.{u_1} :
    {a : N} →
      {motive : (t : ProjDataIndex a) → Sort u_1} →
        (mk : (p : True) → motive (ProjDataIndex.mk a p)) →
          (t : ProjDataIndex a) → motive t :=
  @ProjDataIndex.rec.{u_1}

✋ 087_projIndexData

Projecting out data is not allowed, even if this data appears as an index and the recursor would allow it.

Includes: N, N.zero, N.succ, True, True.intro, ProjDataIndex, ProjDataIndex.mk

def projIndexData : (x : N) → (x : ProjDataIndex x) → N :=
  fun (x : N) (x_1 : ProjDataIndex x) => x_1.1

✋ 088_projIndexData2

Projecting out data is not allowed, even if this data appears as an index and the recursor would allow it.

This also forbids projecting out proofs that follow such fields.

Includes: N, N.zero, N.succ, True, True.intro, ProjDataIndex, ProjDataIndex.mk

def projIndexData2 : ∀ (x : N) (x : ProjDataIndex x), True :=
  fun (x : N) (x_1 : ProjDataIndex x) => x_1.2

👍 089_projRed

Projection reductions

Includes: Eq, Eq.refl, Bool, Bool.false, Bool.true, Prod, Prod.mk, Prod.snd

def rfl.{u} : ∀ {α : Sort u} {a : α}, @Eq.{u} α a a :=
  fun {α : Sort u} {a : α} => @Eq.refl.{u} α a
def projRed :
    @Eq.{1} Bool
      (@Prod.snd.{0, 0} Bool Bool
        (@Prod.mk.{0, 0} Bool Bool Bool.true Bool.false))
      Bool.false :=
  @rfl.{1} Bool
    (@Prod.snd.{0, 0} Bool Bool
      (@Prod.mk.{0, 0} Bool Bool Bool.true Bool.false))

👍 090_ruleK

Rule k for Eq: The recursor reduces even if the major argument is not a constructor, as long replacing the major argument with a constructor is type correct.

Includes: Eq, Eq.refl, Bool, Bool.false, Bool.true

theorem ruleK :
    ∀ (h : @Eq.{1} Bool Bool.true Bool.true) (a : Bool),
      @Eq.{1} Bool
        (@Eq.rec.{1, 1} Bool Bool.true
          (fun (x : Bool) (x_1 : @Eq.{1} Bool Bool.true x) => Bool) a Bool.true
          h)
        a :=
  fun (x : @Eq.{1} Bool Bool.true Bool.true) (a : Bool) => @Eq.refl.{1} Bool a

✋ 091_ruleKbad

Rule k for Eq should not fire if the types of the major argument do not match that of the constructor.

Includes: Eq, Eq.refl, Bool, Bool.false, Bool.true

theorem ruleKbad :
    ∀ (h : @Eq.{1} Bool Bool.true Bool.false) (a : Bool),
      @Eq.{1} Bool
        (@Eq.rec.{1, 1} Bool Bool.true
          (fun (x : Bool) (x_1 : @Eq.{1} Bool Bool.true x) => Bool) a Bool.false
          h)
        a :=
  fun (x : @Eq.{1} Bool Bool.true Bool.false) (a : Bool) => @Eq.refl.{1} Bool a

✋ 092_ruleKAcc

Rule k should not fire for Acc.

Includes: Bool, Bool.false, Bool.true, Eq, Eq.refl

inductive Acc.{u} {α : Sort u} (r : α → α → Prop) : α → Prop
constructor Acc.intro.{u} :
    ∀ {α : Sort u} {r : α → α → Prop} (x : α)
      (h : ∀ (y : α), r y x → @Acc.{u} α r y), @Acc.{u} α r x
theorem ruleKAcc.{u} :
    ∀ (α : Sort u) (p : α → α → Prop) (x : α) (h : @Acc.{u} α p x) (a : Bool),
      @Eq.{1} Bool
        (@Acc.rec.{1, u} α p (fun (x : α) (x_1 : @Acc.{u} α p x) => Bool)
          (fun (x : α) (x_1 : ∀ (y : α), p y x → @Acc.{u} α p y)
              (x_2 :
                (y : α) →
                  (a : p y x) →
                    (fun (x : α) (x_2 : @Acc.{u} α p x) => Bool) y (x_1 y a)) =>
            a)
          x h)
        a :=
  fun (α : Sort u) (p : α → α → Prop) (x : α) (h : @Acc.{u} α p x) (a : Bool) =>
    @Eq.refl.{1} Bool a

👍 093_aNatLit

Type checking Nat literals

inductive Nat : Type
constructor Nat.zero : Nat
constructor Nat.succ : (n : Nat) → Nat
def aNatLit : Nat :=
  failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

👍 094_natLitEq

Reducing Nat literals

Includes: Eq, Eq.refl, Nat, Nat.zero, Nat.succ

theorem natLitEq : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) :=
  failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

👍 095_proofIrrelevance

Proof irrelevance

Includes: Eq, Eq.refl, rfl

def proofIrrelevance : ∀ (p : Prop) (h1 h2 : p), @Eq.{0} p h1 h2 :=
  fun (x : Prop) (x_1 x_2 : x) => @rfl.{0} x x_1

👍 096_unitEta1

Unit eta

Includes: PUnit, PUnit.unit, Eq, Eq.refl, rfl

def Unit : Type :=
  PUnit.{1}
def unitEta1 : ∀ (x y : Unit), @Eq.{1} Unit x y :=
  fun (x x_1 : Unit) => @rfl.{1} Unit x

👍 097_unitEta2

Unit eta

Includes: PUnit, PUnit.unit, Eq, Eq.refl, rfl

def unitEta2.{u} : ∀ (x y : PUnit.{u}), @Eq.{u} PUnit.{u} x y :=
  fun (x x_1 : PUnit.{u}) => @rfl.{u} PUnit.{u} x

👍 098_unitEta3

Unit eta

Includes: PUnit, PUnit.unit, Eq, Eq.refl, rfl

def unitEta3 : ∀ (x y : PUnit.{0}), @Eq.{0} PUnit.{0} x y :=
  fun (x x_1 : PUnit.{0}) => @rfl.{0} PUnit.{0} x

👍 099_structEta

Structure eta

Includes: Prod, Prod.mk, And, And.intro, Eq, Eq.refl, Prod.fst, Prod.snd, rfl

def structEta.{u} :
    ∀ (α β : Type u) (x : Prod.{u, u} α β),
      And
        (@Eq.{u + 1} (Prod.{u, u} α β) x
          (@Prod.mk.{u, u} α β (@Prod.fst.{u, u} α β x)
            (@Prod.snd.{u, u} α β x)))
        (@Eq.{u + 1} (Prod.{u, u} α β)
          (@Prod.mk.{u, u} α β (@Prod.fst.{u, u} α β x)
            (@Prod.snd.{u, u} α β x))
          x) :=
  fun (x x_1 : Type u) (x_2 : Prod.{u, u} x x_1) =>
    @And.intro
      (@Eq.{u + 1} (Prod.{u, u} x x_1) x_2
        (@Prod.mk.{u, u} x x_1 (@Prod.fst.{u, u} x x_1 x_2)
          (@Prod.snd.{u, u} x x_1 x_2)))
      (@Eq.{u + 1} (Prod.{u, u} x x_1)
        (@Prod.mk.{u, u} x x_1 (@Prod.fst.{u, u} x x_1 x_2)
          (@Prod.snd.{u, u} x x_1 x_2))
        x_2)
      (@rfl.{u + 1} (Prod.{u, u} x x_1) x_2)
      (@rfl.{u + 1} (Prod.{u, u} x x_1)
        (@Prod.mk.{u, u} x x_1 (@Prod.fst.{u, u} x x_1 x_2)
          (@Prod.snd.{u, u} x x_1 x_2)))

👍 100_funEta

Function eta for non-dependent functions.

Includes: Eq, Eq.refl, rfl

theorem funEta :
    ∀ (α β : Type) (f : α → β), @Eq.{1} ((x : α) → β) (fun (x : α) => f x) f :=
  fun (x x_1 : Type) (f : x → x_1) =>
    @rfl.{1} ((x : x) → x_1) fun (x : x) => f x

👍 101_funEtaDep

Function eta for dependent functions (pi types).

Includes: Eq, Eq.refl, rfl

theorem funEtaDep :
    ∀ (α : Type) (β : α → Type) (f : (a : α) → β a),
      @Eq.{1} ((a : α) → β a) (fun (a : α) => f a) f :=
  fun (x : Type) (x_1 : x → Type) (f : (a : x) → x_1 a) =>
    @rfl.{1} ((a : x) → x_1 a) fun (a : x) => f a

✋ 102_funEtaBad

Eta should not identify functions with different bodies.

Includes: Eq, Eq.refl

theorem funEtaBad :
    ∀ (α β : Type) (g : α → α) (f : α → β),
      @Eq.{1} ((x : α) → β) (fun (x : α) => f (g x)) f :=
  fun (x x_1 : Type) (x_2 : x → x) (f : x → x_1) =>
    @Eq.refl.{1} ((x : x) → x_1) f

✋ 103_etaRuleK

Corner case for function eta: Does a defeq between a partially applied recursor with rule k and a free variable trigger eta expansion?

Taking the official kernel as the specification, the answer is no. See https://github.com/leanprover/lean4/issues/12520 for a discussion.

Includes: Eq, Eq.refl, Bool, Bool.false, Bool.true

def etaRuleK :
    ∀ (a : @Eq.{1} Bool Bool.true Bool.true → Bool),
      @Eq.{1} (@Eq.{1} Bool Bool.true Bool.true → Bool)
        (@Eq.rec.{1, 1} Bool Bool.true
          (fun (x : Bool) (x_1 : @Eq.{1} Bool Bool.true x) => Bool)
          (a (@Eq.refl.{1} Bool Bool.true)) Bool.true)
        a :=
  fun (a : @Eq.{1} Bool Bool.true Bool.true → Bool) =>
    @Eq.refl.{1} (@Eq.{1} Bool Bool.true Bool.true → Bool) a

✋ 104_etaCtor

Corner case for function eta: Does a defeq between a partially applied constructor trigger eta expansion?

Taking the official kernel as the specification, the answer is no. See https://github.com/leanprover/lean4/issues/12520 for a discussion.

Includes: True, True.intro, Bool, Bool.false, Bool.true, Eq, Eq.refl

inductive T : Type
constructor T.mk : (val : Bool) → (proof : True) → T
def T.val : (self : T) → Bool :=
  fun (self : T) => self.1
def etaCtor :
    ∀ (x : (proof : True) → T),
      @Eq.{1} ((proof : True) → T) (T.mk (T.val (x True.intro))) x :=
  fun (x : (proof : True) → T) => @Eq.refl.{1} ((proof : True) → T) x

✋ 105_reflOccLeft

Rejection: recursive occurrence on the left of an arrow, behind further arrows inside a constructor argument.

The constructor argument is a function type Nat → (I → Nat).

Includes: Nat, Nat.zero, Nat.succ

inductive reflOccLeft : Type
constructor reflOccLeft.mk :
    (x : (x : Nat) → (x : reflOccLeft) → Nat) → reflOccLeft

✋ 106_reflOccInIndex

Rejection: recursive occurrence in index position, behind a further arrow.

We build an indexed inductive I : Type → Type with a constructor argument Nat → I (I α), so the recursive occurrence appears as an index argument.

Includes: Nat, Nat.zero, Nat.succ

inductive reflOccInIndex : (α : Type) → Type
constructor reflOccInIndex.mk :
    (α : Type) →
      (x : (x : Nat) → reflOccInIndex (reflOccInIndex x)) → reflOccInIndex α

👍 107_reduceCtorParamRefl.mk

When checking inductives, we expect the kernel to reduce the types of constructor arguments in all positive positions.

Includes: id, constType

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

👍 108_reduceCtorParamRefl2.mk

When checking inductives, we expect the kernel to reduce the types of constructor arguments in all positive positions.

Includes: id, constType

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

👍 109_rTreeRec

Asserting the type of the generated recursor.

Includes: Bool, Bool.false, Bool.true

inductive RTree : Type
constructor RTree.leaf : RTree
constructor RTree.node : (children : Bool → RTree) → RTree
def rTreeRec.{u_1} :
    {motive : (t : RTree) → Sort u_1} →
      (leaf : motive RTree.leaf) →
        (node :
            (children : Bool → RTree) →
              (children_ih : (a : Bool) → motive (children a)) →
                motive (RTree.node children)) →
          (t : RTree) → motive t :=
  @RTree.rec.{u_1}

👍 110_rtreeRecReduction

Reduction behavior of RTree.rec on RTree.mk.

Includes: Bool, Bool.false, Bool.true, RTree, RTree.leaf, RTree.node, Eq, Eq.refl, rfl

def RTree.left : (t : RTree) → RTree :=
  fun (t : RTree) =>
    @RTree.rec.{1} (fun (x : RTree) => RTree) RTree.leaf
      (fun (children : Bool → RTree)
          (_ih : (a : Bool) → (fun (x : RTree) => RTree) (children a)) =>
        children Bool.true)
      t
theorem rtreeRecReduction :
    ∀ (t1 t2 : RTree),
      @Eq.{1} RTree
        (RTree.left
          (RTree.node fun (t : Bool) =>
            @Bool.rec.{1} (fun (x : Bool) => RTree) t2 t1 t))
        t1 :=
  fun (x x_1 : RTree) =>
    @rfl.{1} RTree
      (RTree.left
        (RTree.node fun (t : Bool) =>
          @Bool.rec.{1} (fun (x : Bool) => RTree) x_1 x t))

👍 111_accRecType

Asserting the type of Acc.rec.

Includes: Acc, Acc.intro

def accRecType.{u_1, u_2} :
    {α : Sort u_1} →
      {r : α → α → Prop} →
        {motive : (a : α) → (t : @Acc.{u_1} α r a) → Sort u_2} →
          (intro :
              (x : α) →
                (h : ∀ (y : α), r y x → @Acc.{u_1} α r y) →
                  (h_ih : (y : α) → (a : r y x) → motive y (h y a)) →
                    motive x (@Acc.intro.{u_1} α r x h)) →
            {a : α} → (t : @Acc.{u_1} α r a) → motive a t :=
  @Acc.rec.{u_2, u_1}

👍 112_accRecReduction

Acc.rec reduces on Acc.intro.

Includes: Acc, Acc.intro, Bool, Bool.false, Bool.true, Eq, Eq.refl

theorem accRecReduction :
    ∀ {α : Type} (r : α → α → Prop) (a : α)
      (h : ∀ (b : α), r b a → @Acc.{1} α r b) (p : Bool),
      @Eq.{1} Bool
        (@Acc.rec.{1, 1} α r (fun (x : α) (x_1 : @Acc.{1} α r x) => Bool)
          (fun (x : α) (x_1 : ∀ (y : α), r y x → @Acc.{1} α r y)
              (x_2 :
                (y : α) →
                  (a : r y x) →
                    (fun (x : α) (x_2 : @Acc.{1} α r x) => Bool) y (x_1 y a)) =>
            p)
          a (@Acc.intro.{1} α r a h))
        p :=
  fun {α : Type} (r : α → α → Prop) (a : α)
      (h : ∀ (b : α), r b a → @Acc.{1} α r b) (p : Bool) =>
    @Eq.refl.{1} Bool
      (@Acc.rec.{1, 1} α r (fun (x : α) (x_1 : @Acc.{1} α r x) => Bool)
        (fun (x : α) (x_1 : ∀ (y : α), r y x → @Acc.{1} α r y)
            (x_2 :
              (y : α) →
                (a : r y x) →
                  (fun (x : α) (x_2 : @Acc.{1} α r x) => Bool) y (x_1 y a)) =>
          p)
        a (@Acc.intro.{1} α r a h))

✋ 113_accRecNoEta

Acc.rec does not have structure eta.

Includes: Acc, Acc.intro, Bool, Bool.false, Bool.true, Eq, Eq.refl

theorem accRecNoEta :
    ∀ {α : Type} (r : α → α → Prop) (a : α) (h : @Acc.{1} α r a) (p : Bool),
      @Eq.{1} Bool
        (@Acc.rec.{1, 1} α r (fun (x : α) (x_1 : @Acc.{1} α r x) => Bool)
          (fun (x : α) (x_1 : ∀ (y : α), r y x → @Acc.{1} α r y)
              (x_2 :
                (y : α) →
                  (a : r y x) →
                    (fun (x : α) (x_2 : @Acc.{1} α r x) => Bool) y (x_1 y a)) =>
            p)
          a h)
        p :=
  fun (α : Type) (r : α → α → Prop) (a : α) (h : @Acc.{1} α r a) (p : Bool) =>
    @Eq.refl.{1} Bool p

👍 114_quotMkType

Asserting the type of Quot.mk.

Includes: Eq, Eq.refl

quot Quot.{u} : {α : Sort u} → (r : α → α → Prop) → Sort u
quot Quot.mk.{u} : {α : Sort u} → (r : α → α → Prop) → (a : α) → @Quot.{u} α r
quot Quot.lift.{u, v} :
    {α : Sort u} →
      {r : α → α → Prop} →
        {β : Sort v} →
          (f : (a : α) → β) →
            (a : ∀ (a b : α) (a_1 : r a b), @Eq.{v} β (f a) (f b)) →
              (a : @Quot.{u} α r) → β
quot Quot.ind.{u} :
    ∀ {α : Sort u} {r : α → α → Prop} {β : (a : @Quot.{u} α r) → Prop}
      (mk : ∀ (a : α), β (@Quot.mk.{u} α r a)) (q : @Quot.{u} α r), β q
def quotMkType.{u} : {α : Sort u} → (r : α → α → Prop) → (a : α) → @Quot.{u} α r :=
  @Quot.mk.{u}

👍 115_quotIndType

Asserting the type of Quot.ind.

Includes: Eq, Eq.refl, Quot, Quot.mk, Quot.lift, Quot.ind

def quotIndType.{u} :
    ∀ {α : Sort u} {r : α → α → Prop} {β : (a : @Quot.{u} α r) → Prop}
      (mk : ∀ (a : α), β (@Quot.mk.{u} α r a)) (q : @Quot.{u} α r), β q :=
  @Quot.ind.{u}

👍 116_quotLiftType

Asserting the type of Quot.lift.

Includes: Eq, Eq.refl, Quot, Quot.mk, Quot.lift, Quot.ind

def quotLiftType.{u, v} :
    {α : Sort u} →
      {r : α → α → Prop} →
        {β : Sort v} →
          (f : (a : α) → β) →
            (a : ∀ (a b : α) (a_1 : r a b), @Eq.{v} β (f a) (f b)) →
              (a : @Quot.{u} α r) → β :=
  @Quot.lift.{u, v}

👍 117_quotSoundType

Asserting the type of Quot.sound.

Includes: Eq, Eq.refl, Quot, Quot.mk, Quot.lift, Quot.ind

axiom Quot.sound.{u} :
    ∀ {α : Sort u} {r : α → α → Prop} {a b : α},
      r a b → @Eq.{u} (@Quot.{u} α r) (@Quot.mk.{u} α r a) (@Quot.mk.{u} α r b)
def quotSoundType.{u} :
    ∀ {α : Sort u} {r : α → α → Prop} {a b : α},
      r a b → @Eq.{u} (@Quot.{u} α r) (@Quot.mk.{u} α r a) (@Quot.mk.{u} α r b) :=
  @Quot.sound.{u}

👍 118_quotLiftReduction

Reduction behavior of Quot.lift on Quot.mk.

Includes: Eq, Eq.refl, Quot, Quot.mk, Quot.lift, Quot.ind

theorem quotLiftReduction.{u, v} :
    ∀ {α : Sort u} {r : α → α → Prop} {β : Sort v} (f : (a : α) → β)
      (h : ∀ (a b : α) (a_1 : r a b), @Eq.{v} β (f a) (f b)) (a : α),
      @Eq.{v} β (@Quot.lift.{u, v} α r β f h (@Quot.mk.{u} α r a)) (f a) :=
  fun {α : Sort u} {r : α → α → Prop} {β : Sort v} (f : (a : α) → β)
      (h : ∀ (a b : α) (a_1 : r a b), @Eq.{v} β (f a) (f b)) (a : α) =>
    @Eq.refl.{v} β (@Quot.lift.{u, v} α r β f h (@Quot.mk.{u} α r a))

👍 119_quotIndReduction

Reduction behavior of Quot.ind on Quot.mk.

Includes: Eq, Eq.refl, Quot, Quot.mk, Quot.lift, Quot.ind

theorem quotIndReduction.{u} :
    ∀ {α : Sort u} (r : α → α → Prop) {β : (a : @Quot.{u} α r) → Prop}
      (mk : ∀ (a : α), β (@Quot.mk.{u} α r a)) (a : α),
      @Eq.{0} (β (@Quot.mk.{u} α r a))
        (@Quot.ind.{u} α r β mk (@Quot.mk.{u} α r a)) (mk a) :=
  fun {α : Sort u} (r : α → α → Prop) {β : (a : @Quot.{u} α r) → Prop}
      (mk : ∀ (a : α), β (@Quot.mk.{u} α r a)) (a : α) =>
    @Eq.refl.{0} (β (@Quot.mk.{u} α r a))
      (@Quot.ind.{u} α r β mk (@Quot.mk.{u} α r a))

✋ 120_dup_defs

Two definitions with the same name

Includes: dup_defs

def dup_defs : Type :=
  Prop

✋ 121_dup_ind_def

A definition and a constructor with the same name

Includes: dup_ind_def

inductive dup_ind_def : Type
constructor dup_ind_def.mk : dup_ind_def

✋ 122_dup_ctor_def

A definition and a constructor with the same name

Includes: dup_ctor_def.mk

constructor dup_ctor_def.mk : dup_ctor_def
inductive dup_ctor_def : Type

✋ 123_dup_rec_def

A definition and a recursor with the same name

inductive dup_rec_def : Type
constructor dup_rec_def.mk : dup_rec_def

✋ 124_dup_rec_def2

A definition with the name of a recursor, and the recursor named differently. This would pass simple checks for duplicate definitions in the parser, but should still be rejected by the checker.

def dup_rec_def2.rec : Type :=
  Prop
inductive dup_rec_def2 : Type
constructor dup_rec_def2.mk : dup_rec_def2

✋ 125_dup_ctor_rec

A constructor and a recursor with the same name

inductive dup_ctor_rec : Type

✋ 126_DupConCon

An inductive with two constructors with the same name

Includes: dup_ind_con_con.mk

inductive DupConCon : Type
constructor dup_ind_con_con.mk : DupConCon