ifr exam

Last updated on January 15, 2024 pm

Questions can be found here and some Lean code can be found here.

Q1

a.

  1. P ↔ Q := P → Q ∧ Q → P
  2. ¬ P := P → false

b.

1
2
¬ (P ∨ Q) ↔ ¬ P ∧ ¬ Q
¬ (P ∧ Q) ↔ ¬ P ∨ ¬ Q

¬ (P ∧ Q) → ¬ P ∨ ¬ Q is not provable in intuitionistic logic.

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
theorem dmg1: ¬ (P ∨ Q) ↔ ¬ P ∧ ¬ Q :=
begin
  constructor,
  assume npq,
  constructor,
  assume p,
  apply npq,
  left,
  assumption,
  assume q,
  apply npq,
  right,
  assumption,
  assume npnq,
  cases npnq with np nq,
  assume pq,
  cases pq with p q,
  apply np,
  exact p,
  apply nq,
  exact q,
end

open classical

theorem dmg2: ¬ (P ∧ Q) ↔ ¬ P ∨ ¬ Q :=
begin
  constructor,
  assume npq,
  cases (em P) with p np,
  right,
  assume q,
  apply npq,
  constructor,
  exact p,
  assumption,
  left,
  exact np,

  assume npnq,
  assume pq,
  cases pq with p q,
  cases npnq with np nq,
  apply np,
  exact p,
  apply nq,
  exact q,
end

c.

  1. No
  2. No
  3. No
  4. Yes
  5. Yes
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
theorem q1c1 : P → (Q ∧ R) ↔ (P → Q) ∧ (P → R) :=
begin
  constructor,
  assume pqr,
  constructor,
  sorry,
  sorry,

  assume pqpr,
  cases pqpr with pq pr,
  assume p,
  constructor,
  apply pq,
  assumption,
  apply pr,
  assumption,
end

theorem q1c2 : (P ∧ Q) → R ↔ (P → R) ∧ (Q → R) :=
begin
  constructor,
  assume pqr,
  constructor,
  assume p,
  apply pqr,
  constructor,
  assumption,
  sorry,
  assume q,
  apply pqr,
  constructor,
  sorry,
  assumption,

  assume prqr,
  assume pq,
  cases prqr with pr qr,
  cases pq with p q,
  apply pr,
  exact p,
end

theorem q1c3 : P → (Q ∨ R) ↔ (P → Q) ∨ (P → R) :=
begin
  constructor,
  assume pqr,
  left,
  assume p,
  sorry,

  assume pqpr,
  assume p,
  cases pqpr with pq pr,
  left,
  apply pq,
  assumption,
  right,
  apply pr,
  assumption,
end

theorem q1c4 : (P ∨ Q) → R ↔ (P → R) ∧ (Q → R) :=
begin
  constructor,
  assume pqr,
  constructor,
  assume p,
  apply pqr,
  left,
  assumption,
  assume q,
  apply pqr,
  right,
  assumption,

  assume prqr,
  cases prqr with pr qr,
  assume pq,
  cases pq with p q,
  apply pr,
  exact p,
  apply qr,
  exact q,
end

theorem q1c5 : (P ∨ Q) → R ↔ (P → R) ∧ (Q → R) :=
begin
  constructor,
  assume pqr,
  constructor,
  assume p,
  apply pqr,
  left,
  assumption,
  assume q,
  apply pqr,
  right,
  assumption,

  assume prqr,
  cases prqr with pr qr,
  assume pq,
  cases pq with p q,
  apply pr,
  exact p,
  apply qr,
  exact q,
end

d.

1
2
3
4
5
6
7
8
9
theorem neg_raa : ¬ ¬ ¬ P → ¬ P :=
begin
  assume nnnp,
  assume p,
  apply nnnp,
  assume np,
  apply np,
  assumption,
end

Q2

a.

refl or reflexivity

rewrite or rewrite←

b.

1
2
3
4
5
6
7
8
9
10
11
12
13
14
-- (i)
theorem q2b1 : ∀ x : People, ∃ y : People, Loves x y := sorry

-- (ii)
theorem q2b2 : ∃ y : People, ∀ x : People, Loves x y := sorry

-- (iii)
theorem q2b3 : ∀ x y z : People, ¬ ((Loves x y) ∧ (Loves y z) → Loves x z) := sorry

-- (iv)
theorem q2b4 : ∃ x : People, ∀ y : People, ¬ (Loves x y) := sorry

-- (v)
theorem q2b5 : ∀ x y : People, ¬ (Loves x y → Loves y x) := sorry

c.

1
2
(∃ x : A, true)
(∀ x : A, false)

Q3

a.

1
2
3
4
def implb : bool → bool → bool
| x tt := tt
| tt _ := ff
| ff _ := tt
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
theorem q3a : ∀ x y : bool, (x = tt) → (y = tt) ↔ implb x y = tt :=
begin
  assume x y,
  constructor,
  assume xtyt,
  cases y,
  cases x,
  dsimp [implb],
  refl,
  dsimp [implb],
  apply xtyt,
  refl,
  cases x,
  dsimp [implb],
  refl,
  dsimp [implb],
  refl,
  assume ixyt,
  assume xt,
  rewrite xt at ixyt,
  cases y,
  dsimp [implb] at ixyt,
  exact ixyt,
  refl,
end

b.

# Provable Provable on negation
(i) ✅ ❎
(ii) ❎ ✅
(iii) ✅ ❎
(iv) ❎ ✅ 
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

theorem q3b1 : ∀ x : bool, ∃ y : bool , x ≠ y :=
begin
  assume x,
  cases x,
  existsi tt,
  assume eq,
  cases eq,
  existsi ff,
  assume eq,
  cases eq,
end

theorem q3b2_neg : ¬ (∃ x : bool, ∀ y : bool , x ≠ y) :=
begin
  assume h,
  cases h with a b,
  cases a,
  have f: ff ≠ ff,
  apply b,
  apply f,
  refl,

  have t: tt ≠ tt,
  apply b,
  apply t,
  refl,
end

theorem q3b3 : ∀ x : bool, ∃ y : bool, x = y :=
begin
  assume x,
  existsi x,
  refl,
end

theorem q3b4_neg : ¬ (∃ x : bool, ∀ y : bool, x = y) :=
begin
  assume h,
  cases h with a b,
  cases a,
  have f: ff = tt,
  apply b,
  contradiction,

  have t: tt = ff,
  apply b,
  contradiction,
end

c.

1
2
3
4
5
6
7
foo 4
= foo (succ (succ 2))
= succ (succ (foo 2))
= succ (succ (foo (succ (succ 0))))
= succ (succ (succ (succ (foo 0))))
= succ (succ (succ (succ 1)))
= 5
1
2
3
4
5
6
7
foo 5
= foo (succ (succ 3))
= succ (succ (foo 3))
= succ (succ (succ (succ (foo 1))))
= succ (succ (succ (succ (foo (succ 0)))))
= succ (succ (succ (succ 0)))
= 4

1.

ifr exam
https://lingkang.dev/2024/01/15/ifr_exam/
Author
Lingkang
Posted on
January 15, 2024
Licensed under