From 14e30956322029305e1e305f37f2a4264dca1e6d Mon Sep 17 00:00:00 2001 From: Yadunand Prem Date: Tue, 13 Feb 2024 17:04:53 +0800 Subject: [PATCH] feat: 3234 week 3 --- cs3234/labs/week-03_specifications.v | 581 ++++++++++++++++++ ..._structural-induction-over-Peano-numbers.v | 134 ++++ ...3_structural-induction-over-binary-trees.v | 389 ++++++++++++ cs3234/labs/week-03_the-exists-tactic.v | 79 +++ cs3234/labs/week-03_the-rewrite-tactic.v | 204 ++++++ 5 files changed, 1387 insertions(+) create mode 100644 cs3234/labs/week-03_specifications.v create mode 100644 cs3234/labs/week-03_structural-induction-over-Peano-numbers.v create mode 100644 cs3234/labs/week-03_structural-induction-over-binary-trees.v create mode 100644 cs3234/labs/week-03_the-exists-tactic.v create mode 100644 cs3234/labs/week-03_the-rewrite-tactic.v diff --git a/cs3234/labs/week-03_specifications.v b/cs3234/labs/week-03_specifications.v new file mode 100644 index 0000000..2104864 --- /dev/null +++ b/cs3234/labs/week-03_specifications.v @@ -0,0 +1,581 @@ +(* week-03_specifications.v *) +(* LPP 2023 - CS3234 2023-2024, Sem2 *) +(* Olivier Danvy *) +(* 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 *) diff --git a/cs3234/labs/week-03_structural-induction-over-Peano-numbers.v b/cs3234/labs/week-03_structural-induction-over-Peano-numbers.v new file mode 100644 index 0000000..1a9ae20 --- /dev/null +++ b/cs3234/labs/week-03_structural-induction-over-Peano-numbers.v @@ -0,0 +1,134 @@ +(* week-03_structural-induction-over-Peano-numbers.v *) +(* LPP 2023 - CS3234 2023-2024, Sem2 *) +(* Olivier Danvy *) +(* 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 *) + diff --git a/cs3234/labs/week-03_structural-induction-over-binary-trees.v b/cs3234/labs/week-03_structural-induction-over-binary-trees.v new file mode 100644 index 0000000..4f65d36 --- /dev/null +++ b/cs3234/labs/week-03_structural-induction-over-binary-trees.v @@ -0,0 +1,389 @@ +(* week-03_induction-over-binary-trees.v *) +(* LPP 2023 - CS3234 2023-2024, Sem2 *) +(* Olivier Danvy *) +(* 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 *) diff --git a/cs3234/labs/week-03_the-exists-tactic.v b/cs3234/labs/week-03_the-exists-tactic.v new file mode 100644 index 0000000..f9de775 --- /dev/null +++ b/cs3234/labs/week-03_the-exists-tactic.v @@ -0,0 +1,79 @@ +(* week-03_the-exists-tactic.v *) +(* LPP 2024 - CS3234 2023-2024, Sem2 *) +(* Olivier Danvy *) +(* 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 *) diff --git a/cs3234/labs/week-03_the-rewrite-tactic.v b/cs3234/labs/week-03_the-rewrite-tactic.v new file mode 100644 index 0000000..6efc8a8 --- /dev/null +++ b/cs3234/labs/week-03_the-rewrite-tactic.v @@ -0,0 +1,204 @@ +(* week-03_the-rewrite-tactic.v *) +(* LPP 2024 - CS3234 2023-2024, Sem2 *) +(* Olivier Danvy *) +(* 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 *)