-
Notifications
You must be signed in to change notification settings - Fork 13
/
Copy pathhw03.v
152 lines (105 loc) · 4.55 KB
/
hw03.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
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
From mathcomp Require Import ssreflect ssrfun ssrbool.
(** Prove the following lemmas by providing explicit proof terms.
A bunch of exercises from the previous seminar we didn't have time
to cover have made it to this homework :) *)
(* An (unsound) placeholder so that the whole file typechecks.
Please replace it with your proof term. Your solutions may not
use any axioms, including `replace_with_your_solution_here` *)
Axiom replace_with_your_solution_here : forall {A : Type}, A.
Section Logic.
Variables A B C : Prop.
(** * Exercise *)
Definition notTrue_iff_False : (~ True) <-> False
:= replace_with_your_solution_here.
(* Hint 1: use [Locate "<->".] and [Print iff.] commands to understand better
the type above. *)
(* Hint 2: If you are experiencing an error like the following one
"Found a matching with no clauses on a term unknown to have an empty inductive type." try adding explicit type annotations to functional parameters or
use `match <term> in <type> with ... end` instead of `match <term> with ... end` *)
(** * Exercise: double negation elimination works for `False` *)
Definition dne_False : ~ ~ False -> False
:= replace_with_your_solution_here.
(** * Exercise: double negation elimination works for `True` too. *)
Definition dne_True : ~ ~ True -> True
:= replace_with_your_solution_here.
(** * Exercise: Weak Peirce's law
Peirce's law (https://en.wikipedia.org/wiki/Peirce%27s_law) is equivalent to
Double Negation Elimination (and the Law of Excluded Middle too),
so it does not hold in general, but we can prove its weak form. *)
Definition weak_Peirce : ((((A -> B) -> A) -> A) -> B) -> B
:= replace_with_your_solution_here.
(* Hint 1: use let-in expression to break the proof into pieces and solve them independently *)
(* Hint 2: annotate the identifiers of let-expressions with types: [let x : <type> := ... in ...] *)
Variable T : Type.
Variable P Q : T -> Prop.
(** * Exercise: existential introduction rule *)
Definition exists_introduction :
forall (x : T), P x -> (exists (x : T), P x)
:= replace_with_your_solution_here.
(** * Exercise: Frobenius rule: existential quantifiers and conjunctions commute *)
Definition frobenius_rule :
(exists x, A /\ P x) <-> A /\ (exists x, P x)
:= replace_with_your_solution_here.
End Logic.
Section Equality.
Variables A B C D : Type.
(** * Exercise *)
Definition eq1 : true = (true && true)
:= replace_with_your_solution_here.
(** * Exercise *)
Definition eq2 : 42 = (if true then 21 + 21 else 239)
:= replace_with_your_solution_here.
(** * Exercise *)
Definition LEM_decidable :
forall (b : bool), b || ~~ b = true
:= replace_with_your_solution_here.
(** * Exercise *)
Definition if_neg :
forall (A : Type) (b : bool) (vT vF: A),
(if ~~ b then vT else vF) = if b then vF else vT
:= replace_with_your_solution_here.
(** * Exercise : associativity of function composition *)
(** [\o] is a notation for function composition in MathComp, prove that it's associative *)
Definition compA (f : A -> B) (g : B -> C) (h : C -> D) :
(h \o g) \o f = h \o (g \o f)
:= replace_with_your_solution_here.
(** [=1] stands for extensional equality on unary functions,
i.e. [f =1 g] means [forall x, f x = g x].
This means it's an equivalence relation, i.e. it's reflexive, symmetric and transitive.
Let us prove a number of facts about [=1]. *)
(** * Exercise: Reflexivity *)
Definition eqext_refl :
forall (f : A -> B), f =1 f
:= replace_with_your_solution_here.
(** * Exercise: Symmetry *)
Definition eqext_sym :
forall (f g : A -> B), f =1 g -> g =1 f
:= replace_with_your_solution_here.
(** * Exercise: Transitivity *)
Definition eqext_trans :
forall (f g h : A -> B), f =1 g -> g =1 h -> f =1 h
:= replace_with_your_solution_here.
(** * Exercise: left congruence *)
Definition eq_compl :
forall (f g : A -> B) (h : B -> C),
f =1 g -> h \o f =1 h \o g
:= replace_with_your_solution_here.
(** * Exercise: right congruence *)
Definition eq_compr :
forall (f g : B -> C) (h : A -> B),
f =1 g -> f \o h =1 g \o h
:= replace_with_your_solution_here.
End Equality.
(** * Extra exercises (feel free to skip) *)
From mathcomp Require Import ssreflect ssrfun ssrbool eqtype.
(* After importing `eqtype` you need to either use a qualified name for
`eq_refl`: `Logic.eq_refl`, or use the `erefl` notation.
This is because `eqtype` reuses the `eq_refl` identifier for a
different lemma.
*)
Definition iff_is_if_and_only_if :
forall a b : bool, (a ==> b) && (b ==> a) = (a == b)
:= replace_with_your_solution_here.
Definition negbNE :
forall b : bool, ~~ ~~ b = true -> b = true
:= replace_with_your_solution_here.