propositional.v

Require Coq.Lists.List.

Module Type Sig.
  Parameter Atomic : Set.
  Parameter Atomic_dec : forall x y : Atomic, {x = y} + {x <> y}.
End Sig.

Module Propositional (UnderlyingAtomic : Sig).
Import UnderlyingAtomic.
Import Coq.Lists.List.
Import ListNotations.

Declare Scope formula_scope.
Delimit Scope formula_scope with formula.
Open Scope formula_scope.

Inductive Formula : Set :=
  | atomic : Atomic -> Formula
  | implication : Formula -> Formula -> Formula
  | negation : Formula -> Formula.

Notation "A --> B" :=
    (implication A B)
    (at level 72, right associativity)
    : formula_scope.

Notation "¬ A" :=
  (negation A)
  (at level 71, no associativity)
  : formula_scope.

Definition orp A B := (¬ A --> B).
Definition andp A B := (¬ (A --> ¬ B)).

Theorem Formula_dec : forall x y : Formula, {x = y} + {x <> y}.
Proof.
    induction x; intros; destruct y; try (right; intros H; discriminate).
    - (* atomic *)
      destruct (Atomic_dec a a0).
        * left. rewrite e. reflexivity.
        * right. intros H. injection H as H. rewrite H in n. apply n. reflexivity.
    - (* impl *)
      destruct (IHx1 y1); destruct (IHx2 y2); try (right; intros H; injection H as H1 H2; contradiction).
      left. rewrite e, e0. reflexivity.
    - (* neg *)
      destruct (IHx y).
      left. rewrite e. reflexivity.
      right. intros H. injection H as H. contradiction.
Qed.

Inductive HilbertProof (axioms : list Formula) (proposition : Formula) : Prop :=
  | axiom : In proposition axioms -> HilbertProof axioms proposition
  | mp : forall (a : Formula), HilbertProof axioms a -> HilbertProof axioms (a --> proposition)
      -> HilbertProof axioms proposition.

Notation "axiom |- proposition" := (HilbertProof axiom proposition)
  (at level 74, no associativity) : formula_scope.

Example axiom1 : forall (a : Formula), HilbertProof [a] a.
Proof.
    intros. apply axiom.
    unfold In. left. reflexivity.
Qed.

Lemma weaken : forall (axs axs' : list Formula) (proposition : Formula),
    incl axs axs' -> HilbertProof axs proposition -> HilbertProof axs' proposition.
Proof.
    intros. induction H0.
    - apply axiom. apply H. assumption.
    - apply mp with a.
      + assumption.
      + assumption.
Qed.

Lemma implication_axiom_append : forall (ax_a ax_a_b : list Formula) (a b : Formula),
  HilbertProof ax_a a -> HilbertProof ax_a_b (a --> b) -> HilbertProof (ax_a ++ ax_a_b) b.
Proof.
    intros.
    assert (HilbertProof (ax_a ++ ax_a_b) a). {
        apply weaken with ax_a.
        apply incl_appl. apply incl_refl.
        assumption.
    }
    assert (HilbertProof (ax_a ++ ax_a_b) (a --> b)). {
        apply weaken with ax_a_b.
        apply incl_appr. apply incl_refl.
        assumption.
    }
    apply mp with a. assumption. assumption.
Qed.

Inductive isClassical : (list Formula -> Prop) :=
  | classical_nil : isClassical []
  | K : forall (phi psi : Formula) (ax' : list Formula),
    isClassical ax' ->
    isClassical ((psi --> phi --> psi) :: ax')
  | S : forall (psi phi chi : Formula) (ax' : list Formula),
    isClassical ax' ->
    isClassical (((psi --> phi --> chi) --> (psi --> phi) --> (psi --> chi)) :: ax')
  | CP : forall (phi psi : Formula) (ax' : list Formula),
    isClassical ax' -> 
    isClassical (((¬ psi --> ¬ phi) --> (phi --> psi)) :: ax').

(* An equivalent formulation for isClassical *)
Definition allClassical (G : list Formula) :=
  forall (x : Formula), In x G -> (
       (exists (phi psi : Formula), x = (psi --> phi --> psi))
    \/ (exists (psi phi chi : Formula), x = ((psi --> phi --> chi) --> (psi --> phi) --> (psi --> chi)))
    \/ (exists (phi psi : Formula), x = ((¬ psi --> ¬ phi) --> (phi --> psi)))
  ).

Lemma allClassical_isClassical_iff : forall G : list Formula, isClassical G <-> allClassical G.
Proof.
    unfold allClassical. split; intros.
    - (* -> *) induction H; inversion H0; try (apply IHisClassical in H1; apply H1); rewrite <- H1.
      + left. exists phi, psi. reflexivity.
      + right. left. exists psi, phi, chi. reflexivity.
      + right. right. exists phi, psi. reflexivity.
    - induction G.
      + constructor.
      + destruct (H a) as [HK | [HS | HCP]].
        * left. reflexivity.
        * destruct HK as [phi [psi HaK]].
          rewrite HaK. apply K.
          apply IHG. intros. apply H. right. assumption.
        * destruct HS as [psi [phi [chi HaS]]].
        rewrite HaS. apply S.
        apply IHG. intros. apply H. right. assumption.
        * destruct HCP as [phi [psi HaCP]].
        rewrite HaCP. apply CP.
        apply IHG. intros. apply H. right. assumption.
Qed.

Lemma isClassical_app : forall G H : list Formula,
  isClassical G -> isClassical H -> isClassical (G ++ H).
Proof.
    intros. rewrite (allClassical_isClassical_iff G) in H0. rewrite (allClassical_isClassical_iff H) in H1.
    rewrite allClassical_isClassical_iff.
    intros x xInGH. apply in_app_or in xInGH. destruct xInGH.
    + apply H0. apply H2.
    + apply H1. apply H2.
Qed.

Ltac recursively_classical := repeat (repeat ((try apply isClassical_app); (try assumption)); repeat constructor).

Definition Classically (ax : list Formula) (p : Formula) := exists (x : list Formula), isClassical x /\ (ax ++ x |- p).
Notation "ax |-c p" := (Classically ax p)
  (at level 74, no associativity) : formula_scope.

Lemma weaken_c : forall (G H : list Formula) (p : Formula),
  incl G H -> G |-c p -> H |-c p.
Proof. unfold Classically.
    intros. destruct H1. exists x. destruct H1. split.
    assumption. apply weaken with (G ++ x).
    apply incl_app. apply incl_appl. assumption. apply incl_appr. apply incl_refl.
    assumption.
Qed.

Theorem identity_implication : forall (p : Formula), [] |-c p --> p.
Proof.
    intros. unfold Classically.
    exists [
        (p --> p --> p) ;
        (p --> (p --> p) --> p);
        ((p --> ((p --> p) --> p)) --> ((p --> (p --> p)) --> (p --> p)))
    ].
    split.
    - repeat constructor.
    - simpl. apply mp with (p --> p --> p).
      apply axiom. simpl. left. reflexivity.
      apply mp with (p --> (p --> p) --> p).
      apply axiom. simpl. right. left. reflexivity.
      apply axiom. simpl. right. right. left. reflexivity.
Qed.

Theorem contraposition : forall (G : list Formula) (p q : Formula), G |-c ¬ p --> ¬ q -> G |-c q --> p.
Proof.
    intros. destruct H as [x [Hxc Hseq]].
    exists (x ++ [(¬ p --> ¬ q) --> (q --> p)]).
    split. recursively_classical.
    apply mp with (¬ p --> ¬ q).
    - apply weaken with (G ++ x).
      rewrite app_assoc. apply incl_appl. apply incl_refl.
      assumption.
    - apply axiom. rewrite app_assoc. apply in_or_app. right. left. reflexivity.
Qed.

Theorem deduction : forall (Gamma : list Formula) (A B : Formula),
  A :: Gamma |-c B -> Gamma |-c A --> B.
Proof.
    unfold Classically. intros. destruct H as [x' [Hclassical_x' seq]].
    induction seq as [ax Hax | prem Hprem Himpl].
    (* Let's find out how "Gamma, A0 |- ax" is proved *)
    - apply in_app_or in Hax. destruct Hax as [Hax | Hp].
      + (* Uses a hypothesis *)
        simpl in Hax. destruct Hax as [HA0 | Hax].
        * (* if the hypothesis is A0 itself *)
          rewrite <- HA0. destruct (identity_implication A) as [x0 [Hx0 Hidimpl]].
          exists x0. split.
          ** recursively_classical.
          ** simpl in Hidimpl. apply weaken with x0.
             apply incl_appr. apply incl_refl.
             assumption.
        * (* if the hypothesis is inside Gamma *)
          exists [ax --> A --> ax]. split.
          ** recursively_classical.
          ** apply mp with ax.
            *** apply axiom.
                apply in_or_app. left. assumption.
            *** apply axiom.
                apply in_or_app. right. left. reflexivity.
      + (* uses an axiom *)
        exists ((ax --> A --> ax) :: x'). split.
        ** recursively_classical.
        ** apply mp with ax.
          *** apply axiom.
              apply in_or_app. right.
              right. assumption.
          *** apply axiom.
              apply in_or_app. right.
              left. reflexivity.
  - (* uses modus ponens *)
    destruct IHHimpl as [xHimpl [HcxHimpl]];
    destruct IHseq1 as [xHseq [HcxHseq]].
    exists (xHimpl ++ xHseq ++ [
        (A --> Hprem --> prem) --> (A --> Hprem) --> A --> prem
    ]). split.
    ** recursively_classical.
    ** apply mp with (A --> Hprem).
      + apply weaken with (Gamma ++ xHimpl).
        ++ repeat rewrite app_assoc. apply incl_appl. apply incl_appl.
           apply incl_refl.
        ++ assumption.
      + apply mp with (A --> Hprem --> prem).
        ++ apply weaken with (Gamma ++ xHseq).
            +++ repeat rewrite app_assoc. apply incl_appl.
            apply incl_app.
            repeat apply incl_appl. apply incl_refl.
            apply incl_appr. apply incl_refl.
            +++ assumption.
        ++ apply axiom. repeat (apply in_or_app; right).
           left. reflexivity.
Qed.
End Propositional.