feat: add subst tactic

src/Init/Lean/Elab/Tactic/Basic.lean

@@ -9,6 +9,7 @@ import Init.Lean.Meta.Tactic.Assumption
 import Init.Lean.Meta.Tactic.Intro
 import Init.Lean.Meta.Tactic.Clear
 import Init.Lean.Meta.Tactic.Revert
+import Init.Lean.Meta.Tactic.Subst
 import Init.Lean.Elab.Util
 import Init.Lean.Elab.Term
 
@@ -346,18 +347,25 @@ fun stx => match_syntax stx with
        setGoals (g :: gs)
   | _                     => throwUnsupportedSyntax
 
+def forEachVar (ref : Syntax) (hs : Array Syntax) (tac : MVarId → FVarId → MetaM MVarId) : TacticM Unit :=
+hs.forM $ fun h => do
+  (g, gs) ← getMainGoal ref;
+  withMVarContext g $ do
+    fvar? ← liftTermElabM $ Term.isLocalTermId? h true;
+    match fvar? with
+    | none      => throwError h ("unknown variable '" ++ toString h.getId ++ "'")
+    | some fvar => do
+      g ← liftMetaM ref $ tac g fvar.fvarId!;
+      setGoals (g :: gs)
+
 @[builtinTactic «clear»] def evalClear : Tactic :=
 fun stx => match_syntax stx with
-  | `(tactic| clear $hs*) =>
-    hs.forM $ fun h => do
-      (g, gs) ← getMainGoal stx;
-      withMVarContext g $ do
-        fvar? ← liftTermElabM $ Term.isLocalTermId? h true;
-        match fvar? with
-        | none      => throwError h ("unknown variable '" ++ toString h.getId ++ "'")
-        | some fvar => do
-          g ← liftMetaM stx $ Meta.clear g fvar.fvarId!;
-          setGoals (g :: gs)
+  | `(tactic| clear $hs*) => forEachVar stx hs Meta.clear
+  | _                     => throwUnsupportedSyntax
+
+@[builtinTactic «subst»] def evalSubst : Tactic :=
+fun stx => match_syntax stx with
+  | `(tactic| subst $hs*) => forEachVar stx hs Meta.subst
   | _                     => throwUnsupportedSyntax
 
 @[builtinTactic paren] def evalParen : Tactic :=

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

@@ -0,0 +1,136 @@
+/-
+Copyright (c) 2020 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.AppBuilder
+import Init.Lean.Meta.Message
+import Init.Lean.Meta.Tactic.Util
+import Init.Lean.Meta.Tactic.Revert
+import Init.Lean.Meta.Tactic.Intro
+import Init.Lean.Meta.Tactic.Clear
+import Init.Lean.Meta.Tactic.FVarSubst
+
+namespace Lean
+namespace Meta
+
+def substCore (mvarId : MVarId) (hFVarId : FVarId) (symm := false) (genFVarSubst := false) : MetaM (FVarSubst × MVarId) :=
+withMVarContext mvarId $ do
+  tag     ← getMVarTag mvarId;
+  checkNotAssigned mvarId `subst;
+  hLocalDecl ← getLocalDecl hFVarId;
+  match hLocalDecl.type.eq? with
+  | none => throwTacticEx `subst mvarId "argument must be an equality proof"
+  | some (α, lhs, rhs) =>
+    let a := if symm then rhs else lhs;
+    let b := if symm then lhs else rhs;
+    match a with
+    | Expr.fvar aFVarId _ => do
+      mctx ← getMCtx;
+      when (mctx.exprDependsOn b aFVarId) $
+        throwTacticEx `subst mvarId ("occurs check failed '" ++ a ++ "' occurs at" ++ indentExpr b);
+      aLocalDecl ← getLocalDecl aFVarId;
+      (vars, mvarId) ← revert mvarId #[aFVarId, hFVarId] true;
+      trace `Meta.Tactic.subst $ fun _ => "revert" ++ Format.line ++ MessageData.ofGoal mvarId;
+      (twoVars, mvarId) ← introN mvarId 2 [] false;
+      trace `Meta.Tactic.subst $ fun _ => "intro2" ++ Format.line ++ MessageData.ofGoal mvarId;
+      let aFVarId := twoVars.get! 0;
+      let a       := mkFVar aFVarId;
+      let hFVarId := twoVars.get! 1;
+      let h       := mkFVar hFVarId;
+      withMVarContext mvarId $ do
+        mvarDecl   ← getMVarDecl mvarId;
+        let type   := mvarDecl.type;
+        hLocalDecl ← getLocalDecl hFVarId;
+        match hLocalDecl.type.eq? with
+        | none => unreachable!
+        | some (α, lhs, rhs) => do
+          let b       := if symm then lhs else rhs;
+          mctx        ← getMCtx;
+          let depElim := mctx.exprDependsOn mvarDecl.type hFVarId;
+          let continue (motive : Expr) (newType : Expr) : MetaM (FVarSubst × MVarId) := do {
+            major   ← if symm then pure h else mkEqSymm h;
+            newMVar ← mkFreshExprSyntheticOpaqueMVar newType tag;
+            let minor := newMVar;
+            newVal  ← if depElim then mkEqRec motive minor major else mkEqNDRec motive minor major;
+            modify $ fun s => { mctx := s.mctx.assignExpr mvarId newVal, .. s };
+            let mvarId := newMVar.mvarId!;
+            trace `Meta.Tactic.subst $ fun _ => "subst" ++ Format.line ++ MessageData.ofGoal mvarId;
+            mvarId ← clear mvarId hFVarId;
+            mvarId ← clear mvarId aFVarId;
+            trace `Meta.Tactic.subst $ fun _ => "clear" ++ Format.line ++ MessageData.ofGoal mvarId;
+            (newFVars, mvarId) ← introN mvarId (vars.size - 2) [] false;
+            trace `Meta.Tactic.subst $ fun _ => "introN" ++ Format.line ++ MessageData.ofGoal mvarId;
+            fvarSubst ← pure {FVarSubst . }; -- TODO
+            pure (fvarSubst, mvarId)
+          };
+          if depElim then do
+            let newType := (type.abstract #[a]).instantiate1 b;
+            reflB ← mkEqRefl b;
+            let newType := (newType.abstract #[h]).instantiate1 reflB;
+            if symm then do
+              motive ← mkLambda #[a, h] type;
+              continue motive newType
+            else do
+              /- `type` depends on (h : a = b). So, we use the following trick to avoid a type incorrect motive.
+                 1- Create a new local (hAux : b = a)
+                 2- Create newType := type [hAux.symm / h]
+                    `newType` is type correct because `h` and `hAux.symm` are definitionally equal by proof irrelevance.
+                 3- Create motive by abstracting `a` and `hAux` in `newType`. -/
+              hAuxType ← mkEq b a;
+              (motive, newType) ← withLocalDecl `_h hAuxType BinderInfo.default $ fun hAux => do {
+                hAuxSymm ← mkEqSymm hAux;
+                /- replace h in type with hAuxSymm -/
+                let newType := (type.abstract #[h]).instantiate1 hAuxSymm;
+                motive ← mkLambda #[a, hAux] newType;
+                pure (motive, newType)
+              };
+              continue motive newType
+          else do
+            motive ← mkLambda #[a] type;
+            let newType := (type.abstract #[a]).instantiate1 b;
+            continue motive newType
+    | _ =>
+      throwTacticEx `subst mvarId $
+        "invalid equality proof, it is not of the form "
+        ++ (if symm then "(t = x)" else "(x = t)")
+        ++ indentExpr hLocalDecl.type
+
+def subst (mvarId : MVarId) (hFVarId : FVarId) : MetaM MVarId :=
+withMVarContext mvarId $ do
+  hLocalDecl ← getLocalDecl hFVarId;
+  match hLocalDecl.type.eq? with
+  | some (α, lhs, rhs) =>
+    if lhs.isFVar then
+      Prod.snd <$> substCore mvarId hFVarId
+    else if rhs.isFVar then
+      Prod.snd <$> substCore mvarId hFVarId true
+    else
+      throwTacticEx `subst mvarId $
+        "invalid equality proof, it is not of the form (x = t) or (t = x)"
+        ++ indentExpr hLocalDecl.type
+  | none => do
+    mctx ← getMCtx;
+    lctx ← getLCtx;
+    some (fvarId, symm) ← lctx.findDeclM?
+      (fun localDecl => match localDecl.type.eq? with
+       | some (α, Expr.fvar fvarId _, rhs) =>
+         if fvarId == hFVarId && !mctx.exprDependsOn rhs fvarId then
+           pure $ some (localDecl.fvarId, false)
+         else
+          pure none
+       | some (α, lhs, Expr.fvar fvarId _) =>
+         if fvarId == hFVarId && !mctx.exprDependsOn lhs fvarId then
+           pure $ some (localDecl.fvarId, true)
+         else
+           pure none
+       | _ => pure none)
+      | throwTacticEx `subst mvarId ("failed to find equation for eliminating '" ++ mkFVar hFVarId ++ "'");
+    Prod.snd <$> substCore mvarId fvarId symm
+
+@[init] private def regTraceClasses : IO Unit :=
+registerTraceClass `Meta.Tactic.subst
+
+end Meta
+end Lean