-
Notifications
You must be signed in to change notification settings - Fork 1
/
HandlersResults.v
118 lines (92 loc) · 2.29 KB
/
HandlersResults.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
Require Import Arith.
Require Import Bool.
Require Import List.
Require Import Handlers.
Require Import HandlersEx.
Open Scope string_scope.
Example runStateComp : reds (outer (runState computation)) expectedResult.
eapply r_step.
eapply frame with (CC:=CC_App _).
eapply handleOp.
tauto.
apply hFor2. discriminate. apply hFor1.
simpl. eapply r_step.
eapply betaApp.
simpl. eapply r_step.
eapply frame with (CC:=CC_App _).
eapply frame with (CC:=CC_App _).
apply betaU.
simpl. eapply r_step.
eapply frame with (CC:=CC_App _).
eapply betaApp.
simpl. eapply r_step.
eapply frame with (CC:=CC_App _).
eapply handleOp.
tauto.
apply hFor1.
simpl. eapply r_step.
apply betaApp.
simpl. eapply r_step.
eapply frame with (CC:=CC_App _).
eapply frame with (CC:=CC_App _).
apply betaU.
simpl. eapply r_step.
eapply frame with (CC:=CC_App _).
eapply betaApp.
simpl. eapply r_step.
eapply frame with (CC:=CC_App _).
eapply handleOp.
tauto.
apply hFor2. discriminate. apply hFor1.
simpl. eapply r_step.
apply betaApp.
simpl. eapply r_step.
eapply frame with (CC:=CC_App _).
eapply frame with (CC:=CC_App _).
apply betaU.
simpl. eapply r_step.
eapply frame with (CC:=CC_App _).
eapply betaApp.
simpl. eapply r_step.
eapply frame with (CC:=CC_App _).
eapply handleOp.
tauto.
apply hFor1.
simpl. eapply r_step.
apply betaApp.
simpl. eapply r_step.
eapply frame with (CC:=CC_App _).
eapply frame with (CC:=CC_App _).
apply betaU.
simpl. eapply r_step.
eapply frame with (CC:=CC_App _).
eapply betaApp.
simpl. eapply r_step.
eapply frame with (CC:=CC_App _).
eapply handleOp.
tauto.
apply hFor2. discriminate. apply hFor1.
simpl. eapply r_step.
apply betaApp.
simpl. eapply r_step.
eapply frame with (CC:=CC_App _).
eapply frame with (CC:=CC_App _).
apply betaU.
simpl. eapply r_step.
eapply frame with (CC:=CC_App _).
eapply betaApp.
simpl. eapply r_step.
eapply frame with (CC:=CC_App _).
eapply handleF.
apply hReturns2. apply hReturns2. apply hReturns1.
simpl. eapply r_step.
apply betaApp.
simpl. apply r_zero.
Qed.
Example nac_bad : needs_alpha_conv bad.
unfold bad.
apply AC_frame with (CC:=CC_Let _ _).
apply AC_frame with (CC:=CC_Handle _).
apply AC_hoistop with (H:=H_Let _ _).
simpl. tauto.
Qed.