Commit 0204cf5e authored by Ralf Jung's avatar Ralf Jung

move equivP ro CSetoid as equivR

parent 91bdb949
......@@ -61,11 +61,6 @@ Module Unsafety (RL : RA_T) (C : CORE_LANG).
by exfalso; omega.
Qed.
(* Leibniz equality arise from SSR's case tactic.
RJ: I could use this ;-) move to CSetoid? *) (* PDS: Feel free. I'd like to eventually get everything but the robust safety theorem out of this file. *)
Lemma equivP {T : Type} `{eqT : Setoid T} {a b : T} : a = b -> a == b.
Proof. by move=>->; reflexivity. Qed.
(*
Simple monotonicity tactics for props and wsat.
......@@ -213,7 +208,7 @@ Module Unsafety (RL : RA_T) (C : CORE_LANG).
exists w'' α; split; [done| split]; last first.
+ by move: HW; rewrite 2! mask_full_union => HW; wsatM HW.
apply: (IH _ HLt _ _ _ _ HSw); last done.
rewrite fillE; exists r' rK; split; [exact: equivP | split; [by propsM Hei' |] ].
rewrite fillE; exists r' rK; split; [exact: equivR | split; [by propsM Hei' |] ].
have {HSw} HSw: w w'' by transitivity w'.
by propsM HK.
......@@ -246,7 +241,7 @@ Module Unsafety (RL : RA_T) (C : CORE_LANG).
rewrite/= in Hei'; rewrite fill_empty -Hk' in Hei' * => {Hk'}.
have {HSw} HSw : w w''' by transitivity w''; first by transitivity w'.
apply: (IH _ HLt _ _ _ _ HSw); last done.
rewrite fillE; exists rei' rK; split; [exact: equivP | split; [done |] ].
rewrite fillE; exists rei' rK; split; [exact: equivR | split; [done |] ].
have {HSw HSw' HSw''} HSw: w w''' by transitivity w''; first by transitivity w'.
by propsM HK.
Qed.
......
......@@ -107,7 +107,7 @@ Module IrisVS (RL : RA_T) (C : CORE_LANG).
do 8 red in HInv.
destruct HE as [rs [HE HM] ].
destruct (rs i) as [ri |] eqn: HLr.
- 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 now eapply equivR.
rewrite ->assoc, <- (assoc (_ r)), (comm rf), assoc in HE.
exists w'.
exists (ra_proj r · ra_proj ri). { destruct HE as [HE _]. eapply ra_op_valid, ra_op_valid; eauto with typeclass_instances. }
......@@ -149,15 +149,15 @@ Module IrisVS (RL : RA_T) (C : CORE_LANG).
{ destruct (rs i) as [rsi |] eqn: EQrsi; subst;
[| simpl; rewrite ->ra_op_unit by apply _; now apply ra_pos_valid].
clear - HE EQrsi. destruct HE as [HE _].
rewrite ->comp_map_remove with (i:=i) in HE by (erewrite EQrsi; reflexivity).
rewrite ->comp_map_remove with (i:=i) in HE by (eapply equivR; eassumption).
rewrite ->(assoc (_ r)), (comm (_ r)), comm, assoc, <-(assoc (_ rsi) _), (comm _ (ra_proj r)), assoc in HE.
eapply ra_op_valid, ra_op_valid; now eauto with typeclass_instances.
}
exists (fdUpdate i rri rs); split; [| intros j Hm].
- simpl. erewrite ra_op_unit by apply _.
clear - HE EQri. destruct (rs i) as [rsi |] eqn: EQrsi.
+ subst rsi. erewrite <-comp_map_insert_old; [ eassumption | rewrite EQrsi; reflexivity | reflexivity ].
+ unfold rri. subst ri. simpl. erewrite <-comp_map_insert_new; [|rewrite EQrsi; reflexivity]. simpl.
+ subst rsi. erewrite <-comp_map_insert_old; [ eassumption | eapply equivR; eassumption | reflexivity ].
+ unfold rri. subst ri. simpl. erewrite <-comp_map_insert_new; [|now eapply equivR]. simpl.
erewrite ra_op_unit by apply _. assumption.
- specialize (HD j); unfold mask_sing, mask_set, mcup in *; simpl in Hm, HD.
destruct (Peano_dec.eq_nat_dec i j);
......@@ -321,7 +321,7 @@ Module IrisVS (RL : RA_T) (C : CORE_LANG).
}
split.
{
rewrite <-comp_map_insert_new by (rewrite HRi; reflexivity).
rewrite <-comp_map_insert_new by now eapply equivR.
rewrite ->assoc, (comm rf). assumption.
}
intros j Hm'.
......
......@@ -16,6 +16,13 @@ Generalizable Variables T U V W.
Definition equiv `{Setoid T} := SetoidClass.equiv.
Arguments equiv {_ _} _ _ /.
(* Proof by reflexivity *)
Lemma equivR {T : Type} `{eqT : Setoid T} {a b : T} :
a = b -> a == b.
Proof.
intros Heq. subst a. reflexivity.
Qed.
Notation "'mkType' R" := (@Build_Setoid _ R _) (at level 10).
(** A morphism between two types is an actual function together with a
......
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