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

feat: 3234 week 3

Browse Source
This commit is contained in:
Yadunand Prem 2024-02-13 17:04:53 +08:00
parent 01ffa3b6aa
commit 14e3095632
No known key found for this signature in database
5 changed files with 1387 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

581
cs3234/labs/week-03_specifications.v Normal file
View File

@ -0,0 +1,581 @@
(* week-03_specifications.v *)
(* LPP 2023 - CS3234 2023-2024, Sem2 *)
(* Olivier Danvy <danvy@yale-nus.edu.sg> *)
(* Version of 01 Feb 2024 *)
(* ********** *)
(* Paraphernalia: *)
Require Import Arith.
(* ********** *)
Definition recursive_specification_of_addition (add : nat -> nat -> nat) :=
(forall y : nat,
add O y = y)
/\
(forall x' y : nat,
add (S x') y = S (add x' y)).
Definition lambda_dropped_recursive_specification_of_addition (add : nat -> nat -> nat) :=
(forall y : nat,
add 0 y = y
/\ forall x' : nat,
add (S x') y = S (add x' y)).
Proposition there_is_at_most_one_recursive_addition :
forall add1 add2 : nat -> nat -> nat,
recursive_specification_of_addition add1 ->
recursive_specification_of_addition add2 ->
forall x y : nat,
add1 x y = add2 x y.
Proof.
intros add1 add2.
unfold recursive_specification_of_addition.
intros [H_add1_0 H_add1_S].
intros [H_add2_0 H_add2_S].
intro x.
induction x as [| x' IHx].
- intro y.
rewrite H_add1_0.
rewrite H_add2_0.
reflexivity.
- intro y.
rewrite H_add1_S.
rewrite H_add2_S.
rewrite IHx.
reflexivity.
Restart.
intros add1 add2.
unfold recursive_specification_of_addition.
intros [H_add1_O H_add1_S] [H_add2_O H_add2_S].
intro x.
induction x as [| x' IHx'].
- intro y.
rewrite -> (H_add2_O y).
Check (H_add1_O y).
exact (H_add1_O y).
- intro y.
rewrite -> (H_add1_S x' y).
rewrite -> (H_add2_S x' y).
Check (IHx' y).
rewrite -> (IHx' y).
reflexivity.
Qed.
(* ********** *)
Definition tail_recursive_specification_of_addition (add : nat -> nat -> nat) :=
(forall y : nat,
add O y = y)
/\
(forall x' y : nat,
add (S x') y = add x' (S y)).
(* ***** *)
(* Exercise 01 *)
Proposition there_is_at_most_one_tail_recursive_addition :
forall add1 add2 : nat -> nat -> nat,
tail_recursive_specification_of_addition add1 ->
tail_recursive_specification_of_addition add2 ->
forall x y : nat,
add1 x y = add2 x y.
Proof.
intros add1 add2.
unfold tail_recursive_specification_of_addition.
intros [H_add1_O H_add1_S] [H_add2_O H_add2_S].
intros x y.
induction x as [| x' IHx'].
- rewrite -> (H_add2_O y).
exact (H_add1_O y).
- rewrite -> (H_add1_S x' y).
rewrite -> (H_add2_S x' y).
(* rewrite -> (IHx' (S y)). *)
Restart.
intros add1 add2.
unfold tail_recursive_specification_of_addition.
intros [H_add1_O H_add1_S] [H_add2_O H_add2_S].
intro x.
induction x as [| x' IHx'].
- intro y.
rewrite -> (H_add2_O y).
exact (H_add1_O y).
- intro y.
rewrite -> (H_add1_S x' y).
rewrite -> (H_add2_S x' y).
rewrite -> (IHx' (S y)).
reflexivity.
Qed.
(* ********** *)
Definition specification_of_the_predecessor_function (pred : nat -> nat) :=
forall n : nat,
pred (S n) = n.
Proposition there_is_at_most_one_predecessor_function :
forall pred1 pred2 : nat -> nat,
specification_of_the_predecessor_function pred1 ->
specification_of_the_predecessor_function pred2 ->
forall n : nat,
pred1 n = pred2 n.
Proof.
intros pred1 pred2.
unfold specification_of_the_predecessor_function.
intros H_pred1_S H_pred2_S.
intro n.
induction n as [ | n' IHn'].
Abort.
Definition make_predecessor_function (zero n : nat) :=
match n with
| 0 => zero
| S n' => n'
end.
Lemma about_make_predecessor_function :
forall zero : nat,
specification_of_the_predecessor_function (make_predecessor_function zero).
Proof.
intro zero.
unfold specification_of_the_predecessor_function.
induction n as [| n' IHn' ].
- unfold make_predecessor_function.
reflexivity.
- unfold make_predecessor_function.
reflexivity.
Qed.
Theorem there_are_at_least_two_predecessor_functions :
exists pred1 pred2 : nat -> nat,
specification_of_the_predecessor_function pred1 /\
specification_of_the_predecessor_function pred2 /\
exists n : nat,
pred1 n <> pred2 n.
Proof.
exists (make_predecessor_function 0).
exists (make_predecessor_function 1).
split.
- exact (about_make_predecessor_function 0).
- split.
-- exact (about_make_predecessor_function 0).
-- exists 0.
unfold make_predecessor_function.
Search (_ <> S _).
Check (n_Sn 0).
exact (n_Sn 0).
Qed.
(* ********** *)
Definition specification_of_the_total_predecessor_function (pred : nat -> option nat) :=
(pred 0 = None)
/\
(forall n : nat,
pred (S n) = Some n).
(* ***** *)
(* Exercise 02 *)
Proposition there_is_at_most_one_total_predecessor_function :
forall pred1 pred2 : nat -> option nat,
specification_of_the_total_predecessor_function pred1 ->
specification_of_the_total_predecessor_function pred2 ->
forall n : nat,
pred1 n = pred2 n.
Proof.
intros pred1 pred2.
unfold specification_of_the_total_predecessor_function.
intros [H_pred1_O H_pred1_S] [H_pred2_O H_pred2_S].
intro n.
induction n as [ | n' IHn'].
- rewrite -> H_pred2_O.
exact H_pred1_O.
- rewrite -> (H_pred2_S n').
exact (H_pred1_S n').
Restart.
intros pred1 pred2.
unfold specification_of_the_total_predecessor_function.
intros [H_pred1_O H_pred1_S] [H_pred2_O H_pred2_S].
intros [ | n'].
- rewrite -> H_pred2_O.
exact H_pred1_O.
- rewrite -> (H_pred2_S n').
exact (H_pred1_S n').
Qed.
(* ********** *)
Definition specification_of_the_predecessor_and_successor_function (ps : nat -> nat) :=
(forall n : nat,
ps (S n) = n)
/\
(forall n : nat,
ps n = (S n)).
(* ***** *)
(* Exercise 03 *)
Theorem there_is_at_most_one_predecessor_and_successor_function :
forall ps1 ps2 : nat -> nat,
specification_of_the_predecessor_and_successor_function ps1 ->
specification_of_the_predecessor_and_successor_function ps2 ->
forall n : nat,
ps1 n = ps2 n.
Proof.
intros ps1 ps2.
unfold specification_of_the_predecessor_and_successor_function.
intros [H_ps1_Sn_n H_ps1_n_Sn] [H_ps2_Sn_n H_ps2_n_Sn].
induction n as [| n' IHn'].
- Check (H_ps1_n_Sn 0).
rewrite (H_ps1_n_Sn 0).
rewrite (H_ps2_n_Sn 0).
reflexivity.
- rewrite -> (H_ps1_Sn_n n').
rewrite -> (H_ps2_Sn_n n').
reflexivity.
Abort.
(* ***** *)
Lemma a_contradictory_aspect_of_the_predecessor_and_successor_function :
forall ps : nat -> nat,
specification_of_the_predecessor_and_successor_function ps ->
ps 1 = 0 /\ ps 1 = 2.
Proof.
intro ps.
unfold specification_of_the_predecessor_and_successor_function.
intros [H_ps_S H_ps].
split.
- rewrite -> (H_ps_S 0).
reflexivity.
- rewrite -> (H_ps 1).
reflexivity.
Qed.
Theorem there_are_zero_predecessor_and_successor_functions :
forall ps : nat -> nat,
specification_of_the_predecessor_and_successor_function ps ->
exists n : nat,
ps n <> ps n.
Proof.
intros ps S_ps.
Check (a_contradictory_aspect_of_the_predecessor_and_successor_function ps S_ps).
destruct (a_contradictory_aspect_of_the_predecessor_and_successor_function ps S_ps) as [H_ps_0 H_ps_2].
exists 1.
rewrite -> H_ps_0.
Restart.
intros ps S_ps.
Check (a_contradictory_aspect_of_the_predecessor_and_successor_function ps S_ps).
destruct (a_contradictory_aspect_of_the_predecessor_and_successor_function ps S_ps) as [H_ps_0 H_ps_2].
exists 1.
rewrite -> H_ps_0 at 1.
rewrite -> H_ps_2.
Search (0 <> S _).
Check (O_S 1).
exact (O_S 1).
Qed.
(* ********** *)
Theorem the_resident_addition_function_satisfies_the_recursive_specification_of_addition :
recursive_specification_of_addition Nat.add.
Proof.
unfold recursive_specification_of_addition.
split.
- intro y.
Search (0 + _ = _).
exact (Nat.add_0_l y).
- intros x' y.
Search (S _ + _ = S (_ + _)).
exact (Nat.add_succ_l x' y).
Qed.
(* ***** *)
(* Exercise 04 *)
Theorem the_resident_addition_function_satisfies_the_tail_recursive_specification_of_addition :
tail_recursive_specification_of_addition Nat.add.
Proof.
unfold tail_recursive_specification_of_addition.
split.
- intro y.
exact (Nat.add_0_l y).
- intros x' y.
Search (S _ + _ = _ + S _).
exact (Nat.add_succ_comm x' y).
Qed.
(* ********** *)
(* Exercise 05 *)
Theorem the_two_specifications_of_addition_are_equivalent :
forall add : nat -> nat -> nat,
recursive_specification_of_addition add <-> tail_recursive_specification_of_addition add.
Proof.
intro add.
unfold recursive_specification_of_addition.
unfold tail_recursive_specification_of_addition.
split.
- intros [H_add_O H_add_S].
split.
* exact H_add_O.
* intros x'.
induction x' as [| x'' IHx''].
+ intro y.
Check (H_add_S 0 y).
rewrite -> (H_add_S 0 y).
rewrite -> (H_add_O y).
rewrite -> (H_add_O (S y)).
reflexivity.
+ intro y.
rewrite -> (H_add_S (S x'') y).
rewrite -> (H_add_S x'' (S y)).
rewrite IHx''.
reflexivity.
- intros [H_add_O H_add_S].
split.
* exact H_add_O.
* intro x'.
induction x' as [| x'' IHx''].
+ intro y.
rewrite -> (H_add_O y).
rewrite -> (H_add_S 0 y).
rewrite -> (H_add_O (S y)).
reflexivity.
+ intro y.
rewrite -> (H_add_S (S x'') y).
rewrite -> (IHx'' (S y)).
rewrite <- (H_add_S x'' y).
reflexivity.
Qed.
(* ********** *)
(* Exercise 06a *)
Theorem associativity_of_recursive_addition :
forall add : nat -> nat -> nat,
recursive_specification_of_addition add ->
forall n1 n2 n3 : nat,
add n1 (add n2 n3) = add (add n1 n2) n3.
Proof.
intro add.
unfold recursive_specification_of_addition.
intros [H_add_O H_add_S].
intros x.
induction x as [| x' IHx'].
- intros y z.
rewrite (H_add_O (add y z)).
rewrite (H_add_O y).
reflexivity.
- intros y z.
rewrite -> (H_add_S x' (add y z)).
rewrite -> (H_add_S x' y).
rewrite -> (H_add_S (add x' y) z).
rewrite -> IHx'.
reflexivity.
Qed.
Lemma about_the_tail_recursive_addition_function :
forall add: nat -> nat -> nat,
tail_recursive_specification_of_addition add ->
forall x y : nat,
add (S x) y = S (add x y).
Proof.
intro add.
unfold tail_recursive_specification_of_addition.
intros [H_add_O H_add_S].
intro x.
induction x as [| x' IHx'].
- intro y.
rewrite -> (H_add_O y).
rewrite -> (H_add_S 0 y).
rewrite -> (H_add_O (S y)).
reflexivity.
- intro y.
rewrite -> (H_add_S x' y).
rewrite <- (IHx' (S y)).
rewrite -> (H_add_S (S x') y).
reflexivity.
Qed.
Theorem associativity_of_tail_recursive_addition :
forall add : nat -> nat -> nat,
tail_recursive_specification_of_addition add ->
forall n1 n2 n3 : nat,
add n1 (add n2 n3) = add (add n1 n2) n3.
Proof.
intros add H_add.
assert (H_tmp := H_add).
destruct H_tmp as [H_add_O H_add_S].
intros x.
induction x as [| x' IHx'].
- intros y z.
rewrite (H_add_O (add y z)).
rewrite (H_add_O y).
reflexivity.
- intros y z.
rewrite -> (H_add_S x' (add y z)).
rewrite -> (H_add_S x' y).
rewrite <- (IHx' (S y) z).
rewrite -> (about_the_tail_recursive_addition_function add H_add y z).
reflexivity.
Qed.
(* ********** *)
(* Exercise 07 *)
Lemma commutativity_of_recursive_addition_O :
forall add : nat -> nat -> nat,
recursive_specification_of_addition add ->
forall n : nat,
add n O = n.
Proof.
intro add.
unfold recursive_specification_of_addition.
intros [H_add_O H_add_S].
intro n.
induction n as [| n' IHn'].
- exact (H_add_O 0).
- rewrite -> (H_add_S n' 0).
rewrite -> IHn'.
reflexivity.
Qed.
Lemma commutativity_of_recursive_addition_S :
forall add : nat -> nat -> nat,
recursive_specification_of_addition add ->
forall n1 n2 : nat,
add n1 (S n2) = S (add n1 n2).
Proof.
intros add H_add.
assert (H_tmp := H_add).
unfold recursive_specification_of_addition.
destruct H_tmp as [H_add_O H_add_S].
intro x.
induction x as [| x' IHx'].
- intro y.
rewrite (H_add_O (S y)).
rewrite (H_add_O y).
reflexivity.
- intro y.
rewrite -> (H_add_S x' (S y)).
rewrite -> (IHx' y).
rewrite -> (H_add_S x' y).
reflexivity.
Qed.
Theorem commutativity_of_recursive_addition :
forall add : nat -> nat -> nat,
recursive_specification_of_addition add ->
forall n1 n2 : nat,
add n1 n2 = add n2 n1.
Proof.
intros add S_add.
assert (H_add_O := commutativity_of_recursive_addition_O add S_add).
assert (H_add_S := commutativity_of_recursive_addition_S add S_add).
unfold recursive_specification_of_addition in S_add.
destruct S_add as [S_add_O S_add_S].
intro x.
induction x as [| x' IHx'].
- intro y.
rewrite -> (S_add_O y).
rewrite -> (H_add_O y).
reflexivity.
- intro y.
rewrite -> (S_add_S x' y).
rewrite -> (H_add_S y).
rewrite -> (IHx' y).
reflexivity.
Qed.
(* ********** *)
(* Exercise 08a *)
Theorem O_is_left_neutral_for_recursive_addition :
forall add : nat -> nat -> nat,
recursive_specification_of_addition add ->
forall n : nat,
add 0 n = n.
Proof.
intros add.
unfold recursive_specification_of_addition.
intros [H_add_O _].
exact H_add_O.
Qed.
(* ***** *)
(* Exercise 08b *)
Theorem O_is_right_neutral_for_recursive_addition :
forall add : nat -> nat -> nat,
recursive_specification_of_addition add ->
forall n : nat,
add n 0 = n.
Proof.
intros add S_add.
unfold recursive_specification_of_addition in S_add.
intro n.
rewrite -> (commutativity_of_recursive_addition add S_add n).
rewrite -> (O_is_left_neutral_for_recursive_addition add S_add n).
reflexivity.
Qed.
(* ********** *)
(* ***** *)
(* Exercise 08c *)
Theorem O_is_left_neutral_for_tail_recursive_addition :
forall add : nat -> nat -> nat,
tail_recursive_specification_of_addition add ->
forall n : nat,
add 0 n = n.
Proof.
intros add.
unfold tail_recursive_specification_of_addition.
intros [H_add_O _].
exact H_add_O.
Qed.
Theorem O_is_right_neutral_for_tail_recursive_addition :
forall add : nat -> nat -> nat,
tail_recursive_specification_of_addition add ->
forall n: nat,
add n 0 = n.
Proof.
Admitted.
(* end of week-03_specifications.v *)

134
cs3234/labs/week-03_structural-induction-over-Peano-numbers.v Normal file
View File

@ -0,0 +1,134 @@
(* week-03_structural-induction-over-Peano-numbers.v *)
(* LPP 2023 - CS3234 2023-2024, Sem2 *)
(* Olivier Danvy <danvy@yale-nus.edu.sg> *)
(* Version of 05 Feb 2024, with a revisitation of Proposition add_0_r_v0 that uses the induction tactic *)
(* was: *)
(* Version of 02 Feb 2024 *)
(* ********** *)
Definition specification_of_the_addition_function_1 (add : nat -> nat -> nat) :=
(forall j : nat,
add O j = j)
/\
(forall i' j : nat,
add (S i') j = S (add i' j)).
Check nat_ind.
(*
nat_ind
: forall P : nat -> Prop, P 0 -> (forall n : nat, P n -> P (S n)) -> forall n : nat, P n
*)
Proposition add_0_r_v0 :
forall add : nat -> nat -> nat,
specification_of_the_addition_function_1 add ->
forall n : nat,
add n 0 = n.
Proof.
intro add.
unfold specification_of_the_addition_function_1.
intros [S_add_O S_add_S].
Check nat_ind.
Check (nat_ind
(fun n => add n 0 = n)).
Check (S_add_O 0).
Check (nat_ind
(fun n => add n 0 = n)
(S_add_O 0)).
apply (nat_ind
(fun n => add n 0 = n)
(S_add_O 0)).
intro n'.
intro IHn'.
Check (S_add_S n' 0).
rewrite -> (S_add_S n' 0).
rewrite -> IHn'.
reflexivity.
Qed.
Search (0 + _ = _).
(* plus_O_n: forall n : nat, 0 + n = n *)
Search (S _ + _ = _).
(* plus_Sn_m: forall n m : nat, S n + m = S (n + m) *)
Proposition add_0_r_v1 :
forall n : nat,
n + 0 = n.
Proof.
Check nat_ind.
Check (nat_ind
(fun n => n + 0 = n)).
Check plus_O_n.
Check (plus_O_n 0).
Check (nat_ind
(fun n => n + 0 = n)
(plus_O_n 0)).
apply (nat_ind
(fun n => n + 0 = n)
(plus_O_n 0)).
intros n'.
intros IHn'.
Check (plus_Sn_m n' 0).
rewrite -> (plus_Sn_m n' 0).
rewrite -> IHn'.
reflexivity.
Restart.
intro n.
induction n using nat_ind.
- Check (plus_O_n 0).
exact (plus_O_n 0).
- revert n IHn.
intros n' IHn'.
Check (plus_Sn_m n' 0).
rewrite -> (plus_Sn_m n' 0).
rewrite -> IHn'.
reflexivity.
Restart.
intro n.
induction n as [ | n' IHn'] using nat_ind.
- Check (plus_O_n 0).
exact (plus_O_n 0).
- Check (plus_Sn_m n' 0).
rewrite -> (plus_Sn_m n' 0).
rewrite -> IHn'.
reflexivity.
Restart.
intro n.
induction n as [ | n' IHn'].
- Check (plus_O_n 0).
exact (plus_O_n 0).
- Check (plus_Sn_m n' 0).
rewrite -> (plus_Sn_m n' 0).
rewrite -> IHn'.
reflexivity.
Qed.
Proposition add_0_r_v0_revisited :
forall add : nat -> nat -> nat,
specification_of_the_addition_function_1 add ->
forall n : nat,
add n 0 = n.
Proof.
intro add.
unfold specification_of_the_addition_function_1.
intros [S_add_O S_add_S].
intro n.
induction n as [ | n' IHn'].
- exact (S_add_O 0).
- rewrite -> (S_add_S n' 0).
rewrite -> IHn'.
reflexivity.
Qed.
(* ********** *)
(* end of week-03_structural-induction-over-Peano-numbers.v *)

389
cs3234/labs/week-03_structural-induction-over-binary-trees.v Normal file
View File

@ -0,0 +1,389 @@
(* week-03_induction-over-binary-trees.v *)
(* LPP 2023 - CS3234 2023-2024, Sem2 *)
(* Olivier Danvy <danvy@yale-nus.edu.sg> *)
(* Version of 01 Feb 2024 *)
(* ********** *)
Inductive binary_tree (V : Type) : Type :=
Leaf : V -> binary_tree V
| Node : binary_tree V -> binary_tree V -> binary_tree V.
(* ********** *)
Check binary_tree_ind.
Definition specification_of_mirror (mirror : forall V : Type, binary_tree V -> binary_tree V) : Prop :=
(forall (V : Type)
(v : V),
mirror V (Leaf V v) =
Leaf V v)
/\
(forall (V : Type)
(t1 t2 : binary_tree V),
mirror V (Node V t1 t2) =
Node V (mirror V t2) (mirror V t1)).
Definition specification_of_number_of_nodes (number_of_nodes : forall V: Type, binary_tree V -> nat) : Prop :=
(forall (V : Type) (v: V),
number_of_nodes V (Leaf V v) = 0)
/\
(forall (V : Type) (t1 t2 : binary_tree V),
number_of_nodes V (Node V t1 t2) =
S (number_of_nodes V t1 + number_of_nodes V t2)).
Definition specification_of_number_of_leaves (number_of_leaves : forall V: Type, binary_tree V -> nat) : Prop :=
(forall (V : Type) (v: V),
number_of_leaves V (Leaf V v) = 1)
/\
(forall (V : Type) (t1 t2 : binary_tree V),
number_of_leaves V (Node V t1 t2) =
number_of_leaves V t1 + number_of_leaves V t2).
(* ***** *)
(* Exercise 09a *)
Proposition there_is_at_most_one_mirror_function :
forall mirror1 mirror2 : forall V : Type, binary_tree V -> binary_tree V,
specification_of_mirror mirror1 ->
specification_of_mirror mirror2 ->
forall (V : Type)
(t : binary_tree V),
mirror1 V t = mirror2 V t.
Proof.
intros mirror1 mirror2.
unfold specification_of_mirror.
intros [S_Leaf1 S_Node1].
intros [S_Leaf2 S_Node2].
intros V t.
induction t as [| t1 IHt1 t2 IHt2].
- rewrite -> (S_Leaf1 V v).
rewrite -> (S_Leaf2 V v).
reflexivity.
- rewrite -> (S_Node1 V t1 t2).
rewrite -> (S_Node2 V t1 t2).
rewrite -> IHt1.
rewrite -> IHt2.
reflexivity.
Qed.
(* Exercise 09b *)
Proposition there_is_at_most_one_number_of_nodes_function :
forall number_of_nodes1 number_of_nodes2 : forall V : Type, binary_tree V -> nat,
specification_of_number_of_nodes number_of_nodes1 ->
specification_of_number_of_nodes number_of_nodes2 ->
forall (V : Type)
(t : binary_tree V),
number_of_nodes1 V t = number_of_nodes2 V t.
Proof.
intros number_of_nodes1 number_of_nodes2.
unfold specification_of_number_of_nodes.
intros [S_Leaf1 S_Node1].
intros [S_Leaf2 S_Node2].
intros V t.
induction t as [| t1 IHt1 t2 IHt2].
- rewrite -> (S_Leaf1 V v).
rewrite -> (S_Leaf2 V v).
reflexivity.
- rewrite -> (S_Node1 V t1 t2).
rewrite -> (S_Node2 V t1 t2).
rewrite -> IHt1.
rewrite -> IHt2.
reflexivity.
Qed.
(* Exercise 09c *)
Proposition there_is_at_most_one_number_of_leaves_function :
forall number_of_leaves1 number_of_leaves2 : forall V : Type, binary_tree V -> nat,
specification_of_number_of_leaves number_of_leaves1 ->
specification_of_number_of_leaves number_of_leaves2 ->
forall (V : Type)
(t : binary_tree V),
number_of_leaves1 V t = number_of_leaves2 V t.
Proof.
intros number_of_leaves1 number_of_leaves2.
unfold specification_of_number_of_leaves.
intros [S_Leaf1 S_Node1].
intros [S_Leaf2 S_Node2].
intros V t.
induction t as [v | t1 IHt1 t2 IHt2].
- rewrite -> (S_Leaf1 V v).
rewrite -> (S_Leaf2 V v).
reflexivity.
- rewrite -> (S_Node1 V t1 t2).
rewrite -> (S_Node2 V t1 t2).
rewrite -> IHt1.
rewrite -> IHt2.
reflexivity.
Qed.
(* ***** *)
Theorem mirror_is_involutory :
forall mirror : forall V : Type, binary_tree V -> binary_tree V,
specification_of_mirror mirror ->
forall (V : Type)
(t : binary_tree V),
mirror V (mirror V t) = t.
Proof.
intro mirror.
unfold specification_of_mirror.
intros [S_Leaf S_Node].
intros V t.
induction t as [v | t1 IHt1 t2 IHt2].
- revert V v.
intros V v.
Check (S_Leaf V v).
rewrite -> (S_Leaf V v).
Check (S_Leaf V v).
(*
exact (S_Leaf V v).
*)
rewrite -> (S_Leaf V v).
reflexivity.
- revert IHt2.
revert t2.
revert IHt1.
revert t1.
intros t1 IHt1 t2 IHt2.
Check (S_Node V t1 t2).
rewrite -> (S_Node V t1 t2).
Check (S_Node V (mirror V t2) (mirror V t1)).
rewrite -> (S_Node V (mirror V t2) (mirror V t1)).
rewrite -> IHt1.
rewrite -> IHt2.
reflexivity.
Restart. (* now for a less verbose proof: *)
intros mirror S_mirror V t.
induction t as [ v | t1 IHt1 t2 IHt2].
- unfold specification_of_mirror in S_mirror.
destruct S_mirror as [S_Leaf _].
Check (S_Leaf V v).
rewrite -> (S_Leaf V v).
Check (S_Leaf V v).
exact (S_Leaf V v).
- unfold specification_of_mirror in S_mirror.
destruct S_mirror as [_ S_Node].
Check (S_Node V t1 t2).
rewrite -> (S_Node V t1 t2).
Check (S_Node V (mirror V t2) (mirror V t1)).
rewrite -> (S_Node V (mirror V t2) (mirror V t1)).
rewrite -> IHt1.
rewrite -> IHt2.
reflexivity.
Qed.
(* ********** *)
(* Exercise 10 *)
Proposition mirror_reverses_itself :
forall mirror : forall V : Type, binary_tree V -> binary_tree V,
specification_of_mirror mirror ->
forall (V : Type)
(t t' : binary_tree V),
mirror V t = t' ->
mirror V t' = t.
Proof.
intros mirror S_mirror.
assert (S_tmp :=S_mirror).
unfold specification_of_mirror in S_tmp.
destruct S_tmp as [S_Leaf S_Node].
intros V t t' M_t_t'.
induction t' as [v | t1 IHt1 t2 IHt2].
- rewrite <- M_t_t'.
rewrite -> (mirror_is_involutory mirror S_mirror V t).
reflexivity.
- rewrite -> (S_Node V t1 t2).
Check (mirror_is_involutory mirror S_mirror V t1).
Proposition mirror_reverses_itself :
forall mirror : forall V : Type, binary_tree V -> binary_tree V,
specification_of_mirror mirror ->
forall (V : Type)
(t t' : binary_tree V),
mirror V t = t' ->
mirror V t' = t.
Proof.
intros mirror S_mirror V t t' M_t_t'.
assert (f_equal :
forall t1 t2 : binary_tree V,
t1 = t2 ->
mirror V t1 = mirror V t2).
{ intros t1 t2 eq_t1_t2.
rewrite -> eq_t1_t2.
reflexivity. }
Check (f_equal (mirror V t) t').
Check (f_equal (mirror V t) t' M_t_t').
assert (H_tmp := f_equal (mirror V t) t' M_t_t').
rewrite <- H_tmp.
Check (mirror_is_involutory mirror S_mirror V t).
rewrite -> (mirror_is_involutory mirror S_mirror V t).
reflexivity.
Qed.
(* ********** *)
Definition specification_of_number_of_leaves (number_of_leaves : forall V : Type, binary_tree V -> nat) : Prop :=
(forall (V : Type)
(v : V),
number_of_leaves V (Leaf V v) =
1)
/\
(forall (V : Type)
(t1 t2 : binary_tree V),
number_of_leaves V (Node V t1 t2) =
number_of_leaves V t1 + number_of_leaves V t2).
(* ***** *)
(* Exercise 09b *)
Proposition there_is_at_most_one_number_of_leaves_function :
forall number_of_leaves1 number_of_leaves2 : forall V : Type, binary_tree V -> nat,
specification_of_number_of_leaves number_of_leaves1 ->
specification_of_number_of_leaves number_of_leaves2 ->
forall (V : Type)
(t : binary_tree V),
number_of_leaves1 V t = number_of_leaves2 V t.
Proof.
Abort.
(* ***** *)
Definition specification_of_number_of_nodes (number_of_nodes : forall V : Type, binary_tree V -> nat) : Prop :=
(forall (V : Type)
(v : V),
number_of_nodes V (Leaf V v) =
0)
/\
(forall (V : Type)
(t1 t2 : binary_tree V),
number_of_nodes V (Node V t1 t2) =
S (number_of_nodes V t1 + number_of_nodes V t2)).
(* ***** *)
(* Exercise 09c *)
Proposition there_is_at_most_one_number_of_nodes_function :
forall number_of_nodes1 number_of_nodes2 : forall V : Type, binary_tree V -> nat,
specification_of_number_of_nodes number_of_nodes1 ->
specification_of_number_of_nodes number_of_nodes2 ->
forall (V : Type)
(t : binary_tree V),
number_of_nodes1 V t = number_of_nodes2 V t.
Proof.
Abort.
(* ***** *)
Theorem about_the_relative_number_of_leaves_and_nodes_in_a_tree :
forall number_of_leaves : forall V : Type, binary_tree V -> nat,
specification_of_number_of_leaves number_of_leaves ->
forall number_of_nodes : forall V : Type, binary_tree V -> nat,
specification_of_number_of_nodes number_of_nodes ->
forall (V : Type)
(t : binary_tree V),
number_of_leaves V t = S (number_of_nodes V t).
Proof.
intro number_of_leaves.
unfold specification_of_number_of_leaves.
intros [S_nol_Leaf S_nol_Node].
intro number_of_nodes.
unfold specification_of_number_of_nodes.
intros [S_non_Leaf S_non_Node].
Restart. (* with less clutter among the assumptions *)
intros nol S_nol non S_non V t.
induction t as [v | t1 IHt1 t2 IHt2].
- unfold specification_of_number_of_leaves in S_nol.
destruct S_nol as [S_nol_Leaf _].
unfold specification_of_number_of_nodes in S_non.
destruct S_non as [S_non_Leaf _].
Check (S_non_Leaf V v).
rewrite -> (S_non_Leaf V v).
Check (S_nol_Leaf V v).
exact (S_nol_Leaf V v).
- unfold specification_of_number_of_leaves in S_nol.
destruct S_nol as [_ S_nol_Node].
unfold specification_of_number_of_nodes in S_non.
destruct S_non as [_ S_non_Node].
Check (S_nol_Node V t1 t2).
rewrite -> (S_nol_Node V t1 t2).
Check (S_non_Node V t1 t2).
rewrite -> (S_non_Node V t1 t2).
rewrite -> IHt1.
rewrite -> IHt2.
Search (S _ + _).
Check (plus_Sn_m (non V t1) (S (non V t2))).
rewrite -> (plus_Sn_m (non V t1) (S (non V t2))).
Search (_ + S _ = _).
Search (_ = _ + S _).
Check (plus_n_Sm (non V t1) (non V t2)).
rewrite <- (plus_n_Sm (non V t1) (non V t2)).
reflexivity.
Restart.
intros nol S_nol non S_non.
Check binary_tree_ind.
intro V.
Check (binary_tree_ind
V).
Check (binary_tree_ind
V
(fun t : binary_tree V => nol V t = S (non V t))).
assert (wanted_Leaf :
forall v : V, nol V (Leaf V v) = S (non V (Leaf V v))).
{ intro v.
unfold specification_of_number_of_leaves in S_nol.
destruct S_nol as [S_nol_Leaf _].
unfold specification_of_number_of_nodes in S_non.
destruct S_non as [S_non_Leaf _].
Check (S_non_Leaf V v).
rewrite -> (S_non_Leaf V v).
Check (S_nol_Leaf V v).
exact (S_nol_Leaf V v). }
Check (binary_tree_ind
V
(fun t : binary_tree V => nol V t = S (non V t))
wanted_Leaf).
apply (binary_tree_ind
V
(fun t : binary_tree V => nol V t = S (non V t))
wanted_Leaf).
intros t1 IHt1 t2 IHt2.
unfold specification_of_number_of_leaves in S_nol.
destruct S_nol as [_ S_nol_Node].
unfold specification_of_number_of_nodes in S_non.
destruct S_non as [_ S_non_Node].
Check (S_nol_Node V t1 t2).
rewrite -> (S_nol_Node V t1 t2).
Check (S_non_Node V t1 t2).
rewrite -> (S_non_Node V t1 t2).
rewrite -> IHt1.
rewrite -> IHt2.
Search (S _ + _).
Check (plus_Sn_m (non V t1) (S (non V t2))).
rewrite -> (plus_Sn_m (non V t1) (S (non V t2))).
Search (_ + S _ = _).
Search (_ = _ + S _).
Check (plus_n_Sm (non V t1) (non V t2)).
rewrite <- (plus_n_Sm (non V t1) (non V t2)).
reflexivity.
Qed.
(* ********** *)
(* end of week-03_induction-over-binary-trees.v *)

79
cs3234/labs/week-03_the-exists-tactic.v Normal file
View File

@ -0,0 +1,79 @@
(* week-03_the-exists-tactic.v *)
(* LPP 2024 - CS3234 2023-2024, Sem2 *)
(* Olivier Danvy <danvy@yale-nus.edu.sg> *)
(* Version of 01 Feb 2024 *)
(* ********** *)
(* Paraphernalia: *)
Require Import Arith.
(* ********** *)
Lemma proving_an_existential_example_0 :
exists n : nat,
n = 0.
Proof.
exists 0.
reflexivity.
Qed.
(* ********** *)
Lemma proving_an_existential_example_1 :
forall n : nat,
exists m : nat,
S m = n + 1.
Proof.
intros n.
exists n.
Search (_ + S _).
Check (plus_n_Sm n 0).
rewrite <- (plus_n_Sm n 0).
Check Nat.add_0_r.
rewrite -> (Nat.add_0_r n).
reflexivity.
Qed.
(* ********** *)
Lemma proving_an_existential_example_2 :
forall n : nat,
exists f : nat -> nat,
f n = n + 1.
Proof.
intro n.
exists S.
rewrite <- (plus_n_Sm n 0).
rewrite -> (Nat.add_0_r n).
reflexivity.
Restart.
intro n.
exists (fun n => S n).
rewrite <- (plus_n_Sm n 0).
rewrite -> (Nat.add_0_r n).
reflexivity.
Restart.
intro n.
exists (fun n => n + 1).
reflexivity.
Qed.
Lemma proving_an_existential_example_3:
forall n : nat,
exists f : nat -> nat,
f n = n + 2.
Proof.
intro n.
exists (fun n => n + 2).
reflexivity.
Qed.
(* ********** *)
(* end of week-03_the-exists-tactic.v *)

204
cs3234/labs/week-03_the-rewrite-tactic.v Normal file
View File

@ -0,0 +1,204 @@
(* week-03_the-rewrite-tactic.v *)
(* LPP 2024 - CS3234 2023-2024, Sem2 *)
(* Olivier Danvy <danvy@yale-nus.edu.sg> *)
(* Version of 01 Feb 2024 *)
(* ********** *)
Require Import Arith Bool.
(* ********** *)
(* Rewriting from left to right in the current goal *)
Proposition p1 :
forall i j : nat,
i = j ->
forall f : nat -> nat,
f i = f j.
Proof.
intros i j H_i_j f.
rewrite <- H_i_j.
reflexivity.
Qed.
(* ********** *)
(* Rewriting a specific occurrence from left to right in the current goal *)
Proposition silly :
forall x y : nat,
x = y ->
x + x * y + (y + y) = y + y * x + (x + x).
Proof.
intros x y H_x_y.
rewrite -> H_x_y.
reflexivity.
Restart.
intros x y H_x_y.
rewrite -> H_x_y at 4.
rewrite -> H_x_y at 1.
rewrite -> H_x_y at 1.
rewrite -> H_x_y at 1.
rewrite -> H_x_y at 1.
reflexivity.
Restart.
intros x y H_x_y.
rewrite -> H_x_y at 4.
rewrite ->3 H_x_y at 1.
rewrite -> H_x_y.
reflexivity.
Qed.
Proposition p2 :
forall x : nat,
x = 0 ->
x = 1 ->
x <> x. (* i.e., not (x = x), or again ~(x = x), or again x = x -> False *)
Proof.
intros x H_x0 H_x1.
rewrite -> H_x0 at 1.
rewrite -> H_x1.
Search (0 <> S _).
Check (Nat.neq_0_succ 0).
exact (Nat.neq_0_succ 0).
Restart.
intros x H_x0 H_x1.
rewrite -> H_x1 at 2.
rewrite -> H_x0.
exact (Nat.neq_0_succ 0).
Qed.
(* ********** *)
(* Rewriting from left to right in an assumption *)
Proposition p3 : (* transitivity of Leibniz equality *)
forall a b c : nat,
a = b ->
b = c ->
a = c.
Proof.
intros a b c H_ab H_bc.
rewrite -> H_ab.
exact H_bc.
Restart.
intros a b c H_ab H_bc.
rewrite -> H_bc in H_ab.
exact H_ab.
Qed.
(* ********** *)
(* Rewriting a specific occurrence from left to right in an assumption *)
Proposition p4 :
forall x : nat,
x = 0 ->
x = 1 ->
x <> x. (* i.e., not (x = x), or again ~(x = x), or again x = x -> False *)
Proof.
unfold not.
intros x H_x0 H_x1 H_xx.
rewrite -> H_x0 in H_xx at 1.
rewrite -> H_x1 in H_xx.
Search (0 <> S _).
Check Nat.neq_0_succ 0.
assert (H_absurd := Nat.neq_0_succ 0).
unfold not in H_absurd.
Check (H_absurd H_xx).
exact (H_absurd H_xx).
Restart.
unfold not.
intros x H_x0 H_x1 H_xx.
rewrite -> H_x1 in H_xx at 2.
rewrite -> H_x0 in H_xx.
assert (H_absurd := Nat.neq_0_succ 0).
unfold not in H_absurd.
exact (H_absurd H_xx).
Qed.
(* ********** *)
(* Rewriting from right to left *)
Proposition p1' :
forall i j : nat,
i = j ->
forall f : nat -> nat,
f i = f j.
Proof.
intros i j H_i_j f.
rewrite <- H_i_j.
reflexivity.
Qed.
(* ********** *)
Check plus_Sn_m. (* : forall n m : nat, S n + m = S (n + m) *)
Check plus_n_Sm. (* : forall n m : nat, S (n + m) = n + S m *)
Proposition p5 :
forall i j : nat,
S i + j = i + S j.
Proof.
intros i j.
Check (plus_Sn_m i j).
rewrite -> (plus_Sn_m i j).
Check (plus_n_Sm i j).
rewrite <- (plus_n_Sm i j).
reflexivity.
Qed.
Proposition p6 :
forall n : nat,
0 + n = n + 0 ->
1 + n = n + 1.
Proof.
intros n H_n.
rewrite -> (plus_Sn_m 0 n).
rewrite <- (plus_n_Sm n 0).
rewrite -> H_n.
reflexivity.
Qed.
Proposition p7 :
forall n : nat,
0 + n = n + 0 ->
2 + n = n + 2.
Proof.
intros n H_n.
rewrite -> (plus_Sn_m 1 n).
rewrite <- (plus_n_Sm n 1).
Check (p6 n H_n).
rewrite -> (p6 n H_n).
reflexivity.
Qed.
Proposition p8 :
forall n : nat,
0 + n = n + 0 ->
3 + n = n + 3.
Proof.
intros n H_n.
rewrite -> (plus_Sn_m 2 n).
rewrite <- (plus_n_Sm n 2).
Check (p7 n H_n).
rewrite -> (p7 n H_n).
reflexivity.
Qed.
(* ********** *)
(* end of week-03_the-rewrite-tactic.v *)