From 9334867238fd7fcdfdaeab35dd305a76c4a4fbea Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?=E6=9D=BE=E4=B8=8B=E7=A5=90=E4=BB=8B?= <y.skm24t@gmail.com>
Date: Fri, 8 Apr 2022 19:15:14 +0900
Subject: [PATCH] Pass over derived_rules.v
---
README.md | 6 +-
theories/typing/examples/derived_rules.v | 88 +++++++++++-------------
2 files changed, 45 insertions(+), 49 deletions(-)
diff --git a/README.md b/README.md
index c93882d2..e13bd896 100644
--- a/README.md
+++ b/README.md
@@ -71,9 +71,9 @@ The filenames are spread across `theories/typing/examples`, `theories/typing`, `
| ------------------- | ----------------- | ------------------------ |
| Adequacy | `soundness.v` | `type_soundness` |
| **Basic** | | |
-| MUTBOR | `derived_rules.v` | `ty_borrow` |
-| MUTREF-WRITE | `derived_rules.v` | `ty_assgn_bor_mut` |
-| MUTREF-BYE | `derived_rules.v` | `ty_resolve` |
+| MUTBOR | `derived_rules.v` | `ty_uniq_bor` |
+| MUTREF-WRITE | `derived_rules.v` | `ty_uniq_ref_write` |
+| MUTREF-BYE | `derived_rules.v` | `ty_uniq_ref_bye` |
| ENDLFT | `programs.v` | `type_endlft` |
| **Prophecies** | | |
| PROPH-INTRO | `prophecy.v` | `proph_intro` |
diff --git a/theories/typing/examples/derived_rules.v b/theories/typing/examples/derived_rules.v
index e8cfab4a..90d43c06 100644
--- a/theories/typing/examples/derived_rules.v
+++ b/theories/typing/examples/derived_rules.v
@@ -1,65 +1,61 @@
From lrust.typing Require Import typing.
Set Default Proof Using "Type".
+Notation "drop: x" := Skip%E (only parsing, at level 102, x at level 1)
+ : expr_scope.
+
+Notation "let: x := &uniq{ κ } p 'in' e" := (let: x := p in e)%E
+ (only parsing, at level 102, x at level 1, e at level 150) : expr_scope.
+
Section rules.
- Local Set Warnings "-non-reversible-notation".
Context `{!typeG Σ}.
- Lemma ty_assgn_box {𝔄 𝔄'} E L p (τ : type 𝔄) p' (τ' : type 𝔄'):
- τ.(ty_size) = τ'.(ty_size) →
- typed_instr E L +[p ◁ box τ; p' ◁ τ'] (p <- p') (λ _, +[p ◁ box τ'])
- (λ post '-[a; b], post -[b]).
+ Lemma ty_box_write {𝔄 𝔅} E L p (ty: type 𝔄) p' (ty': type 𝔅):
+ ty.(ty_size) = ty'.(ty_size) →
+ typed_instr E L +[p ◁ box ty; p' ◁ ty'] (p <- p') (λ _, +[p ◁ box ty'])
+ (λ post '-[_; b], post -[b]).
Proof.
- intros Eq ?.
- eapply (type_assign_instr _ τ _ _ _ _ (λ _ p, p)).
- rewrite /box Eq. solve_typing.
- eapply resolve'_just, resolve_just.
+ move=> Eq. rewrite /box Eq.
+ eapply (type_assign_instr _ _ _ _ _ _ (λ _ post, post));
+ [solve_typing|eapply resolve'_just, resolve_just].
Qed.
- Lemma ty_assgn_bor_mut {𝔄} E L κ (τ : type 𝔄) p p' :
+ Lemma ty_uniq_ref_write {𝔄} E L κ (ty: type 𝔄) p p' :
lctx_lft_alive E L κ →
- typed_instr E L +[p ◁ &uniq{κ} τ; p' ◁ τ] (p <- p') (λ _, +[p ◁ &uniq{κ} τ])
- (λ post '-[a; b], post -[(b, a.2)] ).
- Proof.
- intros ?.
- eapply (type_assign_instr (&uniq{κ} τ) τ (&uniq{κ} τ) τ fst (λ v w, (w, v.2)) (λ _ p, p)).
- solve_typing. eapply resolve'_just, resolve_just.
- Qed.
-
- Lemma ty_deref_bor_mut_copy {𝔄} E L κ (τ : type 𝔄) p :
- lctx_lft_alive E L κ → Copy τ → τ.(ty_size) = 1%nat →
- typed_instr E L +[p ◁ &uniq{κ} τ] (!p) (λ x, +[x ◁ τ; p ◁ &uniq{κ} τ])
- (λ post '-[a], post -[a.1; a] ).
+ typed_instr E L +[p ◁ &uniq{κ} ty; p' ◁ ty] (p <- p')
+ (λ _, +[p ◁ &uniq{κ} ty]) (λ post '-[aa; b], post -[(b, aa.2)] ).
Proof.
- intros ???.
- eapply type_deref_instr; [solve_typing| solve_typing].
+ move=> ?. eapply (type_assign_instr (&uniq{κ} ty) ty (&uniq{κ} ty) ty
+ fst (λ v w, (w, v.2)) (λ _ post, post)); [solve_typing|].
+ eapply resolve'_just, resolve_just.
Qed.
- Notation "drop: x" := (Skip)%E (at level 102, x at level 1) : expr_scope.
+ Lemma ty_uniq_ref_read {𝔄} E L κ (ty: type 𝔄) p :
+ lctx_lft_alive E L κ → Copy ty → ty.(ty_size) = 1%nat →
+ typed_instr E L +[p ◁ &uniq{κ} ty] (!p)
+ (λ x, +[x ◁ ty; p ◁ &uniq{κ} ty]) (λ post '-[aa], post -[aa.1; aa] ).
+ Proof. move=> ???. eapply type_deref_instr; solve_typing. Qed.
- Lemma ty_resolve {𝔄} E L (τ : type 𝔄) κ p :
- lctx_lft_alive E L κ →
- typed_instr E L +[p ◁ &uniq{κ} τ] (drop: p) (λ _, +[])
- (λ post '-[a], a.2 = a.1 → post -[]).
- Proof. intros ?. eapply type_resolve_instr.
- eapply resolve_impl. solve_typing.
- move => [? ?] //=.
+ Lemma ty_uniq_ref_bye {𝔄} E L (ty: type 𝔄) κ p :
+ lctx_lft_alive E L κ →
+ typed_instr E L +[p ◁ &uniq{κ} ty] (drop: p) (λ _, +[])
+ (λ post '-[aa], aa.2 = aa.1 → post -[]).
+ Proof.
+ move=> ?. eapply type_resolve_instr. eapply resolve_impl; [solve_typing|].
+ by case.
Qed.
- Notation "let: x := &mut{ κ } p 'in' e" := (let: x := p in e)%E
- (at level 102, x at level 1, e at level 150) : expr_scope.
-
- Lemma ty_borrow {𝔄 𝔄l ℭ} E L (C : cctx ℭ) (T : tctx 𝔄l) (τ : type 𝔄) p x e κ tr:
- Closed (x :b: []) e → elctx_sat E L (ty_outlives_E τ κ) →
- (∀v: val, typed_body E L C (v ◁ &uniq{κ} τ +:: p ◁{κ} box τ +:: T) (subst' x v e) tr) -∗
- typed_body E L C (p ◁ box τ +:: T) (let: x := &mut{κ} p in e)
- (λ post '(a -:: t), (∀ a', tr post ((a, a') -:: a' -:: t)) : Prop).
+ Lemma ty_uniq_bor {𝔄 𝔄l ℭ} E L (C: cctx ℭ) (T: tctx 𝔄l) (ty: type 𝔄) p x e κ tr:
+ Closed (x :b: []) e → elctx_sat E L (ty_outlives_E ty κ) →
+ (∀v: val, typed_body E L C
+ (v ◁ &uniq{κ} ty +:: p ◁{κ} box ty +:: T) (subst' x v e) tr) -∗
+ typed_body E L C (p ◁ box ty +:: T) (let: x := &uniq{κ} p in e)
+ (λ post '(a -:: t), (∀ a', tr post ((a, a') -:: a' -:: t)))%type.
Proof.
- iIntros (??) "H". via_tr_impl.
- iApply typed_body_tctx_incl.
- eapply (tctx_incl_app +[_] +[_; _] T T _ id), tctx_incl_refl.
- eapply tctx_borrow; [done].
- iApply (type_let' +[_]); [eapply type_path_instr| done].
- rewrite /trans_app => ? [? ?] //=.
+ iIntros (??) "?". via_tr_impl.
+ { iApply typed_body_tctx_incl.
+ { eapply (tctx_incl_frame_r +[_]). by eapply tctx_borrow. }
+ iApply type_letpath; [solve_typing|done]. }
+ by move=> ?[??].
Qed.
End rules.
\ No newline at end of file
--
GitLab