max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

refactor: port below and brecOn construction to Lean (#4517)

Browse source 
This ports the `.below` and `.brecOn` constructions to lean.

I kept them in the same file, as they were in the C code, because they
are
highly coupled and the constructions are very analogous.

For validation I developed this in a separate repository at
https://github.com/nomeata/lean-constructions/tree/fad715e
and checked that all declarations found in Lean and Mathlib are
equivalent, up to

    def canon (e : Expr) : CoreM Expr := do
      Core.transform (← Core.betaReduce e) (pre := fun
        | .const n ls  => return .done (.const n (ls.map (·.normalize)))
        | .sort l => return .done (.sort l.normalize)
        | _ => return .continue)

It was not feasible to make them completely equal, because the kernel's
type inference code seem to optimize level expressions a bit less
aggressively, and beta-reduces less in inference.

The private helper functions about `PProd` can later move into their own
file, used by these constructions as well as the structural recursion
module.
This commit is contained in:
Joachim Breitner 2024-06-26 13:10:39 +02:00 • committed by GitHub
parent 62b6e58789
commit ea22ef4485
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
7 changed files with 395 additions and 454 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

50
src/Lean/Meta/Constructions.lean
View file

@ -9,14 +9,13 @@ import Lean.AddDecl
import Lean.Meta.AppBuilder
import Lean.Meta.CompletionName
import Lean.Meta.Constructions.RecOn
import Lean.Meta.Constructions.BRecOn
namespace Lean
@[extern "lean_mk_cases_on"] opaque mkCasesOnImp (env : Environment) (declName : @& Name) : Except KernelException Declaration
@[extern "lean_mk_no_confusion_type"] opaque mkNoConfusionTypeCoreImp (env : Environment) (declName : @& Name) : Except KernelException Declaration
@[extern "lean_mk_no_confusion"] opaque mkNoConfusionCoreImp (env : Environment) (declName : @& Name) : Except KernelException Declaration
@[extern "lean_mk_below"] opaque mkBelowImp (env : Environment) (declName : @& Name) (ibelow : Bool) : Except KernelException Declaration
@[extern "lean_mk_brec_on"] opaque mkBRecOnImp (env : Environment) (declName : @& Name) (ind : Bool) : Except KernelException Declaration
open Meta
@ -28,52 +27,6 @@ def mkCasesOn (declName : Name) : MetaM Unit := do
modifyEnv fun env => markAuxRecursor env name
modifyEnv fun env => addProtected env name
private def mkBelowOrIBelow (declName : Name) (ibelow : Bool) : MetaM Unit := do
let .inductInfo indVal ← getConstInfo declName | return
unless indVal.isRec do return
if ← isPropFormerType indVal.type then return
let decl ← ofExceptKernelException (mkBelowImp (← getEnv) declName ibelow)
let name := decl.definitionVal!.name
addDecl decl
setReducibleAttribute name
modifyEnv fun env => addToCompletionBlackList env name
modifyEnv fun env => addProtected env name
def mkBelow (declName : Name) : MetaM Unit := mkBelowOrIBelow declName true
def mkIBelow (declName : Name) : MetaM Unit := mkBelowOrIBelow declName false
private def mkBRecOrBInductionOn (declName : Name) (ind : Bool) : MetaM Unit := do
let .inductInfo indVal ← getConstInfo declName | return
unless indVal.isRec do return
if ← isPropFormerType indVal.type then return
let .recInfo recInfo ← getConstInfo (mkRecName declName) | return
unless recInfo.numMotives = indVal.all.length do
/-
The mutual declaration containing `declName` contains nested inductive datatypes.
We don't support this kind of declaration here yet. We probably never will :)
To support it, we will need to generate an auxiliary `below` for each nested inductive
type since their default `below` is not good here. For example, at
```
inductive Term
| var : String -> Term
| app : String -> List Term -> Term
```
The `List.below` is not useful since it will not allow us to recurse over the nested terms.
We need to generate another one using the auxiliary recursor `Term.rec_1` for `List Term`.
-/
return
let decl ← ofExceptKernelException (mkBRecOnImp (← getEnv) declName ind)
let name := decl.definitionVal!.name
addDecl decl
setReducibleAttribute name
modifyEnv fun env => markAuxRecursor env name
modifyEnv fun env => addProtected env name
def mkBRecOn (declName : Name) : MetaM Unit := mkBRecOrBInductionOn declName false
def mkBInductionOn (declName : Name) : MetaM Unit := mkBRecOrBInductionOn declName true
def mkNoConfusionCore (declName : Name) : MetaM Unit := do
-- Do not do anything unless can_elim_to_type. TODO: Extract to util
let .inductInfo indVal ← getConstInfo declName | return
@ -103,7 +56,6 @@ def mkNoConfusionEnum (enumName : Name) : MetaM Unit := do
-- `noConfusionEnum` was not defined yet, so we use `mkNoConfusionCore`
mkNoConfusionCore enumName
where
mkToCtorIdx : MetaM Unit := do
let ConstantInfo.inductInfo info ← getConstInfo enumName | unreachable!
let us := info.levelParams.map mkLevelParam

393
src/Lean/Meta/Constructions/BRecOn.lean Normal file
View file

@ -0,0 +1,393 @@
/-
Copyright (c) 2024 Lean FRO. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Leonardo de Moura, Joachim Breitner
-/
prelude
import Lean.Meta.InferType
import Lean.AuxRecursor
import Lean.AddDecl
import Lean.Meta.CompletionName
namespace Lean
open Meta
section PProd
/--!
Helpers to construct types and values of `PProd` and project out of them, set up to use `And`
instead of `PProd` if the universes allow. Maybe be extracted into a Utils module when useful
elsewhere.
-/
private def mkPUnit : Level → Expr
| .zero => .const ``True []
| lvl => .const ``PUnit [lvl]
private def mkPProd (e1 e2 : Expr) : MetaM Expr := do
let lvl1 ← getLevel e1
let lvl2 ← getLevel e2
if lvl1 matches .zero && lvl2 matches .zero then
return mkApp2 (.const `And []) e1 e2
else
return mkApp2 (.const ``PProd [lvl1, lvl2]) e1 e2
private def mkNProd (lvl : Level) (es : Array Expr) : MetaM Expr :=
es.foldrM (init := mkPUnit lvl) mkPProd
private def mkPUnitMk : Level → Expr
| .zero => .const ``True.intro []
| lvl => .const ``PUnit.unit [lvl]
private def mkPProdMk (e1 e2 : Expr) : MetaM Expr := do
let t1 ← inferType e1
let t2 ← inferType e2
let lvl1 ← getLevel t1
let lvl2 ← getLevel t2
if lvl1 matches .zero && lvl2 matches .zero then
return mkApp4 (.const ``And.intro []) t1 t2 e1 e2
else
return mkApp4 (.const ``PProd.mk [lvl1, lvl2]) t1 t2 e1 e2
private def mkNProdMk (lvl : Level) (es : Array Expr) : MetaM Expr :=
es.foldrM (init := mkPUnitMk lvl) mkPProdMk
/-- `PProd.fst` or `And.left` (as projections) -/
private def mkPProdFst (e : Expr) : MetaM Expr := do
let t ← whnf (← inferType e)
match_expr t with
| PProd _ _ => return .proj ``PProd 0 e
| And _ _ => return .proj ``And 0 e
| _ => throwError "Cannot project .1 out of{indentExpr e}\nof type{indentExpr t}"
/-- `PProd.snd` or `And.right` (as projections) -/
private def mkPProdSnd (e : Expr) : MetaM Expr := do
let t ← whnf (← inferType e)
match_expr t with
| PProd _ _ => return .proj ``PProd 1 e
| And _ _ => return .proj ``And 1 e
| _ => throwError "Cannot project .2 out of{indentExpr e}\nof type{indentExpr t}"
end PProd
/--
If `minorType` is the type of a minor premies of a recursor, such as
```
(cons : (head : α) → (tail : List α) → (tail_hs : motive tail) → motive (head :: tail))
```
of `List.rec`, constructs the corresponding argument to `List.rec` in the construction
of `.below` definition; in this case
```
fun head tail tail_ih =>
PProd (PProd (motive tail) tail_ih) PUnit
```
of type
```
α → List α → Sort (max 1 u_1) → Sort (max 1 u_1)
```
The parameter `typeFormers` are the `motive`s.
-/
private def buildBelowMinorPremise (rlvl : Level) (typeFormers : Array Expr) (minorType : Expr) : MetaM Expr :=
forallTelescope minorType fun minor_args _ => do go #[] minor_args.toList
where
ibelow := rlvl matches .zero
go (prods : Array Expr) : List Expr → MetaM Expr
| [] => mkNProd rlvl prods
| arg::args => do
let argType ← inferType arg
forallTelescope argType fun arg_args arg_type => do
if typeFormers.contains arg_type.getAppFn then
let name ← arg.fvarId!.getUserName
let type' ← forallTelescope argType fun args _ => mkForallFVars args (.sort rlvl)
withLocalDeclD name type' fun arg' => do
let snd ← mkForallFVars arg_args (mkAppN arg' arg_args)
let e' ← mkPProd argType snd
mkLambdaFVars #[arg'] (← go (prods.push e') args)
else
mkLambdaFVars #[arg] (← go prods args)
/--
Constructs the `.below` or `.ibelow` definition for a inductive predicate.
For example for the `List` type, it constructs,
```
@[reducible] protected def List.below.{u_1, u} : {α : Type u} →
{motive : List α → Sort u_1} → List α → Sort (max 1 u_1) :=
fun {α} {motive} t =>
List.rec PUnit (fun head tail tail_ih => PProd (PProd (motive tail) tail_ih) PUnit) t
```
and
```
@[reducible] protected def List.ibelow.{u} : {α : Type u} →
{motive : List α → Prop} → List α → Prop :=
fun {α} {motive} t =>
List.rec True (fun head tail tail_ih => (motive tail ∧ tail_ih) ∧ True) t
```
-/
private def mkBelowOrIBelow (indName : Name) (ibelow : Bool) : MetaM Unit := do
let .inductInfo indVal ← getConstInfo indName | return
unless indVal.isRec do return
if ← isPropFormerType indVal.type then return
let recName := mkRecName indName
-- The construction follows the type of `ind.rec`
let .recInfo recVal ← getConstInfo recName
| throwError "{recName} not a .recInfo"
let lvl::lvls := recVal.levelParams.map (Level.param ·)
| throwError "recursor {recName} has no levelParams"
let lvlParam := recVal.levelParams.head!
-- universe parameter names of ibelow/below
let blvls :=
-- For ibelow we instantiate the first universe parameter of `.rec` to `.zero`
if ibelow then recVal.levelParams.tail!
else recVal.levelParams
let .some ilvl ← typeFormerTypeLevel indVal.type
| throwError "type {indVal.type} of inductive {indVal.name} not a type former?"
-- universe level of the resultant type
let rlvl : Level :=
if ibelow then
0
else if indVal.isReflexive then
if let .max 1 lvl := ilvl then
mkLevelMax' (.succ lvl) lvl
else
mkLevelMax' (.succ lvl) ilvl
else
mkLevelMax' 1 lvl
let refType :=
if ibelow then
recVal.type.instantiateLevelParams [lvlParam] [0]
else if indVal.isReflexive then
recVal.type.instantiateLevelParams [lvlParam] [lvl.succ]
else
recVal.type
let decl ← forallTelescope refType fun refArgs _ => do
assert! refArgs.size == indVal.numParams + recVal.numMotives + recVal.numMinors + indVal.numIndices + 1
let params : Array Expr := refArgs[:indVal.numParams]
let typeFormers : Array Expr := refArgs[indVal.numParams:indVal.numParams + recVal.numMotives]
let minors : Array Expr := refArgs[indVal.numParams + recVal.numMotives:indVal.numParams + recVal.numMotives + recVal.numMinors]
let remaining : Array Expr := refArgs[indVal.numParams + recVal.numMotives + recVal.numMinors:]
let mut val := .const recName (rlvl.succ :: lvls)
-- add parameters
val := mkAppN val params
-- add type formers
for typeFormer in typeFormers do
let arg ← forallTelescope (← inferType typeFormer) fun targs _ =>
mkLambdaFVars targs (.sort rlvl)
val := .app val arg
-- add minor premises
for minor in minors do
let arg ← buildBelowMinorPremise rlvl typeFormers (← inferType minor)
val := .app val arg
-- add indices and major premise
val := mkAppN val remaining
-- All paramaters of `.rec` besides the `minors` become parameters of `.below`
let below_params := params ++ typeFormers ++ remaining
let type ← mkForallFVars below_params (.sort rlvl)
val ← mkLambdaFVars below_params val
let name := if ibelow then mkIBelowName indName else mkBelowName indName
mkDefinitionValInferrringUnsafe name blvls type val .abbrev
addDecl (.defnDecl decl)
setReducibleAttribute decl.name
modifyEnv fun env => markAuxRecursor env decl.name
modifyEnv fun env => addProtected env decl.name
def mkBelow (declName : Name) : MetaM Unit := mkBelowOrIBelow declName true
def mkIBelow (declName : Name) : MetaM Unit := mkBelowOrIBelow declName false
/--
If `minorType` is the type of a minor premies of a recursor, such as
```
(cons : (head : α) → (tail : List α) → (tail_hs : motive tail) → motive (head :: tail))
```
of `List.rec`, constructs the corresponding argument to `List.rec` in the construction
of `.brecOn` definition; in this case
```
fun head tail tail_ih =>
⟨F_1 (head :: tail) ⟨tail_ih, PUnit.unit⟩, ⟨tail_ih, PUnit.unit⟩⟩
```
of type
```
(head : α) → (tail : List α) →
PProd (motive tail) (List.below tail) →
PProd (motive (head :: tail)) (PProd (PProd (motive tail) (List.below tail)) PUnit)
```
The parameter `typeFormers` are the `motive`s.
-/
private def buildBRecOnMinorPremise (rlvl : Level) (typeFormers : Array Expr)
(belows : Array Expr) (fs : Array Expr) (minorType : Expr) : MetaM Expr :=
forallTelescope minorType fun minor_args minor_type => do
let rec go (prods : Array Expr) : List Expr → MetaM Expr
| [] => minor_type.withApp fun minor_type_fn minor_type_args => do
let b ← mkNProdMk rlvl prods
let .some ⟨idx, _⟩ := typeFormers.indexOf? minor_type_fn
| throwError m!"Did not find {minor_type} in {typeFormers}"
mkPProdMk (mkAppN fs[idx]! (minor_type_args.push b)) b
| arg::args => do
let argType ← inferType arg
forallTelescope argType fun arg_args arg_type => do
arg_type.withApp fun arg_type_fn arg_type_args => do
if let .some idx := typeFormers.indexOf? arg_type_fn then
let name ← arg.fvarId!.getUserName
let type' ← mkForallFVars arg_args
(← mkPProd arg_type (mkAppN belows[idx]! arg_type_args) )
withLocalDeclD name type' fun arg' => do
if arg_args.isEmpty then
mkLambdaFVars #[arg'] (← go (prods.push arg') args)
else
let r := mkAppN arg' arg_args
let r₁ ← mkLambdaFVars arg_args (← mkPProdFst r)
let r₂ ← mkLambdaFVars arg_args (← mkPProdSnd r)
let r ← mkPProdMk r₁ r₂
mkLambdaFVars #[arg'] (← go (prods.push r) args)
else
mkLambdaFVars #[arg] (← go prods args)
go #[] minor_args.toList
/--
Constructs the `.brecon` or `.binductionon` definition for a inductive predicate.
For example for the `List` type, it constructs,
```
@[reducible] protected def List.brecOn.{u_1, u} : {α : Type u} → {motive : List α → Sort u_1} →
(t : List α) → ((t : List α) → List.below t → motive t) → motive t :=
fun {α} {motive} t (F_1 : (t : List α) → List.below t → motive t) => (
@List.rec α (fun t => PProd (motive t) (@List.below α motive t))
⟨F_1 [] PUnit.unit, PUnit.unit⟩
(fun head tail tail_ih => ⟨F_1 (head :: tail) ⟨tail_ih, PUnit.unit⟩, ⟨tail_ih, PUnit.unit⟩⟩)
t
).1
```
and
```
@[reducible] protected def List.binductionOn.{u} : ∀ {α : Type u} {motive : List α → Prop}
(t : List α), (∀ (t : List α), List.ibelow t → motive t) → motive t :=
fun {α} {motive} t F_1 => (
@List.rec α (fun t => And (motive t) (@List.ibelow α motive t))
⟨F_1 [] True.intro, True.intro⟩
(fun head tail tail_ih => ⟨F_1 (head :: tail) ⟨tail_ih, True.intro⟩, ⟨tail_ih, True.intro⟩⟩)
t
).1
```
-/
def mkBRecOnOrBInductionOn (indName : Name) (ind : Bool) : MetaM Unit := do
let .inductInfo indVal ← getConstInfo indName | return
unless indVal.isRec do return
if ← isPropFormerType indVal.type then return
let recName := mkRecName indName
let .recInfo recVal ← getConstInfo recName | return
unless recVal.numMotives = indVal.all.length do
/-
The mutual declaration containing `declName` contains nested inductive datatypes.
We don't support this kind of declaration here yet. We probably never will :)
To support it, we will need to generate an auxiliary `below` for each nested inductive
type since their default `below` is not good here. For example, at
```
inductive Term
| var : String -> Term
| app : String -> List Term -> Term
```
The `List.below` is not useful since it will not allow us to recurse over the nested terms.
We need to generate another one using the auxiliary recursor `Term.rec_1` for `List Term`.
-/
return
let lvl::lvls := recVal.levelParams.map (Level.param ·)
| throwError "recursor {recName} has no levelParams"
let lvlParam := recVal.levelParams.head!
-- universe parameter names of brecOn/binductionOn
let blps := if ind then recVal.levelParams.tail! else recVal.levelParams
-- universe arguments of below/ibelow
let blvls := if ind then lvls else lvl::lvls
let .some ⟨idx, _⟩ := indVal.all.toArray.indexOf? indName
| throwError m!"Did not find {indName} in {indVal.all}"
let .some ilvl ← typeFormerTypeLevel indVal.type
| throwError "type {indVal.type} of inductive {indVal.name} not a type former?"
-- universe level of the resultant type
let rlvl : Level :=
if ind then
0
else if indVal.isReflexive then
if let .max 1 lvl := ilvl then
mkLevelMax' (.succ lvl) lvl
else
mkLevelMax' (.succ lvl) ilvl
else
mkLevelMax' 1 lvl
let refType :=
if ind then
recVal.type.instantiateLevelParams [lvlParam] [0]
else if indVal.isReflexive then
recVal.type.instantiateLevelParams [lvlParam] [lvl.succ]
else
recVal.type
let decl ← forallTelescope refType fun refArgs _ => do
assert! refArgs.size == indVal.numParams + recVal.numMotives + recVal.numMinors + indVal.numIndices + 1
let params : Array Expr := refArgs[:indVal.numParams]
let typeFormers : Array Expr := refArgs[indVal.numParams:indVal.numParams + recVal.numMotives]
let minors : Array Expr := refArgs[indVal.numParams + recVal.numMotives:indVal.numParams + recVal.numMotives + recVal.numMinors]
let remaining : Array Expr := refArgs[indVal.numParams + recVal.numMotives + recVal.numMinors:]
-- One `below` for each type former (same parameters)
let belows := indVal.all.toArray.map fun n =>
let belowName := if ind then mkIBelowName n else mkBelowName n
mkAppN (.const belowName blvls) (params ++ typeFormers)
-- create types of functionals (one for each type former)
-- (F_1 : (t : List α) → (f : List.below t) → motive t)
-- and bring parameters of that type into scope
let mut fDecls : Array (Name × (Array Expr -> MetaM Expr)) := #[]
for typeFormer in typeFormers, below in belows, i in [:typeFormers.size] do
let fType ← forallTelescope (← inferType typeFormer) fun targs _ => do
withLocalDeclD `f (mkAppN below targs) fun f =>
mkForallFVars (targs.push f) (mkAppN typeFormer targs)
let fName := .mkSimple s!"F_{i + 1}"
fDecls := fDecls.push (fName, fun _ => pure fType)
withLocalDeclsD fDecls fun fs => do
let mut val := .const recName (rlvl :: lvls)
-- add parameters
val := mkAppN val params
-- add type formers
for typeFormer in typeFormers, below in belows do
-- example: (motive := fun t => PProd (motive t) (@List.below α motive t))
let arg ← forallTelescope (← inferType typeFormer) fun targs _ => do
let cType := mkAppN typeFormer targs
let belowType := mkAppN below targs
let arg ← mkPProd cType belowType
mkLambdaFVars targs arg
val := .app val arg
-- add minor premises
for minor in minors do
let arg ← buildBRecOnMinorPremise rlvl typeFormers belows fs (← inferType minor)
val := .app val arg
-- add indices and major premise
val := mkAppN val remaining
-- project out first component
val ← mkPProdFst val
-- All paramaters of `.rec` besides the `minors` become parameters of `.bRecOn`, and the `fs`
let below_params := params ++ typeFormers ++ remaining ++ fs
let type ← mkForallFVars below_params (mkAppN typeFormers[idx]! remaining)
val ← mkLambdaFVars below_params val
let name := if ind then mkBInductionOnName indName else mkBRecOnName indName
mkDefinitionValInferrringUnsafe name blps type val .abbrev
addDecl (.defnDecl decl)
setReducibleAttribute decl.name
modifyEnv fun env => markAuxRecursor env decl.name
modifyEnv fun env => addProtected env decl.name
def mkBRecOn (declName : Name) : MetaM Unit := mkBRecOnOrBInductionOn declName false
def mkBInductionOn (declName : Name) : MetaM Unit := mkBRecOnOrBInductionOn declName true

2
src/library/constructions/CMakeLists.txt
View file

@ -1,3 +1,3 @@
add_library(constructions OBJECT cases_on.cpp
no_confusion.cpp projection.cpp brec_on.cpp init_module.cpp
no_confusion.cpp projection.cpp init_module.cpp
util.cpp)

318
src/library/constructions/brec_on.cpp
View file

@ -1,318 +0,0 @@
/*
Copyright (c) 2014 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Author: Leonardo de Moura
*/
#include "runtime/sstream.h"
#include "kernel/kernel_exception.h"
#include "kernel/environment.h"
#include "kernel/instantiate.h"
#include "kernel/abstract.h"
#include "kernel/type_checker.h"
#include "kernel/inductive.h"
#include "library/reducible.h"
#include "library/bin_app.h"
#include "library/suffixes.h"
#include "library/util.h"
#include "library/aux_recursors.h"
#include "library/constructions/util.h"
namespace lean {
static optional<unsigned> is_typeformer_app(buffer<name> const & typeformer_names, expr const & e) {
expr const & fn = get_app_fn(e);
if (!is_fvar(fn))
return optional<unsigned>();
unsigned r = 0;
for (name const & n : typeformer_names) {
if (fvar_name(fn) == n)
return optional<unsigned>(r);
r++;
}
return optional<unsigned>();
}
static declaration mk_below(environment const & env, name const & n, bool ibelow) {
local_ctx lctx;
constant_info ind_info = env.get(n);
inductive_val ind_val = ind_info.to_inductive_val();
name_generator ngen = mk_constructions_name_generator();
unsigned nparams = ind_val.get_nparams();
constant_info rec_info = env.get(mk_rec_name(n));
recursor_val rec_val = rec_info.to_recursor_val();
unsigned nminors = rec_val.get_nminors();
unsigned ntypeformers = rec_val.get_nmotives();
names lps = rec_info.get_lparams();
bool is_reflexive = ind_val.is_reflexive();
level lvl = mk_univ_param(head(lps));
levels lvls = lparams_to_levels(tail(lps));
names blvls; // universe parameter names of ibelow/below
level rlvl; // universe level of the resultant type
// The arguments of below (ibelow) are the ones in the recursor - minor premises.
// The universe we map to is also different (l+1 for below of reflexive types) and (0 fo ibelow).
expr ref_type;
expr Type_result;
if (ibelow) {
// we are eliminating to Prop
blvls = tail(lps);
rlvl = mk_level_zero();
ref_type = instantiate_lparam(rec_info.get_type(), param_id(lvl), mk_level_zero());
} else if (is_reflexive) {
blvls = lps;
rlvl = get_datatype_level(env, ind_info.get_type());
// if rlvl is of the form (max 1 l), then rlvl <- l
if (is_max(rlvl) && is_one(max_lhs(rlvl)))
rlvl = max_rhs(rlvl);
rlvl = mk_max(mk_succ(lvl), rlvl);
ref_type = instantiate_lparam(rec_info.get_type(), param_id(lvl), mk_succ(lvl));
} else {
// we can simplify the universe levels for non-reflexive datatypes
blvls = lps;
rlvl = mk_max(mk_level_one(), lvl);
ref_type = rec_info.get_type();
}
Type_result = mk_sort(rlvl);
buffer<expr> ref_args;
to_telescope(lctx, ngen, ref_type, ref_args);
lean_assert(ref_args.size() == nparams + ntypeformers + nminors + ind_val.get_nindices() + 1);
// args contains the below/ibelow arguments
buffer<expr> args;
buffer<name> typeformer_names;
// add parameters and typeformers
for (unsigned i = 0; i < nparams; i++)
args.push_back(ref_args[i]);
for (unsigned i = nparams; i < nparams + ntypeformers; i++) {
args.push_back(ref_args[i]);
typeformer_names.push_back(fvar_name(ref_args[i]));
}
// we ignore minor premises in below/ibelow
for (unsigned i = nparams + ntypeformers + nminors; i < ref_args.size(); i++)
args.push_back(ref_args[i]);
// We define below/ibelow using the recursor for this type
levels rec_lvls = cons(mk_succ(rlvl), lvls);
expr rec = mk_constant(rec_info.get_name(), rec_lvls);
for (unsigned i = 0; i < nparams; i++)
rec = mk_app(rec, args[i]);
// add type formers
for (unsigned i = nparams; i < nparams + ntypeformers; i++) {
buffer<expr> targs;
to_telescope(lctx, ngen, lctx.get_type(args[i]), targs);
rec = mk_app(rec, lctx.mk_lambda(targs, Type_result));
}
// add minor premises
for (unsigned i = nparams + ntypeformers; i < nparams + ntypeformers + nminors; i++) {
expr minor = ref_args[i];
expr minor_type = lctx.get_type(minor);
buffer<expr> minor_args;
minor_type = to_telescope(lctx, ngen, minor_type, minor_args);
buffer<expr> prod_pairs;
for (expr & minor_arg : minor_args) {
buffer<expr> minor_arg_args;
expr minor_arg_type = to_telescope(env, lctx, ngen, lctx.get_type(minor_arg), minor_arg_args);
if (is_typeformer_app(typeformer_names, minor_arg_type)) {
expr fst = lctx.get_type(minor_arg);
minor_arg = lctx.mk_local_decl(ngen, lctx.get_local_decl(minor_arg).get_user_name(), lctx.mk_pi(minor_arg_args, Type_result));
expr snd = lctx.mk_pi(minor_arg_args, mk_app(minor_arg, minor_arg_args));
type_checker tc(env, lctx);
prod_pairs.push_back(mk_pprod(tc, fst, snd, ibelow));
}
}
type_checker tc(env, lctx);
expr new_arg = foldr([&](expr const & a, expr const & b) { return mk_pprod(tc, a, b, ibelow); },
[&]() { return mk_unit(rlvl, ibelow); },
prod_pairs.size(), prod_pairs.data());
rec = mk_app(rec, lctx.mk_lambda(minor_args, new_arg));
}
// add indices and major premise
for (unsigned i = nparams + ntypeformers; i < args.size(); i++) {
rec = mk_app(rec, args[i]);
}
name below_name = ibelow ? name{n, "ibelow"} : name{n, "below"};
expr below_type = lctx.mk_pi(args, Type_result);
expr below_value = lctx.mk_lambda(args, rec);
return mk_definition_inferring_unsafe(env, below_name, blvls, below_type, below_value,
reducibility_hints::mk_abbreviation());
}
static declaration mk_brec_on(environment const & env, name const & n, bool ind) {
local_ctx lctx;
constant_info ind_info = env.get(n);
inductive_val ind_val = ind_info.to_inductive_val();
name_generator ngen = mk_constructions_name_generator();
unsigned nparams = ind_val.get_nparams();
constant_info rec_info = env.get(mk_rec_name(n));
recursor_val rec_val = rec_info.to_recursor_val();
unsigned nminors = rec_val.get_nminors();
unsigned ntypeformers = rec_val.get_nmotives();
names lps = rec_info.get_lparams();
bool is_reflexive = ind_val.is_reflexive();
level lvl = mk_univ_param(head(lps));
levels lvls = lparams_to_levels(tail(lps));
level rlvl;
names blps;
levels blvls; // universe level parameters of brec_on/binduction_on
// The arguments of brec_on (binduction_on) are the ones in the recursor - minor premises.
// The universe we map to is also different (l+1 for below of reflexive types) and (0 fo ibelow).
expr ref_type;
if (ind) {
// we are eliminating to Prop
blps = tail(lps);
blvls = lvls;
rlvl = mk_level_zero();
ref_type = instantiate_lparam(rec_info.get_type(), param_id(lvl), mk_level_zero());
} else if (is_reflexive) {
blps = lps;
blvls = cons(lvl, lvls);
rlvl = get_datatype_level(env, ind_info.get_type());
// if rlvl is of the form (max 1 l), then rlvl <- l
if (is_max(rlvl) && is_one(max_lhs(rlvl)))
rlvl = max_rhs(rlvl);
rlvl = mk_max(mk_succ(lvl), rlvl);
// inner_prod, inner_prod_intro, pr1, pr2 do not use the same universe levels for
// reflective datatypes.
ref_type = instantiate_lparam(rec_info.get_type(), param_id(lvl), mk_succ(lvl));
} else {
// we can simplify the universe levels for non-reflexive datatypes
blps = lps;
blvls = cons(lvl, lvls);
rlvl = mk_max(mk_level_one(), lvl);
ref_type = rec_info.get_type();
}
buffer<expr> ref_args;
to_telescope(lctx, ngen, ref_type, ref_args);
lean_assert(ref_args.size() == nparams + ntypeformers + nminors + ind_val.get_nindices() + 1);
// args contains the brec_on/binduction_on arguments
buffer<expr> args;
buffer<name> typeformer_names;
// add parameters and typeformers
for (unsigned i = 0; i < nparams; i++)
args.push_back(ref_args[i]);
for (unsigned i = nparams; i < nparams + ntypeformers; i++) {
args.push_back(ref_args[i]);
typeformer_names.push_back(fvar_name(ref_args[i]));
}
// add indices and major premise
for (unsigned i = nparams + ntypeformers + nminors; i < ref_args.size(); i++)
args.push_back(ref_args[i]);
// create below terms (one per datatype)
// (below.{lvls} params type-formers)
// Remark: it also creates the result type
buffer<expr> belows;
expr result_type;
unsigned k = 0;
for (name const & n1 : ind_val.get_all()) {
if (n1 == n) {
result_type = ref_args[nparams + k];
for (unsigned i = nparams + ntypeformers + nminors; i < ref_args.size(); i++)
result_type = mk_app(result_type, ref_args[i]);
}
k++;
name bname = name(n1, ind ? "ibelow" : "below");
expr below = mk_constant(bname, blvls);
for (unsigned i = 0; i < nparams; i++)
below = mk_app(below, ref_args[i]);
for (unsigned i = nparams; i < nparams + ntypeformers; i++)
below = mk_app(below, ref_args[i]);
belows.push_back(below);
}
// create functionals (one for each type former)
// Pi idxs t, below idxs t -> C idxs t
buffer<expr> Fs;
name F_name("F");
for (unsigned i = nparams, j = 0; i < nparams + ntypeformers; i++, j++) {
expr const & C = ref_args[i];
buffer<expr> F_args;
to_telescope(lctx, ngen, lctx.get_type(C), F_args);
expr F_result = mk_app(C, F_args);
expr F_below = mk_app(belows[j], F_args);
F_args.push_back(lctx.mk_local_decl(ngen, "f", F_below));
expr F_type = lctx.mk_pi(F_args, F_result);
expr F = lctx.mk_local_decl(ngen, F_name.append_after(j+1), F_type);
Fs.push_back(F);
args.push_back(F);
}
// We define brec_on/binduction_on using the recursor for this type
levels rec_lvls = cons(rlvl, lvls);
expr rec = mk_constant(rec_info.get_name(), rec_lvls);
// add parameters to rec
for (unsigned i = 0; i < nparams; i++)
rec = mk_app(rec, ref_args[i]);
// add type formers to rec
// Pi indices t, prod (C ... t) (below ... t)
for (unsigned i = nparams, j = 0; i < nparams + ntypeformers; i++, j++) {
expr const & C = ref_args[i];
buffer<expr> C_args;
to_telescope(lctx, ngen, lctx.get_type(C), C_args);
expr C_t = mk_app(C, C_args);
expr below_t = mk_app(belows[j], C_args);
type_checker tc(env, lctx);
expr prod = mk_pprod(tc, C_t, below_t, ind);
rec = mk_app(rec, lctx.mk_lambda(C_args, prod));
}
// add minor premises to rec
for (unsigned i = nparams + ntypeformers, j = 0; i < nparams + ntypeformers + nminors; i++, j++) {
expr minor = ref_args[i];
expr minor_type = lctx.get_type(minor);
buffer<expr> minor_args;
minor_type = to_telescope(lctx, ngen, minor_type, minor_args);
buffer<expr> pairs;
for (expr & minor_arg : minor_args) {
buffer<expr> minor_arg_args;
expr minor_arg_type = to_telescope(env, lctx, ngen, lctx.get_type(minor_arg), minor_arg_args);
if (auto k = is_typeformer_app(typeformer_names, minor_arg_type)) {
buffer<expr> C_args;
get_app_args(minor_arg_type, C_args);
type_checker tc(env, lctx);
expr new_minor_arg_type = mk_pprod(tc, minor_arg_type, mk_app(belows[*k], C_args), ind);
minor_arg = lctx.mk_local_decl(ngen, lctx.get_local_decl(minor_arg).get_user_name(), lctx.mk_pi(minor_arg_args, new_minor_arg_type));
if (minor_arg_args.empty()) {
pairs.push_back(minor_arg);
} else {
type_checker tc(env, lctx);
expr r = mk_app(minor_arg, minor_arg_args);
expr r_1 = lctx.mk_lambda(minor_arg_args, mk_pprod_fst(tc, r, ind));
expr r_2 = lctx.mk_lambda(minor_arg_args, mk_pprod_snd(tc, r, ind));
pairs.push_back(mk_pprod_mk(tc, r_1, r_2, ind));
}
}
}
type_checker tc(env, lctx);
expr b = foldr([&](expr const & a, expr const & b) { return mk_pprod_mk(tc, a, b, ind); },
[&]() { return mk_unit_mk(rlvl, ind); },
pairs.size(), pairs.data());
unsigned F_idx = *is_typeformer_app(typeformer_names, minor_type);
expr F = Fs[F_idx];
buffer<expr> F_args;
get_app_args(minor_type, F_args);
F_args.push_back(b);
expr new_arg = mk_pprod_mk(tc, mk_app(F, F_args), b, ind);
rec = mk_app(rec, lctx.mk_lambda(minor_args, new_arg));
}
// add indices and major to rec
for (unsigned i = nparams + ntypeformers + nminors; i < ref_args.size(); i++)
rec = mk_app(rec, ref_args[i]);
type_checker tc(env, lctx);
name brec_on_name = name(n, ind ? g_binduction_on : g_brec_on);
expr brec_on_type = lctx.mk_pi(args, result_type);
expr brec_on_value = lctx.mk_lambda(args, mk_pprod_fst(tc, rec, ind));
return mk_definition_inferring_unsafe(env, brec_on_name, blps, brec_on_type, brec_on_value,
reducibility_hints::mk_abbreviation());
}
extern "C" LEAN_EXPORT object * lean_mk_below(object * env, object * n, uint8 ibelow) {
return catch_kernel_exceptions<declaration>([&]() { return mk_below(environment(env), name(n, true), ibelow); });
}
extern "C" LEAN_EXPORT object * lean_mk_brec_on(object * env, object * n, uint8 ind) {
return catch_kernel_exceptions<declaration>([&]() { return mk_brec_on(environment(env), name(n, true), ind); });
}
}

22
src/library/constructions/brec_on.h
View file

@ -1,22 +0,0 @@
/*
Copyright (c) 2014 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Author: Leonardo de Moura
*/
#pragma once
#include "kernel/environment.h"
namespace lean {
/** \brief Given an inductive datatype \c n in \c env, return declaration for
<tt>n.below</tt> or <tt>.nibelow</tt> auxiliary construction for <tt>n.brec_on</t>
(aka below recursion on).
*/
declaration mk_below(environment const & env, name const & n, bool ibelow);
/** \brief Given an inductive datatype \c n in \c env, return declaration for
<tt>n.brec_on</tt> or <tt>n.binduction_on</tt>.
*/
declaration mk_brec_on(environment const & env, name const & n, bool ind);
}

57
src/library/constructions/util.cpp
View file

@ -12,63 +12,6 @@ Author: Leonardo de Moura
namespace lean {
static name * g_constructions_fresh = nullptr;
static level get_level(type_checker & ctx, expr const & A) {
expr S = ctx.whnf(ctx.infer(A));
if (!is_sort(S))
throw exception("invalid expression, sort expected");
return sort_level(S);
}
expr mk_and_intro(type_checker & ctx, expr const & Ha, expr const & Hb) {
return mk_app(mk_constant(get_and_intro_name()), ctx.infer(Ha), ctx.infer(Hb), Ha, Hb);
}
expr mk_and_left(type_checker &, expr const & H) {
return mk_proj(get_and_name(), nat(0), H);
}
expr mk_and_right(type_checker &, expr const & H) {
return mk_proj(get_and_name(), nat(1), H);
}
expr mk_pprod(type_checker & ctx, expr const & A, expr const & B) {
level l1 = get_level(ctx, A);
level l2 = get_level(ctx, B);
return mk_app(mk_constant(get_pprod_name(), {l1, l2}), A, B);
}
expr mk_pprod_mk(type_checker & ctx, expr const & a, expr const & b) {
expr A = ctx.infer(a);
expr B = ctx.infer(b);
level l1 = get_level(ctx, A);
level l2 = get_level(ctx, B);
return mk_app(mk_constant(get_pprod_mk_name(), {l1, l2}), A, B, a, b);
}
expr mk_pprod_fst(type_checker &, expr const & p) {
return mk_proj(get_pprod_name(), nat(0), p);
}
expr mk_pprod_snd(type_checker &, expr const & p) {
return mk_proj(get_pprod_name(), nat(1), p);
}
expr mk_pprod(type_checker & ctx, expr const & a, expr const & b, bool prop) {
return prop ? mk_and(a, b) : mk_pprod(ctx, a, b);
}
expr mk_pprod_mk(type_checker & ctx, expr const & a, expr const & b, bool prop) {
return prop ? mk_and_intro(ctx, a, b) : mk_pprod_mk(ctx, a, b);
}
expr mk_pprod_fst(type_checker & ctx, expr const & p, bool prop) {
return prop ? mk_and_left(ctx, p) : mk_pprod_fst(ctx, p);
}
expr mk_pprod_snd(type_checker & ctx, expr const & p, bool prop) {
return prop ? mk_and_right(ctx, p) : mk_pprod_snd(ctx, p);
}
name_generator mk_constructions_name_generator() {
return name_generator(*g_constructions_fresh);
}

7
src/library/constructions/util.h
View file

@ -9,13 +9,6 @@ Author: Leonardo de Moura
#include "kernel/type_checker.h"
namespace lean {
environment completion_add_to_black_list(environment const & env, name const & decl_name);
expr mk_pprod(type_checker & ctx, expr const & a, expr const & b, bool prop);
expr mk_pprod_mk(type_checker & ctx, expr const & a, expr const & b, bool prop);
expr mk_pprod_fst(type_checker & ctx, expr const & p, bool prop);
expr mk_pprod_snd(type_checker & ctx, expr const & p, bool prop);
name_generator mk_constructions_name_generator();
void initialize_constructions_util();
void finalize_constructions_util();