From 258605b56b11b24477df44d0b75bca17380b5136 Mon Sep 17 00:00:00 2001 From: Jacques-Henri Jourdan <jacques-henri.jourdan@normalesup.org> Date: Fri, 6 Jan 2017 13:19:54 +0100 Subject: [PATCH] Added a lemma for sharing without reborrowing. --- theories/typing/tests/get_x.v | 4 ++-- theories/typing/uniq_bor.v | 11 +++++++++++ 2 files changed, 13 insertions(+), 2 deletions(-) diff --git a/theories/typing/tests/get_x.v b/theories/typing/tests/get_x.v index daf5f1d8..48290a3f 100644 --- a/theories/typing/tests/get_x.v +++ b/theories/typing/tests/get_x.v @@ -22,7 +22,7 @@ Section get_x. eapply type_let'. { apply _. } - { by apply (type_deref (&uniq{α}Π[int; int])), read_own_move. } + { by eapply (type_deref (&uniq{α} _)), read_own_move. } { solve_typing. } intros p'. simpl_subst. @@ -30,7 +30,7 @@ Section get_x. eapply type_let'. { apply _. } - { eapply (type_delete (uninit 1) 1); solve_typing. } + { by eapply (type_delete (uninit 1) 1). } { solve_typing. } move=> /= _. diff --git a/theories/typing/uniq_bor.v b/theories/typing/uniq_bor.v index bc8db852..a6d7c289 100644 --- a/theories/typing/uniq_bor.v +++ b/theories/typing/uniq_bor.v @@ -201,6 +201,16 @@ Section typing. by apply (tctx_incl_frame_r _ [_] [_]), subtype_tctx_incl, shr_mono'. Qed. + Lemma tctx_extract_hasty_share_samelft E L p ty ty' κ T : + lctx_lft_alive E L κ → subtype E L ty' ty → + tctx_extract_hasty E L p (&shr{κ}ty) ((p ◠&uniq{κ}ty')::T) + ((p ◠&shr{κ}ty')::T). + Proof. + intros. apply (tctx_incl_frame_r _ [_] [_;_]). + rewrite tctx_share // {1}copy_tctx_incl. + by apply (tctx_incl_frame_r _ [_] [_]), subtype_tctx_incl, shr_mono'. + Qed. + Lemma tctx_extract_hasty_reborrow E L p ty ty' κ κ' T : lctx_lft_incl E L κ' κ → eqtype E L ty ty' → tctx_extract_hasty E L p (&uniq{κ'}ty) ((p ◠&uniq{κ}ty')::T) @@ -246,3 +256,4 @@ End typing. Hint Resolve uniq_mono' uniq_proper' tctx_extract_hasty_share tctx_extract_hasty_reborrow : lrust_typing. +Hint Resolve tctx_extract_hasty_share_samelft | 0 : lrust_typing. -- GitLab