Commit b4843a6b authored by Jonas Kastberg Hinrichsen's avatar Jonas Kastberg Hinrichsen
Browse files

Moved and generalised stype_map_equiv

parent f452b81f
......@@ -131,10 +131,6 @@ Section Encodings.
+ intros v. destruct (decode v); eauto.
Qed.
Lemma stype_map_equiv {A B : ofeT} (f : A -n> B) (st st' : stype val A) :
st st' stype_map f st stype_map f st'.
Proof. induction 1=>//. constructor=>//. by repeat f_equiv. Qed.
Notation "⟦ c @ s : sτ ⟧{ γ }" := (interp_st N γ sτ c s)
(at level 10, s at next level, sτ at next level, γ at next level,
format "⟦ c @ s : sτ ⟧{ γ }").
......@@ -160,7 +156,7 @@ Section Encodings.
left.
f_equiv.
f_equiv.
apply stype_map_equiv.
apply stype_map_equiv=> //.
apply dual_stype'_comm.
Qed.
......
......@@ -179,6 +179,9 @@ Proof.
- intros v. f_equiv. apply HP.
- intros v. apply IH.
Qed.
Lemma stype_map_equiv {A B : ofeT} (f g : A -n> B) (st st' : stype val A) :
( x, f x g x) st st' stype_map f st stype_map g st'.
Proof. intros Feq. induction 1=>//. constructor=>//. by repeat f_equiv. Qed.
Lemma stype_fmap_id {V : Type} {A : ofeT} (st : stype V A) :
stype_map id st st.
Proof.
......
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