GQMDeduction.v

Require Import GQM.Base.
Require Import GQM.GQM.

(** Definition *)

Inductive GQMded: form -> Prop :=
| gqm_mp A B: GQMded (A ->> B) -> GQMded A -> GQMded B
| gqm_I1 A B: GQMded (A ->> B ->> A)
| gqm_I2 A B C: GQMded ((A ->> B ->> C) ->> (A ->> B) ->> A ->> C)
| gqm_I3 A B: GQMded ((-! A ->> -! B) ->> B ->> A)
| gqm_swap A B C: GQMded ((A ->> B ->> C) ->> (B ->> A ->> C)) (* TODO prove that this follows from the rest *)
(* | gqm_dneg f: GQMded (-! (-! f) ->> f) *)

| gqm_ADist A B: GQMded ([A](A ->> B) ->> ([A]A ->> [A]B))
| gqm_AE A B: GQMded ([A]A ->> (A.[B.: ids])).

Notation "'|--' A"  := (GQMded A) (at level 80, no associativity).
Hint Constructors GQMded : GQMDB.

(** Lemmas for classical tautologies *)

Lemma gqm_negE : forall f, |-- (Bot ->> f).
  move => f.
  by apply: gqm_AE.
Qed.

Lemma gqm_id : forall A, |-- (A ->> A).
  move => A.
  have H1 : (|-- A ->> (A ->> A) ->> A) by apply: gqm_I1.
  have H2 : (|-- (A ->> (A ->> A) ->> A) ->> (A ->> A ->> A) ->> A ->> A) by apply: gqm_I2.
  have H3 : (|-- (A ->> A ->> A) ->> A ->> A) by apply: gqm_mp; eauto.
  have H4 : (|-- A ->> A ->> A) by apply: gqm_I1.
  apply: gqm_mp.
  - by apply: H3.
  - by eauto.
Qed.

Lemma gqm_id' : forall A, |-- (A ->> A).
  eauto with GQMDB.
  Unshelve.
  apply: (Var 0).
  apply: (Var 0).
Qed.

Lemma gqm_id'' : forall A, |-- (A ->> A).
  move => A.
  apply: (gqm_mp (A ->> A ->> A)); last by apply: gqm_I1.
  apply: (gqm_mp (A ->> (A ->> A) ->> A)); last by apply: gqm_I1.
  by apply: gqm_I2.
Qed.

Lemma gqm_appl : forall A B, |-- ((A ->> B) ->> A ->> B).
Proof.
  eauto with GQMDB.
Qed.

Lemma gqm_appl2 : forall A B, |-- (A ->> (A ->> B) ->> B).
Proof.
  eauto with GQMDB.
  Unshelve.
  apply: (Var 0).
  apply: (Var 0).
Qed.

Lemma gqm_chain : forall A B C, |-- (B ->> C) ->> (A ->> B) ->> (A ->> C).
Proof.
  move => A B C.
  apply: gqm_mp.
  - apply: gqm_mp.
    + apply: (gqm_I2 (B ->> C) (A ->> B ->> C) ((A ->> B) ->> A ->> C)).
    + apply: gqm_mp.
      * apply: (gqm_I1 ((A ->> B ->> C) ->> (A ->> B) ->> A ->> C) (B ->> C)).
      * apply: (gqm_I2 A B C).
  - apply: (gqm_I1 (B ->> C) A).
Qed.

Lemma gqm_discard : forall A B C, |-- (A ->> C) ->> (B ->> A ->> C).
Proof.
  eauto with GQMDB.
Qed.

Lemma gqm_discardr : forall A B C, |-- (A ->> C) ->> (A ->> B ->> C).
Proof.
  eauto with GQMDB.
Qed.

Lemma gqm_discardI : forall A B, |-- (A ->> A ->> B) ->> (A ->> B).
Proof.
  move => A B.
  apply: gqm_mp.
  - apply: gqm_mp.
    + apply: gqm_I2.
      apply: (A ->> A).
    + apply: gqm_I2.
  - apply: gqm_mp.
    + apply: gqm_discard.
    + apply: gqm_id.
Qed.

Lemma gqm_discardIr : forall A B C, |-- (A ->> B ->> A ->> C) ->> (A ->> B ->> C).
Proof.
  eauto with GQMDB.
Qed.

Lemma gqm_dnegI : forall A, |-- (A ->> -! -! A).
Proof.
  move => A.
  unfold Neg.
  apply: gqm_mp.
  - apply: gqm_swap.
  - apply: gqm_appl.
Qed.

Lemma gqm_dnegE : forall A, |-- (-! -! A ->> A).
Proof.
  move => A.
  apply: gqm_mp.
  - apply: gqm_I3.
  - apply: gqm_dnegI.
Qed.

Lemma gqm_em : forall A, |-- (-! A ||| A).
Proof.
  apply: gqm_dnegE.
Qed.

(* Lemma gqm_em : forall f, |-- (-! f ||| f). *)
(* Proof. *)
  (* unfold Or. *)
(* Qed. *)

Lemma gqm_andI : forall A B, |-- (A ->> B ->> A & B).
Proof.
  move => A B.
  unfold And.
  unfold Neg.
  apply: gqm_mp.
  - apply: gqm_mp.
    + apply: gqm_chain.
      apply: ((A ->> B ->> Bot) ->> B ->> Bot).
    + apply: gqm_swap.
  - apply: gqm_mp.
    + apply: gqm_swap.
    + apply: gqm_id.
Qed.

Lemma gqm_andE1 : forall A B, |-- (A & B) ->> A.
Proof.
  move => A B.
  unfold And.
  unfold Neg.
  apply: gqm_mp.
  - apply: gqm_mp.
    + apply: gqm_chain.
      apply: (-! -! A).
    + apply: gqm_dnegE.
  - unfold Neg.
    apply: gqm_mp.
    + apply: gqm_swap.
    + apply: gqm_mp.
      * apply: gqm_mp.
        -- apply: gqm_chain.
           apply: (A ->> B ->> Bot).
        -- apply: gqm_appl2.
      * eauto with GQMDB.
Qed.

Lemma gqm_andE2 : forall A B, |-- (A & B) ->> B.
Proof.
  move => A B.
  unfold And.
  unfold Neg.
  apply: gqm_mp.
  - apply: gqm_mp.
    + apply: gqm_chain.
      apply: (-! -! B).
    + apply: gqm_dnegE.
  - unfold Neg.
    apply: gqm_mp; first by apply: gqm_swap.
    apply: gqm_mp.
    + apply: gqm_mp.
      * apply: gqm_chain.
           apply: (A ->> B ->> Bot).
      * apply: gqm_appl2.
    + apply: gqm_I1.
Qed.

Lemma gqm_orI1 : forall A B, |-- A ->> A ||| B.
Proof.
  move => A B.
  rewrite /Or /Neg.
  apply: gqm_mp; first by apply: gqm_swap.
  apply: gqm_mp; first by apply: gqm_chain.
  apply: gqm_negE.
Qed.

Lemma gqm_orI2 : forall A B, |-- B ->> A ||| B.
Proof.
  move => A B.
  rewrite /Or.
  apply: gqm_I1.
Qed.

(* Lemma gqm_orE : forall A B C, |-- (A ->> C) ->> (B ->> C) ->> (A ||| B) ->> C. *)
(* Proof. *)
  (* move => A B C. *)
  (* rewrite /Or. *)