diff --git a/src/Lean/Elab/Inductive.lean b/src/Lean/Elab/Inductive.lean index c1a45e79b4..ecda085489 100644 --- a/src/Lean/Elab/Inductive.lean +++ b/src/Lean/Elab/Inductive.lean @@ -9,7 +9,7 @@ import Lean.Util.CollectLevelParams import Lean.Util.Constructions import Lean.Meta.CollectFVars import Lean.Meta.SizeOf -import Lean.Meta.ProofBelow +import Lean.Meta.IndPredBelow import Lean.Elab.Command import Lean.Elab.DefView import Lean.Elab.DeclUtil @@ -518,7 +518,7 @@ def elabInductiveViews (views : Array InductiveView) : CommandElabM Unit := do runTermElabM view0.declName fun vars => withRef ref do mkInductiveDecl vars views mkSizeOfInstances view0.declName - mkProofBelow view0.declName + Lean.Meta.IndPredBelow.mkBelow view0.declName applyDerivingHandlers views end Lean.Elab.Command diff --git a/src/Lean/Meta.lean b/src/Lean/Meta.lean index 61f30bfb64..f474c7fadd 100644 --- a/src/Lean/Meta.lean +++ b/src/Lean/Meta.lean @@ -29,7 +29,7 @@ import Lean.Meta.PPGoal import Lean.Meta.UnificationHint import Lean.Meta.Inductive import Lean.Meta.SizeOf -import Lean.Meta.ProofBelow +import Lean.Meta.IndPredBelow import Lean.Meta.Coe import Lean.Meta.SortLocalDecls import Lean.Meta.CollectFVars diff --git a/src/Lean/Meta/ProofBelow.lean b/src/Lean/Meta/IndPredBelow.lean similarity index 87% rename from src/Lean/Meta/ProofBelow.lean rename to src/Lean/Meta/IndPredBelow.lean index 3e840dbd7a..b06c5a790e 100644 --- a/src/Lean/Meta/ProofBelow.lean +++ b/src/Lean/Meta/IndPredBelow.lean @@ -8,23 +8,21 @@ import Lean.Util.Constructions import Lean.Meta.Transform import Lean.Meta.Tactic -namespace Lean.Meta - -namespace ProofBelow +namespace Lean.Meta.IndPredBelow /-- - The context used in the creation of the `ProofBelow` scheme for inductive predicates. + The context used in the creation of the `below` scheme for inductive predicates. -/ structure Context where motives : Array (Name × Expr) typeInfos : Array InductiveVal - proofBelowNames : Array Name + belowNames : Array Name headers : Array Expr numParams : Nat /-- Collection of variables used to keep track of the positions of binders in the construction - of `ProofBelow` motives and constructors. + of `below` motives and constructors. -/ structure Variables where target : Array Expr @@ -57,7 +55,7 @@ def mkContext (declName : Name) : MetaM Context := do typeInfos := typeInfos numParams := indVal.numParams headers := ←headers - proofBelowNames := ←indVal.all.toArray.mapM (·.appendAfter "ProofBelow") } + belowNames := ←indVal.all.toArray.map (· ++ `below) } where motiveName (motiveTypes : Array Expr) (i : Nat) : MetaM Name := if motiveTypes.size > 1 @@ -89,7 +87,7 @@ where partial def mkCtorType (ctx : Context) - (proofBelowIdx : Nat) + (belowIdx : Nat) (originalCtor : ConstructorVal) : MetaM Expr := forallTelescope originalCtor.type fun xs t => addHeaderVars { innerType := t @@ -101,7 +99,7 @@ partial def mkCtorType where addHeaderVars (vars : Variables) := do let headersWithNames ← ctx.headers.mapIdxM fun idx header => - (ctx.proofBelowNames[idx], fun _ => pure header) + (ctx.belowNames[idx], fun _ => pure header) withLocalDeclsD headersWithNames fun xs => addMotives { vars with indVal := xs } @@ -118,7 +116,7 @@ where let binder := vars.args[i] let binderType ←inferType binder if ←checkCount binderType then - mkProofBelowBinder vars binder binderType fun indValIdx x => + mkBelowBinder vars binder binderType fun indValIdx x => mkMotiveBinder vars indValIdx binder binderType fun y => modifyBinders { vars with target := vars.target ++ #[binder, x, y]} i.succ else modifyBinders { vars with target := vars.target.push binder } i.succ @@ -130,7 +128,7 @@ where mkAppN (mkConst originalCtor.name $ ctx.typeInfos[0].levelParams.map mkLevelParam) (vars.params ++ vars.args) - let innerType := mkAppN vars.indVal[proofBelowIdx] $ + let innerType := mkAppN vars.indVal[belowIdx] $ vars.params ++ vars.motives ++ args[ctx.numParams:] ++ #[hApp] let x ← mkForallFVars vars.target innerType replaceTempVars vars x @@ -139,7 +137,7 @@ where let levelParams := ctx.typeInfos[0].levelParams.map mkLevelParam - ctor.replaceFVars vars.indVal $ ctx.proofBelowNames.map fun indVal => + ctor.replaceFVars vars.indVal $ ctx.belowNames.map fun indVal => mkConst indVal levelParams checkCount (domain : Expr) : MetaM Bool := do @@ -156,7 +154,7 @@ where return cnt == 1 - mkProofBelowBinder + mkBelowBinder (vars : Variables) (binder : Expr) (domain : Expr) @@ -200,7 +198,7 @@ where def mkConstructor (ctx : Context) (i : Nat) (ctor : Name) : MetaM Constructor := do let ctorInfo ← getConstInfoCtor ctor - let name := ctor.updatePrefix ctx.proofBelowNames[i] + let name := ctor.updatePrefix ctx.belowNames[i] let type ← mkCtorType ctx i ctorInfo return { name := name @@ -211,11 +209,11 @@ def mkInductiveType (i : Fin ctx.typeInfos.size) (indVal : InductiveVal) : MetaM InductiveType := do return { - name := ctx.proofBelowNames[i] + name := ctx.belowNames[i] type := ctx.headers[i] ctors := ←indVal.ctors.mapM (mkConstructor ctx i) } -def mkProofBelowDecl (ctx : Context) : MetaM Declaration := do +def mkBelowDecl (ctx : Context) : MetaM Declaration := do let lparams := ctx.typeInfos[0].levelParams Declaration.inductDecl lparams @@ -254,7 +252,7 @@ where let motives ← ctx.motives.mapIdxM fun idx (_, motive) => do let motive ← instantiateForall motive params forallTelescope motive fun xs _ => do - mkLambdaFVars xs $ mkAppN (mkConst ctx.proofBelowNames[idx] levelParams) $ (params ++ motives ++ xs) + mkLambdaFVars xs $ mkAppN (mkConst ctx.belowNames[idx] levelParams) $ (params ++ motives ++ xs) withMVarContext m do let recursorInfo ← getConstInfo $ mkRecName indVal.name let recLevels := @@ -267,11 +265,11 @@ where applyCtors (ms : List MVarId) : MetaM $ List MVarId := do let mss ← ms.toArray.mapIdxM fun idx m => do let m ← introNPRec m - (←getMVarType m).withApp fun proofBelow args => + (←getMVarType m).withApp fun below args => args.back.withApp fun ctor args => - let ctor := ctor.constName!.updatePrefix proofBelow.constName! + let ctor := ctor.constName!.updatePrefix below.constName! withMVarContext m do - let ctor := mkConst ctor proofBelow.constLevels! + let ctor := mkConst ctor below.constLevels! apply m ctor return mss.foldr List.append [] @@ -334,32 +332,31 @@ where let args := params ++ motives ++ ys let premise := mkAppN - (mkConst ctx.proofBelowNames[idx.val] levels) args + (mkConst ctx.belowNames[idx.val] levels) args let conclusion := mkAppN motives[idx] ys mkForallFVars ys (←mkArrow premise conclusion) (←name, mkDomain) -end ProofBelow -def mkProofBelow (declName : Name) : MetaM Unit := do +def mkBelow (declName : Name) : MetaM Unit := do if (←isInductivePredicate declName) then let x ← getConstInfoInduct declName if x.isRec then - let ctx ← ProofBelow.mkContext declName - let decl ← ProofBelow.mkProofBelowDecl ctx + let ctx ← IndPredBelow.mkContext declName + let decl ← IndPredBelow.mkBelowDecl ctx addDecl decl - trace[Meta.ProofBelow] "added {ctx.proofBelowNames}" - ctx.proofBelowNames.forM Lean.mkCasesOn + trace[Meta.IndPredBelow] "added {ctx.belowNames}" + ctx.belowNames.forM Lean.mkCasesOn for i in [:ctx.typeInfos.size] do try - let decl ← ProofBelow.mkBrecOnDecl ctx i + let decl ← IndPredBelow.mkBrecOnDecl ctx i addDecl decl - catch e => trace[Meta.ProofBelow] "failed to prove brecOn for {ctx.proofBelowNames[i]}\n{e.toMessageData}" - else trace[Meta.ProofBelow] "Not recursive" - else trace[Meta.ProofBelow] "Not inductive predicate" + catch e => trace[Meta.IndPredBelow] "failed to prove brecOn for {ctx.belowNames[i]}\n{e.toMessageData}" + else trace[Meta.IndPredBelow] "Not recursive" + else trace[Meta.IndPredBelow] "Not inductive predicate" builtin_initialize - registerTraceClass `Meta.ProofBelow + registerTraceClass `Meta.IndPredBelow -end Lean.Meta \ No newline at end of file +end Lean.Meta.IndPredBelow \ No newline at end of file diff --git a/tests/lean/run/inductive_pred.lean b/tests/lean/run/inductive_pred.lean index 3f8f01a94b..4962a9d54c 100644 --- a/tests/lean/run/inductive_pred.lean +++ b/tests/lean/run/inductive_pred.lean @@ -7,7 +7,7 @@ def typeOf {α : Sort u} (a : α) := α theorem LE_brecOn : typeOf @LE.brecOn = ∀ {motive : (a a_1 : Nat) → LE a a_1 → Prop} {a a_1 : Nat} (x : LE a a_1), - (∀ (a a_2 : Nat) (x : LE a a_2), @LEProofBelow motive a a_2 x → motive a a_2 x) → motive a a_1 x := rfl + (∀ (a a_2 : Nat) (x : LE a a_2), @LE.below motive a a_2 x → motive a a_2 x) → motive a a_1 x := rfl theorem LE.trans : LE m n → LE n o → LE m o := by intro h1 h2 @@ -24,7 +24,7 @@ inductive Even : Nat → Prop | ss : Even n → Even n.succ.succ theorem Even_brecOn : typeOf @Even.brecOn = ∀ {motive : (a : Nat) → Even a → Prop} {a : Nat} (x : Even a), - (∀ (a : Nat) (x : Even a), @EvenProofBelow motive a x → motive a x) → motive a x := rfl + (∀ (a : Nat) (x : Even a), @Even.below motive a x → motive a x) → motive a x := rfl theorem Even.add : Even n → Even m → Even (n+m) := by intro h1 h2 @@ -44,7 +44,7 @@ inductive Power2 : Nat → Prop | ind : Power2 n → Power2 (2*n) -- Note that index here is not a constructor theorem Power2_brecOn : typeOf @Power2.brecOn = ∀ {motive : (a : Nat) → Power2 a → Prop} {a : Nat} (x : Power2 a), - (∀ (a : Nat) (x : Power2 a), @Power2ProofBelow motive a x → motive a x) → motive a x := rfl + (∀ (a : Nat) (x : Power2 a), @Power2.below motive a x → motive a x) → motive a x := rfl theorem Power2.mul : Power2 n → Power2 m → Power2 (n*m) := by intro h1 h2 @@ -82,11 +82,11 @@ def deterministic {X : Type} (R : X → X → Prop) := theorem step_deterministic' : deterministic step := λ x y₁ y₂ hy₁ hy₂ => @step.brecOn (λ s t st => ∀ y₂, s ==> y₂ → t = y₂) _ _ hy₁ (λ s t st hy₁ y₂ hy₂ => match hy₁, hy₂ with - | stepProofBelow.ST_PlusConstConst _ _, step.ST_PlusConstConst _ _ => rfl - | stepProofBelow.ST_Plus1 _ _ _ _ hy₁ ih, step.ST_Plus1 _ t₁' _ _ => by rw ←ih t₁'; assumption - | stepProofBelow.ST_Plus1 _ _ _ _ hy₁ ih, step.ST_Plus2 _ _ _ _ => by cases hy₁ - | stepProofBelow.ST_Plus2 _ _ _ _ _ ih, step.ST_Plus2 _ _ t₂ _ => by rw ←ih t₂; assumption - | stepProofBelow.ST_Plus2 _ _ _ _ hy₁ _, step.ST_PlusConstConst _ _ => by cases hy₁ + | step.below.ST_PlusConstConst _ _, step.ST_PlusConstConst _ _ => rfl + | step.below.ST_Plus1 _ _ _ _ hy₁ ih, step.ST_Plus1 _ t₁' _ _ => by rw ←ih t₁'; assumption + | step.below.ST_Plus1 _ _ _ _ hy₁ ih, step.ST_Plus2 _ _ _ _ => by cases hy₁ + | step.below.ST_Plus2 _ _ _ _ _ ih, step.ST_Plus2 _ _ t₂ _ => by rw ←ih t₂; assumption + | step.below.ST_Plus2 _ _ _ _ hy₁ _, step.ST_PlusConstConst _ _ => by cases hy₁ ) y₂ hy₂ section NestedRecursion @@ -111,9 +111,9 @@ axiom FS {n : Nat} : P n → P (f (f n)) theorem foo' : ∀ {n}, is_nat n → P n := fun h => @is_nat.brecOn (fun n hn => P n) _ h fun n h ih => match ih with - | is_natProofBelow.Z => F0 - | is_natProofBelow.S _ is_natProofBelow.Z _ => F1 - | is_natProofBelow.S _ (is_natProofBelow.S a b hx) h₂ => FS hx + | is_nat.below.Z => F0 + | is_nat.below.S _ is_nat.below.Z _ => F1 + | is_nat.below.S _ (is_nat.below.S a b hx) h₂ => FS hx end NestedRecursion diff --git a/tests/lean/run/reflectiveIndPred.lean b/tests/lean/run/reflectiveIndPred.lean index 09d484100a..7abbec8d7f 100644 --- a/tests/lean/run/reflectiveIndPred.lean +++ b/tests/lean/run/reflectiveIndPred.lean @@ -8,5 +8,5 @@ inductive Pos : Expr → Prop | add : Pos e₁ → Pos e₂ → Pos (Expr.add e₁ e₂) | fn : ((n : Nat) → Pos (f n)) → Pos (Expr.fn f) -#print PosProofBelow +#print Pos.below #print Pos.brecOn