From 7dc6721fea48099af2049ae2dfdde35ecc94c7d2 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Tue, 16 Mar 2021 16:41:57 -0700
Subject: [PATCH] fix: missing `pushScope` and `popScope`

---
 src/Lean/Elab/Tactic/Basic.lean    | 10 +++++++---
 src/Lean/Elab/Term.lean            | 10 +++++++---
 src/Lean/ScopedEnvExtension.lean   |  2 +-
 tests/lean/run/openInScopeBug.lean | 32 ++++++++++++++++++++++++++++++
 4 files changed, 47 insertions(+), 7 deletions(-)
 create mode 100644 tests/lean/run/openInScopeBug.lean

diff --git a/src/Lean/Elab/Tactic/Basic.lean b/src/Lean/Elab/Tactic/Basic.lean
index 6ee14b499b..989cdbd26f 100644
--- a/src/Lean/Elab/Tactic/Basic.lean
+++ b/src/Lean/Elab/Tactic/Basic.lean
@@ -328,9 +328,13 @@ private def getOptRotation (stx : Syntax) : Nat :=
   setGoals <| (← getGoals).rotateRight n
 
 @[builtinTactic Parser.Tactic.open] def evalOpen : Tactic := fun stx => do
-  let openDecls ← elabOpenDecl stx[1]
-  withTheReader Core.Context (fun ctx => { ctx with openDecls := openDecls }) do
-    evalTactic stx[3]
+  try
+    pushScope
+    let openDecls ← elabOpenDecl stx[1]
+    withTheReader Core.Context (fun ctx => { ctx with openDecls := openDecls }) do
+      evalTactic stx[3]
+  finally
+    popScope
 
 @[builtinTactic Parser.Tactic.set_option] def elabSetOption : Tactic := fun stx => do
   let options ← Elab.elabSetOption stx[1] stx[2]
diff --git a/src/Lean/Elab/Term.lean b/src/Lean/Elab/Term.lean
index 4693e10853..5a5e980a5b 100644
--- a/src/Lean/Elab/Term.lean
+++ b/src/Lean/Elab/Term.lean
@@ -1421,9 +1421,13 @@ def elabScientificLit : TermElab := fun stx expectedType? => do
   | some msg => elabTermEnsuringType stx[2] expectedType? (errorMsgHeader? := msg)
 
 @[builtinTermElab «open»] def elabOpen : TermElab := fun stx expectedType? => do
-  let openDecls ← elabOpenDecl stx[1]
-  withTheReader Core.Context (fun ctx => { ctx with openDecls := openDecls }) do
-    elabTerm stx[3] expectedType?
+  try
+    pushScope
+    let openDecls ← elabOpenDecl stx[1]
+    withTheReader Core.Context (fun ctx => { ctx with openDecls := openDecls }) do
+      elabTerm stx[3] expectedType?
+  finally
+    popScope
 
 @[builtinTermElab «set_option»] def elabSetOption : TermElab := fun stx expectedType? => do
   let options ← Elab.elabSetOption stx[1] stx[2]
diff --git a/src/Lean/ScopedEnvExtension.lean b/src/Lean/ScopedEnvExtension.lean
index d61a492c74..e8387c5f5c 100644
--- a/src/Lean/ScopedEnvExtension.lean
+++ b/src/Lean/ScopedEnvExtension.lean
@@ -180,7 +180,7 @@ def ScopedEnvExtension.modifyState (ext : ScopedEnvExtension α β σ) (env : En
   let s := ext.ext.getState env
   match s.stateStack with
   | top :: stack => ext.ext.setState env { s with stateStack := { top with state := f top.state } :: stack }
-  | _ => env  
+  | _ => env
 
 def pushScope [Monad m] [MonadEnv m] [MonadLiftT (ST IO.RealWorld) m] : m Unit := do
   for ext in (← scopedEnvExtensionsRef.get) do
diff --git a/tests/lean/run/openInScopeBug.lean b/tests/lean/run/openInScopeBug.lean
new file mode 100644
index 0000000000..52f4fc5f73
--- /dev/null
+++ b/tests/lean/run/openInScopeBug.lean
@@ -0,0 +1,32 @@
+constant f : Nat → Nat
+constant g : Nat → Nat
+
+namespace Foo
+
+@[scoped simp] axiom ax1 (x : Nat) : f (g x) = x
+@[scoped simp] axiom ax2 (x : Nat) : g (g x) = g x
+
+end Foo
+
+theorem ex1 : f (g (g (g x))) = x := by
+  simp -- does not use ax1 and ax2
+  simp [Foo.ax1, Foo.ax2]
+
+theorem ex2 : f (g (g (g x))) = x :=
+  have h₁ : f (g (g (g x))) = f (g x) by simp; /- try again with `Foo` scoped lemmas -/ open Foo in simp
+  have h₂ : f (g x) = x               by simp; open Foo in simp
+  Eq.trans h₁ h₂
+  -- open Foo in simp -- works
+
+theorem ex3 : f (g (g (g x))) = x := by
+  simp
+  simp [Foo.ax1, Foo.ax2]
+
+open Foo in
+theorem ex4 : f (g (g (g x))) = x := by
+  simp
+
+theorem ex5 : f (g (g (g x))) = x ∧ f (g x) = x := by
+  apply And.intro
+  { simp; open Foo in simp }
+  { simp; open Foo in simp }