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 Prop
s
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.
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.
Instances For
Records below proofs and motive proofs available. This is extended using NewDecl
s while visiting
and rewriting match expressions.
Map from proofs
h : ∀ x y z, ...
to pairs ofbelowIndName
and a proof ofh' : ∀ x y z, belowIndName ... (h x y z)
. These are used to find match rewriting candidates.Map from proofs
h : ∀ x y z, ...
to pairs ofn
and a proof ofh' : ∀ 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.
Instances For
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.