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.