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))
(* | 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_contrap: forall A B, |-- (A ->> B) ->> (-! B ->> -! A).
Proof.
  move => A B.
  rewrite /Neg.
  have HA : (|-- (A ->> B) ->> A ->> (B ->> Bot) ->> Bot). {
    apply: gqm_mp; first by apply: gqm_chain.
    eauto with GQMDB.
  }
  eauto with GQMDB.
  Unshelve.
  apply: (Var 0).
  apply: (Var 0).
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_contrap2: forall A B, |-- ((-! A ->> B) ->> (-! B ->> A)).
Proof.
  move => A B.
  have H : (|-- ((-! A ->> B) ->> (-! B ->> -! -! A))) by apply gqm_contrap.
  apply: gqm_mp; last by apply: H.
  apply: gqm_mp; first by apply: gqm_chain.
  apply: gqm_mp; first by apply: gqm_chain.
  apply: gqm_dnegE.
Qed.

Lemma gqm_negE2 : forall A B, |-- (A ->> -! B) ->> (A ->> B) ->> -! A.
Proof.
  move => A B.
  unfold Neg.
  eauto with GQMDB.
Qed.


Lemma gqm_negE3 : forall A B, |-- (A ->> B) ->> (-! A ->> B) ->> B.
Proof.
  move => A B.
  suff HA : (|-- (A ->> B) ->> (-! B ->> A) ->> B). {
    apply: gqm_mp; last by apply: HA.
    clear HA.
    apply: gqm_mp; first by apply: gqm_chain.
    apply: gqm_mp; last by apply: (gqm_contrap2 A B).
    apply: gqm_mp.
    - apply: gqm_mp.
      + apply: gqm_chain.
        apply: ((-! A ->> B) ->> ((-! B ->> A) ->> B) ->> B).
      + eauto with GQMDB.
    - apply: gqm_mp.
      + apply: gqm_chain.
      + eauto with GQMDB.
  }
  suff HA : (|-- (-! B ->> -! A) ->> (-! B ->> A) ->> B). {
    apply: gqm_mp; last by apply: (gqm_contrap A B).
    apply: gqm_mp; first by apply: gqm_chain.
    apply: HA.
  }
  apply: gqm_mp; last by apply: (gqm_negE2 (-! B) A).
  apply: gqm_mp; first by apply: gqm_chain.
  apply: gqm_mp; first by apply: gqm_chain.
  apply: gqm_dnegE.
  Unshelve.
  apply: (Var 0).
  apply: (Var 0).
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.
  apply: gqm_mp.
  - apply: gqm_mp; first by apply: (gqm_negE3 A).
    apply: gqm_mp; first by apply: gqm_swap.
    apply: gqm_mp; first by apply: gqm_chain.
    eauto with GQMDB.
  - apply: gqm_mp; first by apply: gqm_discardr.
    apply: gqm_mp; first by apply: gqm_swap.
    apply: gqm_mp.
    + apply: gqm_mp.
      * apply: gqm_chain.
        apply: ((-! A ->> B) ->> -! A ->> C).
      * apply: gqm_swap.
    + apply: gqm_chain.
Qed.