GQMDeduction.v

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

Inductive GQMded: context -> form -> Prop :=
| gqm_in G f: In f G -> GQMded G f
| gqm_andE1 G f1 f2: GQMded G (f1 & f2) -> GQMded G f1
| gqm_andE2 G f1 f2: GQMded G (f1 & f2) -> GQMded G f2
| gqm_andI G f1 f2: GQMded G f1 -> GQMded G f2 -> GQMded G (f1 & f2)
| gqm_negI G f g: GQMded G (f ->> g) -> GQMded G (f ->> -! g) -> GQMded G (-! f) (* TODO neg intro*)
| gqm_negE G f: GQMded G (Neg (Neg f)) -> GQMded G f. (* TODO neg intro*)

Hint Constructors GQMded : GQMDB.

Lemma gqm_orE1 : forall G f1 f2, GQMded G f1 -> GQMded G (f1 ||| f2).
Proof.
  move => G f1 f2 Hf1.
  unfold Or.
  apply: (gqm_negI _ _ f1).
  - unfold Imp.
    unfold Or.


Lemma gqm_impE : forall G f1 f2, GQMded G f1 -> GQMded G (f1 ->> f2) -> GQMded G f2.
Proof.
  move => G f1.
  elim: f1 G.
  - move => x G f2 Hvar Himp.
    inversion Himp; subst.
  elim: Himp.

Lemma gqm_impI : forall G f1 f2, GQMded (f1 :: G) f2 -> GQMded G (f1 ->> f2).
Proof.
  move => G f1 f2.
  elim.