GQMDeduction.v

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

(** Definition *)

Definition change_top(dest: form)(v : var) : form :=
  match (v) with
  | 0 => dest
  | (S n) => ids (S n)
  end.

Inductive GQMded: form -> Prop :=
| 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/]))
| gqm_Aglob A B: GQMded ([A]A ->> ([A]A.[change_top(B)]))
| gqm_Q5 A: GQMded (-! [A]A ->> [A]-![A](A.[ren(+1)]))

| gqm_BoxCon A B: GQMded ([A](A <<->> B) ->> (|[]|A <<->> |[]| B))

| gqm_mp A B: GQMded (A ->> B) -> GQMded A -> GQMded B
| gqm_Anec A: GQMded A -> GQMded ([A]A.[ren (+1)])
| gqm_univgen A B: GQMded (A ->> [A]B) -> GQMded (A ->> [A][A](B.[ren(+1)]))
.

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