blob: 541b910ab13baa7f76d55c091cbf0809285dd879 (
plain) (
blame)
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
|
Inductive Exp (v : Type) :=
| elit : nat -> Exp v
| evar : v -> Exp v
| eadd : Exp v -> Exp v -> Exp v.
Fixpoint eval {v} (env : v -> nat) (e : Exp v) : nat :=
match e with
| elit _ n => n
| evar _ n => env n
| eadd _ a b => eval env a + eval env b
end.
Inductive RPN (v : Type) : nat -> Type :=
| rpnnil : RPN v 0
| rpnlit : forall {n}, RPN v n -> nat -> RPN v (S n)
| rpnvar : forall {n}, RPN v n -> v -> RPN v (S n)
| rpnadd : forall {n}, RPN v (S (S n)) -> RPN v (S n).
Fixpoint rpn_app {v} {n} {m} (a : RPN v n) (b : RPN v m) : RPN v (n+m) :=
match a with
| rpnnil _ => b
| rpnlit _ rest x => rpnlit _ (rpn_app rest b) x
| rpnvar _ rest x => rpnvar _ (rpn_app rest b) x
| rpnadd _ rest => rpnadd _ (rpn_app rest b)
end.
Definition cast: forall {A m} (v: RPN A m) {n}, m = n -> RPN A n.
intros.
rewrite <- H.
exact v.
Defined.
Require Import Coq.Arith.Plus.
Require Import Coq.Program.Equality.
Lemma rpn_app_assoc_jmeq {v} {p} {q} {r} (a : RPN v p) (b : RPN v q) (c : RPN v r) :
rpn_app a (rpn_app b c) ~= rpn_app (rpn_app a b) c.
induction a.
simpl.
reflexivity.
simpl.
Admitted.
Lemma rpn_app_assoc {v} {p} {q} {r} (a : RPN v p) (b : RPN v q) (c : RPN v r) :
rpn_app (rpn_app a b) c = cast (rpn_app a (rpn_app b c)) (plus_assoc _ _ _).
Fixpoint rpn {v} (e : Exp v) : RPN v 1 :=
match e with
| elit _ n => rpnlit _ (rpnnil _) n
| evar _ n => rpnvar _ (rpnnil _) n
| eadd _ a b => rpnadd _ (rpn_app (rpn a) (rpn b))
end.
Require Import Coq.Vectors.VectorDef.
Fixpoint rpn_eval' {v} {n} (env : v -> nat) (rpn : RPN v n) : t nat n.
refine (match rpn with
| rpnnil _ => nil _
| rpnlit _ rest x => cons _ x _ (rpn_eval' _ _ env rest)
| rpnvar _ rest x => cons _ (env x) _ (rpn_eval' _ _ env rest)
| rpnadd _ rest => _
end).
set (recurse := rpn_eval' _ _ env rest).
remember (S (S n0)) as stack_size.
destruct recurse.
discriminate. (* nil case *)
assert (n1 = S n0) by (abstract congruence).
rewrite H in recurse.
exact recurse.
Defined.
Definition rpn_eval {v} (env : v -> nat) (rpn : RPN v 1) : nat :=
match rpn_eval' env rpn with
| cons _ x _ _ => x
| nil _ => 0
end.
Fixpoint exprsize {v} (e : Exp v) : nat :=
match e with
| elit _ _ => 1
| evar _ _ => 1
| eadd _ a b => 1 + exprsize a + exprsize b
end.
Require Import Wellfounded.
Theorem correctness (v : Type) (e : Exp v) : forall env : v -> nat,
forall n rest (results : t nat n),
results = rpn_eval' env rest ->
cons _ (eval env e) _ results = rpn_eval' env (rpn_app (rpn e) rest).
Proof.
induction e using (well_founded_induction
(wf_inverse_image _ nat _ exprsize PeanoNat.Nat.lt_wf_0)).
intros.
destruct e.
simpl; try rewrite <- H0; try reflexivity.
simpl; try rewrite <- H0; try reflexivity.
simpl (rpn (eadd v e1 e2)).
simpl rpn_app.
assert (rpn_app (rpn_app (rpn e1) (rpn e2)) rest = rpn_app (rpn e1) (rpn_app (rpn e2) rest)).
apply rpn_app_assoc.
rewrite (app_assoc_reverse (rev (rpn v e1)) (rev (rpn v e2)) rest).
Qed.
|
