yadunut/nus
1
0
Fork 0
Code Issues Pull Requests Actions Projects Releases Wiki Activity

feat: 3234 week 2

Browse Source
This commit is contained in:
Yadunand Prem 2024-02-04 15:40:50 +08:00
parent 1b606271ef
commit 6482186773
No known key found for this signature in database
7 changed files with 1438 additions and 45 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

47
cs3234/labs/week-01_functional-programming-in-Gallina.v
View File

@ -5,50 +5,6 @@
(* was: *)
(* Version of 18 Jan 2024 *)
(* ********** *)
(* name:
e-mail address:
student number:
*)
(* name:
e-mail address:
student number:
*)
(* name:
e-mail address:
student number:
*)
(* name:
e-mail address:
student number:
*)
(* name:
e-mail address:
student number:
*)
(* name:
e-mail address:
student number:
*)
(* name:
e-mail address:
student number:
*)
(* name:
e-mail address:
student number:
*)
(* ********** *)
Check 0.
Check O.
@ -309,7 +265,8 @@ Definition test_mult (candidate: nat -> nat -> nat) : bool :=
(let x := 5 in
let y := 6 in
let z := 7 in
(Nat.eqb (candidate x (candidate y z)) (candidate z (candidate x y))))
(Nat.eqb (candidate x (candidate y z))
(candidate (candidate x y) z)))
&&
(
(* Testing the inductive step *)

180
cs3234/labs/week-01_polymorphism.v Normal file
View File

@ -0,0 +1,180 @@
(* week-01_polymorphism.v *)
(* LPP 2024 - CS3234 2023-2024, Sem2 *)
(* Olivier Danvy <danvy@yale-nus.edu.sg> *)
(* Version of 18 Jan 2024 *)
(* ********** *)
Require Import Arith Bool.
(* ********** *)
Definition make_pair_v0 : forall (A : Type) (B : Type), A -> B -> A * B :=
fun A B a b => (a, b).
Definition make_pair_v1 (A : Type) : forall B : Type, A -> B -> A * B :=
fun B a b => (a, b).
Definition make_pair_v2 (A : Type) (B : Type) : A -> B -> A * B :=
fun a b => (a, b).
Definition make_pair_v3 (A : Type) (B : Type) (a : A) : B -> A * B :=
fun b => (a, b).
Definition make_pair_v4 (A : Type) (B : Type) (a : A) (b : B) : A * B :=
(a, b).
(* ***** *)
Compute make_pair_v0 nat bool 1 true.
Compute (make_pair_v4 nat bool 1 true).
(* = (1, true) : nat * bool *)
Definition dupl (V : Type) (v : V) : V * V :=
make_pair_v4 V V v v.
(* ********** *)
Inductive polymorphic_binary_tree (V : Type) : Type :=
| PLeaf : V -> polymorphic_binary_tree V
| PNode : polymorphic_binary_tree V -> polymorphic_binary_tree V -> polymorphic_binary_tree V.
Definition test_number_of_leaves (candidate : forall V : Type, polymorphic_binary_tree V -> nat) :=
(candidate bool (PLeaf bool true) =? 1) &&
(candidate nat (PNode nat (PLeaf nat 0) (PLeaf nat 1)) =? 2).
Fixpoint number_of_leaves (V : Type) (t : polymorphic_binary_tree V) : nat :=
match t with
| PLeaf _ v =>
1
| PNode _ t1 t2 =>
number_of_leaves V t1 + number_of_leaves V t2
end.
Compute (test_number_of_leaves number_of_leaves).
(* ********** *)
Fixpoint eqb_polymorphic_binary_tree (V : Type) (eqb_V : V -> V -> bool) (t1 t2 : polymorphic_binary_tree V) : bool :=
match t1 with
| PLeaf _ v1 =>
match t2 with
| PLeaf _ v2 =>
eqb_V v1 v2
| PNode _ t11 t12 =>
false
end
| PNode _ t11 t12 =>
match t2 with
| PLeaf _ v2 =>
false
| PNode _ t21 t22 =>
eqb_polymorphic_binary_tree V eqb_V t11 t21
&&
eqb_polymorphic_binary_tree V eqb_V t12 t22
end
end.
(* ********** *)
Definition eqb_nat := Nat.eqb.
Definition eqb_binary_tree_of_nats (t1 t2 : polymorphic_binary_tree nat) : bool :=
eqb_polymorphic_binary_tree nat eqb_nat t1 t2.
(* ********** *)
(* Exercise 05 *)
Definition e5a : polymorphic_binary_tree (nat * bool) :=
PNode (nat * bool)
(PLeaf (nat * bool) (0, true))
(PLeaf (nat * bool) (1, false))
.
Check e5a.
Compute e5a.
Definition nTree := (polymorphic_binary_tree nat).
Definition e5b : polymorphic_binary_tree (polymorphic_binary_tree nat) :=
PNode (nTree)
(PLeaf (nTree) (PLeaf nat 1))
(PLeaf (nTree) (PLeaf nat 2))
.
Check e5b.
Compute e5b.
(* Exercise 07 *)
Definition eqb_option (V : Type) (eqb_V : V -> V -> bool) (ov1 ov2 : option V) : bool :=
match ov1 with
| Some v1 =>
match ov2 with
| Some v2 =>
eqb_V v1 v2
| None =>
false
end
| None =>
match ov2 with
| Some v =>
false
| None =>
true
end
end.
Check (eqb_polymorphic_binary_tree nat).
Check (eqb_polymorphic_binary_tree (option nat)).
Check (eqb_option (polymorphic_binary_tree nat)).
(*
Definition eqb_binary_tree_of_optional_nats (t1 t2 : polymorphic_binary_tree (option nat)) : bool :=
*)
(*
Definition eqb_optional_binary_tree_of_nats (t1 t2 : option (polymorphic_binary_tree nat)) : bool :=
*)
(*
Definition eqb_optional_binary_tree_of_optional_nats (t1 t2 : option (polymorphic_binary_tree (option nat))) : bool :=
*)
(*
Definition eqb_binary_tree_of_optional_binary_tree_of_nats (t1 t2 : polymorphic_binary_tree (option (polymorphic_binary_tree nat))) : bool :=
*)
(*
Definition eqb_binary_tree_of_optional_binary_tree_of_optional_nats (t1 t2 : polymorphic_binary_tree (option (polymorphic_binary_tree (option nat)))) : bool :=
*)
(* ********** *)
Inductive option' (V : Type) : Type :=
| Some' : V -> option' V
| None' : option' V.
Print option'.
Set Implicit Arguments.
Inductive option'' (V : Type) : Type :=
| Some'' : V -> option'' V
| None'' : option'' V.
Print option''.
Check (Some 10, Some true).
Check (Some' nat 10, Some' bool true).
Check (Some'' 10, Some'' true).
Check None.
Check None'.
Check None''.
Check (@None nat).
Check (@None' nat).
Check (@None'' nat).
(* ********** *)
(* end of week-01_polymorphism.v *)

215
cs3234/labs/week-02_exercises.v Normal file
View File

@ -0,0 +1,215 @@
(* week-02_exercises.v *)
(* LPP 2024 - CS3234 2023-2024, Sem2 *)
(* Olivier Danvy <danvy@yale-nus.edu.sg> *)
(* Version of 25 Jan 2024 *)
(* ********** *)
(* Exercises about types: *)
Definition ta : forall A : Type, A -> A * A :=
fun (A: Type) (a: A) => (a, a).
Definition tb : forall A B : Type, A -> B -> A * B :=
fun (A B: Type) (a: A) (b: B) => (a, b).
Definition tc : forall A B : Type, A -> B -> B * A :=
fun (A B: Type) (a: A) (b: B) => (b, a).
Check (tt : unit).
Definition td : forall (A : Type), (unit -> A) -> A :=
fun (A : Type) (f: unit -> A) => f tt.
Definition te : forall A B : Type, (A -> B) -> A -> B :=
fun (A B : Type) (f: A -> B) (a: A) => f a.
Definition tf : forall A B : Type, A -> (A -> B) -> B :=
fun (A B : Type) (a: A) (f: A -> B) => f a.
Definition tg : forall A B C : Type, (A -> B -> C) -> A -> B -> C :=
fun (A B C : Type) (f: A -> B -> C) (a: A) (b: B) => f a b.
Definition th : forall A B C : Type, (A -> B -> C) -> B -> A -> C :=
fun (A B C : Type) (f: A -> B -> C) (b: B) (a: A) => f a b.
Definition ti : forall A B C D : Type, (A -> C) -> (B -> D) -> A -> B -> C * D :=
fun (A B C D : Type) (f: A -> C) (g: B -> D) (a: A) (b: B) => (f a, g b).
Definition tj : forall A B C : Type, (A -> B) -> (B -> C) -> A -> C :=
fun (A B C : Type) (f: A -> B) (g: B -> C) (a: A) => (g (f a)).
Definition tk : forall A B : Type, A * B -> B * A :=
fun (A B: Type) (p: A * B) =>
match p with
| (a, b) => (b, a)
end.
Definition tl : forall A B C : Type, (A * B -> C) -> A -> B -> C :=
fun (A B C: Type) (f: A * B -> C) (a: A) (b: B) => f (a, b).
Definition tm : forall A B C : Type, (A -> B -> C) -> A * B -> C :=
fun (A B C: Type) (f: A -> B -> C) (p: A * B) =>
match p with
(a, b) => f a b
end.
Definition tn : forall A B C : Type, A * (B * C) -> (A * B) * C :=
fun (A B C: Type) (p: A * (B * C)) =>
match p with
(a, (b, c)) => ((a, b), c)
end.
(* ********** *)
(* Exercises about propositions: *)
Proposition pa :
forall A : Prop,
A -> A /\ A.
Proof.
intros A H_A.
split.
- exact H_A.
- exact H_A.
Qed.
Proposition pb :
forall A B : Prop,
A -> B -> A /\ B.
Proof.
intros A B H_A H_B.
split.
exact H_A.
exact H_B.
Qed.
Proposition pc :
forall A B : Prop,
A -> B -> B /\ A.
Proof.
intros A B H_A H_B.
split.
exact H_B.
exact H_A.
Qed.
Check tt.
Proposition pd :
forall (A : Prop),
(unit -> A) -> A.
Proof.
intros A H_A.
exact (H_A tt).
Qed.
Proposition pe :
forall A B : Prop,
(A -> B) -> A -> B.
Proof.
intros A B H_A_implies_B.
exact H_A_implies_B.
Restart.
intros A B H_A_implies_B H_A.
apply H_A_implies_B.
exact H_A.
Qed.
Proposition pf :
forall A B : Prop,
A -> (A -> B) -> B.
Proof.
intros A B H_A H_A_implies_B.
exact (H_A_implies_B H_A).
Qed.
Proposition pg :
forall A B C : Prop,
(A -> B -> C) -> A -> B -> C.
Proof.
intros A B C H_A_B_C.
exact H_A_B_C.
Qed.
Proposition ph :
forall A B C : Prop,
(A -> B -> C) -> B -> A -> C.
Proof.
intros A B C H_A_B_C H_B H_A.
apply H_A_B_C.
- exact H_A.
- exact H_B.
Restart.
intros A B C H_ABC H_B H_A.
exact (H_ABC H_A H_B).
Qed.
Proposition pi :
forall A B C D : Prop,
(A -> C) -> (B -> D) -> A -> B -> C /\ D.
Proof.
intros A B C D H_AC H_BD H_A H_B.
split.
- exact (H_AC H_A).
- exact (H_BD H_B).
Qed.
Proposition pj :
forall A B C : Prop,
(A -> B) -> (B -> C) -> A -> C.
Proof.
intros A B C H_AB H_BC H_A.
apply H_BC.
apply H_AB.
exact H_A.
Qed.
Proposition pk :
forall A B : Prop,
A /\ B -> B /\ A.
Proof.
intros A B [H_A H_B].
split.
- exact H_B.
- exact H_A.
Qed.
Proposition pl :
forall A B C : Prop,
(A /\ B -> C) -> A -> B -> C.
Proof.
intros A B C H_ABC H_A H_B.
apply H_ABC.
exact (conj H_A H_B).
Qed.
Proposition pm :
forall A B C : Prop,
(A -> B -> C) -> A /\ B -> C.
Proof.
intros A B C H_ABC [H_A H_B].
exact (H_ABC H_A H_B).
Qed.
Proposition pn :
forall A B C : Prop,
(A /\ (B /\ C)) -> (A /\ B) /\ C.
Proof.
intros A B C [H_A [H_B H_C]].
split.
- split.
* exact H_A.
* exact H_B.
- exact H_C.
Qed.
(* ********** *)
(* end of week-02_exercises.v *)

325
cs3234/labs/week-02_formalizing-a-proof-in-tcpa.v Normal file
View File

@ -0,0 +1,325 @@
(* week-02_formalizing-a-proof-in-tcpa.v *)
(* LPP 2024 - CS3234 2023-2024, Sem2 *)
(* Olivier Danvy <danvy@yale-nus.edu.sg> *)
(* Version of 26 Jan 2024 with a correct definition of the specifications *)
(* was: *)
(* Version of 25 Jan 2024 *)
(* ********** *)
Require Import Arith Bool.
(* ********** *)
Definition lambda_dropped_specification_of_the_addition_function (add : nat -> nat -> nat) : Prop :=
forall j : nat,
(add O j = j)
/\
(forall i' ih : nat,
add i' j = ih ->
add (S i') j = S ih).
Definition lambda_lifted_specification_of_the_addition_function (add : nat -> nat -> nat) : Prop :=
(forall j : nat,
add O j = j)
/\
(forall j i' ih : nat,
add i' j = ih ->
add (S i') j = S ih).
(* ********** *)
Lemma soundness_of_evenp (evenp : nat -> bool) :
forall n : nat,
evenp n = true ->
exists m : nat,
n = 2 * m.
Admitted.
Lemma completeness_of_evenp (evenp : nat -> bool) :
forall n : nat,
(exists m : nat,
n = 2 * m) ->
evenp n = true.
Admitted.
(* ********** *)
(* Exercise 01 *)
Proposition soundness_of_the_lambda_dropped_specification_of_the_addition_function :
forall add : nat -> nat -> nat,
lambda_dropped_specification_of_the_addition_function add ->
forall x y z : nat,
add x y = z ->
z = x + y.
Admitted.
Proposition completeness_of_the_lambda_lifted_specification_of_the_addition_function :
forall add : nat -> nat -> nat,
lambda_lifted_specification_of_the_addition_function add ->
forall x y z : nat,
x + y = z ->
z = add x y.
Admitted.
(* ********** *)
(* Exercise 02 *)
Definition specification_of_negation (candidate : bool -> bool) : Prop :=
(candidate true = false) /\
(candidate false = true).
Theorem soundness_of_the_specification_of_negation_with_respect_to_negb :
forall candidate: bool -> bool,
specification_of_negation candidate ->
forall b b': bool,
candidate b = b' ->
b' = negb b.
Admitted.
Theorem completeness_of_the_specification_of_negation_with_respect_to_negb :
forall candidate: bool -> bool,
specification_of_negation candidate ->
forall b b': bool,
negb b = b' ->
candidate b = b'.
Admitted.
Definition negation (b : bool) : bool :=
if b then false else true.
Theorem negation_satisfies_the_specification_of_negation :
specification_of_negation negation.
Admitted.
Theorem soundness_of_negation_with_respect_to_negb :
forall b b' : bool,
negation b = b' ->
b' = negb b.
Admitted.
Theorem completeness_of_negation_with_respect_to_negb :
forall b b' : bool,
negb b = b' ->
b' = negation b.
Admitted.
Theorem soundness_of_negb_with_respect_to_negation :
forall b b' : bool,
negb b = b' ->
b' = negation b.
Admitted.
Theorem completeness_of_negb_with_respect_to_negation :
forall b b' : bool,
negation b = b' ->
b' = negb b.
Admitted.
(* ********** *)
Search (_ + 0 = _).
Check Nat.add_0_r.
Proposition first_formal_proof :
forall n : nat,
n + 0 = 0 + n.
Proof.
intro n.
Check (Nat.add_0_r n).
rewrite -> (Nat.add_0_r n).
Check (Nat.add_0_l n).
rewrite -> (Nat.add_0_l n).
reflexivity.
Qed.
Check first_formal_proof.
Proposition first_formal_proof' :
forall n : nat,
n + 0 = 0 + n.
Proof.
intro n.
rewrite -> (Nat.add_0_l n).
rewrite -> (Nat.add_0_r n).
reflexivity.
Qed.
Proposition first_formal_proof'' :
forall n : nat,
n + 0 = 0 + n.
Proof.
intro n.
rewrite -> (Nat.add_0_r n).
rewrite -> (Nat.add_0_l n).
reflexivity.
Restart.
intro n.
rewrite -> (Nat.add_0_l n).
rewrite -> (Nat.add_0_r n).
reflexivity.
Qed.
Proposition first_formal_proof''' :
forall n : nat,
n + 0 = 0 + n.
Proof.
intro n.
Check (Nat.add_comm n 0).
exact (Nat.add_comm n 0).
Restart.
intro n.
Check (Nat.add_comm 0 n).
symmetry.
exact (Nat.add_comm 0 n).
Qed.
(* ********** *)
Search (_ + _ = _ + _).
Proposition first_formal_proof'''' :
forall n : nat,
n + 0 = 0 + n.
Proof.
intro n.
exact (Nat.add_comm n 0).
Restart.
intro n.
symmetry.
exact (Nat.add_comm 0 n).
Qed.
(*
Nat.add_comm: forall n m : nat, n + m = m + n
Nat.add_assoc: forall n m p : nat, n + (m + p) = n + m + p
*)
Check (Nat.add_comm 2 3).
Proposition second_formal_proof:
forall x y z : nat,
x + (y + z) = y + (x + z).
Proof.
intro x.
intro y.
intro z.
Search (_ + (_ + _)).
Check (Nat.add_assoc x y z).
rewrite -> (Nat.add_assoc x y z).
Check Nat.add_comm.
rewrite -> (Nat.add_comm x y).
rewrite <- (Nat.add_assoc).
reflexivity.
Restart.
intros x y z.
rewrite -> (Nat.add_assoc x y z).
rewrite -> (Nat.add_comm x y).
rewrite <- (Nat.add_assoc y x z).
reflexivity.
Qed.
(* ********** *)
Proposition third_formal_proof:
forall n : nat,
n + 0 + 0 = 0 + 0 + n.
Proof.
intro n.
rewrite -> (Nat.add_0_r n).
rewrite -> (Nat.add_0_r n).
Check (Nat.add_0_l 0).
rewrite -> (Nat.add_0_l 0).
rewrite -> (Nat.add_0_l n).
reflexivity.
Restart.
intro n.
rewrite -> (Nat.add_0_r n).
rewrite -> (Nat.add_0_r n).
rewrite -> (Nat.add_0_l 0).
exact (Nat.add_0_l n).
Restart.
intro n.
Check (first_formal_proof (n + 0)).
rewrite -> (first_formal_proof (n + 0)).
Check (first_formal_proof n).
rewrite -> (first_formal_proof n).
exact (Nat.add_assoc 0 0 n).
Restart.
intro n.
Check (Nat.add_0_l 0).
rewrite -> (Nat.add_0_l 0).
rewrite -> (Nat.add_0_r n).
Check first_formal_proof.
exact (first_formal_proof n).
Qed.
(* ********** *)
(* Exercise 3 *)
Proposition foo :
forall n1 n2 n3 n4 : nat,
n1 + (n2 + (n3 + n4)) = ((n1 + n2) + n3) + n4.
Proof.
intros a b c d.
Search (_ + (_ + _) = _ + _ + _).
rewrite -> (Nat.add_assoc a b (c + d)).
Check Nat.add_assoc.
rewrite -> (Nat.add_assoc (a + b) c d).
reflexivity.
Qed.
(* ********** *)
(* Exercise 4 *)
(* ********** *)
(* Exercise 5 *)
Proposition binomial_expansion_2_warmup :
forall x y : nat,
(x + y) * (x + y) = x * x + x * y + x * y + y * y.
Proof.
intros x y.
Search (_ * (_ + _) = _).
Check Nat.mul_add_distr_l.
Check Nat.mul_add_distr_r.
rewrite -> (Nat.mul_add_distr_l (x + y) x y).
rewrite -> (Nat.mul_add_distr_r x y x ).
rewrite -> (Nat.mul_comm y x).
rewrite -> (Nat.mul_add_distr_r x y y ).
Check Nat.add_assoc.
rewrite -> (Nat.add_assoc (x * x + x * y) (x * y) (y * y)).
reflexivity.
Qed.
Proposition binomial_expansion_2 :
forall x y : nat,
(x + y) * (x + y) = x * x + 2 * (x * y) + y * y.
Proof.
intros x y.
Check (Nat.mul_succ_l 1 (x * y)).
rewrite -> (Nat.mul_succ_l 1 (x * y)).
Search (1 * _).
rewrite -> (Nat.mul_1_l (x * y)).
rewrite -> (Nat.add_assoc (x * x) (x * y) (x * y)).
exact (binomial_expansion_2_warmup x y).
Qed.
(* ********** *)
(* end of week-02_formalizing-a-proof-in-tcpa.v *)

539
cs3234/labs/week-02_proving-logical-properties.v Normal file
View File

@ -0,0 +1,539 @@
(* week-02_proving-logical-properties.v *)
(* LPP 2024 - CS3234 2023-2024, Sem2 *)
(* Olivier Danvy <danvy@yale-nus.edu.sg> *)
(* Version of 25 Jan 2024 *)
(* ********** *)
Lemma identity :
forall A : Prop,
A -> A.
Proof.
intro A.
intro H_A.
exact H_A.
Qed.
(* ********** *)
Lemma proving_a_conjunction :
forall A B : Prop,
A -> B -> A /\ B.
Proof.
intros A B H_A H_B.
split.
exact H_A.
exact H_B.
Restart.
intros A B H_A H_B.
split.
{ exact H_A. }
{ exact H_B. }
Restart.
intros A B H_A H_B.
split.
- exact H_A.
- exact H_B.
Restart.
intros A B H_A H_B.
Check (conj H_A H_B).
exact (conj H_A H_B).
Qed.
(* ********** *)
Lemma proving_a_ternary_conjunction :
forall A B C : Prop,
A -> B -> C -> A /\ B /\ C.
Proof.
intros A B C.
intros H_A H_B H_C.
split.
- exact H_A.
- split.
+ exact H_B.
+ exact H_C.
Restart.
intros A B C.
intros H_A H_B H_C.
exact (conj H_A (conj H_B H_C)).
Restart.
intros A B C.
intros H_A H_B H_C.
split.
{ exact H_A. }
split.
{ exact H_B. }
exact H_C.
Qed.
(* ********** *)
Lemma example_for_Anton :
forall A B C D : Prop,
A /\ B /\ C /\ D.
Proof.
intros A B C D.
split.
- admit.
- split.
+ admit.
+ split.
* admit.
* admit.
Restart.
intros A B C D.
split.
{ admit. }
{ split.
{ admit. }
{ split.
{ admit. }
{ admit. } } }
Restart.
intros A B C D.
split.
{ admit. }
split.
{ admit. }
split.
{ admit. }
admit.
Abort.
(* ********** *)
Lemma proving_a_disjunction :
forall A B : Prop,
A -> B -> A \/ B.
Proof.
intros A B H_A H_B.
left.
exact H_A.
Restart.
intros A B H_A H_B.
right.
exact H_B.
Qed.
(* ********** *)
(* Exercise 06 *)
Lemma conjunction_is_commutative:
forall A B : Prop,
A /\ B <-> B /\ A.
Proof.
intros A B.
split.
- intros [H_A H_B].
exact (conj H_B H_A).
- intros [H_B H_A].
exact (conj H_A H_B).
Qed.
Lemma conjunction_is_commutative_aux :
forall A B : Prop,
A /\ B -> B /\ A.
Proof.
intros A B [H_A H_B].
exact (conj H_B H_A).
Qed.
Lemma conjunction_is_commutative_revisited :
forall A B : Prop,
A /\ B <-> B /\ A.
Proof.
intros A B.
split.
- exact (conjunction_is_commutative_aux A B).
- exact (conjunction_is_commutative_aux B A).
Qed.
(* ********** *)
(* Exercise 07 *)
Lemma conjunction_is_associative_aux:
forall A B C : Prop,
A /\ (B /\ C) -> (A /\ B) /\ C.
Proof.
intros A B C.
intros [H_A [H_B H_C]].
exact (conj (conj H_A H_B) H_C).
Qed.
Lemma conjunction_is_associative :
forall A B C : Prop,
A /\ (B /\ C) <-> (A /\ B) /\ C.
Proof.
intros A B C.
split.
- intros [H_A [H_B H_C]].
Check (conj (conj H_A H_B) H_C).
exact (conj (conj H_A H_B) H_C).
- intros [[H_A H_B] H_C].
exact (conj H_A (conj H_B H_C)).
Restart.
intros A B C.
split.
- intros [H_A [H_B H_C]].
split.
* split.
exact H_A.
exact H_B.
* exact H_C.
- intros [[H_A H_B] H_C].
split.
exact H_A.
* split.
exact H_B.
exact H_C.
Qed.
(* ********** *)
(* Exercise 08 *)
Lemma disjunction_is_commutative_aux :
forall A B : Prop,
A \/ B -> B \/ A.
Proof.
intros A B.
intros [H_A | H_B].
right.
exact H_A.
left.
exact H_B.
Qed.
Lemma disjunction_is_commutative :
forall A B : Prop,
A \/ B <-> B \/ A.
Proof.
intros A B.
split.
- intros [H_A | H_B].
right.
exact H_A.
left.
exact H_B.
- intros [H_B | H_A].
right.
exact H_B.
left.
exact H_A.
Restart.
intros A B.
split.
- exact (disjunction_is_commutative_aux A B).
- exact (disjunction_is_commutative_aux B A).
Qed.
(* ********** *)
(* Exercise 09 *)
Lemma disjunction_is_associative :
forall A B C : Prop,
A \/ (B \/ C) <-> (A \/ B) \/ C.
Proof.
intros A B C.
split.
- intros [H_A | [H_B | H_C]].
left.
left.
exact H_A.
left.
right.
exact H_B.
right.
exact H_C.
- intros [[H_A | H_B] | H_C].
left.
exact H_A.
right.
left.
exact H_B.
right.
right.
exact H_C.
Qed.
(* ********** *)
(* Exercise 10 *)
(* Prove whether disjunction distribute over conjunction on the left and on the right. *)
Proposition disjunction_distributes_over_conjunction_on_the_left :
forall A B C : Prop,
A \/ (B /\ C) <-> (A \/ B) /\ (A \/ C).
Proof.
intros A B C.
split.
- intros [H_A | [H_B H_C]].
+ split.
* left.
exact H_A.
* left.
exact H_A.
+ split.
* right.
exact H_B.
* right.
exact H_C.
- intros [[H_A | H_B] [H_A' | H_C]].
+ left.
exact H_A.
+ left.
exact H_A.
+ left.
exact H_A'.
+ right.
exact (conj H_B H_C).
Qed.
Proposition disjunction_distributes_over_conjunction_on_the_right :
forall A B C : Prop,
(B /\ C) \/ A <-> (B \/ A) /\ (C \/ A).
Proof.
intros A B C.
split.
- intros [[H_B H_C] | H_A].
+ split.
* left.
exact H_B.
* left.
exact H_C.
+ split.
* right.
exact H_A.
* right.
exact H_A.
- intros [[H_B | H_A] [H_C | H_A']].
+ left.
exact (conj H_B H_C).
+ right.
exact H_A'.
+ right.
exact H_A.
+ right.
exact H_A.
Qed.
(* ********** *)
(* Exercise 11 *)
(*
Does conjunction distribute over disjunction on the left?
And what about on the right?
*)
(* ********** *)
Proposition modus_ponens :
forall A B : Prop,
A -> (A -> B) -> B.
Proof.
intros A B.
intros H_A H_A_implies_B.
Check (H_A_implies_B H_A).
exact (H_A_implies_B H_A).
Restart.
intros A B.
intros H_A H_A_implies_B.
apply H_A_implies_B.
exact H_A.
Qed.
(* ********** *)
(* Exercise 12 *)
Proposition following :
forall A B : Prop,
(A -> B) -> A -> B.
Proof.
intros A B.
intros H_A_implies_B.
intros H_A.
exact (H_A_implies_B H_A).
Restart.
intros A B.
intros H_A_implies_B.
apply H_A_implies_B.
Qed.
(* ********** *)
Proposition modus_tollens :
forall A B : Prop,
~B -> (A -> B) -> ~A.
Proof.
intros A B.
unfold not.
intros H_B_implies_False H_A_implies_B H_A.
apply H_B_implies_False.
apply H_A_implies_B.
exact H_A.
Restart.
intros A B.
unfold not.
intros H_B_implies_False H_A_implies_B H_A.
Check (H_A_implies_B H_A).
Check (H_B_implies_False (H_A_implies_B H_A)).
exact (H_B_implies_False (H_A_implies_B H_A)).
Restart.
intros A B.
unfold not.
intros H_B_implies_False H_A_implies_B H_A.
Check (modus_ponens A B).
Check (modus_ponens A B H_A).
Check (modus_ponens A B H_A H_A_implies_B).
Check (H_B_implies_False (modus_ponens A B H_A H_A_implies_B)).
exact (H_B_implies_False (modus_ponens A B H_A H_A_implies_B)).
Qed.
(* ********** *)
(* Exercise 13 *)
Proposition implication_distributes_over_conjunction_on_the_left :
forall A B C : Prop,
(A -> B /\ C) <-> ((A -> B) /\ (A -> C)).
Proof.
intros A B C.
split.
- intros H_A_implies_B_and_C.
split.
* intro H_A.
Check (H_A_implies_B_and_C H_A).
destruct (H_A_implies_B_and_C H_A) as [H_B _].
exact H_B.
* intro H_A.
destruct (H_A_implies_B_and_C H_A) as [_ H_C].
exact H_C.
- intros [H_A_implies_B H_A_implies_C] H_A.
Check (H_A_implies_B H_A).
Check (H_A_implies_C H_A).
Check (conj (H_A_implies_B H_A) (H_A_implies_C H_A)).
exact (conj (H_A_implies_B H_A) (H_A_implies_C H_A)).
Qed.
(* ********** *)
(* Exercise 14 *)
Proposition implication_distributes_over_disjunction_on_the_right_and_with_a_twist :
forall A B C : Prop,
((A \/ B) -> C) <-> ((A -> C) /\ (B -> C)).
Proof.
intros A B C.
split.
- intros H_A_or_B_implies_C.
split.
+ intro H_A.
apply H_A_or_B_implies_C.
left.
exact H_A.
+ intro H_B.
apply H_A_or_B_implies_C.
right.
exact H_B.
- intros [H_A_implies_C H_B_implies_C] [H_A | H_B].
+ Check (H_A_implies_C H_A).
exact (H_A_implies_C H_A).
+ exact (H_B_implies_C H_B).
Qed.
(* ********** *)
(* Exercise 15 *)
Proposition contrapositive_of_implication :
forall A B : Prop,
(A -> B) -> ~B -> ~A.
Proof.
intros A B.
intros H_A_implies_B H_not_B.
Check (modus_tollens A B H_not_B H_A_implies_B).
exact (modus_tollens A B H_not_B H_A_implies_B).
Qed.
(* ********** *)
(* Exercise 16 *)
Proposition contrapositive_of_contrapositive_of_implication :
forall A B : Prop,
(~B -> ~A) -> ~~A -> ~~B.
Proof.
intros A B.
Check (contrapositive_of_implication (not B) (not A)).
exact (contrapositive_of_implication (not B) (not A)).
Qed.
(* ********** *)
(* Exercise 17 *)
Proposition double_negation :
forall A : Prop,
A -> ~~A.
Proof.
intros A.
intros H_A.
unfold not.
intros H_A_implies_false.
apply H_A_implies_false.
exact H_A.
Qed.
(* ********** *)
(* end of week-02_proving-logical-properties.v *)

110
cs3234/labs/week-02_the-intro-tactic.v Normal file
View File

@ -0,0 +1,110 @@
(* week-02_the-intro-tactic.v *)
(* LPP 2023 - CS3234 2023-2024, Sem2 *)
(* Olivier Danvy <danvy@yale-nus.edu.sg> *)
(* Version of 25 Jan 2024 *)
(* ********** *)
Lemma a_proposition_implies_itself :
forall A : Prop,
A -> A.
Proof.
intro A.
intro H_A.
exact H_A.
Restart.
intro rose.
intro H_rose.
exact H_rose.
Qed.
(* ********** *)
Lemma the_following_example :
forall A B C : Prop,
A ->
B ->
C ->
forall i j : nat,
A /\ B /\ C /\ i = i /\ j = j.
Proof.
intros A B C.
intros H_A H_B H_C.
intros i j.
split.
exact H_A.
split.
exact H_B.
split.
exact H_C.
split.
reflexivity.
reflexivity.
Qed.
(* ********** *)
Lemma a_pair_of_propositions_implies_the_left_one :
forall A B : Prop,
A /\ B -> A.
Proof.
intros A B.
intro H_A_and_B.
destruct H_A_and_B.
exact H.
Restart.
intros A B.
intro H_A_and_B.
destruct H_A_and_B as [H_A H_B].
exact H_A.
Restart.
intros A B.
intros [H_A H_B].
exact H_A.
Qed.
(* ********** *)
Lemma disjunction_is_commutative :
forall A B : Prop,
A \/ B -> B \/ A.
Proof.
intros A B.
intros [H_A | H_B].
- right.
exact H_A.
- left.
exact H_B.
Qed.
(* ********** *)
Lemma about_nested_conjunctions :
forall A B C D : Prop,
(A /\ B) /\ (C /\ D) -> (D /\ A) /\ (B /\ C).
Proof.
intros A B C D.
intros [[H_A H_B] [H_C H_D]].
Check (conj (conj H_D H_A) (conj H_B H_C)).
exact (conj (conj H_D H_A) (conj H_B H_C)).
Qed.
Lemma about_nested_conjunctions_and_disjunctions :
forall A B C D E F : Prop,
(A \/ B) /\ (C \/ (D /\ E)) -> F.
Proof.
intros A B C D E F.
intros [[H_A | H_B] [H_C | [H_D H_E]]].
Abort.
(* ********** *)
(* end of week-02_the-intro-tactic.v *)

67
cs3234/labs/week-02_the-revert-tactic.v Normal file
View File

@ -0,0 +1,67 @@
(* week-02_the-revert-tactic.v *)
(* LPP 2024 - CS3234 2023-2024, Sem2 *)
(* Olivier Danvy <danvy@yale-nus.edu.sg> *)
(* Version of 28 Jan 2024, with an instance of revert with several arguments *)
(* was: *)
(* Version of 25 Jan 2024 *)
(* ********** *)
Lemma a_proposition_implies_itself :
forall A : Prop,
A -> A.
Proof.
intro A.
intro H_A.
exact H_A.
Restart.
intro A.
intro H_A.
revert H_A. (* <-- *)
revert A. (* <-- *)
intros A H_A.
exact H_A.
Qed.
(* ********** *)
Lemma swapping_the_order_of_quantifiers :
forall A B : Prop,
(A -> B -> A /\ B) -> B -> A -> A /\ B.
Proof.
intros A B H_implication H_B H_A.
exact (H_implication H_A H_B).
Restart.
intros A B H_implication H_B H_A.
revert H_B.
revert H_A.
exact H_implication.
Restart.
intros A B H_implication H_B H_A.
revert H_B.
revert H_A.
revert H_implication.
exact (a_proposition_implies_itself (A -> B -> A /\ B)).
Restart.
intros A B H_implication H_B H_A.
revert H_A H_B.
exact H_implication.
Restart.
intros A B H_implication H_B H_A.
revert H_implication H_A H_B.
exact (a_proposition_implies_itself (A -> B -> A /\ B)).
Qed.
(* ********** *)
(* end of week-02_the-revert-tactic.v *)