-
Notifications
You must be signed in to change notification settings - Fork 6
/
Copy pathAssignment07_00.v
104 lines (84 loc) · 2.8 KB
/
Assignment07_00.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
Require Export SfLib.
(* Important:
- You are NOT allowed to use the [admit] tactic
because [admit] simply admits any goal
regardless of whether it is provable or not.
But, you can leave [admit] for problems that you cannot prove.
Then you will get zero points for those problems.
- You are ALLOWED to use any tactics including.
[tauto], [intuition], [firstorder], [omega].
- Do NOT add any additional `Require Import/Export`.
*)
Inductive aexp : Type :=
| ANum : nat -> aexp
| APlus : aexp -> aexp -> aexp
| AMinus : aexp -> aexp -> aexp
| AMult : aexp -> aexp -> aexp.
Inductive bexp : Type :=
| BTrue : bexp
| BFalse : bexp
| BEq : aexp -> aexp -> bexp
| BLe : aexp -> aexp -> bexp
| BNot : bexp -> bexp
| BAnd : bexp -> bexp -> bexp.
Fixpoint aeval (a : aexp) : nat :=
match a with
| ANum n => n
| APlus a1 a2 => (aeval a1) + (aeval a2)
| AMinus a1 a2 => (aeval a1) - (aeval a2)
| AMult a1 a2 => (aeval a1) * (aeval a2)
end.
Fixpoint beval (b : bexp) : bool :=
match b with
| BTrue => true
| BFalse => false
| BEq a1 a2 => beq_nat (aeval a1) (aeval a2)
| BLe a1 a2 => ble_nat (aeval a1) (aeval a2)
| BNot b1 => negb (beval b1)
| BAnd b1 b2 => andb (beval b1) (beval b2)
end.
Fixpoint optimize_0plus (a:aexp) : aexp :=
match a with
| ANum n =>
ANum n
| APlus (ANum 0) e2 =>
optimize_0plus e2
| APlus e1 e2 =>
APlus (optimize_0plus e1) (optimize_0plus e2)
| AMinus e1 e2 =>
AMinus (optimize_0plus e1) (optimize_0plus e2)
| AMult e1 e2 =>
AMult (optimize_0plus e1) (optimize_0plus e2)
end.
Reserved Notation "e '||' n" (at level 50, left associativity).
Inductive aevalR : aexp -> nat -> Prop :=
| E_ANum : forall (n:nat),
(ANum n) || n
| E_APlus : forall (e1 e2: aexp) (n1 n2 : nat),
(e1 || n1) -> (e2 || n2) -> (APlus e1 e2) || (n1 + n2)
| E_AMinus : forall (e1 e2: aexp) (n1 n2 : nat),
(e1 || n1) -> (e2 || n2) -> (AMinus e1 e2) || (n1 - n2)
| E_AMult : forall (e1 e2: aexp) (n1 n2 : nat),
(e1 || n1) -> (e2 || n2) -> (AMult e1 e2) || (n1 * n2)
where "e '||' n" := (aevalR e n) : type_scope.
Tactic Notation "aevalR_cases" tactic(first) ident(c) :=
first;
[ Case_aux c "E_ANum" | Case_aux c "E_APlus"
| Case_aux c "E_AMinus" | Case_aux c "E_AMult" ].
Theorem aeval_iff_aevalR : forall a n,
(a || n) <-> aeval a = n.
Proof.
(* WORKED IN CLASS *)
split.
Case "->".
intros H; induction H; subst; reflexivity.
Case "<-".
generalize dependent n.
induction a; simpl; intros; subst; constructor;
try apply IHa1; try apply IHa2; reflexivity.
Qed.
Definition state := id -> nat.
Definition empty_state : state :=
fun _ => 0.
Definition update (st : state) (x : id) (n : nat) : state :=
fun x' => if eq_id_dec x x' then n else st x'.