Try to not even get unwanted hyps into the context, using mvarId.intro1_

Author: nomeata

src/Lean/Meta/Match/CaseValues.lean

@@ -12,20 +12,14 @@ import Lean.Meta.Tactic.Subst
 
 namespace Lean.Meta
 
-structure CaseValueSubgoal where
-  mvarId : MVarId
-  newH   : FVarId
-  deriving Inhabited
-
 /--
-  Split goal `... |- C x` into two subgoals
-  `..., (h : x = value)  |- C x`
-  `..., (h : x != value) |- C x`
-  where `fvarId` is `x`s id.
+  Split goal `... |- C x`,, where `fvarId` is `x`s id, into two subgoals
+  `..., |- (h : x = value)  → C x`
+  `..., |- (h : x != value) → C x`
   The type of `x` must have decidable equality.
  -/
 def caseValue (mvarId : MVarId) (fvarId : FVarId) (value : Expr) (hName : Name := `h)
-    : MetaM (CaseValueSubgoal × CaseValueSubgoal) :=
+    : MetaM (MVarId × MVarId) :=
   mvarId.withContext do
     let tag ← mvarId.getTag
     mvarId.checkNotAssigned `caseValue
@@ -38,15 +32,7 @@ def caseValue (mvarId : MVarId) (fvarId : FVarId) (value : Expr) (hName : Name :
     let elseMVar ← mkFreshExprSyntheticOpaqueMVar elseTarget tag
     let val ← mkAppOptM `dite #[none, xEqValue, none, thenMVar, elseMVar]
     mvarId.assign val
-    let (elseH, elseMVarId) ← elseMVar.mvarId!.intro1P
-    let elseSubgoal := { mvarId := elseMVarId, newH := elseH }
-    let (thenH, thenMVarId) ← thenMVar.mvarId!.intro1P
-    thenMVarId.withContext do
-      trace[Meta] "searching for decl"
-      let _ ← thenH.getDecl
-      trace[Meta] "found decl"
-    let thenSubgoal := { mvarId := thenMVarId, newH := thenH }
-    pure (thenSubgoal, elseSubgoal)
+    return (thenMVar.mvarId!, elseMVar.mvarId!)
 
 public structure CaseValuesSubgoal where
   mvarId : MVarId
@@ -55,41 +41,43 @@ public structure CaseValuesSubgoal where
   deriving Inhabited
 
 /--
-  Split goal `... |- C x` into values.size + 1 subgoals
-  1) `..., (h_1 : x = value[0])  |- C value[0]`
+  Split goal `... |- C x`, where `fvarId` is `x`s id, into `values.size + 1` subgoals
+  1)   `..., (h_1 : x = value[0])      |- C value[0]`
   ...
-  n) `..., (h_n : x = value[n - 1])  |- C value[n - 1]`
+  n)   `..., (h_n : x = value[n - 1])  |- C value[n - 1]`
   n+1) `..., (h_1 : x != value[0]) ... (h_n : x != value[n-1]) |- C x`
   where `n = values.size`
-  where `fvarId` is `x`s id.
   The type of `x` must have decidable equality.
 
   Remark: the last subgoal is for the "else" catchall case, and its `subst` is `{}`.
   Remark: the field `newHs` has size 1 forall but the last subgoal.
 
-  If `needsHyps = false` then the else case has the hypotheses cleared.
+  If `needsHyps = false` then the else case comes without hypotheses.
 -/
 public def caseValues (mvarId : MVarId) (fvarId : FVarId) (values : Array Expr) (hNamePrefix := `h)
     (needHyps := true) : MetaM (Array CaseValuesSubgoal) :=
   let rec loop : Nat → MVarId → List Expr → Array FVarId → Array CaseValuesSubgoal → MetaM (Array CaseValuesSubgoal)
     | _, mvarId, [],    _,  _        => throwTacticEx `caseValues mvarId "list of values must not be empty"
     | i, mvarId, v::vs, hs, subgoals => do
-      let (thenSubgoal, elseSubgoal) ← caseValue mvarId fvarId v (hNamePrefix.appendIndexAfter i)
-      appendTagSuffix thenSubgoal.mvarId ((`case).appendIndexAfter i)
-      let thenMVarId ← thenSubgoal.mvarId.tryClearMany  hs
-      let (subst, mvarId) ← substCore thenMVarId thenSubgoal.newH (symm := false) {} (clearH := true)
-      let subgoals := subgoals.push { mvarId := mvarId, newHs := #[], subst := subst }
+      let (thenMVarId, elseMVarId) ← caseValue mvarId fvarId v (hNamePrefix.appendIndexAfter i)
+      appendTagSuffix thenMVarId ((`case).appendIndexAfter i)
+      let thenMVarId ← thenMVarId.tryClearMany hs
+      let (thenH, thenMVarId) ← thenMVarId.intro1P
+      let (subst, thenMVarId) ← substCore thenMVarId thenH (symm := false) {} (clearH := true)
+      let subgoals := subgoals.push { mvarId := thenMVarId, newHs := #[], subst := subst }
+      let (hs', elseMVarId) ←
+        if needHyps then
+          let (elseH, elseMVarId) ← elseMVarId.intro1P
+          pure (hs.push elseH, elseMVarId)
+        else
+          let elseMVarId ← elseMVarId.intro1_
+          pure (hs, elseMVarId)
       match vs with
       | [] => do
-        appendTagSuffix elseSubgoal.mvarId ((`case).appendIndexAfter (i+1))
-        pure $ subgoals.push { mvarId := elseSubgoal.mvarId, newHs := hs.push elseSubgoal.newH, subst := {} }
+        appendTagSuffix elseMVarId ((`case).appendIndexAfter (i+1))
+        pure $ subgoals.push { mvarId := elseMVarId, newHs := hs', subst := {} }
       | vs =>
-        let (mvarId', hs') ←
-          if needHyps then
-            pure (elseSubgoal.mvarId, hs.push elseSubgoal.newH)
-          else
-            pure (← elseSubgoal.mvarId.tryClear elseSubgoal.newH, hs)
-        loop (i+1) mvarId' vs hs' subgoals
+        loop (i+1) elseMVarId vs hs' subgoals
 
   loop 1 mvarId values.toList #[] #[]
 

src/Lean/Meta/Tactic/Intro.lean

@@ -161,6 +161,23 @@ does not start with a forall, lambda or let. -/
 abbrev _root_.Lean.MVarId.intro1P (mvarId : MVarId) : MetaM (FVarId × MVarId) :=
   intro1Core mvarId true
 
+/--
+Given a goal `... |- β → α`, returns a goal `... ⊢ α`.
+Like `intro h; clear h`, but without ever appending to the local context.
+-/
+def _root_.Lean.MVarId.intro1_ (mvarId : MVarId) : MetaM MVarId := do
+  mvarId.withContext do
+    let target ← mvarId.getType'
+    match target with
+    | .forallE n β α bi =>
+      if α.hasLooseBVars then
+        throwError "intro1_: expected arrow type\n{mvarId}"
+      let tag ← mvarId.getTag
+      let newMVar ← mkFreshExprSyntheticOpaqueMVar α tag
+      mvarId.assign (.lam n β newMVar bi)
+      return newMVar.mvarId!
+    | _ => throwError "intro1_: expected arrow type\n{mvarId}"
+
 /--
 Calculate the number of new hypotheses that would be created by `intros`,
 i.e. the number of binders which can be introduced without unfolding definitions.