(****************************************************************
   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 Core.
Require Export Recdef.
Require Import Coq.Program.Subset.

Notation "~t A" := (trileanNot A) (at level 75, right associativity).
Notation "A /\t B" := (trileanAnd A B) (at level 80, right associativity).
Notation "A =b B" := (Zeq_bool A B) (at level 90).

Inductive srac : Set :=
| single : core -> nat -> srac
| and : srac -> srac -> srac
| or : srac -> srac -> srac
| not : srac -> srac.

Open Scope nat_scope.

Definition notCheck (c : core) (n:nat) : srac :=
if invalidArgs c then single na n else
match c with
| any r => single (empty r) n
| empty r => single (any r) n
| timeInRange m M => if m =b 0 then if M =b Z'MIDNIGHT then single (empty (timeReq Z'NM0)) n else single (timeInRange M Z'MIDNIGHT) n 
                     else if M =b Z'MIDNIGHT then single (timeInRange Z'0 m) n 
                     else or (single (timeInRange Z'0 m) n) (single (timeInRange M Z'MIDNIGHT) n)
| intInRange m M => or (single (intLt m) n) (single (intGt M) n)
| intGt m => single (intLt (m+1)) n
| intLt M => single (intGt (M-1)) n
| na => single na n
end.

Definition trileanOr (t1 t2 : trilean) : trilean :=
match t1 with
| T => 
  match t2 with
  | NA => NA
  | _ => T
  end
| F => t2
| NA => NA
end.

Notation "A \/t B" := (trileanOr A B) (at level 85, right associativity).

Fixpoint sracMatch (reql : list reqValue) (s : srac) :trilean :=
match s with
| single c n => coreMatch (nth n reql blank) c
| and s1 s2 => sracMatch reql s1 /\t sracMatch reql s2
| or s1 s2 => sracMatch reql s1 \/t sracMatch reql s2
| not s1 => ~t sracMatch reql s1
end.

Open Scope Z_scope.

Lemma notsCancel: forall (t:trilean), (~t (~t t)) = t.
Proof.
intros.
destruct t;
simpl in *; trivial.
Qed.

Lemma notCheckSoundComp : forall (ls : list reqValue) (c: core) (n:nat), sracMatch ls (notCheck c n) = ~t sracMatch ls (single c n).
Proof.
intros.
unfold notCheck.
findIf;
unfold coreMatch.
rewrite C.
simpl.
trivial.

remember c. induction c0;
simpl;
remember (nth n ls blank); induction y;
try solve[try induction r; trivial];

repeat findIf;
try rewrite <- Heqy;
simpl; trivial;
unfold coreMatch;
simpl in *;
try (b2PH; unfold MIDNIGHT in *; omega);
repeat findIf; b2PH; try omega;
try solve[assert (0 <= z <= MIDNIGHT); try solve[destruct z; trivial];
assert (0 <= z0 <= MIDNIGHT); try solve[destruct z0; trivial];
assert (0 <= z1 < MIDNIGHT); try solve[destruct z1; trivial];
b2PH; omega].
Qed.

Open Scope nat_scope.
Fixpoint depth (s: srac) : nat :=
match s with
| single c n => 1
| or s1 s2 => (depth s1) + (depth s2) + 1
| and s1 s2 => (depth s1) + (depth s2) + 1
| not s1 => (depth s1) + 1
end.

Fixpoint notSize (s: srac) : nat :=
match s with
| single c n => 1
| or s1 s2 => (notSize s1) + (notSize s2) + 1
| and s1 s2 => (notSize s1) + (notSize s2) + 1
| not s1 => (notSize s1) + (depth s1)
end.

Function removeNots (s:srac) {measure notSize s} : srac :=
match s with 
| not (single c1 n) => notCheck c1 n
| not (or s1 s2) => and (removeNots (not s1)) (removeNots (not s2))
| not (and s1 s2) => or (removeNots (not s1)) (removeNots (not s2))
| not (not s1) => removeNots s1

| and s1 s2 => and (removeNots s1) (removeNots s2)
| or s1 s2 => or (removeNots s1) (removeNots s2)
| single c n => s
end.
intros; simpl; omega.
intros; simpl; omega.
intros; simpl; omega.
intros; simpl; omega.
intros; simpl; omega.
intros; simpl; omega.
intros; simpl; omega.
intros; simpl; omega.
intros; simpl; omega.
Qed.

Theorem strongind_aux : forall P : nat -> Prop,
  P 0 ->
  (forall n, (forall m, m <= n -> P m) -> P (S n)) ->
  forall n, (forall m, ((m <= n) -> P m)).
Proof.
induction n as [ | n' IHn' ].
intros m H1.
inversion H1.
assumption.
intros.
assert (m <= n' \/ m = S n').
omega.
inversion H2.
apply IHn'; assumption.
rewrite H3.
apply (H0 n'); assumption.
Qed.

Lemma weaken : forall P : nat -> Prop,
  (forall n, (forall m, ((m <= n) -> P m))) -> (forall n, P n).
Proof.
  intros P H n.
  apply (H n n).
  apply le_n.
Qed.

Theorem strongind : forall P : nat -> Prop,
  P 0 ->
  (forall n, (forall m, m <= n -> P m) -> P (S n)) ->
  forall n, P n.
Proof.
  intros.
  apply weaken.
  apply strongind_aux; assumption.
Qed.

Fixpoint numNots (s:srac) : nat :=
match s with
| and s1 s2 => numNots s1 + numNots s2
| or s1 s2 => numNots s1 + numNots s2
| single c n => 0
| not s1 => 1 + numNots s1
end.

Ltac unfoldRemoveNotsG :=
match goal with
| [ |- context[removeNots ?s] ] => generalize (removeNots_equation s); intro C; rewrite C in *; clear C
end.

Ltac unfoldRemoveNots H :=
match type of H with
| context[removeNots ?s] => generalize (removeNots_equation s); intro C; rewrite C in *; clear C
end.

Definition P (n: nat) : Prop := forall s:srac, depth s = n -> numNots(removeNots s) = 0.

Lemma notBase : P 0.
Proof.
unfold P.
intros.
induction s.
unfoldRemoveNotsG.
simpl.
trivial.

simpl in H.
exfalso; omega.
simpl in H.
exfalso; omega.
simpl in H.
exfalso; omega.
Qed.

Ltac define s def :=
set (temp := def);
remember temp as s;
unfold temp in *; clear temp.

Lemma notRec : forall (n : nat), (forall (m : nat), m <= n -> P m) -> P (S n).
Proof.
unfold P.
intros.
induction s;
unfoldRemoveNotsG.
unfold numNots.
trivial.

simpl in *.
cut (numNots (removeNots s1) = 0 /\ numNots (removeNots s2) = 0).
omega.
split.
apply (H (depth s1)); omega.
apply (H (depth s2)); omega.

simpl in *.
cut (numNots (removeNots s1) = 0 /\ numNots (removeNots s2) = 0).
omega.
split.
apply (H (depth s1)); omega.
apply (H (depth s2)); omega.

simpl in H0.
induction s.
destruct c; unfold notCheck; simpl; trivial; try solve[repeat findIf].

simpl in *.
cut (numNots (removeNots (not s1)) = 0 /\ numNots (removeNots (not s2)) = 0).
omega.
split.
apply (H (depth s1 + 1)). omega.
simpl.
auto.
apply (H (depth s2 + 1)). omega.
simpl.
auto.

simpl in *.
cut (numNots (removeNots (not s1)) = 0 /\ numNots (removeNots (not s2)) = 0).
omega.
split.
apply (H (depth s1 + 1)). omega.
simpl.
auto.
apply (H (depth s2 + 1)). omega.
simpl.
auto.

apply (H (depth s)).
simpl in H0; omega.
trivial.
Qed.

Lemma notAllDepth : forall (s :srac) (n:nat), P n.
Proof.
intros.
apply (strongind P notBase notRec n).
Qed.

Lemma numNots0 : forall (s :srac), numNots(removeNots s) = 0.
Proof.
intros.
apply (notAllDepth s (depth s)).
trivial.
Qed.

Lemma removeIsntNot : forall (s1 s2 :srac), removeNots s1 = not s2 -> False.
Proof.
intros.
generalize (numNots0 s1); intro.
rewrite H in H0.
simpl in H0.
omega.
Qed.

Fixpoint numOrs (s:srac) : nat :=
match s with
| single c n => 0
| or s1 s2 => 1 + numOrs s1 + numOrs s2
| and s1 s2 => numOrs s1 + numOrs s2
| not s1 => numOrs s1
end.

Function moveOrUp (s:srac) {measure depth s} : srac :=
match s with
| or s1 s2 => or (moveOrUp s1) (moveOrUp s2)
| and s1 s2 => 
  match (s1, s2) with
  | (single c1 z1, single c2 z2) => s
  | (not s3, _) => s (* shouldn't be any*)
  | (_, not s4) => s (* shouldn't be any*)

  | (or s3 s4, _) => or (moveOrUp (and s3 s2)) (moveOrUp (and s4 s2))
  | (_, or s3 s4) => or (moveOrUp (and s1 s3)) (moveOrUp (and s1 s4))

  | (single c1 z1, and s3 s4) => and s1 (moveOrUp s2)
  | (and s3 s4, single c2 z2) => and (moveOrUp s1) s2
  | (and s3 s4, and s5 s6) => and (moveOrUp s1) (moveOrUp s2)
  end
| single c n => s
| not s1 => s (* shouldn't be any*)
end.
intros; simpl; omega.
intros; simpl; omega.
intros; simpl; omega.
intros; simpl; omega.
intros; simpl; omega.
intros; simpl; omega.
intros; simpl; omega.
intros; simpl; omega.
intros; simpl; omega.
intros; simpl; omega.
intros; simpl; omega.
intros; simpl; omega.
intros; simpl; omega.
intros; simpl; omega.
intros; simpl; omega.
intros; simpl; omega.
Defined.

Ltac unfoldMoveOrUpG :=
match goal with
| [ |- context[moveOrUp ?s] ] => generalize (moveOrUp_equation s); intro C; rewrite C in *; clear C
end.

Ltac unfoldMoveOrUp H :=
match type of H with
| context[moveOrUp ?s] => generalize (moveOrUp_equation s); intro C; rewrite C in *; clear C
end.

Fixpoint numAndsOverOr (s:srac) : nat :=
match s with
| or s1 s2 => numAndsOverOr s1 + numAndsOverOr s2
| and s1 s2 => numAndsOverOr s1 + numAndsOverOr s2 + numOrs s1 + numOrs s2
| _ => 0
end.

Definition P2 (n: nat) : Prop := forall (ls : list reqValue) (s : srac), depth s = n -> sracMatch ls (removeNots s) = sracMatch ls s.

Lemma notSoundBase : P2 0.
Proof.
unfold P2.
intros.
induction s;
simpl in H;
omega.
Qed.

Lemma notSoundRec : forall (n : nat), (forall m : nat, m <= n -> P2 m) -> P2 (S n).
Proof.
unfold P2.
intros.
destruct s; 
unfoldRemoveNotsG; trivial;
simpl in *;
try (assert (depth s1 <= n); [omega|]);
try (assert (depth s2 <= n); [omega|]).
cut ((sracMatch ls (removeNots s1) = sracMatch ls s1) /\ (sracMatch ls (removeNots s2) = sracMatch ls s2)).
intro.
destruct H3.
rewrite H3, H4.
trivial. 
split.
apply (H (depth s1) H1 _ _); trivial.
apply (H (depth s2) H2 _ _); trivial.

assert (depth s1 = depth s1); [trivial |].
generalize (H (depth s1) H1 ls s1 H3); intro.
rewrite H4.

assert (depth s2 = depth s2); [trivial |].
generalize (H (depth s2) H2 ls s2 H5); intro.
rewrite H6.
trivial. 

destruct s.
simpl in *.
rewrite (notCheckSoundComp ls c n0).
unfold sracMatch.
trivial.

simpl in *.
assert (depth (not s1) <= n); [simpl; omega|];
assert (depth (not s2) <= n); [simpl; omega|].
cut ((sracMatch ls (removeNots (not s1)) = ~t sracMatch ls s1) /\ (sracMatch ls (removeNots (not s2)) = ~t sracMatch ls s2)).
intro.
destruct H3.
rewrite H3, H4.
destruct (sracMatch ls s1), (sracMatch ls s2); trivial.
simpl.
split.
rewrite (H (depth (not s1)) H1 _ _); trivial.
rewrite (H (depth (not s2)) H2 _ _); trivial.

simpl in *.
assert (depth (not s1) <= n); [simpl; omega|];
assert (depth (not s2) <= n); [simpl; omega|].
assert (depth (not s1) = depth (not s1)); [trivial |].
generalize (H (depth (not s1)) H1 ls (not s1) H3); intro.
rewrite H4.

assert (depth (not s2) = depth (not s2)); [trivial |].
generalize (H (depth (not s2)) H2 ls (not s2) H5); intro.
rewrite H6.
simpl.
destruct (sracMatch ls s1), (sracMatch ls s2); trivial.

simpl in *.
rewrite notsCancel.
apply (H (depth s)); omega.
Qed.

Lemma removeNotSoundComp : forall (ls : list reqValue) (s : srac), sracMatch ls (removeNots s) = sracMatch ls s.
Proof.
intros.
generalize (strongind P2); intro.
apply (H notSoundBase notSoundRec (depth s)).
trivial.
Qed.

Fixpoint distr' (s1 s2 : srac) :=
match s2 with
|or s3 s4 => or (distr' s1 s3) (distr' s1 s4)
| _ => and s1 s2
end.

Fixpoint distr (s1 s2 : srac) : srac :=
match s1 with
| or s3 s4 => or (distr s3 s2) (distr s4 s2)
| _ => distr' s1 s2
end.

Lemma andOrDistributivity1: forall (s1 s2 s3: trilean), (s1 /\t (s2 \/t s3)) = ((s1 /\t s2) \/t (s1 /\t s3)).
Proof.
intros.
destruct s1; destruct s2; destruct s3;
simpl; trivial.
Qed.

Lemma andOrDistributivity2: forall (s1 s2 s3: trilean), ((s1 \/t s2) /\t s3) = ((s1 /\t s3) \/t (s2 /\t s3)).
Proof.
intros.
destruct s1; destruct s2; destruct s3;
simpl; trivial.
Qed.

Ltac distrAndOr :=
match goal with
| [ |- context[(?s1 /\t (?s2 \/t ?s3))] ] => rewrite (andOrDistributivity1 s1 s2 s3) in *
| [ |- context[((?s1 \/t ?s2) /\t ?s3)] ] => rewrite (andOrDistributivity2 s1 s2 s3) in *
end.

Lemma distr'SoundComp : forall (ls : list reqValue) (s1 s2 : srac), sracMatch ls (and s1 s2) = sracMatch ls (distr' s1 s2).
Proof.
intros.
induction s2; 
simpl; trivial.
distrAndOr.
rewrite <- IHs2_1, <- IHs2_2.
simpl; trivial.
Qed.

Lemma distrSoundComp : forall (ls : list reqValue) (s1 s2 : srac), sracMatch ls (and s1 s2) = sracMatch ls (distr s1 s2).
Proof.
intros.
induction s1; simpl;
try solve [rewrite <- distr'SoundComp; simpl; trivial].
rewrite <- IHs1_1, <- IHs1_2.
distrAndOr.
simpl; trivial.
Qed.

Lemma noOrs : forall s : srac, numOrs s = 0 -> numAndsOverOr s = 0.
Proof.
intros.
induction s;
simpl in *;
trivial.
rewrite IHs1, IHs2;
omega.
discriminate H. 
Qed.

Lemma distr'DNF: forall (s1 s2 : srac), numOrs s1 = 0 -> numNots s2 = 0 -> numAndsOverOr s2 = 0 -> numAndsOverOr (distr' s1 s2) = 0.
Proof.
intros.
induction s2;
simpl in *.
rewrite H, (noOrs s1); trivial.
rewrite (noOrs s1); trivial.
omega.
rewrite IHs2_1, IHs2_2; trivial;
omega.
discriminate H0.
Qed.

Lemma distrDNF: forall (s1 s2 : srac), numNots s1 = 0 -> numAndsOverOr s1 = 0 -> numNots s2 = 0 -> numAndsOverOr s2 = 0 -> numAndsOverOr (distr s1 s2) = 0.
Proof.
intros.
induction s1;
simpl in *;
try apply distr'DNF; trivial.
simpl.
omega.
rewrite IHs1_1, IHs1_2; trivial; omega.
discriminate H.
Qed.

Fixpoint DNF (s : srac) : srac :=
match s with
| or s1 s2 => or (DNF s1) (DNF s2)
| and s1 s2 => distr (DNF s1) (DNF s2)
| _ => s
end.

Lemma DNFSoundComp: forall (ls : list reqValue) (s : srac), sracMatch ls s = sracMatch ls (DNF s).
Proof.
intros.
induction s;
simpl; trivial.
rewrite <- distrSoundComp.
simpl.
rewrite IHs1, IHs2.
trivial.
rewrite IHs1, IHs2.
trivial.
Qed.

Lemma numNotsDistr': forall (s1 s2 : srac), numNots s1 = 0 -> numNots s2 = 0 -> numNots (distr' s1 s2) = 0.
Proof.
intros.
induction s2; 
simpl in *; try omega.
rewrite IHs2_1, IHs2_2; omega.
Qed.

Lemma numNotsDNF: forall (s : srac), numNots s = 0 -> numNots (DNF s) = 0.
Proof.
intros.
induction s; 
simpl; trivial.
simpl in H.
assert (numNots (DNF s1) = 0); [apply IHs1; omega |].
assert (numNots (DNF s2) = 0); [apply IHs2; omega |].
clear H IHs1 IHs2.
induction (DNF s1); simpl;
try apply numNotsDistr'; trivial.
rewrite IHs1, IHs2; simpl in *; omega.
rewrite IHs1, IHs2; simpl in *; omega.
Qed.

Definition convertDNF (s : srac) : srac := DNF (removeNots s).

Lemma DNFisDNF: forall (s : srac), numNots s = 0 -> numAndsOverOr (DNF s) = 0.
Proof.
intros.
induction s;
simpl in *; trivial.
apply distrDNF; try auto with *;
apply numNotsDNF; omega.
rewrite IHs1, IHs2; omega.
Qed.

Lemma DNFRemoveNotsisDNF: forall (s : srac), numAndsOverOr (convertDNF s) = 0.
Proof.
intros.
unfold convertDNF.
apply DNFisDNF.
apply numNots0.
Qed.

Lemma convertDNFSoundComp: forall (ls : list reqValue) (s : srac), sracMatch ls s = sracMatch ls (convertDNF s).
Proof.
intros.
unfold convertDNF.
rewrite <- DNFSoundComp.
rewrite removeNotSoundComp.
trivial.
Qed.

Lemma numNotsConvertDNF: forall (s : srac), numNots (convertDNF s) = 0.
Proof.
intros.
unfold convertDNF.
apply numNotsDNF.
apply numNots0.
Qed.

Fixpoint blt_nat (n m : nat) : bool :=
match n, m with
| _, O => false
| O, S m' => true
| S n',S m' => blt_nat n' m'
end.

Fixpoint merge l1 l2 :=
let fix merge_aux  l2 :=
match l1, l2 with
| nil, _ => l2
| _, nil => l1
| (c1, n1)::l1', (c2, n2)::l2' =>
    if blt_nat n1 n2 then (c1, n1) :: merge l1' l2 else 
    if beq_nat n1 n2 then (coreCheck c1 c2, n1) :: merge l1' l2' else
                          (c2, n2) :: merge_aux l2'
end
in merge_aux l2.

Fixpoint split' (s : srac) : list (core * nat) :=
match s with
| and s1 s2 => merge (split' s1) (split' s2)
| single c n => (c, n) :: nil
| _ => nil
end.

Fixpoint split (s : srac) : list (list (core * nat)) :=
match s with
| or s1 s2 => split s1 ++ split s2
| _ => split' s :: nil
end.

Definition toLists (s :srac): list (list (core*nat)) := split (convertDNF s).

Fixpoint lMatch (lc : list (core*nat)) (lr : list reqValue) : trilean := 
match lc with
| nil => T
| (c,n):: lc' => (coreMatch (nth n lr blank) c) /\t (lMatch lc' lr)
end.

Fixpoint llMatch (llc : list (list (core*nat))) (lr : list reqValue) : trilean := 
match llc with
| nil => F
| lc :: llc' => (lMatch lc lr) \/t (llMatch llc' lr)
end.

Lemma mergeNil : forall l : list (core * nat), merge nil l = l.
Proof.
intros.
induction l; simpl;
trivial.
Qed.

Lemma mergeNil2 : forall l : list (core * nat), merge l nil = l.
Proof.
intros.
induction l; simpl;
trivial.
destruct a.
trivial. 
Qed.

Lemma andTrue : forall t : trilean, (t /\t T) = t.
Proof.
induction t;
trivial.
Qed.

Definition P3' (n: nat) : Prop :=
forall (l1 l2 : list (core * nat)) (lr : list reqValue), length l1 + length l2 = n -> 
lMatch (merge l1 l2) lr = (lMatch l1 lr /\t lMatch l2 lr).

Lemma mergeBase : P3' 0.
Proof.
unfold P3'.
intros.
destruct l1; destruct l2; simpl in *; trivial; omega.
Qed.

Lemma andAssoc : forall (t1 t2 t3: trilean), ((t1 /\t t2) /\t t3) = (t1 /\t (t2 /\t t3)).
Proof.
intros.
destruct t1, t2, t3; simpl; trivial.
Qed.

Lemma mergeNoNils : forall (l1 l2 : list (core * nat)) (c1 c2 : core) (n1 n2 : nat),
(merge ((c1, n1):: l1) ((c2, n2):: l2) = (c1, n1) :: merge l1 ((c2, n2):: l2)) \/
((merge ((c1, n1):: l1) ((c2, n2):: l2) = (coreCheck c1 c2, n1) :: merge l1 l2) /\ (beq_nat n1 n2) = true) \/
(merge ((c1, n1):: l1) ((c2, n2):: l2) = (c2, n2) :: merge ((c1, n1):: l1) l2).
Proof.
intros.
simpl.
caseSimpl (blt_nat n1 n2); [left| right].
trivial.

caseSimpl (beq_nat n1 n2); [left| right].
split; trivial.
trivial.
Qed. 

Lemma mergeRec : forall (n : nat), (forall m : nat, m <= n -> P3' m) -> P3' (S n).
Proof.
unfold P3'.
intros.
destruct l1.
rewrite mergeNil.
simpl.
trivial.

destruct l2.
rewrite mergeNil2.
unfold lMatch at 3.
rewrite andTrue.
trivial.
destruct p, p0.
generalize (mergeNoNils l1 l2 c c0 n0 n1); intro.
destruct H1.
rewrite H1.
simpl.
rewrite (H n); trivial.
simpl.
repeat (rewrite andAssoc).
trivial. 
simpl in *; omega.

destruct H1.
destruct H1.
rewrite H1.
simpl.
rewrite (H (pred n)).
simpl.
rewrite coreCheckCorrect.
rewrite (beq_nat_true n0 n1); trivial.
repeat (rewrite andAssoc).
rewrite (trileanAndSym (lMatch l1 lr) (coreMatch (nth n1 lr blank) c0 /\t lMatch l2 lr)).
repeat (rewrite andAssoc).
rewrite (trileanAndSym (lMatch l1 lr) (lMatch l2 lr)).
trivial.
omega.
simpl in *; omega.

rewrite H1.
unfold lMatch; fold lMatch.
rewrite (H n); trivial.
simpl.
rewrite (trileanAndSym (coreMatch (nth n1 lr blank) c0) ((coreMatch (nth n0 lr blank) c /\t lMatch l1 lr) /\t lMatch l2 lr)).
repeat (rewrite andAssoc).
rewrite (trileanAndSym (lMatch l2 lr) (coreMatch (nth n1 lr blank) c0)).
trivial. 
simpl in *; omega.
Qed.

Lemma mergeCorrect : forall (l1 l2 : list (core * nat)) (lr : list reqValue),
lMatch (merge l1 l2) lr = (lMatch l1 lr /\t lMatch l2 lr).
Proof.
intros.
generalize (strongind P3'); intro.
apply (H mergeBase mergeRec (length (l1++l2))).
symmetry.
apply app_length.
Qed.

Definition P3 (n: nat) : Prop :=
forall (s : srac) (lr : list reqValue), depth s = n -> 
numNots s = 0 -> numOrs s = 0 -> lMatch (split' s) lr = sracMatch lr s.

Lemma listCorrectBase : P3 0.
Proof.
unfold P3.
intros.
destruct s;
simpl in *;
try omega.
Qed.

Lemma listCorrectRec : forall (n : nat), (forall m : nat, m <= n -> P3 m) -> P3 (S n).
Proof.
unfold P3.
intros.
destruct s;
simpl in *;
try omega.

rewrite andTrue; trivial.
assert (depth s1 <= n  /\ depth s2 <= n); [omega|].
destruct H3.
rewrite <- (H (depth s1) H3 s1); try omega.
rewrite <- (H (depth s2) H4 s2); try omega.
apply mergeCorrect.
Qed.


Lemma listCorrect : forall (s : srac) (lr : list reqValue),
numNots s = 0 -> numOrs s = 0 -> lMatch (split' s) lr = sracMatch lr s.
Proof.
intros.
generalize (strongind P3); intro.
apply (H1 listCorrectBase listCorrectRec (depth s)); trivial.
Qed.


Lemma llCorrect:forall (s : srac) (lr : list reqValue),
llMatch (toLists s) lr = sracMatch lr s.
Proof.
intros.
unfold toLists.
rewrite convertDNFSoundComp.
generalize (DNFRemoveNotsisDNF s); intro.
generalize (numNotsConvertDNF s); intro.
induction (convertDNF s); simpl.
destruct (coreMatch (nth n lr blank) c); trivial.
simpl in H, H0.
rewrite mergeCorrect.
rewrite listCorrect; try omega.
rewrite listCorrect; try omega.
destruct (sracMatch lr s0_1 /\t sracMatch lr s0_2); trivial.
simpl in H, H0.
rewrite <- IHs0_1; try omega.
rewrite <- IHs0_2; try omega.
clear.
induction (split s0_1).
simpl; trivial.
simpl.
rewrite IHl.
destruct (lMatch a lr); destruct (llMatch l lr); destruct (llMatch (split s0_2) lr); simpl; trivial.
simpl in H0.
discriminate H0.
Qed.