-
Notifications
You must be signed in to change notification settings - Fork 9
/
Copy pathprod_rect.v
135 lines (100 loc) · 3.58 KB
/
prod_rect.v
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
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
From Ornamental Require Import Ornaments.
Require Import Infrastructure.
Set DEVOID search prove equivalence.
Set DEVOID lift type.
Set Nonrecursive Elimination Schemes.
(*
* This code is a minimized example from @ptival, which I use as a regression test
* to make sure projections aren't expanded and left as applications of prod_rect,
* and that projections/accessors lift to accessors/projections.
*
* The proofs here are purposely brittle, since they should break if the terms are not _exactly_ syntactically equal.
*)
Module Pairs.
Definition profile : Type := (bool * nat).
Definition page : Type := (nat * (nat * (bool * ((bool * nat) * nat)))).
Definition visible (pr : profile) (pa : page) : bool :=
andb (fst pr) (fst (snd (snd pa))).
End Pairs.
Preprocess Module Pairs as Pairs_PP { opaque andb }.
Module Records.
Record Profile :=
{
public : bool;
age : nat;
}.
Definition is_public (pr : Pairs.profile) : bool := fst pr.
Definition get_age (pr : Pairs.profile) : nat := snd pr.
End Records.
Preprocess Module Records as Records_PP.
Lift Records_PP.Profile Pairs_PP.profile in Records_PP.public as is_public.
Lift Pairs_PP.profile Records_PP.Profile in Records_PP.is_public as public.
Definition is_public_expected (h : Pairs_PP.profile) :=
Prod.fst _ _ h.
Lemma test_is_public:
is_public = is_public_expected.
Proof.
unfold is_public, is_public_expected.
test_exact_equality.
Qed.
Lemma test_public:
public = fun h => Records_PP.public h.
Proof.
unfold public.
test_exact_equality.
Qed.
Lift Records_PP.Profile Pairs_PP.profile in Records_PP.age as get_age.
Lift Pairs_PP.profile Records_PP.Profile in Records_PP.get_age as age.
Definition get_age_expected (h : Pairs_PP.profile) :=
Prod.snd _ _ h.
Lemma test_get_h_n:
get_age = get_age_expected.
Proof.
unfold get_age, get_age_expected.
test_exact_equality.
Qed.
Lemma testGetHN:
age = fun (h : Records_PP.Profile) => Records_PP.age h.
Proof.
unfold age.
test_exact_equality.
Qed.
Lift Pairs_PP.profile Records_PP.Profile in Pairs_PP.visible as visible_PP { opaque andb }.
Definition visible_PP_expected (pr : Records_PP.Profile) (pa : nat * (nat * (bool * (Records_PP.Profile * nat)))) : bool :=
Records_PP.public pr
&&
Pairs_PP.Coq_Init_Datatypes_fst bool (Records_PP.Profile * nat)
(Pairs_PP.Coq_Init_Datatypes_snd nat (bool * (Records_PP.Profile * nat))
(Pairs_PP.Coq_Init_Datatypes_snd nat (nat * (bool * (Records_PP.Profile * nat))) pa)).
Lemma test_visible_PP:
visible_PP = visible_PP_expected.
Proof.
unfold visible_PP, visible_PP_expected.
test_exact_equality.
Qed.
Module MoreRecords.
Record Page :=
{
friends : nat;
groups : nat;
active : bool;
profile : Records_PP.Profile;
photos : nat;
}.
(* We'd like to wrap the ugly access into this: *)
Definition is_active (pa : Pairs.page) : bool := fst (snd (snd pa)).
End MoreRecords.
Preprocess Module MoreRecords as MoreRecords_PP.
Lift Pairs_PP.profile Records_PP.Profile in Pairs_PP.page as page_PP.
Lift Pairs_PP.profile Records_PP.Profile in MoreRecords_PP.is_active as active0.
Lift page_PP MoreRecords_PP.Page in active0 as active.
Lift Pairs_PP.profile Records_PP.Profile in Pairs_PP.visible as visible0 { opaque andb }.
Lift page_PP MoreRecords_PP.Page in visible0 as visible { opaque andb }.
Definition visible_expected (pr : Records_PP.Profile) (pa : MoreRecords_PP.Page) : bool :=
(Records_PP.public pr && MoreRecords_PP.active pa)%bool.
Lemma test_visible :
visible = visible_expected.
Proof.
unfold visible, visible_expected.
test_exact_equality.
Qed.