Commit 41576e6e authored by David Swasey's avatar David Swasey

Changed validity character to ↓ due to font problems.

(I've seen ↓a before for validity, …)
parent 0846921f
...@@ -191,8 +191,8 @@ Module IrisCore (RL : RA_T) (C : CORE_LANG). ...@@ -191,8 +191,8 @@ Module IrisCore (RL : RA_T) (C : CORE_LANG).
Proof. Proof.
intros w n r; split; [intros Hut | intros [r1 [r2 [EQr [Hu Ht] ] ] ] ]. intros w n r; split; [intros Hut | intros [r1 [r2 [EQr [Hu Ht] ] ] ] ].
- destruct Hut as [s Heq]. rewrite-> assoc in Heq. - destruct Hut as [s Heq]. rewrite-> assoc in Heq.
exists (s · u) by auto_valid. exists (s · u) by auto_valid.
exists t by auto_valid. exists t by auto_valid.
split; [|split]. split; [|split].
+ rewrite <-Heq. reflexivity. + rewrite <-Heq. reflexivity.
+ exists s. reflexivity. + exists s. reflexivity.
...@@ -203,7 +203,7 @@ Module IrisCore (RL : RA_T) (C : CORE_LANG). ...@@ -203,7 +203,7 @@ Module IrisCore (RL : RA_T) (C : CORE_LANG).
rewrite <-assoc, (comm _ u), assoc. reflexivity. rewrite <-assoc, (comm _ u), assoc. reflexivity.
Qed. Qed.
Lemma ownR_valid u (INVAL: ~u): Lemma ownR_valid u (INVAL: ~u):
ownR u . ownR u .
Proof. Proof.
intros w n [r VAL] [v Heq]. hnf. unfold ra_proj, proj1_sig in Heq. intros w n [r VAL] [v Heq]. hnf. unfold ra_proj, proj1_sig in Heq.
...@@ -346,7 +346,7 @@ Module IrisCore (RL : RA_T) (C : CORE_LANG). ...@@ -346,7 +346,7 @@ Module IrisCore (RL : RA_T) (C : CORE_LANG).
rewrite-> !assoc, (comm (_ r2)); reflexivity. rewrite-> !assoc, (comm (_ r2)); reflexivity.
Qed. Qed.
Definition state_sat (r: res) σ: Prop := r /\ Definition state_sat (r: res) σ: Prop := r /\
match fst r with match fst r with
| ex_own s => s = σ | ex_own s => s = σ
| _ => True | _ => True
...@@ -404,7 +404,7 @@ Module IrisCore (RL : RA_T) (C : CORE_LANG). ...@@ -404,7 +404,7 @@ Module IrisCore (RL : RA_T) (C : CORE_LANG).
Qed. Qed.
Lemma wsat_valid σ m (r: res) w k : Lemma wsat_valid σ m (r: res) w k :
wsat σ m r w (S k) tt -> r. wsat σ m r w (S k) tt -> r.
Proof. Proof.
intros [rs [HD _] ]. destruct HD as [VAL _]. intros [rs [HD _] ]. destruct HD as [VAL _].
eapply ra_op_valid; [now apply _|]. eassumption. eapply ra_op_valid; [now apply _|]. eassumption.
......
...@@ -135,7 +135,7 @@ Module IrisMeta (RL : RA_T) (C : CORE_LANG). ...@@ -135,7 +135,7 @@ Module IrisMeta (RL : RA_T) (C : CORE_LANG).
wptp safe m w' (S k') tp' rs' (Q :: φs') /\ wsat σ' m (comp_list rs') w' @ S k'. wptp safe m w' (S k') tp' rs' (Q :: φs') /\ wsat σ' m (comp_list rs') w' @ S k'.
Proof. Proof.
destruct (steps_stepn _ _ HSN) as [n HSN']. clear HSN. destruct (steps_stepn _ _ HSN) as [n HSN']. clear HSN.
pose r := (ex_own _ σ, 1:RL.res). pose r := (ex_own _ σ, 1:RL.res).
{ unfold ra_valid. simpl. eapply ra_valid_unit. now apply _. } { unfold ra_valid. simpl. eapply ra_valid_unit. now apply _. }
edestruct (adequacy_ht (w:=fdEmpty) (k:=k') (r:=r) HT HSN') as [w' [rs' [φs' [HW [HSWTP HWS] ] ] ] ]; clear HT HSN'. edestruct (adequacy_ht (w:=fdEmpty) (k:=k') (r:=r) HT HSN') as [w' [rs' [φs' [HW [HSWTP HWS] ] ] ] ]; clear HT HSN'.
- exists (ra_unit _); now rewrite ->ra_op_unit by apply _. - exists (ra_unit _); now rewrite ->ra_op_unit by apply _.
......
...@@ -227,7 +227,7 @@ Module Unsafety (RL : RA_T) (C : CORE_LANG). ...@@ -227,7 +227,7 @@ Module Unsafety (RL : RA_T) (C : CORE_LANG).
move: {HD} (mask_emp_disjoint (mask_full mask_full)) => HD. move: {HD} (mask_emp_disjoint (mask_full mask_full)) => HD.
move: {He HSw' HW} (He _ _ _ _ _ HSw' HLt' HD HW) => [w'' [r' [HSw' [Hei' HW] ] ] ]. move: {He HSw' HW} (He _ _ _ _ _ HSw' HLt' HD HW) => [w'' [r' [HSw' [Hei' HW] ] ] ].
move: HW; rewrite assoc. move=>HW. move: HW; rewrite assoc. move=>HW.
pose α := (ra_proj r' · ra_proj rK). pose α := (ra_proj r' · ra_proj rK).
{ clear -HW. apply wsat_valid in HW. auto_valid. } { clear -HW. apply wsat_valid in HW. auto_valid. }
have {HSw} HSw: w w'' by transitivity w'. have {HSw} HSw: w w'' by transitivity w'.
exists w'' α; split; [done| split]; last first. exists w'' α; split; [done| split]; last first.
...@@ -259,7 +259,7 @@ Module Unsafety (RL : RA_T) (C : CORE_LANG). ...@@ -259,7 +259,7 @@ Module Unsafety (RL : RA_T) (C : CORE_LANG).
move: {Hv} (Hv HV) => [w''' [rei' [HSw'' [Hei' HW] ] ] ]. move: {Hv} (Hv HV) => [w''' [rei' [HSw'' [Hei' HW] ] ] ].
(* now IH *) (* now IH *)
move: HW; rewrite assoc. move=>HW. move: HW; rewrite assoc. move=>HW.
pose α := (ra_proj rei' · ra_proj rK). pose α := (ra_proj rei' · ra_proj rK).
{ clear -HW. apply wsat_valid in HW. auto_valid. } { clear -HW. apply wsat_valid in HW. auto_valid. }
exists w''' α. split; first by transitivity w''. exists w''' α. split; first by transitivity w''.
split; last by rewrite mask_full_union -(mask_full_union mask_emp). split; last by rewrite mask_full_union -(mask_full_union mask_emp).
......
...@@ -29,7 +29,7 @@ Module IrisVS (RL : RA_T) (C : CORE_LANG). ...@@ -29,7 +29,7 @@ Module IrisVS (RL : RA_T) (C : CORE_LANG).
- eapply wsat_equiv, HE; try reflexivity. - eapply wsat_equiv, HE; try reflexivity.
rewrite ->assoc, (comm (_ r1)), HR; reflexivity. rewrite ->assoc, (comm (_ r1)), HR; reflexivity.
- rewrite ->assoc, (comm (_ r1')) in HE'. - rewrite ->assoc, (comm (_ r1')) in HE'.
exists w2. exists (rd · ra_proj r1'). exists w2. exists (rd · ra_proj r1').
{ apply wsat_valid in HE'. auto_valid. } { apply wsat_valid in HE'. auto_valid. }
split; [assumption | split; [| assumption] ]. split; [assumption | split; [| assumption] ].
eapply uni_pred, HP'; [reflexivity|]. exists rd. reflexivity. eapply uni_pred, HP'; [reflexivity|]. exists rd. reflexivity.
...@@ -110,7 +110,7 @@ Module IrisVS (RL : RA_T) (C : CORE_LANG). ...@@ -110,7 +110,7 @@ Module IrisVS (RL : RA_T) (C : CORE_LANG).
- rewrite ->comp_map_remove with (i := i) (r := ri) in HE by (rewrite HLr; reflexivity). - rewrite ->comp_map_remove with (i := i) (r := ri) in HE by (rewrite HLr; reflexivity).
rewrite ->assoc, <- (assoc (_ r)), (comm rf), assoc in HE. rewrite ->assoc, <- (assoc (_ r)), (comm rf), assoc in HE.
exists w'. exists w'.
exists (ra_proj r · ra_proj ri). { destruct HE as [HE _]. eapply ra_op_valid, ra_op_valid; eauto with typeclass_instances. } exists (ra_proj r · ra_proj ri). { destruct HE as [HE _]. eapply ra_op_valid, ra_op_valid; eauto with typeclass_instances. }
split; [reflexivity |]. split; [reflexivity |].
split. split.
+ simpl; eapply HInv; [now auto with arith |]. + simpl; eapply HInv; [now auto with arith |].
...@@ -145,7 +145,7 @@ Module IrisVS (RL : RA_T) (C : CORE_LANG). ...@@ -145,7 +145,7 @@ Module IrisVS (RL : RA_T) (C : CORE_LANG).
exists w' ra_pos_unit; split; [reflexivity | split; [exact I |] ]. exists w' ra_pos_unit; split; [reflexivity | split; [exact I |] ].
rewrite ->(comm (_ r)), <-assoc in HE. rewrite ->(comm (_ r)), <-assoc in HE.
remember (match rs i with Some ri => ri | None => ra_pos_unit end) as ri eqn: EQri. remember (match rs i with Some ri => ri | None => ra_pos_unit end) as ri eqn: EQri.
pose rri := (ra_proj ri · ra_proj r). pose rri := (ra_proj ri · ra_proj r).
{ destruct (rs i) as [rsi |] eqn: EQrsi; subst; { destruct (rs i) as [rsi |] eqn: EQrsi; subst;
[| simpl; rewrite ->ra_op_unit by apply _; now apply ra_pos_valid]. [| simpl; rewrite ->ra_op_unit by apply _; now apply ra_pos_valid].
clear - HE EQrsi. destruct HE as [HE _]. clear - HE EQrsi. destruct HE as [HE _].
...@@ -222,7 +222,7 @@ Module IrisVS (RL : RA_T) (C : CORE_LANG). ...@@ -222,7 +222,7 @@ Module IrisVS (RL : RA_T) (C : CORE_LANG).
- rewrite ->assoc, HR; eapply wsat_equiv, HE; try reflexivity; []. - rewrite ->assoc, HR; eapply wsat_equiv, HE; try reflexivity; [].
clear; intros i; unfold mcup; tauto. clear; intros i; unfold mcup; tauto.
- rewrite ->assoc in HEq. - rewrite ->assoc in HEq.
exists w''. exists (ra_proj rq · ra_proj rr). exists w''. exists (ra_proj rq · ra_proj rr).
{ apply wsat_valid in HEq. auto_valid. } { apply wsat_valid in HEq. auto_valid. }
split; [assumption | split]. split; [assumption | split].
+ unfold lt in HLe0; rewrite ->HSub, HSub', <- HLe0 in Hr; exists rq rr. + unfold lt in HLe0; rewrite ->HSub, HSub', <- HLe0 in Hr; exists rq rr.
...@@ -241,7 +241,7 @@ Module IrisVS (RL : RA_T) (C : CORE_LANG). ...@@ -241,7 +241,7 @@ Module IrisVS (RL : RA_T) (C : CORE_LANG).
ownL <M< inclM. ownL <M< inclM.
Lemma vsGhostUpd m rl (P : RL.res -> Prop) Lemma vsGhostUpd m rl (P : RL.res -> Prop)
(HU : forall rf (HD : (rl · rf)), exists sl, P sl /\ (sl · rf)) : (HU : forall rf (HD : (rl · rf)), exists sl, P sl /\ (sl · rf)) :
valid (vs m m (ownL rl) (xist (ownLP P))). valid (vs m m (ownL rl) (xist (ownLP P))).
Proof. Proof.
unfold ownLP; intros _ _ _ w _ n [ [rp' rl'] Hrval] _ _ HG w'; intros. unfold ownLP; intros _ _ _ w _ n [ [rp' rl'] Hrval] _ _ HG w'; intros.
...@@ -251,7 +251,7 @@ Module IrisVS (RL : RA_T) (C : CORE_LANG). ...@@ -251,7 +251,7 @@ Module IrisVS (RL : RA_T) (C : CORE_LANG).
- clear - Hval EQrl. eapply ra_prod_valid2 in Hval. destruct Hval as [_ Hsnd]. - clear - Hval EQrl. eapply ra_prod_valid2 in Hval. destruct Hval as [_ Hsnd].
rewrite ->assoc, (comm rl), EQrl. rewrite ->assoc, (comm rl), EQrl.
rewrite ra_op_prod_snd in Hsnd. exact Hsnd. rewrite ra_op_prod_snd in Hsnd. exact Hsnd.
- exists w'. exists (rp', rsl). - exists w'. exists (rp', rsl).
{ clear - Hval HCrsl. { clear - Hval HCrsl.
apply ra_prod_valid. split; [|auto_valid]. apply ra_prod_valid. split; [|auto_valid].
eapply ra_prod_valid2 in Hval. destruct Hval as [Hfst _]. eapply ra_prod_valid2 in Hval. destruct Hval as [Hfst _].
......
...@@ -60,21 +60,21 @@ Module IrisWP (RL : RA_T) (C : CORE_LANG). ...@@ -60,21 +60,21 @@ Module IrisWP (RL : RA_T) (C : CORE_LANG).
split; [clear HS HF | split; [clear HV HF | split; clear HV HS; [| clear HF ] ] ]; intros. split; [clear HS HF | split; [clear HV HF | split; clear HV HS; [| clear HF ] ] ]; intros.
- specialize (HV HV0); destruct HV as [w'' [r1' [HSw' [Hφ HE'] ] ] ]. - specialize (HV HV0); destruct HV as [w'' [r1' [HSw' [Hφ HE'] ] ] ].
rewrite ->assoc, (comm (_ r1')) in HE'. rewrite ->assoc, (comm (_ r1')) in HE'.
exists w''. exists (rd · ra_proj r1'). exists w''. exists (rd · ra_proj r1').
{ clear -HE'. apply wsat_valid in HE'. auto_valid. } { clear -HE'. apply wsat_valid in HE'. auto_valid. }
split; [assumption | split; [| assumption] ]. split; [assumption | split; [| assumption] ].
eapply uni_pred, Hφ; [| exists rd]; reflexivity. eapply uni_pred, Hφ; [| exists rd]; reflexivity.
- specialize (HS _ _ _ _ HDec HStep); destruct HS as [w'' [r1' [HSw' [HWP HE'] ] ] ]. - specialize (HS _ _ _ _ HDec HStep); destruct HS as [w'' [r1' [HSw' [HWP HE'] ] ] ].
rewrite ->assoc, (comm (_ r1')) in HE'. exists w''. rewrite ->assoc, (comm (_ r1')) in HE'. exists w''.
destruct k as [| k]; [exists r1'; simpl wsat; tauto |]. destruct k as [| k]; [exists r1'; simpl wsat; tauto |].
exists (rd · ra_proj r1'). exists (rd · ra_proj r1').
{ clear- HE'. apply wsat_valid in HE'. auto_valid. } { clear- HE'. apply wsat_valid in HE'. auto_valid. }
split; [assumption | split; [| assumption] ]. split; [assumption | split; [| assumption] ].
eapply uni_pred, HWP; [| exists rd]; reflexivity. eapply uni_pred, HWP; [| exists rd]; reflexivity.
- specialize (HF _ _ HDec); destruct HF as [w'' [rfk [rret1 [HSw' [HWR [HWF HE'] ] ] ] ] ]. - specialize (HF _ _ HDec); destruct HF as [w'' [rfk [rret1 [HSw' [HWR [HWF HE'] ] ] ] ] ].
destruct k as [| k]; [exists w'' rfk rret1; simpl wsat; tauto |]. destruct k as [| k]; [exists w'' rfk rret1; simpl wsat; tauto |].
rewrite ->assoc, <- (assoc (_ rfk)) in HE'. rewrite ->assoc, <- (assoc (_ rfk)) in HE'.
exists w''. exists rfk. exists (rd · ra_proj rret1). exists w''. exists rfk. exists (rd · ra_proj rret1).
{ clear- HE'. apply wsat_valid in HE'. rewrite comm. eapply ra_op_valid, ra_op_valid; try now apply _. { clear- HE'. apply wsat_valid in HE'. rewrite comm. eapply ra_op_valid, ra_op_valid; try now apply _.
rewrite ->(comm (_ rfk)) in HE'. eassumption. } rewrite ->(comm (_ rfk)) in HE'. eassumption. }
repeat (split; try assumption). repeat (split; try assumption).
...@@ -468,14 +468,14 @@ Module IrisWP (RL : RA_T) (C : CORE_LANG). ...@@ -468,14 +468,14 @@ Module IrisWP (RL : RA_T) (C : CORE_LANG).
clear He; split; [intros HVal; clear HS HF IH HE | split; [clear HV HF HE | clear HV HS HE; split; [clear HS' | clear HF] ]; intros ]. clear He; split; [intros HVal; clear HS HF IH HE | split; [clear HV HF HE | clear HV HS HE; split; [clear HS' | clear HF] ]; intros ].
- specialize (HV HVal); destruct HV as [w'' [r1' [HSw' [Hφ HE] ] ] ]. - specialize (HV HVal); destruct HV as [w'' [r1' [HSw' [Hφ HE] ] ] ].
rewrite ->assoc in HE. exists w''. rewrite ->assoc in HE. exists w''.
exists (ra_proj r1' · ra_proj r2). exists (ra_proj r1' · ra_proj r2).
{ apply wsat_valid in HE. auto_valid. } { apply wsat_valid in HE. auto_valid. }
split; [eassumption | split; [| eassumption ] ]. split; [eassumption | split; [| eassumption ] ].
exists r1' r2; split; [reflexivity | split; [assumption |] ]. exists r1' r2; split; [reflexivity | split; [assumption |] ].
unfold lt in HLt; rewrite ->HLt, <- HSw', <- HSw; apply HLR. unfold lt in HLt; rewrite ->HLt, <- HSw', <- HSw; apply HLR.
- edestruct HS as [w'' [r1' [HSw' [He HE] ] ] ]; try eassumption; []; clear HS. - edestruct HS as [w'' [r1' [HSw' [He HE] ] ] ]; try eassumption; []; clear HS.
destruct k as [| k]; [exists w' r1'; split; [reflexivity | split; [apply wpO | exact I] ] |]. destruct k as [| k]; [exists w' r1'; split; [reflexivity | split; [apply wpO | exact I] ] |].
rewrite ->assoc in HE. exists w''. exists (ra_proj r1' · ra_proj r2). rewrite ->assoc in HE. exists w''. exists (ra_proj r1' · ra_proj r2).
{ apply wsat_valid in HE. auto_valid. } { apply wsat_valid in HE. auto_valid. }
split; [eassumption | split; [| eassumption] ]. split; [eassumption | split; [| eassumption] ].
eapply IH; try eassumption; [ reflexivity |]. eapply IH; try eassumption; [ reflexivity |].
...@@ -483,7 +483,7 @@ Module IrisWP (RL : RA_T) (C : CORE_LANG). ...@@ -483,7 +483,7 @@ Module IrisWP (RL : RA_T) (C : CORE_LANG).
- specialize (HF _ _ HDec); destruct HF as [w'' [rfk [rret [HSw' [HWF [HWR HE] ] ] ] ] ]. - specialize (HF _ _ HDec); destruct HF as [w'' [rfk [rret [HSw' [HWF [HWR HE] ] ] ] ] ].
destruct k as [| k]; [exists w' rfk rret; split; [reflexivity | split; [apply wpO | split; [apply wpO | exact I] ] ] |]. destruct k as [| k]; [exists w' rfk rret; split; [reflexivity | split; [apply wpO | split; [apply wpO | exact I] ] ] |].
rewrite ->assoc, <- (assoc (_ rfk)) in HE. rewrite ->assoc, <- (assoc (_ rfk)) in HE.
exists w''. exists rfk. exists (ra_proj rret · ra_proj r2). exists w''. exists rfk. exists (ra_proj rret · ra_proj r2).
{ clear- HE. apply wsat_valid in HE. eapply ra_op_valid2, ra_op_valid; try now apply _. eassumption. } { clear- HE. apply wsat_valid in HE. eapply ra_op_valid2, ra_op_valid; try now apply _. eassumption. }
split; [eassumption | split; [| split; eassumption] ]. split; [eassumption | split; [| split; eassumption] ].
eapply IH; try eassumption; [ reflexivity |]. eapply IH; try eassumption; [ reflexivity |].
...@@ -508,7 +508,7 @@ Module IrisWP (RL : RA_T) (C : CORE_LANG). ...@@ -508,7 +508,7 @@ Module IrisWP (RL : RA_T) (C : CORE_LANG).
edestruct He as [_ [HeS _] ]; try eassumption; []. edestruct He as [_ [HeS _] ]; try eassumption; [].
edestruct HeS as [w'' [r1' [HSw' [He' HE'] ] ] ]; try eassumption; []. edestruct HeS as [w'' [r1' [HSw' [He' HE'] ] ] ]; try eassumption; [].
clear HE He HeS; rewrite ->assoc in HE'. clear HE He HeS; rewrite ->assoc in HE'.
exists w''. exists (ra_proj r1' · ra_proj r2). exists w''. exists (ra_proj r1' · ra_proj r2).
{ clear- HE'. apply wsat_valid in HE'. auto_valid. } { clear- HE'. apply wsat_valid in HE'. auto_valid. }
split; [eassumption | split; [| eassumption] ]. split; [eassumption | split; [| eassumption] ].
assert (HNV : ~ is_value ei) assert (HNV : ~ is_value ei)
...@@ -523,7 +523,7 @@ Module IrisWP (RL : RA_T) (C : CORE_LANG). ...@@ -523,7 +523,7 @@ Module IrisWP (RL : RA_T) (C : CORE_LANG).
edestruct He' as [HVal _]; try eassumption; []. edestruct He' as [HVal _]; try eassumption; [].
specialize (HVal HV); destruct HVal as [w'' [r1'' [HSw' [Hφ HE'] ] ] ]. specialize (HVal HV); destruct HVal as [w'' [r1'' [HSw' [Hφ HE'] ] ] ].
rewrite ->assoc in HE'. rewrite ->assoc in HE'.
exists w''. exists (ra_proj r1'' · ra_proj r2). exists w''. exists (ra_proj r1'' · ra_proj r2).
{ clear- HE'. apply wsat_valid in HE'. auto_valid. } { clear- HE'. apply wsat_valid in HE'. auto_valid. }
split; [eassumption | split; [| eassumption] ]. split; [eassumption | split; [| eassumption] ].
exists r1'' r2; split; [reflexivity | split; [assumption |] ]. exists r1'' r2; split; [reflexivity | split; [assumption |] ].
......
...@@ -178,7 +178,7 @@ Section UPredBI. ...@@ -178,7 +178,7 @@ Section UPredBI.
Next Obligation. Next Obligation.
intros n m r1 r2 HLe [rd HEq] [r11 [r12 [HEq' [HP HQ]]]]. intros n m r1 r2 HLe [rd HEq] [r11 [r12 [HEq' [HP HQ]]]].
rewrite <- HEq', assoc in HEq; setoid_rewrite HLe. rewrite <- HEq', assoc in HEq; setoid_rewrite HLe.
exists (rd · ra_proj r11) by auto_valid. exists (rd · ra_proj r11) by auto_valid.
exists r12. exists r12.
split; [|split;[|assumption] ]. split; [|split;[|assumption] ].
- simpl. assumption. - simpl. assumption.
...@@ -192,7 +192,7 @@ Section UPredBI. ...@@ -192,7 +192,7 @@ Section UPredBI.
Next Obligation. Next Obligation.
intros n m r1 r2 HLe [r12 HEq] HSI k r rr HEq' HSub HP. intros n m r1 r2 HLe [r12 HEq] HSI k r rr HEq' HSub HP.
rewrite comm in HEq; rewrite <- HEq, <- assoc in HEq'. rewrite comm in HEq; rewrite <- HEq, <- assoc in HEq'.
pose rc := (r12 · ra_proj r) by auto_valid. pose rc := (r12 · ra_proj r) by auto_valid.
eapply HSI with (r':=rc); [| etransitivity; eassumption |]. eapply HSI with (r':=rc); [| etransitivity; eassumption |].
- simpl. assumption. - simpl. assumption.
- eapply uni_pred, HP; [reflexivity|]. exists r12. reflexivity. - eapply uni_pred, HP; [reflexivity|]. exists r12. reflexivity.
...@@ -366,13 +366,13 @@ Section UPredBI. ...@@ -366,13 +366,13 @@ Section UPredBI.
intros P Q R n r; split. intros P Q R n r; split.
- intros [r1 [rr [EQr [HP [r2 [r3 [EQrr [HQ HR]]]]]]]]. - intros [r1 [rr [EQr [HP [r2 [r3 [EQrr [HQ HR]]]]]]]].
rewrite <- EQrr, assoc in EQr. unfold sc. rewrite <- EQrr, assoc in EQr. unfold sc.
exists (ra_proj r1 · ra_proj r2) by auto_valid. exists (ra_proj r1 · ra_proj r2) by auto_valid.
exists r3; split; [assumption | split; [| assumption] ]. exists r3; split; [assumption | split; [| assumption] ].
exists r1 r2; split; [reflexivity | split; assumption]. exists r1 r2; split; [reflexivity | split; assumption].
- intros [rr [r3 [EQr [[r1 [r2 [EQrr [HP HQ]]]] HR]]]]. - intros [rr [r3 [EQr [[r1 [r2 [EQrr [HP HQ]]]] HR]]]].
rewrite <- EQrr, <- assoc in EQr; clear EQrr. rewrite <- EQrr, <- assoc in EQr; clear EQrr.
exists r1. exists r1.
exists (ra_proj r2 · ra_proj r3) by auto_valid. exists (ra_proj r2 · ra_proj r3) by auto_valid.
split; [assumption | split; [assumption |] ]. split; [assumption | split; [assumption |] ].
exists r2 r3; split; [reflexivity | split; assumption]. exists r2 r3; split; [reflexivity | split; assumption].
Qed. Qed.
......
...@@ -32,11 +32,11 @@ Arguments ra_valid {T} {_} t. ...@@ -32,11 +32,11 @@ Arguments ra_valid {T} {_} t.
Notation "1" := (ra_unit _) : ra_scope. Notation "1" := (ra_unit _) : ra_scope.
Notation "p · q" := (ra_op _ p q) (at level 40, left associativity) : ra_scope. Notation "p · q" := (ra_op _ p q) (at level 40, left associativity) : ra_scope.
Notation "'' p" := (ra_valid p = true) (at level 35) : ra_scope. Notation "'' p" := (ra_valid p = true) (at level 35) : ra_scope.
Notation "'~' '' p" := (ra_valid p <> true) (at level 35) : ra_scope. Notation "'~' '' p" := (ra_valid p <> true) (at level 35) : ra_scope.
Delimit Scope ra_scope with ra. Delimit Scope ra_scope with ra.
Tactic Notation "decide" ident(t1) "as" ident(H) := destruct (ra_valid t1) eqn:H; [|apply not_true_iff_false in H]. Tactic Notation "decide" ident(t1) "as" ident(H) := destruct (ra_valid t1) eqn:H; [|apply not_true_iff_false in H].
(* General RA lemmas *) (* General RA lemmas *)
...@@ -49,19 +49,19 @@ Section RAs. ...@@ -49,19 +49,19 @@ Section RAs.
rewrite comm. now eapply ra_op_unit. rewrite comm. now eapply ra_op_unit.
Qed. Qed.
Lemma ra_op_valid2 t1 t2: (t1 · t2) -> t2. Lemma ra_op_valid2 t1 t2: (t1 · t2) -> t2.
Proof. Proof.
rewrite comm. now eapply ra_op_valid. rewrite comm. now eapply ra_op_valid.
Qed. Qed.
Lemma ra_op_invalid t1 t2: ~t1 -> ~(t1 · t2). Lemma ra_op_invalid t1 t2: ~t1 -> ~(t1 · t2).
Proof. Proof.
intros Hinval Hval. intros Hinval Hval.
apply Hinval. apply Hinval.
eapply ra_op_valid; now eauto. eapply ra_op_valid; now eauto.
Qed. Qed.
Lemma ra_op_invalid2 t1 t2: ~t2 -> ~(t1 · t2). Lemma ra_op_invalid2 t1 t2: ~t2 -> ~(t1 · t2).
Proof. Proof.
rewrite comm. now eapply ra_op_invalid. rewrite comm. now eapply ra_op_invalid.
Qed. Qed.
...@@ -115,7 +115,7 @@ Section ProductLemmas. ...@@ -115,7 +115,7 @@ Section ProductLemmas.
Qed. Qed.
Lemma ra_prod_valid (s: S) (t: T): Lemma ra_prod_valid (s: S) (t: T):
(s, t) <-> s /\ t. (s, t) <-> s /\ t.
Proof. Proof.
unfold ra_valid, ra_valid_prod. unfold ra_valid, ra_valid_prod.
rewrite andb_true_iff. rewrite andb_true_iff.
...@@ -123,7 +123,7 @@ Section ProductLemmas. ...@@ -123,7 +123,7 @@ Section ProductLemmas.
Qed. Qed.
Lemma ra_prod_valid2 (st: S*T): Lemma ra_prod_valid2 (st: S*T):
st <-> (fst st) /\ (snd st). st <-> (fst st) /\ (snd st).
Proof. Proof.
destruct st as [s t]. unfold ra_valid, ra_valid_prod. destruct st as [s t]. unfold ra_valid, ra_valid_prod.
rewrite andb_true_iff. rewrite andb_true_iff.
...@@ -136,37 +136,37 @@ Section PositiveCarrier. ...@@ -136,37 +136,37 @@ Section PositiveCarrier.
Context {T} `{raT : RA T}. Context {T} `{raT : RA T}.
Local Open Scope ra_scope. Local Open Scope ra_scope.
Definition ra_pos: Type := { r | r }. Definition ra_pos: Type := { r | r }.
Coercion ra_proj (t:ra_pos): T := proj1_sig t. Coercion ra_proj (t:ra_pos): T := proj1_sig t.
Definition ra_mk_pos t {VAL: t}: ra_pos := exist _ t VAL. Definition ra_mk_pos t {VAL: t}: ra_pos := exist _ t VAL.
Program Definition ra_pos_unit: ra_pos := exist _ 1 _. Program Definition ra_pos_unit: ra_pos := exist _ 1 _.
Next Obligation. Next Obligation.
now erewrite ra_valid_unit by apply _. now erewrite ra_valid_unit by apply _.
Qed. Qed.
Lemma ra_proj_cancel r (VAL: r): Lemma ra_proj_cancel r (VAL: r):
ra_proj (ra_mk_pos r (VAL:=VAL)) = r. ra_proj (ra_mk_pos r (VAL:=VAL)) = r.
Proof. Proof.
reflexivity. reflexivity.
Qed. Qed.
Lemma ra_op_pos_valid t1 t2 t: Lemma ra_op_pos_valid t1 t2 t:
t1 · t2 == ra_proj t -> t1. t1 · t2 == ra_proj t -> t1.
Proof. Proof.
destruct t as [t Hval]; simpl. intros Heq. rewrite <-Heq in Hval. destruct t as [t Hval]; simpl. intros Heq. rewrite <-Heq in Hval.
eapply ra_op_valid; eassumption. eapply ra_op_valid; eassumption.
Qed. Qed.
Lemma ra_op_pos_valid2 t1 t2 t: Lemma ra_op_pos_valid2 t1 t2 t:
t1 · t2 == ra_proj t -> t2. t1 · t2 == ra_proj t -> t2.
Proof. Proof.
rewrite comm. now eapply ra_op_pos_valid. rewrite comm. now eapply ra_op_pos_valid.
Qed. Qed.
Lemma ra_pos_valid (r : ra_pos): Lemma ra_pos_valid (r : ra_pos):
(ra_proj r). (ra_proj r).
Proof. Proof.
destruct r as [r VAL]. destruct r as [r VAL].
exact VAL. exact VAL.
...@@ -186,10 +186,10 @@ Ltac auto_valid := match goal with ...@@ -186,10 +186,10 @@ Ltac auto_valid := match goal with
end. end.
(* FIXME put the common parts into a helper tactic, and allow arbitrary tactics after "by" *) (* FIXME put the common parts into a helper tactic, and allow arbitrary tactics after "by" *)
Tactic Notation "exists✓" constr(t) := let H := fresh "Hval" in assert(H:(t)%ra); [|exists (ra_mk_pos t (VAL:=H) ) ]. Tactic Notation "exists↓" constr(t) := let H := fresh "Hval" in assert(H:(t)%ra); [|exists (ra_mk_pos t (VAL:=H) ) ].
Tactic Notation "exists✓" constr(t) "by" "auto_valid" := let H := fresh "Hval" in assert(H:(t)%ra); [auto_valid|exists (ra_mk_pos t (VAL:=H) ) ]. Tactic Notation "exists↓" constr(t) "by" "auto_valid" := let H := fresh "Hval" in assert(H:(t)%ra); [auto_valid|exists (ra_mk_pos t (VAL:=H) ) ].
Tactic Notation "pose✓" ident(name) ":=" constr(t) := let H := fresh "Hval" in assert(H:(t)%ra); [|pose (name := ra_mk_pos t (VAL:=H) ) ]. Tactic Notation "pose↓" ident(name) ":=" constr(t) := let H := fresh "Hval" in assert(H:(t)%ra); [|pose (name := ra_mk_pos t (VAL:=H) ) ].
Tactic Notation "pose✓" ident(name) ":=" constr(t) "by" "auto_valid" := let H := fresh "Hval" in assert(H:(t)%ra); [auto_valid|pose (name := ra_mk_pos t (VAL:=H) ) ]. Tactic Notation "pose↓" ident(name) ":=" constr(t) "by" "auto_valid" := let H := fresh "Hval" in assert(H:(t)%ra); [auto_valid|pose (name := ra_mk_pos t (VAL:=H) ) ].
Section Order. Section Order.
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment