Remove unused files

ExtraRelations.v

-(******************************************************************************)
-(* c11comp: Coq development attached to the paper                             *)
-(*                                                                            *)
-(*  Vafeiadis, Balabonski, Chakraborty, Morisset, and Zappa Nardelli.         *)
-(*  Common compiler optimisations are invalid in the C11 memory model         *)
-(*  and what we can do about it.                                              *)
-(*  In POPL 2015.                                                             *)
-(*                                                                            *)
-(* Copyright (c) MPI-SWS and INRIA                                            *)
-(* Released under a BSD-style license. See README.txt for details.            *)
-(******************************************************************************)
-
-(******************************************************************************)
-(** * Basic properties of relations *)
-(******************************************************************************)
-
-Require Import Vbase List Relations Classical. 
-Set Implicit Arguments.
-
-(** Definitions of relations *)
-(******************************************************************************)
-
-Definition immediate X (rel : relation X) (a b: X) :=
-  rel a b /\ (forall c (R1: rel a c) (R2: rel c b), False).
-
-Definition irreflexive X (rel : relation X) := forall x, rel x x -> False.
-
-Definition asymmetric X (rel : relation X) := forall x y, rel x y /\ rel y x -> False.
-
-Definition acyclic X (rel : relation X) := irreflexive (clos_trans X rel).
-
-Definition is_total X (cond: X -> Prop) (rel: relation X) :=
-  forall a (IWa: cond a)
-         b (IWb: cond b) (NEQ: a <> b),
-    rel a b \/ rel b a.
-
-Definition restr_subset X (cond: X -> Prop) (rel rel': relation X) :=
-  forall a (IWa: cond a)
-         b (IWb: cond b) (REL: rel a b),
-    rel' a b.
-
-Definition restr_rel X (cond : X -> Prop) (rel : relation X) : relation X :=
-  fun a b => rel a b /\ cond a /\ cond b.
-
-Definition restr_eq_rel A B (f : A -> B) rel x y :=
-  rel x y /\ f x = f y.
-
-Definition upward_closed (X: Type) (rel: relation X) (P: X -> Prop) :=
-  forall x y (REL: rel x y) (POST: P y), P x.
-
-Definition max_elt (X: Type) (rel: relation X) (a: X) :=
-  forall b (REL: rel a b), False.
-
-Notation "r 'UNION1' ( a , b )" := 
-  (fun x y => x = a /\ y = b \/ r x y) (at level 100). 
-
-Notation "a <--> b" := (same_relation _ a b)  (at level 110).
-
-
-(** Very basic properties of relations *)
-(******************************************************************************)
-
-
-Lemma clos_trans_mon A (r r' : relation A) a b :
-  clos_trans A r a b ->
-  (forall a b, r a b -> r' a b) ->
-  clos_trans A r' a b.
-Proof.
-  induction 1; ins; eauto using clos_trans.
-Qed.
-
-Lemma clos_refl_trans_mon A (r r' : relation A) a b :
-  clos_refl_trans A r a b ->
-  (forall a b, r a b -> r' a b) ->
-  clos_refl_trans A r' a b.
-Proof.
-  induction 1; ins; eauto using clos_refl_trans.
-Qed.
-
-
-Lemma clos_refl_transE A r a b :
-  clos_refl_trans A r a b <-> a = b \/ clos_trans A r a b.
-Proof.
-  split; ins; desf; vauto; induction H; desf; vauto. 
-Qed.
-
-Lemma clos_trans_in_rt A r a b :
-  clos_trans A r a b -> clos_refl_trans A r a b.
-Proof.
-  induction 1; vauto. 
-Qed.
-
-Lemma rt_t_trans A r a b c :
-  clos_refl_trans A r a b -> clos_trans A r b c -> clos_trans A r a c.
-Proof.
-  ins; induction H; eauto using clos_trans. 
-Qed.
-
-Lemma t_rt_trans A r a b c :
-  clos_trans A r a b -> clos_refl_trans A r b c -> clos_trans A r a c.
-Proof.
-  ins; induction H0; eauto using clos_trans. 
-Qed.
-
-
-Lemma t_step_rt A R x y : 
-  clos_trans A R x y <-> exists z, R x z /\ clos_refl_trans A R z y.
-Proof.
-  split; ins; desf.
-    by apply clos_trans_tn1 in H; induction H; desf; eauto using clos_refl_trans.
-  by rewrite clos_refl_transE in *; desf; eauto using clos_trans.
-Qed.
-
-Lemma t_rt_step A R x y : 
-  clos_trans A R x y <-> exists z, clos_refl_trans A R x z /\ R z y.
-Proof.
-  split; ins; desf.
-    by apply clos_trans_t1n in H; induction H; desf; eauto using clos_refl_trans.
-  by rewrite clos_refl_transE in *; desf; eauto using clos_trans.
-Qed.
-
-Lemma clos_trans_of_transitive A R (T: transitive A R) x y : 
-  clos_trans A R x y -> R x y.
-Proof.
-  induction 1; eauto.
-Qed.
-
-Lemma clos_trans_eq :
-  forall X (rel: relation X) Y (f : X -> Y) 
-         (H: forall a b (SB: rel a b), f a = f b) a b
-         (C: clos_trans _ rel a b),
-    f a = f b.
-Proof.
-  ins; induction C; eauto; congruence.
-Qed.
-
-Lemma trans_irr_acyclic : 
-  forall A R, irreflexive R -> transitive A R -> acyclic R.
-Proof.
-  eby repeat red; ins; eapply H, clos_trans_of_transitive. 
-Qed.
-
-Lemma restr_rel_trans :
-  forall X dom rel, transitive X rel -> transitive X (restr_rel dom rel).
-Proof.
-  unfold restr_rel; red; ins; desf; eauto.
-Qed.
-
-Lemma clos_trans_of_clos_trans1 :
-  forall X rel1 rel2 x y,
-    clos_trans X (fun a b => clos_trans _ rel1 a b \/ rel2 a b) x y <->
-    clos_trans X (fun a b => rel1 a b \/ rel2 a b) x y.
-Proof.
-  split; induction 1; desf; 
-  eauto using clos_trans, clos_trans_mon.
-Qed.
-
-Lemma upward_clos_trans:
-  forall X (rel: X -> X -> Prop) P,
-    upward_closed rel P -> upward_closed (clos_trans _ rel) P.
-Proof.
-  ins; induction 1; by eauto.
-Qed.
-
-Lemma max_elt_clos_trans:
-  forall X rel a b
-         (hmax: max_elt rel a)
-         (hclos: clos_trans X rel a b),
-    False.
-Proof.
-  ins. eapply clos_trans_t1n in hclos. induction hclos; eauto.
-Qed.
-
-Lemma is_total_restr :
-  forall X (dom : X -> Prop) rel,
-    is_total dom rel ->
-    is_total dom (restr_rel dom rel).
-Proof.
-  red; ins; eapply H in NEQ; eauto; desf; vauto.
-Qed.
-
-Lemma clos_trans_restrD :
-  forall X rel f x y, clos_trans X (restr_rel f rel) x y -> f x /\ f y.
-Proof.
-  unfold restr_rel; induction 1; ins; desf. 
-Qed.
-
-Lemma clos_trans_restr_eqD :
-  forall A rel B (f: A -> B) x y, clos_trans _ (restr_eq_rel f rel) x y -> f x = f y.
-Proof.
-  unfold restr_eq_rel; induction 1; ins; desf; congruence. 
-Qed.
-
-Lemma irreflexive_inclusion:
-  forall X (R1 R2: relation X),
-  inclusion X R1 R2 ->
-  irreflexive R2 ->
-  irreflexive R1.
-Proof.
-  unfold irreflexive, inclusion.
-  by eauto.
-Qed.
-
-Lemma clos_trans_inclusion:
-  forall X (R: relation X),
-  inclusion X R (clos_trans X R).
-Proof.
-  unfold inclusion. intros.
-  by econstructor; eauto.
-Qed.
-
-Lemma clos_trans_inclusion_clos_refl_trans:
-  forall X (R: relation X),
-  inclusion X (clos_trans X R) (clos_refl_trans X R).
-Proof.
-  unfold inclusion. intros.
-  induction H.
-    by eauto using rt_step.
-    by eauto using rt_trans.
-Qed.
-
-Lemma clos_trans_monotonic:
-  forall X (R1 R2: relation X),
-  inclusion X R1 R2 ->
-  inclusion X (clos_trans X R1) (clos_trans X R2).
-Proof.
-  intros.
-  intros x y hR1.
-  eapply clos_t1n_trans.
-  eapply clos_trans_t1n in hR1.
-  induction hR1.
-    by eauto using clos_t1n_trans, t1n_step.
-    (* [t1n_trans] is masked by a notation for [clos_t1n_trans] *)
-    by eauto using clos_t1n_trans, Relation_Operators.t1n_trans.
-Qed.
-
-(******************************************************************************)
-(** Set up setoid rewriting *)
-(******************************************************************************)
-
-Require Import Setoid.
-
-Lemma same_relation_refl: forall A, reflexive _ (same_relation A).
-Proof. split; ins. Qed.
-
-Lemma same_relation_sym: forall A, symmetric _ (same_relation A).
-Proof. unfold same_relation; split; ins; desf. Qed.
-
-Lemma same_relation_trans: forall A, transitive _ (same_relation A).
-Proof. unfold same_relation; split; ins; desf; red; eauto. Qed.
-
-Add Parametric Relation (X : Type) : (relation X) (same_relation X) 
- reflexivity proved by (@same_relation_refl X)
- symmetry proved by (@same_relation_sym X)
- transitivity proved by (@same_relation_trans X)
- as same_rel.
-
-Add Parametric Morphism X : (@union X) with 
-  signature (@same_relation X) ==> (@same_relation X) ==> (@same_relation X) as union_mor.
-Proof.
-  unfold same_relation, union; ins; desf; split; red; ins; desf; eauto.
-Qed.
-
-Add Parametric Morphism X P : (@restr_rel X P) with 
-  signature (@same_relation X) ==> (@same_relation X) as restr_rel_mor.
-Proof.
-  unfold same_relation, restr_rel; ins; desf; split; red; ins; desf; eauto.
-Qed.
-
-Add Parametric Morphism X : (@clos_trans X) with 
-  signature (@same_relation X) ==> (@same_relation X) as clos_trans_mor.
-Proof.
-  unfold same_relation; ins; desf; split; red; ins; desf; eauto using clos_trans_mon.
-Qed.
-
-Add Parametric Morphism X : (@clos_refl_trans X) with 
-  signature (@same_relation X) ==> (@same_relation X) as clos_relf_trans_mor.
-Proof.
-  unfold same_relation; ins; desf; split; red; ins; desf; eauto using clos_refl_trans_mon.
-Qed.
-
-Add Parametric Morphism X : (@irreflexive X) with 
-  signature (@same_relation X) ==> iff as irreflexive_mor.
-Proof.
-  unfold same_relation; ins; desf; split; red; ins; desf; eauto using clos_refl_trans_mon.
-Qed.
-
-Add Parametric Morphism X : (@acyclic X) with 
-  signature (@same_relation X) ==> iff as acyclic_mor.
-Proof.
-  unfold acyclic; ins; rewrite H; reflexivity.
-Qed.
-
-
-Lemma same_relation_restr X (f : X -> Prop) rel rel' :
-   (forall x (CONDx: f x) y (CONDy: f y), rel x y <-> rel' x y) ->
-   (restr_rel f rel <--> restr_rel f rel').
-Proof.
-  unfold restr_rel; split; red; ins; desf; rewrite H in *; eauto.
-Qed.
-
-Lemma union_restr X f rel rel' :
-  union X (restr_rel f rel) (restr_rel f rel')
-  <--> restr_rel f (union _ rel rel').
-Proof.
-  split; unfold union, restr_rel, inclusion; ins; desf; eauto.
-Qed.
-
-Lemma clos_trans_restr X f rel (UC: upward_closed rel f) :
-  clos_trans X (restr_rel f rel) 
-  <--> restr_rel f (clos_trans _ rel).
-Proof.
-  split; unfold union, restr_rel, inclusion; ins; desf; eauto.
-    split; [|by apply clos_trans_restrD in H].
-    by eapply clos_trans_mon; eauto; unfold restr_rel; ins; desf.
-  clear H0; apply clos_trans_tn1 in H.
-  induction H; eauto 10 using clos_trans.
-Qed.
-
-
-(******************************************************************************)
-(** ** Lemmas about cycles *)
-(******************************************************************************)
-
-Lemma path_decomp_u1 X (rel : relation X) a b c d : 
-  clos_trans X (rel UNION1 (a, b)) c d ->
-  clos_trans X rel c d \/ 
-  clos_refl_trans X rel c a /\ clos_refl_trans X rel b d.
-Proof.
-  induction 1; desf; eauto using clos_trans, clos_refl_trans, clos_trans_in_rt.
-Qed.
-
-Lemma cycle_decomp_u1 X (rel : relation X) a b c : 
-  clos_trans X (rel UNION1 (a, b)) c c ->
-  clos_trans X rel c c \/ clos_refl_trans X rel b a.
-Proof.
-  ins; apply path_decomp_u1 in H; desf; eauto using clos_refl_trans.
-Qed.
-
-Lemma path_decomp_u_total :
-  forall X rel1 dom rel2 (T: is_total dom rel2) 
-    (D: forall a b (REL: rel2 a b), dom a /\ dom b) x y
-    (C: clos_trans X (fun a b => rel1 a b \/ rel2 a b) x y),
-    clos_trans X rel1 x y \/
-    (exists m n, 
-      clos_refl_trans X rel1 x m /\ clos_trans X rel2 m n /\ clos_refl_trans X rel1 n y) \/
-    (exists m n, 
-      clos_refl_trans X rel1 m n /\ clos_trans X rel2 n m).
-Proof.
-  ins; induction C; desf; eauto 8 using rt_refl, clos_trans.
-  by right; left; exists m, n; eauto using clos_trans_in_rt, rt_trans.
-  by right; left; exists m, n; eauto using clos_trans_in_rt, rt_trans.
-
-  destruct (classic (m = n0)) as [|NEQ]; desf.
-  by right; left; exists m0, n; eauto using t_trans, rt_trans.
-  eapply T in NEQ; desf.
-    by right; right; exists n0, m; eauto 8 using clos_trans, rt_trans.
-    by right; left; exists m0, n; eauto 8 using clos_trans, rt_trans.
-    by apply t_step_rt in IHC0; desf; eapply D in IHC0; desf.
-    by apply t_rt_step in IHC4; desf; eapply D in IHC6; desf.
-Qed.
-
-Lemma cycle_decomp_u_total :
-  forall X rel1 dom rel2 (T: is_total dom rel2) 
-    (D: forall a b (REL: rel2 a b), dom a /\ dom b) x
-    (C: clos_trans X (fun a b => rel1 a b \/ rel2 a b) x x),
-    clos_trans X rel1 x x \/
-    (exists m n, clos_refl_trans X rel1 m n /\ clos_trans X rel2 n m).
-Proof.
-  ins; exploit path_decomp_u_total; eauto; ins; desf; eauto 8 using rt_trans.
-Qed.
-
-Lemma clos_trans_disj_rel :
-  forall X (rel rel' : relation X)
-    (DISJ: forall x y (R: rel x y) z (R': rel' y z), False) x y
-    (R: clos_trans _ rel x y) z
-    (R': clos_trans _ rel' y z),
-    False.
-Proof.
-  ins; induction R; eauto; induction R'; eauto.
-Qed.
-
-Lemma path_decomp_u_1 :
-  forall X (rel rel' : relation X)
-    (DISJ: forall x y (R: rel x y) z (R': rel' y z), False) x y
-    (T: clos_trans X (union X rel rel') x y),
-    clos_trans _ rel x y \/ clos_trans _ rel' x y
-    \/ exists z, clos_trans _ rel' x z /\ clos_trans _ rel z y.
-Proof.
-  unfold union; ins.
- induction T; desf; eauto 6 using clos_trans;
-   try by exfalso; eauto using clos_trans_disj_rel.
-Qed.
-
-Lemma cycle_decomp_u_1 :
-  forall X (rel rel' : relation X)
-    (DISJ: forall x y (R: rel x y) z (R': rel' y z), False) x
-    (T: clos_trans X (union X rel rel') x x),
-    clos_trans _ rel x x \/ clos_trans _ rel' x x. 
-Proof.
-  ins; exploit path_decomp_u_1; eauto; ins; desf; eauto.
-  exfalso; eauto using clos_trans_disj_rel.
-Qed.
-
-Lemma cycle_disj :
-  forall X (rel : relation X)
-    (DISJ: forall x y (R: rel x y) z (R': rel y z), False) x
-    (T: clos_trans X rel x x), False.
-Proof.
-  ins; inv T; eauto using clos_trans_disj_rel.
-Qed.
-
-Lemma clos_trans_restr_trans_mid : 
-  forall X (rel rel' : relation X) f x y
-    (A : clos_trans _ (restr_rel f (fun x y => rel x y \/ rel' x y)) x y)
-    z (B : rel y z) w
-    (C : clos_trans _ (restr_rel f (fun x y => rel x y \/ rel' x y)) z w),
-    clos_trans _ (restr_rel f (fun x y => rel x y \/ rel' x y)) x w.
-Proof.
-  ins; eapply t_trans, t_trans; vauto.
-  eapply t_step; repeat split; eauto.
-    by apply clos_trans_restrD in A; desc.
-  by apply clos_trans_restrD in C; desc.
-Qed.
-
-Lemma clos_trans_restr_trans_cycle : 
-  forall X (rel rel' : relation X) f x y
-    (A : clos_trans _ (restr_rel f (fun x y => rel x y \/ rel' x y)) x y)
-    (B : rel y x),
-    clos_trans _ (restr_rel f (fun x y => rel x y \/ rel' x y)) x x.
-Proof.
-  ins; eapply t_trans, t_step; eauto. 
-  by red; apply clos_trans_restrD in A; desf; auto.
-Qed.
-
-
-Lemma restr_eq_union : 
-  forall X (rel rel' : relation X) B (f: X -> B) x y
-         (R: forall x y, rel' x y -> f x = f y),
-   restr_eq_rel f (fun x y => rel x y \/ rel' x y) x y <->
-   restr_eq_rel f rel x y \/ rel' x y.
-Proof.
-  unfold restr_eq_rel; ins; intuition.
-Qed.
-
-Lemma clos_trans_restr_eq_union : 
-  forall X (rel rel' : relation X) B (f: X -> B)
-         (R: forall x y, rel' x y -> f x = f y),
-   clos_trans _ (restr_eq_rel f (fun x y => rel x y \/ rel' x y)) <-->
-   clos_trans _ (fun x y => restr_eq_rel f rel x y \/ rel' x y).
-Proof.
-  split; red; ins; eapply clos_trans_mon; eauto; ins; instantiate;
-  rewrite restr_eq_union in *; eauto.
-Qed.
-
-Lemma acyclic_mon X (rel rel' : relation X) :
-  acyclic rel -> inclusion _ rel' rel -> acyclic rel'.
-Proof.
-  eby repeat red; ins; eapply H, clos_trans_mon.
-Qed. 
-
-(** Extension of a partial order to a total order *)
-
-Section one_extension.
-
-  Variable X : Type.
-  Variable elem : X.
-  Variable rel : relation X.
-
-  Definition one_ext : relation X := 
-    fun x y =>
-      clos_trans _ rel x y 
-      \/ clos_refl_trans _ rel x elem /\ ~ clos_refl_trans _ rel y elem.
-
-  Lemma one_ext_extends x y : rel x y -> one_ext x y. 
-  Proof. vauto. Qed.
-
-  Lemma one_ext_trans : transitive _ one_ext.
-  Proof. 
-    red; ins; unfold one_ext in *; desf; desf; 
-      intuition eauto using clos_trans_in_rt, t_trans, rt_trans.
-  Qed.
- 
-  Lemma one_ext_irr : acyclic rel -> irreflexive one_ext.
-  Proof.
-    red; ins; unfold one_ext in *; desf; eauto using clos_trans_in_rt.
-  Qed.
-
-  Lemma one_ext_total_elem : 
-    forall x, x <> elem -> one_ext elem x \/ one_ext x elem.
-  Proof.
-    unfold one_ext; ins; rewrite !clos_refl_transE; tauto.
-  Qed.
-
-End one_extension.
-
-Fixpoint tot_ext X (dom : list X) (rel : relation X) : relation X :=
-  match dom with 
-    | nil => clos_trans _ rel
-    | x::l => one_ext x (tot_ext l rel) 
-  end.
-
-Lemma tot_ext_extends : 
-  forall X dom (rel : relation X) x y, rel x y -> tot_ext dom rel x y. 
-Proof. 
-  induction dom; ins; eauto using t_step, one_ext_extends.
-Qed.
-
-Lemma tot_ext_trans : forall X dom rel, transitive X (tot_ext dom rel).
-Proof. 
-  induction dom; ins; vauto; apply one_ext_trans. 
-Qed.
-
-Lemma tot_ext_irr : 
-  forall X (dom : list X) rel, acyclic rel -> irreflexive (tot_ext dom rel).
-Proof.
-  induction dom; ins.
-  apply one_ext_irr, trans_irr_acyclic; eauto using tot_ext_trans.
-Qed.
-
-(*Lemma tot_ext_total : 
-  forall X (dom : list X) rel, is_total (fun x => In x dom) (tot_ext dom rel).
-Proof.
-  induction dom; red; ins; desf.
-  eapply one_ext_total_elem in NEQ; desf; eauto.
-  eapply nesym, one_ext_total_elem in NEQ; desf; eauto.
-  eapply IHdom in NEQ; desf; eauto using one_ext_extends.
-Qed.*)
-
-Lemma tot_ext_inv :
-  forall X dom rel (x y : X),
-    acyclic rel -> tot_ext dom rel x y -> ~ rel y x.
-Proof.
-  red; ins; eapply tot_ext_irr, tot_ext_trans, tot_ext_extends; eauto.
-Qed.
-
-
-(** Misc properties *)
-(******************************************************************************)
-
-
-Lemma clos_trans_imm :
-  forall X (R : relation X) (I: irreflexive R) 
-         (T: transitive _ R) L (ND: NoDup L) a b
-         (D: forall c, R a c -> R c b -> In c L)
-         (REL: R a b),
-    clos_trans _ (immediate R) a b.
-Proof.
-  intros until 3; induction ND; ins; vauto.
-  destruct (classic (R a x /\ R x b)) as [|N]; desf;
-    [apply t_trans with x|]; eapply IHND; ins;
-    exploit (D c); eauto; intro; desf; exfalso; eauto.
-Qed.
-
-
-(** Remove duplicate list elements (classical) *)
-(******************************************************************************)
-
-Require Import extralib.
-
-Fixpoint undup A dec (l: list A) :=
-  match l with nil => nil
-    | x :: l =>
-      if In_dec dec x l then undup dec l else x :: undup dec l
-  end.
-
-Lemma In_undup X dec (x: X) l : In x (undup dec l) <-> In x l.
-Proof.
-  induction l; ins; des_if; ins; rewrite IHl; split; ins; desf; vauto.
-Qed.
-
-Lemma NoDup_undup X dec (l : list X) : NoDup (undup dec l).
-Proof.
-  induction l; ins; desf; constructor; eauto; rewrite In_undup; eauto. 
-Qed.
-
-
-Lemma clos_trans_imm2 :
-  forall X (dec : forall x y : X, {x = y} + {x <> y}) 
-         (R : relation X) (I: irreflexive R) 
-         (T: transitive _ R) L a b
-         (D: forall c, R a c -> R c b -> In c L)
-         (REL: R a b),
-    clos_trans _ (immediate R) a b.
-Proof.
-  ins; eapply clos_trans_imm with (L := undup dec L); ins;
-  try rewrite In_undup; eauto using NoDup_undup.
-Qed.
-
-
-
-
-Lemma total_immediate_unique:
-  forall X (eq_X_dec: forall (x y: X), {x=y} + {x<>y}) (rel: X -> X -> Prop) (P: X -> Prop)
-         (Tot: is_total P rel)
-         a b c (pa: P a) (pb: P b) (pc: P c)
-         (iac: immediate rel a c)
-         (ibc: immediate rel b c),
-    a = b.
-Proof.
-  ins.
-  destruct (eq_X_dec a b); eauto.
-  exfalso.
-  unfold immediate in *; desf.
-  eapply Tot in n; eauto.
-  desf; eauto.
-Qed.
-

coqdoc.css

-body { padding: 0px 0px;
-       margin: 0px 0px; 
-       background-color: white }
-
-#page { display: block;
-        padding: 0px;
-        margin: 0px;
-        padding-bottom: 10px; }
-
-#header { display: block;
-          position: relative;
-          padding: 0;
-          margin: 0;
-          vertical-align: middle;
-          border-bottom-style: solid;
-          border-width: thin }
-
-#header h1 { padding: 0; 
-             margin: 0;}
-
-
-/* Contents */
-
-#main{ display: block;
-       padding: 10px;
-       font-family: sans-serif;
-       font-size: 100%;
-       line-height: 100% }
-
-#main  h1 { line-height: 95% } /* allow for multi-line headers */
-
-#main  a.idref:visited {color : #416DFF; text-decoration : none; }
-#main  a.idref:link {color : #416DFF; text-decoration : none; }
-#main  a.idref:hover {text-decoration : none; }
-#main  a.idref:active {text-decoration : none; }
-
-#main  a.modref:visited {color : #416DFF; text-decoration : none; }
-#main  a.modref:link {color : #416DFF; text-decoration : none; }
-#main  a.modref:hover {text-decoration : none; }
-#main  a.modref:active {text-decoration : none; }
-
-#main .keyword { color : #cf1d1d }
-#main { color: black }
-
-.section { background-color: rgb(60%,60%,100%);
-           padding-top: 13px; 
-           padding-bottom: 13px; 
-           padding-left: 3px; 
-           margin-top: 5px;
-           margin-bottom: 5px;
-           font-size : 175% }
-
-h2.section { background-color: rgb(80%,80%,100%);
-             padding-left: 3px; 
-             padding-top: 12px; 
-             padding-bottom: 10px; 
-             font-size : 130% }
-
-h3.section { background-color: rgb(90%,90%,100%);
-             padding-left: 3px; 
-             padding-top: 7px; 
-             padding-bottom: 7px; 
-             font-size : 115% }
-
-h4.section { 
-/*
-                   background-color: rgb(80%,80%,80%);
-                   max-width: 20em;
-                   padding-left: 5px; 
-                   padding-top: 5px; 
-                   padding-bottom: 5px; 
-*/
-                   background-color: white;
-                   padding-left: 0px; 
-                   padding-top: 0px; 
-                   padding-bottom: 0px; 
-                   font-size : 100%;
-                   font-style : bold;
-                   text-decoration : underline;
- }
-
-#main .doc { margin: 0px;
-             font-family: sans-serif;
-             font-size: 100%;
-	     line-height: 125%;
-             max-width: 40em;
-             color: black;
-	     padding: 10px;
-             background-color: #90bdff;
-             border-style: plain}
-
-.inlinecode { 
-    display: inline;
-/*    font-size: 125%; */
-    color: #666666;
-    font-family: monospace } 
-
-.doc .inlinecode { 
-    display: inline;
-    font-size: 120%; 
-    color: rgb(30%,30%,70%);
-    font-family: monospace } 
-
-.doc .inlinecode .id { 
-    color: rgb(30%,30%,70%); 
-} 
-
-.inlinecodenm { 
-    display: inline;
-    color: #444444;
-}
-
-.doc .code { 
-    display: inline;
-    font-size: 120%; 
-    color: rgb(30%,30%,70%); 
-    font-family: monospace } 
-
-.comment { 
-    display: inline;
-    font-family: monospace;
-    color: rgb(50%,50%,80%); 
-} 
-
-.code { 
-    display: block;
-/*  padding-left: 15px; */
-    font-size: 110%; 
-    font-family: monospace;
- } 
-
-table.infrule {
-  border: 0px;
-  margin-left: 50px;
-  margin-top: 10px;
-  margin-bottom: 10px;
-}
-
-td.infrule {
-    font-family: monospace;
-    text-align: center;
-/*    color: rgb(35%,35%,70%);  */
-    padding: 0px;
-    line-height: 100%;
-}
-
-tr.infrulemiddle hr {
-    margin: 1px 0 1px 0;
-}
-
-.infrulenamecol {
-    color: rgb(60%,60%,60%); 
-    font-size: 80%;
-    padding-left: 1em;
-    padding-bottom: 0.1em
-}
-
-/* Pied de page */
-
-#footer { font-size: 65%;
-          font-family: sans-serif; }
-
-.id { display: inline; }
-
-.id[type="constructor"] { 
-    color: rgb(60%,0%,0%);
-}
-
-.id[type="var"] { 
-    color: rgb(40%,0%,40%);
-}
-
-.id[type="variable"] { 
-    color: rgb(40%,0%,40%);
-}
-
-.id[type="definition"] { 
-    color: rgb(0%,40%,0%);
-}
-
-.id[type="abbreviation"] { 
-    color: rgb(0%,40%,0%);
-}
-
-.id[type="lemma"] { 
-    color: rgb(0%,40%,0%);
-}
-
-.id[type="instance"] { 
-    color: rgb(0%,40%,0%);
-}
-
-.id[type="projection"] { 
-    color: rgb(0%,40%,0%);
-}
-
-.id[type="method"] { 
-    color: rgb(0%,40%,0%);
-}
-
-.id[type="inductive"] { 
-    color: rgb(0%,0%,80%);
-}
-
-.id[type="record"] { 
-    color: rgb(0%,0%,80%);
-}
-
-.id[type="class"] { 
-    color: rgb(0%,0%,80%);
-}
-
-.id[type="keyword"] { 
- color : #cf1d1d;
-/*     color: black; */
-}
-
-.inlinecode .id {
-    color: rgb(0%,0%,0%);
-}
-
-
-/* TOC */
-
-#toc h2 {
-    padding: 10px;
-    background-color: rgb(60%,60%,100%);
-}
-
-#toc li {
-    padding-bottom: 8px;
-}
-
-/* Index */
-
-#index {
-    margin: 0;
-    padding: 0;
-    width: 100%;
-}
-
-#index #frontispiece {
-    margin: 1em auto;
-    padding: 1em;
-    width: 60%;
-}
-
-.booktitle { font-size : 140%  }
-.authors { font-size : 90%;
-	         line-height: 115%;  }
-.moreauthors { font-size : 60%  }
-
-#index #entrance {
-    text-align: center;
-}
-
-#index #entrance .spacer {
-    margin: 0 30px 0 30px;
-}
-
-#index #footer {
-    position: absolute;
-    bottom: 0;
-    text-align: bottom;
-}
-
-.paragraph {
-    height: 0.75em;
-}
-
-ul.doclist {
-    margin-top: 0em;
-    margin-bottom: 0em;
-}

extralib.v

-(******************************************************************************)
-(* c11comp: Coq development attached to the paper                             *)
-(*                                                                            *)
-(*  Vafeiadis, Balabonski, Chakraborty, Morisset, and Zappa Nardelli.         *)
-(*  Common compiler optimisations are invalid in the C11 memory model         *)
-(*  and what we can do about it.                                              *)
-(*  In POPL 2015.                                                             *)
-(*                                                                            *)
-(* Copyright (c) MPI-SWS and INRIA                                            *)
-(* Released under a BSD-style license. See README.txt for details.            *)
-(******************************************************************************)
-
-Require Import List Permutation Vbase Classical.
-Set Implicit Arguments.
-
-Fixpoint flatten A (l: list (list A)) :=
-  match l with 
-    | nil => nil
-    | x :: l' => x ++ flatten l'
-  end.
-
-Definition disjoint A (l1 l2 : list A) := 
-  forall a (IN1: In a l1) (IN2: In a l2), False. 
-
-
-Definition appA := app_assoc_reverse. 
-
-(** Properties of [In] *)
-
-Lemma In_eq : forall A (a:A) (l:list A), In a (a :: l).
-Proof. vauto. Qed.
-
-Lemma In_cons : forall A (a b:A) (l:list A), In b l -> In b (a :: l).
-Proof. vauto. Qed.
-
-
-Lemma In_nil : forall A (a:A), ~ In a nil.
-Proof. by red. Qed.
-
-Lemma In_split : forall A x (l:list A), In x l -> exists l1 l2, l = l1++x::l2.
-Proof.
-  induction l; simpl; intros; des; vauto.
-  - exists nil; vauto.
-  - destruct IHl; des; try done; eexists (_ :: _); vauto.
-Qed.
-
-Lemma In_dec :
-  forall A (D: forall x y:A, {x = y} + {x <> y}) (a: A) l, {In a l} + {~ In a l}.
-Proof.
-  induction l; vauto; simpl; destruct (D a a0); intuition.
-Qed.
-
-Lemma In_appI1 : forall A (x:A) l (IN: In x l) l', In x (l++l').
-Proof. induction l; ins; desf; eauto. Qed.
-
-Lemma In_appI2 : forall A (x:A) l' (IN: In x l') l, In x (l++l').
-Proof. induction l; ins; desf; eauto. Qed.
-
-Lemma In_appD : forall A (x:A) l l' (IN: In x (l++l')), In x l \/ In x l'.
-Proof. induction l; intuition. Qed.
-
-Lemma In_app : forall A (x:A) l l', In x (l++l') <-> In x l \/ In x l'.
-Proof. intuition; auto using In_appI1, In_appI2. Qed.
-
-Lemma In_rev : forall A (x: A) l, In x (rev l) <-> In x l.
-Proof.
-  induction l; ins; rewrite In_app, IHl; ins; tauto.
-Qed.
-
-Lemma In_revI : forall A (x: A) l (IN: In x l), In x (rev l).
-Proof. by intros; apply In_rev. Qed.
-
-Lemma In_revD : forall A (x: A) l (IN: In x (rev l)), In x l.
-Proof. by intros; apply In_rev. Qed.
-
-Lemma In_mapI : forall A B (f: A -> B) x l (IN: In x l), In (f x) (map f l).
-Proof. induction l; ins; intuition vauto. Qed.
-
-Lemma In_mapD :
-  forall A B (f: A->B) y l, In y (map f l) -> exists x, f x = y /\ In x l.
-Proof.
-  induction l; ins; intuition; des; eauto.
-Qed.
-
-Lemma In_map :
-  forall A B (f: A->B) y l, In y (map f l) <-> exists x, f x = y /\ In x l.
-Proof.
-  split; intros; des; clarify; auto using In_mapI, In_mapD.
-Qed.
-
-Lemma In_filter :
-  forall A (x:A) f l,  In x (filter f l) <-> In x l /\ f x.
-Proof. induction l; ins; desf; simpls; intuition; clarify. Qed.
-
-Lemma In_filterI :
-  forall A x l (IN: In x l) (f: A->bool) (F: f x), In x (filter f l).
-Proof. by intros; apply In_filter. Qed.
-
-Lemma In_filterD :
-  forall A (x:A) f l (D: In x (filter f l)), In x l /\ f x.
-Proof. by intros; apply In_filter. Qed.
-
-Lemma In_flatten A (x:A) l : 
-  In x (flatten l) <-> exists y, In x y /\ In y l.
-Proof.
-  induction l; ins; rewrite ?In_app, ?IHl; clear; split; ins; desf; eauto.
-Qed.
-
-Hint Resolve In_eq In_cons In_appI1 In_appI2 In_mapI In_revI In_filterI : vlib.
-
-
-Lemma nodup_one A (x: A) : NoDup (x :: nil).
-Proof. vauto. Qed.
-
-Hint Resolve NoDup_nil nodup_one.
-
-Lemma nodup_map:
-  forall (A B: Type) (f: A -> B) (l: list A),
-  NoDup l ->
-  (forall x y, In x l -> In y l -> x <> y -> f x <> f y) ->
-  NoDup (map f l).
-Proof.
-  induction 1; ins; vauto. 
-  constructor; eauto.
-  intro; rewrite In_map in *; desf.
-  edestruct H1; try eapply H2; eauto.
-  intro; desf.
-Qed.
-
-Lemma nodup_append_commut:
-  forall (A: Type) (a b: list A),
-  NoDup (a ++ b) -> NoDup (b ++ a).
-Proof.
-  intro A.
-  assert (forall (x: A) (b: list A) (a: list A), 
-           NoDup (a ++ b) -> ~(In x a) -> ~(In x b) -> 
-           NoDup (a ++ x :: b)).
-    induction a; simpl; intros.
-    constructor; auto.
-    inversion H. constructor. red; intro.
-    elim (in_app_or _ _ _ H6); intro.
-    elim H4. apply in_or_app. tauto.
-    elim H7; intro. subst a. elim H0. left. auto. 
-    elim H4. apply in_or_app. tauto.
-    auto.
-  induction a; simpl; intros.
-  rewrite <- app_nil_end. auto.
-  inversion H0. apply H. auto. 
-  red; intro; elim H3. apply in_or_app. tauto.
-  red; intro; elim H3. apply in_or_app. tauto.
-Qed.
-
-Lemma nodup_cons A (x: A) l:
-  NoDup (x :: l) <-> ~ In x l /\ NoDup l.
-Proof. split; inversion 1; vauto. Qed.
-
-Lemma nodup_app:
-  forall (A: Type) (l1 l2: list A),
-  NoDup (l1 ++ l2) <->
-  NoDup l1 /\ NoDup l2 /\ disjoint l1 l2.
-Proof.
-  induction l1; ins. 
-    by split; ins; desf; vauto.
-  rewrite !nodup_cons, IHl1, In_app; unfold disjoint.
-  ins; intuition (subst; eauto). 
-Qed.
-
-Lemma nodup_append:
-  forall (A: Type) (l1 l2: list A),
-  NoDup l1 -> NoDup l2 -> disjoint l1 l2 ->
-  NoDup (l1 ++ l2).
-Proof.
-  generalize nodup_app; firstorder.
-Qed.
-
-Lemma nodup_append_right:
-  forall (A: Type) (l1 l2: list A),
-  NoDup (l1 ++ l2) -> NoDup l2.
-Proof.
-  generalize nodup_app; firstorder.
-Qed.
-
-Lemma nodup_append_left:
-  forall (A: Type) (l1 l2: list A),
-  NoDup (l1 ++ l2) -> NoDup l1.
-Proof.
-  generalize nodup_app; firstorder.
-Qed.
-
-Lemma NoDup_filter A (l: list A) (ND: NoDup l) f : NoDup (filter f l). 
-Proof. 
-  induction l; ins; inv ND; desf; eauto using NoDup.
-  econstructor; eauto; rewrite In_filter; tauto.
-Qed.
-
-Hint Resolve NoDup_filter.
-
-Lemma NoDup_eq_one A (x : A) l : 
-   NoDup l -> In x l -> (forall y (IN: In y l), y = x) -> l = x :: nil.
-Proof.
-  destruct l; ins; f_equal; eauto.
-  inv H; desf; clear H H5; induction l; ins; desf; case H4; eauto using eq_sym.
-  rewrite IHl in H0; ins; desf; eauto.
-Qed.
-
-Lemma Permutation_NoDup A ( l l' : list A) : 
-  Permutation l l' -> NoDup l -> NoDup l'.
-Proof.
-  induction 1; eauto; rewrite !nodup_cons in *; ins; desf; intuition. 
-  eby symmetry in H; eapply H0; eapply Permutation_in.
-Qed.
-
-Lemma NoDup_mapD A B (f : A-> B) l :
-  NoDup (map f l) -> NoDup l.
-Proof.
-  induction l; ins; rewrite !nodup_cons, In_map in *; desf; eauto 8.
-Qed.
-
-Lemma perm_from_subset : 
-  forall A (l : list A) l',
-    NoDup l' ->
-    (forall x, In x l' -> In x l) ->
-    exists l'', Permutation l (l' ++ l''). 
-Proof.
-  induction l; ins; vauto.
-    by destruct l'; ins; vauto; exfalso; eauto.
-  destruct (classic (In a l')).
-
-    eapply In_split in H1; desf; rewrite ?nodup_app, ?nodup_cons in *; desf.
-    destruct (IHl (l1 ++ l2)); ins. 
-      by rewrite ?nodup_app, ?nodup_cons in *; desf; repeat split; ins; red; eauto using In_cons.
-      by specialize (H0 x); rewrite In_app in *; ins; desf;
-         destruct (classic (a = x)); subst; try tauto; exfalso; eauto using In_eq.
-    eexists; rewrite appA in *; ins.
-    by eapply Permutation_trans, Permutation_middle; eauto.
-
-  destruct (IHl l'); eauto; ins.
-    by destruct (H0 x); auto; ins; subst.
-  by eexists (a :: _); eapply Permutation_trans, Permutation_middle; eauto.
-Qed.
-

liulayland.tmp

-Require Import List Arith Sorting Vbase job task schedule identmp priority helper response_time task_arrival.
-
-Section LiuLayland.
-Variable ts: taskset.
-Variable sched: schedule.
-Variable hp: sched_job_hp_relation.
-Variable cpumap: job_mapping.
-
-Hypothesis RM_priority : convert_fp_jldp RM hp.
-
-Definition uniprocessor := ident_mp 1 hp cpumap. (* Uniprocessor system *)
-Hypothesis platform : uniprocessor sched.
-
-Hypothesis arr_seq_from_ts: ts_arrival_sequence ts sched. (* Arrival sequence from task set *)
-Hypothesis periodic_tasks: periodic_task_model ts sched.
-Hypothesis implicit_deadlines: implicit_deadline_model ts.
-
-Hypothesis ts_non_empty: ts <> nil.
-Hypothesis ts_sorted_by_prio: StronglySorted RM ts. 
-
-Hypothesis job_cost_wcet: forall j t tsk (JOBj: job_task j = tsk) (ARRj: arrives_at sched j t), job_cost j = task_cost tsk.
-
-(*Lemma periodic_arrival_k_times : 
-  forall j tsk (JOBj: job_task j = tsk) t (ARRj: arrives_at sched j t) k,
-    exists j', << JOBj': job_task j' = tsk >> /\
-               << ARRj': arrives_at sched j' (t + k*(task_period tsk)) >>.
-Proof.
-  revert periodic_tasks; unfold periodic_task_model; intros PER; ins; des.
-  induction k; simpl; des.
-    by rewrite <- plus_n_O; eauto.
-    {
-      apply NEXT in ARRj'; des; subst; rewrite JOBj' in *.
-      exists j'0; split; eauto using eq_trans.
-      assert (COMM : t + k * task_period (job_task j) + task_period (job_task j) =
-                     t + (task_period (job_task j) + k * task_period (job_task j))); [by omega |].
-      rewrite <- COMM; trivial.
-    }
-Qed.*)
-
-(*Lemma sync_release_is_critical_instant :
-  forall t tsk_i (INi: In tsk_i ts) (SYNC: sync_release ts sched t),
-    critical_instant uniprocessor tsk_i ts sched t.
-Proof.
-
-
-Lemma hp_task_no_interference :
-    forall (tsk_i: sporadic_task),
-        Forall (task_hp tsk_i) ts ->
-            task_response_time tsk_i (tsk_i :: ts) (task_cost tsk_i).
-Proof.
-*)
-
-End LiuLayland.