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

Definition context := Ensemble form.

Definition empty_con : context := Empty_set form.

Definition context_cons (c : context) (o : form) : context :=
 Add form c o.

Definition elem (o : form) (c : context) := In form c o.

Notation " '{}' " := empty_con (at level 50).
Notation " c ',,' o " := (context_cons c o)
  (at level 45, left associativity).


(** Definition *)

Inductive GQMded: context -> form -> Prop :=
| gqm_in G f1: elem f1 G -> GQMded G f1
| gqm_impI G f1 f2: GQMded (G,,f1) f2 -> GQMded G (f1 ->> f2)
| gqm_impE G f1 f2: GQMded G f1 -> GQMded G (f1 ->> f2) -> GQMded G f2

| gqm_dneg G f: GQMded G (-! (-! f) ->> f)

| gqm_ADist G f1 f2: GQMded G ([A](f1 ->> f2) ->> ([A]f1 ->> [A]f2))
| gqm_AE G f1 f2: GQMded G ([A]f1 ->> (f1.[f2.: ids])).

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

(** Basic facts *)
(** cut elimination *)

Lemma cut_elim : forall G f1 f2, G |-- f1 -> G,,f1 |-- f2 -> G |-- f2.
Proof.
  eauto with GQMDB.
Qed.

(** context *)

Lemma context_weakening : forall G G' f, Included form G G' -> G |-- f -> G' |-- f.
Proof.
  move => G f1 f2 Hin H.
  elim: H f1 Hin; eauto with GQMDB; clear G f2.
  - move => G f1 Helem G2 Hinc.
    apply: gqm_in.
    by apply: Hinc.
  - move => G f1 f2 Hi IH G2 Hinc.
    apply: gqm_impI.
    apply: IH.
    unfold Included.
    move => _ [x Hx| x Hx].
    + apply: Union_introl.
      by eauto.
    + by apply: Union_intror.
Qed.

(** Lemmas for classical tautologies *)

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

Lemma gqm_em : forall G f, G |-- (-! f ||| f).
Proof.
  by apply: gqm_dneg.
Qed.

Lemma gqm_andI : forall G f1 f2, G |-- f1 -> G |-- f2 -> G |-- (f1 & f2).
Proof.
  move => G f1 f2 Hf1 Hf2.
  unfold And.
  apply: gqm_impI.
  unfold Neg.
  have Hn : (G,, (f1 ->> f2 ->> Bot) |-- f2 ->> Bot). {
    apply: (gqm_impE _ f1).
    - apply: (context_weakening G); eauto.
        by apply: Union_introl.
    - apply: gqm_in.
      by apply: Union_intror.
  }
  apply: (gqm_impE _ f2).
  - apply: (context_weakening G); eauto.
        by apply: Union_introl.
  - apply: cut_elim.
    + by apply: Hn.
    + apply: gqm_in.
      by apply: Union_intror.
Qed.

Lemma gqm_andE1 : forall G f1 f2, G |-- (f1 & f2) -> G |-- f1.
Proof.
  move => G f1 f2 Hand.
  unfold And in Hand.




Lemma gqm_orI1 : forall G f1 f2, G |-- f1 -> G |-- (f1 ||| f2).
Proof.
  move => G f1 f2 Hf1.
  unfold Or.
  apply: gqm_impI.
  apply: gqm_impE; last by apply: gqm_botE.
  apply: (gqm_impE _ f1).
  - apply: cut_elim.
    + apply: (context_weakening G); try by apply: Union_introl.
        by apply: Hf1.
    + apply: gqm_in.
      by apply: Union_intror.
  - apply: gqm_in.
    by apply: Union_intror.
Qed.

Lemma gqm_orI2 : forall G f1 f2, G |-- f2 -> G |-- (f1 ||| f2).
Proof.
  move => G f1 f2 Hf1.
  unfold Or.
  apply: gqm_impI.
  apply: (context_weakening G); eauto.
  apply: Union_introl.
Qed.

Lemma gqm_orE : forall G f1 f2 f3, G |-- (f1 ||| f2) -> G,,f1 |-- f3 -> G,,f2 |-- f3 -> G |-- f3.
Proof.
  move => G f1 f2 f3 Hor Hf1 Hf2.
  unfold Or in Hor.