feat: add intro and assumption

src/Init/Lean/Meta.lean

@@ -16,3 +16,4 @@ import Init.Lean.Meta.Instances
 import Init.Lean.Meta.AbstractMVars
 import Init.Lean.Meta.SynthInstance
 import Init.Lean.Meta.AppBuilder
+import Init.Lean.Meta.Tactic

src/Init/Lean/Meta/Tactic.lean

@@ -0,0 +1,8 @@
+/-
+Copyright (c) 2019 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura
+-/
+prelude
+import Init.Lean.Meta.Tactic.Intro
+import Init.Lean.Meta.Tactic.Assumption

src/Init/Lean/Meta/Tactic/Assumption.lean

@@ -0,0 +1,27 @@
+/-
+Copyright (c) 2019 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura
+-/
+prelude
+import Init.Lean.Meta.ExprDefEq
+import Init.Lean.Meta.Tactic.Util
+
+namespace Lean
+namespace Meta
+
+def assumptionAux (mvarId : MVarId) : MetaM Bool :=
+withMVarContext mvarId $ do
+  checkNotAssigned mvarId "assumption";
+  mvarType ← getMVarType mvarId;
+  lctx ← getLCtx;
+  h? ← lctx.findDeclRevM $ fun decl => condM (isDefEq mvarType decl.type) (pure (some decl.toExpr)) (pure none);
+  match h? with
+  | some h => do assignExprMVar mvarId h; pure true
+  | none   => pure false
+
+def assumption (mvarId : MVarId) : MetaM Unit :=
+unlessM (assumptionAux mvarId) $ throw $ Exception.other "`assumption` failed"
+
+end Meta
+end Lean

src/Init/Lean/Meta/Tactic/Intro.lean

@@ -0,0 +1,73 @@
+/-
+Copyright (c) 2019 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura
+-/
+prelude
+import Init.Lean.Meta.Tactic.Util
+
+namespace Lean
+namespace Meta
+
+@[specialize]
+def introNCoreAux {σ} (mvarId : MVarId) (mkName : LocalContext → Name → σ → Name × σ)
+    : Nat → LocalContext → Array Expr → Nat → σ → Expr → MetaM (Array Expr × MVarId)
+| 0, lctx, fvars, j, _, type =>
+  let type := type.instantiateRevRange j fvars.size fvars;
+  adaptReader (fun (ctx : Context) => { lctx := lctx, .. ctx }) $
+    withNewLocalInstances isClassExpensive fvars j $ do
+      newMVar ← mkFreshExprSyntheticMVar type;
+      lctx    ← getLCtx;
+      modify $ fun s => { mctx := s.mctx.assignDelayed mvarId lctx fvars newMVar, .. s };
+      pure $ (fvars, newMVar.mvarId!)
+| (i+1), lctx, fvars, j, s, Expr.letE n type val body _ => do
+  let type   := type.instantiateRevRange j fvars.size fvars;
+  let val    := val.instantiateRevRange j fvars.size fvars;
+  fvarId ← mkFreshId;
+  let (n, s) := mkName lctx n s;
+  let lctx   := lctx.mkLetDecl fvarId n type val;
+  let fvar   := mkFVar fvarId;
+  let fvars  := fvars.push fvar;
+  introNCoreAux i lctx fvars j s body
+| (i+1), lctx, fvars, j, s, Expr.forallE n type body c => do
+  let type   := type.instantiateRevRange j fvars.size fvars;
+  fvarId ← mkFreshId;
+  let (n, s) := mkName lctx n s;
+  let lctx   := lctx.mkLocalDecl fvarId n type c.binderInfo;
+  let fvar   := mkFVar fvarId;
+  let fvars  := fvars.push fvar;
+  introNCoreAux i lctx fvars j s body
+| (i+1), lctx, fvars, j, s, type =>
+  let type := type.instantiateRevRange j fvars.size fvars;
+  adaptReader (fun (ctx : Context) => { lctx := lctx, .. ctx }) $
+    withNewLocalInstances isClassExpensive fvars j $ do
+      newType ← whnf type;
+      if newType.isForall then
+        introNCoreAux i lctx fvars fvars.size s newType
+      else
+        throw $ Exception.other "`introN` failed insufficient number of binders"
+
+@[specialize] def introNCore {σ} (mvarId : MVarId) (n : Nat) (mkName : LocalContext → Name → σ → Name × σ) (s : σ) : MetaM (Array Expr × MVarId) :=
+withMVarContext mvarId $ do
+  checkNotAssigned mvarId "introN";
+  mvarType ← getMVarType mvarId;
+  lctx ← getLCtx;
+  introNCoreAux mvarId mkName n lctx #[] 0 s mvarType
+
+def mkAuxName (lctx : LocalContext) (defaultName : Name) : List Name → Name × List Name
+| []         => (lctx.getUnusedName defaultName, [])
+| n :: rest  => (if n == "_" then lctx.getUnusedName defaultName else n, rest)
+
+def introN (mvarId : MVarId) (n : Nat) (givenNames : List Name := []) : MetaM (Array Expr × MVarId) :=
+introNCore mvarId n mkAuxName givenNames
+
+def intro (mvarId : MVarId) (name : Name) : MetaM (Expr × MVarId) :=
+do (fvars, mvarid) ← introN mvarId 1 [name];
+   pure (fvars.get! 0, mvarId)
+
+def intro1 (mvarId : MVarId) : MetaM (Expr × MVarId) :=
+do (fvars, mvarid) ← introN mvarId 1 [];
+   pure (fvars.get! 0, mvarId)
+
+end Meta
+end Lean

src/Init/Lean/Meta/Tactic/Util.lean

@@ -0,0 +1,27 @@
+/-
+Copyright (c) 2019 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura
+-/
+prelude
+import Init.Lean.Meta.Basic
+
+namespace Lean
+namespace Meta
+
+def mkFreshExprSyntheticMVar (type : Expr) (userName : Name := Name.anonymous) : MetaM Expr :=
+mkFreshExprMVar type userName true
+
+def checkNotAssigned (mvarId : MVarId) (tacticName : String) : MetaM Unit :=
+whenM (isExprMVarAssigned mvarId) $
+  throw $ Exception.other ("`" ++ tacticName ++ "` failed, metavariable has already been assigned")
+
+def getMVarType (mvarId : MVarId) : MetaM Expr :=
+do mvarDecl ← getMVarDecl mvarId;
+   pure mvarDecl.type
+
+@[init] private def regTraceClasses : IO Unit :=
+registerTraceClass `Meta.Tactic
+
+end Meta
+end Lean

tests/lean/run/tactic.lean

@@ -0,0 +1,21 @@
+import Init.Lean.Meta
+open Lean
+open Lean.Meta
+
+axiom simple : forall {p q : Prop}, p → q → p
+
+def print (msg : MessageData) : MetaM Unit :=
+trace! `Meta.Tactic msg
+
+set_option trace.Meta.Tactic true
+
+def tst1 : MetaM Unit :=
+do cinfo ← getConstInfo `simple;
+   mvar  ← mkFreshExprSyntheticMVar cinfo.type;
+   let mvarId := mvar.mvarId!;
+   (_, mvarId) ← introN mvarId 4;
+   assumption mvarId;
+   result ← instantiateMVars mvar;
+   print result
+
+#eval tst1