From 95ad26cc23d116a03a2f7ed2a20ced5da5a7d898 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sun, 9 Feb 2020 11:02:35 -0800
Subject: [PATCH] feat: add `mkEqNDRec` and `mkEqRec`

---
 src/Init/Lean/Meta/AppBuilder.lean | 28 +++++++++++++++++++++
 tests/lean/run/meta2.lean          | 40 +++++++++++++++++++++++++++++-
 2 files changed, 67 insertions(+), 1 deletion(-)

diff --git a/src/Init/Lean/Meta/AppBuilder.lean b/src/Init/Lean/Meta/AppBuilder.lean
index dbe8b2dd30..11bf749986 100644
--- a/src/Init/Lean/Meta/AppBuilder.lean
+++ b/src/Init/Lean/Meta/AppBuilder.lean
@@ -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
diff --git a/tests/lean/run/meta2.lean b/tests/lean/run/meta2.lean
index cc6fda69fa..843f5a070a 100644
--- a/tests/lean/run/meta2.lean
+++ b/tests/lean/run/meta2.lean
@@ -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