Added ldrf/ to compilation and fixed bugs there.

Author: anlun

Makefile

@@ -1,5 +1,5 @@
 COQMODULE    := imm 
-COQTHEORIES  := src/basic/*.v src/imm/*.v src/hardware/*.v src/rc11/*.v src/c11/*.v src/jsmm/*.v src/ocamlmm/*.v src/traversal/*.v src/travorder/*.v src/simhelpers/*.v
+COQTHEORIES  := src/basic/*.v src/imm/*.v src/hardware/*.v src/rc11/*.v src/c11/*.v src/jsmm/*.v src/ocamlmm/*.v src/traversal/*.v src/travorder/*.v src/simhelpers/*.v src/ldrf/*.v
 
 .PHONY: all theories clean tounicode
 

src/ldrf/LDRF_Fsc.v

@@ -108,7 +108,7 @@ Hypothesis WATF2: W ∩₁ AT ⊆₁ dom_rel (immediate sb ⨾ ⦗F ∩₁ Sc⦘
 
 Lemma mode_split (S: actid -> Prop) (HASLOC: forall x, S x -> exists l, loc x = Some l):
   S ≡₁ (S ∩₁ NA) ∪₁ (S ∩₁ AT).
-Proof using.
+Proof using LOCMODE.
   red. split; [| basic_solver].
   rewrite <- set_inter_union_r.
   apply set_subset_inter_r. split; [basic_solver| ]. 
@@ -121,7 +121,7 @@ Qed.
 
 Lemma sb_f_helper T M (TF: T ⊆₁ codom_rel (⦗F ∩₁ M⦘ ⨾ immediate sb)):
   ⦗RW⦘ ⨾ sb ⨾ ⦗T⦘ ⊆ ⦗RW⦘ ⨾ sb ⨾ ⦗F ∩₁ M⦘ ⨾ sb ⨾ ⦗T⦘.
-Proof using.
+Proof using WNAF WF WATF2 WATF1 RWMODE RATF2 RATF1 NA AT.
   unfolder. intros e a H. destruct H as [RWe [SBew Ta]]. split; auto.
   red in TF. specialize (@TF a).
   pose proof (TF Ta) as [f HH].
@@ -141,7 +141,7 @@ Qed.
 
 Lemma sb_f_w:
   ⦗RW⦘ ⨾ sb ⨾ ⦗W⦘ ⊆ ⦗RW⦘ ⨾ sb ⨾ ⦗F ∩₁ Sc⦘ ⨾ sb ⨾ ⦗W ∩₁ AT⦘ ∪ ⦗RW⦘ ⨾ sb ⨾ ⦗F ∩₁ Acqrel⦘ ⨾ sb ⨾ ⦗W ∩₁ NA⦘.
-Proof using.
+Proof using All.
   assert (FENCE: forall MW MF (COMP: W ∩₁ MW
           ⊆₁ codom_rel (⦗F ∩₁ MF⦘ ⨾ immediate sb) ∪₁ Init),
              ⦗RW⦘ ⨾ sb ⨾ ⦗W ∩₁ MW⦘ ⊆ ⦗RW⦘ ⨾ sb ⨾ ⦗F ∩₁ MF⦘ ⨾ sb ⨾ ⦗W ∩₁ MW⦘). 
@@ -160,7 +160,7 @@ Proof using.
 Qed. 
 
 Lemma sb_rf_acyclic: acyclic (sb ⨾ rfe).
-Proof using.
+Proof using All.
   rewrite ((wf_rfeD WF)). arewrite (R ⊆₁ RW).
   rewrite <- !seqA, acyclic_rotl, !seqA.
   sin_rewrite sb_f_w.
@@ -172,18 +172,20 @@ Proof using.
     sin_rewrite sb_to_f_in_bob. sin_rewrite sb_from_f_in_bob. basic_solver. }
   do 2 sin_rewrite FBOB.
   rewrite !inclusion_seq_eqv_r, !inclusion_seq_eqv_l.
-  arewrite (rfe ⊆ ar). arewrite (bob ⊆ ar).
+  arewrite (rfe ⊆ ar).
+  arewrite (bob ⊆ ar).
+  { unfold ar, ar_int. eauto with hahn. }
   rewrite unionK, seqA.
   red.
   red in Cext0.
   arewrite (ar ⨾ ar ⨾ ar ⊆ ar^+).
-  { do 2 rewrite <- ct_unit. rewrite seqA. basic_solver 10. }
+  { do 2 rewrite <- ct_unit. rewrite seqA. now rewrite <- ct_step. }
   rewrite ct_of_ct. auto.
 Qed.
 
 
 Lemma sb_rfe_crt_hb: (⦗RW⦘ ⨾ sb ⨾ rfe)^* ⨾ sb ⨾ ⦗F ∩₁ Sc⦘ ⊆ hb.
-Proof using.
+Proof using All.
   rewrite (dom_l (wf_rfeD WF)).
   sin_rewrite sb_f_w.  
   arewrite (F ∩₁ Sc ⊆₁ F ∩₁ Acqrel) by mode_solver.
@@ -218,7 +220,7 @@ Qed.
 
 Lemma sl_mode r (SL: r ⊆ same_loc):
   ⦗RW⦘ ⨾ r ⨾ ⦗RW⦘ ⊆ restr_rel NA r ∪ restr_rel AT r.
-Proof using.
+Proof using All.
   unfolder. ins. destruct H as [RWx [RELxy RWy]].
   assert (exists l, Loc_ l x) as [l Lx].
   { unfold Events.loc. unfold is_f in *.
@@ -233,7 +235,7 @@ Proof using.
 Qed.
 
 Lemma sb_f_at: RW ∩₁ AT ∩₁ NInit ⊆₁ codom_rel (⦗F ∩₁ Sc⦘ ⨾ immediate sb).
-Proof using.
+Proof using All.
   do 2 rewrite set_inter_union_l.
   apply set_subset_union_l.
   split.
@@ -244,7 +246,7 @@ Qed.
 
 
 Lemma f_sb_at: RW ∩₁ AT ∩₁ NInit  ⊆₁ dom_rel (immediate sb ⨾ ⦗F ∩₁ Sc⦘).
-Proof using.   
+Proof using All.   
   do 2 rewrite set_inter_union_l.
   apply set_subset_union_l.
   split.
@@ -256,7 +258,7 @@ Qed.
 
 Lemma ct_dom_start: forall (A: Type) (r: relation A) (dom: A -> Prop), 
     ⦗dom⦘ ⨾ (r ⨾ ⦗dom⦘)^+ ≡ (⦗dom⦘ ⨾ r ⨾ ⦗dom⦘)^+.
-Proof using.
+Proof using All.
   intros A r dom. 
   rewrite ct_rotl.
   rewrite <- (seqA ⦗dom⦘ r ⦗dom⦘). rewrite ct_rotl.
@@ -266,20 +268,20 @@ Proof using.
 Qed.
 
 Lemma acyclic_empty: forall (A: Type), @acyclic A ∅₂.
-Proof using.
+Proof using All.
   intros A. red.
   rewrite ct_of_trans; [| basic_solver]. 
   basic_solver.
 Qed. 
 
 Lemma sb_eco_sb_psc: ⦗F ∩₁ Sc⦘ ⨾ sb ⨾ eco ⨾ sb ⨾ ⦗F ∩₁ Sc⦘ ⊆ psc G.
-Proof using. unfold psc. rewrite sb_in_hb. basic_solver 10. Qed. 
+Proof using All. unfold psc. rewrite sb_in_hb. basic_solver 10. Qed. 
 
 Lemma RFE1: rfe^+ ≡ rfe.
-Proof using.  apply ct_no_step. rewrite (wf_rfeD WF). type_solver. Qed. 
+Proof using All.  apply ct_no_step. rewrite (wf_rfeD WF). type_solver. Qed. 
 
 Lemma no_eco_to_init: eco ≡ eco ⨾ ⦗NInit⦘. 
-Proof using.
+Proof using All.
   split; [| basic_solver].
   arewrite (eco ≡ eco ⨾ ⦗codom_rel eco⦘) at 1 by basic_solver.
   apply seq_mori; [basic_solver|]. 
@@ -293,8 +295,8 @@ Proof using.
 Qed. 
 
 Lemma acyclic_sb_rf_eco: acyclic (sb ∪ restr_rel NA rf ∪ restr_rel AT eco). 
-Proof using.
-  rewrite rfi_union_rfe, <- union_restr, <- unionA.
+Proof using All.
+  rewrite rfi_union_rfe, restr_union, <- unionA.
   arewrite (restr_rel NA rfi ⊆ sb). rewrite unionK. 
   assert (na_at_rels_empty: restr_rel NA rfe ⨾ restr_rel AT eco ≡ ∅₂).
   { generalize DIFMODE. basic_solver. }
@@ -386,14 +388,14 @@ Qed.
 
 Lemma imm_to_ocaml_causal:
   acyclic (sb ∪ rfe ∪ restr_rel AT (coe ∪ fre G)).
-Proof using.
+Proof using All.
   arewrite (rfe ⊆ rf). 
   arewrite (rf ⊆ restr_rel NA rf ∪ restr_rel AT rf).
   { rewrite (wf_rfD WF) at 1. arewrite (R ⊆₁ RW). arewrite (W ⊆₁ RW) at 1.  
     rewrite sl_mode; [basic_solver | apply (wf_rfl WF)]. }
 
   do 2 rewrite unionA.
-  rewrite union_restr. 
+  rewrite <- restr_union. 
   arewrite ((rf ∪ (coe ∪ fre G)) ⊆ eco).
   { unfold Execution_eco.eco, Execution.rf, Execution.coe, Execution.fre. basic_solver 10. }
   rewrite <- unionA. apply acyclic_sb_rf_eco. 
@@ -403,7 +405,7 @@ Qed.
 Lemma f_sb_helper T M (TF: T ⊆₁ dom_rel (immediate sb ⨾ ⦗F ∩₁ M⦘))
   (NIT: T ∩₁ is_init ≡₁ ∅):
   ⦗T⦘ ⨾ sb ⨾ ⦗RW⦘ ⊆ ⦗T⦘ ⨾ sb ⨾ ⦗F ∩₁ M⦘ ⨾ sb ⨾ ⦗RW⦘.
-Proof using.
+Proof using All.
   unfolder. intros a e [Ta [SBae RWe]]. split; auto. 
   red in TF. specialize (@TF a).
   pose proof (TF Ta) as [f HH].
@@ -423,13 +425,13 @@ Proof using.
 Qed.
 
 Lemma ac_irr: forall A (r: relation A), acyclic r <-> irreflexive r^+.
-Proof using. intros A r. basic_solver. Qed. 
+Proof using All. intros A r. basic_solver. Qed. 
 
 Definition ae := (⦗AT⦘ ⨾ (rfe ∪ co) ⨾ ⦗AT⦘).
 
 
 Lemma imm_to_ocaml_coherent: irreflexive ((sb ∪ ae)^+ ⨾ (co ∪ fr)).
-Proof using.
+Proof using All.
   arewrite (co ∪ fr ⊆ eco) by unfold Execution_eco.eco; basic_solver 10. 
   rewrite ct_unionE.
   assert (ae_in_eco: ae ⊆ eco).
@@ -534,7 +536,7 @@ Qed.
 
 Theorem ldrf_condition_ext:
   acyclic(sb ∪ rf ∪ ⦗F ∩₁ Sc⦘ ⨾ sb ⨾ eco ⨾ sb ⨾ ⦗F ∩₁ Sc⦘). 
-Proof using.
+Proof using All.
   apply acyclic_union1.
   { rewrite (wf_rfD WF). arewrite (W ⊆₁ RW). arewrite (R ⊆₁ RW) at 2 .
     rewrite (sl_mode); [| apply (wf_rfl WF)].
@@ -585,7 +587,7 @@ Proof using.
 Qed.
 
 Theorem ldrf_condition: acyclic(sb ∪ rf ∪ ⦗AT⦘ ⨾ sb ⨾ eco ⨾ sb ⨾ ⦗AT⦘).
-Proof using. 
+Proof using All. 
   arewrite (sb ∪ rf ∪ ⦗AT⦘ ⨾ sb ⨾ eco ⨾ sb ⨾ ⦗AT⦘ ⊆ (sb ∪ rf ∪ ⦗AT⦘ ⨾ sb ⨾ eco ⨾ sb ⨾ ⦗AT⦘) ⨾ ⦗NInit⦘).
   { rewrite (no_sb_to_init G) at 1. rewrite (no_sb_to_init G) at 3.
     rewrite (no_rf_to_init WF) at 1.