(* Conflict detection for firewall rules *)
(* Venanzio Capretta and Bernard Stepien *)
(* May 2006                              *)
(* Feb 2015: updated to Coq version 8.4  *)

Require Export Arith.
Require Export ZArith.
Require Export List.
Require Export Sumbool.
Require Export bytes_masks.

(* PREMISE *)

(* Projection on lists, without default value. *)
Fixpoint Nth (A:Set)(l:list A){struct l}:
  forall i:nat, (i<length l)%nat -> A :=
match l return forall i:nat, (i<length l)%nat -> A with
  nil => fun i H => False_rec A (lt_n_O i H)
| cons a l => fun i =>
     match i return (i<length (cons a l))%nat -> A with
       0 => fun H => a
     | S i => fun H => Nth A l i (lt_S_n i (length l) H)
     end
end.

Implicit Arguments Nth [A].

Lemma Nth_proof_independent:
  forall (A:Set)(l:list A)(i:nat)(H1 H2:(i<length l)%nat),
    Nth l i H1 = Nth l i H2.
Proof.
intros A l; elim l; simpl.
intros i H1; elim (lt_n_O i H1).
intros a l' IH i; case i.
trivial.
intros i' H1 H2; apply IH.
Qed.

(* Dependent conjunction. *)
Inductive dep_and (A:Prop)(B:A->Prop): Prop :=
  dep_pair: forall (a:A)(b:B a), dep_and A B.

Notation " { A ** B } " := (dep_and A B).


(* Some small lemmas about order on natural numbers
   not provided by the library. *)

Lemma lt_0_lt_minus:
  forall n m:nat, lt n m -> lt 0 (m-n).
Proof.
intros n m H.
apply plus_lt_reg_l with n.
rewrite plus_0_r.
rewrite le_plus_minus_r.
exact H.
apply lt_le_weak.
exact H.
Qed.

Lemma minus_S_pred: forall n m:nat, n-(S m) = pred (n-m).
Proof.
induction n; simpl.
trivial.
intros m; case m; simpl.
symmetry; apply minus_n_O.
exact IHn.
Qed.

(* DEFINITION OF REQUESTS *)

Open Scope Z_scope.

Inductive action: Set :=
        | permit : action
        | deny : action.

Inductive protocol : Set :=
	| udp : protocol
	| tcp : protocol.

(* Port numbers are just integers (Z). *)
Definition port_number: Set := Z.

(* ip_address is defined in bytes_masks. *)

Record request: Set := ask_request {
  req_protocol: protocol;
  req_source_ip: ip_address;
  req_source_pn: port_number;
  req_dest_ip: ip_address;
  req_dest_pn: port_number
}.

(* DEFINITION OF RULES AND RULE SETS. *)

(* ip ranges are defined in bytes_masks.v *)

Definition pn_interval := (port_number*port_number)%type.

Record access_rule: Set := rule {
  r_action: action;
  r_protocol: protocol;
  r_source_ip: ip_range;
  r_source_pn: pn_interval;
  r_dest_ip: ip_range;
  r_dest_pn: pn_interval
}.

Definition rule_set:= list access_rule.

(* Semantics of rules and rule sets. *)

Definition pn_match: port_number -> pn_interval -> Prop :=
fun pn pni => let (i1,i2):=pni in (i1 <= pn <= i2).

Definition rule_permit: access_rule -> request -> Prop :=
fun rl rq => 
  r_action rl = permit /\
  req_protocol rq = r_protocol rl /\
  ip_match (req_source_ip rq) (r_source_ip rl) /\
  pn_match (req_source_pn rq) (r_source_pn rl) /\
  ip_match (req_dest_ip rq) (r_dest_ip rl) /\
  pn_match (req_dest_pn rq) (r_dest_pn rl).

Definition rule_deny: access_rule -> request -> Prop :=
fun rl rq => 
  r_action rl = deny /\
  req_protocol rq = r_protocol rl /\
  ip_match (req_source_ip rq) (r_source_ip rl) /\
  pn_match (req_source_pn rq) (r_source_pn rl) /\
  ip_match (req_dest_ip rq) (r_dest_ip rl) /\
  pn_match (req_dest_pn rq) (r_dest_pn rl).

Definition rule_conflict: access_rule -> access_rule -> Prop :=
fun r1 r2 =>
  exists r:request, (rule_permit r1 r /\ rule_deny r2 r) \/
                    (rule_deny r1 r /\ rule_permit r2 r).

Definition rs_conflict: rule_set -> nat -> nat -> Prop :=
fun rs i j =>
  {(i < (length rs))%nat ** fun Hi =>
  {(j < (length rs))%nat ** fun Hj =>
   (rule_conflict (Nth rs i Hi) (Nth rs j Hj))}}.

(* THE CONFLICT DETECTION PROGRAM *)

(* Boolean functions to decide each field. *)

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

Definition protocol_bool: protocol -> protocol -> bool :=
fun pt1 pt2 =>
match pt1, pt2 with
  udp, udp => true
| tcp, tcp => true
| _  , _   => false
end.

Lemma protocol_bool_id: 
  forall p:protocol, protocol_bool p p = true.
Proof.
intro p; case p; auto.
Qed.

(* ip_address_bool is defined in bytes_masks *)

Definition pn_bool: pn_interval -> pn_interval -> bool :=
fun pn1 pn2 =>
match pn1 with (x1,y1) =>
match pn2 with (x2,y2) =>
  andb (andb (Zle_bool x1 y1) (Zle_bool x2 y2))
       (andb (Zle_bool x1 y2) (Zle_bool x2 y1))
end
end.

(* Check if there is a conflict between two rules *)

Definition conflict_check: access_rule -> access_rule -> bool :=
fun r1 r2 =>
match r1 with (rule a1 pt1 sip1 spn1 dip1 dpn1) =>
match r2 with (rule a2 pt2 sip2 spn2 dip2 dpn2) =>
  if (action_bool a1 a2)
  then false  (* same action, no conflict *)
  else andb (protocol_bool pt1 pt2)  (* same protocol *)
       (andb (ip_address_bool sip1 sip2)  (* source ip ranges intersect *)
       (andb (pn_bool spn1 spn2)  (* source port numbers intersect *)
       (andb (ip_address_bool dip1 dip2)  (* dest   ip ranges intersect *)
             (pn_bool dpn1 dpn2)  (* dest   port numbers intersect *)
       )))
end
end.

(* Finds conflicts between a rule and a rule set:
     i = position of the rule r in the original rule set
     n = position of the first rule of rs in the original rule set
*)

Fixpoint rrs_conflicts (i n:nat)(r:access_rule)(rs:rule_set){struct rs}:
  list (nat*nat) :=
match rs with
  nil => nil
| (cons rh rt) => if (conflict_check r rh)
                  then (i,n)::(rrs_conflicts i (S n) r rt)
                  else (rrs_conflicts i (S n) r rt)
end.

(* Tail-recursive version. *)

Fixpoint rrs_conflicts_tl
  (i:nat)(l:list (nat*nat))(n:nat)(r:access_rule)(rs:rule_set){struct rs}:
  list (nat*nat) :=
match rs with
  nil => l
| (cons rh rt) => if (conflict_check r rh)
                  then (rrs_conflicts_tl i ((i,n)::l) (S n) r rt)
                  else (rrs_conflicts_tl i l (S n) r rt)
end.

Lemma rrs_conflicts_tl_app:
  forall (i:nat)(l:list (nat*nat))(n:nat)(r:access_rule)(rs:rule_set),
    rrs_conflicts_tl i l n r rs = (rrs_conflicts_tl i nil n r rs) ++ l.
Proof.
intros i l n r rs; generalize n; clear n; generalize l; clear l; elim rs; simpl.
trivial.
intros rl rs' IH l n.
case (conflict_check r rl).
rewrite IH.
rewrite IH with (l:=(i,n)::nil).
rewrite app_ass.
rewrite <- app_comm_cons.
trivial.
apply IH.
Qed.

Lemma rrs_conflicts_tl_equivalence:
  forall (i n:nat)(r:access_rule)(rs:rule_set),
    rrs_conflicts i n r rs = rev (rrs_conflicts_tl i nil n r rs).
Proof.
intros i n r rs; generalize n; clear n; elim rs; simpl.
trivial.
intros a l IH n.
case (conflict_check r a).
rewrite rrs_conflicts_tl_app.
rewrite distr_rev; simpl.
rewrite IH.
trivial.
apply IH.
Qed.

(* Find conflicts (assuming that rs starts with rule number n *)

Fixpoint conflicts_aux (n:nat)(rs:rule_set){struct rs}:
  list (nat*nat) :=
match rs with
  nil => nil
| (cons r rs') => (rrs_conflicts n (S n) r rs') ++ (conflicts_aux (S n) rs')
end.

(* Tail recursive version. *)
Fixpoint conflicts_aux_tl (l:list (nat*nat))(n:nat)(rs:rule_set){struct rs}:
  list (nat*nat) :=
match rs with
  nil => l
| (cons r rs') => (conflicts_aux_tl (rrs_conflicts_tl n l (S n) r rs') (S n) rs')
end.

Lemma conflicts_aux_tl_app:
  forall (l:list (nat*nat))(n:nat)(rs:rule_set),
  conflicts_aux_tl l n rs = (conflicts_aux_tl nil n rs) ++ l.
Proof.
intros l n rs; generalize n; generalize l; clear n; clear l; elim rs; simpl.
trivial.
intros rl rs' IH l n.
rewrite IH.
rewrite IH with (l:= rrs_conflicts_tl n nil (S n) rl rs').
rewrite app_ass.
rewrite rrs_conflicts_tl_app.
trivial.
Qed.

Lemma conflicts_aux_tl_equivalence:
  forall (n:nat)(rs:rule_set),
  conflicts_aux n rs = rev (conflicts_aux_tl nil n rs).
Proof.
intros n rs; generalize n; clear n; elim rs; simpl.
trivial.
intros rl rs' IH n.
rewrite conflicts_aux_tl_app.
rewrite distr_rev.
rewrite IH.
rewrite rrs_conflicts_tl_equivalence.
trivial.
Qed.

(* The conflict-detection program. *)

Definition find_conflicts: rule_set -> list (nat*nat)
:= conflicts_aux 0.

(* Tail-recursive version. *)

Definition find_conflicts_tl: rule_set -> list (nat*nat)
:= conflicts_aux_tl nil 0.

Theorem find_conflicts_tl_equivalence:
  forall rs:rule_set, find_conflicts rs = rev (find_conflicts_tl rs).
Proof.
intro rs; unfold find_conflicts; unfold find_conflicts_tl.
apply conflicts_aux_tl_equivalence.
Qed.

(* SOUNDNESS AND COMPLETENESS OF THE ALGORITHM *)

(* Soundness *)

(* ip_range_intersection is defined in bytes_masks.v *)

Lemma pn_range_intersection:
  forall pn1 pn2:pn_interval, (pn_bool pn1 pn2)=true ->
    exists pn:port_number, pn_match pn pn1 /\ pn_match pn pn2.
Proof.
intros [x1 y1] [x2 y2] H; simpl in H.
generalize (andb_prop _ _ H); clear H; intros [H1 H2].
generalize (andb_prop _ _ H1); clear H1; intros [H11 H12].
generalize (andb_prop _ _ H2); clear H2; intros [H21 H22].
generalize (Zle_bool_imp_le _ _ H11); clear H11; intro H11.
generalize (Zle_bool_imp_le _ _ H12); clear H12; intro H12.
generalize (Zle_bool_imp_le _ _ H21); clear H21; intro H21.
generalize (Zle_bool_imp_le _ _ H22); clear H22; intro H22.
case (Z_le_gt_dec x1 x2); intro HH.
exists x2; split; simpl.
auto.
split; [apply Zle_refl | auto].

exists x1; split; simpl.
split; [apply Zle_refl | auto].
split; [apply Zlt_le_weak; apply Zgt_lt; auto | auto].
Qed.

Lemma conflict_check_action:
  forall r1 r2:access_rule,
    conflict_check r1 r2 = true
    -> (r_action r1 = permit /\ r_action r2 = deny) \/
       (r_action r1 = deny /\ r_action r2 = permit).
Proof.
intros [a1 pt1 sip1 spn1 dip1 dpn1] [a2 pt2 sip2 spn2 dip2 dpn2];
  case a1; case a2; simpl; intro H; try (discriminate H).
left; auto.
right; auto.
Qed.

Lemma conflict_check_protocol:
  forall r1 r2:access_rule,
    conflict_check r1 r2 = true
    -> (r_protocol r1) = (r_protocol r2).
Proof.
intros  [a1 pt1 sip1 spn1 dip1 dpn1] [a2 pt2 sip2 spn2 dip2 dpn2];
  simpl; case (action_bool a1 a2); case pt1; case pt2; simpl; intro H;
  try (discriminate H); try trivial.
Qed.

Lemma conflict_check_sip:
  forall r1 r2: access_rule,
    conflict_check r1 r2 =true
    -> ip_address_bool (r_source_ip r1) (r_source_ip r2) = true.
Proof.
intros [a1 pt1 sip1 spn1 dip1 dpn1]  [a2 pt2 sip2 spn2 dip2 dpn2]; simpl.
case (action_bool a1 a2); simpl; intro H.
discriminate H.
generalize (andb_prop _ _ H); clear H; intros [_ H].
generalize (andb_prop _ _ H); clear H; intros [H _].
exact H.
Qed.

Lemma conflict_check_dip:
  forall r1 r2: access_rule,
    conflict_check r1 r2 =true
    -> ip_address_bool (r_dest_ip r1) (r_dest_ip r2) = true.
Proof.
intros [a1 pt1 sip1 spn1 dip1 dpn1]  [a2 pt2 sip2 spn2 dip2 dpn2]; simpl.
case (action_bool a1 a2); simpl; intro H.
discriminate H.
generalize (andb_prop _ _ H); clear H; intros [_ H].
generalize (andb_prop _ _ H); clear H; intros [_ H].
generalize (andb_prop _ _ H); clear H; intros [_ H].
generalize (andb_prop _ _ H); clear H; intros [H _].
exact H.
Qed.

Lemma conflict_check_spn:
  forall r1 r2: access_rule,
    conflict_check r1 r2 =true
    -> pn_bool (r_source_pn r1) (r_source_pn r2) = true.
Proof.
intros [a1 pt1 sip1 spn1 dip1 dpn1]  [a2 pt2 sip2 spn2 dip2 dpn2]; simpl.
case (action_bool a1 a2); simpl; intro H.
discriminate H.
generalize (andb_prop _ _ H); clear H; intros [_ H].
generalize (andb_prop _ _ H); clear H; intros [_ H].
generalize (andb_prop _ _ H); clear H; intros [H _].
exact H.
Qed.

Lemma conflict_check_dpn:
  forall r1 r2: access_rule,
    conflict_check r1 r2 =true
    -> pn_bool (r_dest_pn r1) (r_dest_pn r2) = true.

Proof.
intros [a1 pt1 sip1 spn1 dip1 dpn1]  [a2 pt2 sip2 spn2 dip2 dpn2]; simpl.
case (action_bool a1 a2); simpl; intro H.
discriminate H.
generalize (andb_prop _ _ H); clear H; intros [_ H].
generalize (andb_prop _ _ H); clear H; intros [_ H].
generalize (andb_prop _ _ H); clear H; intros [_ H].
generalize (andb_prop _ _ H); clear H; intros [_ H].
exact H.
Qed.

Lemma conflict_check_soundness:
  forall r1 r2: access_rule,
    conflict_check r1 r2 = true -> rule_conflict r1 r2.
Proof.
intros r1 r2 H; red.
generalize (conflict_check_protocol r1 r2 H); intro Hpt.
generalize (conflict_check_sip r1 r2 H); intro Hip.
case (ip_range_intersection _ _ Hip);
  clear Hip; intros sip [Hsip1 Hsip2].
generalize (conflict_check_spn r1 r2 H); intro Hpn.
case (pn_range_intersection _ _ Hpn);
  clear Hpn; intros spn [Hspn1 Hspn2].
generalize (conflict_check_dip r1 r2 H); intro Hip.
case (ip_range_intersection _ _ Hip);
  clear Hip; intros dip [Hdip1 Hdip2].
generalize (conflict_check_dpn r1 r2 H); intro Hpn.
case (pn_range_intersection _ _ Hpn);
  clear Hpn; intros dpn [Hdpn1 Hdpn2].
exists (ask_request (r_protocol r1) sip spn dip dpn).
case (conflict_check_action r1 r2 H); intros [Ha1 Ha2].
left; split; red; repeat (split; try assumption).
right; split; red; repeat (split; try assumption).
Qed.

(* rrs_conflict_res r rs n means that there is a conflict between
   r and the nth rule of rs
*)
Inductive rrs_conflict_rel (r:access_rule): rule_set -> nat -> Prop :=
  rrs_conflict_head:
    forall (rh:access_rule)(rt:rule_set),
      rule_conflict r rh -> rrs_conflict_rel r (rh::rt) 0
| rrs_conflict_tail:
    forall (rh:access_rule)(rt:rule_set)(n:nat),
      rrs_conflict_rel r rt n -> rrs_conflict_rel r (rh::rt) (S n).

Lemma rrs_conflicts_n_le_j:
  forall (i i':nat)(r:access_rule)(rs:rule_set)(j n:nat),
    In (i,j) (rrs_conflicts i' n r rs) -> (n<=j)%nat.
Proof.
intros i i' r rs; elim rs; simpl.
intros j n H; elim H.
intros r0 rs' IH j n.
case (conflict_check r r0); simpl.
intros H; case H; clear H; intro H.
injection H; clear H; intros Hi Hj.
rewrite Hi; apply le_n.
apply le_Sn_le; apply IH; exact H.
intro H; apply le_Sn_le; apply IH; exact H.
Qed.

Lemma rrs_conflicts_soundness:
  forall (i i':nat)(r:access_rule)(rs:rule_set)(j n:nat),
    In (i,j) (rrs_conflicts i' n r rs) -> 
    i'=i /\ rrs_conflict_rel r rs (j-n)%nat.
Proof.
intros i i' r rs; elim rs; simpl.
intros j n H; elim H.
intros r0 rs' IH j n.
generalize (conflict_check_soundness r r0).
case (conflict_check r r0); simpl.
intros H0 H; case H; clear H; intro H.
injection H; clear H; intros H1 H2.
split.
exact H2.
rewrite H1; rewrite <- minus_n_n.
apply rrs_conflict_head.
apply H0; trivial.
generalize (IH j (S n) H); intros [IH1 IH2].
split.
exact IH1.
rewrite (S_pred (j-n) 0).
apply rrs_conflict_tail.
rewrite <- minus_S_pred.
exact IH2.
apply lt_0_lt_minus.
red; eapply rrs_conflicts_n_le_j; apply H.

intros _ H; generalize (IH j (S n) H); intros [IH1 IH2].
split.
exact IH1.
rewrite (S_pred (j-n) 0).
apply rrs_conflict_tail.
rewrite <- minus_S_pred.
exact IH2.
apply lt_0_lt_minus.
red; eapply rrs_conflicts_n_le_j; apply H.
Qed.

Lemma rrs_conflict_rel_rs_conflict_aux:
  forall (r:access_rule)(rs:rule_set)(m:nat), rrs_conflict_rel r rs m ->
    forall n:nat, (n = S m) -> rs_conflict (r::rs) 0 n.
Proof.
intros r rs m H; elim H.
intros rh rt Hr n Hn1.
rewrite Hn1; red.
cut (0<S (length (rh::rt)))%nat.
intro HH1; exists HH1.
cut (1<S (S (length rt)))%nat.
intro HH2; exists HH2.
exact Hr.
apply lt_n_S; apply lt_O_Sn.
apply lt_O_Sn.

intros rh rt m' Hm' IH n Hn.
rewrite Hn.
generalize (IH (S m') (refl_equal (S m'))); intros [H1 [H2 H3]].
red.
exists (lt_O_Sn (length (rh::rt))). 
exists (lt_n_S _ _ H2).
simpl; simpl in H3.
rewrite Nth_proof_independent with (H2:=lt_S_n m' (length rt) H2).
exact H3.
Qed.

Lemma rrs_conflict_rel_rs_conflict:
  forall (r:access_rule)(rs:rule_set)(n:nat),
    (0<n)%nat -> rrs_conflict_rel r rs (pred n) -> rs_conflict (r::rs) 0 n.
Proof.
intros r rs n Hn H; apply rrs_conflict_rel_rs_conflict_aux with (m:=pred n).
exact H.
apply S_pred with (m:=0%nat).
exact Hn.
Qed.

Lemma rs_conflict_cons:
  forall (r:access_rule)(rs:rule_set)(i j:nat),
    rs_conflict rs i j -> rs_conflict (r::rs) (S i) (S j).
Proof.
intros r rs i j [H1 [H2 H3]]; red.
exists (lt_n_S _ _ H1).
exists (lt_n_S _ _ H2).
simpl.
rewrite Nth_proof_independent with (H2:=H1).
rewrite Nth_proof_independent with (H2:=H2).
exact H3.
Qed.

Lemma conflicts_aux_le:
  forall (rs:rule_set)(i j n:nat),
    In (i,j) (conflicts_aux n rs) -> (n<=i)%nat /\ (n<=j)%nat.
Proof.
intro rs; elim rs; simpl.
intros i j n H; elim H.
clear rs; intros r rs IH i j n H.
case in_app_or with (1:=H); clear H; intro H.
split.
generalize (rrs_conflicts_soundness _ _ _ _ _ _ H); intros [Hi _].
rewrite Hi; apply le_n.
apply lt_le_weak.
apply rrs_conflicts_n_le_j with (1:=H).

generalize (IH _ _ _ H); intros [H1 H2].
split; apply lt_le_weak; assumption.
Qed.

Lemma conflicts_aux_soundness:
  forall (rs:rule_set)(n i j:nat),
    In (i,j) (conflicts_aux n rs) -> rs_conflict rs (i-n)%nat (j-n)%nat.
Proof.
intros rs; elim rs; simpl.
intros n i j H; elim H.
intros r rs' IH n i j H.
case in_app_or with (1:=H); clear H; intro H.
generalize (rrs_conflicts_soundness i n r rs' j (S n) H); intros [Hi HH].
rewrite <- Hi; rewrite <- minus_n_n.
apply rrs_conflict_rel_rs_conflict.
apply lt_0_lt_minus.
red.
apply rrs_conflicts_n_le_j with (1:=H).
rewrite <- minus_S_pred.
exact HH.
generalize (conflicts_aux_le _ _ _ _ H); intros [H1 H2].
rewrite (S_pred (i-n) 0).
rewrite (S_pred (j-n) 0).
apply rs_conflict_cons.
rewrite <- (minus_S_pred i n); rewrite <- (minus_S_pred j n).
apply IH; exact H.
apply lt_0_lt_minus; exact H2.
apply lt_0_lt_minus; exact H1.
Qed.

Theorem conflicts_soundness:
  forall (rs:rule_set)(i j:nat),
    In (i,j) (find_conflicts rs) -> rs_conflict rs i j.
Proof.
intros rs i j H.
rewrite (minus_n_O i); rewrite (minus_n_O j).
apply conflicts_aux_soundness.
exact H.
Qed.


(* Completeness *)

(* intersection_ip_range is defined in bytes_masks.v *)

Lemma intersection_pn_range:
  forall (pn1 pn2:pn_interval)(pn:port_number),
     pn_match pn pn1 -> pn_match pn pn2 -> (pn_bool pn1 pn2)=true.
Proof.
intros [pn11 pn12] [pn21 pn22] pn; simpl; intros [H11 H12] [H21 H22].
apply andb_true_intro.
split; apply andb_true_intro; split;
  apply Zle_imp_le_bool; apply Zle_trans with pn; assumption.
Qed.

Lemma conflict_check_completeness:
  forall r1 r2: access_rule,
     rule_conflict r1 r2 -> conflict_check r1 r2 = true.
Proof.
intros [a1 p1 sip1 spn1 dip1 dpn1] [a2 p2 sip2 spn2 dip2 dpn2].
intros [[p sip spn dip dpn] H].
case H; clear H;
  intros [[H11 [H12 [H13 [H14 [H15 H16]]]]] [H21 [H22 [H23 [H24 [H25 H26]]]]]];
  simpl in H11; simpl in H21; rewrite H11; rewrite H21; simpl;
  simpl in H12; simpl in H22; rewrite <- H12; rewrite <- H22;
  rewrite protocol_bool_id; simpl.

apply andb_true_intro; split.
simpl in H13; simpl in H23.
apply intersection_ip_range with sip; assumption.
apply andb_true_intro; split.
simpl in H14; simpl in H24.
apply intersection_pn_range with spn; assumption.
apply andb_true_intro; split.
simpl in H15; simpl in H25.
apply intersection_ip_range with dip; assumption.
simpl in H16; simpl in H26.
apply intersection_pn_range with dpn; assumption.

apply andb_true_intro; split.
simpl in H13; simpl in H23.
apply intersection_ip_range with sip; assumption.
apply andb_true_intro; split.
simpl in H14; simpl in H24.
apply intersection_pn_range with spn; assumption.
apply andb_true_intro; split.
simpl in H15; simpl in H25.
apply intersection_ip_range with dip; assumption.
simpl in H16; simpl in H26.
apply intersection_pn_range with dpn; assumption.
Qed.

Lemma Nth_singleton:
  forall (A:Set)(a:A)(i:nat)(hi:(i<1)%nat),
    Nth (a::nil) i hi = a.
Proof.
intros A a i; case i; simpl.
trivial.
intros i' hi'.
red in hi'.
elim (le_Sn_O i').
apply le_S_n; exact hi'.
Qed.

Lemma rule_permit_no_deny:
  forall (rl:access_rule)(r:request),
    rule_permit rl r -> rule_deny rl r -> False.
Proof.
intros rl r [H1 _] [H2 _].
rewrite H1 in H2.
discriminate H2.
Qed.

Lemma no_rule_conflict_self:
  forall r:access_rule, ~ (rule_conflict r r).
Proof.
intros r [q H]; case H; intros [H1 H2];
apply rule_permit_no_deny with r q; assumption.
Qed.

Lemma rs_conflict_singleton:
  forall (r:access_rule)(i j:nat),
    ~ (rs_conflict (r::nil) 0 j).
Proof.
intros r i j [h1 [h2 H]].
rewrite Nth_singleton in H.
rewrite Nth_singleton in H.
apply no_rule_conflict_self with r; exact H.
Qed.

Lemma rrs_conflicts_S:
  forall (r:access_rule)(rs:rule_set)(n j m:nat),
    In (n, j) (rrs_conflicts n m r rs) ->
    In (n, S j) (rrs_conflicts n (S m) r rs).
Proof.
intros r rs; elim rs; simpl.
trivial.
clear rs; intros r1 rs IH n j m; case (conflict_check r r1).
intro H; case H.
intro Heq.
replace m with (snd (n,m)).
rewrite Heq; simpl.
left; trivial.
trivial.

intro H'.
right.
apply IH.
exact H'.
apply IH.
Qed.

Lemma conflicts_0_Sj_rrs_conflicts:
  forall (n:nat)(r:access_rule)(rs:rule_set)(j:nat),
  rs_conflict (r::rs) 0 (S j) ->
  In (n,j+(S n))%nat (rrs_conflicts n (S n) r rs).
Proof.
intros n r rs j; generalize rs; clear rs; elim j.
intro rs; case rs.
intro H; elim (rs_conflict_singleton r 0 1 H).
clear rs; intros r1 rs.
intros [h1 [h2 H]].
simpl in H.
simpl.
rewrite conflict_check_completeness.
simpl.
left; trivial.
exact H.

clear j; intros j IH.
intro rs; case rs.
intro H; elim (rs_conflict_singleton r 0 (S (S j)) H).
clear rs; intros r1 rs H.
simpl.
cut (In (n, S (j+S n)) (rrs_conflicts n (S (S n)) r rs)).
intro HH.
case (conflict_check r r1).
right.
exact HH.
exact HH.
apply rrs_conflicts_S.
apply IH.

case H; clear H; intros h1 [h2 H].
simpl in h1; simpl in h2; simpl in H.

exists (lt_O_Sn (length rs)).
esplit.
simpl.
apply H.
Qed.

Lemma conflicts_0_rrs_conflicts:
  forall (n:nat)(r:access_rule)(rs:rule_set)(j:nat),
  (0<j)%nat ->
  rs_conflict (r::rs) 0 j ->
  In (n,j+n)%nat (rrs_conflicts n (S n) r rs).
Proof.
intros n r rs j Hj; rewrite S_pred with (m:=0%nat)(1:=Hj).
intro H.
rewrite plus_Sn_m; rewrite plus_n_Sm.
apply conflicts_0_Sj_rrs_conflicts.
exact H.
Qed.

Lemma rs_conflict_S:
  forall (r:access_rule)(rs:rule_set)(i j:nat), 
    rs_conflict (r::rs) (S i) (S j) -> rs_conflict rs i j.
Proof.
intros r rs i j [Hi [Hj H]].
simpl in Hi; simpl in Hj; simpl in H.
esplit.
esplit.
apply H.
Qed.

Lemma conflicts_aux_completeness:
  forall (i j:nat), (i<j)%nat ->
  forall (n:nat)(rs:rule_set),
    rs_conflict rs i j -> In (i+n,j+n)%nat (conflicts_aux n rs).
Proof.
intro i; elim i.
intros j h n rs; case rs.
intros [Hi H].
elim lt_n_O with O.
exact Hi.

clear rs; intros r rs H; simpl.
apply in_or_app.
left.
apply conflicts_0_rrs_conflicts.
exact h.
exact H.

clear i; intros i IH j h.
rewrite (S_pred j (S i) h).
intros n rs; case rs.
intros [Hi H].
elim lt_n_O with (S i).
exact Hi.

clear rs; intros r rs Hj; simpl.
apply in_or_app; right.
rewrite plus_n_Sm with i n.
rewrite plus_n_Sm with (pred j) n.
apply IH with (j:=pred j)(n:=S n).
apply lt_pred.
exact h.
apply rs_conflict_S with r.
exact Hj.
Qed.

Theorem conflicts_completeness:
  forall (rs:rule_set)(i j:nat), (i<j)%nat -> 
    rs_conflict rs i j -> In (i,j) (find_conflicts rs).
Proof.
intros rs i j Hlt H; unfold find_conflicts; simpl.
rewrite <- plus_0_r with (n:=i); rewrite <- plus_0_r with (n:=j). 
apply conflicts_aux_completeness.
exact Hlt.
exact H.
Qed.




Unset Extraction Optimize.

Extraction "find_conflicts.ml" find_conflicts.