parametricity.v 2.1 KB
 Ralf Jung committed Jan 20, 2020 1 ``````From solutions Require Export safety. `````` Ralf Jung committed Jan 20, 2020 2 `````` `````` Ralf Jung committed Jan 20, 2020 3 ``````(** * Parametricity *) `````` Ralf Jung committed Jan 20, 2020 4 5 6 ``````Section parametricity. Context `{!heapG Σ}. `````` Ralf Jung committed Jan 20, 2020 7 `````` (** * The polymorphic identity function *) `````` Ralf Jung committed Jan 20, 2020 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 `````` Lemma identity_param `{!heapPreG Σ} e (v : val) σ w es σ' : (∀ `{!heapG Σ}, (∅ ⊨ e : ∀ A, A → A)%I) → rtc erased_step ([e <_> v]%E, σ) (of_val w :: es, σ') → w = v. Proof. intros He. apply sem_gen_type_safety with (φ := λ u, u = v)=> ?. pose (T := SemTy (λ w, ⌜w = v⌝)%I : sem_ty Σ). exists T. split. { by iIntros (?) "?". } iIntros (vs) "!# #Hvs". iPoseProof (He with "Hvs") as "He /=". wp_apply (wp_wand with "He"). iIntros (u) "#Hu". iSpecialize ("Hu" \$! T). wp_apply (wp_wand with "Hu"). iIntros (w') "Hw'". by iApply "Hw'". Qed. `````` Ralf Jung committed Jan 20, 2020 25 `````` (** * Exercise (empty_type_param, easy) *) `````` Ralf Jung committed Jan 20, 2020 26 27 28 29 30 31 `````` Lemma empty_type_param `{!heapPreG Σ} e (v : val) σ w es σ' : (∀ `{!heapG Σ}, (∅ ⊨ e : ∀ A, A)%I) → rtc erased_step ([e <_>]%E, σ) (of_val w :: es, σ') → False. Proof. (* FILL IN YOUR PROOF *) Qed. `````` Ralf Jung committed Jan 20, 2020 32 `````` (** * Exercise (boolean_param, moderate) *) `````` Ralf Jung committed Jan 20, 2020 33 34 35 36 37 `````` Lemma boolean_param `{!heapPreG Σ} e (v1 v2 : val) σ w es σ' : (∀ `{!heapG Σ}, (∅ ⊨ e : ∀ A, A → A → A)%I) → rtc erased_step ([e <_> v1 v2]%E, σ) (of_val w :: es, σ') → w = v1 ∨ w = v2. Proof. (* FILL IN YOUR PROOF *) Qed. `````` Ralf Jung committed Jan 20, 2020 38 `````` (** * Exercise (nat_param, hard) *) `````` Ralf Jung committed Jan 20, 2020 39 40 41 42 43 44 `````` Lemma nat_param `{!heapPreG Σ} e σ w es σ' : (∀ `{!heapG Σ}, (∅ ⊨ e : ∀ A, (A → A) → A → A)%I) → rtc erased_step ([e <_> (λ: "n", "n" + #1)%V #0]%E, σ) (of_val w :: es, σ') → ∃ n : nat, w = #n. Proof. (* FILL IN YOUR PROOF *) Qed. `````` Ralf Jung committed Jan 20, 2020 45 `````` (** * Exercise (strong_nat_param, hard) *) `````` Ralf Jung committed Jan 20, 2020 46 47 48 49 50 51 52 53 54 `````` Lemma strong_nat_param `{!heapPreG Σ} e σ w es σ' (vf vz : val) φ : (∀ `{!heapG Σ}, ∃ Φ : sem_ty Σ, (∅ ⊨ e : ∀ A, (A → A) → A → A)%I ∧ (∀ w, {{{ Φ w }}} vf w {{{ w', RET w'; Φ w' }}})%I ∧ (Φ vz)%I ∧ (∀ w, Φ w -∗ ⌜φ w⌝)%I) → rtc erased_step ([e <_> vf vz]%E, σ) (of_val w :: es, σ') → φ w. Proof. (* FILL IN YOUR PROOF *) Qed. End parametricity.``````