The below and brecOn constructions for inductive predicates

This module defines the below and brecOn constructions for inductive predicates. While the brecOn construction for inductive predicates is structurally indentical to the one for regular types apart from only eliminating to propositions, the below construction is changed since it is unlike for types not possible to eliminate proofs of inductive predicates to Props containing nested proofs. Instead, each below declaration is defined as an inductive type with one constructor per constructor of the original inductive, containing additional motive proofs and nested below proofs.

Additionally, this module defines the function mkBelowMatcher which can be used to rewrite match expressions to expose these motive proofs and nested below proofs.

def Lean.Meta.IndPredBelow.mkBelow (indName : Name) : MetaM Unit

Generates the auxiliary lemmas below and brecOn for a recursive inductive predicate.

Equations

• One or more equations did not get rendered due to their size.

structure Lean.Meta.IndPredBelow.RecursionContext : Type

Records below proofs and motive proofs available. This is extended using NewDecls while visiting and rewriting match expressions.

• belows : FVarIdMap (Name × Expr)

  Map from proofs h : ∀ x y z, ... to pairs of belowIndName and a proof of h' : ∀ x y z, belowIndName ... (h x y z). These are used to find match rewriting candidates.

• motives : FVarIdMap (Nat × Expr)

  Map from proofs h : ∀ x y z, ... to pairs of n and a proof of h' : ∀ x y z, <nth motive> ... (h' x y z) (nth motive corresponds to the order of motives in the recursor). These are used to eliminate recursive calls.

def Lean.Meta.IndPredBelow.mkBelowMatcher (matcherApp : MatcherApp) (belowParams : Array Expr) (nrealParams : Nat) (ctx : RecursionContext) (transformAlt : RecursionContext → Expr → MetaM Expr) : MetaM (Option (Expr × MetaM Unit))

This function adds an additional below discriminant to a matcher application and transforms each alternative with the provided transformAlt function. The provided recursion context is used for finding below proofs that correspond to discriminants and is extended with new proofs when calling transformAlt. belowParams should contain parameters and motives for below applications where the first nrealParams are parameters and the remaining are motives.

Equations

• One or more equations did not get rendered due to their size.