Library twoAssn

Require Import language.
Require Import synEq.

Definition TwoAssn :=prod BExpr Expr.

Notation "b '>>' a '#'" := ((b,a):TwoAssn) (at level 100).

Definition twoAssnEqual (A1 A2: TwoAssn) : bool :=
  match A1, A2 with
    | (phi, (AExp A)), (phi', AExp A') => andb (BSynEq phi phi') (ASynEq A A')
    | (phi, (BExp B)), (phi', BExp B') => andb (BSynEq phi phi') (BSynEq B B')
    | (phi, (HExp H)), (phi', HExp H') => andb (BSynEq phi phi') (HSynEq H H')
    | _,_ => false end.

Lemma twoAssnEqual_eq: forall a b c d, true = twoAssnEqual (a,b) (c,d) -> (a = c) /\ (b = d).
intros. split. inv H. destruct b. destruct d. symmetry in H1. rewrite andb_true_iff in H1.
destruct H1. apply bSynEq_eq. symmetry in H. auto. inv H1. inv H1. destruct d. inv H1.
symmetry in H1; rewrite andb_true_iff in H1. destruct H1. apply bSynEq_eq. auto. inv H1.
destruct d. inv H1. inv H1. apply bSynEq_eq . symmetry in H1. rewrite andb_true_iff in H1.
destruct H1; auto.
simpl in *. destruct b. destruct d.
symmetry in H; rewrite andb_true_iff in H. destruct H. assert (z:=aSynEq_eq a0 a1). rewrite z.
auto. auto. inv H. inv H. destruct d. inv H.
symmetry in H; rewrite andb_true_iff in H. destruct H. assert (z:=bSynEq_eq b b0). rewrite z.
auto. auto. inv H. destruct d. inv H. inv H. symmetry in H. apply andb_true_iff in H. destruct H.
assert (y:= hSynEq_eq h h0). rewrite y. auto. auto.
Qed.

Lemma twoAssnEqual_eq2: forall a b, true = twoAssnEqual a b -> a = b.
intros. destruct a. destruct b. apply twoAssnEqual_eq in H. destruct H. subst. auto.
Qed.

Lemma twoAssnEq_refl: forall x, true = twoAssnEqual x x.
Proof.
intros. destruct x. simpl. destruct e. simpl. rewrite bSynEq_refl. rewrite aSynEq_refl.
auto. repeat rewrite bSynEq_refl. auto. rewrite bSynEq_refl. rewrite hSynEq_refl.
auto.
Qed.

Definition TwoAssns := list TwoAssn.

Definition TwoAssnSubstA (Theta :TwoAssn) (x: SkalVar) (A:AExpr) : TwoAssn :=
 match Theta with
    (phi, E) => ((BSubstA phi A x), (SubstA E A x))
end.

Fixpoint TwoAssnsSubstA (Theta: TwoAssns) (x:SkalVar) (A:AExpr) : TwoAssns :=
 match Theta with
 | h::t => (TwoAssnSubstA h x A)::(TwoAssnsSubstA t x A)
 | [] => []
end.

Definition TwoAssnSubstB (Theta :TwoAssn) (x: SkalVar) (B:BExpr) : TwoAssn :=
 match Theta with
    (phi, E) => ((BSubstB phi B x), (SubstB E B x))
end.

Fixpoint TwoAssnsSubstB (Theta: TwoAssns) (x:SkalVar) (B:BExpr) : TwoAssns :=
 match Theta with
 | h::t => (TwoAssnSubstB h x B)::(TwoAssnsSubstB t x B)
 | [] => []
end.

Definition TwoAssnSubstH (Theta :TwoAssn) (x: SkalVar) (H:HExpr) : TwoAssn :=
 match Theta with
    (phi, E) => ((BSubstH phi H x), (SubstH E H x))
end.

Fixpoint TwoAssnsSubstH (Theta: TwoAssns) (x:SkalVar) (H:HExpr) : TwoAssns :=
 match Theta with
 | h::t => (TwoAssnSubstH h x H)::(TwoAssnsSubstH t x H)
 | [] => []
end.

Definition TwoAssnsSubst (Theta: TwoAssns) (x:SkalVar) (e:Expr) : TwoAssns :=
match e with
| AExp a => TwoAssnsSubstA Theta x a
| BExp b => TwoAssnsSubstB Theta x b
| HExp h => TwoAssnsSubstH Theta x h
end.

Fixpoint TwoAssnsFv (ta: TwoAssns) : list SkalVar :=
 match ta with
| h::t => (match h with
          | (phi, A) => (BFv phi) ++ (fv A)
          end)
          ++ (TwoAssnsFv t)
| [] => [] end.

Fixpoint andIntoTheta (Theta: TwoAssns) (B: BExpr):TwoAssns:=
match Theta with
  h::t => match h with
                 | (phi, E) => ((AndExpr phi B), E) :: andIntoTheta t B
              end
| nil => nil
end.

Fixpoint conBoolAgreementHelp (phi1: BExpr) (Theta2 :TwoAssns) (B:BExpr) : TwoAssns:=
  let firstbool := (AndExpr phi1 B) in
  match Theta2 with
    h::t => match h with
                   |(phi2, _) => ((OrExpr firstbool (AndExpr phi2 (NotExpr B))),BExp B) :: conBoolAgreementHelp phi1 t B
                 end
  | nil => nil
end.

Fixpoint conBoolAgreement (Theta1: TwoAssns) (Theta2: TwoAssns) (B:BExpr) :=
match Theta1 with
   h::t => match h with
                   (phi1, _) => conBoolAgreementHelp phi1 Theta2 B ++ conBoolAgreement t Theta2 B
               end
| nil => nil
  end.

Fixpoint contains (Theta : TwoAssns) (assn : TwoAssn) : bool :=
  match Theta with
  | h::t => if twoAssnEqual h assn then true else contains t assn
  | _ => false end.

Lemma containsIn : forall Theta assn, contains Theta assn=true <-> In assn Theta.
Proof.
intros. split; intros. induction Theta. inv H. simpl. simpl in H. remember (twoAssnEqual a assn).
destruct b. apply twoAssnEqual_eq2 in Heqb. auto. intuition.

induction Theta. auto. simpl in *. destruct H. subst. rewrite <- twoAssnEq_refl. auto.
intuition. remember (twoAssnEqual a assn). destruct b; auto.
Qed.

Fixpoint subtractAssns (Theta1 Theta2 :TwoAssns) : TwoAssns :=
  match Theta1 with
  | h::t => if contains Theta2 h then subtractAssns t Theta2 else h::subtractAssns t Theta2
  | _ => [] end.

Fixpoint superSet Theta1 Theta2 :=
match Theta2 with
 h::t => if contains Theta1 h then superSet Theta1 t else false
|[] => true
end.

Fixpoint vacuous (Theta: TwoAssns) : bool:=
match Theta with
  (b , _)::t => match b with (BvalExpr b2) => if(b2) then false else vacuous t
                   | _ => false end
| [] => true
end.

Fixpoint antec w Theta :=
  match Theta with
  | [] => BvalExpr false
  | (b,e)::t => if (synEq w e) then b else antec w t end.

Fixpoint antecSet w Theta : list BExpr:=
  match Theta with
  | [] => []
  | (b,e)::t => if (synEq w e) then b::(antecSet w t) else antecSet w t end.

Fixpoint antecs (Theta:TwoAssns) : list BExpr :=
  match Theta with
  | [] => []
  | (b,e)::t => b::antecs t
end.

Fixpoint skalVarListDifference L1 L2:=
match L1 with
  | [] => []
  | h::t => if (skalVarIn h L2) then skalVarListDifference t L2 else h::skalVarListDifference t L2
end.