Library varLists

Require Import language.
Require Import synEq.

Fixpoint IntersectionNull (fv: list SkalVar) (x: list SkalVar) :=
match fv with
| h::t => if (skalVarIn h x) then false else (IntersectionNull t x)
| [] => true end.

Fixpoint IntersectionNullP (fv: list SkalVar) (x: list SkalVar) :=
match fv with
| h::t => if (skalVarIn h x) then False else (IntersectionNullP t x)
| [] => True end.

Fixpoint SubtractVars a b :=
match a with
   [] => []
| h::t => if (skalVarIn h b) then SubtractVars t b else h::(SubtractVars t b)
end.

Lemma intersectionNullNilTrue : forall L1, IntersectionNullP L1 [].
intros. induction L1. simpl. auto. simpl. apply IHL1.
Qed.

Lemma intersectionNullSubset: forall x L1 L2, IntersectionNullP L1 (x::L2) -> IntersectionNullP L1 L2.
Proof.
intros. induction L1. simpl. auto. simpl in *. remember (beq_SkalVar x a). destruct b.
symmetry in Heqb. apply beq_SkalVar_eq in Heqb. subst. rewrite beq_SkalVar_refl in H.
inv H. remember (skalVarIn a L2). destruct b. remember (beq_SkalVar a x). destruct b.
inv H. inv H. apply IHL1. remember (beq_SkalVar a x). destruct b. inv H. apply H.
Qed.

Lemma intersectionNullSubset2: forall L1 L2 L3, IntersectionNullP (L1++L2) L3 -> IntersectionNullP L1 L3.
intros. induction L1. simpl. auto. simpl in *. destruct (skalVarIn a L3). inv H. apply IHL1. apply H.
Qed.

Lemma intersectionNullSubset3: forall x L1 L2, IntersectionNullP (x::L1) (L2) -> IntersectionNullP L1 L2.
Proof.
intros. generalize dependent L1. induction L2; intros. simpl in H. auto. simpl in *.
remember (beq_SkalVar x a). destruct b. inv H. remember (skalVarIn x L2). destruct b. inv H.
apply H.
Qed.

Lemma intersectionNullInNot :forall x L1 L2, In x L1 -> In x L2 -> ~IntersectionNullP L1 L2.
intuition. induction L1. inv H. induction L2. inv H0. simpl in *. remember (beq_SkalVar a a0).
destruct b. inv H1. remember (skalVarIn a L2). destruct b. inv H1. apply IHL2.
destruct H0. subst. destruct H. subst. rewrite beq_SkalVar_refl in Heqb. inv Heqb.
destruct IHL1; assumption. assumption. apply intersectionNullSubset in H1. assumption.
intros. apply IHL1; assumption.
Qed.

Lemma intersectionNullNotIn : forall x L1 L2, IntersectionNullP L1 L2 -> In x L1 ->
~ In x L2.
intros. generalize dependent L1. induction L2. intuition. intuition.
simpl in H1. destruct H1. subst. destruct L1. inv H0. simpl in H0. destruct H0. subst.
simpl in H. rewrite beq_SkalVar_refl in H. inv H.
simpl in H. destruct (beq_SkalVar s x).
inv H. destruct (skalVarIn s L2). inv H. eapply intersectionNullInNot in H. auto.
apply H0. simpl. intuition. eapply IHL2. apply intersectionNullSubset in H. apply H.
assumption. assumption.
Qed.

Lemma inSkalVarInFalse : forall x L1, ~In x L1 -> skalVarIn x L1 =false.
intros. intuition. induction L1. auto. simpl in H. simpl.
apply orb_false_iff. split. remember (beq_SkalVar a x). destruct b. destruct H.
left. symmetry in Heqb. apply beq_SkalVar_eq in Heqb. assumption. symmetry.
rewrite beq_SkalVar_sem in Heqb. auto. apply IHL1. intros. destruct H. right. auto.
Qed.

Lemma intersectionNullSymmetry : forall L1 L2 L3, IntersectionNullP (L1 ++ L2) L3 ->
IntersectionNullP (L2 ++ L1) L3.
Proof.
intros L1. induction L1; intros. simpl in H. rewrite app_nil_r. auto.
simpl in H. remember (skalVarIn a L3). destruct b. inv H. apply IHL1 in H.
induction L2. simpl. simpl in H. rewrite <- Heqb. apply H. simpl.
remember (skalVarIn a0 L3). destruct b. simpl in H. rewrite <- Heqb0 in H. inv H.
apply IHL2. rewrite <- app_comm_cons in H. apply intersectionNullSubset3 in H.
apply H.
Qed.

Lemma splitIntersectionNull : forall L1 L2 L3, IntersectionNullP (L1 ++ L2) L3 ->
IntersectionNullP (L1) L3 /\ IntersectionNullP (L2) L3.
Proof.
split; intros. induction (L1). simpl; auto. simpl. simpl in H. destruct (skalVarIn a L3).
inv H. apply (IHL1 H).
induction (L2). simpl; auto. simpl. remember (skalVarIn a L3). destruct b.
apply intersectionNullSymmetry in H. simpl in H. rewrite <- Heqb in H. inv H.
apply intersectionNullSymmetry in H. simpl in H. rewrite <- Heqb in H.
apply IHL2. apply intersectionNullSymmetry in H. apply H.
Qed.

Lemma intersectionNullSymmetry2 : forall L1 L2, IntersectionNullP L1 L2 ->
IntersectionNullP L2 L1.
intros. generalize dependent L1. induction L2; intros. simpl. auto.
simpl. remember (skalVarIn a L1). destruct b. induction L1. inv Heqb.
simpl in H. simpl in Heqb. rewrite beq_SkalVar_sem in Heqb. remember (beq_SkalVar a0 a). destruct b.
simpl in H. inv H. simpl in H. remember (skalVarIn a0 L2). destruct b. inv H.
symmetry in Heqb. apply IHL1. assumption. symmetry. assumption.
apply IHL2. apply intersectionNullSubset in H. assumption.
Qed.

Theorem intersectionNullToP : forall a b, IntersectionNull a b = true <-> IntersectionNullP a b.
Proof.
intros a. induction a; split; intros. simpl. auto.
simpl. auto. simpl in *. remember (skalVarIn a b). destruct b0. inv H. apply IHa. auto.
simpl. auto. simpl in *. remember (skalVarIn a b). destruct b0. inv H. apply IHa. auto.

Qed.

Theorem splitAllVarsIn: forall a b X, allVarsIn (a ++ b) X =true -> allVarsIn a X =true
/\ allVarsIn b X =true.
intros. split. induction a. auto. simpl. simpl in H. remember (skalVarIn a X).
destruct b0. apply IHa. apply H. inv H.
induction a. auto. simpl. simpl in H. apply IHa. remember (skalVarIn a X). destruct b0. apply H. inv H.
Qed.

Theorem allVarsInSplit:forall a b X, allVarsIn a X =true -> allVarsIn b X =true ->
 allVarsIn (a ++ b) X =true.
intros. induction a. simpl. apply H0. simpl in *. remember (skalVarIn a X). destruct b0.
apply IHa. apply H. inversion H.
Qed.

Theorem skalVarInIn: forall x X, skalVarIn x X =true <-> In x X.
split. intros. induction X. inv H.
simpl in *. remember (beq_SkalVar x a). destruct b. symmetry in Heqb. apply beq_SkalVar_eq in Heqb.
subst. left. auto.

right. apply IHX. apply H.

intros. induction X. inv H. simpl in *. destruct H. subst. rewrite beq_SkalVar_refl.
auto. destruct (beq_SkalVar x a). auto. apply IHX. auto.
Qed.

Theorem varInEither: forall X Y a, allVarsIn X (a::Y)=true <-> (forall b, In b X -> b=a \/ In b Y).
Proof.
split.
intros. induction X. inv H0. simpl in H0. destruct H0. subst. simpl in *.
remember (beq_SkalVar b a). destruct b0. symmetry in Heqb0. apply beq_SkalVar_eq in Heqb0.
subst. left. auto.
remember (skalVarIn b Y). destruct b0. right. apply skalVarInIn. auto. inv H.
simpl in *. remember (beq_SkalVar a0 a). destruct b0. destruct IHX; try assumption.
auto. auto. apply IHX. remember (skalVarIn a0 Y). destruct b0. auto.
inv H. auto.

intros. induction X. auto.
simpl in *. edestruct H. auto. subst. rewrite beq_SkalVar_refl. apply IHX. intros.
apply H. right. auto.
remember (beq_SkalVar a0 a). destruct b. apply IHX. intros. apply H. auto.
rewrite <- skalVarInIn in H0. rewrite H0. apply IHX. intros. apply H. auto.
Qed.

Theorem allVarsInRefl: forall X, allVarsIn X X = true.
intros.
induction X. simpl. auto. simpl. rewrite beq_SkalVar_refl. destruct (varInEither X X a).
eapply H0. intros. right. auto.
Qed.

Theorem allVarsInOr: forall X Y Z, allVarsIn X Z=true \/ allVarsIn X Y=true
-> allVarsIn X (Y++Z)=true.
intros X. induction X; intros. auto. destruct H. simpl. remember (skalVarIn a (Y++Z)).
destruct b. apply IHX. simpl in H. destruct (skalVarIn a Z). auto. inv H.
simpl in *. remember (skalVarIn a Z). destruct b. assert (skalVarIn a (Y++Z)=true).
apply skalVarInIn. apply in_or_app. symmetry in Heqb0. rewrite skalVarInIn in Heqb0. auto.
rewrite <- Heqb in H0. inv H0. inv H.

simpl. remember (skalVarIn a (Y++Z)).
destruct b. apply IHX. simpl in H. destruct (skalVarIn a Y). auto. inv H.
simpl in *. remember (skalVarIn a Y). destruct b. assert (skalVarIn a (Y++Z)=true).
apply skalVarInIn. apply in_or_app. symmetry in Heqb0. rewrite skalVarInIn in Heqb0. auto.
rewrite <- Heqb in H0. inv H0. inv H.
Qed.

Lemma inAllVarsInTrans: forall x X Y, In x X -> allVarsIn X Y =true -> In x Y.
intros x X. induction X; intros. inv H. simpl in H. destruct H. simpl in H0. remember (skalVarIn a Y).
destruct b. subst. symmetry in Heqb. rewrite skalVarInIn in Heqb. auto. inv H0. simpl in H0.
remember (skalVarIn a Y). destruct b. apply IHX. auto. auto. inv H0.
Qed.

Theorem allVarsInSkalVarIn: forall Y Z a, true=skalVarIn a Y -> allVarsIn Y Z = true ->
true = skalVarIn a Z.
intros Y. induction Y. intros. inv H.
intros. simpl in *. remember (beq_SkalVar a0 a). remember (skalVarIn a Z).
destruct b. destruct b0. symmetry in Heqb. apply beq_SkalVar_eq in Heqb. subst.
auto. inv H0. apply IHY. auto. destruct b0. auto. inv H0.
Qed.

Theorem allVarsInTrans: forall X Y Z, allVarsIn X Y =true -> allVarsIn Y Z = true ->
allVarsIn X Z = true.
Proof.
intros X. induction X. intros. auto.
intros. simpl in *. remember (skalVarIn a Z). remember (skalVarIn a Y). destruct b0. destruct b.
eapply IHX. eauto. auto. assert (true=skalVarIn a Z). eapply allVarsInSkalVarIn.
eauto. auto. rewrite <- Heqb in H1. inv H1.
inv H.
Qed.