Skip to content
Snippets Groups Projects
Commit 2f1e2d96 authored by Jonas Kastberg's avatar Jonas Kastberg
Browse files

More clean up

parent cb171719
No related branches found
No related tags found
No related merge requests found
Pipeline #26967 passed
Stage: build
Hide whitespace changes
Inline Side-by-side
theories/logrel/subtyping.v
+ 13
− 20
View file @ 2f1e2d96
...@@ -324,8 +324,7 @@ Section subtype. ...@@ -324,8 +324,7 @@ Section subtype.
+ rewrite /lsty_select /lsty_choice. + rewrite /lsty_select /lsty_choice.
iApply iProto_le_send. iApply iProto_le_send.
iIntros "!>" (x HSs). iExists _ => /=. iIntros "!>" (x HSs). iExists _ => /=.
iSplit; first done. iSplit; first done. iSplit.
iSplit.
* rewrite lookup_fmap in HSs. rewrite ->fmap_is_Some in HSs. done. * rewrite lookup_fmap in HSs. rewrite ->fmap_is_Some in HSs. done.
* destruct HSs as [S HSs]=> /=. * destruct HSs as [S HSs]=> /=.
rewrite !lookup_total_alt HSs /=. rewrite !lookup_total_alt HSs /=.
...@@ -334,8 +333,7 @@ Section subtype. ...@@ -334,8 +333,7 @@ Section subtype.
iApply iProto_le_refl. iApply iProto_le_refl.
+ rewrite /lsty_select /lsty_choice. + rewrite /lsty_select /lsty_choice.
iApply iProto_le_send. iApply iProto_le_send.
iIntros "!>" (x HSs). iIntros "!>" (x HSs). iExists _.
iExists _.
iSplit; first done. iSplit. iSplit; first done. iSplit.
* by rewrite lookup_fmap fmap_is_Some. * by rewrite lookup_fmap fmap_is_Some.
* destruct HSs as [S HSs]=> /=. * destruct HSs as [S HSs]=> /=.
...@@ -346,16 +344,14 @@ Section subtype. ...@@ -346,16 +344,14 @@ Section subtype.
+ rewrite /lsty_select /lsty_choice. + rewrite /lsty_select /lsty_choice.
iApply iProto_le_recv. iApply iProto_le_recv.
iIntros "!>" (x HSs). iExists _ => /=. iIntros "!>" (x HSs). iExists _ => /=.
iSplit; first done. iSplit; first done. iSplit.
iSplit.
* by rewrite lookup_fmap fmap_is_Some. * by rewrite lookup_fmap fmap_is_Some.
* destruct HSs as [S HSs]=> /=. * destruct HSs as [S HSs]=> /=.
rewrite !lookup_total_alt lookup_fmap HSs. rewrite !lookup_total_alt lookup_fmap HSs.
iApply iProto_le_refl. iApply iProto_le_refl.
+ rewrite /lsty_select /lsty_choice. + rewrite /lsty_select /lsty_choice.
iApply iProto_le_recv. iApply iProto_le_recv.
iIntros "!>" (x HSs). iIntros "!>" (x HSs). iExists _.
iExists _.
iSplit; first done. iSplit. iSplit; first done. iSplit.
* rewrite lookup_fmap in HSs. rewrite ->fmap_is_Some in HSs. done. * rewrite lookup_fmap in HSs. rewrite ->fmap_is_Some in HSs. done.
* destruct HSs as [S HSs]=> /=. * destruct HSs as [S HSs]=> /=.
...@@ -407,16 +403,14 @@ Section subtype. ...@@ -407,16 +403,14 @@ Section subtype.
+ rewrite /lsty_select /lsty_choice. + rewrite /lsty_select /lsty_choice.
iApply iProto_le_recv. iApply iProto_le_recv.
iIntros "!>" (x HSs). iExists _ => /=. iIntros "!>" (x HSs). iExists _ => /=.
iSplit; first done. iSplit; first done. iSplit.
iSplit.
* by rewrite lookup_fmap fmap_is_Some. * by rewrite lookup_fmap fmap_is_Some.
* destruct HSs as [S HSs]=> /=. * destruct HSs as [S HSs]=> /=.
rewrite !lookup_total_alt lookup_fmap HSs. rewrite !lookup_total_alt lookup_fmap HSs.
iApply iProto_le_refl. iApply iProto_le_refl.
+ rewrite /lsty_select /lsty_choice. + rewrite /lsty_select /lsty_choice.
iApply iProto_le_recv. iApply iProto_le_recv.
iIntros "!>" (x HSs). iIntros "!>" (x HSs). iExists _.
iExists _.
iSplit; first done. iSplit. iSplit; first done. iSplit.
* rewrite lookup_fmap in HSs. rewrite ->fmap_is_Some in HSs. done. * rewrite lookup_fmap in HSs. rewrite ->fmap_is_Some in HSs. done.
* destruct HSs as [S HSs]=> /=. * destruct HSs as [S HSs]=> /=.
...@@ -429,14 +423,13 @@ Section subtype. ...@@ -429,14 +423,13 @@ Section subtype.
+ rewrite /lsty_select /lsty_choice. + rewrite /lsty_select /lsty_choice.
iApply iProto_le_send. iApply iProto_le_send.
iIntros "!>" (x HSs). iExists _ => /=. iIntros "!>" (x HSs). iExists _ => /=.
iSplit; first done. iSplit; first done. iSplit.
iSplit. * rewrite lookup_fmap in HSs. rewrite ->fmap_is_Some in HSs. done.
* rewrite lookup_fmap in HSs. rewrite ->fmap_is_Some in HSs. done. * destruct HSs as [S HSs]=> /=.
* destruct HSs as [S HSs]=> /=. rewrite !lookup_total_alt HSs /=.
rewrite !lookup_total_alt HSs /=. rewrite lookup_fmap in HSs.
rewrite lookup_fmap in HSs. apply fmap_Some_1 in HSs as [S' [-> ->]].
apply fmap_Some_1 in HSs as [S' [-> ->]]. iApply iProto_le_refl.
iApply iProto_le_refl.
+ rewrite /lsty_select /lsty_choice. + rewrite /lsty_select /lsty_choice.
iApply iProto_le_send. iApply iProto_le_send.
iIntros "!>" (x HSs). iIntros "!>" (x HSs).
......
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