Partial proof for bang_valid_of_allQuest

Cslib/Logics/LinearLogic/CLL/Basic.lean

@@ -92,6 +92,15 @@ def Proposition.negative : Proposition Atom → Bool
   | quest _ => true
   | _ => false
 
+/--
+Whether a proposition is in the multiplicative-additive fragment (MALL), i.e. it
+contains no exponentials.
+-/
+def Proposition.IsMALL : Proposition Atom → Prop
+  | .atom _ | .atomDual _ | .one | .bot | .top | .zero => True
+  | .tensor a b | .parr a b | .oplus a b | .with a b => a.IsMALL ∧ b.IsMALL
+  | .bang _ | .quest _ => False
+
 /-- Whether a `Proposition` is positive is decidable. -/
 instance Proposition.positive_decidable (a : Proposition Atom) : Decidable a.positive :=
   a.positive.decEq true
@@ -151,6 +160,10 @@ def Proposition.linImpl (a b : Proposition Atom) : Proposition Atom := a⫠ ⅋
 /-- A sequent in CLL is a multiset of propositions. -/
 abbrev Sequent Atom := Multiset (Proposition Atom)
 
+/-- A sequent is MALL if every proposition in it is MALL. -/
+def Sequent.IsMALL (Γ : Sequent Atom) : Prop :=
+  ∀ A ∈ Γ, (A : Proposition Atom).IsMALL
+
 /-- Checks that all propositions in a sequent `Γ` are question marks. -/
 def Sequent.allQuest (Γ : Sequent Atom) :=
   Γ.map (· matches ʔ_)

Cslib/Logics/LinearLogic/CLL/PhaseSemantics/Basic.lean

@@ -332,8 +332,8 @@ instance : Min (Fact P) where
 /-- The idempotent elements within a given set X. -/
 def idempotentsIn [Monoid M] (X : Set M) : Set M := {m | IsIdempotentElem m ∧ m ∈ X}
 
-/-- The set I of idempotents that "belong to 1" in the phase semantics. -/
-def I : Set P := idempotentsIn (1 : Set P)
+/-- The set I of idempotents in the fact `1` (i.e., in `⊥⫠`). -/
+def I : Set P := idempotentsIn (↑(1 : Fact P))
 
 /-! ## Interpretation of the connectives -/
 
@@ -459,6 +459,10 @@ lemma par_le_par {G H K L : Fact P} (hGK : G ≤ K) (hHL : H ≤ L) : (G ⅋ H)
 
 lemma par_comm (G H : Fact P) : (G ⅋ H) = (H ⅋ G) := by simp [par_of_tensor, tensor_comm]
 
+instance : Std.Commutative (α := Fact P) (· ⅋ ·) := ⟨par_comm⟩
+
+instance : Std.Associative (α := Fact P) (· ⅋ ·) := ⟨fun _ _ _ => par_assoc⟩
+
 /--
 Linear implication between facts,
 defined as the dual of the orthogonal of the pointwise product.