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

feat: add mkEqNDRec and mkEqRec

Browse source
This commit is contained in:
Leonardo de Moura 2020-02-09 11:02:35 -08:00
parent d8b69d4fe1
commit 95ad26cc23
2 changed files with 67 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

28
src/Init/Lean/Meta/AppBuilder.lean
View file

@ -168,5 +168,33 @@ traceCtx `Meta.appBuilder $ withNewMCtxDepth $ do
let fType := cinfo.instantiateTypeLevelParams us;
mkAppMAux f xs 0 #[] 0 #[] fType
def mkEqNDRec (motive h1 h2 : Expr) : MetaM Expr :=
if h2.isAppOf `Eq.refl then pure h1
else do
h2Type ← infer h2;
match h2Type.eq? with
| none => throwEx $ Exception.appBuilder `Eq.ndrec "equality proof expected" #[h2]
| some (α, a, b) => do
u2 ← getLevel α;
motiveType ← infer motive;
match motiveType with
| Expr.forallE _ _ (Expr.sort u1 _) _ =>
pure $ mkAppN (mkConst `Eq.ndrec [u1, u2]) #[α, a, motive, h1, b, h2]
| _ => throwEx $ Exception.appBuilder `Eq.ndrec "invalid motive" #[motive]
def mkEqRec (motive h1 h2 : Expr) : MetaM Expr :=
if h2.isAppOf `Eq.refl then pure h1
else do
h2Type ← infer h2;
match h2Type.eq? with
| none => throwEx $ Exception.appBuilder `Eq.rec "equality proof expected" #[h2]
| some (α, a, b) => do
u2 ← getLevel α;
motiveType ← infer motive;
match motiveType with
| Expr.forallE _ _ (Expr.forallE _ _ (Expr.sort u1 _) _) _ =>
pure $ mkAppN (mkConst `Eq.rec [u1, u2]) #[α, a, motive, h1, b, h2]
| _ => throwEx $ Exception.appBuilder `Eq.rec "invalid motive" #[motive]
end Meta
end Lean

40
tests/lean/run/meta2.lean
View file

@ -515,4 +515,42 @@ print t;
check $ isDefEq t m;
pure ()
#eval tst31
def tst32 : MetaM Unit := do
print "----- tst32 -----";
withLocalDecl `a nat BinderInfo.default $ fun a => do
withLocalDecl `b nat BinderInfo.default $ fun b => do
aeqb ← mkEq a b;
withLocalDecl `h2 aeqb BinderInfo.default $ fun h2 => do
t ← mkEq (mkApp2 add a a) a;
print t;
let motive := Lean.mkLambda `x BinderInfo.default nat (mkApp3 (mkConst `Eq [levelOne]) nat (mkApp2 add a (mkBVar 0)) a);
withLocalDecl `h1 t BinderInfo.default $ fun h1 => do
r ← mkEqNDRec motive h1 h2;
print r;
rType ← inferType r >>= whnf;
print rType;
check r;
pure ()
#eval tst32
def tst33 : MetaM Unit := do
print "----- tst33 -----";
withLocalDecl `a nat BinderInfo.default $ fun a => do
withLocalDecl `b nat BinderInfo.default $ fun b => do
aeqb ← mkEq a b;
withLocalDecl `h2 aeqb BinderInfo.default $ fun h2 => do
t ← mkEq (mkApp2 add a a) a;
let motive :=
Lean.mkLambda `x BinderInfo.default nat $
Lean.mkLambda `h BinderInfo.default (mkApp3 (mkConst `Eq [levelOne]) nat a (mkBVar 0)) $
(mkApp3 (mkConst `Eq [levelOne]) nat (mkApp2 add a (mkBVar 1)) a);
withLocalDecl `h1 t BinderInfo.default $ fun h1 => do
r ← mkEqRec motive h1 h2;
print r;
rType ← inferType r >>= whnf;
print rType;
check r;
pure ()
#eval tst33