forked from blanchette/logical_verification_2021
-
Notifications
You must be signed in to change notification settings - Fork 1
/
Copy pathlove01_definitions_and_statements_exercise_solution.lean
165 lines (123 loc) · 6.32 KB
/
love01_definitions_and_statements_exercise_solution.lean
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
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
import .love01_definitions_and_statements_demo
/-! # LoVe Exercise 1: Definitions and Statements
Replace the placeholders (e.g., `:= sorry`) with your solutions. -/
set_option pp.beta true
set_option pp.generalized_field_notation false
namespace LoVe
/-! ## Question 1: Truncated Subtraction
1.1. Define the function `sub` that implements truncated subtraction on natural
numbers by recursion. "Truncated" means that results that mathematically would
be negative are represented by 0. For example:
`sub 7 2 = 5`
`sub 2 7 = 0` -/
def sub : ℕ → ℕ → ℕ
| m 0 := m
| 0 _ := 0
| (nat.succ m) (nat.succ n) := sub m n
/-! 1.2. Check that your function works as expected. -/
#eval sub 0 0 -- expected: 0
#eval sub 0 1 -- expected: 0
#eval sub 0 7 -- expected: 0
#eval sub 1 0 -- expected: 1
#eval sub 1 1 -- expected: 0
#eval sub 3 0 -- expected: 3
#eval sub 2 7 -- expected: 0
#eval sub 3 1 -- expected: 2
#eval sub 3 3 -- expected: 0
#eval sub 3 7 -- expected: 0
#eval sub 7 2 -- expected: 5
/-! ## Question 2: Arithmetic Expressions
Consider the type `aexp` from the lecture and the function `eval` that
computes the value of an expression. You will find the definitions in the file
`love01_definitions_and_statements_demo.lean`. One way to find them quickly is
to
1. hold the Control (on Linux and Windows) or Command (on macOS) key pressed;
2. move the cursor to the identifier `aexp` or `eval`;
3. click the identifier. -/
#check aexp
#check eval
/-! 2.1. Test that `eval` behaves as expected. Make sure to exercise each
constructor at least once. You can use the following environment in your tests.
What happens if you divide by zero?
Make sure to use `#eval`. For technical reasons, `#reduce` does not work well
here. Note that `#eval` (Lean's evaluation command) and `eval` (our evaluation
function on `aexp`) are unrelated. -/
def some_env : string → ℤ
| "x" := 3
| "y" := 17
| _ := 201
#eval eval some_env (aexp.var "x") -- expected: 3
#eval eval some_env (aexp.num 12) -- expected: 12
#eval eval some_env (aexp.add (aexp.var "x") (aexp.var "y")) -- expected: 20
#eval eval some_env (aexp.sub (aexp.num 5) (aexp.var "y")) -- expected: -12
#eval eval some_env (aexp.mul (aexp.num 11) (aexp.var "z")) -- expected: 2211
#eval eval some_env (aexp.div (aexp.num 2) (aexp.num 0)) -- expected: 0
/-! 2.2. The following function simplifies arithmetic expressions involving
addition. It simplifies `0 + e` and `e + 0` to `e`. Complete the definition so
that it also simplifies expressions involving the other three binary
operators. -/
def simplify : aexp → aexp
| (aexp.add (aexp.num 0) e₂) := simplify e₂
| (aexp.add e₁ (aexp.num 0)) := simplify e₁
| (aexp.sub e₁ (aexp.num 0)) := simplify e₁
| (aexp.mul (aexp.num 0) e₂) := aexp.num 0
| (aexp.mul e₁ (aexp.num 0)) := aexp.num 0
| (aexp.mul (aexp.num 1) e₂) := simplify e₂
| (aexp.mul e₁ (aexp.num 1)) := simplify e₁
| (aexp.div (aexp.num 0) e₂) := aexp.num 0
| (aexp.div e₁ (aexp.num 0)) := aexp.num 0
| (aexp.div e₁ (aexp.num 1)) := simplify e₁
-- catch-all cases below
| (aexp.num i) := aexp.num i
| (aexp.var x) := aexp.var x
| (aexp.add e₁ e₂) := aexp.add (simplify e₁) (simplify e₂)
| (aexp.sub e₁ e₂) := aexp.sub (simplify e₁) (simplify e₂)
| (aexp.mul e₁ e₂) := aexp.mul (simplify e₁) (simplify e₂)
| (aexp.div e₁ e₂) := aexp.div (simplify e₁) (simplify e₂)
/-! 2.3. Is the `simplify` function correct? In fact, what would it mean for it
to be correct or not? Intuitively, for `simplify` to be correct, it must
return an arithmetic expression that yields the same numeric value when
evaluated as the original expression.
Given an environment `env` and an expression `e`, state (without proving it)
the property that the value of `e` after simplification is the same as the
value of `e` before. -/
lemma simplify_correct (env : string → ℤ) (e : aexp) :
eval env (simplify e) = eval env e :=
sorry
/-! ## Question 3: λ-Terms
3.1. Complete the following definitions, by replacing the `sorry` markers by
terms of the expected type.
Hint: A procedure for doing so systematically is described in Section 1.1.4 of
the Hitchhiker's Guide. As explained there, you can use `_` as a placeholder
while constructing a term. By hovering over `_`, you will see the current
logical context. -/
def I : α → α :=
λa, a
def K : α → β → α :=
λa b, a
def C : (α → β → γ) → β → α → γ :=
λg b a, g a b
def proj_1st : α → α → α :=
λx y, x
/-! Please give a different answer than for `proj_1st`. -/
def proj_2nd : α → α → α :=
λx y, y
def some_nonsense : (α → β → γ) → α → (α → γ) → β → γ :=
λg a f b, g a b
/-! 3.2. Show the typing derivation for your definition of `C` above, on paper
or using ASCII or Unicode art. You might find the characters `–` (to draw
horizontal bars) and `⊢` useful. -/
/-! Let `D` := `g : α → β → γ, b : β, a : α`. We have
–––––––––––––––––– Var –––––––––– Var
D ⊢ g : α → β → γ D ⊢ a : α
–––––––––––––––––––––––––––––––––––– App –––––––––– Var
D ⊢ g a : β → γ D ⊢ b : β
–––––––––––––––––––––––––––––––––––––––––––––––––––––– App
D ⊢ g a b : γ
–––––––––––––––––––––––––––––––––––––––––––--- Lam
g : α → β → γ, b : β ⊢ (λa : α, g a b) : α → γ
––––––––––––––––––––––––––––––––––––––––––––––------- Lam
g : α → β → γ ⊢ (λ(b : β) (a : α), g a b) : β → α → γ
–––––––––––––––––––––––––––––––––––––––––––––––---------------------- Lam
⊢ (λ(g : α → β → γ) (b : β) (a : α), g a b) : (α → β → γ) → β → α → γ -/
end LoVe