Commit 5b048a31 authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

Simplify up_set_proper.

parent edfd4f51
...@@ -59,8 +59,8 @@ Global Instance valid : Valid (bound sts) := λ x, ...@@ -59,8 +59,8 @@ Global Instance valid : Valid (bound sts) := λ x,
end. end.
Definition up (s : state) (T : set token) : set state := Definition up (s : state) (T : set token) : set state :=
mkSet (rtc (frame_step T) s). mkSet (rtc (frame_step T) s).
Definition up_set (S : set state) (T : set token) : set state Definition up_set (S : set state) (T : set token) : set state :=
:= S = λ s, up s T. S = λ s, up s T.
Global Instance unit : Unit (bound sts) := λ x, Global Instance unit : Unit (bound sts) := λ x,
match x with match x with
| bound_frag S' _ => bound_frag (up_set S' ) | bound_frag S' _ => bound_frag (up_set S' )
...@@ -135,9 +135,7 @@ Proof. ...@@ -135,9 +135,7 @@ Proof.
f_equiv; last done. move =>s1 s2 Hs. simpl in HT. by apply up_preserving. f_equiv; last done. move =>s1 s2 Hs. simpl in HT. by apply up_preserving.
Qed. Qed.
Instance up_set_proper : Proper (() ==> () ==> ()) up_set. Instance up_set_proper : Proper (() ==> () ==> ()) up_set.
Proof. Proof. by intros S1 S2 [??] T1 T2 [??]; split; apply up_set_preserving. Qed.
by intros ?? EQ1 ?? EQ2; split; apply up_set_preserving; rewrite ?EQ1 ?EQ2.
Qed.
Lemma elem_of_up s T : s up s T. Lemma elem_of_up s T : s up s T.
Proof. constructor. Qed. Proof. constructor. Qed.
Lemma subseteq_up_set S T : S up_set S T. Lemma subseteq_up_set S T : S up_set S T.
......
Supports Markdown
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