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

Clean up

parent 65509b98
No related branches found
No related tags found
No related merge requests found
Pipeline #26966 passed
Stage: build
Hide whitespace changes
Inline Side-by-side
theories/logrel/subtyping.v
+ 28
− 28
View file @ cb171719
...@@ -323,43 +323,43 @@ Section subtype. ...@@ -323,43 +323,43 @@ Section subtype.
iSplit; iIntros "!>". iSplit; iIntros "!>".
+ rewrite /lsty_select /lsty_choice. + rewrite /lsty_select /lsty_choice.
iApply iProto_le_send. iApply iProto_le_send.
iIntros "!>" (x) "%". iExists _ => /=. iIntros "!>" (x HSs). iExists _ => /=.
iSplit; first done. iSplit; first done.
iSplit. iSplit.
* rewrite lookup_fmap in a. rewrite ->fmap_is_Some in a. done. * rewrite lookup_fmap in HSs. rewrite ->fmap_is_Some in HSs. done.
* destruct a as [S HSs]=> /=. * destruct HSs as [S HSs]=> /=.
rewrite lookup_total_alt 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) "%". 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 a as [S HSs]=> /=. * destruct HSs as [S HSs]=> /=.
rewrite lookup_total_alt lookup_total_alt lookup_fmap HSs. rewrite !lookup_total_alt lookup_fmap HSs.
iApply iProto_le_refl. iApply iProto_le_refl.
- rewrite /lsty_app iProto_app_message_tele. - rewrite /lsty_app iProto_app_message_tele.
iSplit; iIntros "!>". iSplit; iIntros "!>".
+ rewrite /lsty_select /lsty_choice. + rewrite /lsty_select /lsty_choice.
iApply iProto_le_recv. iApply iProto_le_recv.
iIntros "!>" (x) "%". 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 a as [S HSs]=> /=. * destruct HSs as [S HSs]=> /=.
rewrite lookup_total_alt 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) "%". iIntros "!>" (x HSs).
iExists _. iExists _.
iSplit; first done. iSplit. iSplit; first done. iSplit.
* rewrite lookup_fmap in a. rewrite ->fmap_is_Some in a. done. * rewrite lookup_fmap in HSs. rewrite ->fmap_is_Some in HSs. done.
* destruct a as [S HSs]=> /=. * destruct HSs as [S HSs]=> /=.
rewrite lookup_total_alt 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.
...@@ -406,21 +406,21 @@ Section subtype. ...@@ -406,21 +406,21 @@ Section subtype.
iSplit; iIntros "!>". iSplit; iIntros "!>".
+ rewrite /lsty_select /lsty_choice. + rewrite /lsty_select /lsty_choice.
iApply iProto_le_recv. iApply iProto_le_recv.
iIntros "!>" (x) "%". 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 a as [S HSs]=> /=. * destruct HSs as [S HSs]=> /=.
rewrite lookup_total_alt 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) "%". iIntros "!>" (x HSs).
iExists _. iExists _.
iSplit; first done. iSplit. iSplit; first done. iSplit.
* rewrite lookup_fmap in a. rewrite ->fmap_is_Some in a. done. * rewrite lookup_fmap in HSs. rewrite ->fmap_is_Some in HSs. done.
* destruct a as [S HSs]=> /=. * destruct HSs as [S HSs]=> /=.
rewrite lookup_total_alt 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.
...@@ -428,23 +428,23 @@ Section subtype. ...@@ -428,23 +428,23 @@ Section subtype.
iSplit; iIntros "!>". iSplit; iIntros "!>".
+ rewrite /lsty_select /lsty_choice. + rewrite /lsty_select /lsty_choice.
iApply iProto_le_send. iApply iProto_le_send.
iIntros "!>" (x) "%". iExists _ => /=. iIntros "!>" (x HSs). iExists _ => /=.
iSplit; first done. iSplit; first done.
iSplit. iSplit.
* rewrite lookup_fmap in a. rewrite ->fmap_is_Some in a. done. * rewrite lookup_fmap in HSs. rewrite ->fmap_is_Some in HSs. done.
* destruct a as [S HSs]=> /=. * destruct HSs as [S HSs]=> /=.
rewrite lookup_total_alt 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) "%". 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 a as [S HSs]=> /=. * destruct HSs as [S HSs]=> /=.
rewrite lookup_total_alt lookup_total_alt lookup_fmap HSs. rewrite !lookup_total_alt lookup_fmap HSs.
iApply iProto_le_refl. iApply iProto_le_refl.
Qed. Qed.
......
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