-
Notifications
You must be signed in to change notification settings - Fork 9
/
ProofsOrig.v
121 lines (109 loc) · 3.15 KB
/
ProofsOrig.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
Require Import Prelude.
Require Import CompilerOrig.
Import ListNotations.
(* Alternative proof that goes through, even
with patternFailures in the code.
*)
Lemma comp_correct_helper: forall e s d,
exec (comp e ++ d) s = exec d (eval e :: s).
Proof.
induction e; intros; auto.
simpl.
rewrite <- app_assoc.
rewrite <- app_assoc.
rewrite IHe1.
rewrite IHe2.
simpl.
reflexivity.
Qed.
Theorem comp_correct: forall e,
exec (comp e) [] = [eval e].
Proof.
intros.
replace (comp e) with (comp e ++ []) by apply app_nil_r.
apply comp_correct_helper.
Qed.
(* Anther approach that tries to follow the original code
in the presence of pattenFailure *)
(* Nice, but actually useless: The precondition cannot be
shown for concrete [c] and [s]. *)
(* AKA comp_correct_book *)
Lemma distributivity: forall c s d,
exec c s <> patternFailure ->
exec (c ++ d) s = exec d (exec c s).
Proof.
induction c; intros; auto.
destruct a.
- simpl. rewrite IHc. auto.
simpl in H. auto.
- simpl. destruct s. simpl in H. contradiction.
destruct s. simpl in H. contradiction.
simpl in H.
rewrite IHc.
auto. auto.
Qed.
Axiom bottom_ne_cons : forall A (x : A) xs, (x :: xs) <> patternFailure.
(* COQ8.8 ok? *)
Lemma stack_replace : forall e s s' i j, exec e (s' ++ i :: s) <> patternFailure ->
exec e (s' ++ j :: s) <> patternFailure.
Proof.
induction e; intros; simpl in *; auto.
- destruct s'; simpl; apply bottom_ne_cons.
- destruct a.
+ replace (i0 :: s' ++ j :: s) with ((i0 :: s') ++ j :: s); auto.
apply IHe with (i:=i); auto.
+ destruct s'. simpl in *. destruct s. contradiction.
match goal with
| [ H:_ |- exec ?e ?s <> patternFailure] => rewrite <- (app_nil_l s)
end.
eapply IHe.
simpl. eauto.
simpl in *.
destruct s'. simpl in *.
match goal with
| [ H:_ |- exec ?e ?s <> patternFailure] => rewrite <- (app_nil_l s)
end.
eapply IHe.
simpl. eauto.
simpl in *.
Admitted.
Lemma stack_extend : forall e s i, exec e s <> patternFailure ->
exec e (i :: s) <> patternFailure.
Proof.
induction e; intros.
simpl.
simpl in H.
apply bottom_ne_cons.
destruct a.
- simpl in *.
apply IHe.
eapply stack_replace with (s' := nil). simpl. eauto.
- simpl. destruct s. contradiction.
apply IHe.
simpl in H. destruct s. contradiction.
eapply stack_replace with (s' := nil). simpl. eauto.
Qed.
Lemma stack_extend_app : forall e s s', exec e s <> patternFailure ->
exec e (s' ++ s) <> patternFailure.
Proof.
induction s'. simpl. auto.
intros. simpl.
apply stack_extend. auto.
Qed.
(* We need a precondition to this lemma too. Can't put my finger on it though. *)
Lemma comp_correct_book : forall e s,
exec (comp e) s = eval e :: s.
Proof.
induction e; intros s.
auto.
simpl.
rewrite <- app_assoc.
rewrite distributivity.
rewrite IHe1.
rewrite distributivity.
rewrite IHe2.
simpl.
auto.
admit. (* exec (comp e2) (eval e1 :: s) <> patternFailure *)
admit. (* Cannot prove exec (comp e1) s <> patternFailure *)
Abort.