1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
|
Require Import Parametricity.
(** Separate compilation: *)
Parametricity nat as test.
Require List.
Parametricity Recursive List.rev.
Check rev_R.
(** Module translation *)
Module A.
Definition t := nat.
Module B.
Definition t := nat -> nat.
End B.
End A.
Parametricity Recursive bool.
Parametricity Module A.
Print Module A_R.
Print Module A_R.B_R.
(* Parametricity Module Bool. *)
(* Print Module Bool_R. *)
(** Unary parametricity *)
Parametricity Translation (forall X, X -> X) as ID_R arity 1.
Lemma ID_unique:
forall f, ID_R f -> forall A x, f A x = x.
intros f f_R A x.
specialize (f_R A (fun y => y = x) x).
apply f_R.
reflexivity.
Defined.
Parametricity nat arity 10.
Print nat_R_10.
Set Universe Polymorphism.
(** Realizing axioms and section variables. *)
Section Test.
Variable A : Set.
Variable R : A -> A -> Set.
Realizer A as A_R := R.
Definition id : A -> A := fun x => x.
Parametricity id.
End Test.
(** Opaque terms. **)
Require ProofIrrelevance.
Lemma opaque : True.
trivial.
Qed.
Parametricity Recursive opaque.
Eval compute in opaque.
Eval compute in opaque_R.
Lemma opaqueunit : unit.
exact tt.
Qed.
(*
Fail Parametricity Recursive opaqueunit.
DepRefs:
opaqueunit
Vernac Interpreter Executing command
Anomaly: Uncaught exception Not_found. Please report at
destruct opaqueunit.
reflexivity.
Parametricity Done.
*)
|
