(****************************************************************
   Michel St-Martin and Amy Felty
   December 2015, Coq version V8.4
                                                                 
   A Verified Algorithm for Detecting Conflicts in XACML Access
   Control Rules, Michel St-Martin and Amy P. Felty, In Proceedings of
   the Fifth ACM SIGPLAN Conference on Certified Programs and Proofs
   (CPP), January 2016.

  ***************************************************************)

Require Export Srac.

(* The action for a rule to take if it applies*)
Inductive effect: Set := permit | deny.

(* A rule is made up of 4 srac (formulas), and an access action to take *)
Record rule: Set := ruleCons {
  eff: effect;
  rules: srac
}.

(* is true iff the rule applies, and its access action is permit *)
Definition rule_permit (rq : list reqValue) (rl : rule) : Prop :=
  eff rl = permit /\
  sracMatch rq (rules rl) = T.

(* is true iff the rule applies, and its access action is deny *) 
Definition rule_deny (rq : list reqValue) (rl : rule) : Prop :=
  eff rl = deny /\
  sracMatch rq (rules rl) = T.

(* there is a conflict between 2 rules, one permits a request
   the other denies the same request *)
Definition rule_conflict (r1 r2: rule) : Prop := 
  exists rq:list reqValue, (rule_permit rq r1 /\ rule_deny rq r2) \/
                    (rule_deny rq r1 /\ rule_permit rq r2).

Fixpoint nonEmptyRule (lc : list (core*nat)) : trilean :=
match lc with
| nil => T
| (c,n):: lc' => nonEmptyCore c /\t nonEmptyRule lc'
end.

Fixpoint lCheck (l1 : list (list (core*nat))) (l2 : list (core*nat)) : trilean :=
match l1 with
| nil => F
| l :: l1' => nonEmptyRule (merge l l2) \/t lCheck l1' l2
end.

Fixpoint llCheck (l1 l2: list (list (core*nat))) : trilean :=
match l2 with
| nil => F
| l :: l2' => lCheck l1 l \/t llCheck l1 l2'
end.

Definition effectDiff: effect -> effect -> bool :=
fun a1 a2 =>
match a1, a2 with
permit, deny => true
| deny, permit => true
| _, _ => false
end.

Definition trileanTrue (t:trilean) : bool :=
match t with
| T => true
| _ => false
end.

Definition type2 (reqv : reqValue) : reqValue :=
match reqv with
| timeReq _ => timeReq Z'NM0
| intReq _ => intReq 0
| blank => blank
end.

Fixpoint changeNth (n : nat) (lr : list reqValue) (rv: reqValue) :list reqValue :=
match n with
| O => 
  match lr with
  | nil => rv :: nil
  | _ :: lr' => rv :: lr'
  end
| S n' =>
  match lr with
  | nil => blank :: changeNth n' nil rv
  | rv2 :: lr' => rv2 :: changeNth n' lr' rv
  end
end.

Fixpoint validCoresCN' (lc : list (core*nat)) (c1 : core) (n1 : nat) : bool :=
match lc with
| nil => true
| (c2, n2) :: lc' => (if beq_nat n1 n2 then negb (typeDiff (type c1) (type c2)) else true) && validCoresCN' lc' c1 n1
end.

Fixpoint validCoresCN (llc : list (list (core*nat))) (c : core) (n : nat) : bool :=
match llc with
| nil => true
| lc :: llc' => validCoresCN' lc c n && validCoresCN llc' c n
end.

Fixpoint validCoresLc (llc : list (list (core*nat))) (lc : list (core*nat)) : bool :=
match lc with
| nil => true
| (c, n) :: lc' => negb (invalidArgs c) && validCoresCN llc c n && validCoresLc llc lc'
end.

Fixpoint validCores (llc : list (list (core*nat))) : bool :=
match llc with
| nil => true
| lc :: llc' => validCoresLc llc' lc && validCores llc'
end.

Definition conflict_check: rule -> rule -> bool :=
fun r1 r2 =>
match r1 with (ruleCons e1 s1) =>
match r2 with (ruleCons e2 s2) =>
effectDiff e1 e2 && trileanTrue(llCheck (toLists s1) (toLists s2)) &&
  validCores (toLists s1) && validCores (toLists s2)
end
end.

Fixpoint sorted (lc : list (core*nat)) : bool :=
match lc with
| nil => true
| (_,n1)::lc' => 
  match lc' with
  | nil => true
  | (_,n2)::lc'' => blt_nat n1 n2 && sorted lc'
  end
end.

Lemma ltboolIsLt: forall n m:nat, blt_nat n m = true -> n < m.
Proof.
induction n; destruct m;
auto with *.
Qed.

Lemma ltboolIsLt2: forall n m:nat, blt_nat n m = false -> n < m -> False.
Proof.
induction n; destruct m;
auto with *.
simpl.
intros.
apply (IHn m H).
omega.
Qed.

Definition P4 (i: nat) : Prop := forall (c1 c2 : core) (n1 n2 : nat) (lc : list (core*nat)), length lc = i -> 
sorted ((c1,n1)::lc) = true -> In (c2, n2) lc -> n1 < n2.

Lemma minIsFirstBase : P4 0.
Proof.
unfold P4.
intros.
destruct lc.
simpl in H1.
tauto.

simpl in H; omega.
Qed.

Lemma minIsFirstRec : forall (i : nat), (forall j : nat, j <= i -> P4 j) -> P4 (S i).
Proof.
unfold P4.
intros.
destruct lc.
simpl in H0; omega.

simpl in H2.
destruct H2.
rewrite H2 in *.
simpl in H1.
caseSimpl (blt_nat n1 n2); [|auto with *].
apply (ltboolIsLt _ _ C).

assert (i <= i); [omega|].
apply (H i H3 c1 c2 n1 n2 lc); trivial.
auto.

clear -H1.
simpl in *.
destruct p.
destruct lc.
trivial.
destruct p.
simpl in *.

caseSimpl (blt_nat n1 n); [|auto with *].
caseSimpl (blt_nat n n0); [|auto with *].
simpl in H1.
caseSimpl (blt_nat n1 n0).
trivial.

generalize (ltboolIsLt _ _ C).
generalize (ltboolIsLt _ _ C0).
generalize (ltboolIsLt2 _ _ C1).
omega.
Qed.

Lemma minIsFirst : forall (c1 c2 : core) (n1 n2 : nat) (lc : list (core*nat)), 
sorted ((c1,n1)::lc) = true -> In (c2, n2) lc -> n1 < n2.
Proof.
intros.
generalize (strongind P4); intro.
unfold P4 in H1 at 4.
apply (H1 minIsFirstBase minIsFirstRec (length lc) c1 c2 n1 n2 lc); trivial.
Qed.

Lemma allSorted : forall (cn : core * nat) (lc : list (core * nat)), sorted (cn :: lc) = true -> sorted lc = true.
Proof.
intros.
simpl in H.
destruct cn.
destruct lc.
trivial.
destruct p.
destruct (blt_nat n n0).
trivial.
auto with *.
Qed.

Lemma sortedListCEqual : forall (lc : list (core*nat)) (c1 c2 : core) (n : nat),
sorted lc = true -> In (c1, n) lc -> In (c2, n) lc -> c1 = c2.
Proof.
intros.
induction lc.
auto with *.
destruct H0.
subst a.
destruct H1.
inversion H0.
trivial.
generalize (minIsFirst _ _ _ _ _ H H0).
omega.
destruct H1.
subst a.
generalize (minIsFirst _ _ _ _ _ H H0).
omega.
apply IHlc; trivial.
apply (allSorted _ _ H).
Qed.

Lemma validCoresCN'Types : forall (lc : list (core*nat)) (c1 c2 : core) (n1 : nat),
validCoresCN' lc c1 n1 = true -> In (c2, n1) lc -> type c1 = type c2.
Proof.
intros.
induction lc.
auto with *.
simpl in H.
destruct H0.
subst a.
rewrite <- (beq_nat_refl n1) in H.
destruct c1, c2; try destruct r; try destruct r0; simpl in *; trivial; discriminate.
destruct a.
destruct (andbSplit _ _ H).
apply IHlc; trivial.
Qed.

Lemma validCoresCNTypes : forall (llc : list (list (core*nat))) (lc : list (core*nat)) (c1 c2 : core) (n1 : nat),
validCoresCN llc c1 n1 = true -> In (c2, n1) lc -> In lc llc -> type c1 = type c2.
Proof.
intros.
induction llc.
auto with *.
simpl in H.
destruct (andbSplit _ _ H).
destruct H1.
subst a.
apply (validCoresCN'Types lc _ _ n1); trivial.
apply IHllc; trivial.
Qed.

Lemma validCoresLcTypes : forall (llc : list (list (core*nat))) (l1 l2 : list (core*nat)) (c1 c2 : core) (n1 : nat),
validCoresLc llc l1 = true -> In (c1, n1) l1 -> In (c2, n1) l2 -> In l2 llc -> type c1 = type c2.
Proof.
intros.
induction l1.
auto with *.
simpl in H.
destruct a.
destruct (andbSplit _ _ H); clear H.
destruct (andbSplit _ _ H3); clear H3.
destruct H0.
inversion H0; clear H0.
subst c1; subst n1.
apply (validCoresCNTypes llc l2 _ _ n); trivial.
apply IHl1; trivial.
Qed.

Lemma validCoresTypes : forall (llc : list (list (core*nat))) (l1 l2 : list (core*nat)) (c1 c2 : core) (n : nat),
validCores llc = true -> sorted l1 = true -> In (c1, n) l1 -> In (c2, n) l2 -> In l1 llc -> In l2 llc -> type c1 = type c2.
Proof.
intros.
induction llc.
auto with *.
simpl in H.
destruct (andbSplit _ _ H); clear H.
destruct H3.
subst a.
destruct H4.
subst l1.
rewrite (sortedListCEqual _ _ _ _ H0 H1 H2).
trivial.
apply (validCoresLcTypes llc l1 l2 _ _ n); trivial.

destruct H4.
subst a.
rewrite (validCoresLcTypes llc l2 l1 c2 c1 n); trivial.
tauto.
Qed.

Lemma validCoresLcArgs : forall (llc : list (list (core*nat))) (lc: list (core*nat)) (c : core) (n : nat),
validCoresLc llc lc = true -> In (c, n) lc -> invalidArgs c = false.
Proof.
intros.
induction lc.
auto with *.
simpl in H.
destruct a.
destruct (andbSplit _ _ H); clear H.
destruct (andbSplit _ _ H1); clear H1.
destruct H0.
inversion H0; clear H0.
subst c0; subst n0.
apply negb_true_iff.
trivial.
apply IHlc; trivial.
Qed.

Lemma validCoresArgs : forall (llc : list (list (core*nat))) (lc: list (core*nat)) (c : core) (n : nat),
validCores llc = true -> In (c, n) lc -> In lc llc -> invalidArgs c = false.
Proof.
intros.
induction llc.
auto with *.
simpl in H.
destruct (andbSplit _ _ H); clear H.
destruct H1.
subst a.
apply (validCoresLcArgs llc lc _ n); trivial.
apply IHllc; trivial.
Qed.

Lemma orT : forall (t1 t2: trilean), (t1 \/t t2) = T -> t1 = T \/ t2 = T.
Proof.
intros.
caseSimpl t1; caseSimpl t2; tauto.
Qed.

Lemma andT : forall (t1 t2: trilean), (t1 /\t t2) = T -> t1 = T /\ t2 = T.
Proof.
intros.
caseSimpl t1; caseSimpl t2; try tauto; discriminate.
Qed.

Lemma orNA : forall (t1 t2: trilean), (t1 \/t t2) = NA -> t1 = NA \/ t2 = NA.
Proof.
intros.
caseSimpl t1; caseSimpl t2; try tauto; discriminate.
Qed.

Lemma andT2 : forall (t1 t2: trilean), t1 = T -> t2 = T -> (t1 /\t t2) = T.
Proof.
intros.
rewrite H, H0.
trivial.
Qed.

Lemma orT2 : forall (t1 t2: trilean), t1 = T -> t2 <> NA -> (t1 \/t t2) = T.
Proof.
intros.
rewrite H.
caseSimpl t2; trivial.
tauto.
Qed.

Lemma andNA : forall (t1 t2: trilean), (t1 /\t t2) = NA -> t1 = NA \/ t2 = NA.
Proof.
intros.
caseSimpl t1; caseSimpl t2; try tauto; discriminate.
Qed.

Lemma orNotNa : forall (t1 t2 : trilean), t1 <> NA -> t2 <> NA -> (t1 \/t t2) <> NA.
Proof.
intros.
destruct t1, t2; trivial.
Qed.

Lemma andNotNa2 : forall (t1 t2 : trilean), (t1 /\t t2) <> NA -> t1 <> NA /\ t2 <> NA.
Proof.
intros.
destruct t1, t2; split; trivial; discriminate.
Qed.

Lemma orNotNa2 : forall (t1 t2 : trilean), (t1 \/t t2) <> NA -> t1 <> NA /\ t2 <> NA.
Proof.
intros.
destruct t1, t2; split; trivial; discriminate.
Qed.

Fixpoint afterN (lr : list reqValue) (n : nat): list reqValue :=
match lr with
| nil => nil
| rv::lr' =>
  match n with
  | O => lr'
  | S n' => afterN lr' n'
  end
end.

Definition P5 (i: nat) : Prop := forall (n : nat) (lr : list reqValue) (rv: reqValue),  length lr = i -> 
afterN (changeNth n lr rv) n = afterN lr n.

Lemma endOfChangeNthBase : P5 0.
Proof.
unfold P5.
intros.
destruct lr.
simpl.
induction n.
trivial.
trivial.
simpl in H; omega.
Qed.

Lemma endOfChangeNthRec : forall (i : nat), (forall j : nat, j <= i -> P5 j) -> P5 (S i).
Proof.
unfold P5.
intros.
destruct lr.
simpl in H0; omega.

destruct n; simpl.
trivial.
apply (H i); trivial.
auto.
Qed.

Lemma endOfChangeNth : forall (n : nat) (lr : list reqValue) (rv: reqValue), afterN (changeNth n lr rv) n = afterN lr n.
Proof.
intros.
generalize (strongind P5); intro.
apply (H endOfChangeNthBase endOfChangeNthRec (length lr)); trivial.
Qed.

Definition P6 (i: nat) : Prop := forall (n m : nat) (lr : list reqValue) (rv: reqValue),  length lr = i -> 
n < m -> nth m lr blank = nth (m-n-1) (afterN lr n) blank.

Lemma mthAfterNBase : P6 0.
Proof.
unfold P6.
intros.
destruct lr.
simpl.
destruct m.
omega.
destruct (S m - n - 1); trivial.

simpl in H; omega.
Qed.

Lemma mthAfterNRec : forall (i : nat), (forall j : nat, j <= i -> P6 j) -> P6 (S i).
Proof.
unfold P6.
intros.
destruct lr.
simpl in H0; omega.

destruct m; simpl.
omega.

destruct n.
simpl.
destruct m; trivial.

apply (H i); trivial.
auto.
omega.
Qed.

Lemma mthAfterN :  forall (n m: nat) (lr : list reqValue) (rv: reqValue),  
n < m -> nth m lr blank = nth (m-n-1) (afterN lr n) blank.
Proof.
intros.
generalize (strongind P6); intro.
apply (H0 mthAfterNBase mthAfterNRec (length lr)); trivial.
Qed.

Lemma changeNthLeavesEnd : forall (n m : nat) (lr : list reqValue) (rv: reqValue), n < m ->
(nth m (changeNth n lr rv) blank) = (nth m lr blank).
Proof.
intros.
rewrite (mthAfterN n m lr rv H).
rewrite  <- (endOfChangeNth n lr rv).
apply (mthAfterN n m (changeNth n lr rv) rv H).
Qed.

Definition P7 (i: nat) : Prop := forall (n : nat) (lr : list reqValue) (rv: reqValue), length lr = i -> 
(nth n (changeNth n lr rv) blank) = rv.

Lemma nthOfChangeNthBase : P7 0.
Proof.
unfold P7.
intros.
destruct lr.
induction n; trivial.

simpl in H; omega.
Qed.

Lemma nthOfChangeNthRec : forall (i : nat), (forall j : nat, j <= i -> P7 j) -> P7 (S i).
Proof.
unfold P7.
intros.
destruct lr.
simpl in H0; omega.

destruct n.
trivial.
simpl.

apply (H i); trivial.
auto.
Qed.

Lemma nthOfChangeNth :  forall (n : nat) (lr : list reqValue) (rv: reqValue),
(nth n (changeNth n lr rv) blank) = rv.
Proof.
intros.
generalize (strongind P7); intro.
apply (H nthOfChangeNthBase nthOfChangeNthRec (length lr)); trivial.
Qed.

Lemma allNonEmpty : forall (a : core * nat) (lc : list (core * nat)),  nonEmptyRule (a :: lc) = T ->  nonEmptyRule lc = T.
Proof.
intros.
simpl in H.
destruct a.
destruct (nonEmptyCore c); trivial;
destruct (nonEmptyRule lc); discriminate H.
Qed.

Lemma sortedWithout2nd : forall (a b : core * nat) (lc : list (core * nat)), sorted (a :: b :: lc) = true -> sorted (a :: lc) = true.
Proof.
intros.
simpl in *.
destruct a.
destruct b.
destruct lc.
trivial.
destruct p.

caseSimpl (blt_nat n n0); [|auto with *].
caseSimpl (blt_nat n0 n1); [|auto with *].
simpl in H.
caseSimpl (blt_nat n n1).
trivial.

generalize (ltboolIsLt _ _ C).
generalize (ltboolIsLt _ _ C0).
generalize (ltboolIsLt2 _ _ C1).
omega.
Qed.

Lemma nonEmptySound : forall lc : list (core*nat), sorted lc = true -> nonEmptyRule lc = T -> 
exists lr : list reqValue, lMatch lc lr = T.
Proof.
intros.
induction lc; simpl.
exists nil.
trivial.
generalize (IHlc (allSorted a lc H) (allNonEmpty a lc H0)); intro.
clear IHlc.
destruct a.

simpl in H0.
caseSimpl (nonEmptyCore c); try (destruct (nonEmptyRule lc); discriminate H0).
generalize (nonEmpty' c C); intro.

destruct H1, H2.

exists (changeNth n x x0).
rewrite nthOfChangeNth.
rewrite H2.
simpl.

clear -H H1.
induction lc; trivial.
generalize (sortedWithout2nd _ _ _ H); intro.

simpl in H, H1.
simpl.
destruct a.
caseSimpl (blt_nat n n0); [| auto with *].
rewrite (changeNthLeavesEnd n n0 x x0 (ltboolIsLt _ _ C)).
caseSimpl (coreMatch (nth n0 x blank) c0); caseSimpl (lMatch lc x); simpl in H1; try discriminate H1.
simpl.
apply IHlc;
trivial.
Qed.

Definition P8 (i: nat) : Prop := forall (l1 l2 : list (core*nat)), length l1 + length l2 = i -> 
sorted l1 = true -> sorted l2 = true -> sorted (merge l1 l2) = true.

Lemma mergeSortedBase : P8 0.
Proof.
unfold P8.
intros.
destruct l1; destruct l2; simpl in *; trivial;
omega.
Qed.

Ltac foldMerge c n l1 l2 := 
assert (((fix merge_aux (l0 : list (core * nat)) : list (core * nat) :=
            match l0 with
            | nil => (c, n) :: l1
            | (c0, n2) :: l2' =>
                if blt_nat n n2
                then (c, n) :: merge l1 l0
                else
                 if beq_nat n n2
                 then (coreCheck c c0, n) :: merge l1 l2'
                 else (c0, n2) :: merge_aux l2'
            end) l2) = merge ((c, n) :: l1) l2) as temp; trivial;
rewrite temp in *; clear temp.

Lemma mergeSortedRec : forall (i : nat), (forall j : nat, j <= i -> P8 j) -> P8 (S i).
Proof.
unfold P8.
intros.
destruct l1; destruct l2; trivial.
destruct p; trivial.
destruct p, p0.
simpl.

caseSimpl (blt_nat n n0).
simpl.
rewrite (H i); trivial.
destruct l1.
simpl.
auto with *.
destruct p.
simpl.
caseSimpl (blt_nat n1 n0).
simpl in H1.
caseSimpl (blt_nat n n1); auto with *.
caseSimpl (beq_nat n1 n0).
simpl in H1.
caseSimpl (blt_nat n n1); auto with *.
auto with *.
simpl in *; omega.
apply (allSorted (c,n)); trivial.

caseSimpl (beq_nat n n0).
rewrite <- (beq_nat_true _ _ C0) in *.
simpl.
rewrite (H (i-1)); trivial; try solve [simpl in *; omega].
destruct l1; destruct l2; simpl; trivial. 
destruct p.
simpl in H2.
caseSimpl (blt_nat n n1); auto with *.
destruct p.
simpl in H1.
caseSimpl (blt_nat n n1); auto with *.
destruct p, p0.
caseSimpl (blt_nat n1 n2).
simpl in H1.
caseSimpl (blt_nat n n1); auto with *.
caseSimpl (beq_nat n1 n2).
simpl in H1.
caseSimpl (blt_nat n n1); auto with *.
simpl in H2.
caseSimpl (blt_nat n n2); auto with *.
apply (allSorted (c,n)); trivial.
apply (allSorted (c0,n)); trivial.

assert (n0 < n).
generalize (ltboolIsLt2 _ _ C);
generalize (beq_nat_false _ _ C0); intros.
omega.
assert (blt_nat n0 n = true).
caseSimpl (blt_nat n0 n); trivial.
contradiction (ltboolIsLt2 _ _ C1 H3).
simpl.
foldMerge c n l1 l2.
rewrite (H i); trivial; try solve [simpl in *; omega].

destruct l2.
simpl.
auto with *.
simpl.
destruct p.
caseSimpl (blt_nat n n1); auto with *.
caseSimpl (beq_nat n n1); auto with *.
simpl in H2.
caseSimpl (blt_nat n0 n1); auto with *.
apply (allSorted (c0,n0)); trivial.
Qed.

Lemma mergeSorted : forall (l1 l2 : list (core*nat)),
sorted l1 = true -> sorted l2 = true -> sorted (merge l1 l2) = true.
Proof.
intros.
generalize (strongind P8); intro.
apply (H1 mergeSortedBase mergeSortedRec (length l1 + length l2)); trivial.
Qed.

Lemma split'Sorted : forall (s : srac), sorted (split' s) = true.
Proof.
intros.
induction s; simpl; trivial.
apply mergeSorted; trivial.
Qed.

Lemma inLCN : forall (s : srac) (lcn : list (core*nat)), In lcn (toLists s) -> exists (s':srac), lcn = split' s'.
Proof.
intros.
unfold toLists in H.
induction (convertDNF s); simpl in *.
destruct H; [|contradiction].
rewrite <- H.
exists (single c n).
trivial.

destruct H; [|contradiction].
rewrite <- H.
exists (and s0_1 s0_2).
trivial.

generalize (in_app_or _ _ _ H); intros.
destruct H0; tauto.

destruct H; [|contradiction].
rewrite <- H.
exists (not s0).
trivial.
Qed.

Lemma sortedLists : forall (s : srac) (lcn : list (core*nat)), In lcn (toLists s) -> sorted lcn = true.
Proof.
intros.
destruct (inLCN _ _ H).
rewrite H0.
apply split'Sorted.
Qed.

Lemma nonEmptyNa : forall (lc : list (core*nat)), nonEmptyRule lc = NA -> exists (c: core) (n:nat), invalidArgs c = true /\ In (c,n) lc.
Proof.
intros.
induction lc.
discriminate H.
simpl in *.
destruct a.
destruct (andNA _ _ H).
exists c, n.
split; [|tauto].
caseSimpl (invalidArgs c); trivial.
unfold nonEmptyCore in H0.
destruct c; rewrite C in H0; discriminate.
destruct (IHlc H0).
destruct H1.
exists x, x0.
tauto.
Qed.

Lemma coreMatchNa : forall (c :core) (rv : reqValue), coreMatch rv c = NA -> 
invalidArgs c = true \/ rv = blank \/ typeDiff (type c) rv = true.
Proof.
intros.
unfold coreMatch in H.
caseSimpl (invalidArgs c).
tauto.
right.

caseSimpl (typeDiff (type c) rv).
tauto.
left.
destruct rv; trivial; exfalso;
destruct c; try destruct r; try discriminate.
caseSimpl (z0 <=b z /\b z <b z1); discriminate.
caseSimpl (z0 <=b z /\b z <=b z1); discriminate.
caseSimpl (z0 <b z); discriminate.
caseSimpl (z <b z0); discriminate.
Qed.

Lemma coreMatchNa2 : forall (c :core) (rv : reqValue), 
invalidArgs c = true \/ rv = blank \/ typeDiff (type c) rv = true -> coreMatch rv c = NA.
Proof.
intros.
unfold coreMatch.
caseSimpl (invalidArgs c); trivial.
destruct H.
discriminate H.

destruct H.
rewrite H; trivial.
unfold typeDiff in H.
destruct rv; destruct c; try destruct r; trivial; discriminate.
Qed.

Lemma lCheckNa : forall (l1 : list (list (core*nat))) (l2 : list (core*nat)), lCheck l1 l2 = NA -> 
exists (lc : list (core*nat)) (c: core) (n:nat), invalidArgs c = true /\ In (c,n) (merge lc l2) /\ In lc l1. 
Proof.
intros.
induction l1.
discriminate H.
simpl in *.
destruct (orNA _ _ H).
destruct (nonEmptyNa _ H0).
destruct H1, H1.
exists a, x, x0.
tauto.

destruct (IHl1 H0).
destruct H1, H1.
exists x, x0, x1.
tauto.
Qed.

Lemma blankInvalid : forall (c : core), type c = blank -> invalidArgs c = true.
Proof.
intros.
unfold invalidArgs.
destruct c; try destruct r; trivial; discriminate.
Qed.

Lemma lMatchNa : forall (lc : list (core*nat)) (lr : list reqValue), lMatch lc lr = NA -> 
exists (c: core) (n:nat), In (c,n) lc /\ 
(invalidArgs c = true \/ typeDiff (type c) (nth n lr blank) = true).
Proof.
intros.
induction lc.
discriminate H.
simpl in *.
destruct a.
destruct (andNA _ _ H).

exists c, n.
destruct (coreMatchNa _ _ H0).
tauto.

destruct H1.
rewrite H1 in *.
caseSimpl (type c);
try tauto.
rewrite (blankInvalid _ C).
tauto.
tauto.

destruct (IHlc H0).
destruct H1, H1.
exists x, x0.
tauto.
Qed.

Lemma lMatchNa2 : forall (lc : list (core*nat)) (lr : list reqValue),  
(exists (c: core) (n:nat), In (c,n) lc /\ (invalidArgs c = true \/ typeDiff (type c) (nth n lr blank) = true)) ->
lMatch lc lr = NA.
Proof.
intros.
destruct H, H, H.
induction lc.
auto with *.

simpl in *.
destruct H.
subst a.
rewrite (coreMatchNa2 x (nth x0 lr blank)); trivial.
tauto.
rewrite (IHlc H).
destruct a.
destruct (coreMatch (nth n lr blank) c); trivial.
Qed.

Lemma coreCheckNA : forall (c1 c2 : core), invalidArgs (coreCheck c1 c2) = true ->
invalidArgs c1 = true \/ invalidArgs c2 = true \/ typeDiff (type c1) (type c2) = true.
Proof.
intros.
caseSimpl (invalidArgs c1); [tauto|].
right.
caseSimpl (invalidArgs c2); [tauto|].
right.
caseSimpl (typeDiff (type c1) (type c2)); [tauto|].
generalize (coreCheckNotNa _ _ C C0 C1).
intuition.
destruct H0.

unfold coreCheck in *.
induction c1; induction c2;
try destruct r; try destruct r0; trivial; try discriminate;
simpl in *;
repeat findIf; trivial;
try discriminate H; simpl in *;
unfold min', max' in *;
unfold min, Core.max in *;
repeat findIf;
b2PH; omega.
Qed.

Definition P9 (i: nat) : Prop := forall (l1 l2 : list (core*nat)) (c: core) (n:nat), length l1 + length l2 = i -> 
invalidArgs c = true -> In (c,n) (merge l1 l2) -> (exists (c': core), invalidArgs c' = true /\ (In (c',n) l1 \/ In (c',n) l2)) \/
exists (c1 c2 : core), typeDiff (type c1) (type c2) = true /\ In (c1, n) l1 /\ In (c2, n) l2.

Lemma mergeNABase : P9 0.
Proof.
unfold P9.
intros.
destruct l1, l2; simpl in *; try omega.
Qed.

Lemma mergeNARec : forall (i : nat), (forall j : nat, j <= i -> P9 j) -> P9 (S i).
Proof.
unfold P9.
intros.
destruct l1.
simpl in *.
left.
exists c.
induction l2; tauto.

destruct l2.
simpl in *.
destruct p.
left.
exists c.
tauto.
simpl in H2.
destruct p, p0.
caseSimpl (blt_nat n0 n1).
simpl in *.
destruct H2.
rewrite H2.
left.
exists c.
tauto.
simpl in H0.
destruct (H i (le_n i) l1 ((c1, n1) :: l2) c n); trivial.
simpl in *; omega.
destruct H3, H3.
left.
exists x.
tauto.
destruct H3, H3, H3.
right.
exists x, x0.
tauto.

caseSimpl (beq_nat n0 n1).
rewrite <- (beq_nat_true _ _ C0).
simpl in H1.
destruct H2.
inversion H2.
rewrite <- H4 in H1.
destruct (coreCheckNA _ _ H1).
left.
exists c0.
auto with *.
destruct H3.
left.
exists c1.
auto with *.
right.
exists c0, c1.
rewrite H5 in *.
auto with *.

simpl in *.
assert (i-1 <= i); [omega|].
destruct (H (i-1) H3 l1 l2 c n); trivial.
omega.
destruct H4, H4.
left.
exists x.
tauto.
destruct H4, H4, H4.
right.
exists x, x0.
tauto.

simpl in *.
foldMerge c0 n0 l1 l2.
destruct H2.
rewrite H2.
left.
exists c.
tauto.

destruct (H i (le_n i) ((c0, n0) :: l1) l2 c n); trivial.
simpl in *; omega.
destruct H3, H3.
left.
exists x.
tauto.
destruct H3, H3, H3.
right.
exists x, x0.
tauto.
Qed.

Lemma mergeNA : forall (l1 l2 : list (core*nat)) (c: core) (n:nat), 
invalidArgs c = true -> In (c,n) (merge l1 l2) -> (exists (c': core), invalidArgs c' = true /\ (In (c',n) l1 \/ In (c',n) l2)) \/
exists (c1 c2 : core), typeDiff (type c1) (type c2) = true /\ In (c1, n) l1 /\ In (c2, n) l2.
Proof.
intros.
generalize (strongind P9 mergeNABase mergeNARec); intro.
unfold P9 in H1.
apply (H1 (length l1 + length l2) _ _ c n); trivial.
Qed.

Lemma lCheckAndMatchNa : forall (l1 : list (list (core*nat))) (l2 : list (core*nat)) (lr : list reqValue), 
lCheck l1 l2 = NA -> llMatch l1 lr = NA \/ lMatch l2 lr = NA.
Proof.
intros.
destruct (lCheckNa _ _ H).
destruct H0, H0, H0.
destruct H1.
destruct (mergeNA _ _ _ _ H0 H1).
destruct H3, H3.
destruct H4.
left.

clear -H2 H3 H4.
induction l1.
auto with *.
simpl in *.
destruct H2.
rewrite H in *.
cut (lMatch x lr = NA).
intro; rewrite H0.
trivial.
apply lMatchNa2.
exists x2, x1.
tauto.
rewrite (IHl1 H).
caseSimpl (lMatch a lr); trivial.

right.
apply lMatchNa2.
exists x2, x1.
tauto.

destruct H3, H3, H3.
destruct H4.
clear -H2 H3 H4 H5.
induction l1.
auto with *.
simpl in *.
destruct H2.
subst a.

caseSimpl (typeDiff (type x2) (nth x1 lr blank)).
rewrite lMatchNa2.
tauto.
exists x2, x1.
tauto.

caseSimpl (typeDiff (type x3) (nth x1 lr blank)).
right.
rewrite lMatchNa2.
tauto.
exists x3, x1.
tauto.

destruct (type x2), (type x3), (nth x1 lr blank); discriminate.
destruct (IHl1 H).
rewrite H0.
destruct (lMatch a lr); tauto.
tauto.
Qed.

Lemma lMatchTrue : forall (lc : list (core*nat)) (lr : list reqValue) (c : core) (n : nat), 
lMatch lc lr = T -> sorted lc = true -> In (c, n) lc  -> coreMatch (nth n lr blank) c = T.
Proof.
intros.
induction lc.
auto with *.
generalize (allSorted _ _ H0); intro.
destruct H1.
simpl in H.
subst a.
destruct (andT _ _ H).
rewrite H1.
trivial.
simpl in H.
destruct a.
destruct (andT _ _ H).
apply IHlc; trivial.
Qed.

Lemma lMatchTrue2 : forall (lc : list (core*nat)) (lr : list reqValue), sorted lc = true -> 
(forall (c : core) (n : nat), In (c, n) lc  -> coreMatch (nth n lr blank) c = T) -> lMatch lc lr = T.
Proof.
intros.
induction lc.
trivial.
simpl.
destruct a.
generalize (allSorted _ _ H); intro.
simpl.
rewrite (H0 c n); auto with *.
Qed.

Lemma typeDiffXXFalse : forall (rv : reqValue), typeDiff rv rv = false.
Proof.
intros.
destruct rv; trivial.
Qed.

Lemma type2Type : forall (c : core), type2 (type c) = type c.
Proof.
intros.
destruct c; try destruct r; trivial.
Qed.

Lemma nonEmptyNotNa: forall (lc : list (core * nat)) (c : core) (n : nat),
nonEmptyRule lc <> NA -> In (c, n) lc -> invalidArgs c = false.
Proof.
intros.
induction lc.
auto with *.
simpl in *.
destruct H0;
[subst a|destruct a];
destruct (andNotNa2 _ _ H).
clear IHlc H H1.
unfold nonEmptyCore in H0.
caseSimpl (invalidArgs c); trivial.
destruct c; rewrite C in H0; tauto.
tauto.
Qed.

Lemma inOrNot : forall (lc : list (core*nat)) (n : nat), (exists c : core, In (c, n) lc) \/ forall c : core, ~ In (c, n) lc.
Proof.
intros.
induction lc.
right.
tauto.

destruct IHlc.
left.
destruct H.
exists x.
auto with *.

destruct a.
caseSimpl (beq_nat n n0).
rewrite <- (proj1 (beq_nat_true_iff n n0)); trivial.
left.
exists c.
auto with *.

right.
intros.
simpl.
intuition.
injection H1.
intros.
subst n0.
rewrite NPeano.Nat.eqb_refl in C.
discriminate.
apply (H c0 H1).
Qed.

Fixpoint maxNLc (lc :list (core*nat)) : nat :=
match lc with
| nil => 0
| (c, n)::lc' => Peano.max n (maxNLc lc')
end.

Fixpoint maxN (llc : list (list (core*nat))) : nat :=
match llc with
| nil => 0
| lc::llc' => Peano.max (maxNLc lc) (maxN llc')
end.

Lemma maxNIsMax : forall (llc : list (list (core*nat))) (n : nat) (lc : list (core*nat)) (c:core),
In (c, n) lc -> In lc llc -> n <= maxN llc.
intros.
induction llc.
auto with *.
destruct H0.
subst a.
simpl.

cut (n <= maxNLc lc).
intro.
generalize (NPeano.Nat.le_max_l (maxNLc lc) (maxN llc)).
omega.
clear IHllc.
induction lc.
auto with *.
destruct H.
subst a.
simpl.
auto with *.
simpl.
destruct a.
generalize (NPeano.Nat.le_max_r n0 (maxNLc lc)).
intro.
generalize (IHlc H).
omega.

simpl.
generalize (IHllc H0); intro.
generalize (NPeano.Nat.le_max_r (maxNLc a) (maxN llc)).
omega.
Qed.

Fixpoint getNLc (lc : list (core*nat)) (n : nat) : (bool*reqValue) :=
match lc with
| nil => (false, blank)
| (c, n0) :: lc' => if beq_nat n n0 then (true, type c) else getNLc lc' n
end.

Definition getBool (br : bool*reqValue) :=
match br with
| (b, r) => b
end.

Definition getReq (br : bool*reqValue) :=
match br with
| (b, r) => r
end.

Fixpoint getN (llc : list (list (core*nat))) (n : nat) : (bool*reqValue) :=
match llc with
| nil => (false, blank)
| lc :: llc' => let hn := getNLc lc n in if getBool hn then hn else getN llc' n
end.

Lemma getNLcTrue : forall (lc : list (core*nat)) (c : core) (n : nat), In (c, n) lc -> getBool (getNLc lc n) = true.
Proof.
intros.
induction lc.
auto.
destruct H.
subst a.
simpl.
rewrite NPeano.Nat.eqb_refl.
trivial.
simpl.
destruct a.
destruct (beq_nat n n0); trivial.
tauto.
Qed.

Lemma getNLcTrue2 : forall (lc : list (core*nat)) (n : nat), getBool (getNLc lc n) = true -> exists (c : core), In (c, n) lc.
Proof.
intros.
induction lc.
discriminate.
simpl in *.
destruct a.
caseSimpl (beq_nat n n0).
rewrite (beq_nat_true _ _ C).
exists c.
tauto.

destruct (IHlc H).
exists x.
tauto.
Qed.

Lemma getNTrue : forall (llc : list (list (core*nat))) (lc : list (core*nat)) (c : core) (n : nat), 
In (c, n) lc -> In lc llc -> getBool (getN llc n) = true.
Proof.
intros.
induction llc.
auto.
destruct H0.
subst a.
simpl.
rewrite (getNLcTrue _ _ _ H).
apply (getNLcTrue _ _ _ H).
simpl.
caseSimpl (getBool (getNLc a n)).
trivial.
tauto.
Qed.

Lemma getNTrue2 : forall (llc : list (list (core*nat))) (n : nat), getBool (getN llc n) = true -> 
exists (lc : list (core*nat)) (c : core), In (c, n) lc /\ In lc llc.
Proof.
intros.
induction llc.
discriminate.
simpl in *.
caseSimpl (getBool (getNLc a n)).
exists a.
destruct (getNLcTrue2 _ _ C).
exists x.
tauto.

destruct (IHllc H).
destruct H0.
exists x, x0.
tauto.
Qed.

Lemma getNSound : forall (llc : list (list (core*nat))) (lc : list (core*nat)) (c : core) (n : nat),
(forall (l2 : list (core*nat)), In l2 llc -> sorted l2 = true) ->
validCores llc = true -> In (c, n) lc -> In lc llc -> type2 (getReq (getN llc n)) = type c.
Proof.
intros.
induction llc.
auto with *.
destruct H2.
subst a.
clear IHllc.
induction lc.
auto with *.
destruct H1.
subst a.
simpl.
rewrite NPeano.Nat.eqb_refl.
apply type2Type.

simpl; simpl in IHlc, H0.
destruct a.
b2PH.
rewrite H3, H2 in IHlc.
caseSimpl (beq_nat n n0).
rewrite <- (beq_nat_true _ _ C) in *.
assert (sorted ((c0, n) :: lc) = true).
auto with *.
generalize (minIsFirst _ _ _ _ _ H5 H1); omega.
apply IHlc; trivial.
intros.
assert (sorted ((c0, n0) :: lc) = true).
auto with *.
destruct H5.
subst lc.
apply (allSorted _ _ H6).
auto with *.

simpl.
caseSimpl (getBool (getNLc a n)).
destruct (getNLcTrue2 _ _ C).
assert (sorted lc = true).
auto with *.
rewrite (validCoresTypes _ _ _ _ _ _ H0 H4 H1 H3); auto with *.
clear -H H0 H3.
induction a.
auto with *.
simpl.
destruct a.
destruct H3.
inversion H1.
subst n0.
subst x.
rewrite NPeano.Nat.eqb_refl.
apply type2Type.

caseSimpl (beq_nat n n0).
rewrite <- (beq_nat_true _ _ C) in *.
assert (sorted ((c, n) :: a0) = true).
auto with *.
rewrite (validCoresTypes _ _ ((c, n) :: a0) _ x n H0 H2); auto with *.
apply type2Type.
apply IHa.
intros.
assert (sorted ((c, n0) :: a0) = true).
auto with *.
destruct H2.
subst a0.
apply (allSorted _ _ H3).
auto with *.

simpl in *.
b2PH.
rewrite H2, H3.
trivial.
trivial.
apply IHllc; trivial.
intros.
auto with *.
simpl in H0.
b2PH.
Qed.

Fixpoint addBlanks (lr : list reqValue) (lc : list (core*nat)) (n : nat) : list reqValue :=
match lr with
| nil => nil
| rv :: lr' => (if getBool (getNLc lc n) then rv else blank)::(addBlanks lr' lc (n+1))
end.

Definition P10 (n: nat) : Prop := forall (lc : list (core*nat)) (lr : list reqValue) (c : core) (t : nat), 
In (c, n + t) lc -> nth n (addBlanks lr lc t) blank = nth n lr blank.

Lemma usedUnchangedBase : P10 0.
Proof.
unfold P10.
intros.
destruct lr.
trivial.
simpl in *.
rewrite (getNLcTrue _ _ _ H).
trivial.
Qed.

Lemma usedUnchangedRec : forall (i : nat), (forall j : nat, j <= i -> P10 j) -> P10 (S i).
Proof.
unfold P10.
intros.
destruct lr.
trivial.

simpl.
rewrite (H i (le_n i) _ _ c).
trivial.
assert (i + (t + 1) = S i + t).
omega.
rewrite H1.
trivial. 
Qed.

Lemma usedUnchanged : forall (lc : list (core*nat)) (lr : list reqValue) (c : core) (n : nat), 
In (c, n) lc -> nth n (addBlanks lr lc 0) blank = nth n lr blank.
Proof.
intros.
generalize (strongind P10 usedUnchangedBase usedUnchangedRec n); intro.
unfold P10 in H0.
apply (H0 lc lr c 0).
rewrite plus_0_r.
trivial.
Qed.

Definition P11 (i: nat) := forall (lc : list (core*nat)) (lr : list reqValue) (n t : nat), length lr = i ->
(forall c : core, ~In (c, n+t) lc) -> nth n (addBlanks lr lc t) blank = blank.

Lemma unusedBlankBase : P11 0.
Proof.
unfold P11.
intros.
destruct lr.
destruct n; trivial.
simpl in *.
omega.
Qed.

Lemma unusedBlankRec : forall (i : nat), (forall j : nat, j <= i -> P11 j) -> P11 (S i).
Proof.
unfold P11.
intros.
destruct lr.
discriminate.
simpl in *.

destruct n.
caseSimpl (getBool (getNLc lc t)); trivial.
destruct (getNLcTrue2 _ _ C).
simpl in H1.
generalize (H1 x); intro.
tauto.

apply (H i).
trivial.
auto.
assert (n + (t + 1) = S (n + t)). omega.
rewrite H2.
trivial.
Qed.

Lemma unusedBlank : forall (lc : list (core*nat)) (lr : list reqValue) (n : nat),
(forall c : core, ~In (c, n) lc) -> nth n (addBlanks lr lc 0) blank = blank.
Proof.
intros.
apply (strongind P11 unusedBlankBase unusedBlankRec (length lr)); trivial.
rewrite plus_0_r.
trivial.
Qed.

Fixpoint padWithBlanks (lr : list reqValue) (n : nat): list reqValue :=
match lr, n with
| _, O => lr
| nil, S n' => blank::padWithBlanks nil n'
| rv::lr', S n' => rv::padWithBlanks lr' n'
end.

Definition P12 (n: nat) : Prop := forall (lr : list reqValue), n <= length (padWithBlanks lr n).

Lemma padLengthBase : P12 0.
Proof.
unfold P12.
intros.
destruct lr.
auto.
simpl.
omega.
Qed.

Lemma padLengthRec : forall (i : nat), (forall j : nat, j <= i -> P12 j) -> P12 (S i).
Proof.
unfold P12.
intros.
destruct lr.
simpl.
auto with *.
simpl.
apply le_n_S.
apply (H i).
trivial.
Qed.

Lemma padLength : forall (lr : list reqValue) (n : nat), n <= length (padWithBlanks lr n).
Proof.
intros.
apply (strongind P12 padLengthBase padLengthRec n).
Qed.

Definition P13 (n: nat) : Prop :=  forall (lr : list reqValue) (m : nat), nth n (padWithBlanks lr m) blank = nth n lr blank.

Lemma padSoundBase : P13 0.
Proof.
unfold P13.
intros.
destruct m, lr; trivial.
Qed.

Lemma padSoundRec : forall (i : nat), (forall j : nat, j <= i -> P13 j) -> P13 (S i).
Proof.
unfold P13.
intros.
destruct m, lr; trivial.
simpl.
rewrite (H i).
simpl.
destruct i; trivial.
trivial.
simpl.
apply (H i).
trivial.
Qed.

Lemma padSound : forall (lr : list reqValue) (n m : nat), nth n (padWithBlanks lr m) blank = nth n lr blank.
Proof.
intros.
apply (strongind P13 padSoundBase padSoundRec n).
Qed.

Fixpoint merge3 (ll1 ll2 : list (list (core*nat))) (lr : list reqValue) (n : nat): list reqValue :=
match lr with
| nil => nil
| blank::lr' => (let hn := getN ll1 n in if getBool hn then getReq hn else getReq (getN ll2 n))::merge3 ll1 ll2 lr' (n+1)
| rv::lr' => rv::merge3 ll1 ll2 lr' (n+1)
end.

Definition P14 (i: nat) : Prop := forall (ll1 ll2 : list (list (core*nat))) (lr : list reqValue) (n t : nat), length lr = i ->
nth n lr blank <> blank -> nth n (merge3 ll1 ll2 lr t) blank = nth n lr blank.

Lemma merge3lrSoundBase : P14 0.
Proof.
unfold P14.
intros.
destruct lr.
trivial.
simpl in H.
omega.
Qed.

Lemma merge3lrSoundRec : forall (i : nat), (forall j : nat, j <= i -> P14 j) -> P14 (S i).
Proof.
unfold P14.
intros.
destruct lr.
trivial.
simpl in *.
destruct n.
destruct r; trivial.
tauto.

destruct r;
simpl;
apply (H i); trivial;
auto.
Qed.

Lemma merge3lrSound : forall (ll1 ll2 : list (list (core*nat))) (lr : list reqValue) (n : nat),
nth n lr blank <> blank -> nth n (merge3 ll1 ll2 lr 0) blank = nth n lr blank.
Proof.
intros.
apply (strongind P14 merge3lrSoundBase merge3lrSoundRec (length lr)).
trivial.
trivial.
Qed.

Definition P15 (i: nat) : Prop := forall (ll1 ll2 : list (list (core*nat))) (lc : list (core*nat)) 
(lr : list reqValue) (c : core) (n t : nat), length lr = i -> validCores ll1 = true -> 
(forall l1 : list (core * nat), In l1 ll1 -> sorted l1 = true) ->
(forall (l1 : list (core * nat)) (c1 : core), In (c1, n+t) l1 -> In l1 ll1 -> nth n lr blank <> blank -> type2 (nth n lr blank) = type c1) -> 
In (c, n+t) lc -> In lc ll1 -> n < length lr -> type2 (nth n (merge3 ll1 ll2 lr t) blank) = type c.

Lemma merge3ll1SoundBase : P15 0.
Proof.
unfold P15.
intros.
destruct lr.
simpl in H5.
omega.
omega.
Qed.

Lemma merge3ll1SoundRec : forall (i : nat), (forall j : nat, j <= i -> P15 j) -> P15 (S i).
Proof.
unfold P15.
intros.
destruct lr.
discriminate.
simpl in *.
destruct n.
destruct r; simpl in *; try (apply (H3 _ _ H4 H5); discriminate).
rewrite (getNTrue _ _ _ _ H4 H5).
apply (getNSound _ lc); trivial.
cut (type2 (nth n (merge3 ll1 ll2 lr (t + 1)) blank) = type c).
destruct r; simpl; trivial.

assert (n + (t + 1) = S n + t). omega.
rewrite <- H7 in *.
apply (H i (le_n i) _ _ lc); trivial.
auto.
omega.
Qed.

Lemma merge3ll1Sound : forall (ll1 ll2 : list (list (core*nat))) (lc : list (core*nat)) 
(lr : list reqValue) (c : core) (n t : nat), validCores ll1 = true -> 
(forall l1 : list (core * nat), In l1 ll1 -> sorted l1 = true) ->
(forall (l1 : list (core * nat)) (c1 : core), In (c1, n) l1 -> In l1 ll1 -> nth n lr blank <> blank -> type2 (nth n lr blank) = type c1) -> 
In (c, n) lc -> In lc ll1 -> n < length lr -> type2 (nth n (merge3 ll1 ll2 lr 0) blank) = type c.
Proof.
intros.
generalize (strongind P15 merge3ll1SoundBase merge3ll1SoundRec (length lr)); intro.
unfold P15 in H5.
apply (H5 _ _ lc); trivial.
rewrite plus_0_r.
trivial.
rewrite plus_0_r.
trivial.
Qed.

Definition P16 (i: nat) : Prop := forall (ll1 ll2 : list (list (core*nat))) (lc : list (core*nat)) 
(lr : list reqValue) (c : core) (n t : nat), length lr = i -> validCores ll1 = true -> validCores ll2 = true -> 
(forall l1 : list (core * nat), In l1 ll1 -> sorted l1 = true) ->
(forall l2 : list (core * nat), In l2 ll2 -> sorted l2 = true) ->
(forall (l2 : list (core * nat)) (c2 : core), In (c2, n+t) l2 -> In l2 ll2 -> nth n lr blank <> blank -> type2 (nth n lr blank) = type c2) -> 
(forall (l1 l2 : list (core * nat)) (c1 c2 : core) (n1 : nat), In (c1, n1) l1 -> In l1 ll1 -> In (c2, n1) l2 -> In l2 ll2 -> type c1 = type c2) ->
In (c, n+t) lc -> In lc ll2 -> n < length lr -> type2 (nth n (merge3 ll1 ll2 lr t) blank) = type c.

Lemma merge3ll2SoundBase : P16 0.
Proof.
unfold P16.
intros.
destruct lr.
simpl in H8.
omega.
omega.
Qed.

Lemma merge3ll2SoundRec : forall (i : nat), (forall j : nat, j <= i -> P16 j) -> P16 (S i).
Proof.
unfold P16.
intros.
destruct lr.
discriminate.
destruct n.
destruct r; simpl in *; try (apply (H5 _ _ H7 H8); discriminate).
caseSimpl (getBool (getN ll1 t)).
destruct (getNTrue2 _ _ C).
destruct H10, H10.
rewrite (getNSound _ _ _ _ H3 H1 H10 H11).
apply (H6 _ _ _ _ _ H10 H11 H7 H8).
apply (getNSound _ lc); trivial.

assert (n + (t + 1) = S n + t). omega.
rewrite <- H10 in *.
cut (type2 (nth n (merge3 ll1 ll2 lr (t+1)) blank) = type c).
destruct r; simpl; trivial.
apply (H i (le_n i) _ _ lc); trivial.
auto.
simpl in H9.
omega.
Qed.

Lemma merge3ll2Sound : forall (ll1 ll2 : list (list (core*nat))) (lc : list (core*nat)) 
(lr : list reqValue) (c : core) (n t : nat), validCores ll1 = true -> validCores ll2 = true -> 
(forall l1 : list (core * nat), In l1 ll1 -> sorted l1 = true) ->
(forall l2 : list (core * nat), In l2 ll2 -> sorted l2 = true) ->
(forall (l2 : list (core * nat)) (c2 : core), In (c2, n) l2 -> In l2 ll2 -> nth n lr blank <> blank -> type2 (nth n lr blank) = type c2) -> 
(forall (l1 l2 : list (core * nat)) (c1 c2 : core) (n1 : nat), In (c1, n1) l1 -> In l1 ll1 -> In (c2, n1) l2 -> In l2 ll2 -> type c1 = type c2) ->
In (c, n) lc -> In lc ll2 -> n < length lr -> type2 (nth n (merge3 ll1 ll2 lr 0) blank) = type c.
Proof.
intros.
generalize (strongind P16 merge3ll2SoundBase merge3ll2SoundRec (length lr)); intro.
unfold P16 in H8.
apply (H8 _ _ lc); trivial.
rewrite plus_0_r.
trivial.
rewrite plus_0_r.
trivial.
Qed.

Lemma llMatchNotNA : forall (llc : list (list (core*nat))) (lr : list reqValue), validCores llc = true ->
(forall (lc : list (core * nat)) (c : core) (n : nat), In (c, n) lc -> In lc llc -> type2 (nth n lr blank) = type c) -> llMatch llc lr <> NA.
Proof.
intros.
induction llc.
discriminate.
simpl.
apply orNotNa.
clear IHllc.
caseSimpl (lMatch a lr); try discriminate.
generalize (lMatchNa _ _ C); intro.
destruct H1, H1, H1.
rewrite (validCoresArgs _ _ _ _ H H1) in H2; auto with *.
destruct H2.
discriminate.
rewrite <- (H0 _ _ _ H1) in H2.
destruct (nth x0 lr blank); discriminate.
auto with *.
apply IHllc.
simpl in H.
b2PH.
intros.
apply (H0 lc); trivial.
auto with *.
Qed.

Definition P17 (i: nat) : Prop := forall (l1 l2 : list (core*nat)) (c : core) (n : nat), length l1 + length l2 = i ->
In (c, n) l1 \/ In (c, n) l2 -> exists c' : core, In (c', n) (merge l1 l2).

Lemma mergekeepsNBase : P17 0.
Proof.
unfold P17.
intros.
destruct l1, l2; simpl in H; try omega.
destruct H0; auto with *.
Qed.

Lemma mergekeepsNRec : forall (i : nat), (forall j : nat, j <= i -> P17 j) -> P17 (S i).
Proof.
unfold P17.
intros.
destruct l1, l2.
discriminate.
destruct H1.
auto with *.
exists c.
trivial.
destruct H1.
exists c.
rewrite (mergeNil2).
trivial.
auto with *.

destruct p, p0.
destruct (mergeNoNils l1 l2 c0 c1 n0 n1).
rewrite H2.
caseSimpl (beq_nat n n0).
rewrite (beq_nat_true _ _ C).
exists c0.
auto with *.
cut (exists c' : core, In (c', n) (merge l1 ((c1, n1) :: l2))).
intro.
destruct H3.
exists x.
auto with *.
apply (H i (le_n i) _ _ c).
auto.
destruct H1; [|tauto].
left.
destruct H1; trivial.
inversion H1.
subst n0.
rewrite NPeano.Nat.eqb_refl in C.
discriminate.

destruct H2.
destruct H2.
rewrite H2.
rewrite (beq_nat_true _ _ H3) in *.
caseSimpl (beq_nat n n1).
rewrite (beq_nat_true _ _ C).
exists (coreCheck c0 c1).
auto with *.
cut (exists c' : core, In (c', n) (merge l1 l2)).
intro.
destruct H4.
exists x.
auto with *.
assert (i-1 <= i). omega.
apply (H (i-1) H4 _ _ c).
simpl in H0.
omega.
destruct H1, H1; try tauto;
inversion H1;
subst n1;
rewrite NPeano.Nat.eqb_refl in C;
discriminate.

rewrite H2.
caseSimpl (beq_nat n n1).
rewrite (beq_nat_true _ _ C).
exists c1.
auto with *.
cut (exists c' : core, In (c', n) (merge ((c0, n0)::l1) l2)).
intro.
destruct H3.
exists x.
auto with *.
apply (H i (le_n i) _ _ c).
simpl in *.
omega.
destruct H1; [tauto|].
right.
destruct H1; trivial.
inversion H1.
subst n1.
rewrite NPeano.Nat.eqb_refl in C.
discriminate.
Qed.

Lemma mergekeepsN : forall (l1 l2 : list (core*nat)) (c : core) (n : nat),
In (c, n) l1 \/ In (c, n) l2 -> exists c' : core, In (c', n) (merge l1 l2).
Proof.
intros.
generalize (strongind P17 mergekeepsNBase mergekeepsNRec (length l1 + length l2)); intro.
unfold P17 in H0.
apply (H0 _ _ c); trivial.
Qed.

Definition P18 (i: nat) : Prop := forall (l1 l2 : list (core*nat)) (c : core) (n : nat), length l1 + length l2 = i ->
In (c, n) (merge l1 l2) -> exists c' : core, In (c', n) l1 \/ In (c', n) l2.

Lemma mergekeepsN2Base : P18 0.
Proof.
unfold P18.
intros.
destruct l1, l2; simpl in H; try omega.
auto with *.
Qed.

Lemma mergekeepsN2Rec : forall (i : nat), (forall j : nat, j <= i -> P18 j) -> P18 (S i).
Proof.
unfold P18.
intros.
destruct l1, l2.
auto with *.
exists c.
auto.
rewrite mergeNil2 in H1.
exists c.
tauto.
destruct p, p0.
simpl.

destruct (mergeNoNils l1 l2 c0 c1 n0 n1).
rewrite H2 in H1.
destruct H1.
exists c0.
inversion H1.
tauto.
assert (length l1 + length ((c1, n1) :: l2) = i).
auto.
destruct (H i (le_n i) _ _ _ _ H3 H1).
exists x.
tauto.

destruct H2.
destruct H2.
rewrite H2 in H1.
destruct H1.
inversion H1.
exists c0.
tauto.
simpl in H0.
assert (length l1 + length l2 = i - 1).
omega.
assert (i-1 <= i). omega.
destruct (H (i-1) H5 _ _ _ _ H4 H1).
exists x.
tauto.

rewrite H2 in H1.
destruct H1.
exists c1.
inversion H1.
tauto.
assert (length ((c0, n0) :: l1) + length l2 = i).
simpl in *.
omega.
destruct (H i (le_n i) _ _ _ _ H3 H1).
exists x.
tauto.
Qed.

Lemma mergekeepsN2 : forall (l1 l2 : list (core*nat)) (c : core) (n : nat),
In (c, n) (merge l1 l2) -> exists c' : core, In (c', n) l1 \/ In (c', n) l2.
Proof.
intros.
generalize (strongind P18 mergekeepsN2Base mergekeepsN2Rec (length l1 + length l2)); intro.
unfold P18 in H0.
apply (H0 _ _ c); trivial.
Qed.

Lemma sameThenElse : forall (b : bool) (t : trilean), (if b then t else t) = t.
Proof.
destruct b; trivial.
Qed.

Lemma coreMatchTrue : forall (rv : reqValue) (c : core),
coreMatch rv c = T -> type2 rv = type c.
Proof.
intros.
destruct rv, c; try destruct r; trivial; try discriminate;
unfold coreMatch in H; rewrite sameThenElse in H; discriminate.
Qed.

Lemma merge3Sound : forall (ll1 ll2 : list (list (core*nat))) (lc1 lc2 : list (core*nat)) (lr lr' : list reqValue) , 
validCores (lc1::ll1) = true -> validCores (lc2::ll2) = true -> 
(forall l1 : list (core * nat), In l1 (lc1::ll1) -> sorted l1 = true) ->
(forall l2 : list (core * nat), In l2 (lc2::ll2) -> sorted l2 = true) ->
(forall (l1 : list (core * nat)) (c1 cm : core) (n : nat), In (c1, n) l1 -> In l1 (lc1::ll1) -> In (cm, n) (merge lc1 lc2) -> type c1 = type cm) ->
(forall (l2 : list (core * nat)) (c2 cm : core) (n : nat), In (c2, n) l2 -> In l2 (lc2::ll2) -> In (cm, n) (merge lc1 lc2) -> type c2 = type cm) ->
(forall (l1 l2 : list (core * nat)) (c1 c2 : core) (n1 : nat), In (c1, n1) l1 -> In l1 (lc1::ll1) -> In (c2, n1) l2 -> In l2 (lc2::ll2) -> type c1 = type c2) ->
(lMatch (merge lc1 lc2) lr) = T -> 
lr' = (merge3 ll1 ll2 (padWithBlanks (addBlanks lr (merge lc1 lc2) 0) ((Peano.max (maxN ll1) (maxN ll2))+1)) 0) ->
((llMatch (lc1::ll1) lr') /\t (llMatch (lc2::ll2) lr')) = T.
Proof.
intros.
subst lr'.
generalize (maxNIsMax ll1); intro.
generalize (maxNIsMax ll2); intro.
simpl.
assert (lMatch (merge lc1 lc2) (merge3 ll1 ll2 (padWithBlanks (addBlanks lr (merge lc1 lc2) 0) ((Peano.max (maxN ll1) (maxN ll2))+1)) 0) = T).
apply (lMatchTrue2).
apply mergeSorted; auto with *.
intros.
generalize (H7 n); intro.
rewrite merge3lrSound;
rewrite padSound;
rewrite (usedUnchanged _ _ c).
apply (lMatchTrue (merge lc1 lc2)); trivial.
apply mergeSorted; auto with *.
trivial.
caseSimpl (nth n lr blank); try discriminate.
assert (coreMatch (nth n lr blank) c = NA).
apply coreMatchNa2.
tauto.
rewrite (lMatchTrue _ _ _ _ H6) in H11; trivial.
discriminate.
apply mergeSorted; auto with *.
trivial.
rewrite mergeCorrect in H9.
destruct (andT _ _ H9).
rewrite H10, H11.
clear H9 H10 H11.

apply andT2; apply orT2; trivial.
apply llMatchNotNA.
simpl in H.
b2PH.
intros.
rewrite (merge3ll1Sound _ _ lc _ c); trivial.
simpl in H.
b2PH.
auto with *.
rewrite padSound.
destruct (inOrNot (merge lc1 lc2) n).
destruct H11.
rewrite (usedUnchanged _ _ x) in *; trivial.
intros.
rewrite (H3 l1 _ x n); trivial.
apply coreMatchTrue.
apply (lMatchTrue _ _ _ _ H6); trivial.
apply mergeSorted; auto with *.
auto with *.
rewrite (unusedBlank _ _ _ H11).
intros.
tauto.
cut (n <= (Peano.max (maxN ll1) (maxN ll2))).
generalize (padLength (addBlanks lr (merge lc1 lc2) 0) (Peano.max (maxN ll1) (maxN ll2) + 1)).
omega.
apply (le_trans _ _ _ (maxNIsMax _ _ _ _ H9 H10)).
apply Max.le_max_l.

apply llMatchNotNA.
simpl in H0.
b2PH.
intros.
rewrite (merge3ll2Sound _ _ lc _ c); trivial.
simpl in H; b2PH.
simpl in H0; b2PH.
auto with *.
auto with *.
rewrite padSound.
destruct (inOrNot (merge lc1 lc2) n).
destruct H11.
rewrite (usedUnchanged _ _ x) in *; trivial.
intros.
rewrite (H4 l2 _ x n); trivial.
apply coreMatchTrue.
apply (lMatchTrue _ _ _ _ H6); trivial.
apply mergeSorted; auto with *.
auto with *.
rewrite (unusedBlank _ _ _ H11).
intros.
tauto.
intros.
apply (H5 l1 l2 _ _ n1); trivial.
auto with *.
auto with *.
cut (n <= (Peano.max (maxN ll1) (maxN ll2))).
generalize (padLength (addBlanks lr (merge lc1 lc2) 0) (Peano.max (maxN ll1) (maxN ll2) + 1)).
omega.
apply (le_trans _ _ _ (maxNIsMax _ _ _ _ H9 H10)).
apply Max.le_max_r.
Qed.

Lemma llMatchCom : forall (ll1 : list (list (core*nat))) (l1 : list (core*nat)) (lr : list reqValue),
In l1 ll1 -> llMatch ll1 lr = llMatch (l1::ll1) lr.
Proof.
intros.
simpl.
induction ll1.
auto with *.
destruct H.
simpl.
subst a.
caseSimpl (lMatch l1 lr); caseSimpl (llMatch ll1 lr); trivial.
simpl.
rewrite (IHll1 H) at 1.
caseSimpl (lMatch l1 lr); caseSimpl (lMatch a lr); trivial.
Qed.

Lemma validCoresCN'True : forall (lc : list (core * nat)) (c1 : core) (n : nat),
(forall c2 : core, In (c2, n) lc -> type c1 = type c2) -> validCoresCN' lc c1 n = true.
Proof.
intros.
induction lc.
trivial.
simpl in *.
destruct a.
rewrite IHlc.
caseSimpl (beq_nat n n0); trivial.
rewrite (H c).
rewrite typeDiffXXFalse.
trivial.
rewrite (beq_nat_true _ _ C).
tauto.
intros.
auto.
Qed.

Lemma validCoresCNTrue : forall (llc : list (list (core*nat))) (c1 : core) (n : nat),
(forall (lc : list (core * nat)) (c2 : core), In (c2, n) lc -> In lc llc -> type c1 = type c2) -> validCoresCN llc c1 n = true.
Proof.
intros.
induction llc.
trivial.
simpl in *.
rewrite validCoresCN'True.
rewrite IHllc.
trivial.
intros.
apply (H lc).
trivial.
tauto.
intros.
apply (H a).
trivial.
tauto.
Qed.

Lemma validCoresLcTrue : forall (llc : list (list (core*nat))) (l1 : list (core*nat)),
(forall (c : core) (n : nat), In (c, n) l1 -> invalidArgs c = false) ->
(forall (l2 : list (core * nat)) (c1 c2 : core) (n : nat), In (c1, n) l1 -> In (c2, n) l2 -> In l2 llc -> type c1 = type c2) -> 
validCoresLc llc l1 = true.
Proof.
intros.
induction l1.
trivial.
simpl in *.
destruct a.
rewrite (H c n).
rewrite validCoresCNTrue.
rewrite IHl1.
trivial.
intros.
apply (H _ n0).
tauto.
intros.
apply (H0 l2 _ _ n0).
tauto.
trivial.
trivial.
intros.
apply (H0 lc _ _ n).
tauto.
trivial.
tauto.
tauto.
Qed.

Lemma validCoresTrue : forall (llc : list (list (core*nat))),
(forall (lc : list (core*nat)) (c : core) (n : nat), In (c, n) lc -> In lc llc -> invalidArgs c = false) ->
(forall (l1 l2 : list (core * nat)) (c1 c2 : core) (n : nat), In (c1, n) l1 -> In (c2, n) l2 -> 
In l1 llc -> In l2 llc -> type c1 = type c2) -> 
(forall (lc : list (core*nat)), In lc llc -> sorted lc = true) -> validCores llc = true.
Proof.
intros.
induction llc.
trivial.
simpl in *.
rewrite validCoresLcTrue.
rewrite IHllc.
trivial.
intros.
apply (H lc _ n).
trivial.
tauto.
intros.
apply (H0 l1 l2 _ _ n); trivial.
intros.
tauto.
tauto.
intros.
apply H1.
tauto.
intros.
apply (H a _ n).
trivial.
tauto.
intros.
apply (H0 a l2 _ _ n); trivial.
tauto.
tauto.
Qed.

Lemma validCoresCom : forall (llc : list (list (core*nat))) (lc : list (core*nat)),
validCores llc = true -> In lc llc -> sorted lc = true -> validCores (lc :: llc) = true.
Proof.
intros.
simpl.
rewrite H.
rewrite andb_true_r.
apply validCoresLcTrue.
intros.
apply (validCoresArgs _ _ _ _ H H2 H0).
intros.
apply (validCoresTypes _ _ _ _ _ _ H H1 H2 H3 H0 H4).
Qed.

Lemma merge3Sound2 : forall (ll1 ll2 : list (list (core*nat))) (lc1 lc2 : list (core*nat)) (lr lr': list reqValue), 
validCores ll1 = true -> validCores ll2 = true -> 
(forall l1 : list (core * nat), In l1 ll1 -> sorted l1 = true) ->
(forall l2 : list (core * nat), In l2 ll2 -> sorted l2 = true) ->
(forall (l1 : list (core * nat)) (c1 cm : core) (n : nat), In (c1, n) l1 -> In l1 ll1 -> In (cm, n) (merge lc1 lc2) -> type c1 = type cm) ->
(forall (l2 : list (core * nat)) (c2 cm : core) (n : nat), In (c2, n) l2 -> In l2 ll2 -> In (cm, n) (merge lc1 lc2) -> type c2 = type cm) ->
(forall (l1 l2 : list (core * nat)) (c1 c2 : core) (n1 : nat), In (c1, n1) l1 -> In l1 ll1 -> In (c2, n1) l2 -> In l2 ll2 -> type c1 = type c2) ->
(lMatch (merge lc1 lc2) lr) = T -> In lc1 ll1 -> In lc2 ll2 -> 
lr' = (merge3 ll1 ll2 (padWithBlanks (addBlanks lr (merge lc1 lc2) 0) ((Peano.max (maxN ll1) (maxN ll2))+1)) 0) ->
((llMatch ll1 lr') /\t (llMatch ll2 lr')) = T.
Proof.
intros.
subst lr'.
rewrite (llMatchCom _ _ _ H7).
rewrite (llMatchCom _ _ _ H8).
apply (merge3Sound _ _ _ _ lr); trivial.
apply validCoresCom; trivial.
auto.
apply validCoresCom; trivial.
auto.
intros.
apply H1.
destruct H9.
subst lc1.
trivial.
trivial.
intros.
apply H2.
destruct H9.
subst lc2.
trivial.
trivial.
intros.
apply (H3 l1 _ _ n); trivial.
destruct H10.
subst lc1.
trivial.
trivial.
intros.
apply (H4 l2 _ _ n); trivial.
destruct H10.
subst lc2.
trivial.
trivial.
intros.
apply (H5 l1 l2 _ _ n1); trivial.
destruct H10.
subst lc1.
trivial.
trivial.
destruct H12.
subst lc2.
trivial.
trivial.
Qed.

Lemma llCheckTrue : forall (ll1 ll2 : list (list (core*nat))), llCheck ll1 ll2 = T ->
exists (l1 l2 : list (core * nat)), In l1 ll1 /\ In l2 ll2 /\ nonEmptyRule (merge l1 l2) = T.
Proof.
intros.
induction ll2.
discriminate.
simpl in H.
destruct (orT _ _ H).
clear H IHll2.
induction ll1.
discriminate.
simpl in H0.
destruct (orT _ _ H0).
exists a0, a.
auto with *.

destruct (IHll1 H).
destruct H1.
exists x, x0.
destruct H1.
auto with *.

destruct (IHll2 H0).
destruct H1.
exists x, x0.
destruct H1.
destruct H2.
auto with *.
Qed.

Definition P19 (i: nat) : Prop := forall (l1 l2 : list (core*nat)) (c1 : core) (n : nat), length l1 + length l2 = i ->
In (c1, n) l1 -> In (c1, n) (merge l1 l2) \/ exists c2 : core, In ((coreCheck c1 c2), n) (merge l1 l2).

Lemma inMerge1Base : P19 0.
Proof.
unfold P19.
intros.
destruct l1, l2; simpl in H; try omega.
auto with *.
Qed.

Lemma inMerge1Rec : forall (i : nat), (forall j : nat, j <= i -> P19 j) -> P19 (S i).
Proof.
unfold P19.
intros.
destruct l1.
auto with *.
destruct H1.
subst p.
destruct l2.
rewrite mergeNil2.
auto with *.
simpl.
foldMerge c1 n l1 l2.
destruct p.
caseSimpl (blt_nat n n0).
auto with *.
caseSimpl (beq_nat n n0).
right.
exists c.
auto with *.
cut (In (c1, n) (merge ((c1, n) :: l1) l2) \/ (exists c2 : core, In (coreCheck c1 c2, n) (merge ((c1, n) :: l1) l2))).
intro.
destruct H1.
auto with *.
right.
destruct H1.
exists x.
auto with *.
apply (H i).
trivial.
simpl in *; omega.
auto with *.

destruct l2.
rewrite mergeNil2.
auto with *.
destruct p, p0.
simpl.
foldMerge c n0 l1 l2.
caseSimpl (blt_nat n0 n1).
cut (In (c1, n) (merge l1 ((c0, n1) :: l2)) \/ (exists c2 : core, In (coreCheck c1 c2, n) (merge l1 ((c0, n1) :: l2)))).
intro.
destruct H2.
auto with *.
right.
destruct H2.
exists x.
auto with *.
apply (H i).
trivial.
simpl in *; omega.
auto with *.

caseSimpl (beq_nat n0 n1).
cut (In (c1, n) (merge l1 l2) \/ (exists c2 : core, In (coreCheck c1 c2, n) (merge l1 l2))).
intro.
destruct H2.
auto with *.
right.
destruct H2.
exists x.
auto with *.
apply (H (i-1)).
omega.
simpl in *; omega.
auto with *.

cut (In (c1, n) (merge ((c, n0) :: l1) l2) \/ (exists c2 : core, In (coreCheck c1 c2, n) (merge ((c, n0) :: l1) l2))).
intro.
destruct H2.
auto with *.
right.
destruct H2.
exists x.
auto with *.
apply (H i).
trivial.
simpl in *; omega.
auto with *.
Qed.

Lemma inMerge1 : forall (l1 l2 : list (core*nat)) (c1 : core) (n : nat), 
In (c1, n) l1 -> In (c1, n) (merge l1 l2) \/ exists c2 : core, In ((coreCheck c1 c2), n) (merge l1 l2).
Proof.
intros.
apply (strongind P19 inMerge1Base inMerge1Rec (length l1 + length l2)); trivial.
Qed.

Definition P20 (i: nat) : Prop := forall (l1 l2 : list (core*nat)) (c2 : core) (n : nat), length l1 + length l2 = i ->
In (c2, n) l2 -> In (c2, n) (merge l1 l2) \/ exists c1 : core, In ((coreCheck c1 c2), n) (merge l1 l2).

Lemma inMerge2Base : P20 0.
Proof.
unfold P20.
intros.
destruct l1, l2; simpl in H; try omega.
auto with *.
Qed.

Lemma inMerge2Rec : forall (i : nat), (forall j : nat, j <= i -> P20 j) -> P20 (S i).
Proof.
unfold P20.
intros.
destruct l2.
auto with *.
destruct H1.
subst p.
destruct l1.
rewrite mergeNil.
auto with *.
simpl.
destruct p.
foldMerge c n0 l1 l2.
caseSimpl (blt_nat n0 n).
cut (In (c2, n) (merge l1 ((c2, n) :: l2)) \/ (exists c1 : core, In (coreCheck c1 c2, n) (merge l1 ((c2, n) :: l2)))).
intro.
destruct H1.
auto with *.
right.
destruct H1.
exists x.
auto with *.
apply (H i).
trivial.
simpl in *; omega.
auto with *.
caseSimpl (beq_nat n0 n).
right.
exists c.
rewrite (beq_nat_true _ _ C0).
auto with *.
auto with *.

destruct l1.
rewrite mergeNil.
auto with *.
destruct p, p0.
simpl.
foldMerge c0 n1 l1 l2.
caseSimpl (blt_nat n1 n0).
cut (In (c2, n) (merge l1 ((c, n0) :: l2)) \/ (exists c1 : core, In (coreCheck c1 c2, n) (merge l1 ((c, n0) :: l2)))).
intro.
destruct H2.
auto with *.
right.
destruct H2.
exists x.
auto with *.
apply (H i).
trivial.
simpl in *; omega.
auto with *.

caseSimpl (beq_nat n1 n0).
cut (In (c2, n) (merge l1 l2) \/ (exists c1 : core, In (coreCheck c1 c2, n) (merge l1 l2))).
intro.
destruct H2.
auto with *.
right.
destruct H2.
exists x.
auto with *.
apply (H (i-1)).
omega.
simpl in *; omega.
auto with *.

cut (In (c2, n) (merge ((c0, n1) :: l1) l2) \/ (exists c1 : core, In (coreCheck c1 c2, n) (merge ((c0, n1) :: l1) l2))).
intro.
destruct H2.
auto with *.
right.
destruct H2.
exists x.
auto with *.
apply (H i).
trivial.
simpl in *; omega.
auto with *.
Qed.

Lemma inMerge2 : forall (l1 l2 : list (core*nat)) (c2 : core) (n : nat),
In (c2, n) l2 -> In (c2, n) (merge l1 l2) \/ exists c1 : core, In ((coreCheck c1 c2), n) (merge l1 l2).
Proof.
intros.
apply (strongind P20 inMerge2Base inMerge2Rec (length l1 + length l2)); trivial.
Qed.

Lemma coreCheckTypes : forall (c1 c2 : core), invalidArgs c1 = false -> invalidArgs c2 = false ->
typeDiff (type c1) (type c2) = false -> type (coreCheck c1 c2) = type c1.
Proof.
intros.
unfold coreCheck.
rewrite H, H0, H1.
destruct c1, c2; try destruct r; try destruct r0; trivial; try discriminate;
findIf.
Qed.

Lemma coreCheckTypes2 : forall (c1 c2 : core), invalidArgs c1 = true \/ invalidArgs c2 = true \/
typeDiff (type c1) (type c2) = true -> coreCheck c1 c2 = na.
Proof.
intros.
destruct H.
unfold coreCheck; rewrite H.
caseSimpl (typeDiff (type c1) (type c2)); trivial.
destruct H;
unfold coreCheck; rewrite H.
caseSimpl (typeDiff (type c1) (type c2)); trivial.
caseSimpl (invalidArgs c1); trivial.
trivial.
Qed.

Lemma nonEmptyMergeTypes : forall (l1 l2 : list (core*nat)) (c cm : core) (n : nat),
sorted l1 = true -> sorted l2 = true -> In (cm, n) (merge l1 l2) -> nonEmptyRule (merge l1 l2) <> NA -> 
In (c, n) l1 \/ In (c, n) l2 -> type c = type cm.
Proof.
intros.
cut (typeDiff (type c) (type cm) = false).
destruct c, cm; try destruct r; try destruct r0; trivial; discriminate.
caseSimpl (typeDiff (type c) (type cm)); trivial.
exfalso.
generalize (mergeSorted _ _ H H0); intro.

destruct H3.
destruct (inMerge1 _ l2 _ _ H3).
rewrite (sortedListCEqual _ _ _ _ H4 H1 H5) in C.
rewrite typeDiffXXFalse in C; discriminate.
destruct H5.
rewrite (sortedListCEqual _ _ _ _ H4 H1 H5) in C.
generalize (nonEmptyNotNa _ _ _ H2 H5); intro.
generalize (coreCheckTypes2 c x); intro.
caseSimpl (invalidArgs c). rewrite H7 in H6; [discriminate | tauto].
caseSimpl (invalidArgs x). rewrite H7 in H6; [discriminate | tauto].
caseSimpl (typeDiff (type c) (type x)). rewrite H7 in H6; [discriminate | tauto].
rewrite (coreCheckTypes c x) in C; trivial.
rewrite typeDiffXXFalse in C; discriminate.

destruct (inMerge2 l1 _ _ _ H3).
rewrite (sortedListCEqual _ _ _ _ H4 H1 H5) in C.
rewrite typeDiffXXFalse in C; discriminate.
destruct H5.
rewrite (sortedListCEqual _ _ _ _ H4 H1 H5) in C.
generalize (nonEmptyNotNa _ _ _ H2 H5); intro.
generalize (coreCheckTypes2 x c); intro.
caseSimpl (invalidArgs c). rewrite H7 in H6; [discriminate | tauto].
caseSimpl (invalidArgs x). rewrite H7 in H6; [discriminate | tauto].
caseSimpl (typeDiff (type x) (type c)). rewrite H7 in H6; [discriminate | tauto].
rewrite (coreCheckTypes x c) in C; trivial.
destruct (type c), (type x); discriminate.
Qed.

Lemma nonEmptyMergeTypes2 : forall (l1 l2 : list (core * nat)) (c1 c2 : core) (n : nat),
sorted l1 = true -> sorted l2 = true ->
In (c1, n) l1 -> In (c2, n) l2 -> nonEmptyRule (merge l1 l2) <> NA -> type c1 = type c2.
Proof.
intros.
destruct (mergekeepsN l1 l2 c1 n).
tauto.
rewrite (nonEmptyMergeTypes l1 l2 _ x n); trivial.
rewrite (nonEmptyMergeTypes l1 l2 c2 x n); trivial.
tauto.
tauto.
Qed.

Lemma llCheckTrueTypes : forall (ll1 ll2 : list (list (core*nat))) (l1 l2 : list (core * nat)) (c1 c2 : core) (n : nat),
llCheck ll1 ll2 <> NA -> In (c1, n) l1 -> In l1 ll1 -> In (c2, n) l2 -> In l2 ll2 -> sorted l1 = true -> sorted l2 = true -> type c1 = type c2.
Proof.
intros.
induction ll2.
auto with *.
destruct H3.
subst a.
simpl in H.
destruct (orNotNa2 _ _ H).
clear H H6 IHll2.
induction ll1.
auto with *.
destruct H1.
subst a.
simpl in H3.
destruct (orNotNa2 _ _ H3).
clear H1 H3 IHll1.
apply (nonEmptyMergeTypes2 l1 l2 _ _ n); trivial.
apply (IHll1 H).
simpl in H3.
destruct (orNotNa2 _ _ H3).
trivial.
apply (IHll2).
simpl in H.
destruct (orNotNa2 _ _ H).
trivial.
trivial.
Qed.

Lemma llCheckSound : forall (s1 s2: srac), llCheck (toLists s1) (toLists s2) = T ->
validCores (toLists s1) = true -> validCores (toLists s2) = true -> 
exists lr : list reqValue, (llMatch (toLists s1) lr /\t llMatch (toLists s2) lr) = T.
Proof.
intros.
generalize (sortedLists s1); intro.
generalize (sortedLists s2); intro.
destruct (llCheckTrue _ _ H) as [l1].
destruct H4 as [l2], H4.
destruct H5.
generalize (mergeSorted _ _ (H2 _ H4) (H3 _ H5)); intro.
destruct (nonEmptySound _ H7 H6) as [lr].
exists (merge3 (toLists s1) (toLists s2) (padWithBlanks (addBlanks lr (merge l1 l2) 0) ((Peano.max (maxN (toLists s1)) (maxN (toLists s2)))+1)) 0).
apply (merge3Sound2 (toLists s1) (toLists s2) l1 l2 lr); trivial.

intros.
destruct (mergekeepsN2 _ _ _ _ H11).
assert (type x = type cm).
apply (nonEmptyMergeTypes l1 l2 _ _ n); trivial.
auto.
auto.
rewrite H6.
discriminate.
rewrite <- H13.
destruct H12.
apply (validCoresTypes _ _ _ _ _ _ H0 (H2 _ H10) H9 H12); trivial.
apply (llCheckTrueTypes (toLists s1) (toLists s2) l0 l2 _ _ n); trivial.
rewrite H.
discriminate.
auto.
auto.

intros.
destruct (mergekeepsN2 _ _ _ _ H11).
assert (type x = type cm).
apply (nonEmptyMergeTypes l1 l2 _ _ n); trivial.
auto.
auto.
rewrite H6.
discriminate.
rewrite <- H13.
destruct H12.
symmetry.
apply (llCheckTrueTypes (toLists s1) (toLists s2) l1 l0 _ _ n); trivial.
rewrite H.
discriminate.
auto.
auto.
apply (validCoresTypes _ _ _ _ _ _ H1 (H3 _ H10) H9 H12); trivial.

intros.
apply (llCheckTrueTypes (toLists s1) (toLists s2) l0 l3 _ _ n1); trivial.
rewrite H.
discriminate.
auto.
auto.
Qed.

Lemma trileanTrueIsT : forall t : trilean, trileanTrue t = true -> t = T.
Proof.
intros.
destruct t;
trivial;
discriminate.
Qed.

Lemma nonEmptyCoreComplete : forall (c : core) (rv : reqValue), coreMatch rv c = T -> nonEmptyCore c = T.
Proof.
intros.
unfold coreMatch in H.
caseSimpl (invalidArgs c); try discriminate.
destruct rv; destruct c; try destruct r; trivial; try discriminate.
unfold nonEmptyCore, invalidArgs.
caseSimpl (z0 <=b z /\b z <b z1); try discriminate.
findIf.
b2PH.
omega.
unfold nonEmptyCore, invalidArgs.
caseSimpl (z0 <=b z /\b z <=b z1); try discriminate.
findIf.
b2PH.
omega.
Qed.

Lemma nonEmptyRuleNa : forall (lc : list (core*nat)) (lr : list reqValue), 
nonEmptyRule lc = NA -> lMatch lc lr = NA.
Proof.
intros.
induction lc.
trivial.
simpl in *.
destruct a.
destruct (andNA _ _ H).
cut (coreMatch (nth n lr blank) c = NA).
intro.
rewrite H1; trivial.
clear -H0.
unfold nonEmptyCore in H0;
unfold coreMatch;
caseSimpl (invalidArgs c); destruct c; rewrite C in *; trivial; try discriminate.
rewrite (IHlc H0).
destruct (coreMatch (nth n lr blank) c); trivial.
Qed.

Lemma lCheckComplete : forall (s1 : srac) (l2 : list (core*nat)),
(exists lr : list reqValue, (llMatch (toLists s1) lr /\t lMatch l2 lr) = T) -> lCheck (toLists s1) l2 = T.
Proof.
intros.
destruct H.
destruct (andT _ _ H).
clear H.
induction (toLists s1).
discriminate.
simpl in *.
destruct (orT _ _ H0).
clear IHl.
generalize (mergeCorrect a l2 x).
rewrite H, H1;
simpl; intro.

induction (merge a l2).
unfold nonEmptyRule.
caseSimpl (lCheck l l2); trivial.
rewrite H in H0.
destruct (lCheckAndMatchNa l l2 x C); rewrite H3 in *; discriminate.
simpl in *.
destruct a0.
destruct (andT _ _ H2).
cut (nonEmptyCore c = T).
intros.
rewrite H5.
generalize (IHl0 H4); intro.
destruct (nonEmptyRule l0);
destruct (lCheck l l2); trivial; discriminate.
apply (nonEmptyCoreComplete _ _ H3).

rewrite (IHl H).
caseSimpl (nonEmptyRule (merge a l2)); trivial.
generalize (nonEmptyRuleNa _ x C); intro.
rewrite (mergeCorrect a l2 x), H1 in H2.
destruct (lMatch a x); discriminate.
Qed.

Lemma llCheckAndMatchNa:  forall (l1 l2 : list (list (core * nat))) (lr : list reqValue),
llCheck l1 l2 = NA -> llMatch l1 lr = NA \/ llMatch l2 lr = NA.
Proof.
intros.
induction l2.
tauto.
simpl in *.
destruct (orNA _ _ H).
destruct (lCheckAndMatchNa l1 a lr H0).
tauto.
rewrite H1.
tauto.
destruct (IHl2 H0).
tauto.
rewrite H1.
destruct (lMatch a lr); tauto.
Qed.

Lemma llCheckComplete : forall (s1 s2: srac),
(exists lr : list reqValue, (llMatch (toLists s1) lr /\t llMatch (toLists s2) lr) = T) -> llCheck (toLists s1) (toLists s2) = T.
Proof.
intros.
destruct H.
induction (toLists s2).
simpl in *.
destruct (llMatch (toLists s1) x); discriminate.
simpl in *.
destruct (andT _ _ H).
clear H.
destruct (orT _ _ H1).
rewrite (lCheckComplete).
caseSimpl (llCheck (toLists s1) l); trivial.
rewrite H in *.
destruct (llCheckAndMatchNa _ _ x C);
rewrite H2 in *; discriminate.
exists x.
rewrite H0, H; trivial.

rewrite H0, H in *.
rewrite IHl; trivial.
caseSimpl (lCheck (toLists s1) a); trivial.
destruct (lCheckAndMatchNa _ _ x C);
rewrite H2 in *; discriminate.
Qed.

Lemma validCoresTrue2 : forall (s : srac) (lr : list reqValue),
llMatch (toLists s) lr <> NA -> validCores (toLists s) = true.
Proof.
intros.
apply validCoresTrue.
intros.
induction (toLists s).
auto with *.
destruct H1.
clear IHl.
subst a.
simpl in H.
caseSimpl (invalidArgs c); trivial.
rewrite lMatchNa2 in H.
tauto.
exists c, n.
tauto.
simpl in H.
destruct (orNotNa2 _ _ H).
tauto.

intros.
generalize (sortedLists s); intro.
generalize (llMatchCom _ _ lr H2); intro.
generalize (llMatchCom _ _ lr H3); intro.
generalize H; intro.
generalize H; intro.
rewrite H5 in H7.
rewrite H6 in H8.
simpl in *.
assert (typeDiff (type c1) (nth n lr blank) = false).
caseSimpl (typeDiff (type c1) (nth n lr blank)); trivial.
rewrite lMatchNa2 in H7.
tauto.
exists c1, n.
tauto.
assert (typeDiff (type c2) (nth n lr blank) = false).
caseSimpl (typeDiff (type c2) (nth n lr blank)); trivial.
rewrite lMatchNa2 in H8.
tauto.
exists c2, n.
tauto.
assert (type c1 = type2 (nth n lr blank)).
destruct c1, (nth n lr blank); trivial;
try destruct r; try destruct r0; trivial;
discriminate.
rewrite H11.
destruct c2, (nth n lr blank); trivial;
try destruct r; try destruct r0; trivial;
discriminate.
apply (sortedLists s).
Qed.

Theorem conflict_check_soundness: forall r1 r2: rule, conflict_check r1 r2 = true -> rule_conflict r1 r2.
Proof.
intros.
unfold conflict_check in H.
unfold rule_conflict, rule_permit, rule_deny.
destruct r1, r2.
simpl.
b2PH.
generalize (trileanTrueIsT _ H2); clear H2; intro.
destruct (llCheckSound _ _ H2 H1 H0).
exists x.
rewrite llCorrect in H3.
rewrite llCorrect in H3.
destruct (andT _ _ H3).
rewrite H4, H5.
destruct eff0, eff1; try discriminate;
tauto.
Qed.

Theorem conflict_check_completeness: forall r1 r2: rule, rule_conflict r1 r2 -> (conflict_check r1 r2 = true).
Proof.
intros.
intros.
unfold conflict_check.
unfold rule_conflict, rule_permit, rule_deny in H.
destruct r1, r2.
simpl in *.
destruct H.
cut (effectDiff eff0 eff1 = true /\ trileanTrue (llCheck (toLists rules0) (toLists rules1)) = true /\
  validCores (toLists rules0) = true /\ validCores (toLists rules1) = true).
intros.
destruct H0; rewrite H0.
destruct H1.
destruct H2; rewrite H2.
rewrite H3.
auto with *.

split.
destruct H, H, H;
destruct H0;
rewrite H, H0;
trivial.

assert (sracMatch x rules0 = T /\ sracMatch x rules1 = T).
tauto.
clear H. 
split.
cut (llCheck (toLists rules0) (toLists rules1) = T).
intro.
rewrite H.
trivial.
destruct H0.
rewrite <- llCorrect in *.
apply llCheckComplete.
exists x.
rewrite H, H0.
trivial.

destruct H0.
rewrite <- llCorrect in *.
rewrite (validCoresTrue2 _ x).
rewrite (validCoresTrue2 _ x).
tauto.
rewrite H0.
discriminate.
rewrite H.
discriminate.
Qed.