(****************************************************************
   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 ZArith.
Require Export Bool.

Open Scope Z_scope.

Infix "<=b" := Zle_bool (at level 70): Z_scope.
Infix "<b" := Zlt_bool (at level 70): Z_scope.
Notation "A /\b B" := (andb A B) (at level 80, right associativity).
Notation "A \/b B" := (orb A B) (at level 85, right associativity).

(* a few simple lemmas used by tactics *)
Lemma Zlt_bool_imp_lt : forall n m:Z, Zlt_bool n m = true -> (n < m).
Proof.
intros.
generalize (Zlt_is_lt_bool n m).
intuition.
Qed.

Lemma Zlt_imp_lt_bool : forall n m:Z, (n < m) -> Zlt_bool n m = true.
Proof.
intros.
generalize (Zlt_is_lt_bool n m).
intuition.
Qed.

Lemma andbSplit :
forall b1 b2:bool, (b1 && b2) = true -> b1 = true /\ b2 = true.
Proof.
auto with *.
Qed.

Lemma splitB : forall b1 b2 : bool, b1 = true -> b2 = true -> (b1 && b2) = true.
Proof.
auto with *.
Qed.

Lemma orOrb: forall  b1 b2 : bool, b1 = true \/ b2 = true -> (b1 || b2) = true.
Proof.
auto with *.
Qed.

Lemma deMorganOr: forall (a b: bool), (a || b) = false -> a = false /\ b = false.
Proof.
induction a; induction b; tauto.
Qed.

Lemma deMorganAnd: forall (a b: bool), (a && b) = false -> a = false \/ b = false.
Proof.
induction a; induction b; tauto.
Qed.

Lemma Nlt_Nltbool: forall A B: Z, ~A < B -> (A <b B = false).
Proof.
intros.
case_eq (A <b B).
intros.
generalize (Zlt_cases A B); intro.
rewrite H0 in H1.
tauto.
trivial.
Qed.

Lemma Nle_Nlebool: forall A B: Z, ~A <= B -> (A <=b B = false).
Proof.
intros.
case_eq (A <=b B).
intros.
generalize (Zle_cases A B); intro.
rewrite H0 in H1.
tauto.
trivial.
Qed.

Lemma eqLe : forall A B:Z, (A = B) -> (A <=b B) = true.
intros.
generalize (Zle_imp_le_bool A B).
auto with *.
Qed.

Lemma flip': forall A B:Z, 0 <= A -> ~A + B < B.
Proof.
intros; omega.
Qed.

Lemma flip: forall A B:Z, 0 <= A -> (A + B <b B) = false.
Proof.
intros.
generalize (flip' A B H); intro.
generalize (Zlt_is_lt_bool (A + B) B); intro.
case_eq (A + B <b B); intro;
tauto.
Qed.

(* tries to decide if H, an inequality, is true or false 
   Also test each part of ands, ors and if statements *)
Ltac test H :=
first [
match goal with 
 | x : H = true |- _ => rewrite x in *
 | x : H = false |- _ => rewrite x in *
 | x : true = H |- _ => rewrite <- x in *
 | x : false = H |- _ => rewrite <- x in *
end|
 match H with
  | ?A + ?B <b _ => 
     match goal with
     | x : 0 <= A |- _  => generalize (flip A B x); intro temp; try rewrite temp in *; clear temp
    end
   | ?A <=b ?A => generalize (Zle_refl A) ; intro temp;  generalize (Zle_imp_le_bool _ _ temp); intro temp2; try rewrite temp2 in *; clear temp temp2
   | ?A <=b ?B =>  
     match goal with
     | x : ~A <= B |- _ => generalize (Nle_Nlebool _ _ x); intro temp;  try rewrite temp in *; clear temp
     | x :  B <  A |- _ => generalize (Zlt_not_le _ _ x) ; intro temp;  generalize (Nle_Nlebool _ _ temp); intro temp2;  try rewrite temp2 in *; clear temp temp2
     | x :  A <= B |- _ => generalize (Zle_imp_le_bool _ _ x); intro temp; try rewrite temp in *; clear temp
     | x :  A <  B |- _ => generalize (Zlt_le_weak _ _ x) ; intro temp;  generalize (Zle_imp_le_bool _ _ temp); intro temp2; try rewrite temp2 in *; clear temp temp2
     | x :  A =  B |- _ => generalize (eqLe _ _ x) ; intro temp; try rewrite temp in *; clear temp
     | x :  B =  A |- _ => symmetry in x; generalize (eqLe _ _ x) ; intro temp; try rewrite temp in *; clear temp
     end

  |  ?A <b ?B =>
    match goal with
     | x : ~A < B |- _ => generalize (Nlt_Nltbool _ _ x); intro temp;  try rewrite temp in *; clear temp
     | x : B <  A |- _ => generalize (Zlt_le_weak _ _ x) ; intro temp; generalize (Zle_not_lt _ _ temp) ; intro temp2; generalize (Nlt_Nltbool _ _ temp2); intro temp3;  try rewrite temp3 in *; clear temp temp2 temp3
     | x : B <= A |- _ => generalize (Zle_not_lt _ _ x) ; intro temp;  generalize (Nlt_Nltbool _ _ temp); intro temp2;  try rewrite temp2 in *; clear temp temp2
     | x : A <  B |- _  => generalize (Zlt_imp_lt_bool _ _ x); intro temp;  try rewrite temp in *; clear temp
    end
  | ?A = ?B => first[test A| test B]
  | if ?A then _ else _ => test A
  | ?A = ?B => first[test A| test B]
  | ?A && ?B => first[test A| test B]
  | ?A \/ ?B => first[test A| test B]

  | ?A && ?B => first[test A| test B]
  | ?A /\ ?B => first[test A| test B]
  | ?A || ?B => first[test A| test B]
  | ?A \/ ?B => first[test A| test B]
end].

(* Some tactics (and lemmas to use them) used to simplify proofs *)
(* Converts bools into Props *)

Ltac caseSimpl b :=
case_eq b; 
let C := fresh "C" in 
intro C;
try rewrite C in *.

Lemma NLeB_NLe: forall A B: Z, (A <=b B) = false -> ~A <= B.
Proof.
intros.
generalize (Zle_is_le_bool A B); intro.
caseSimpl (A <=b B).
auto with *.
intuition.
Qed.

Lemma NLtB_NLt: forall A B: Z, (A <b B) = false -> ~A < B.
Proof.
intros.
generalize (Zlt_is_lt_bool A B); intro.
caseSimpl (A <b B).
auto with *.
intuition.
Qed.

Ltac b2PH := 
repeat
match goal with
  | [ x : Zeq_bool ?a ?b = true |- _ ] => generalize (Zeq_bool_eq a b x); clear x; intro x
  | [ x : Zeq_bool ?a ?b = false |- _ ] => generalize (Zeq_bool_neq a b x); clear x; intro x
  
  | [ x : (true /\b ?b) = true |- _ ] => generalize (andbSplit _ _ x); clear x; intro x; elim x; clear x; intros temp1 x; clear temp1; split; trivial
  | [ x : (?a /\b ?b) = true |- _ ] => generalize (andbSplit _ _ x); clear x; intro x; destruct x; try eauto; try omega
  | [ x : (?a \/b ?b) = true |- _ ] => generalize (orb_prop _ _ x); clear x; intro x; destruct x

  | [ x : (?a /\b ?b) = false |- _ ] => generalize (deMorganAnd _ _ x); clear x; intro x; destruct x
  | [ x : (?a \/b ?b) = false |- _ ] => generalize (deMorganOr _ _ x); clear x; intro x; destruct x

  | [ x : (?a <b ?b) = true |- _ ] => generalize (Zlt_bool_imp_lt _ _ x); clear x; intro x
  | [ x : (?a <=b ?b) = true |- _ ] => generalize (Zle_bool_imp_le _ _ x); clear x; intro x

  | [ x : (?a <b ?b) = false |- _ ] => generalize (NLtB_NLt _ _ x); clear x; intro x
  | [ x : (?a <=b ?b) = false |- _ ] => generalize (NLeB_NLe _ _ x); clear x; intro x

  | [ x : (if ?a then _ else _) = true |- _] => split; intro; test a
end.

Lemma aebZeq: forall a b:Z, a = b -> Zeq_bool a b = true.
Proof.
intros.
generalize (Zeq_is_eq_bool a b); intro.
destruct H0.
apply (H0 H).
Qed.

Lemma LeGt2: forall a b : Z, a <= b \/ b < a.
Proof.
intros; omega.
Qed.

Ltac b2P :=
repeat
match goal with
  | [x : (?a <= ?b -> _) /\ _ |- _ ] => generalize (LeGt2 a b); intro temp; elim temp; clear temp; intro temp3; test(a <=b b); elim x; clear x; [intros x temp| intros temp x]; clear temp; generalize (x temp3); clear temp3 x; intro x
  | [x : _ /\ _ |- ((?a /\b ?b) = true)] => apply (splitB a b); elim x; clear x; intro x; [intro temp; clear temp | clear x; intro x]
  | [x : _ \/ _  |- ((?a \/b ?b) = true)] => apply (orOrb a b); destruct x; [left | right]
  | [ |- ((?a <b ?b) = true)] => apply (Zlt_imp_lt_bool a b)
  | [ |- ((?a <=b ?b) = true)] => apply (Zle_imp_le_bool a b)
  | [ |- Zeq_bool ?a ?b = true ] => apply aebZeq
end.

Ltac caseSimplParts b :=
first [
match b with 
| true => fail 1
| false => fail 1
| _ => test b
end|
match b with
| ?A /\b ?B => caseSimplParts A; caseSimplParts B
| ?A \/b ?B => caseSimplParts A; caseSimplParts B
| context[if ?A then _ else _] => caseSimplParts A
| true => idtac
| false => idtac
| _ => caseSimpl b
end].

Ltac findIf :=
match goal with
| [ |- context[if ?X then _ else _] ] => caseSimplParts X; simpl; trivial
end.