started gqm

_CoqProject

 -Q theories GQM
 -arg -w -arg -notation-overridden
-theories/GQM.v
\ No newline at end of file
+theories/Base.v
+theories/GQM.v
+theories/GQMDeduction.v
\ No newline at end of file

theories/Base.v

+From Coq Require Export ssreflect ssrfun ssrbool.
+Require Export Coq.Lists.List.
+Export ListNotations.
+
+Set Implicit Arguments.
+Unset Strict Implicit.
+Unset Printing Implicit Defensive.

theories/GQM.v

 Require Import Autosubst.Autosubst.
 
+Require Import GQM.Base.
+
 Inductive form :=
 | Var (x : var)
-| App (s t : form)
-| Lam (s : {bind form}).
+| Neg (f : form)
+| And (f g : form)
+| Box (f : form)
+| SquareAll (f : {bind form}).
 
 Instance Ids_form : Ids form. derive. Defined.
 Instance Rename_form : Rename form. derive. Defined.
 Instance Subst_form : Subst form. derive. Defined.
-Instance SubstLemmas_form : SubstLemmas form. derive. Qed.
\ No newline at end of file
+Instance SubstLemmas_form : SubstLemmas form. derive. Qed.
+
+Infix "&" :=  And (at level 75, right associativity).
+Notation "'[A]' B"   := (SquareAll B) (at level 74, right associativity).
+Notation "|[]| A"   := (Box A) (at level 74, right associativity).
+Notation "'-!' A" := (Neg A) (at level 73, right associativity).
+Definition Or A B := (-! (-! A & -! B)).
+Notation "A '|||' B" := (Or A B) (at level 76, right associativity).
+Definition Imp A B := ((-! A) ||| B).
+Notation "A '->>' B" := (Imp A B) (at level 77, right associativity).
+Notation "A '<<->>' B" := ((A ->> B) & (B ->> A)) (at level 78).
+
+Notation context := (list form).
+
+(** ** Decidable Equality *)
+
+Lemma dceq_v : forall n n0,  {Var n = Var n0} + {Var n <> Var n0}.
+Proof.
+  elim.
+  - case; by [ left | right].
+  - move => n IH.
+    case; try by right.
+    move => n0.
+    case: (IH n0).
+    + case => ->.
+        by left.
+    + move => Hneq.
+      right.
+      move => [Heq].
+      apply: Hneq.
+      by rewrite Heq.
+Qed.
+
+Lemma dceq_f: forall (A B: form), {A = B} + {A <> B}.
+Proof.
+  elim; intros; case: B; try by [right];
+    try by [ move => f2; case: (X f2); try by [move => ->; left];
+    move => Hneq;
+    right;
+     move => [Heq]].
+  - apply: dceq_v.
+  - move => f2 g2.
+    case: (X f2);case: (X0 g2);move => H1 H2;subst; try by [left]; right; by move => [].
+Qed.
\ No newline at end of file

theories/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.
\ No newline at end of file