Commit 76dddf93 authored by Ralf Jung's avatar Ralf Jung

prevent masks from clobbering the == notation

parent adedfdce
......@@ -155,7 +155,7 @@ Module IrisMeta (RL : RA_T) (C : CORE_LANG).
Next Obligation.
intros x y H_xy P m r. simpl in H_xy. destruct n.
- intros LEZ. exfalso. omega.
- intros _. simpl. assert(H_xy': equiv x y) by assumption. rewrite H_xy'. tauto.
- intros _. simpl. assert(H_xy': x == y) by assumption. rewrite H_xy'. tauto.
Qed.
......@@ -217,7 +217,7 @@ Module IrisMeta (RL : RA_T) (C : CORE_LANG).
Next Obligation.
intros x y H_xy P m r. simpl in H_xy. destruct n.
- intros LEZ. exfalso. omega.
- intros _. simpl. assert(H_xy': equiv x y) by assumption. rewrite H_xy'. tauto.
- intros _. simpl. assert(H_xy': x == y) by assumption. rewrite H_xy'. tauto.
Qed.
Program Definition plugExpr safe m φ P Q: expr -n> Props :=
......
......@@ -168,7 +168,7 @@ Module IrisVS (RL : RA_T) (C : CORE_LANG).
rewrite ->HSub in HP; specialize (HSub i); rewrite HLu in HSub.
destruct (w' i) as [π' |]; [| contradiction].
split; [intuition now eauto | intros].
simpl in HLw, HSub. change (equiv rri ri0) in HLrs. rewrite <- HLw, <- HSub.
simpl in HLw, HSub. change (rri == ri0) in HLrs. rewrite <- HLw, <- HSub.
apply HInv; [now auto with arith |].
eapply uni_pred, HP; [now auto with arith |].
rewrite <-HLrs. clear dependent ri0.
......
......@@ -271,16 +271,13 @@ Section Exclusive.
| _, _ => False
end.
Global Program Instance ra_eq_equiv : Equivalence ra_res_ex_eq.
Next Obligation.
intros [t| |]; simpl; now auto.
Qed.
Next Obligation.
intros [t1| |] [t2| |]; simpl; now auto.
Qed.
Next Obligation.
intros [t1| |] [t2| |] [t3| |]; simpl; try now auto.
- intros ? ?. etransitivity; eassumption.
Global Instance ra_eq_equiv : Equivalence ra_res_ex_eq.
Proof.
split.
- intros [t| |]; simpl; now auto.
- intros [t1| |] [t2| |]; simpl; now auto.
- intros [t1| |] [t2| |] [t3| |]; simpl; try now auto.
+ intros ? ?. etransitivity; eassumption.
Qed.
Global Program Instance ra_type_ex : Setoid ra_res_ex :=
......
Require Import Arith Program RelationClasses Morphisms.
Require Import ModuRes.CSetoid.
Definition mask := nat -> Prop.
......@@ -28,8 +29,16 @@ Definition mcup (m1 m2 : mask) : mask :=
Definition mminus (m1 m2 : mask) : mask :=
fun i => (m1 : mask) i /\ ~ (m2 : mask) i.
Global Instance meq_Equivalence: Equivalence meq.
Proof.
split.
- intros m. unfold meq. tauto.
- intros m1 m2. unfold meq. now auto.
- intros m1 m2 m3. unfold meq. now firstorder.
Qed.
Global Instance mask_type : Setoid mask := mkType meq.
Delimit Scope mask_scope with mask.
Notation "m1 == m2" := (meq m1 m2) (at level 70) : mask_scope.
Notation "m1 ⊆ m2" := (mle m1 m2) (at level 70) : mask_scope.
Notation "m1 ∩ m2" := (mcap m1 m2) (at level 40) : mask_scope.
Notation "m1 \ m2" := (mminus m1 m2) (at level 30) : mask_scope.
......
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