From ea22ef44852876fcbfbc330909cbcae9bf5e8ee2 Mon Sep 17 00:00:00 2001 From: Joachim Breitner Date: Wed, 26 Jun 2024 13:10:39 +0200 Subject: [PATCH] refactor: port below and brecOn construction to Lean (#4517) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit 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. --- src/Lean/Meta/Constructions.lean | 50 +-- src/Lean/Meta/Constructions/BRecOn.lean | 393 +++++++++++++++++++++++ src/library/constructions/CMakeLists.txt | 2 +- src/library/constructions/brec_on.cpp | 318 ------------------ src/library/constructions/brec_on.h | 22 -- src/library/constructions/util.cpp | 57 ---- src/library/constructions/util.h | 7 - 7 files changed, 395 insertions(+), 454 deletions(-) create mode 100644 src/Lean/Meta/Constructions/BRecOn.lean delete mode 100644 src/library/constructions/brec_on.cpp delete mode 100644 src/library/constructions/brec_on.h diff --git a/src/Lean/Meta/Constructions.lean b/src/Lean/Meta/Constructions.lean index 149e00de28..bafb7e7052 100644 --- a/src/Lean/Meta/Constructions.lean +++ b/src/Lean/Meta/Constructions.lean @@ -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 diff --git a/src/Lean/Meta/Constructions/BRecOn.lean b/src/Lean/Meta/Constructions/BRecOn.lean new file mode 100644 index 0000000000..c7368a4081 --- /dev/null +++ b/src/Lean/Meta/Constructions/BRecOn.lean @@ -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 diff --git a/src/library/constructions/CMakeLists.txt b/src/library/constructions/CMakeLists.txt index b115cc0a33..0737620c57 100644 --- a/src/library/constructions/CMakeLists.txt +++ b/src/library/constructions/CMakeLists.txt @@ -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) diff --git a/src/library/constructions/brec_on.cpp b/src/library/constructions/brec_on.cpp deleted file mode 100644 index 912e803f52..0000000000 --- a/src/library/constructions/brec_on.cpp +++ /dev/null @@ -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 is_typeformer_app(buffer const & typeformer_names, expr const & e) { - expr const & fn = get_app_fn(e); - if (!is_fvar(fn)) - return optional(); - unsigned r = 0; - for (name const & n : typeformer_names) { - if (fvar_name(fn) == n) - return optional(r); - r++; - } - return optional(); -} - -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 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 args; - buffer 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 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 minor_args; - minor_type = to_telescope(lctx, ngen, minor_type, minor_args); - buffer prod_pairs; - for (expr & minor_arg : minor_args) { - buffer 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 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 args; - buffer 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 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 Fs; - name F_name("F"); - for (unsigned i = nparams, j = 0; i < nparams + ntypeformers; i++, j++) { - expr const & C = ref_args[i]; - buffer 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 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 minor_args; - minor_type = to_telescope(lctx, ngen, minor_type, minor_args); - buffer pairs; - for (expr & minor_arg : minor_args) { - buffer 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 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 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([&]() { 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([&]() { return mk_brec_on(environment(env), name(n, true), ind); }); -} -} diff --git a/src/library/constructions/brec_on.h b/src/library/constructions/brec_on.h deleted file mode 100644 index 4eed3fc22c..0000000000 --- a/src/library/constructions/brec_on.h +++ /dev/null @@ -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 - n.below or .nibelow auxiliary construction for n.brec_on - (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 - n.brec_on or n.binduction_on. -*/ -declaration mk_brec_on(environment const & env, name const & n, bool ind); - -} diff --git a/src/library/constructions/util.cpp b/src/library/constructions/util.cpp index 7a3da4a234..139d3bae66 100644 --- a/src/library/constructions/util.cpp +++ b/src/library/constructions/util.cpp @@ -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); } diff --git a/src/library/constructions/util.h b/src/library/constructions/util.h index c099daaedb..555622d8b6 100644 --- a/src/library/constructions/util.h +++ b/src/library/constructions/util.h @@ -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();