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

test: extend inductive_pred.lean with tests using the new construction.

Browse source
This commit is contained in:
Daniel Fabian 2021-04-24 02:51:13 +00:00 • committed by Leonardo de Moura
parent 371504e9cf
commit eda4bdd337
2 changed files with 90 additions and 24 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

42
src/Lean/Meta/ProofBelow.lean
View file

@ -49,7 +49,7 @@ def mkContext (declName : Name) : MetaM Context := do
let indVal ← getConstInfoInduct declName
let typeInfos ← indVal.all.toArray.mapM getConstInfoInduct
let motiveTypes ← typeInfos.mapM motiveType
let motives := ←motiveTypes.mapIdxM fun j motive => do
let motives ←motiveTypes.mapIdxM fun j motive => do
(←motiveName motiveTypes j.val, motive)
let headers := typeInfos.mapM $ mkHeader motives indVal.numParams
return {
@ -65,9 +65,9 @@ where
else mkFreshUserName "motive"
mkHeader
(motives : Array (Name × Expr))
(numParams : Nat)
(indVal : InductiveVal) : MetaM Expr := do
(motives : Array (Name × Expr))
(numParams : Nat)
(indVal : InductiveVal) : MetaM Expr := do
let header ← forallTelescope indVal.type fun xs t => do
withNewBinderInfos (xs.map fun x => (x.fvarId!, BinderInfo.implicit)) $
mkForallFVars xs $ ←mkArrow (mkAppN (mkIndValConst indVal) xs) t
@ -116,7 +116,7 @@ where
modifyBinders (vars : Variables) (i : Nat) := do
if i < vars.args.size then
let binder := vars.args[i]
let binderType := ←inferType binder
let binderType ←inferType binder
if ←checkCount binderType then
mkProofBelowBinder vars binder binderType fun indValIdx x =>
mkMotiveBinder vars indValIdx binder binderType fun y =>
@ -144,18 +144,15 @@ where
checkCount (domain : Expr) : MetaM Bool := do
let run (x : StateRefT Nat MetaM Expr) : MetaM (Expr × Nat) := StateRefT'.run x 0
let (_, cnt) := ←run $ transform domain fun e => do
let (_, cnt) ←run $ transform domain fun e => do
if let some name := e.constName? then
if let some idx := ctx.typeInfos.findIdx? fun indVal => indVal.name == name then
let cnt := ←get
let cnt ←get
set $ cnt + 1
TransformStep.visit e
if cnt > 1 then
let message :=
"only arrows are allowed as premises. Multiple recursive occurrences detected:\n "
++ (←ppExpr domain)
throwError message
throwError "only arrows are allowed as premises. Multiple recursive occurrences detected:{indentExpr domain}"
return cnt == 1
@ -166,10 +163,7 @@ where
{α : Type} (k : Nat → Expr → MetaM α) : MetaM α := do
forallTelescope domain fun xs t => do
let fail _ := do
let message :=
"only trivial inductive applications supported in premises:\n "
++ (←ppExpr t)
throwError message
throwError "only trivial inductive applications supported in premises:{indentExpr t}"
t.withApp fun f args => do
if let some name := f.constName? then
@ -194,8 +188,6 @@ where
{α : Type} (k : Expr → MetaM α) : MetaM α := do
forallTelescope domain fun xs t => do
t.withApp fun f args => do
let name := f.constName!
let indVal := ctx.typeInfos[indValIdx]
let hApp := mkAppN binder xs
let t := mkAppN vars.motives[indValIdx] $ args[ctx.numParams:] ++ #[hApp]
let newDomain ← mkForallFVars xs t
@ -215,9 +207,9 @@ def mkConstructor (ctx : Context) (i : Nat) (ctor : Name) : MetaM Constructor :=
type := type }
def mkInductiveType
(ctx : Context)
(i : Fin ctx.typeInfos.size)
(indVal : InductiveVal) : MetaM InductiveType := do
(ctx : Context)
(i : Fin ctx.typeInfos.size)
(indVal : InductiveVal) : MetaM InductiveType := do
return {
name := ctx.proofBelowNames[i]
type := ctx.headers[i]
@ -253,7 +245,7 @@ where
match ←vars.indHyps.findSomeM?
(fun ih => do try some $ (←apply m $ mkFVar ih) catch ex => none) with
| some goals => goals
| none => throwError "cannot apply induction hypothesis: {←ppGoal m}"
| none => throwError "cannot apply induction hypothesis: {MessageData.ofGoal m}"
induction (m : MVarId) (vars : BrecOnVariables) : MetaM (List MVarId) := do
let params := vars.params.map mkFVar
@ -264,7 +256,7 @@ where
forallTelescope motive fun xs _ => do
mkLambdaFVars xs $ mkAppN (mkConst ctx.proofBelowNames[idx] levelParams) $ (params ++ motives ++ xs)
withMVarContext m do
let recursorInfo ← getConstInfo $ indVal.name ++ "rec"
let recursorInfo ← getConstInfo $ mkRecName indVal.name
let recLevels :=
if recursorInfo.numLevelParams > levelParams.length
then levelZero::levelParams
@ -360,8 +352,10 @@ def mkProofBelow (declName : Name) : MetaM Unit := do
trace[Meta.ProofBelow] "added {ctx.proofBelowNames}"
ctx.proofBelowNames.forM Lean.mkCasesOn
for i in [:ctx.typeInfos.size] do
let decl ← ProofBelow.mkBrecOnDecl ctx i
addDecl decl
try
let decl ← ProofBelow.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"

72
tests/lean/run/inductive_pred.lean
View file

@ -2,6 +2,12 @@ namespace Ex
inductive LE : Nat → Nat → Prop
| refl : LE n n
| succ : LE n m → LE n m.succ
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
theorem LE.trans : LE m n → LE n o → LE m o := by
intro h1 h2
@ -17,6 +23,9 @@ inductive Even : Nat → Prop
| zero : Even 0
| 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
theorem Even.add : Even n → Even m → Even (n+m) := by
intro h1 h2
induction h2 with
@ -33,6 +42,9 @@ theorem mul_left_comm (n m o : Nat) : n * (m * o) = m * (n * o) := by
inductive Power2 : Nat → Prop
| base : Power2 1
| 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
theorem Power2.mul : Power2 n → Power2 m → Power2 (n*m) := by
intro h1 h2
@ -45,4 +57,64 @@ theorem Power2.mul : Power2 n → Power2 m → Power2 (n*m) := by
-- theorem Power2.mul' : Power2 n → Power2 m → Power2 (n*m)
-- | h1, base => by simp_all
-- | h1, ind h2 => mul_left_comm .. ▸ ind (mul' h1 h2)
inductive tm : Type :=
| C : Nat → tm
| P : tm → tm → tm
open tm
set_option hygiene false in
infixl:40 " ==> " => step
inductive step : tm → tm → Prop :=
| ST_PlusConstConst : ∀ n1 n2,
P (C n1) (C n2) ==> C (n1 + n2)
| ST_Plus1 : ∀ t1 t1' t2,
t1 ==> t1' →
P t1 t2 ==> P t1' t2
| ST_Plus2 : ∀ n1 t2 t2',
t2 ==> t2' →
P (C n1) t2 ==> P (C n1) t2'
def deterministic {X : Type} (R : X → X → Prop) :=
∀ x y1 y2 : X, R x y1 → R x y2 → y1 = y2
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₁
) y₂ hy₂
section NestedRecursion
axiom f : Nat → Nat
inductive is_nat : Nat -> Prop
| Z : is_nat 0
| S {n} : is_nat n → is_nat (f n)
axiom P : Nat → Prop
axiom F0 : P 0
axiom F1 : P (f 0)
axiom FS {n : Nat} : P n → P (f (f n))
-- we would like to write this
-- theorem foo : ∀ {n}, is_nat n → P n
-- | _, is_nat.Z => F0
-- | _, is_nat.S is_nat.Z => F1
-- | _, is_nat.S (@is_nat.S n h) => FS (foo h)
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
end NestedRecursion
end Ex