Add comments and introduce 'satisfies'

Author: GBathie

BoltLean/Basic.lean

@@ -1,28 +1,41 @@
-abbrev Valuation (n_var: Nat): Type := Vector Bool n_var
+/-- A valuation represents the membership of a given element `x` of the universe
+in each of the sets `S_1, ..., S_{n_sets}` of the instance.
+It is an alias for `Vector Bool n_sets`,
+and `v[i]` says whether `x` is in `S_i`.-/
+abbrev Valuation (n_sets: Nat): Type := Vector Bool n_sets
 
 /- Boolean formulas in NNF -/
-inductive BoolFormula (n_var: Nat)
-  | False: BoolFormula n_var
-  | True : BoolFormula n_var
-  | Var : Fin n_var -> (neg: Bool) -> BoolFormula n_var
-  | And : BoolFormula n_var -> BoolFormula n_var -> BoolFormula n_var
-  | Or : BoolFormula n_var -> BoolFormula n_var -> BoolFormula n_var
+inductive BoolFormula (n_sets: Nat)
+  | False: BoolFormula n_sets
+  | True : BoolFormula n_sets
+  | Var : Fin n_sets -> (neg: Bool) -> BoolFormula n_sets
+  | And : BoolFormula n_sets -> BoolFormula n_sets -> BoolFormula n_sets
+  | Or : BoolFormula n_sets -> BoolFormula n_sets -> BoolFormula n_sets
   deriving DecidableEq, Repr
 
 namespace BoolFormula
   @[simp]
-  def accepts (f: BoolFormula n_var) (v: Valuation n_var): Prop :=
+  def accepts (f: BoolFormula n_sets) (v: Valuation n_sets): Prop :=
     match f with
     | False => _root_.False
     | True => _root_.True
     | Var i neg => v[i] ^^ neg
     | And f1 f2 => f1.accepts v ∧ f2.accepts v
     | Or f1 f2 => f1.accepts v ∨ f2.accepts v
 
-  def dominates (f1 f2: BoolFormula n_var): Prop :=
-    ∀ (v: Valuation n_var), f2.accepts v → f1.accepts v
+  /-- A formula satisfies an examples if it is positive and the formula accepts,
+  or if it is negative and the formula rejects.-/
+  @[simp]
+  def satisfies (f: BoolFormula n_sets) (v: Valuation n_sets) (positive: Bool) : Prop :=
+    f.accepts v ↔ positive
+
+  /-- A formula `f1` dominates `f2` another if `f1` satisfies a superset
+  of the elements satisfied by `f2`.-/
+  def dominates (f1 f2: BoolFormula n_sets): Prop :=
+    ∀ (v: Valuation n_sets) (b: Bool), f2.satisfies v b → f1.satisfies v b
 
-  def replace (f pat repl: BoolFormula n_var): BoolFormula n_var :=
+  /-- Replace all occurrence of the formula `pat` in `f` with the formula `repl`.-/
+  def replace (f pat repl: BoolFormula n_sets): BoolFormula n_sets :=
     if f = pat then
       repl
     else match f with

BoltLean/Boolean/Basic.lean

@@ -1,21 +1,36 @@
 import BoltLean.Boolean.Basic
 
 namespace BoolFormula
-  theorem true_replace_accepts (f1 f2: BoolFormula n_var):
-    f1.dominates f2 -> ∀ (v: Valuation n_var), (True.replace f2 f1).accepts v := by
+  /-- Aux Lemma: `True` -/
+  theorem true_replace_accepts (f1 f2: BoolFormula n):
+    f1.dominates f2 -> ∀ (v: Valuation n), (True.replace f2 f1).accepts v := by
       intro h v
       simp [replace]
       split
       . next heq =>
           rw [←heq] at h
+          simp [dominates] at h
           apply h
-          simp
       . next hne => simp
 
+  /-- Aux Lemma: `False` -/
+  theorem false_replace_not_accepts (f1 f2: BoolFormula n):
+    f1.dominates f2 -> ∀ (v: Valuation n), ¬ (False.replace f2 f1).accepts v := by
+      intro h v
+      simp [replace]
+      split
+      . next heq =>
+          rw [←heq] at h
+          simp [dominates] at h
+          apply h
+      . next hne => simp
 
-  theorem var_replace_accepts (f1 f2: BoolFormula n_var) (i: Fin n_var) (neg: Bool):
-    f1.dominates f2 -> ∀ (v: Valuation n_var), (Var i neg).accepts v -> ((Var i neg).replace f2 f1).accepts v := by
-      intro h v hv
+  /-- Aux Lemma: `Var` -/
+  theorem var_replace_accepts (f1 f2: BoolFormula n) (i: Fin n) (neg: Bool):
+    f1.dominates f2 ->
+      ∀ (v: Valuation n) (b: Bool),
+        (Var i neg).satisfies v b -> ((Var i neg).replace f2 f1).satisfies v b := by
+      intro h v b hv
       simp [replace]
       split
       . next heq =>
@@ -24,41 +39,59 @@ namespace BoolFormula
           exact hv
       . next hne => assumption
 
-  theorem domin_replace (f1 f2: BoolFormula n_var):
+  /-- Theorem: if f1 dominates f2, then in any formula f,
+  replacing f2 by f1 yields a dominating formula.-/
+  theorem domin_replace (f1 f2: BoolFormula n):
     f1.dominates f2 →
-      ∀ (f: BoolFormula n_var), (f.replace f2 f1).dominates f := by
-      intro hd f v ha
+      ∀ (f: BoolFormula n), (f.replace f2 f1).dominates f := by
+      intro hd f v b ha
       induction f with
-      | True => exact true_replace_accepts f1 f2 hd v
-      | False => contradiction
+      | True =>
+        cases b with
+        | false => simp at ha
+        | true => simp; exact true_replace_accepts f1 f2 hd v
+      | False =>
+        cases b with
+        | false => simp [replace]; exact false_replace_not_accepts f1 f2 hd v
+        | true => simp at ha
       | Var i neg =>
         apply var_replace_accepts
           <;> assumption
       | And g1 g2 ih1 ih2 =>
         simp [replace]
         split
         . next heq =>
-          rw [←heq] at hd
-          apply hd v
-          assumption
+          apply hd
+          rw [heq] at ha
+          exact ha
         . next hne =>
-          simp
-          simp at ha
-          constructor
-          . exact ih1 ha.left
-          . exact ih2 ha.right
+          cases b with
+          | false =>
+            simp at *
+            intro h
+            by_cases hx: g1.accepts v
+            . exact ih2 (ha hx)
+            . have hc:= ih1 hx
+              contradiction
+          | true =>
+            simp at *
+            exact ⟨ih1 ha.left, ih2 ha.right⟩
       | Or g1 g2 ih1 ih2 =>
         simp [replace]
         split
         . next heq =>
-          rw [←heq] at hd
-          apply hd v
+          apply hd
+          rw [heq] at ha
           assumption
         . next hne =>
-          simp
-          simp at ha
-          match ha with
-          | .inl h1 => left; exact ih1 h1
-          | .inr h2 => right; exact ih2 h2
+          cases b with
+          | false =>
+            simp at *
+            exact ⟨ih1 ha.left, ih2 ha.right⟩
+          | true =>
+            simp at *
+            match ha with
+            | .inl h1 => left; exact ih1 h1
+            | .inr h2 => right; exact ih2 h2
 
 end BoolFormula

BoltLean/Boolean/Domination.lean

@@ -1,10 +1,13 @@
+/-- `Trace n_pred` is an alias for `List (Vector Bool n_pred)`.
+At position `i` in the list, the vector contains the truth value of the `n_pred` predicates at time `i`.-/
 abbrev Trace (n_pred: Nat): Type := List (Vector Bool n_pred)
 
 /-- LTL Formulas in NNF -/
 inductive Formula n_pred
   | True : Formula n_pred
   | False : Formula n_pred
-  | Var : Fin n_pred -> (neg: Bool) -> Formula n_pred -- neg: Whether the variable is negated
+  /-- neg: Whether the variable is negated -- negations are only allowed at variables. -/
+  | Var : Fin n_pred -> (neg: Bool) -> Formula n_pred
   | Next : Formula n_pred -> Formula n_pred
   | WeakNext : Formula n_pred -> Formula n_pred
   | Globally : Formula n_pred -> Formula n_pred
@@ -15,9 +18,11 @@ inductive Formula n_pred
 deriving DecidableEq
 
 namespace Formula
-
+  /-- Whether the formula is satisfied by the Trace.-/
   def accepts (phi: Formula n) (t: Trace n): Prop :=
   match t with
+    -- Special case of the empty Trace: it is only accepted by True and Globally,
+    -- or their boolean combinations.
     | .nil => match phi with
       | True | Globally _ => _root_.True
       | False | Finally _ | Var _ _ | Next _ | WeakNext _ | Until _ _ => _root_.False
@@ -37,6 +42,4 @@ namespace Formula
                                 (accepts psi2 (t.drop j)) ∧
                                 (∀ k, k < j → accepts psi1 (t.drop k))
 
-  def equivalence (phi psi : Formula n) : Prop := ∀ (t : Trace n), accepts phi t ↔ accepts psi t
-
 end Formula

BoltLean/Ltl/Basic.lean

@@ -1,14 +1,22 @@
 import BoltLean.Ltl.Basic
 
 namespace Trace
+  /-- Returns a formula that accepts the value of predicate number `v`,
+  at the given position,
+  i.e. it returns the variable x_v if x_v is true,
+  and ¬x_v otherwise. -/
   def get_exact_var (pos: Vector Bool n) (v: Fin n): Formula n :=
     Formula.Var v (not pos[v])
 
-  /-- Auxiliary function for constructing a formula that is true on t and only on t-/
+  /-- Construct a formula that accepts the value of all predicates listed in `l`
+  at the given position.
+  To build the `exact` function, this function is called with `List.finRange n`,
+  but having `l` as a free parameter makes proofs easier.-/
   def exact_at_pos (pos: Vector Bool n) (l: List (Fin n)): Formula n :=
     let all_var := l.map (get_exact_var pos)
-    all_var.foldr (fun phi psi => phi.And psi) Formula.True
+    all_var.foldr Formula.And Formula.True
 
+  /-- Return a formula that accepts `t` and rejects all other traces.-/
   def exact (t: Trace n) : Formula n :=
     match t with
     | .nil => Formula.False.Globally
@@ -41,9 +49,8 @@ namespace Trace
       . exact ih
 
   -- Soundness
-  /-- Taking the `And` of a list of formulas and evaluating is the same as
-  evaluating and taking the `And`.
-  -/
+  /-- Lemma: Taking the `And` of a list of formulas and evaluating is the same as
+  evaluating and taking the Boolean `And`.-/
   theorem foldr_and_aux (l: List (Formula n)) (t: Trace n):
     (l.foldr Formula.And Formula.True).accepts t
       → ∀ f ∈ l, f.accepts t := by
@@ -62,6 +69,7 @@ namespace Trace
             simp [*] at he
             cases t <;> simp at he <;> apply ih he.right f h_in
 
+  /-- Lemma: If `exact_at_pos pos l` accepts, then `get_exact_var pos v` also accepts for all `v ∈ l`-/
   theorem exact_at_pos_accepts_all (pos pos': Vector Bool n) (t: Trace n) (l: List (Fin n)) :
     (exact_at_pos pos l).accepts (pos' :: t) → ∀ v ∈ l, (get_exact_var pos v).accepts (pos' :: t) := by
       intro h v hv
@@ -83,6 +91,7 @@ namespace Trace
       apply h1
       exact h2
 
+  /-- Lemma: If `exact t` accepts `t'`, then `t` and `t'` have the same head.-/
   theorem exact_accepts_head (h h': Vector Bool n) (t t': Trace n):
     (exact (h::t)).accepts (h'::t') → h = h' := by
       simp [exact, Formula.accepts]
@@ -93,6 +102,7 @@ namespace Trace
       simp [get_exact_var] at h1
       rw [h1]
 
+  /-- Lemma: If `exact t` accepts `t'`, then `t` and `t'` have the same tail.-/
   theorem exact_accepts_cons (h h': Vector Bool n) (t t': Trace n):
     (exact (h::t)).accepts (h'::t') → (exact t).accepts t' := by
       intro hyp
@@ -104,6 +114,7 @@ namespace Trace
       simp at h2
       exact h2
 
+  /-- Lemma: `exact` of the empty trace does not accept non-empty traces.-/
   theorem exact_nil_not_accepts_cons (h: Vector Bool n) (t: Trace n):
     ¬ (exact []).accepts (h :: t) := by
     intro h1
@@ -139,7 +150,7 @@ namespace Trace
             assumption
 
 
-  /-- Correctness of `t.exact` -/
+  /-- Correctness and soundness of `t.exact` -/
   theorem exact_correct (t t': Trace n):
     t.exact.accepts t' ↔ t = t' := by
       constructor
@@ -162,12 +173,14 @@ namespace Trace
 
 end Trace
 
-
+/-- Given a list of traces, construct a formula that accepts
+exactly these traces, and no other. -/
 def UpperBoundFormula (ts: List (Trace n)) : Formula n :=
   let fs := ts.map Trace.exact
   fs.foldr Formula.Or Formula.False
 
-
+/-- Lemma: If all formulas in a list accept `t`,
+then the `Or` of this list also accepts `t`.-/
 theorem foldr_or_aux (l: List (Formula n)) (t: Trace n):
   ∀ f ∈ l, f.accepts t → (l.foldr Formula.Or Formula.False).accepts t := by
       induction l with
@@ -186,6 +199,9 @@ theorem foldr_or_aux (l: List (Formula n)) (t: Trace n):
           cases t <;> simp <;> right <;> apply ih f h_in he
 
 
+
+/-- Lemma: If the `Or` of a list of formulas accepts `t`,
+then some formula in the list accepts `t`.-/
 theorem foldr_or_aux_rev (l: List (Formula n)) (t: Trace n):
   (l.foldr Formula.Or Formula.False).accepts t → ∃ f ∈ l, f.accepts t := by
       intro h
@@ -221,8 +237,9 @@ theorem list_map_contains (l: List α) (f: α → β):
         exact h2
 
 
-/-- Theorem X (TODO) from the paper:
-For any disjoint set of positive and negative examples, there exists a formula that accepts the positive rand rejects the negatives.
+/-- Theorem:
+For any disjoint set of positive and negative examples,
+there exists a formula that accepts all the positive and rejects the negatives.
 -/
 theorem UpperBound (pos: List (Trace n)) (neg: List (Trace n)) (h: ∀ t ∈ pos, ∀ t'∈ neg, t ≠ t') :
   exists (phi: Formula n), (∀ t ∈ pos, phi.accepts t) ∧ (∀t ∈ neg, ¬ phi.accepts t):= by