Fix context out of section error

coq/Completeness.v

@@ -2,6 +2,7 @@ Require Import Decidable Equality Relations.
 Require Import Modal_Library Modal_Notations Modal_Tactics Deductive_System Soundness List Classical Bool Sets.
 Set Implicit Arguments.
 
+Section Completeness.
 Context `{X: modal_index_set}.
 
 (* Assume that formulas are constructively countable for now. *)
@@ -151,8 +152,6 @@ Proof.
   - assumption.
 Qed.
 
-Section Completeness.
-
   Variable A: axiom -> Prop.
 
   Hypothesis extending_P: Subset P A.

coq/Deductive_System.v

@@ -30,14 +30,14 @@ Inductive axiom: Set :=
 Definition instantiate (a: axiom): formula :=
   match a with
   | ax1      φ ψ   => [! φ -> (ψ -> φ) !]
-  | ax2      φ ψ Ɣ => [! (φ -> (ψ -> Ɣ)) -> ((φ -> ψ) -> (φ -> Ɣ)) !]
+  | ax2      φ ψ γ => [! (φ -> (ψ -> γ)) -> ((φ -> ψ) -> (φ -> γ)) !]
   | ax3      φ ψ   => [! (~ψ -> ~φ) -> (φ -> ψ) !]
   | ax4      φ ψ   => [! φ -> (ψ -> (φ /\ ψ)) !]
   | ax5      φ ψ   => [! (φ /\ ψ) -> φ !]
   | ax6      φ ψ   => [! (φ /\ ψ) -> ψ !]
   | ax7      φ ψ   => [! φ -> (φ \/ ψ) !]
   | ax8      φ ψ   => [! ψ -> (φ \/ ψ) !]
-  | ax9      φ ψ Ɣ => [! (φ -> Ɣ) -> ((ψ -> Ɣ) -> ((φ \/ ψ) -> Ɣ)) !]
+  | ax9      φ ψ γ => [! (φ -> γ) -> ((ψ -> γ) -> ((φ \/ ψ) -> γ)) !]
   | ax10     φ     => [! ~~φ -> φ !]
   | axK    i φ ψ   => [! [i](φ -> ψ) -> ([i]φ -> [i]ψ) !]
   | axDual i φ     => [! <i>φ <-> ~[i]~φ !]

coq/Examples.v

@@ -1,131 +1,133 @@
 Require Import List Modal_Library Modal_Notations Deductive_System Modal_Tactics Sets.
 Import ListNotations.
 
-Context `{X: modal_index_set}.
+Section Examples.
+  Context `{X: modal_index_set}.
 
-Definition fixed_point A G i :=
-  forall f,
-  exists p,
-  (A; G |-- [! (p <-> f ([i] p))!]).
+  Definition fixed_point A G i :=
+    forall f,
+    exists p,
+    (A; G |-- [! (p <-> f ([i] p))!]).
 
-Definition subset {T} (P: T -> Prop) (Q: T -> Prop): Prop :=
-  forall x, P x -> Q x.
+  Definition subset {T} (P: T -> Prop) (Q: T -> Prop): Prop :=
+    forall x, P x -> Q x.
 
-(* Some quick automation! *)
-Local Hint Unfold subset: modal.
-Local Hint Constructors P: modal.
-Local Hint Constructors K: modal.
-Local Hint Constructors K4: modal.
+  (* Some quick automation! *)
+  Local Hint Unfold subset: modal.
+  Local Hint Constructors P: modal.
+  Local Hint Constructors K: modal.
+  Local Hint Constructors K4: modal.
 
-Theorem Lob:
-  (* Löb's theorem is provable in any superset of K4 with fixed points. *)
-  forall A i,
-  subset (K4 i) A /\ fixed_point A Empty i ->
-  forall p,
-  (A; Empty |-- [! [i]p -> p !]) ->
-  (A; Empty |-- [! p !]).
-Proof.
-  set (G := Empty).
-  (* Step 1. *)
-  intros A i [I FP] p H1.
-  (* Step 2. *)
-  destruct FP with (fun X => [! X -> p !]) as (psi, H2).
-  (* Step 3. *)
-  assert (A; G |-- [! psi -> [i]psi -> p !]) as H3.
-  apply modal_ax5 in H2; auto with modal.
-  (* Step 4. *)
-  assert (A; G |-- [! [i](psi -> [i]psi -> p) !]) as H4.
-  apply Nec; auto.
-  (* Step 5. *)
-  assert (A; G |-- [! [i]psi -> [i]([i]psi -> p) !]) as H5.
-  apply modal_axK in H4; auto with modal.
-  (* Step 6. *)
-  assert (A; G |-- [! [i]([i]psi -> p) -> [i][i]psi -> [i]p !]) as H6.
-  eapply Ax with (a := axK i ?[X] ?[Y]); auto with modal.
-  reflexivity.
-  (* Step 7. *)
-  assert (A; G |-- [! [i]psi -> [i][i]psi -> [i]p !]) as H7.
-  eapply modal_syllogism; eauto with modal.
-  (* Step 8. *)
-  assert (A; G |-- [! [i]psi -> [i][i]psi !]) as H8.
-  apply modal_axK4; auto with modal.
-  (* Step 9. *)
-  assert (A; G |-- [! [i]psi -> [i]p !]) as H9.
-  eapply modal_ax2; eauto with modal.
-  (* Step 10. *)
-  assert (A; G |-- [! [i]psi -> p !]) as H10.
-  eapply modal_syllogism; eauto with modal.
-  (* Step 11. *)
-  assert (A; G |-- [! ([i]psi -> p) -> psi !]) as H11.
-  apply modal_ax6 in H2; auto with modal.
-  (* Step 12. *)
-  assert (A; G |-- psi) as H12.
-  eapply Mp; try eassumption.
-  (* Step 13. *)
-  assert (A; G |-- [! [i]psi !]) as H13.
-  apply Nec; try assumption.
-  (* Step 14. *)
-  eapply Mp; eassumption.
-Qed.
+  Theorem Lob:
+    (* Löb's theorem is provable in any superset of K4 with fixed points. *)
+    forall A i,
+    subset (K4 i) A /\ fixed_point A Empty i ->
+    forall p,
+    (A; Empty |-- [! [i]p -> p !]) ->
+    (A; Empty |-- [! p !]).
+  Proof.
+    set (G := Empty).
+    (* Step 1. *)
+    intros A i [I FP] p H1.
+    (* Step 2. *)
+    destruct FP with (fun X => [! X -> p !]) as (psi, H2).
+    (* Step 3. *)
+    assert (A; G |-- [! psi -> [i]psi -> p !]) as H3.
+    apply modal_ax5 in H2; auto with modal.
+    (* Step 4. *)
+    assert (A; G |-- [! [i](psi -> [i]psi -> p) !]) as H4.
+    apply Nec; auto.
+    (* Step 5. *)
+    assert (A; G |-- [! [i]psi -> [i]([i]psi -> p) !]) as H5.
+    apply modal_axK in H4; auto with modal.
+    (* Step 6. *)
+    assert (A; G |-- [! [i]([i]psi -> p) -> [i][i]psi -> [i]p !]) as H6.
+    eapply Ax with (a := axK i ?[X] ?[Y]); auto with modal.
+    reflexivity.
+    (* Step 7. *)
+    assert (A; G |-- [! [i]psi -> [i][i]psi -> [i]p !]) as H7.
+    eapply modal_syllogism; eauto with modal.
+    (* Step 8. *)
+    assert (A; G |-- [! [i]psi -> [i][i]psi !]) as H8.
+    apply modal_axK4; auto with modal.
+    (* Step 9. *)
+    assert (A; G |-- [! [i]psi -> [i]p !]) as H9.
+    eapply modal_ax2; eauto with modal.
+    (* Step 10. *)
+    assert (A; G |-- [! [i]psi -> p !]) as H10.
+    eapply modal_syllogism; eauto with modal.
+    (* Step 11. *)
+    assert (A; G |-- [! ([i]psi -> p) -> psi !]) as H11.
+    apply modal_ax6 in H2; auto with modal.
+    (* Step 12. *)
+    assert (A; G |-- psi) as H12.
+    eapply Mp; try eassumption.
+    (* Step 13. *)
+    assert (A; G |-- [! [i]psi !]) as H13.
+    apply Nec; try assumption.
+    (* Step 14. *)
+    eapply Mp; eassumption.
+  Qed.
 
-(* TODO: review later!
+  (* TODO: review later!
 
-Definition fromList (ps: list formula): theory :=
-  fun p =>
-    In p ps.
+  Definition fromList (ps: list formula): theory :=
+    fun p =>
+      In p ps.
 
-Example Ex1:
-  (* TODO: fix notation for deduction! *)
-  T; (fromList ([! [](#0 -> #1) !] :: [! [](#1 -> #2) !] :: nil)) |--
-    [! [](#0 -> #2) !].
-Proof.
-  (* Line: 16 *)
-  apply Nec.
-  (* Line: 15 *)
-  apply Mp with (f := [! #0 -> #1 !]).
-    (* Line: 14 *)
-  - apply Mp with (f := [! #1 -> #2 !]).
-      (* Line: 9 *)
-    + apply Mp with (f := [! (#1 -> #2) -> (#0 -> (#1 -> #2)) !]).
-        (* Line: 7 *)
-      * apply Mp with (f := [! (#1 -> #2) -> ((#0 -> (#1 -> #2)) -> (#0 -> #1) -> (#0 -> #2)) !]).
-          (* Line: 6 *)
-        -- apply Ax with (a := ax2 [! #1 -> #2 !] [! #0 -> (#1 -> #2) !] [! (#0 -> #1) -> (#0 -> #2) !]).
-          ++ constructor.
-             constructor.
-          ++ reflexivity.
-        (* Line: 5 *)
-        -- apply Mp with (f := [! (#0 -> (#1 -> #2)) -> ((#0 -> #1) -> (#0 -> #2)) !]).
-          (* Line: 3 *)
-          ++ apply Ax with (a := ax1 [! (#0 -> (#1 -> #2)) -> ((#0 -> #1) -> (#0 -> #2)) !] [! #1 -> #2 !]).
-            ** constructor.
-               constructor.
-            ** reflexivity.
-          (* Line: 4 *)
-          ++ apply Ax with (a := ax2 [! #0 !] [! #1 !] [! #2 !]).
-            ** constructor; constructor.
-            ** reflexivity.
-        (* Line: 8 *)
-      * apply Ax with (a := ax1 [! #1 -> #2 !] [! #0 !]).
-        -- constructor; constructor.
-        -- reflexivity.
-      (* Line: 11 *)
-    + apply Mp with (f := [! [](#1 -> #2) !]).
-      * apply Ax with (a := axT [! #1 -> #2 !]).
-        -- constructor; constructor.
-        -- reflexivity.
-        (* Line: 2 *)
-      * apply Prem; simpl.
+  Example Ex1:
+    (* TODO: fix notation for deduction! *)
+    T; (fromList ([! [](#0 -> #1) !] :: [! [](#1 -> #2) !] :: nil)) |--
+      [! [](#0 -> #2) !].
+  Proof.
+    (* Line: 16 *)
+    apply Nec.
+    (* Line: 15 *)
+    apply Mp with (f := [! #0 -> #1 !]).
+      (* Line: 14 *)
+    - apply Mp with (f := [! #1 -> #2 !]).
+        (* Line: 9 *)
+      + apply Mp with (f := [! (#1 -> #2) -> (#0 -> (#1 -> #2)) !]).
+          (* Line: 7 *)
+        * apply Mp with (f := [! (#1 -> #2) -> ((#0 -> (#1 -> #2)) -> (#0 -> #1) -> (#0 -> #2)) !]).
+            (* Line: 6 *)
+          -- apply Ax with (a := ax2 [! #1 -> #2 !] [! #0 -> (#1 -> #2) !] [! (#0 -> #1) -> (#0 -> #2) !]).
+            ++ constructor.
+              constructor.
+            ++ reflexivity.
+          (* Line: 5 *)
+          -- apply Mp with (f := [! (#0 -> (#1 -> #2)) -> ((#0 -> #1) -> (#0 -> #2)) !]).
+            (* Line: 3 *)
+            ++ apply Ax with (a := ax1 [! (#0 -> (#1 -> #2)) -> ((#0 -> #1) -> (#0 -> #2)) !] [! #1 -> #2 !]).
+              ** constructor.
+                constructor.
+              ** reflexivity.
+            (* Line: 4 *)
+            ++ apply Ax with (a := ax2 [! #0 !] [! #1 !] [! #2 !]).
+              ** constructor; constructor.
+              ** reflexivity.
+          (* Line: 8 *)
+        * apply Ax with (a := ax1 [! #1 -> #2 !] [! #0 !]).
+          -- constructor; constructor.
+          -- reflexivity.
+        (* Line: 11 *)
+      + apply Mp with (f := [! [](#1 -> #2) !]).
+        * apply Ax with (a := axT [! #1 -> #2 !]).
+          -- constructor; constructor.
+          -- reflexivity.
+          (* Line: 2 *)
+        * apply Prem; simpl.
+          firstorder.
+      (* Line: 13 *)
+    - apply Mp with (f := [! [](#0 -> #1) !]).
+        (* Line: 12 *)
+      + apply Ax with (a := axT [! #0 -> #1 !]).
+        * constructor; constructor.
+        * reflexivity.
+        (* Line: 1 *)
+      + apply Prem; simpl.
         firstorder.
-    (* Line: 13 *)
-  - apply Mp with (f := [! [](#0 -> #1) !]).
-      (* Line: 12 *)
-    + apply Ax with (a := axT [! #0 -> #1 !]).
-      * constructor; constructor.
-      * reflexivity.
-      (* Line: 1 *)
-    + apply Prem; simpl.
-      firstorder.
-Qed.
+  Qed.
 
-*)
+  *)
+End Examples.