parametricity.v 2.1 KB
Newer Older
Ralf Jung's avatar
Ralf Jung committed
1
From solutions Require Export safety.
2

Ralf Jung's avatar
Ralf Jung committed
3
(** * Parametricity *)
4
5
6
Section parametricity.
  Context `{!heapG Σ}.

Ralf Jung's avatar
Ralf Jung committed
7
  (** * The polymorphic identity function *)
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's avatar
Ralf Jung committed
25
  (** * Exercise (empty_type_param, easy) *)
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's avatar
Ralf Jung committed
32
  (** * Exercise (boolean_param, moderate) *)
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's avatar
Ralf Jung committed
38
  (** * Exercise (nat_param, hard) *)
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's avatar
Ralf Jung committed
45
  (** * Exercise (strong_nat_param, hard) *)
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.