Add ProofMode.SynthInstance

src/Iris/ProofMode/Classes.lean

@@ -4,34 +4,32 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Lars König
 -/
 import Iris.BI
+import Iris.ProofMode.SynthInstance
 
 namespace Iris.ProofMode
 open Iris.BI
 
-/-
-The two type classes `AsEmpValid1` and `AsEmpValid2` are necessary since type class instance
-search is used in both directions in `as_emp_valid_1` and `as_emp_valid_2`. When type class
-instance search is supposed to generate `φ` based on `P`, `AsEmpValid1` is used, since `φ` is
-declared as an `outParam`. Consequently, if type class instance search is supposed to generate `P`,
-`AsEmpValid2` is used.
--/
-
-class AsEmpValid1 (φ : semiOutParam Prop) {PROP : Type _} (P : PROP) [BI PROP] where
-  as_emp_valid : φ ↔ ⊢ P
+/-- [InOut] is used to dynamically determine whether a type class
+parameter is an input or an output. This is important for classes that
+are used with multiple modings, e.g., IntoWand. Instances can match on
+the InOut parameter to avoid accidentially instantiating outputs if
+matching on an input was intended. -/
+inductive InOut where
+  | in
+  | out
 
-class AsEmpValid2 (φ : Prop) {PROP : outParam (Type _)} (P : outParam PROP) [BI PROP] where
-  as_emp_valid : φ ↔ ⊢ P
+inductive AsEmpValid.Direction where
+  | into
+  | from
 
-def AsEmpValid1.to2 {φ : Prop} {PROP : Type _} {P : PROP} [BI PROP]
-    [AsEmpValid1 φ P] : AsEmpValid2 φ P := ⟨AsEmpValid1.as_emp_valid⟩
+@[ipm_class]
+class AsEmpValid (d : AsEmpValid.Direction) (φ : Prop) {PROP : outParam (Type _)} (P : outParam PROP) [BI PROP] where
+  as_emp_valid : (d = .into → φ → ⊢ P) ∧ (d = .from → (⊢ P) → φ)
 
-def AsEmpValid2.to1 {φ : Prop} {PROP : Type _} {P : PROP} [BI PROP]
-    [AsEmpValid2 φ P] : AsEmpValid1 φ P := ⟨AsEmpValid2.as_emp_valid⟩
-
-theorem as_emp_valid_1 [BI PROP] (P : PROP) [AsEmpValid1 φ P] : φ → ⊢ P :=
-  AsEmpValid1.as_emp_valid.mp
-theorem as_emp_valid_2 [BI PROP] (φ : Prop) [AsEmpValid2 φ (P : PROP)] : (⊢ P) → φ :=
-  AsEmpValid2.as_emp_valid.mpr
+theorem asEmpValid_1 [BI PROP] (P : PROP) [AsEmpValid .into φ P] : φ → ⊢ P :=
+  AsEmpValid.as_emp_valid.1 rfl
+theorem asEmpValid_2 [BI PROP] (φ : Prop) [AsEmpValid .from φ (P : PROP)] : (⊢ P) → φ :=
+  AsEmpValid.as_emp_valid.2 rfl
 
 
 /- Depending on the use case, type classes with the prefix `From` or `Into` are used. Type classes
@@ -40,84 +38,101 @@ proposition can be derived. Type classes with the prefix `Into` are used to gene
 *into* which the original proposition can be turned by derivation. Additional boolean flags are
 used to indicate that certain propositions should be intuitionistic. -/
 
-class IntoEmpValid (φ : Prop) {PROP : outParam (Type _)} (P : outParam PROP) [BI PROP] where
-  into_emp_valid : φ → ⊢ P
-export IntoEmpValid (into_emp_valid)
-
+@[ipm_class]
 class FromImp [BI PROP] (P : PROP) (Q1 Q2 : outParam PROP) where
   from_imp : (Q1 → Q2) ⊢ P
 export FromImp (from_imp)
 
+@[ipm_class]
 class FromWand [BI PROP] (P : PROP) (Q1 Q2 : outParam PROP) where
   from_wand : (Q1 -∗ Q2) ⊢ P
 export FromWand (from_wand)
 
-class IntoWand [BI PROP] (p q : Bool) (R : PROP) (P Q : outParam PROP) where
+@[ipm_class]
+class IntoWand [BI PROP] (p q : Bool) (R : PROP)
+  (ioP : InOut) (P : semiOutParam PROP)
+  (ioQ : InOut) (Q : semiOutParam PROP) where
   into_wand : □?p R ⊢ □?q P -∗ Q
 export IntoWand (into_wand)
 
+@[ipm_class]
 class FromForall [BI PROP] (P : PROP) {α : outParam (Sort _)} (Ψ : outParam <| α → PROP) where
   from_forall : (∀ x, Ψ x) ⊢ P
 export FromForall (from_forall)
 
+@[ipm_class]
 class IntoForall [BI PROP] (P : PROP) {α : outParam (Sort _)} (Φ : outParam <| α → PROP) where
   into_forall : P ⊢ ∀ x, Φ x
 export IntoForall (into_forall)
 
+@[ipm_class]
 class FromExists [BI PROP] (P : PROP) {α : outParam (Sort _)} (Φ : outParam <| α → PROP) where
   from_exists : (∃ x, Φ x) ⊢ P
 export FromExists (from_exists)
 
+@[ipm_class]
 class IntoExists [BI PROP] (P : PROP) {α : outParam (Sort _)} (Φ : outParam <| α → PROP) where
   into_exists : P ⊢ ∃ x, Φ x
 export IntoExists (into_exists)
 
+@[ipm_class]
 class FromAnd [BI PROP] (P : PROP) (Q1 Q2 : outParam PROP) where
   from_and : Q1 ∧ Q2 ⊢ P
 export FromAnd (from_and)
 
+@[ipm_class]
 class IntoAnd (p : Bool) [BI PROP] (P : PROP) (Q1 Q2 : outParam PROP) where
   into_and : □?p P ⊢ □?p (Q1 ∧ Q2)
 export IntoAnd (into_and)
 
+@[ipm_class]
 class FromSep [BI PROP] (P : PROP) (Q1 Q2 : outParam PROP) where
   from_sep : Q1 ∗ Q2 ⊢ P
 export FromSep (from_sep)
 
+@[ipm_class]
 class IntoSep [BI PROP] (P : PROP) (Q1 Q2 : outParam PROP) where
   into_sep : P ⊢ Q1 ∗ Q2
 export IntoSep (into_sep)
 
+@[ipm_class]
 class FromOr [BI PROP] (P : PROP) (Q1 Q2 : outParam PROP) where
   from_or : Q1 ∨ Q2 ⊢ P
 export FromOr (from_or)
 
+@[ipm_class]
 class IntoOr [BI PROP] (P : PROP) (Q1 Q2 : outParam PROP) where
   into_or : P ⊢ Q1 ∨ Q2
 export IntoOr (into_or)
 
 
+@[ipm_class]
 class IntoPersistently (p : Bool) [BI PROP] (P : PROP) (Q : outParam PROP) where
   into_persistently : <pers>?p P ⊢ <pers> Q
 export IntoPersistently (into_persistently)
 
+@[ipm_class]
 class FromAffinely [BI PROP] (P : outParam PROP) (Q : PROP) (p : Bool := true) where
   from_affinely : <affine>?p Q ⊢ P
 export FromAffinely (from_affinely)
 
+@[ipm_class]
 class IntoAbsorbingly [BI PROP] (P : outParam PROP) (Q : PROP) where
   into_absorbingly : P ⊢ <absorb> Q
 export IntoAbsorbingly (into_absorbingly)
 
 
-class FromAssumption (p : Bool) [BI PROP] (P : semiOutParam PROP) (Q : PROP) where
+@[ipm_class]
+class FromAssumption (p : Bool) [BI PROP] (ioP : InOut) (P : semiOutParam PROP) (Q : PROP) where
   from_assumption : □?p P ⊢ Q
 export FromAssumption (from_assumption)
 
+@[ipm_class]
 class IntoPure [BI PROP] (P : PROP) (φ : outParam Prop) where
   into_pure : P ⊢ ⌜φ⌝
 export IntoPure (into_pure)
 
+@[ipm_class]
 class FromPure [BI PROP] (a : outParam Bool) (P : PROP) (φ : outParam Prop) where
   from_pure : <affine>?a ⌜φ⌝ ⊢ P
 export FromPure (from_pure)

src/Iris/ProofMode/Goals.lean

@@ -0,0 +1,43 @@
+/-
+Copyright (c) 2025 Michael Sammler. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Michael Sammler
+-/
+import Iris.ProofMode.Expr
+
+namespace Iris.ProofMode
+open Lean Elab Tactic Meta Qq BI Std
+
+structure Goals {prop : Q(Type u)} (bi : Q(BI $prop)) where
+  goals : IO.Ref (Array MVarId)
+
+def Goals.new {prop : Q(Type u)} (bi : Q(BI $prop)) : BaseIO (Goals bi) :=
+  do return {goals := ← IO.mkRef #[]}
+
+def Goals.addGoal {prop : Q(Type u)} {bi : Q(BI $prop)} (g : Goals bi)
+    {e} (hyps : Hyps bi e) (goal : Q($prop)) (name : Name := .anonymous) : MetaM Q($e ⊢ $goal) := do
+  let m : Q($e ⊢ $goal) ← mkFreshExprSyntheticOpaqueMVar <|
+    IrisGoal.toExpr { prop, bi, hyps, goal, .. }
+  m.mvarId!.setUserName name
+  g.goals.modify (·.push m.mvarId!)
+  pure m
+
+def Goals.addPureGoal {prop : Q(Type u)} {bi : Q(BI $prop)} (g : Goals bi)
+    (m : MVarId) (name : Name := .anonymous) : MetaM Unit := do
+  if ← m.isAssignedOrDelayedAssigned then
+    return
+  if (← g.goals.get).contains m then
+    return
+  -- don't override an existing name, e.g. for ?_
+  if !name.isAnonymous then
+    m.setUserName name
+  g.goals.modify (·.push m)
+
+-- TODO: change this to replace main goal that deduplicates goals
+def Goals.getGoals {prop : Q(Type u)} {bi : Q(BI $prop)} (g : Goals bi) : MetaM (List MVarId) := do
+  let goals ← g.goals.get
+  -- put the goals that depend on other goals last
+  let mvars ← goals.foldlM (λ m g => do
+    return m ∪ (← g.getMVarDependencies)) ∅
+  let (dep, nonDep) := goals.partition (λ x => mvars.contains x)
+  return (nonDep ++ dep).toList