feat: list_length with fold left and right

cs2109s/labs/final/final.py

@@ -16,6 +16,7 @@ from torch import nn
 import numpy as np
 import torch
 import os
+from torchvision.transforms.functional import equalize
 
 class CNN3D(nn.Module):
     def __init__(self, hidden_size=32, dropout=0.0):
@@ -27,7 +28,7 @@ class CNN3D(nn.Module):
         self.maxpool = nn.MaxPool3d(kernel_size=2, stride=2)
         self.fc1 = nn.Linear(hidden_size*32, 256)  # Calculate input size based on output from conv3
         self.fc2 = nn.Linear(256, 6)
-        self.dropout = nn.Dropout(dropout)
+        # self.dropout = nn.Dropout(dropout)
 
     def forward(self, x):
         x = self.conv1(x)
@@ -37,7 +38,7 @@ class CNN3D(nn.Module):
         x = self.conv2(x)
         x = self.relu(x)
         x = self.maxpool(x)
-        x = self.dropout(x)
+        # x = self.dropout(x)
 
         x = x.view(x.size(0), -1)  # Flatten features for fully connected layers
         x = self.fc1(x)
@@ -56,17 +57,16 @@ def train(model, criterion, optimizer, loader, epochs=5):
         print(f'Epoch {epoch}, Loss: {loss.item()}')
     return model
 
-
-
-
 class Model():
-    def __init__(self, batch_size=8,lr=0.001,epochs=10, dropout=0.0, hidden_size=32):
+    def __init__(self, batch_size=64,lr=0.001,epochs=5, dropout=0.0, hidden_size=32, n_samples=900):
+        print(batch_size, epochs, lr, dropout, hidden_size, n_samples)
         self.batch_size = batch_size
         self.lr = lr
         self.epochs = epochs
         self.model = CNN3D(dropout=dropout, hidden_size=hidden_size)
         self.criterion = nn.CrossEntropyLoss()
         self.optimizer = torch.optim.Adam(self.model.parameters(), lr=self.lr)
+        self.n_samples = n_samples
 
     def fit(self, X, y):
         X, y = self.process_data(X, y)
@@ -81,31 +81,25 @@ class Model():
             tensor_videos = torch.tensor(X, dtype=torch.float32)
             # Clip values to 0 and 255
             tensor_videos = np.clip(tensor_videos, 0, 255)
-            # TEMP
-            threshold = 180
-            tensor_videos[tensor_videos > threshold] = 255
-            tensor_videos[tensor_videos < threshold] = 0
-            # END TEMP
 
             # Replace NaNs in each frame, with the average of the frame. This was generated with GPT
             for i in range(tensor_videos.shape[0]):
                 for j in range(tensor_videos.shape[1]):
                     tensor_videos[i][j][torch.isnan(tensor_videos[i][j])] = torch.mean(
                         tensor_videos[i][j][~torch.isnan(tensor_videos[i][j])])
-            X = torch.Tensor(tensor_videos.unsqueeze(1))
-            result = self.model(X)
+            # tensor_videos = torch.Tensor(tensor_videos).to(torch.uint8).reshape(-1, 1, 16, 16)
+            # tensor_videos = equalize(tensor_videos).float().reshape(-1, 1, 6, 16, 16)
+            tensor_videos = torch.Tensor(tensor_videos).reshape(-1, 1, 6, 16, 16)
+            # some funky code to make the features more prominent
+
+            result = self.model(tensor_videos)
         return torch.max(result, dim=1)[1].numpy()
-    def process_data(self, X, y, n_samples=600):
+    def process_data(self, X, y):
         y = np.array(y)
         X = np.array([video[:6] for video in X])
         tensor_videos = torch.tensor(X, dtype=torch.float32)
         # Clip values to 0 and 255
         tensor_videos = np.clip(tensor_videos, 0, 255)
-        # TEMP
-        threshold = 180
-        tensor_videos[tensor_videos > threshold] = 255
-        tensor_videos[tensor_videos < threshold] = 0
-        # END TEMP
 
         # Replace NaNs in each frame, with the average of the frame. This was generated with GPT
         for i in range(tensor_videos.shape[0]):
@@ -118,13 +112,19 @@ class Model():
         indices = [np.argwhere(y == i).squeeze(1) for i in range(6)]
         # Get the number of samples to take for each class
         # Get the indices of the samples to take
-        indices_to_take = [np.random.choice(indices[i], n_samples, replace=True) for i in range(6)]
+        indices_to_take = [np.random.choice(indices[i], self.n_samples, replace=True) for i in range(6)]
         # Concatenate the indices
         indices_to_take = np.concatenate(indices_to_take)
         # Select the samples
-        tensor_videos = tensor_videos[indices_to_take].unsqueeze(1)
+        tensor_videos = tensor_videos[indices_to_take]
+
+        tensor_videos = torch.Tensor(tensor_videos).reshape(-1, 1, 6, 16, 16)
+        # Reshape the tensor to int for image processing
+        # tensor_videos = torch.Tensor(tensor_videos).to(torch.uint8).reshape(-1, 1, 16, 16)
+        # tensor_videos = equalize(tensor_videos).float().reshape(-1, 1, 6, 16, 16)
+
         y = y[indices_to_take]
-        return torch.Tensor(tensor_videos), torch.Tensor(y).long()
+        return tensor_videos, torch.Tensor(y).long()
 
 
 X_train, X_test, y_train, y_test = train_test_split(X, y, test_size=0.1)

cs2109s/labs/final/main.ipynb

@@ -315,12 +315,12 @@
   },
   {
    "cell_type": "code",
-   "execution_count": 72,
+   "execution_count": 10,
    "id": "a44b7aa4",
    "metadata": {
     "ExecuteTime": {
-     "end_time": "2024-04-28T12:00:17.228662Z",
-     "start_time": "2024-04-28T12:00:17.209494Z"
+     "end_time": "2024-04-28T12:27:25.926991Z",
+     "start_time": "2024-04-28T12:27:25.917322Z"
     }
    },
    "outputs": [],
@@ -406,8 +406,8 @@
     "    def fit(self, X, y):\n",
     "        X, y = process_data(X, y)\n",
     "        train_dataset = torch.utils.data.TensorDataset(X, y)\n",
-    "        train_loader = torch.utils.data.DataLoader(train_dataset, batch_size=128, shuffle=True)\n",
-    "        train(self.model, self.criterion, self.optimizer, train_loader, 10)\n",
+    "        train_loader = torch.utils.data.DataLoader(train_dataset, batch_size=64, shuffle=True)\n",
+    "        train(self.model, self.criterion, self.optimizer, train_loader, 20)\n",
     "\n",
     "    def predict(self, X):\n",
     "        self.model.eval()\n",
@@ -438,12 +438,12 @@
   },
   {
    "cell_type": "code",
-   "execution_count": 73,
+   "execution_count": 2,
    "id": "4f4dd489",
    "metadata": {
     "ExecuteTime": {
-     "end_time": "2024-04-28T12:00:19.363096Z",
-     "start_time": "2024-04-28T12:00:19.352424Z"
+     "end_time": "2024-04-28T12:09:46.115322Z",
+     "start_time": "2024-04-28T12:09:45.631452Z"
     }
    },
    "outputs": [],
@@ -458,12 +458,12 @@
   },
   {
    "cell_type": "code",
-   "execution_count": 74,
+   "execution_count": 3,
    "id": "3064e0ff",
    "metadata": {
     "ExecuteTime": {
-     "end_time": "2024-04-28T12:00:20.265060Z",
-     "start_time": "2024-04-28T12:00:20.234748Z"
+     "end_time": "2024-04-28T12:09:47.340881Z",
+     "start_time": "2024-04-28T12:09:47.317719Z"
     }
    },
    "outputs": [],
@@ -477,12 +477,12 @@
   },
   {
    "cell_type": "code",
-   "execution_count": 75,
+   "execution_count": 12,
    "id": "27c9fd10",
    "metadata": {
     "ExecuteTime": {
-     "end_time": "2024-04-28T12:00:37.185569Z",
-     "start_time": "2024-04-28T12:00:22.239036Z"
+     "end_time": "2024-04-28T12:28:29.269402Z",
+     "start_time": "2024-04-28T12:28:02.494602Z"
     }
    },
    "outputs": [
@@ -490,19 +490,29 @@
      "name": "stdout",
      "output_type": "stream",
      "text": [
-      "Epoch 0, Loss: 0.7495917081832886\n",
-      "Epoch 1, Loss: 0.42713749408721924\n",
-      "Epoch 2, Loss: 0.21424821019172668\n",
-      "Epoch 3, Loss: 0.02086367830634117\n",
-      "Epoch 4, Loss: 0.005386564414948225\n",
-      "Epoch 5, Loss: 0.00319607718847692\n",
-      "Epoch 6, Loss: 0.007663913071155548\n",
-      "Epoch 7, Loss: 0.003004509722813964\n",
-      "Epoch 8, Loss: 0.0044013322331011295\n",
-      "Epoch 9, Loss: 0.0016760551370680332\n",
-      "F1 Score (macro): 0.75\n",
-      "CPU times: user 57.8 s, sys: 1min 12s, total: 2min 10s\n",
-      "Wall time: 14.9 s\n"
+      "Epoch 0, Loss: 0.5610745549201965\n",
+      "Epoch 1, Loss: 0.22023160755634308\n",
+      "Epoch 2, Loss: 0.03679683431982994\n",
+      "Epoch 3, Loss: 0.009054183959960938\n",
+      "Epoch 4, Loss: 0.0021134500857442617\n",
+      "Epoch 5, Loss: 0.002705463906750083\n",
+      "Epoch 6, Loss: 0.0045105633325874805\n",
+      "Epoch 7, Loss: 0.001958428416401148\n",
+      "Epoch 8, Loss: 0.0010891605634242296\n",
+      "Epoch 9, Loss: 0.0010821395553648472\n",
+      "Epoch 10, Loss: 0.0007317279814742506\n",
+      "Epoch 11, Loss: 0.0006673489115200937\n",
+      "Epoch 12, Loss: 0.00047141974209807813\n",
+      "Epoch 13, Loss: 0.00024128056247718632\n",
+      "Epoch 14, Loss: 0.0003150832490064204\n",
+      "Epoch 15, Loss: 0.0004005862574558705\n",
+      "Epoch 16, Loss: 0.00024190203112084419\n",
+      "Epoch 17, Loss: 0.0004451812419574708\n",
+      "Epoch 18, Loss: 0.000376795680494979\n",
+      "Epoch 19, Loss: 0.0003616203321143985\n",
+      "F1 Score (macro): 0.65\n",
+      "CPU times: user 2min 33s, sys: 255 ms, total: 2min 34s\n",
+      "Wall time: 26.8 s\n"
      ]
     }
    ],

cs3234/labs/question-for-Yadunand-Prem-midterm.txt

@@ -0,0 +1,85 @@
+% question-for-Yadunand-Prem.txt
+% CS3234, Fri 05 Apr 2024
+
+%%%%%%%%%%
+
+This oral exam is a continuation of the midterm project. 
+So, make a copy of midterm_project.v (naming it midterm_project_copy-for-oral-exam.v)
+and start editing this file after
+
+(* end of midterm_project.v *)
+
+%%%%%%%%%%
+
+The goal of this oral exam is to revisit
+
+  Proposition list_reverse_acc_and_list_append_commute_with_each_other :
+    forall (V : Type)
+           (v1s v2s: list V),
+      list_append V (list_reverse_acc V v2s nil) (list_reverse_acc V v1s nil) =
+      list_reverse_acc V (list_append V v1s v2s) nil.
+
+So, copy the following proposition at the very end of midterm_project_copy-for-oral-exam.v:
+
+  Proposition a_generalized_alternative :
+    forall (V : Type)
+           (v1s v2s v3s : list V),
+      list_reverse_acc V (list_append V v1s v2s) v3s
+      = nil.
+
+%%%%%
+
+a. The first thing to do is to figure out what to put instead of nil on the right-hand side,
+   so that the equality holds.
+   We (in the sense of you) are going to do that empirically by testing.
+   To this end, write:
+
+     Proof.
+       Compute (let V := nat in
+                let v1s := 11 :: 12 :: nil in
+                let v2s := 21 :: 22 :: nil in
+                let v3s := 31 :: 32 :: nil in
+                list_reverse_acc V (list_append V v1s v2s) v3s
+                = nil).
+      
+   Then, replace nil on the right-hand-side by an expression that does not use list_append
+   but that only uses two occurrences of list_reverse_acc,
+   and that is such that the equality holds.
+   (Let us name this expression as YOUR_EXPRESSION.)
+
+   Hint: use "(list_reverse_acc V ... ...)" as an accumulator for list_reverse_acc.
+
+b. To make sure, write:
+
+       Compute (let V := nat in
+                let v1s := 11 :: 12 :: nil in
+                let v2s := 21 :: 22 :: nil in
+                let v3s := 31 :: 32 :: nil in
+                eqb_list
+                  nat
+                  Nat.eqb
+                  (list_reverse_acc V (list_append V v1s v2s) v3s)
+                  YOUR_EXPRESSION).
+
+    Verify that the result of this computation is true.
+    If it is false, then go back to a. and revise YOUR_EXPRESSION
+    until the result of the computation just above is true.
+
+c. Prove this equality by induction.
+
+d. Time permitting, write:
+
+       Restart.
+
+   Prove these equalities not by induction,
+   but using the many properties you have proved earlier in the file,
+   e.g., about_list_reverse_acc_and_append,
+   list_reverse_acc_and_list_append_commute_with_each_other,
+   list_append_is_associative,
+   etc.
+   (Maybe you will need to state and prove more similar properties to carry our this proof,
+   maybe not, who knows, this is an exploration.)
+
+%%%%%%%%%%
+
+% end of question-for-Yadunand-Prem.txt

cs3234/labs/question-for-Yadunand.v

@@ -0,0 +1,621 @@
+(* question-for-Yadunand.v *)
+(* CS3234 oral exam *)
+(* Sun 05 May 2024 *)
+
+(* ********** *)
+
+(* Your oral exam is about primitive recursion for Peano numbers. *)
+
+(* ********** *)
+
+Ltac fold_unfold_tactic name := intros; unfold name; fold name; reflexivity.
+
+Require Import Arith Bool List.
+
+(* ********** *)
+
+(* Reminder:
+   Any function that is expressible as an instance of nat_fold_right is said to be "primitive iterative". *)
+
+Fixpoint nat_fold_right (V : Type) (zero_case : V) (succ_case : V -> V) (n : nat) : V :=
+  match n with
+    O =>
+    zero_case
+  | S n' =>
+    succ_case (nat_fold_right V zero_case succ_case n')
+  end.
+
+(* Definition:
+   Any function that is expressible as an instance of nat_parafold_right is said to be "primitive recursive". *)
+
+Fixpoint nat_parafold_right (V : Type) (zero_case : V) (succ_case : nat -> V -> V) (n : nat) : V := match n with
+    O =>
+    zero_case
+  | S n' =>
+    succ_case n' (nat_parafold_right V zero_case succ_case n')
+  end.
+
+Lemma fold_unfold_nat_parafold_right_O :
+  forall (V : Type)
+         (zero_case : V)
+         (succ_case : nat -> V -> V),
+    nat_parafold_right V zero_case succ_case 0 =
+    zero_case.
+Proof.
+  fold_unfold_tactic nat_parafold_right.
+Qed.
+
+Lemma fold_unfold_nat_parafold_right_S :
+  forall (V : Type)
+         (zero_case : V)
+         (succ_case : nat -> V -> V)
+         (n' : nat),
+    nat_parafold_right V zero_case succ_case (S n') =
+    succ_case n' (nat_parafold_right V zero_case succ_case n').
+Proof.
+  fold_unfold_tactic nat_parafold_right.
+Qed.
+
+(* ***** *)
+
+Fixpoint nat_parafold_left (V : Type) (zero_case : V) (succ_case : nat -> V -> V) (n : nat) : V :=
+  match n with
+    O =>
+    zero_case
+  | S n' =>
+    nat_parafold_left V (succ_case n' zero_case) succ_case n'    
+  end.
+
+Lemma fold_unfold_nat_parafold_left_O :
+  forall (V : Type)
+         (zero_case : V)
+         (succ_case : nat -> V -> V),
+    nat_parafold_left V zero_case succ_case 0 =
+    zero_case.
+Proof.
+  fold_unfold_tactic nat_parafold_left.
+Qed.
+
+Lemma fold_unfold_nat_parafold_left_S :
+  forall (V : Type)
+         (zero_case : V)
+         (succ_case : nat -> V -> V)
+         (n' : nat),
+    nat_parafold_left V zero_case succ_case (S n') =
+    nat_parafold_left V (succ_case n' zero_case) succ_case n'.
+Proof.
+  fold_unfold_tactic nat_parafold_left.
+Qed.
+
+(* ********** *)
+
+Definition test_fac (candidate: nat -> nat) : bool :=
+  (Nat.eqb (candidate 0) 1)
+  &&
+  (Nat.eqb (candidate 5) 120).
+
+(* ***** *)
+
+(* Recursive implementation of the factorial function: *)
+
+Fixpoint r_fac (n : nat) : nat :=
+  match n with
+    O =>
+    1
+  | S n' =>
+    S n' * r_fac n'
+  end.
+
+Compute (test_fac r_fac).
+
+(* 1.a Implement r_fac as an instance of nat_parafold_right: *)
+
+Definition r_fac_right (n : nat) : nat :=
+  nat_parafold_right nat 1 (fun n' ih => (S n') * ih) n.
+
+(* 1.b Test your implementation. *)
+Compute (test_fac r_fac).
+
+(* 1.c Prove that r_fac and r_fac_right are equivalent. *)
+
+Lemma fold_unfold_r_fac_O :
+  r_fac 0 = 1.
+Proof.
+  fold_unfold_tactic r_fac.
+Qed.
+Lemma fold_unfold_r_fac_S :
+  forall (n' : nat),
+    r_fac (S n') = S n' * r_fac n'.
+Proof.
+  fold_unfold_tactic r_fac.
+Qed.
+
+Lemma about_r_fac_and_r_fac_right :
+  forall (n : nat),
+    r_fac n = nat_parafold_right nat 1 (fun n' ih : nat => S n' * ih) n.
+Proof.
+  intro n.
+  induction n as [ | n' IHn' ].
+  - rewrite -> fold_unfold_r_fac_O.
+    rewrite -> fold_unfold_nat_parafold_right_O.
+    reflexivity.
+  - rewrite -> fold_unfold_r_fac_S.
+    rewrite -> fold_unfold_nat_parafold_right_S.
+    rewrite <- IHn'.
+    reflexivity.
+Qed.
+
+Theorem r_fac_and_r_fac_right_are_equivalent :
+  forall (n : nat),
+    r_fac n = r_fac_right n.
+Proof.
+  intro n.
+  unfold r_fac_right.
+  exact (about_r_fac_and_r_fac_right n).
+Qed.
+
+(* ***** *)
+
+(* Tail-recursive implementation of the factorial function: *)
+
+Fixpoint tr_fac_acc (n a : nat) : nat :=
+  match n with
+    O =>
+    a
+  | S n' =>
+    tr_fac_acc n' (S n' * a)
+  end.
+
+Lemma fold_unfold_tr_fac_acc_O :
+  forall (a : nat),
+  tr_fac_acc 0 a = a.
+Proof.
+  fold_unfold_tactic r_fac.
+Qed.
+
+Lemma fold_unfold_tr_fac_acc_S :
+  forall (n' a : nat),
+    tr_fac_acc (S n') a = tr_fac_acc n' (S n' * a).
+Proof.
+  fold_unfold_tactic r_fac.
+Qed.
+
+Definition tr_fac (n : nat) : nat :=
+  tr_fac_acc n 1.
+
+Compute (test_fac tr_fac).
+
+(* 2.a Implement tr_fac as an instance of nat_parafold_left: *)
+
+Definition tr_fac_left (n : nat) : nat :=
+  nat_parafold_left nat 1 (fun n' a => S n' * a) n.
+
+(* 2.b Test your implementation. *)
+
+Compute (test_fac tr_fac_left).
+
+(* 2.c Prove that tr_fac and tr_fac_left are equivalent. *)
+(* Lemma about_tr_fac_acc : *)
+(*   forall (n a : nat), *)
+(*     tr_fac_acc n a = (tr_fac_acc n 1) * a. *)
+(* Proof. *)
+(*   intros n. *)
+(*   induction n as [ | n' IHn' ]. *)
+(*   - intro a. *)
+(*     rewrite -> fold_unfold_tr_fac_acc_O. *)
+(*     rewrite -> fold_unfold_tr_fac_acc_O. *)
+(*     rewrite -> Nat.mul_1_l. *)
+(*     reflexivity. *)
+(*   - intro a. *)
+(*     rewrite -> fold_unfold_tr_fac_acc_S. *)
+(*     rewrite -> (IHn' (S (S n') * a)). *)
+(*     rewrite ->  *)
+
+
+Lemma about_tr_fac_and_tr_fac_left :
+  forall (n : nat),
+    tr_fac_acc n 1 = nat_parafold_left nat 1 (fun n' a : nat => S n' * a) n.
+  Proof.
+    intro n.
+    induction n as [ | n' IHn' ].
+    - rewrite -> fold_unfold_tr_fac_acc_O.
+      rewrite -> fold_unfold_nat_parafold_left_O.
+      reflexivity.
+    - rewrite -> fold_unfold_tr_fac_acc_S.
+      rewrite -> fold_unfold_nat_parafold_left_S.
+      rewrite -> Nat.mul_1_r.
+    Abort.
+
+Lemma about_tr_fac_and_tr_fac_left :
+  forall (n a: nat),
+    tr_fac_acc n a = nat_parafold_left nat a (fun n' a : nat => S n' * a) n.
+Proof.
+  intro n.
+  induction n as [ | n' IHn' ].
+  - intro a.
+    rewrite -> fold_unfold_tr_fac_acc_O.
+    rewrite -> fold_unfold_nat_parafold_left_O.
+    reflexivity.
+  - intro a.
+    rewrite -> fold_unfold_tr_fac_acc_S.
+    rewrite -> fold_unfold_nat_parafold_left_S.
+    exact (IHn' (S n' * a)).
+Qed.
+
+Theorem tr_fac_and_tr_fac_left_are_equivalent :
+  forall (n : nat),
+    tr_fac n = tr_fac_left n.
+Proof.
+  intro n.
+  unfold tr_fac.
+  unfold tr_fac_left.
+  exact (about_tr_fac_and_tr_fac_left n 1).
+Qed.
+
+
+(* ********** *)
+
+Definition test_Sigma (candidate: nat -> (nat -> nat) -> nat) : bool :=
+  (Nat.eqb (candidate 0 (fun n => S (2 * n))) 1)
+  &&
+  (Nat.eqb (candidate 1 (fun n => S (2 * n))) 4)
+  &&
+  (Nat.eqb (candidate 2 (fun n => S (2 * n))) 9)
+  &&
+  (Nat.eqb (candidate 3 (fun n => S (2 * n))) 16).
+
+(* ***** *)
+
+(* Recursive implementation of the summation function: *)
+
+Fixpoint r_Sigma (n : nat) (f : nat -> nat) : nat :=
+  match n with
+    O =>
+    f 0
+  | S n' =>
+    (r_Sigma n' f) + f (S n')
+  end.
+
+Compute (test_Sigma r_Sigma).
+
+(* 3.a Implement r_Sigma as an instance of nat_parafold_right: *)
+
+Definition r_Sigma_right (n : nat) (f : nat -> nat) : nat :=
+  nat_parafold_right
+    nat
+    (f 0)
+    (fun n' ih => (ih + f (S n')))
+    n.
+
+(* 3.b Test your implementation. *)
+
+Compute (test_Sigma r_Sigma_right).
+
+(* 3.c Prove that r_Sigma and r_Sigma_right are equivalent. *)
+
+Lemma fold_unfold_r_Sigma_O :
+  forall (f : nat -> nat),
+    r_Sigma O f = f 0.
+Proof.
+  fold_unfold_tactic r_Sigma.
+Qed.
+Lemma fold_unfold_r_Sigma_S :
+  forall (n' : nat)
+    (f : nat -> nat),
+    r_Sigma (S n') f = (r_Sigma n' f) + f (S n').
+Proof.
+  fold_unfold_tactic r_Sigma.
+Qed.
+
+Lemma about_r_Sigma_and_r_Sigma_right :
+  forall (n : nat)
+    (f : nat -> nat),
+    r_Sigma n f = nat_parafold_right nat (f 0) (fun n' ih : nat => ih + f (S n')) n.
+Proof.
+  intros n f.
+  induction n as [ | n' IHn' ].
+  - rewrite -> fold_unfold_r_Sigma_O.
+    rewrite -> fold_unfold_nat_parafold_right_O.
+    reflexivity.
+  - rewrite -> fold_unfold_r_Sigma_S.
+    rewrite -> fold_unfold_nat_parafold_right_S.
+    rewrite <- IHn'.
+    reflexivity.
+Qed.
+
+Theorem r_Sigma_and_r_Sigma_right_are_equivalent :
+  forall (n : nat)
+    (f : nat -> nat),
+    r_Sigma n f = r_Sigma_right n f.
+Proof.
+  intros n f.
+  unfold r_Sigma_right.
+  exact (about_r_Sigma_and_r_Sigma_right n f).
+Qed.
+
+(* ***** *)
+
+(* Tail-recursive implementation of the summation function: *)
+
+Fixpoint tr_Sigma_acc (n : nat) (f : nat -> nat) (a : nat) : nat :=
+  match n with
+    O =>
+    a
+  | S n' =>
+    tr_Sigma_acc n' f (a + f (S n'))
+  end.
+
+Lemma fold_unfold_tr_Sigma_acc_O :
+  forall (f : nat -> nat)
+    (a : nat),
+    tr_Sigma_acc 0 f a = a.
+Proof.
+  fold_unfold_tactic tr_Sigma_acc.
+Qed.
+Lemma fold_unfold_tr_Sigma_acc_S :
+  forall (n' : nat)
+    (f : nat -> nat)
+    (a : nat),
+    tr_Sigma_acc (S n') f a = tr_Sigma_acc n' f (a + f (S n')).
+Proof.
+  fold_unfold_tactic tr_Sigma_acc.
+Qed.
+
+Definition tr_Sigma (n : nat) (f : nat -> nat) : nat :=
+  tr_Sigma_acc n f (f 0).
+
+Compute (test_Sigma tr_Sigma).
+
+(* 4.a Implement tr_Sigma as an instance of nat_parafold_left: *)
+
+Definition tr_Sigma_left (n : nat) (f : nat -> nat) : nat :=
+  nat_parafold_left nat (f 0) (fun n' a => a + f (S n')) n.
+
+
+(* 4.b Test your implementation. *)
+
+Compute (test_Sigma tr_Sigma_left).
+
+(* 4.c Prove that tr_Sigma and tr_Sigma_left are equivalent. *)
+
+Lemma about_tr_Sigma_and_tr_Sigma_left :
+  forall (n : nat)
+    (f : nat -> nat),
+    tr_Sigma_acc n f (f 0) = nat_parafold_left nat (f 0) (fun n' a : nat => a + f (S n')) n.
+Proof.
+Abort.
+
+Lemma about_tr_Sigma_and_tr_Sigma_left :
+  forall (n: nat)
+    (f : nat -> nat)
+    (a : nat),
+    tr_Sigma_acc n f a = nat_parafold_left nat a (fun n' a : nat => a + f (S n')) n.
+Proof.
+  intros n f.
+  induction n as [ | n' IHn' ].
+  - intros a.
+    rewrite -> (fold_unfold_tr_Sigma_acc_O f a).
+    rewrite -> fold_unfold_nat_parafold_left_O.
+    reflexivity.
+  - intros a.
+    rewrite -> (fold_unfold_tr_Sigma_acc_S n' f a).
+    rewrite -> fold_unfold_nat_parafold_left_S.
+    exact (IHn' (a + f (S n'))).
+Qed.
+
+Theorem tr_Sigma_and_tr_Sigma_left_are_equivalent :
+  forall (n : nat)
+    (f : nat -> nat),
+    tr_Sigma n f = tr_Sigma_left n f.
+Proof.
+  intros n f.
+  unfold tr_Sigma,tr_Sigma_left.
+  exact (about_tr_Sigma_and_tr_Sigma_left n f (f 0)).
+Qed.
+(* ********** *)
+
+(* 5. Taking inspiration from the theorem about folding left and right over lists in the midterm project,
+      state and admit a similar theorem about parafolding left and right over Peano numbers. *)
+
+(* Theorem folding_left_and_right_over_lists : *)
+(*   forall (V W : Type) *)
+(*          (cons_case : V -> W -> W), *)
+(*     is_left_permutative V W cons_case -> *)
+(*     forall (nil_case : W) *)
+(*            (vs : list V), *)
+(*       list_fold_left  V W nil_case cons_case vs = *)
+(*       list_fold_right V W nil_case cons_case vs. *)
+(* Proof. *)
+(*   intros V W cons_case. *)
+(*   unfold is_left_permutative. *)
+(*   intros H_left_permutative nil_case vs. *)
+(*   induction vs as [ | v' vs' IHvs']. *)
+(*   - rewrite -> (fold_unfold_list_fold_left_nil  V W nil_case cons_case). *)
+(*     rewrite -> (fold_unfold_list_fold_right_nil V W nil_case cons_case). *)
+(*     reflexivity. *)
+(*   - rewrite -> (fold_unfold_list_fold_left_cons  V W nil_case cons_case v' vs'). *)
+(*     rewrite -> (fold_unfold_list_fold_right_cons V W nil_case cons_case v' vs'). *)
+(*     rewrite <- IHvs'. *)
+(*     rewrite -> (about_list_fold_left_with_left_permutative_cons_case *)
+(*                  V W cons_case H_left_permutative nil_case v' vs'). *)
+(*     reflexivity. *)
+(* Qed. *)
+(* Definition is_left_permutative (V W : Type) (op2 : V -> W -> W) := *)
+(*   forall (v1 v2 : V) *)
+(*          (w : W), *)
+(*     op2 v1 (op2 v2 w) = op2 v2 (op2 v1 w). *)
+(* ********** *)
+
+Definition is_left_permutative (V : Type) (op2 : nat -> V -> V) :=
+  forall (n1 n2 : nat)
+    (v : V),
+    op2 n1 (op2 n2 v) = op2 n2 (op2 n1 v).
+
+Lemma about_parafolding_l_over_peano_numbers :
+  forall (V: Type)
+    (succ_case : nat -> V -> V),
+    is_left_permutative V succ_case ->
+    forall (n : nat)
+      (zero_case : V),
+  nat_parafold_left V (succ_case n zero_case) succ_case n =
+  succ_case n (nat_parafold_left V zero_case succ_case n).
+Proof.
+  intros V succ_case H_is_left_permutative n.
+  unfold is_left_permutative in H_is_left_permutative.
+  induction n as [| n' IHn'].
+  - intro zero_case.
+    rewrite -> 2 fold_unfold_nat_parafold_left_O.
+    reflexivity.
+  - intro zero_case.
+    rewrite -> fold_unfold_nat_parafold_left_S.
+    rewrite ->H_is_left_permutative.
+    Abort. (* The lemma I stated here is a bit wrong. *)
+
+Lemma about_parafolding_left_over_peano_numbers :
+  forall (V: Type)
+    (succ_case : nat -> V -> V),
+    is_left_permutative V succ_case ->
+    forall (n m : nat)
+      (zero_case : V),
+  nat_parafold_left V (succ_case m zero_case) succ_case n =
+  succ_case m (nat_parafold_left V zero_case succ_case n).
+Proof.
+  intros V succ_case H_is_left_permutative n m.
+  unfold is_left_permutative in H_is_left_permutative.
+  induction n as [| n' IHn'].
+  - intros zero_case.
+    rewrite -> 2 fold_unfold_nat_parafold_left_O.
+    reflexivity.
+  - intros zero_case.
+    rewrite -> fold_unfold_nat_parafold_left_S.
+    rewrite -> H_is_left_permutative.
+    rewrite -> (IHn' (succ_case n' zero_case)).
+    rewrite -> fold_unfold_nat_parafold_left_S.
+    reflexivity.
+Qed.
+
+Lemma about_parafolding_right_over_peano_numbers :
+  forall (V : Type)
+    (succ_case : nat -> V -> V),
+    is_left_permutative V succ_case ->
+    forall (n m : nat)
+      (zero_case : V),
+      nat_parafold_right V (succ_case m zero_case) succ_case n =
+        succ_case m (nat_parafold_right V zero_case succ_case n).
+Proof.
+  intros V succ_case H_left_permutative n m zero_case.
+  unfold is_left_permutative in H_left_permutative.
+  induction n as [ | n' IHn' ].
+  - rewrite -> 2 fold_unfold_nat_parafold_right_O.
+    reflexivity.
+  - rewrite -> 2 fold_unfold_nat_parafold_right_S.
+    rewrite -> H_left_permutative.
+    rewrite -> IHn'.
+    reflexivity.
+Qed.
+Theorem parafolding_left_and_right_over_peano_numbers :
+  forall (V : Type)
+    (succ_case : nat -> V -> V),
+    is_left_permutative V succ_case ->
+    forall (n : nat)
+      (zero_case : V),
+      nat_parafold_left V zero_case succ_case n = nat_parafold_right V zero_case succ_case n.
+Proof.
+  intros V succ_case H_left_permutative n zero_case.
+  (* Generalizing the accumulator(?) *)
+  induction n as [ | n' IHn' ].
+  - rewrite -> fold_unfold_nat_parafold_left_O.
+    rewrite -> fold_unfold_nat_parafold_right_O.
+    reflexivity.
+  - rewrite -> fold_unfold_nat_parafold_left_S.
+    rewrite -> fold_unfold_nat_parafold_right_S.
+    rewrite <- IHn'.
+    Check (about_parafolding_left_over_peano_numbers V succ_case H_left_permutative n' n' zero_case).
+    exact (about_parafolding_left_over_peano_numbers V succ_case H_left_permutative n' n' zero_case).
+    Restart.
+    intros V succ_case H_left_permutative n.
+    (* Generalizing the accumulator(?) *)
+    induction n as [ | n' IHn' ].
+  - intro zero_case.
+    rewrite -> fold_unfold_nat_parafold_left_O.
+    rewrite -> fold_unfold_nat_parafold_right_O.
+    reflexivity.
+  - intro zero_case.
+    rewrite -> fold_unfold_nat_parafold_right_S.
+    rewrite -> fold_unfold_nat_parafold_left_S.
+    rewrite -> (IHn' (succ_case n' zero_case)).
+    exact (about_parafolding_right_over_peano_numbers
+             V
+             succ_case
+             H_left_permutative
+             n'
+             n'
+             zero_case
+          ).
+Qed.
+
+(* 6. As a corollary of your similar theorem,
+      prove that tr_fac_left and r_fac_right are equivalent
+      and that tr_Sigma_left and r_Sigma_right are equivalent. *)
+
+Lemma succ_case_of_fac_is_left_permutative :
+  is_left_permutative nat (fun n' a : nat => S n' * a).
+Proof.
+  unfold is_left_permutative.
+  intros n1 n2 v.
+  rewrite -> Nat.mul_shuffle3.
+  reflexivity.
+Qed.
+
+Corollary tr_fac_left_and_r_fac_right_are_equivalent :
+  forall (n : nat),
+    tr_fac_left n = r_fac_right n.
+Proof.
+  intros n.
+  unfold tr_fac_left.
+  unfold r_fac_right.
+  exact (parafolding_left_and_right_over_peano_numbers
+           nat
+           (fun n' a : nat => S n' * a)
+           succ_case_of_fac_is_left_permutative
+           n
+           1
+        ).
+Qed.
+
+Lemma succ_case_of_Sigma_is_left_permutative :
+  forall (f : nat -> nat),
+    is_left_permutative nat (fun n' a : nat => a + f (S n')).
+Proof.
+  intro f.
+  unfold is_left_permutative.
+  intros n1 n2 v.
+  Search (_ + _ + _).
+  rewrite -> Nat.add_shuffle0.
+  reflexivity.
+Qed.
+
+Corollary tr_Sigma_left_and_r_Sigma_right_are_equivalent :
+  forall (n : nat)
+    (f : nat -> nat),
+
+    tr_Sigma_left n f = r_Sigma_right n f.
+Proof.
+  intros n f.
+  unfold tr_Sigma_left.
+  unfold r_Sigma_right.
+  exact (parafolding_left_and_right_over_peano_numbers
+           nat
+           (fun n' a : nat => a + f (S n'))
+           (succ_case_of_Sigma_is_left_permutative f)
+           n
+           (f 0)
+        ).
+Qed.
+(* ********** *)
+
+(* 7. Prove your similar theorem. *)
+
+(* ********** *)
+
+(* end of question-for-Yadunand.v *)

cs3234/labs/term-project.v

@@ -7,6 +7,7 @@
 
 (* Three language processors for arithmetic expressions. *)
 
+
 (*
    group name:
 
@@ -488,7 +489,7 @@ Definition specification_of_decode_execute (decode_execute : byte_code_instructi
   (forall (n1 n2 : nat)
      (ds : data_stack),
       n1 <? n2 = false ->
-      decode_execute SUB (n2 :: n1 :: ds) = OK ((n2 - n1) :: ds))
+      decode_execute SUB (n2 :: n1 :: ds) = OK ((n1 - n2) :: ds))
   /\
  (* if the data stack does not contain at least two nats
    evaluating
@@ -516,7 +517,7 @@ Definition decode_execute (bci : byte_code_instruction) (ds : data_stack) : resu
       | n2 :: n1 :: ds' =>
           if n1 <? n2
           then KO (String.append "numerical underflow: -" (string_of_nat (n2 - n1)))
-          else OK ((n2 - n1) :: ds')
+          else OK ((n1 - n2) :: ds')
       | _ => KO "ADD: stack underflow"
       end
   end.
@@ -725,6 +726,7 @@ Definition specification_of_run (run : target_program -> expressible_value) :=
        run (Target_program bcis) = Expressible_msg s).
 
 
+(* Since this is talking mostly about the data stack, thats where we will work from *)
 Theorem there_is_at_most_one_run_function :
   forall (f g : target_program -> expressible_value),
     specification_of_run f ->
@@ -732,16 +734,93 @@ Theorem there_is_at_most_one_run_function :
     forall (t: target_program),
     f t = g t.
 Proof.
-  intros f g.
-  unfold specification_of_run.
-  intros S_f S_g [bcis].
-  case (fetch_decode_execute_loop bcis nil) as [ds | s] eqn:H_fdel.
-  - destruct (S_f fetch_decode_execute_loop fetch_decode_execute_loop_satifies_the_specification) as [S_f_nil _].
+  intros f g S_f S_g [bcis].
+  (* This was the tricky part in my understanding. We are operating on the result of FDEL. Thus, we
+   check every case of fdel and work from there *)
+  case (fetch_decode_execute_loop bcis nil) as [[| n [| n' ds'']] | s] eqn:H_fdel.
+  - unfold specification_of_run in S_f,S_g.
+    destruct (S_f fetch_decode_execute_loop fetch_decode_execute_loop_satifies_the_specification) as [S_f_nil _].
     destruct (S_g fetch_decode_execute_loop fetch_decode_execute_loop_satifies_the_specification) as [S_g_nil _].
-    case ds as [ | n ds' ] eqn:H_ds.
-    + rewrite -> (S_g_nil bcis H_fdel).
+    rewrite -> (S_g_nil bcis H_fdel).
     exact (S_f_nil bcis H_fdel).
-    + Check (S_f_nil bcis).
+  - unfold specification_of_run in S_f,S_g.
+    destruct (S_f fetch_decode_execute_loop fetch_decode_execute_loop_satifies_the_specification) as [_ [S_f_one _]].
+    destruct (S_g fetch_decode_execute_loop fetch_decode_execute_loop_satifies_the_specification) as [_ [S_g_one _]].
+    rewrite -> (S_g_one bcis n H_fdel).
+    exact (S_f_one bcis n H_fdel).
+  - unfold specification_of_run in S_f,S_g.
+    destruct (S_f fetch_decode_execute_loop fetch_decode_execute_loop_satifies_the_specification) as [_ [_ [S_f_mult _]]].
+    destruct (S_g fetch_decode_execute_loop fetch_decode_execute_loop_satifies_the_specification) as [_ [_ [S_g_mult _]]].
+    rewrite -> (S_g_mult bcis n n' ds'' H_fdel).
+    exact (S_f_mult bcis n n' ds'' H_fdel).
+  - unfold specification_of_run in S_f,S_g.
+    destruct (S_f fetch_decode_execute_loop fetch_decode_execute_loop_satifies_the_specification) as [_ [_ [_ S_f_KO]]].
+    destruct (S_g fetch_decode_execute_loop fetch_decode_execute_loop_satifies_the_specification) as [_ [_ [_ S_g_KO]]].
+    rewrite -> (S_g_KO bcis s H_fdel).
+    exact (S_f_KO bcis s H_fdel).
+Qed.
+
+
+Definition run (p : target_program) : expressible_value :=
+  match p with
+    Target_program bcis =>
+      match (fetch_decode_execute_loop bcis nil) with
+      | OK nil => Expressible_msg "no result on the data stack"
+      | OK (n :: nil) => Expressible_nat n
+      | OK (n :: n' :: ds'') => Expressible_msg "too many results on the data stack"
+      | KO s => Expressible_msg s
+      end
+  end.
+
+
+Theorem run_satisfies_the_specification_of_run :
+ specification_of_run run.
+Proof.
+  unfold specification_of_run.
+  intros fdel.
+  intros S_fdel.
+  split.
+  { intros bcis H_fdel.
+    unfold run.
+    rewrite -> (there_is_at_most_one_fetch_decode_execute_loop
+                 fetch_decode_execute_loop fdel
+                 fetch_decode_execute_loop_satifies_the_specification S_fdel
+                 bcis nil
+      ).
+    rewrite -> H_fdel.
+    reflexivity. }
+  split.
+  { intros bcis n H_fdel.
+    unfold run.
+    rewrite -> (there_is_at_most_one_fetch_decode_execute_loop
+                 fetch_decode_execute_loop fdel
+                 fetch_decode_execute_loop_satifies_the_specification S_fdel
+                 bcis nil
+      ).
+    rewrite -> H_fdel.
+    reflexivity.
+  }
+  split.
+  { intros bcis n n' ds'' H_fdel .
+    unfold run.
+    rewrite -> (there_is_at_most_one_fetch_decode_execute_loop
+                 fetch_decode_execute_loop fdel
+                 fetch_decode_execute_loop_satifies_the_specification S_fdel
+                 bcis nil
+      ).
+    rewrite -> H_fdel.
+    reflexivity.
+  }
+  intros bcis s H_fdel .
+  unfold run.
+  rewrite -> (there_is_at_most_one_fetch_decode_execute_loop
+               fetch_decode_execute_loop fdel
+               fetch_decode_execute_loop_satifies_the_specification S_fdel
+               bcis nil
+    ).
+  rewrite -> H_fdel.
+  reflexivity.
+Qed.
 
 
 (* Task 4:
@@ -762,6 +841,71 @@ Definition specification_of_compile_aux (compile_aux : arithmetic_expression ->
   (forall ae1 ae2 : arithmetic_expression,
      compile_aux (Minus ae1 ae2) = (compile_aux ae1) ++ (compile_aux ae2) ++ (SUB :: nil)).
 
+Theorem there_is_at_most_one_compile_aux_function :
+  forall (f g : arithmetic_expression -> list byte_code_instruction),
+    (specification_of_compile_aux f) ->
+    (specification_of_compile_aux g) ->
+    forall (ae : arithmetic_expression),
+    f ae = g ae.
+Proof.
+  intros f g S_f S_g ae.
+  destruct S_f as [S_f_Literal [S_f_Plus S_f_Minus]].
+  destruct S_g as [S_g_Literal [S_g_Plus S_g_Minus]].
+  induction ae as [n | ae1 IHae1 ae2 IHae2 | ae1 IHae1 ae2 IHae2 ].
+  - rewrite -> S_g_Literal.
+    exact (S_f_Literal n).
+  - rewrite -> S_g_Plus.
+    rewrite -> S_f_Plus.
+    rewrite -> IHae1.
+    rewrite -> IHae2.
+    reflexivity.
+  - rewrite -> S_g_Minus.
+    rewrite -> S_f_Minus.
+    rewrite -> IHae1.
+    rewrite -> IHae2.
+    reflexivity.
+Qed.
+
+Fixpoint compile_aux (ae : arithmetic_expression) : (list byte_code_instruction) :=
+  match ae with
+  | Literal n => PUSH n :: nil
+  | Plus ae1 ae2 => (compile_aux ae1) ++ (compile_aux ae2) ++ (ADD :: nil)
+  | Minus ae1 ae2 => (compile_aux ae1) ++ (compile_aux ae2) ++ (SUB :: nil)
+  end.
+
+Lemma fold_unfold_compile_aux_Literal :
+  forall (n : nat),
+    compile_aux (Literal n) = PUSH n :: nil.
+Proof.
+  fold_unfold_tactic compile_aux.
+Qed.
+
+Lemma fold_unfold_compile_aux_Plus :
+  forall (ae1 ae2 : arithmetic_expression),
+    compile_aux (Plus ae1 ae2) = (compile_aux ae1) ++ (compile_aux ae2) ++ (ADD :: nil).
+Proof.
+  fold_unfold_tactic compile_aux.
+Qed.
+
+Lemma fold_unfold_compile_aux_Minus :
+  forall (ae1 ae2 : arithmetic_expression),
+    compile_aux (Minus ae1 ae2) = (compile_aux ae1) ++ (compile_aux ae2) ++ (SUB :: nil).
+Proof.
+  fold_unfold_tactic compile_aux.
+Qed.
+
+Theorem compile_aux_satifies_the_specification_of_compile_aux :
+  specification_of_compile_aux compile_aux.
+Proof.
+  unfold specification_of_compile_aux.
+  split.
+  { exact fold_unfold_compile_aux_Literal.}
+  split.
+  { exact fold_unfold_compile_aux_Plus.}
+  exact fold_unfold_compile_aux_Minus.
+Qed.
+
+
 (* Task 5:
    a. time permitting, prove that the definition above specifies at most one function;
    b. implement this function using list concatenation, i.e., ++; and
@@ -774,6 +918,37 @@ Definition specification_of_compile (compile : source_program -> target_program)
     forall ae : arithmetic_expression,
       compile (Source_program ae) = Target_program (compile_aux ae).
 
+Theorem there_is_at_most_one_compile_function :
+  forall (f g : source_program -> target_program),
+    (specification_of_compile f) ->
+    (specification_of_compile g) ->
+    forall (sp : source_program),
+      f sp = g sp.
+Proof.
+  intros f g.
+  unfold specification_of_compile.
+  intros S_f S_g [ae].
+  rewrite -> (S_g compile_aux compile_aux_satifies_the_specification_of_compile_aux ae).
+  exact (S_f compile_aux compile_aux_satifies_the_specification_of_compile_aux ae).
+Qed.
+
+Definition compile (sp : source_program) : target_program :=
+  match sp with
+  | Source_program ae => Target_program (compile_aux ae)
+  end.
+
+Theorem compile_satifies_the_specification_of_compile :
+  specification_of_compile compile.
+Proof.
+  unfold specification_of_compile, compile.
+  intros compile_aux' S_compile_aux' ae.
+  rewrite -> (there_is_at_most_one_compile_aux_function
+           compile_aux' compile_aux
+           S_compile_aux' compile_aux_satifies_the_specification_of_compile_aux ae).
+  reflexivity.
+Qed.
+
+
 (* Task 6:
    a. time permitting, prove that the definition above specifies at most one function;
    b. implement this function; and
@@ -782,6 +957,120 @@ Definition specification_of_compile (compile : source_program -> target_program)
 
 (* ********** *)
 
+Fixpoint compile_alt_aux_acc (ae : arithmetic_expression) (acc : list byte_code_instruction) : (list byte_code_instruction) :=
+  match ae with
+  | Literal n => PUSH n :: acc
+  | Plus ae1 ae2 => (compile_alt_aux_acc ae1 (compile_alt_aux_acc ae2 (ADD :: acc)))
+  | Minus ae1 ae2 => (compile_alt_aux_acc ae1 (compile_alt_aux_acc ae2 (SUB :: acc)))
+  end.
+
+Lemma fold_unfold_compile_alt_aux_acc_Literal :
+  forall (n : nat)
+    (acc : list byte_code_instruction),
+    compile_alt_aux_acc (Literal n) acc = PUSH n :: acc.
+Proof.
+  fold_unfold_tactic compile_alt_aux_acc.
+Qed.
+
+Lemma fold_unfold_compile_alt_aux_acc_Plus :
+  forall (ae1 ae2 : arithmetic_expression)
+    (acc : list byte_code_instruction),
+    compile_alt_aux_acc (Plus ae1 ae2) acc = (compile_alt_aux_acc ae1 (compile_alt_aux_acc ae2 (ADD :: acc))).
+Proof.
+  fold_unfold_tactic compile_alt_aux_acc.
+Qed.
+
+Lemma fold_unfold_compile_alt_aux_acc_Minus :
+  forall (ae1 ae2 : arithmetic_expression)
+    (acc : list byte_code_instruction),
+    compile_alt_aux_acc (Minus ae1 ae2) acc = (compile_alt_aux_acc ae1 (compile_alt_aux_acc ae2 (SUB :: acc))).
+Proof.
+  fold_unfold_tactic compile_alt_aux_acc.
+Qed.
+
+Definition compile_alt_aux (ae : arithmetic_expression) : list byte_code_instruction :=
+  compile_alt_aux_acc ae nil.
+
+Lemma about_compile_alt_aux_acc :
+  forall (ae : arithmetic_expression)
+    (ds : list byte_code_instruction),
+    compile_alt_aux_acc ae ds = compile_alt_aux_acc ae nil ++ ds.
+  Proof.
+    intros ae.
+    induction ae as [n | ae1 IHae1 ae2 IHae2 | ae1 IHae1 ae2 IHae2].
+    - intro ds.
+      Check (fold_unfold_compile_alt_aux_acc_Literal n ds).
+      rewrite -> (fold_unfold_compile_alt_aux_acc_Literal n ds).
+      rewrite -> (fold_unfold_compile_alt_aux_acc_Literal n nil).
+      rewrite -> fold_unfold_list_append_cons.
+      rewrite -> fold_unfold_list_append_nil.
+      reflexivity.
+    - intro ds.
+      rewrite -> (fold_unfold_compile_alt_aux_acc_Plus ae1 ae2).
+      rewrite -> (fold_unfold_compile_alt_aux_acc_Plus ae1 ae2).
+      rewrite -> (IHae2 (ADD :: ds)).
+      rewrite -> (IHae2 (ADD :: nil)).
+      rewrite -> (IHae1 (compile_alt_aux_acc ae2 nil ++ ADD :: ds)).
+      rewrite -> (IHae1 (compile_alt_aux_acc ae2 nil ++ ADD :: nil)).
+      rewrite <- 2 app_assoc.
+      rewrite -> fold_unfold_list_append_cons.
+      rewrite -> fold_unfold_list_append_nil.
+      reflexivity.
+    - intro ds.
+      rewrite -> (fold_unfold_compile_alt_aux_acc_Minus ae1 ae2).
+      rewrite -> (fold_unfold_compile_alt_aux_acc_Minus ae1 ae2).
+      rewrite -> (IHae2 (SUB :: ds)).
+      rewrite -> (IHae2 (SUB :: nil)).
+      rewrite -> (IHae1 (compile_alt_aux_acc ae2 nil ++ SUB :: ds)).
+      rewrite -> (IHae1 (compile_alt_aux_acc ae2 nil ++ SUB :: nil)).
+      rewrite <- 2 app_assoc.
+      rewrite -> fold_unfold_list_append_cons.
+      rewrite -> fold_unfold_list_append_nil.
+      reflexivity.
+Qed.
+
+Theorem compile_alt_aux_satisifes_the_specification_of_compile_aux :
+  specification_of_compile_aux compile_alt_aux.
+Proof.
+  unfold specification_of_compile_aux, compile_alt_aux.
+  split.
+  { intros n.
+    rewrite -> (fold_unfold_compile_alt_aux_acc_Literal n nil).
+    reflexivity. }
+  split.
+  { intros ae1 ae2.
+    rewrite -> (fold_unfold_compile_alt_aux_acc_Plus ae1 ae2 nil).
+    Check about_compile_alt_aux_acc.
+    rewrite -> (about_compile_alt_aux_acc ae2 (ADD :: nil)).
+    rewrite -> (about_compile_alt_aux_acc ae1 (compile_alt_aux_acc ae2 nil ++ ADD :: nil)).
+
+    reflexivity. }
+  intros ae1 ae2.
+  rewrite -> (fold_unfold_compile_alt_aux_acc_Minus ae1 ae2 nil).
+  Check about_compile_alt_aux_acc.
+  rewrite -> (about_compile_alt_aux_acc ae2 (SUB :: nil)).
+  rewrite -> (about_compile_alt_aux_acc ae1 (compile_alt_aux_acc ae2 nil ++ SUB :: nil)).
+  reflexivity.
+Qed.
+
+Definition compile_alt (sp : source_program) : target_program :=
+  match sp with
+  | Source_program ae => Target_program (compile_alt_aux ae)
+  end.
+
+Theorem compile_alt_satisfies_the_specificiation_of_compile :
+  specification_of_compile compile_alt.
+Proof.
+  unfold specification_of_compile, compile_alt.
+  intros compile_aux' S_compile_aux ae.
+  rewrite -> (there_is_at_most_one_compile_aux_function
+               compile_aux' compile_alt_aux
+               S_compile_aux compile_alt_aux_satisifes_the_specification_of_compile_aux
+               ae
+    ).
+  reflexivity.
+Qed.
+
 (* Task 7:
    implement an alternative compiler
    using an auxiliary function with an accumulator
@@ -795,8 +1084,155 @@ Definition specification_of_compile (compile : source_program -> target_program)
 
 (* ********** *)
 
+Theorem the_commuting_diagram_evaluate_nat :
+  forall (ae : arithmetic_expression)
+    (n : nat)
+    (ds : data_stack),
+    evaluate ae = Expressible_nat n ->
+    fetch_decode_execute_loop (compile_aux ae) ds = OK (n :: ds).
+Proof.
+  intro ae.
+  induction ae as [n | ae1 IHae1 ae2 IHae2| ae1 IHae1 ae2 IHae2];
+    intros n' ds H_eval.
+  - rewrite -> fold_unfold_compile_aux_Literal.
+    rewrite -> fold_unfold_fetch_decode_execute_loop_cons.
+    unfold decode_execute.
+    rewrite -> fold_unfold_fetch_decode_execute_loop_nil.
+    rewrite -> fold_unfold_evaluate_Literal in H_eval.
+    injection H_eval as n_is_n'.
+    rewrite -> n_is_n'.
+    reflexivity.
+  - rewrite -> fold_unfold_compile_aux_Plus.
+    rewrite -> fold_unfold_evaluate_Plus in H_eval.
+    (* I need the 2 statements evaluate ae1 = Expressible_nat n *)
+    case (evaluate ae1) as [n1 | s1] eqn:H_eval_ae1.
+    + case (evaluate ae2) as [n2 | s2] eqn:H_eval_ae2.
+      * injection H_eval as n1_plus_n2_is_n'.
+        Search fetch_decode_execute_loop.
+        destruct (about_fetch_decode_execute_loop (compile_aux ae1) (compile_aux ae2 ++ ADD :: nil) ds) as [H_fdel_append_ae1 _].
+        rewrite -> (H_fdel_append_ae1
+                     (n1::ds)
+                     (IHae1 n1 ds eq_refl)
+          ).
+        destruct (about_fetch_decode_execute_loop (compile_aux ae2) (ADD :: nil) (n1 :: ds)) as [H_fdel_append_ae2 _].
+        rewrite -> (H_fdel_append_ae2
+                     (n2::n1::ds)
+                     (IHae2 n2 (n1::ds) eq_refl)
+          ).
+        rewrite -> fold_unfold_fetch_decode_execute_loop_cons.
+        unfold decode_execute.
+        rewrite -> fold_unfold_fetch_decode_execute_loop_nil.
+        rewrite -> n1_plus_n2_is_n'.
+        reflexivity.
+      * discriminate H_eval.
+    + discriminate H_eval.
+  - rewrite -> fold_unfold_compile_aux_Minus.
+    rewrite -> fold_unfold_evaluate_Minus in H_eval.
+    case (evaluate ae1) as [n1 | s1] eqn:H_eval_ae1.
+    + case (evaluate ae2) as [n2 | s2] eqn:H_eval_ae2.
+      * case (n1 <? n2) eqn:H_n1_lt_n2.
+        ++ discriminate H_eval.
+        ++ injection H_eval as n1_minus_n2_is_n'.
+           destruct (about_fetch_decode_execute_loop
+                       (compile_aux ae1)
+                       (compile_aux ae2 ++ SUB :: nil) ds) as [H_fdel_append_ae1 _].
+           rewrite -> (H_fdel_append_ae1
+                        (n1::ds)
+                        (IHae1 n1 ds eq_refl)
+             ).
+           destruct (about_fetch_decode_execute_loop
+                       (compile_aux ae2)
+                       (SUB :: nil) (n1::ds)) as [H_fdel_append_ae2 _].
+           rewrite -> (H_fdel_append_ae2
+                        (n2::n1::ds)
+                        (IHae2 n2 (n1::ds) eq_refl)
+             ).
+           rewrite -> fold_unfold_fetch_decode_execute_loop_cons.
+           unfold decode_execute.
+           rewrite -> H_n1_lt_n2.
+           rewrite -> fold_unfold_fetch_decode_execute_loop_nil.
+           rewrite <- n1_minus_n2_is_n'.
+           reflexivity.
+      * discriminate H_eval.
+  + discriminate H_eval.
+Qed.
+
+Theorem the_commuting_diagram_evaluate_msg :
+  forall (ae : arithmetic_expression)
+    (s : string)
+    (ds : data_stack),
+    evaluate ae = Expressible_msg s ->
+    fetch_decode_execute_loop (compile_aux ae) ds = KO s.
+  Proof.
+    intro ae.
+    induction ae as [n | ae1 IHae1 ae2 IHae2 | ae1 IHae1 ae2 IHae2]; intros s ds H_eval.
+    - rewrite -> fold_unfold_evaluate_Literal in H_eval.
+      discriminate H_eval.
+    - rewrite -> fold_unfold_evaluate_Plus in H_eval.
+      case (evaluate ae1) as [n1 | s1] eqn:H_eval_ae1.
+      + case (evaluate ae2) as [n2 | s2] eqn:H_eval_ae2.
+        * discriminate H_eval.
+        * rewrite -> fold_unfold_compile_aux_Plus.
+          injection H_eval as s2_is_s.
+          destruct (about_fetch_decode_execute_loop (compile_aux ae1) (compile_aux ae2 ++ ADD :: nil) ds) as [H_fdel_append _].
+          rewrite -> (H_fdel_append (n1 :: ds) (the_commuting_diagram_evaluate_nat ae1 n1 ds H_eval_ae1)).
+          destruct (about_fetch_decode_execute_loop (compile_aux ae2) (ADD::nil) (n1::ds)) as [_ H_fdel_append_KO].
+          rewrite -> (H_fdel_append_KO s2 (IHae2 s2 (n1::ds) eq_refl)).
+          rewrite -> s2_is_s.
+          reflexivity.
+      + injection H_eval as s1_is_s.
+          destruct (about_fetch_decode_execute_loop (compile_aux ae1) (compile_aux ae2 ++ ADD :: nil) ds) as [_ H_fdel_append_KO].
+          rewrite -> fold_unfold_compile_aux_Plus.
+          rewrite -> (H_fdel_append_KO s1 (IHae1 s1 ds eq_refl)).
+          rewrite -> s1_is_s.
+          reflexivity.
+    - rewrite -> fold_unfold_evaluate_Minus in H_eval.
+      case (evaluate ae1) as [n1 | s1] eqn:H_eval_ae1.
+      + case (evaluate ae2) as [n2 | s2] eqn:H_eval_ae2.
+        * case (n1 <? n2) eqn:H_n1_lt_n2.
+          ++ rewrite -> fold_unfold_compile_aux_Minus.
+             destruct (about_fetch_decode_execute_loop (compile_aux ae1) (compile_aux ae2 ++ SUB :: nil) ds) as [H_fdel_append_ae1 _].
+             rewrite -> (H_fdel_append_ae1 (n1 :: ds) (the_commuting_diagram_evaluate_nat ae1 n1 ds H_eval_ae1)).
+             destruct (about_fetch_decode_execute_loop (compile_aux ae2) (SUB :: nil) (n1::ds)) as [H_fdel_append_ae2 _].
+             rewrite -> (H_fdel_append_ae2 (n2::n1::ds) (the_commuting_diagram_evaluate_nat ae2 n2 (n1::ds) H_eval_ae2)).
+             rewrite -> fold_unfold_fetch_decode_execute_loop_cons.
+             unfold decode_execute.
+             rewrite -> H_n1_lt_n2.
+             injection H_eval as n1_lt_n2_msg.
+             simpl (KO ("numerical underflow: -" ++ string_of_nat (n2 - n1))).
+             rewrite -> n1_lt_n2_msg.
+             reflexivity.
+          ++ discriminate H_eval.
+        * injection H_eval as s2_is_s.
+          ++ rewrite -> fold_unfold_compile_aux_Minus.
+             destruct (about_fetch_decode_execute_loop (compile_aux ae1) (compile_aux ae2 ++ SUB :: nil) ds) as [H_fdel_append_ae1 _].
+             rewrite -> (H_fdel_append_ae1 (n1 :: ds) (the_commuting_diagram_evaluate_nat ae1 n1 ds H_eval_ae1)).
+             destruct (about_fetch_decode_execute_loop (compile_aux ae2) (SUB::nil) (n1::ds)) as [_ H_fdel_append_KO].
+             rewrite -> (H_fdel_append_KO s2 (IHae2 s2 (n1::ds) eq_refl)).
+             rewrite -> s2_is_s.
+             reflexivity.
+      + injection H_eval as s1_is_s.
+        rewrite -> fold_unfold_compile_aux_Minus.
+        destruct (about_fetch_decode_execute_loop (compile_aux ae1) (compile_aux ae2 ++ SUB :: nil) ds) as [_ H_fdel_append_KO].
+        rewrite -> (H_fdel_append_KO s1 (IHae1 s1 ds eq_refl)).
+        rewrite -> s1_is_s.
+        reflexivity.
+  Qed.
+
+Theorem the_commuting_diagram :
+  forall (sp : source_program),
+    interpret sp = run (compile sp).
+Proof.
+  intros [ae].
+  unfold interpret, compile,run.
+  case evaluate as [n | s] eqn:H_eval.
+  - rewrite -> (the_commuting_diagram_evaluate_nat ae n nil H_eval).
+    reflexivity.
+  - rewrite -> (the_commuting_diagram_evaluate_msg ae s nil H_eval).
+    reflexivity.
+Qed.
 (* Task 8 (the capstone):
-   Prove that interpreting an arithmetic expression gives the same result
+
    as first compiling it and then executing the compiled program.
 *)
 
@@ -829,6 +1265,33 @@ Fixpoint verify_aux (bcis : list byte_code_instruction) (n : nat) : option nat :
       end
   end.
 
+Definition fold_unfold_verify_aux_nil :
+  forall (n : nat),
+    verify_aux nil n = Some n.
+Proof.
+  fold_unfold_tactic verify_aux.
+Qed.
+
+Definition fold_unfold_verify_aux_cons :
+  forall (bci : byte_code_instruction)
+    (bcis : list byte_code_instruction)
+    (n : nat),
+    verify_aux (bci :: bcis) n =
+      match bci with
+        | PUSH _ =>
+          verify_aux bcis (S n)
+        | _ =>
+          match n with
+            | S (S n') =>
+              verify_aux bcis (S n')
+            | _ =>
+              None
+          end
+      end.
+Proof.
+  fold_unfold_tactic verify_aux.
+Qed.
+
 Definition verify (p : target_program) : bool :=
   match p with
   | Target_program bcis =>
@@ -849,19 +1312,265 @@ Definition verify (p : target_program) : bool :=
    Prove that the compiler emits code
    that is accepted by the verifier.
 *)
-
-(*
-Theorem the_compiler_emits_well_behaved_code :
-  forall ae : arithmetic_expression,
-    verify (compile ae) = true.
+Lemma about_verify_aux_some :
+  forall (bci1s bci2s : list byte_code_instruction)
+    (n n' : nat),
+    (verify_aux bci1s n) = Some n' ->
+    (verify_aux (bci1s ++ bci2s) n) = (verify_aux bci2s n').
 Proof.
-Abort.
-*)
+  intros bci1s.
+  induction bci1s as [ | bci bci1s' IHbci1s' ].
+  - intros bci2s n n' H_verify_aux.
+    rewrite -> fold_unfold_verify_aux_nil in H_verify_aux.
+    injection H_verify_aux as n_is_n'.
+    rewrite -> fold_unfold_list_append_nil.
+    rewrite -> n_is_n'.
+    reflexivity.
+  - intros bci2s n n' H_verify_aux.
+    rewrite -> fold_unfold_list_append_cons.
+    rewrite -> fold_unfold_verify_aux_cons.
+    case bci as [ x |  | ] eqn:H_bci.
+    + rewrite -> fold_unfold_verify_aux_cons in H_verify_aux.
+      rewrite -> (IHbci1s' bci2s (S n) n' H_verify_aux).
+      reflexivity.
+    + case n as [ | [ | n'' ] ].
+      * rewrite -> fold_unfold_verify_aux_cons in H_verify_aux.
+        discriminate H_verify_aux.
+      * rewrite -> fold_unfold_verify_aux_cons in H_verify_aux.
+        discriminate H_verify_aux.
+      * rewrite -> fold_unfold_verify_aux_cons in H_verify_aux.
+        rewrite -> (IHbci1s' bci2s (S n'') n' H_verify_aux).
+        reflexivity.
+    + case n as [ | [ | n'' ] ].
+      * rewrite -> fold_unfold_verify_aux_cons in H_verify_aux.
+        discriminate H_verify_aux.
+      * rewrite -> fold_unfold_verify_aux_cons in H_verify_aux.
+        discriminate H_verify_aux.
+      * rewrite -> fold_unfold_verify_aux_cons in H_verify_aux.
+        rewrite -> (IHbci1s' bci2s (S n'') n' H_verify_aux).
+        reflexivity.
+Qed.
+
+Lemma compile_aux_emits_one_value :
+  forall (ae : arithmetic_expression)
+    (n : nat),
+    verify_aux (compile_aux ae) n = Some (S n).
+Proof.
+  intro ae.
+  induction ae as [n | ae1 IHae1 ae2 IHae2 | ae1 IHae1 ae2 IHae2]; intro n'.
+  - rewrite -> fold_unfold_compile_aux_Literal.
+    rewrite -> fold_unfold_verify_aux_cons.
+    rewrite -> fold_unfold_verify_aux_nil.
+    reflexivity.
+  - rewrite -> fold_unfold_compile_aux_Plus.
+    rewrite -> (about_verify_aux_some
+             (compile_aux ae1)
+             (compile_aux ae2 ++ ADD :: nil)
+             n' (S n')
+             (IHae1 n')).
+    rewrite -> (about_verify_aux_some
+             (compile_aux ae2)
+             (ADD :: nil)
+             (S n') (S (S n'))
+             (IHae2 (S n'))).
+    rewrite -> fold_unfold_verify_aux_cons.
+    rewrite -> fold_unfold_verify_aux_nil.
+    reflexivity.
+  - rewrite -> fold_unfold_compile_aux_Minus.
+    rewrite -> (about_verify_aux_some
+                 (compile_aux ae1)
+                 (compile_aux ae2 ++ SUB :: nil)
+                 n' (S n')
+                 (IHae1 n')).
+    rewrite -> (about_verify_aux_some
+             (compile_aux ae2)
+             (SUB :: nil)
+             (S n') (S (S n'))
+             (IHae2 (S n'))).
+    rewrite -> fold_unfold_verify_aux_cons.
+    rewrite -> fold_unfold_verify_aux_nil.
+    reflexivity.
+Qed.
+
+
+
+Theorem the_compiler_emits_well_behaved_code :
+  forall sp : source_program,
+    verify (compile sp) = true.
+Proof.
+  intros [ae].
+  unfold verify, compile.
+rewrite -> (compile_aux_emits_one_value ae 0).
+reflexivity.
+Qed.
+
 
 (* Subsidiary question:
    What is the practical consequence of this theorem?
 *)
 
+Definition alternative_specification_of_run (run : target_program -> expressible_value) :=
+  forall fetch_decode_execute_loop : list byte_code_instruction -> data_stack -> result_of_decoding_and_execution,
+    specification_of_fetch_decode_execute_loop fetch_decode_execute_loop ->
+    forall (bcis : list byte_code_instruction),
+      (fetch_decode_execute_loop bcis nil = OK nil ->
+       run (Target_program bcis) = Expressible_msg "no result on the data stack")
+      /\
+      (forall (n : nat),
+         fetch_decode_execute_loop bcis nil = OK (n :: nil) ->
+         run (Target_program bcis) = Expressible_nat n)
+      /\
+      (forall (n n' : nat)
+              (ds'' : data_stack),
+         fetch_decode_execute_loop bcis nil = OK (n :: n' :: ds'') ->
+         run (Target_program bcis) = Expressible_msg "too many results on the data stack")
+      /\
+      (forall (s : string),
+         fetch_decode_execute_loop bcis nil = KO s ->
+         run (Target_program bcis) = Expressible_msg s).
+
+Theorem run_satisfies_the_alternative_specification_of_run :
+  alternative_specification_of_run run.
+Proof.
+  unfold alternative_specification_of_run.
+  intros fdel' S_fdel' bcis.
+  split.
+  { intros H_fdel_nil.
+    unfold run.
+    rewrite <- (there_is_at_most_one_fetch_decode_execute_loop
+             fdel' fetch_decode_execute_loop
+             S_fdel' fetch_decode_execute_loop_satifies_the_specification
+             bcis nil
+          ).
+    rewrite -> H_fdel_nil.
+    reflexivity. }
+  split.
+  { intros n H_fdel_one.
+    unfold run.
+    rewrite <- (there_is_at_most_one_fetch_decode_execute_loop
+             fdel' fetch_decode_execute_loop
+             S_fdel' fetch_decode_execute_loop_satifies_the_specification
+             bcis nil
+          ).
+    rewrite -> H_fdel_one.
+    reflexivity.
+  }
+  split.
+  { intros n n' ds H_fdel_many.
+    unfold run.
+    rewrite <- (there_is_at_most_one_fetch_decode_execute_loop
+             fdel' fetch_decode_execute_loop
+             S_fdel' fetch_decode_execute_loop_satifies_the_specification
+             bcis nil
+          ).
+    rewrite -> H_fdel_many.
+    reflexivity.
+  }
+  intros s H_fdel_KO.
+  unfold run.
+  rewrite <- (there_is_at_most_one_fetch_decode_execute_loop
+               fdel' fetch_decode_execute_loop
+               S_fdel' fetch_decode_execute_loop_satifies_the_specification
+               bcis nil
+    ).
+  rewrite -> H_fdel_KO.
+  reflexivity.
+Qed.
 (* ********** *)
 
+Theorem there_is_at_most_one_run_function_with_this_alternative :
+  forall run1 run2 : target_program -> expressible_value,
+    alternative_specification_of_run run1 ->
+    alternative_specification_of_run run2 ->
+    forall tp :
+
+ target_program,
+      run1 tp = run2 tp.
+Proof.
+  intros run1 run2 S_run1 S_run2 [bcis].
+
+  case (fetch_decode_execute_loop bcis nil) as [ ds | s] eqn:H_fdel.
+  - case ds as [ | n ds' ] eqn:H_ds.
+    + destruct (S_run1 fetch_decode_execute_loop fetch_decode_execute_loop_satifies_the_specification bcis) as [H_run1_nil _].
+      destruct (S_run2 fetch_decode_execute_loop fetch_decode_execute_loop_satifies_the_specification bcis) as [H_run2_nil _].
+      rewrite -> (H_run1_nil H_fdel).
+      rewrite -> (H_run2_nil H_fdel).
+      reflexivity.
+    + case ds' as [ | n' ds'' ] eqn:H_ds'.
+      * destruct (S_run1 fetch_decode_execute_loop fetch_decode_execute_loop_satifies_the_specification bcis) as [_ [H_run1_one _]].
+        destruct (S_run2 fetch_decode_execute_loop fetch_decode_execute_loop_satifies_the_specification bcis) as [_ [H_run2_one _]].
+        rewrite -> (H_run1_one n H_fdel).
+        rewrite -> (H_run2_one n H_fdel).
+        reflexivity.
+      * destruct (S_run1 fetch_decode_execute_loop fetch_decode_execute_loop_satifies_the_specification bcis) as [_ [_ [H_run1_many _]]].
+        destruct (S_run2 fetch_decode_execute_loop fetch_decode_execute_loop_satifies_the_specification bcis) as [_ [_ [H_run2_many _]]].
+        rewrite -> (H_run1_many n n' ds'' H_fdel).
+        rewrite -> (H_run2_many n n' ds'' H_fdel).
+        reflexivity.
+  - destruct (S_run1 fetch_decode_execute_loop fetch_decode_execute_loop_satifies_the_specification bcis) as [_ [_ [_ H_run1_KO]]].
+    destruct (S_run2 fetch_decode_execute_loop fetch_decode_execute_loop_satifies_the_specification bcis) as [_ [_ [_ H_run2_KO]]].
+    rewrite -> (H_run1_KO s H_fdel).
+    rewrite -> (H_run2_KO s H_fdel).
+    reflexivity.
+Qed.
+
+Proposition equivalence_of_the_two_specifications :
+  forall run : target_program -> expressible_value,
+    specification_of_run run <-> alternative_specification_of_run run.
+Proof.
+  intro run'.
+  unfold specification_of_run.
+  unfold alternative_specification_of_run.
+  split.
+  - intro S_run.
+    assert (S_run := S_run fetch_decode_execute_loop fetch_decode_execute_loop_satifies_the_specification).
+    destruct S_run as [S_run_nil [S_run_one [S_run_many S_run_KO]]].
+    intros fdel S_fdel bcis.
+    rewrite -> (there_is_at_most_one_fetch_decode_execute_loop fdel fetch_decode_execute_loop S_fdel fetch_decode_execute_loop_satifies_the_specification bcis).
+    split.
+    { intros H_fdel_nil.
+      rewrite -> (S_run_nil bcis H_fdel_nil).
+      reflexivity. }
+    split.
+    { intros n H_fdel_one.
+      rewrite -> (S_run_one bcis n H_fdel_one).
+      reflexivity. }
+    split.
+    { intros n n' ds'' H_fdel_many.
+      rewrite -> (S_run_many bcis n n' ds'' H_fdel_many ).
+      reflexivity. }
+    intros s H_fdel_KO.
+    rewrite -> (S_run_KO bcis s H_fdel_KO).
+    reflexivity.
+  - intro S_run.
+    assert (S_run := S_run fetch_decode_execute_loop fetch_decode_execute_loop_satifies_the_specification).
+    intros fdel S_fdel.
+    split.
+    { intros bcis H_fdel_nil.
+      rewrite -> (there_is_at_most_one_fetch_decode_execute_loop fdel fetch_decode_execute_loop S_fdel fetch_decode_execute_loop_satifies_the_specification bcis) in H_fdel_nil.
+      destruct (S_run bcis) as [S_run_nil _].
+      rewrite -> (S_run_nil H_fdel_nil).
+      reflexivity.
+    }
+    split.
+    { intros bcis n H_fdel_one.
+      rewrite -> (there_is_at_most_one_fetch_decode_execute_loop fdel fetch_decode_execute_loop S_fdel fetch_decode_execute_loop_satifies_the_specification bcis) in H_fdel_one.
+      destruct (S_run bcis) as [_ [S_run_one _]].
+      rewrite -> (S_run_one n H_fdel_one).
+      reflexivity.
+    }
+    split.
+    { intros bcis n n' ds'' H_fdel_many.
+      rewrite -> (there_is_at_most_one_fetch_decode_execute_loop fdel fetch_decode_execute_loop S_fdel fetch_decode_execute_loop_satifies_the_specification bcis) in H_fdel_many.
+      destruct (S_run bcis) as [_ [_ [S_run_many _]]].
+      rewrite -> (S_run_many n n' ds'' H_fdel_many).
+      reflexivity.
+    }
+    intros bcis s H_fdel_KO.
+    rewrite -> (there_is_at_most_one_fetch_decode_execute_loop fdel fetch_decode_execute_loop S_fdel fetch_decode_execute_loop_satifies_the_specification bcis) in H_fdel_KO.
+    destruct (S_run bcis) as [_ [_ [_ S_run_KO]]].
+    rewrite -> (S_run_KO s H_fdel_KO).
+    reflexivity.
+Qed.
+
 (* end of term-project.v *)

cs3234/labs/week-06_a_simple_problem.v

@@ -0,0 +1,72 @@
+(* Paraphernalia: *)
+
+Ltac fold_unfold_tactic name := intros; unfold name; fold name; reflexivity.
+
+Require Import Arith Bool.
+
+(* ********** *)
+
+Check Bool.eqb. (* : bool -> bool -> bool *)
+
+Check eqb. (* : bool -> bool -> bool *)
+
+Search (eqb _ _ = true -> _ = _).
+(* eqb_prop: forall a b : bool, eqb a b = true -> a = b *)
+
+Search (eqb _ _ = true).
+(* eqb_reflx: forall b : bool, eqb b b = true *)
+
+Search (_ * _).
+
+(* Definition is_even (n: nat) := *)
+
+(* Proposition product_of_n_and_even_is_even : *)
+(*   forall n : nat, *)
+
+Proposition product_of_2_consecutive_natural_numbers_is_even:
+  forall n: nat,
+  exists a: nat,
+    n * (S n) = 2 * a.
+Proof.
+  intro n.
+  induction n as [ | n' IHn'].
+  - exists 0.
+    rewrite -> (Nat.mul_0_l 1).
+    rewrite -> (Nat.mul_0_r 2).
+    reflexivity.
+  - rewrite -> (Nat.mul_succ_r (S n') (S n')).
+    rewrite -> (Nat.mul_succ_r (S n') n').
+    rewrite -> (Nat.mul_comm (S n') n').
+    destruct IHn' as [k IHn'].
+    rewrite -> IHn'.
+    rewrite <- (Nat.add_assoc (2 * k) (S n') (S n')).
+    remember (S n' + S n') as x eqn:H_x.
+    rewrite <- (Nat.mul_1_l (S n')) in H_x at 1.
+    rewrite -> H_x.
+    rewrite <- (Nat.mul_succ_l 1 (S n')).
+    Search (_ * _ + _ * _).
+    rewrite <- (Nat.mul_add_distr_l 2 k (S n')).
+    exists (k + S n').
+    reflexivity.
+Qed.
+
+Proposition product_of_3_consecutive_natural_numbers_is_divisible_by_2:
+  forall n : nat,
+  exists a : nat,
+    n * (S n) * (S (S n)) = 2 * a.
+Proof.
+  intro n.
+  induction n as [ | n' IHn' ].
+  - exists 0.
+    rewrite -> (Nat.mul_0_l 1).
+    rewrite -> (Nat.mul_0_l 2).
+    rewrite -> (Nat.mul_0_r 2).
+    reflexivity.
+  - destruct IHn' as [k IHn'].
+    destruct (product_of_2_consecutive_natural_numbers_is_even (S n')) as [x H_product_of_2_consecutive_natural_numbers_is_even].
+    rewrite -> H_product_of_2_consecutive_natural_numbers_is_even.
+    exists (x * S (S (S n'))).
+    Check (Nat.mul_assoc 2 x (S (S (S n')))).
+    rewrite -> (Nat.mul_assoc 2 x (S (S (S n')))).
+    reflexivity.
+Qed.

cs3234/labs/week-06_ex-falso-quodlibet.v

@@ -0,0 +1,172 @@
+(* week-06_ex-falso-quodlibet.v *)
+(* LPP 2024 - CS3234 2023-2024, Sem2 *)
+(* Olivier Danvy <danvy@yale-nus.edu.sg> *)
+(* Version of 22 Feb 2024 *)
+
+(* ********** *)
+
+Require Import Arith.
+
+(* ********** *)
+
+Property foo :
+  forall P : nat -> Prop,
+    (exists i : nat,
+        P i) ->
+    forall j : nat,
+      P j.
+Proof.
+Abort. (* does not hold, see just below *)
+
+Theorem ex_falso_quodlibet_eg_False :
+  (forall P : nat -> Prop,
+      (exists i : nat,
+          P i) ->
+      forall j : nat,
+        P j) ->
+  0 = 1.
+Proof.
+  intro H_absurd.
+  Check (H_absurd
+           (fun n : nat => 0 = n)).
+  (* : (exists i : nat, 0 = i) -> forall j : nat, 0 = j *)
+  (* wanted: exists i : nat, 0 = i *)
+  Check ex_intro.
+  Check (ex_intro
+           (fun i : nat => 0 = i)).
+  (* : forall x : nat, 0 = x -> exists i : nat, 0 = i *)
+  (* let's pick 0, for example *)
+  Check (ex_intro
+           (fun i : nat => 0 = i)
+           0).
+  Check (ex_intro
+           (fun i : nat => 0 = i)
+           0
+           (eq_refl 0)).
+  (* : exists i : nat, 0 = i *)
+  (* which is what we wanted *)
+  Check (H_absurd
+           (fun n : nat => 0 = n)
+           (ex_intro
+              (fun i : nat => 0 = i)
+              0
+              (eq_refl 0))).
+  (* : forall j : nat, 0 = j *)
+  (* let's pick 1, for example *)
+  Check (H_absurd
+           (fun n : nat => 0 = n)
+           (ex_intro
+              (fun i : nat => 0 = i)
+              0
+              (eq_refl 0))
+           1).
+  (* : 0 = 1 *)
+  exact (H_absurd
+           (fun n : nat => 0 = n)
+           (ex_intro
+              (fun i : nat => 0 = i)
+              0
+              (eq_refl 0))
+           1).
+Qed.
+
+(* ********** *)
+
+(* Exercise 06 *)
+
+Proposition ex_falso_quodlibet_indeed :
+  (forall (P : nat -> Prop),
+      (exists i : nat,
+          P i) ->
+      forall j : nat,
+        P j) -> False.
+Proof.
+Abort.
+
+(* ********** *)
+
+(* Exercise 07 *)
+
+Property foo : (* stated again, but admitted this time... *)
+  forall P : nat -> Prop,
+    (exists i : nat,
+        P i) ->
+    forall j : nat,
+      P j.
+Proof.
+Admitted. (* ...to prove the following theorem as a corollary of foo *)
+
+Theorem ex_falso_quodlibet_eg_True :
+  forall m : nat,
+    exists n : nat,
+      m < n.
+Proof.
+  Check (foo (fun m : nat => exists n : nat, m < n)).
+Abort.
+
+(* ********** *)
+
+(* Exercise 08 *)
+
+Proposition an_equivalence :
+  (forall P : nat -> Prop,
+      (exists i : nat,
+          P i) ->
+      forall j : nat,
+        P j)
+  <->
+  (forall (P : nat -> Prop)
+          (i : nat),
+      P i ->
+      forall j : nat,
+        P j).
+Proof.
+Admitted.
+
+(* ********** *)
+
+(* Exercise 08 *)
+
+Property bar :
+  forall (P : nat -> Prop)
+         (i : nat),
+    P i ->
+    forall j : nat,
+      P j.
+Proof.
+Abort. (* does not hold, see just below *)
+
+Theorem ex_falso_quodlibet_eg_False_revisited :
+  (forall (P : nat -> Prop)
+          (i : nat),
+      P i ->
+      forall j : nat,
+        P j) ->
+  0 = 1.
+Proof.
+Abort.
+
+(* ********** *)
+
+(* Exercise 10 *)
+
+Property bar : (* stated again, but admitted this time... *)
+  forall (P : nat -> Prop)
+         (i : nat),
+    P i ->
+    forall j : nat,
+      P j.
+Proof.
+Admitted. (* ...to prove the following theorem as a corollary of bar *)
+
+Theorem ex_falso_quodlibet_eg_True_revisited :
+  forall m : nat,
+    exists n : nat,
+      m < n.
+Proof.
+  Check (bar (fun m : nat => exists n : nat, m < n)).
+Abort.
+
+(* ********** *)
+
+(* end of week-06_ex-falso-quodlibet.v *)

cs3234/labs/week-06_miscellany.v

@@ -0,0 +1,320 @@
+(* week-06_miscellany.v *)
+(* LPP 2024 - CS3234 2023-2024, Sem2 *)
+(* Olivier Danvy <danvy@yale-nus.edu.sg> *)
+(* Version of 22 Feb 2024 *)
+
+(* ********** *)
+
+Require Import Arith Bool.
+
+(* ********** *)
+
+Lemma truism :
+  forall P : nat -> Prop,
+    (exists n : nat,
+        P n) ->
+    exists n : nat,
+      P n.
+Proof.
+  intros P H_P.
+  exact H_P.
+
+  Restart.
+
+  intros P H_P.
+  destruct H_P as [n H_Pn].
+  exists n.
+  exact H_Pn.
+
+  Restart.
+
+  intros P [n H_Pn].
+  exists n.
+  exact H_Pn.
+Qed.
+
+(* ***** *)
+
+Lemma other_truism :
+  forall P Q : nat -> Prop,
+    (exists n : nat,
+        P n /\ Q n) ->
+    exists m : nat,
+      P m \/ Q m.
+Proof.
+  intros P Q [n [H_Pn H_Qn]].
+  exists n.
+  left.
+  exact H_Pn.
+
+  Restart.
+
+  intros P Q [n [H_Pn H_Qn]].
+  exists n.
+  right.
+  exact H_Qn.
+Qed.
+
+(* ********** *)
+
+Lemma about_the_existential_quantifier_and_disjunction :
+  forall P Q : nat -> Prop,
+    (exists n : nat, P n \/ Q n)
+    <->
+    ((exists n : nat, P n)
+     \/
+     (exists n : nat, Q n)).
+Proof.
+  intros P Q.
+  split.
+  - intros [n [H_P | H_Q]].
+    + left.
+      exists n.
+      exact H_P.
+    + right.
+      exists n.
+      exact H_Q.
+  - intros [[n H_P] | [n H_Q]].
+    + exists n.
+      left.
+      exact H_P.
+    + exists n.
+      right.
+      exact H_Q.
+Qed.
+
+(* ********** *)
+
+Lemma about_the_universal_quantifier_and_conjunction :
+  forall P Q : nat -> Prop,
+    (forall n : nat, P n /\ Q n)
+    <->
+    ((forall n : nat, P n)
+     /\
+     (forall n : nat, Q n)).
+Proof.
+  intros P Q.
+  split.
+  - intro H_PQ.
+    split.
+    + intro n.
+      destr
+
+  Restart.
+  intros P Q.
+  split.
+  - intro H_PQ.
+    split.
+    + intro n.
+      destruct (H_PQ n) as [H_Pn _].
+      exact H_Pn.
+    + intro n.
+      destruct (H_PQ n) as [_ H_Qn].
+      exact H_Qn.
+  - intros [H_P H_Q] n.
+    exact (conj (H_P n) (H_Q n)).
+Qed.
+
+(* ********** *)
+
+Definition specification_of_addition (add : nat -> nat -> nat) :=
+  (forall m : nat,
+      add O m = m)
+  /\
+  (forall n' m : nat,
+      add (S n') m = S (add n' m)).
+
+Definition specification_of_addition' (add : nat -> nat -> nat) :=
+  forall n' m : nat,
+    add O m = m
+    /\
+    add (S n') m = S (add n' m).
+
+Lemma about_two_universal_quantifiers_and_conjunction :
+  forall (P : nat -> Prop)
+         (Q : nat -> nat -> Prop),
+    ((forall j : nat, P j)
+     /\
+     (forall i j : nat, Q i j))
+    <->
+    (forall i j : nat, P j /\ Q i j).
+Proof.
+  intros P Q.
+  split.
+  - intros [H_P H_Q] i j.
+    split.
+    + exact (H_P j).
+    + exact (H_Q i j).
+  - intro H_PQ.
+    split.
+    + intro j.
+      destruct (H_PQ 0 j) as [H_Pj _].
+      exact H_Pj.
+    + intros i j.
+      destruct (H_PQ i j) as [_ H_Qij].
+      exact H_Qij.
+Qed.
+
+Proposition the_two_specifications_of_addition_are_equivalent :
+  forall add : nat -> nat -> nat,
+    specification_of_addition add <-> specification_of_addition' add.
+Proof.
+  intro add.
+  unfold specification_of_addition, specification_of_addition'.
+  Check (about_two_universal_quantifiers_and_conjunction
+           (fun m : nat => add 0 m = m)
+           (fun n' m : nat => add (S n') m = S (add n' m))).
+  exact (about_two_universal_quantifiers_and_conjunction
+           (fun m : nat => add 0 m = m)
+           (fun n' m : nat => add (S n') m = S (add n' m))).
+Qed.
+
+(* ********** *)
+
+Lemma even_or_odd_dropped :
+  forall n : nat,
+    (exists q : nat,
+        n = 2 * q)
+    \/
+    (exists q : nat,
+        n = S (2 * q)).
+Proof.
+Admitted.
+
+Lemma even_or_odd_lifted :
+  forall n : nat,
+  exists q : nat,
+    n = 2 * q
+    \/
+    n = S (2 * q).
+Proof.
+Admitted.
+
+Proposition the_two_specifications_of_even_or_odd_are_equivalent :
+  forall n : nat,
+    (exists q : nat,
+        n = 2 * q
+        \/
+        n = S (2 * q))
+    <->
+    ((exists q : nat,
+         n = 2 * q)
+     \/
+     (exists q : nat,
+         n = S (2 * q))).
+Proof.
+  intro n.
+  Check (about_the_existential_quantifier_and_disjunction
+           (fun q : nat => n = 2 * q)
+           (fun q : nat => n = S (2 * q))).
+  exact (about_the_existential_quantifier_and_disjunction
+           (fun q : nat => n = 2 * q)
+           (fun q : nat => n = S (2 * q))).
+Qed.
+
+(* ********** *)
+
+Proposition factoring_and_distributing_a_forall_in_a_conclusion :
+  forall (P : nat -> Prop)
+         (Q : Prop),
+    (Q -> forall n : nat, P n)
+    <->
+    (forall n : nat,
+        Q -> P n).
+Proof.
+  intros P Q.
+  split.
+  - intros H_QP n H_Q.
+    exact (H_QP H_Q n).
+  - intros H_QP H_Q n.
+    exact (H_QP n H_Q).
+Qed.
+
+(* ********** *)
+
+Proposition interplay_between_quantifiers_and_implication :
+  forall (P : nat -> Prop)
+         (Q : Prop),
+    (exists n : nat, P n -> Q) ->
+    (forall n : nat, P n) -> Q.
+Proof.
+  intros P Q [n H_PnQ] H_P.
+  Check (H_PnQ (H_P n)).
+  exact (H_PnQ (H_P n)).
+Qed.    
+
+(* ********** *)
+
+Proposition interplay_between_implication_and_quantifiers :
+  forall (P : nat -> Prop)
+         (Q : Prop),
+    ((exists n : nat, P n) -> Q) ->
+    forall n : nat, P n -> Q.
+Proof.
+  intros P Q H_PQ n H_Pn.
+  apply H_PQ.
+  exists n.
+  exact H_Pn.
+Qed.
+
+(* ********** *)
+
+Proposition strengthening_X_in_the_conclusion :
+  forall A B C D X Y : Prop,
+    (A -> X) -> (B -> Y) -> (X -> C) -> (Y -> D) -> (X -> Y) -> A -> Y.
+Proof.
+  intros A B C D X Y H_AX H_BY H_XC H_YD H_XY.
+Abort.
+
+Proposition weakening_X_in_the_conclusion :
+  forall A B C D X Y : Prop,
+    (A -> X) -> (B -> Y) -> (X -> C) -> (Y -> D) -> (X -> Y) -> C -> Y.
+Proof.
+  intros A B C D X Y H_AX H_BY H_XC H_YD H_XY.
+Abort.
+
+Proposition strengthening_Y_in_the_conclusion :
+  forall A B C D X Y : Prop,
+    (A -> X) -> (B -> Y) -> (X -> C) -> (Y -> D) -> (X -> Y) -> X -> B.
+Proof.
+  intros A B C D X Y H_AX H_BY H_XC H_YD H_XY.
+Abort.
+
+Proposition weakening_Y_in_the_conclusion :
+  forall A B C D X Y : Prop,
+    (A -> X) -> (B -> Y) -> (X -> C) -> (Y -> D) -> (X -> Y) -> X -> D.
+Proof.
+  intros A B C D X Y H_AX H_BY H_XC H_YD H_XY.
+Abort.
+
+Proposition strengthening_X_in_a_premise :
+  forall A B C D X Y : Prop,
+    (A -> X) -> (B -> Y) -> (X -> C) -> (Y -> D) -> (A -> Y) -> X -> Y.
+Proof.
+  intros A B C D X Y H_AX H_BY H_XC H_YD.
+Abort.
+
+Proposition weakening_X_in_a_premise :
+  forall A B C D X Y : Prop,
+    (A -> X) -> (B -> Y) -> (X -> C) -> (Y -> D) -> (C -> Y) -> X -> Y.
+Proof.
+  intros A B C D X Y H_AX H_BY H_XC H_YD.
+Abort.
+
+Proposition strengthening_Y_in_a_premise :
+  forall A B C D X Y : Prop,
+    (A -> X) -> (B -> Y) -> (X -> C) -> (Y -> D) -> (X -> B) -> X -> Y.
+Proof.
+  intros A B C D X Y H_AX H_BY H_XC H_YD.
+Abort.
+
+Proposition weakening_Y_in_a_premise :
+  forall A B C D X Y : Prop,
+    (A -> X) -> (B -> Y) -> (X -> C) -> (Y -> D) -> (X -> D) -> X -> Y.
+Proof.
+  intros A B C D X Y H_AX H_BY H_XC H_YD.
+Abort.
+
+(* ********** *)
+
+(* end of week-06_miscellany.v *)

cs3234/labs/week-06_soundness-and-completeness-of-equality-predicates.v

@@ -0,0 +1,784 @@
+(* week-06_soundness-and-completeness-of-equality-predicates.v *)
+(* LPP 2024 - CS3234 2023-2024, Sem2 *)
+(* Olivier Danvy <danvy@yale-nus.edu.sg> *)
+(* Version of 22 Feb 2024 *)
+
+(* ********** *)
+
+(* Paraphernalia: *)
+
+Ltac fold_unfold_tactic name := intros; unfold name; fold name; reflexivity.
+
+Require Import Arith Bool.
+
+(* ********** *)
+
+Check Bool.eqb. (* : bool -> bool -> bool *)
+
+Check eqb. (* : bool -> bool -> bool *)
+
+Search (eqb _ _ = true -> _ = _).
+(* eqb_prop: forall a b : bool, eqb a b = true -> a = b *)
+
+Search (eqb _ _ = true).
+(* eqb_reflx: forall b : bool, eqb b b = true *)
+
+Theorem soundness_of_equality_over_booleans :
+  forall b1 b2 : bool,
+    eqb b1 b2 = true -> b1 = b2.
+Proof.
+  exact eqb_prop.
+
+  Restart.
+
+  intros [ | ] [ | ].
+  - intros _.
+    reflexivity.
+  - unfold eqb.
+    intro H_absurd.
+    discriminate H_absurd.
+  - unfold eqb.
+    intro H_absurd.
+    exact H_absurd.
+  - intros _.
+    reflexivity.
+Qed.
+
+Theorem completeness_of_equality_over_booleans :
+  forall b1 b2 : bool,
+    b1 = b2 -> eqb b1 b2 = true.
+Proof.
+  intros b1 b2 H_b1_b2.
+  rewrite <- H_b1_b2.
+  Search (eqb _ _ = true).
+  Check (eqb_reflx b1).
+  exact (eqb_reflx b1).
+
+  Restart.
+
+  intros [ | ] [ | ].
+  - intros _.
+    unfold eqb.
+    reflexivity.
+  - intros H_absurd.
+    discriminate H_absurd.
+  - intros H_absurd.
+    discriminate H_absurd.
+  - intros _.
+    unfold eqb.
+    reflexivity.
+Qed.
+
+Corollary soundness_of_equality_over_booleans_the_remaining_case :
+  forall b1 b2 : bool,
+    eqb b1 b2 = false -> b1 <> b2.
+Proof.
+  intros b1 b2 H_eqb_b1_b2.
+  unfold not.
+  intros H_eq_b1_b2.
+  Check (completeness_of_equality_over_booleans b1 b2 H_eq_b1_b2).
+  rewrite -> (completeness_of_equality_over_booleans b1 b2 H_eq_b1_b2) in H_eqb_b1_b2.
+  discriminate H_eqb_b1_b2.
+Qed.
+
+Corollary completeness_of_equality_over_booleans_the_remaining_case :
+  forall b1 b2 : bool,
+    b1 <> b2 -> eqb b1 b2 = false.
+Proof.
+  intros b1 b2 H_neq_b1_b2.
+  unfold not in H_neq_b1_b2.
+  Search (not (_ = true) -> _ = false).
+  Check (not_true_is_false (eqb b1 b2)).
+  apply (not_true_is_false (eqb b1 b2)).
+  unfold not.
+  intro H_eqb_b1_b2.
+  Check (soundness_of_equality_over_booleans b1 b2 H_eqb_b1_b2).
+  Check (H_neq_b1_b2 (soundness_of_equality_over_booleans b1 b2 H_eqb_b1_b2)).
+  contradiction (H_neq_b1_b2 (soundness_of_equality_over_booleans b1 b2 H_eqb_b1_b2)).
+(* Or alternatively:
+  exact (H_neq_b1_b2 (soundness_of_equality_over_booleans b1 b2 H_eqb_b1_b2)).
+*)
+Qed. 
+
+Check Bool.eqb_eq.
+(* eqb_eq : forall x y : bool, Is_true (eqb x y) -> x = y *)
+
+Search (eqb _ _ = true).
+(* eqb_true_iff: forall a b : bool, eqb a b = true <-> a = b *)
+
+Theorem soundness_and_completeness_of_equality_over_booleans :
+  forall b1 b2 : bool,
+    eqb b1 b2 = true <-> b1 = b2.
+Proof.
+  exact eqb_true_iff.
+
+  Restart.
+
+  intros b1 b2.
+  split.
+  - exact (soundness_of_equality_over_booleans b1 b2).
+  - exact (completeness_of_equality_over_booleans b1 b2).
+Qed.
+
+(* ***** *)
+
+(* user-defined: *)
+
+Definition eqb_bool (b1 b2 : bool) : bool :=
+  match b1 with
+    true =>
+    match b2 with
+      true =>
+      true
+    | false =>
+      false
+    end
+  | false =>
+    match b2 with
+      true =>
+      false
+    | false =>
+      true
+    end
+  end.
+
+Theorem soundness_of_eqb_bool :
+  forall b1 b2 : bool,
+    eqb_bool b1 b2 = true ->
+    b1 = b2.
+Proof.
+  intros [ | ] [ | ].
+  - intros _.
+    reflexivity.
+  - unfold eqb_bool.
+    intros H_absurd.
+    discriminate H_absurd.
+  - unfold eqb_bool.
+    intros H_absurd.
+    exact H_absurd.
+  - intros _.
+    reflexivity.
+Qed.
+
+Theorem completeness_of_eqb_bool :
+  forall b1 b2 : bool,
+    b1 = b2 ->
+    eqb_bool b1 b2 = true.
+Proof.
+  intros [ | ] [ | ].
+  - intros _.
+    reflexivity.
+  - intros H_absurd.
+    discriminate H_absurd.
+  - intros H_absurd.
+    unfold eqb_bool.
+    exact H_absurd.
+  - intros _.
+    unfold eqb_bool.
+    reflexivity.
+Qed.
+
+(* ********** *)
+
+Check Nat.eqb. (* : nat -> nat -> bool *)
+
+Check beq_nat. (* : nat -> nat -> bool *)
+
+Search (beq_nat _ _ = true -> _ = _).
+(* beq_nat_true: forall n m : nat, (n =? m) = true -> n = m *)
+
+Search (beq_nat _ _ = true).
+
+(* Nat.eqb_eq: forall n m : nat, (n =? m) = true <-> n = m *)
+
+Theorem soundness_and_completeness_of_equality_over_natural_numbers :
+  forall n1 n2 : nat,
+    n1 =? n2 = true <-> n1 = n2.
+Proof.
+  exact Nat.eqb_eq.
+Qed.
+
+(* ***** *)
+
+(* user-defined: *)
+
+Fixpoint eqb_nat (n1 n2 : nat) : bool :=
+  match n1 with
+    O =>
+    match n2 with
+      O =>
+      true
+    | S n2' =>
+      false
+    end
+  | S n1' =>
+    match n2 with
+      O =>
+      false
+    | S n2' =>
+      eqb_nat n1' n2'
+    end
+  end.
+
+Lemma fold_unfold_eqb_nat_O :
+  forall n2 : nat,
+    eqb_nat O n2 =
+    match n2 with
+      O =>
+      true
+    | S n2' =>
+      false
+    end.
+Proof.
+  fold_unfold_tactic eqb_nat.
+Qed.
+
+Lemma fold_unfold_eqb_nat_S :
+  forall n1' n2 : nat,
+    eqb_nat (S n1') n2 =
+    match n2 with
+      O =>
+      false
+    | S n2' =>
+      eqb_nat n1' n2'
+    end.
+Proof.
+  fold_unfold_tactic eqb_nat.
+Qed.
+
+Theorem soundness_of_eqb_nat :
+  forall n1 n2 : nat,
+    eqb_nat n1 n2 = true ->
+    n1 = n2.
+Proof.
+  intro n1.
+  induction n1 as [ | n1' IHn1'].
+  - intros [ | n2'].
+    + intros _.
+      reflexivity.
+    + rewrite -> fold_unfold_eqb_nat_O.
+      intro H_absurd.
+      discriminate H_absurd.
+  - intros [ | n2'].
+    + rewrite -> fold_unfold_eqb_nat_S.
+      intro H_absurd.
+      discriminate H_absurd.
+    + rewrite -> fold_unfold_eqb_nat_S.
+      intro H_n1'_n2'.
+      Check (IHn1' n2' H_n1'_n2').
+      rewrite -> (IHn1' n2' H_n1'_n2').
+      reflexivity.
+Qed.
+
+Theorem completeness_of_eqb_nat :
+  forall n1 n2 : nat,
+    n1 = n2 ->
+    eqb_nat n1 n2 = true.
+Proof.
+  intro n1.
+  induction n1 as [ | n1' IHn1'].
+  - intros [ | n2'].
+    + intros _.
+      rewrite -> fold_unfold_eqb_nat_O.
+      reflexivity.
+    + intro H_absurd.
+      discriminate H_absurd.
+  - intros [ | n2'].
+    + intro H_absurd.
+      discriminate H_absurd.
+    + rewrite -> fold_unfold_eqb_nat_S.
+      intro H_Sn1'_Sn2'.
+      injection H_Sn1'_Sn2' as H_n1'_n2'.
+      Check (IHn1' n2' H_n1'_n2').
+      rewrite -> (IHn1' n2' H_n1'_n2').
+      reflexivity.
+Qed.
+
+(* ********** *)
+
+Lemma from_one_equivalence_to_two_implications :
+  forall (V : Type)
+         (eqb_V : V -> V -> bool),
+    (forall v1 v2 : V,
+        eqb_V v1 v2 = true <-> v1 = v2) ->
+    (forall v1 v2 : V,
+        eqb_V v1 v2 = true -> v1 = v2)
+    /\
+    (forall v1 v2 : V,
+        v1 = v2 -> eqb_V v1 v2 = true).
+Proof.
+  intros V eqb_V H_eqv.
+  split.
+  - intros v1 v2 H_eqb.
+    destruct (H_eqv v1 v2) as [H_key _].
+    exact (H_key H_eqb).
+  - intros v1 v2 H_eq.
+    destruct (H_eqv v1 v2) as [_ H_key].
+    exact (H_key H_eq).
+Qed.
+
+(* ********** *)
+
+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 v2 =>
+      false
+    | None =>
+      true
+    end
+  end.
+
+Theorem soundness_of_equality_over_optional_values :
+  forall (V : Type)
+         (eqb_V : V -> V -> bool),
+    (forall v1 v2 : V,
+        eqb_V v1 v2 = true -> v1 = v2) ->
+    forall ov1 ov2 : option V,
+      eqb_option V eqb_V ov1 ov2 = true ->
+      ov1 = ov2.
+Proof.
+  intros V eqb_V S_eqb_V [v1 | ] [v2 | ] H_eqb.
+  - unfold eqb_option in H_eqb.
+    Check (S_eqb_V v1 v2 H_eqb).
+    rewrite -> (S_eqb_V v1 v2 H_eqb).
+    reflexivity.
+  - unfold eqb_option in H_eqb.
+    discriminate H_eqb.
+  - unfold eqb_option in H_eqb.
+    discriminate H_eqb.
+  - reflexivity.
+Qed.
+
+Theorem completeness_of_equality_over_optional_values :
+  forall (V : Type)
+         (eqb_V : V -> V -> bool),
+    (forall v1 v2 : V,
+        v1 = v2 -> eqb_V v1 v2 = true) ->
+    forall ov1 ov2 : option V,
+      ov1 = ov2 ->
+      eqb_option V eqb_V ov1 ov2 = true.
+Proof.
+  intros V eqb_V C_eqb_V ov1 ov2 H_eq.
+  rewrite -> H_eq.
+  case ov1 as [v1 | ].
+  - case ov2 as [v2 | ].
+    -- unfold eqb_option.
+       Check (eq_refl v2).
+       Check (C_eqb_V v2 v2 (eq_refl v2)).
+       exact (C_eqb_V v2 v2 (eq_refl v2)).
+    -- discriminate H_eq.
+  - case ov2 as [v2 | ].
+    -- discriminate H_eq.
+    -- unfold eqb_option.
+       reflexivity.
+Qed.
+
+Theorem soundness_and_completeness_of_equality_over_optional_values :
+  forall (V : Type)
+         (eqb_V : V -> V -> bool),
+    (forall v1 v2 : V,
+        eqb_V v1 v2 = true <-> v1 = v2) ->
+    forall ov1 ov2 : option V,
+      eqb_option V eqb_V ov1 ov2 = true <-> ov1 = ov2.
+Proof.
+  intros V eqb_V SC_eqb_V.
+  Check (from_one_equivalence_to_two_implications V eqb_V SC_eqb_V).
+  destruct (from_one_equivalence_to_two_implications V eqb_V SC_eqb_V) as [S_eqb_V C_eqb_V].
+  intros ov1 ov2.
+  split.
+  - exact (soundness_of_equality_over_optional_values V eqb_V S_eqb_V ov1 ov2).
+  - exact (completeness_of_equality_over_optional_values V eqb_V C_eqb_V ov1 ov2).
+Qed.
+
+(* ********** *)
+
+Definition eqb_pair (V : Type) (eqb_V : V -> V -> bool) (W : Type) (eqb_W : W -> W -> bool) (p1 p2 : V * W) : bool :=
+  let (v1, w1) := p1 in
+  let (v2, w2) := p2 in
+  eqb_V v1 v2 && eqb_W w1 w2.
+
+Theorem soundness_of_equality_over_pairs :
+  forall (V : Type)
+         (eqb_V : V -> V -> bool),
+    (forall v1 v2 : V,
+        eqb_V v1 v2 = true -> v1 = v2) ->
+    forall (W : Type)
+           (eqb_W : W -> W -> bool),
+      (forall w1 w2 : W,
+          eqb_W w1 w2 = true -> w1 = w2) ->
+      forall p1 p2 : V * W,
+        eqb_pair V eqb_V W eqb_W p1 p2 = true ->
+        p1 = p2.
+Proof.
+  intros V eqb_V S_eqb_V W eqb_W S_eqb_W [v1 w1] [v2 w2] H_eqb.
+  unfold eqb_pair in H_eqb.
+  Search (_ && _ = true -> _ /\ _).
+  Check (andb_prop (eqb_V v1 v2) (eqb_W w1 w2)).
+  Check (andb_prop (eqb_V v1 v2) (eqb_W w1 w2) H_eqb).
+  destruct (andb_prop (eqb_V v1 v2) (eqb_W w1 w2) H_eqb) as [H_eqb_V H_eqb_W].
+  Check (S_eqb_V v1 v2 H_eqb_V).
+  rewrite -> (S_eqb_V v1 v2 H_eqb_V).
+  rewrite -> (S_eqb_W w1 w2 H_eqb_W).
+  reflexivity.
+Qed.
+
+Theorem completeness_of_equality_over_pairs :
+  forall (V : Type)
+         (eqb_V : V -> V -> bool),
+    (forall v1 v2 : V,
+        v1 = v2 -> eqb_V v1 v2 = true) ->
+    forall (W : Type)
+           (eqb_W : W -> W -> bool),
+      (forall w1 w2 : W,
+          w1 = w2 -> eqb_W w1 w2 = true) ->
+      forall p1 p2 : V * W,
+        p1 = p2 ->
+        eqb_pair V eqb_V W eqb_W p1 p2 = true.
+Proof.
+  intros V eqb_V S_eqb_V W eqb_W S_eqb_W [v1 w1] [v2 w2] H_eq.
+  unfold eqb_pair.
+  injection H_eq as H_eq_V H_eq_W.
+  Check (S_eqb_V v1 v2 H_eq_V).
+  rewrite -> (S_eqb_V v1 v2 H_eq_V).
+  rewrite -> (S_eqb_W w1 w2 H_eq_W).
+  unfold andb.
+  reflexivity.
+Qed.
+
+Theorem soundness_and_completeness_of_equality_over_pairs :
+  forall (V : Type)
+         (eqb_V : V -> V -> bool),
+    (forall v1 v2 : V,
+        eqb_V v1 v2 = true <-> v1 = v2) ->
+    forall (W : Type)
+           (eqb_W : W -> W -> bool),
+      (forall w1 w2 : W,
+          eqb_W w1 w2 = true <-> w1 = w2) ->
+      forall p1 p2 : V * W,
+        eqb_pair V eqb_V W eqb_W p1 p2 = true <-> p1 = p2.
+Proof.
+  intros V eqb_V SC_eqb_V.
+  Check (from_one_equivalence_to_two_implications V eqb_V SC_eqb_V).
+  destruct (from_one_equivalence_to_two_implications V eqb_V SC_eqb_V) as [S_eqb_V C_eqb_V].
+  intros W eqb_W SC_eqb_W.
+  Check (from_one_equivalence_to_two_implications W eqb_W SC_eqb_W).
+  destruct (from_one_equivalence_to_two_implications W eqb_W SC_eqb_W) as [S_eqb_W C_eqb_W].
+  intros p1 p2.
+  split.
+  - exact (soundness_of_equality_over_pairs V eqb_V S_eqb_V W eqb_W S_eqb_W p1 p2).
+  - exact (completeness_of_equality_over_pairs V eqb_V C_eqb_V W eqb_W C_eqb_W p1 p2).
+Qed.
+
+(* ********** *)
+
+Inductive binary_tree (V : Type) : Type :=
+  Leaf : V -> binary_tree V
+| Node : binary_tree V -> binary_tree V -> binary_tree V.
+
+Fixpoint eqb_binary_tree (V : Type) (eqb_V : V -> V -> bool) (t1 t2 : binary_tree V) : bool :=
+  match t1 with
+    Leaf _ v1 =>
+    match t2 with
+      Leaf _ v2 =>
+      eqb_V v1 v2
+    | Node _ t11 t12 =>
+      false
+    end
+  | Node _ t11 t12 =>
+    match t2 with
+      Leaf _ v2 =>
+      false
+    | Node _ t21 t22 =>
+      eqb_binary_tree V eqb_V t11 t21
+      &&
+      eqb_binary_tree V eqb_V t12 t22
+    end
+  end.
+
+Lemma fold_unfold_eqb_binary_tree_Leaf :
+  forall (V : Type)
+         (eqb_V : V -> V -> bool)
+         (v1 : V)
+         (t2 : binary_tree V),
+    eqb_binary_tree V eqb_V (Leaf V v1) t2 =
+    match t2 with
+      Leaf _ v2 =>
+      eqb_V v1 v2
+    | Node _ t11 t12 =>
+      false
+    end.
+Proof.
+  fold_unfold_tactic eqb_binary_tree.
+Qed.
+
+Lemma fold_unfold_eqb_binary_tree_Node :
+  forall (V : Type)
+         (eqb_V : V -> V -> bool)
+         (t11 t12 t2 : binary_tree V),
+    eqb_binary_tree V eqb_V (Node V t11 t12) t2 =
+    match t2 with
+      Leaf _ v2 =>
+      false
+    | Node _ t21 t22 =>
+      eqb_binary_tree V eqb_V t11 t21
+      &&
+      eqb_binary_tree V eqb_V t12 t22
+    end.
+Proof.
+  fold_unfold_tactic eqb_binary_tree.
+Qed.
+
+Theorem soundness_of_equality_over_binary_trees :
+  forall (V : Type)
+         (eqb_V : V -> V -> bool),
+    (forall v1 v2 : V,
+        eqb_V v1 v2 = true -> v1 = v2) ->
+    forall t1 t2 : binary_tree V,
+      eqb_binary_tree V eqb_V t1 t2 = true ->
+      t1 = t2.
+Proof.
+  intros V eqb_V S_eqb_V t1.
+  induction t1 as [v1 | t11 IHt11 t12 IHt12].
+  - intros [v2 | t21 t22] H_eqb.
+    -- rewrite -> (fold_unfold_eqb_binary_tree_Leaf V eqb_V v1 (Leaf V v2)) in H_eqb.
+       Check (S_eqb_V v1 v2 H_eqb).
+       rewrite -> (S_eqb_V v1 v2 H_eqb).
+       reflexivity.
+    -- rewrite -> (fold_unfold_eqb_binary_tree_Leaf V eqb_V v1 (Node V t21 t22)) in H_eqb.
+       discriminate H_eqb.
+  - intros [v2 | t21 t22] H_eqb.
+    -- rewrite -> (fold_unfold_eqb_binary_tree_Node V eqb_V t11 t12 (Leaf V v2)) in H_eqb.
+       discriminate H_eqb.
+    -- rewrite -> (fold_unfold_eqb_binary_tree_Node V eqb_V t11 t12 (Node V t21 t22)) in H_eqb.
+       Search (_ && _ = true -> _ /\ _).
+       Check (andb_prop (eqb_binary_tree V eqb_V t11 t21) (eqb_binary_tree V eqb_V t12 t22)).
+       Check (andb_prop (eqb_binary_tree V eqb_V t11 t21) (eqb_binary_tree V eqb_V t12 t22) H_eqb).
+       destruct (andb_prop (eqb_binary_tree V eqb_V t11 t21) (eqb_binary_tree V eqb_V t12 t22) H_eqb) as [H_eqb_1 H_eqb_2].
+       Check (IHt11 t21 H_eqb_1).
+       rewrite -> (IHt11 t21 H_eqb_1).
+       rewrite -> (IHt12 t22 H_eqb_2).
+       reflexivity.
+Qed.
+
+Theorem completeness_of_equality_over_binary_trees :
+  forall (V : Type)
+         (eqb_V : V -> V -> bool),
+    (forall v1 v2 : V,
+        v1 = v2 -> eqb_V v1 v2 = true) ->
+    forall t1 t2 : binary_tree V,
+      t1 = t2 ->
+      eqb_binary_tree V eqb_V t1 t2 = true.
+Proof.
+  intros V eqb_V C_eqb_V t1.
+  induction t1 as [v1 | t11 IHt11 t12 IHt12].
+  - intros [v2 | t21 t22] H_eq.
+    -- rewrite -> (fold_unfold_eqb_binary_tree_Leaf V eqb_V v1 (Leaf V v2)).
+       injection H_eq as H_eq_V.
+       Check (C_eqb_V v1 v2).
+       Check (C_eqb_V v1 v2 H_eq_V).
+       exact (C_eqb_V v1 v2 H_eq_V).
+    -- discriminate H_eq.
+  - intros [v2 | t21 t22] H_eq.
+    -- discriminate H_eq.
+    -- rewrite -> (fold_unfold_eqb_binary_tree_Node V eqb_V t11 t12 (Node V t21 t22)).
+       injection H_eq as H_eq_1 H_eq_2.
+       Check (IHt11 t21 H_eq_1).
+       rewrite -> (IHt11 t21 H_eq_1).
+       Search (true && _ = _).
+       rewrite -> (andb_true_l (eqb_binary_tree V eqb_V t12 t22)).
+       exact (IHt12 t22 H_eq_2).
+Qed.
+
+Theorem soundness_and_completeness_of_equality_over_binary_trees :
+  forall (V : Type)
+         (eqb_V : V -> V -> bool),
+    (forall v1 v2 : V,
+        eqb_V v1 v2 = true <-> v1 = v2) ->
+    forall t1 t2 : binary_tree V,
+      eqb_binary_tree V eqb_V t1 t2 = true <-> t1 = t2.
+Proof.
+  intros V eqb_V SC_eqb_V t1 t2.
+  Check (from_one_equivalence_to_two_implications V eqb_V SC_eqb_V).
+  destruct (from_one_equivalence_to_two_implications V eqb_V SC_eqb_V) as [S_eqb_V C_eqb_V].
+  split.
+  - exact (soundness_of_equality_over_binary_trees V eqb_V S_eqb_V t1 t2).
+  - exact (completeness_of_equality_over_binary_trees V eqb_V C_eqb_V t1 t2).
+
+  Restart.
+
+  intros V eqb_V SC_eqb_V t1.
+  induction t1 as [v1 | t11 IHt11 t12 IHt12].
+  - intros [v2 | t21 t22].
+    + rewrite -> (fold_unfold_eqb_binary_tree_Leaf V eqb_V v1 (Leaf V v2)).
+      split.
+      * intro H_eqb_V.
+        destruct (from_one_equivalence_to_two_implications V eqb_V SC_eqb_V) as [S_eqb_V _].
+        rewrite -> (S_eqb_V v1 v2 H_eqb_V).
+        reflexivity.
+      * intro H_eq.
+        injection H_eq as H_eq.
+        destruct (from_one_equivalence_to_two_implications V eqb_V SC_eqb_V) as [_ C_eqb_V].
+        exact (C_eqb_V v1 v2 H_eq).
+    + rewrite -> (fold_unfold_eqb_binary_tree_Leaf V eqb_V v1 (Node V t21 t22)).
+      split.
+      * intro H_absurd.
+        discriminate H_absurd.
+      * intro H_absurd.
+        discriminate H_absurd.
+  - intros [v2 | t21 t22].
+    + rewrite -> (fold_unfold_eqb_binary_tree_Node V eqb_V t11 t12 (Leaf V v2)).
+      split.
+      * intro H_absurd.
+        discriminate H_absurd.
+      * intro H_absurd.
+        discriminate H_absurd.
+    + rewrite -> (fold_unfold_eqb_binary_tree_Node V eqb_V t11 t12 (Node V t21 t22)).
+      split.
+      * intro H_eqb.
+        destruct (andb_prop (eqb_binary_tree V eqb_V t11 t21) (eqb_binary_tree V eqb_V t12 t22) H_eqb) as [H_eqb_1 H_eqb_2].
+        destruct (IHt11 t21) as [H_key1 _].
+        destruct (IHt12 t22) as [H_key2 _].
+        rewrite -> (H_key1 H_eqb_1).
+        rewrite -> (H_key2 H_eqb_2).
+        reflexivity.
+      * intro H_eq.
+        injection H_eq as H_eq_1 H_eq_2.
+        destruct (IHt11 t21) as [_ H_key1].
+        destruct (IHt12 t22) as [_ H_key2].
+        rewrite -> (H_key1 H_eq_1).
+        rewrite -> (andb_true_l (eqb_binary_tree V eqb_V t12 t22)).
+        exact (H_key2 H_eq_2).
+Qed.        
+
+(* ********** *)
+
+(* pilfering from the String library: *)
+
+Require Import String Ascii.
+
+Print string.
+
+Check "foo"%string.
+
+Definition eqb_char (c1 c2 : ascii) : bool :=
+  match c1 with
+    Ascii b11 b12 b13 b14 b15 b16 b17 b18 =>
+    match c2 with
+      Ascii b21 b22 b23 b24 b25 b26 b27 b28 =>
+      eqb_bool b11 b21 && eqb_bool b12 b22 && eqb_bool b13 b23 && eqb_bool b14 b24 && eqb_bool b15 b25 && eqb_bool b16 b26 && eqb_bool b17 b27 && eqb_bool b18 b28
+    end
+  end.
+
+Proposition soundness_of_eqb_char :
+  forall c1 c2 : ascii,
+    eqb_char c1 c2 = true -> c1 = c2.
+Proof.
+Admitted.
+
+Proposition completeness_of_eqb_char :
+  forall c1 c2 : ascii,
+    c1 = c2 -> eqb_char c1 c2 = true.
+Proof.
+Admitted.
+
+Fixpoint eqb_string (c1s c2s : string) : bool :=
+  match c1s with
+    String.EmptyString =>
+    match c2s with
+      String.EmptyString =>
+      true
+    |  String.String c2 c2s' =>
+      false
+    end
+  | String.String c1 c1s' =>
+    match c2s with
+      String.EmptyString =>
+      true
+    | String.String c2 c2s' =>
+      eqb_char c1 c2 && eqb_string c1s' c2s'
+    end
+  end.
+
+Lemma fold_unfold_eqb_string_Empty :
+  forall c2s : string,
+    eqb_string String.EmptyString c2s =
+    match c2s with
+      String.EmptyString =>
+      true
+    | String.String c2 c2s' =>
+      false
+    end.
+Proof.
+  fold_unfold_tactic eqb_string.
+Qed.
+
+Lemma fold_unfold_eqb_string_String :
+  forall (c1 : ascii)
+         (c1s' c2s : string),
+    eqb_string (String.String c1 c1s') c2s =
+    match c2s with
+      String.EmptyString =>
+      true
+    | String.String c2 c2s' =>
+      eqb_char c1 c2 && eqb_string c1s' c2s'
+    end.
+Proof.
+  fold_unfold_tactic eqb_string.
+Qed.
+
+Proposition soundness_of_eqb_string :
+  forall c1s c2s : string,
+    eqb_string c1s c2s = true -> c1s = c2s.
+Proof.
+Admitted.
+
+Proposition completeness_of_eqb_string :
+  forall c1s c2s : string,
+    c1s = c2s -> eqb_string c1s c2s = true.
+Proof.
+Admitted.
+
+(* ********** *)
+
+Inductive funky_tree : Type :=
+  Nat : nat -> funky_tree
+| Bool : bool -> funky_tree
+| String : string -> funky_tree
+| Singleton : funky_tree -> funky_tree
+| Pair : funky_tree -> funky_tree -> funky_tree
+| Triple : funky_tree -> funky_tree -> funky_tree -> funky_tree.
+
+(* ***** *)
+
+(* A silly proposition, just to get a feel about how to destructure a value of type funky_tree: *)
+
+Proposition identity_over_funky_tree :
+  forall e : funky_tree,
+    e = e.
+Proof.
+  intro e.
+  case e as [n | b | s | e1 | e1 e2 | e1 e2 e3] eqn:H_e.
+  - reflexivity.
+  - reflexivity.
+  - reflexivity.
+  - reflexivity.
+  - reflexivity.
+  - reflexivity.
+Qed.
+
+(* ***** *)
+
+(* Exercise: implement eqb_funky_tree and prove its soundness and completeness. *)
+
+(* ********** *)
+
+(* end of week-06_soundness-and-completeness-of-equality-predicates.v *)

cs3234/labs/week-07_isometries3.v

@@ -0,0 +1,514 @@
+(* week-07_isometries3.v *)
+(* LPP 2024 - CS3234 2023-2024, Sem2 *)
+(* Olivier Danvy <danvy@yale-nus.edu.sg> *)
+(* Version of 08 Mar 2024 *)
+
+(* ********** *)
+
+(* A formal study of isometries of the equilateral triangle, *)
+(* after Chantal Keller, Damien Pous and Sylvain Chevillard. *)
+
+(* ********** *)
+
+Inductive Rotation : Type :=
+  R000 : Rotation  (* 0 degrees (identity) *)
+| R120 : Rotation  (* 120 degrees *)
+| R240 : Rotation. (* 240 degrees *)
+
+(* ********** *)
+
+(* Performing two rotations in a row, clockwise. *)
+(* "RaR" stands for "a Rotation after a Rotation" *)
+
+Definition RaR (r2 r1: Rotation) : Rotation :=
+  match r1 with
+    R000 => match r2 with
+              R000 => R000
+            | R120 => R120
+            | R240 => R240
+            end
+  | R120 => match r2 with
+              R000 => R120
+            | R120 => R240
+            | R240 => R000
+            end
+  | R240 => match r2 with
+              R000 => R240
+            | R120 => R000
+            | R240 => R120
+            end
+  end.
+
+(* Some properties: *)
+
+Proposition R000_is_neutral_for_RaR_on_the_left :
+  forall r : Rotation,
+    RaR R000 r = r.
+Proof.
+  intros [ | | ].
+  - unfold RaR.
+    reflexivity.
+  - unfold RaR.
+    reflexivity.
+  - unfold RaR.
+    reflexivity.
+Qed.
+
+Proposition R000_is_neutral_for_RaR_on_the_right :
+  forall r : Rotation,
+    RaR r R000 = r.
+Proof.
+  intros [ | | ]; unfold RaR.
+  reflexivity.
+  reflexivity.
+  reflexivity.
+Qed.
+
+Proposition RaR_is_commutative :
+  forall r1 r2 : Rotation,
+    RaR r2 r1 = RaR r1 r2.
+Proof.
+  intros [ | | ] [ | | ]; unfold RaR; reflexivity.
+  Restart.
+  intros [ | | ] [ | | ]; reflexivity.
+Qed.
+
+Proposition RaR_is_associative :
+  forall r1 r2 r3 : Rotation,
+    RaR (RaR r3 r2) r1 = RaR r3 (RaR r2 r1).
+Proof.
+  intros [ | | ] [ | | ] [ | | ]; reflexivity.
+Abort.
+
+Proposition RaR_is_nilpotent_with_order_3 :
+  forall r : Rotation,
+    RaR (RaR r r) (RaR r r)  = r.
+Proof.
+  intros [ | | ]; unfold RaR; reflexivity.
+Qed.
+
+(* Abort. *)
+
+(* ********** *)
+
+(* The following symmetries are indexed by the invariant vertex: *)
+
+Inductive Reflection : Type :=
+  S_NN : Reflection  (* North, at the top *)
+| S_SW : Reflection  (* South-West, at the bottom left *)
+| S_SE : Reflection. (* South-East, at the bottom right *)
+
+(* These reflections are symmetries here. *)
+
+(* Performing two reflections in a row. *)
+(* "SaS" stands for "a Symmetry after a Symmetry" *)
+
+Definition SaS (s2 s1 : Reflection) : Rotation :=
+  match s1 with
+    S_NN => match s2 with
+              S_NN => R000
+            | S_SW => R120
+            | S_SE => R240
+            end
+  | S_SW => match s2 with
+              S_NN => R240
+            | S_SW => R000
+            | S_SE => R120
+            end
+  | S_SE => match s2 with
+              S_NN => R120
+            | S_SW => R240
+            | S_SE => R000
+            end
+  end.
+
+(* is SaS commutative? *)
+Proposition SaS_is_not_commutative :
+  exists s1 s2 : Reflection,
+    SaS s1 s2 <> SaS s2 s1.
+Proof.
+  exists S_NN, S_SW.
+  unfold SaS.
+  unfold not.
+  intro H_absurd.
+  discriminate H_absurd.
+Qed.
+(* is SaS associative? *)
+
+(* is SaS nilpotent?   *)
+
+(* ********** *)
+
+(* Performing a rotation and then a reflection in a row. *)
+(* "SaR" stands for "a Symmetry after a Rotation" *)
+
+Definition SaR (s : Reflection) (r : Rotation) : Reflection :=
+  match r with
+    R000 => match s with
+              S_NN => S_NN
+            | S_SW => S_SW
+            | S_SE => S_SE
+            end
+  | R120 => match s with
+              S_NN => S_SE
+            | S_SW => S_NN
+            | S_SE => S_SW
+            end
+  | R240 => match s with
+              S_NN => S_SW
+            | S_SW => S_SE
+            | S_SE => S_NN
+            end
+  end.
+
+(* ********** *)
+
+(* Performing a reflection and then a rotation in a row. *)
+(* "RaS" stands for "a Rotation after a Symmetry" *)
+
+Definition RaS (r : Rotation) (s : Reflection) : Reflection :=
+  match s with
+    S_NN => match r with
+              R000 => S_NN
+            | R120 => S_SW
+            | R240 => S_SE
+            end
+  | S_SW => match r with
+              R000 => S_SW
+            | R120 => S_SE
+            | R240 => S_NN
+            end
+  | S_SE => match r with
+              R000 => S_SE
+            | R120 => S_NN
+            | R240 => S_SW
+            end
+  end.
+
+(* ********** *)
+
+Inductive Isomorphism : Type :=
+| IR : Rotation -> Isomorphism
+| IS : Reflection -> Isomorphism.
+
+(* Identity: *)
+
+Definition Id : Isomorphism := IR R000.
+
+(* Composition: *)
+
+Definition C (i2 i1 : Isomorphism) : Isomorphism :=
+  match i1 with
+    IR r1 => match i2 with
+               IR r2 => IR (RaR r2 r1)
+             | IS s2 => IS (SaR s2 r1)
+             end
+  | IS s1 => match i2 with
+               IR r2 => IS (RaS r2 s1)
+             | IS s2 => IR (SaS s2 s1)
+             end
+  end.
+
+Proposition Id_is_neutral_on_the_left_of_C :
+  forall i : Isomorphism,
+    C Id i = i.
+Proof.
+  intros [[ | | ] | [ | | ]]; reflexivity.
+Qed.
+
+Proposition Id_is_neutral_on_the_right_of_C :
+  forall i : Isomorphism,
+    C i Id = i.
+Proof.
+  intros [[ | | ] | [ | | ]]; reflexivity.
+Qed.
+
+Proposition C_is_associative :
+  forall i1 i2 i3 : Isomorphism,
+    C i3 (C i2 i1) = C (C i3 i2) i1.
+Proof.
+  intros [[ | | ] | [ | | ]]
+    [[ | | ] | [ | | ]]
+    [[ | | ] | [ | | ]] ; reflexivity.
+Abort.
+
+Lemma composing_an_isomorphism_is_injective_on_the_right :
+  forall i x y : Isomorphism,
+    C i x = C i y -> x = y.
+Proof.
+  intros [[ | | ] | [ | | ]]
+         [[ | | ] | [ | | ]]
+         [[ | | ] | [ | | ]]; unfold C, RaR, SaR, RaS, SaS.
+  - intro H.
+    reflexivity.
+  - intro H_absurd.
+    discriminate H_absurd.
+    Restart.
+  intros [[ | | ] | [ | | ]]
+         [[ | | ] | [ | | ]]
+         [[ | | ] | [ | | ]];
+    intro H; (reflexivity || discriminate H).
+
+
+
+Qed.
+
+Lemma composing_an_isomorphism_is_injective_on_the_left :
+  forall i x y : Isomorphism,
+    C x i = C y i -> x = y.
+Proof.
+  intros [[ | | ] | [ | | ]]
+         [[ | | ] | [ | | ]]
+         [[ | | ] | [ | | ]];
+    intro H; (reflexivity || discriminate H).
+Qed.
+
+Lemma composing_an_isomorphism_is_surjective_on_the_right :
+  forall i2 i3 : Isomorphism,
+    exists i1 : Isomorphism,
+      C i2 i1 = i3.
+Proof.
+  intros [[ | | ] | [ | | ]]
+         [[ | | ] | [ | | ]].
+  - exists Id.
+    reflexivity.
+  - exists (IR R120).
+    reflexivity.
+  - exists (IR R240).
+    reflexivity.
+    Restart.
+  intros [[ | | ] | [ | | ]]
+         [[ | | ] | [ | | ]];
+    (
+      (exists (IR R000); reflexivity )
+      ||
+        (exists (IR R120); reflexivity )
+      ||
+        (exists (IR R240); reflexivity )
+      ||
+        (exists (IS S_NN); reflexivity )
+      ||
+        (exists (IS S_SW); reflexivity )
+      ||
+        (exists (IS S_SE); reflexivity )
+    ).
+  Show Proof.
+Qed.
+
+Lemma composing_an_isomorphism_is_surjective_on_the_left :
+  forall i1 i3 : Isomorphism,
+    exists i2 : Isomorphism,
+      C i2 i1 = i3.
+Proof.
+  intros [[ | | ] | [ | | ]]
+         [[ | | ] | [ | | ]];
+    (
+      (exists (IR R000); reflexivity )
+      ||
+        (exists (IR R120); reflexivity )
+      ||
+        (exists (IR R240); reflexivity )
+      ||
+        (exists (IS S_NN); reflexivity )
+      ||
+        (exists (IS S_SW); reflexivity )
+      ||
+        (exists (IS S_SE); reflexivity )
+    ).
+Qed.
+
+Proposition C_over_rotations_is_nilpotent_with_order_3 :
+  forall r : Rotation,
+    C (C (IR r) (IR r)) (IR r) = Id.
+Proof.
+Abort.
+
+Proposition C_over_symmetries_is_nilpotent_with_order_2 :
+  forall s : Reflection,
+    C (IS s) (IS s) = Id.
+Proof.
+  intros [ | | ]; unfold C, SaS, Id; reflexivity.
+Qed.
+
+(* Proposition C_is_nilpotent_with_order_??? : *)
+(*   forall i : Isomorphism, *)
+(*     ... *)
+(* Proof. *)
+(* Abort. *)
+
+(* ********** *)
+
+(* Let us now introduce the vertices: *)
+
+Inductive Vertex : Type := (* enumerated clockwise *)
+  NN : Vertex
+| SW : Vertex
+| SE : Vertex.
+
+(* And let us define the effect of applying an isomorphism
+   to a vertex: *)
+
+Definition A (i : Isomorphism) (v : Vertex) : Vertex :=
+  match i with
+    IR r => match r with
+              R000 => match v with
+                        NN => NN
+                      | SW => SW
+                      | SE => SE
+                      end
+            | R120 => match v with
+                        NN => SW
+                      | SW => SE
+                      | SE => NN
+                      end
+            | R240 => match v with
+                        NN => SE
+                      | SE => SW
+                      | SW => NN
+                      end
+            end
+  | IS s => match s with
+              S_NN => match v with
+                        NN => NN
+                      | SW => SE
+                      | SE => SW
+                      end
+            | S_SE => match v with
+                        NN => SW
+                      | SW => NN
+                      | SE => SE
+                      end
+            | S_SW => match v with
+                        NN => SE
+                      | SW => SW
+                      | SE => NN
+                      end
+              end
+  end.
+
+(*
+Proposition A_is_equivalent_to_C :
+  forall (i1 i2 : Isomorphism) (v : Vertex),
+    A i2 (A i1 v) = A (C i2 i1) v.
+Proof.
+Abort.
+
+Proposition applying_an_isomorphism_is_injective :
+  forall (i : Isomorphism) (v1 v2 : Vertex),
+    (A i v1 = A i v2) -> v1 = v2.
+Proof.
+Abort.
+
+Proposition applying_an_isomorphism_is_surjective :
+  forall (i : Isomorphism) (v2 : Vertex),
+    exists v1 : Vertex,
+      A i v1 = v2.
+Proof.
+Abort.
+*)
+
+(* ********** *)
+
+(* Intensional equality:
+   two isomorphisms are equal
+   iff
+   they are are constructed alike.
+ *)
+
+Definition intensional_equality (i1 i2: Isomorphism) : Prop :=
+  i1 = i2.
+
+(* Extensional equality:
+   two isomorphisms are equal
+   iff
+   their graphs are the same.
+ *)
+
+Definition extensional_equality (i1 i2: Isomorphism) : Prop :=
+  forall v : Vertex,
+    A i1 v = A i2 v.
+
+(* The two notions of equalities coincide: *)
+
+Proposition the_two_equalities_are_the_same :
+  forall i1 i2 : Isomorphism,
+    intensional_equality i1 i2 <-> extensional_equality i1 i2.
+Proof.
+Abort.
+
+(* ********** *)
+
+(*
+Lemma isomorphism_equality_in_context_on_the_left :
+  forall x y i : Isomorphism,
+    x = y -> C x i = C y i.
+Proof.
+Abort.
+
+Proposition take_five :
+  forall i : Isomorphism,
+    extensional_equality (C (C (C (C i i) i) i) i) Id
+    ->
+    i = Id.
+Proof.
+Abort.
+
+Proposition characteristic_property_of_Id :
+  forall i : Isomorphism,
+    i = Id <-> forall v : Vertex, A i v = v.
+Proof.
+Abort.
+
+Proposition one_for_the_road :
+  forall i : Isomorphism,
+    (forall v : Vertex, A i v = v)
+    ->
+    C i i = Id.
+Proof.
+Abort.
+
+Proposition notable_property_of_Id :
+  exists i : Isomorphism,
+    exists v : Vertex,
+      not (A i v = v -> i = Id).
+Proof.
+Abort.
+
+Proposition notable_property_of_Id' :
+  not (forall (i : Isomorphism) (v : Vertex),
+         A i v = v -> i = Id).
+Proof.
+Abort.
+
+Proposition notable_property_of_symmetries :
+  forall (i : Isomorphism)
+         (v : Vertex),
+    A i v = v ->
+    ((i = IR R0)
+     \/
+     (exists s : Reflection,
+        i = IS s)).
+Proof.
+Abort.
+
+Proposition notable_property_of_symmetries' :
+  forall i : Isomorphism,
+    (exists v : Vertex,
+       A i v = v) ->
+    ((i = IR R0)
+     \/
+     (exists s : Reflection,
+        i = IS s)).
+Proof.
+Abort.
+
+Proposition one_more_for_the_road :
+  forall (i : Isomorphism) (v : Vertex),
+    A i v = v -> C i i = Id.
+Proof.
+Abort.
+*)
+
+(* ********** *)
+
+(* end of week-07_isometries3.v *)

cs3234/labs/week-07_soundness-and-completeness-of-equality-predicates-revisited.v

@@ -0,0 +1,281 @@
+(* week-07_soundness-and-completeness-of-equality-predicates-revisited.v *)
+(* LPP 2024 - S3C234 2023-2024, Sem2 *)
+(* Olivier Danvy <danvy@yale-nus.edu.sg> *)
+(* Version of 08 Mar 2024 *)
+
+(* ********** *)
+
+Ltac fold_unfold_tactic name := intros; unfold name; fold name; reflexivity.
+
+Require Import Arith Bool List.
+
+(* ********** *)
+
+Definition is_a_sound_and_complete_equality_predicate (V : Type) (eqb_V : V -> V -> bool) :=
+  forall v1 v2 : V,
+    eqb_V v1 v2 = true <-> v1 = v2.
+
+(* ********** *)
+
+Check Bool.eqb.
+(* eqb : bool -> bool -> bool *)
+
+Definition eqb_bool (b1 b2 : bool) : bool :=
+  match b1 with
+    true =>
+    match b2 with
+      true =>
+      true
+    | false =>
+      false
+    end
+  | false =>
+    match b2 with
+      true =>
+      false
+    | false =>
+      true
+    end
+  end.
+
+Lemma eqb_bool_is_reflexive :
+  forall b : bool,
+    eqb_bool b b = true.
+Proof.
+Abort.
+
+Search (eqb _ _ = _ -> _ = _).
+(* eqb_prop: forall a b : bool, eqb a b = true -> a = b *)
+
+Proposition soundness_and_completeness_of_eqb_bool :
+  is_a_sound_and_complete_equality_predicate bool eqb_bool.
+Proof.
+  unfold is_a_sound_and_complete_equality_predicate.
+Proof.
+Abort.
+
+(* ***** *)
+
+Proposition soundness_and_completeness_of_eqb_bool :
+  is_a_sound_and_complete_equality_predicate bool eqb.
+Proof.
+Abort.
+
+(* ********** *)
+
+Check Nat.eqb.
+(* Nat.eqb : nat -> nat -> bool *)
+
+Fixpoint eqb_nat (n1 n2 : nat) : bool :=
+  match n1 with
+    O =>
+    match n2 with
+      O =>
+      true
+    | S n2' =>
+      false
+    end
+  | S n1' =>
+    match n2 with
+      O =>
+      false
+    | S n2' =>
+      eqb_nat n1' n2'
+    end
+  end.
+
+Lemma fold_unfold_eqb_nat_O :
+  forall n2 : nat,
+    eqb_nat 0 n2 =
+    match n2 with
+      O =>
+      true
+    | S _ =>
+      false
+    end.
+Proof.
+  fold_unfold_tactic eqb_nat.
+Qed.
+
+Lemma fold_unfold_eqb_nat_S :
+  forall n1' n2 : nat,
+    eqb_nat (S n1') n2 =
+    match n2 with
+      O =>
+      false
+    | S n2' =>
+      eqb_nat n1' n2'
+    end.
+Proof.
+  fold_unfold_tactic eqb_nat.
+Qed.
+
+Search (Nat.eqb _ _ = true -> _ = _).
+(* beq_nat_true: forall n m : nat, (n =? m) = true -> n = m *)
+
+Proposition soundness_and_completeness_of_eqb_nat :
+  is_a_sound_and_complete_equality_predicate nat eqb_nat.
+Proof.
+Abort.
+
+(* ***** *)
+
+Lemma fold_unfold_eqb_Nat_O :
+  forall n2 : nat,
+    0 =? n2 =
+    match n2 with
+      O =>
+      true
+    | S _ =>
+      false
+    end.
+Proof.
+  fold_unfold_tactic Nat.eqb.
+Qed.
+
+Lemma fold_unfold_eqb_Nat_S :
+  forall n1' n2 : nat,
+    S n1' =? n2 =
+    match n2 with
+      O =>
+      false
+    | S n2' =>
+      n1' =? n2'
+    end.
+Proof.
+  fold_unfold_tactic Nat.eqb.
+Qed.
+
+Proposition soundness_and_completeness_of_eqb_nat :
+  is_a_sound_and_complete_equality_predicate nat Nat.eqb.
+Proof.
+Abort.
+
+(* ********** *)
+
+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 v2 =>
+      false
+    | None =>
+      true
+    end
+  end.
+
+Proposition soundness_and_completeness_of_eqb_option :
+  forall (V : Type)
+         (eqb_V : V -> V -> bool),
+    is_a_sound_and_complete_equality_predicate V eqb_V ->
+    is_a_sound_and_complete_equality_predicate (option V) (eqb_option V eqb_V).
+Proof.
+Abort.
+
+(* ***** *)
+
+(*
+Definition eqb_option_option (V : Type) (eqb_V : V -> V -> bool) (oov1 oov2 : option (option V)) : bool :=
+*)
+
+(*
+Proposition soundness_and_completeness_of_eqb_option_option :
+  forall (V : Type)
+         (eqb_V : V -> V -> bool),
+    is_a_sound_and_complete_equality_predicate V eqb_V ->
+    is_a_sound_and_complete_equality_predicate (option (option V)) (eqb_option_option V eqb_V).
+Proof.
+Abort.
+*)
+
+(* ********** *)
+
+Definition eqb_pair (V : Type) (eqb_V : V -> V -> bool) (W : Type) (eqb_W : W -> W -> bool) (p1 p2 : V * W) : bool :=
+  match p1 with
+    (v1, w1) =>
+    match p2 with
+      (v2, w2) =>
+      eqb_V v1 v2 && eqb_W w1 w2
+    end
+  end.
+
+Proposition soundness_and_completeness_of_eqb_pair :
+  forall (V : Type)
+         (eqb_V : V -> V -> bool)
+         (W : Type)
+         (eqb_W : W -> W -> bool),
+    is_a_sound_and_complete_equality_predicate V eqb_V ->
+    is_a_sound_and_complete_equality_predicate W eqb_W ->
+    is_a_sound_and_complete_equality_predicate (V * W) (eqb_pair V eqb_V W eqb_W).
+Proof.
+Abort.
+
+(* ********** *)
+
+Fixpoint eqb_list (V : Type) (eqb_V : V -> V -> bool) (v1s v2s : list V) : bool :=
+  match v1s with
+    nil =>
+    match v2s with
+      nil =>
+      true
+    | v2 :: v2s' =>
+      false
+    end
+  | v1 :: v1s' =>
+    match v2s with
+      nil =>
+      false
+    | v2 :: v2s' =>
+      eqb_V v1 v2 && eqb_list V eqb_V v1s' v2s'
+    end
+  end.
+
+Lemma fold_unfold_eqb_list_nil :
+  forall (V : Type)
+         (eqb_V : V -> V -> bool)
+         (v2s : list V),
+    eqb_list V eqb_V nil v2s =
+    match v2s with
+      nil =>
+      true
+    | v2 :: v2s' =>
+      false
+    end.
+Proof.
+  fold_unfold_tactic eqb_list.
+Qed.
+
+Lemma fold_unfold_eqb_list_cons :
+  forall (V : Type)
+         (eqb_V : V -> V -> bool)
+         (v1 : V)
+         (v1s' v2s : list V),
+    eqb_list V eqb_V (v1 :: v1s') v2s =
+    match v2s with
+      nil =>
+      false
+    | v2 :: v2s' =>
+      eqb_V v1 v2 && eqb_list V eqb_V v1s' v2s'
+    end.
+Proof.
+  fold_unfold_tactic eqb_list.
+Qed.
+
+Proposition soundness_and_completeness_of_eqb_list :
+  forall (V : Type)
+         (eqb_V : V -> V -> bool),
+    is_a_sound_and_complete_equality_predicate V eqb_V ->
+    is_a_sound_and_complete_equality_predicate (list V) (eqb_list V eqb_V).
+Proof.
+Abort.
+
+(* ********** *)
+
+(* end of week-07_soundness-and-completeness-of-equality-predicates-revisited.v *)

cs3234/labs/week-09_formalizing-two-by-two-matrices.v

@@ -0,0 +1,126 @@
+(* week-09_formalizing-two-by-two-matrices.v *)
+(* LPP 2024 - CS3234 2023-2024, Sem2 *)
+(* Olivier Danvy <danvy@yale-nus.edu.sg> *)
+(* Version of Fri 22 Mar 2024 *)
+
+(* ********** *)
+
+Ltac fold_unfold_tactic name := intros; unfold name; fold name; reflexivity.
+
+Require Import Arith.
+
+(* ********** *)
+
+Inductive m22 : Type := M22 : nat -> nat -> nat -> nat -> m22.
+
+Property componential_equality_m22 :
+  forall x11 x12 x21 x22 y11 y12 y21 y22 : nat,
+    M22 x11 x12
+        x21 x22 =
+    M22 y11 y12
+        y21 y22
+    <->
+    x11 = y11 /\ x12 = y12 /\ x21 = y21 /\ x22 = y22.
+Proof.
+  intros x11 x12 x21 x22 y11 y12 y21 y22.
+  split.
+
+  - intro H_tmp.
+    injection H_tmp as H11 H12 H21 H22.
+    rewrite -> H11.
+    rewrite -> H12.
+    rewrite -> H21.
+    rewrite -> H22.
+    split; [reflexivity | split; [reflexivity | split; [reflexivity | reflexivity]]].
+
+  - intros [H11 [H12 [H21 H22]]].
+    rewrite -> H11.
+    rewrite -> H12.
+    rewrite -> H21.
+    rewrite -> H22.
+    reflexivity.
+Qed.
+
+(* ***** *)
+
+Definition zero_m22 := M22 0 0
+                           0 0.
+
+Definition add_m22 (x y : m22) : m22 :=
+  match (x, y) with
+    (M22 x11 x12
+         x21 x22,
+     M22 y11 y12
+         y21 y22) =>
+    M22 (x11 + y11) (x12 + y12)
+        (x21 + y21) (x22 + y22)
+  end.
+
+Lemma add_m22_assoc :
+  forall x y z : m22,
+    add_m22 x (add_m22 y z) =
+    add_m22 (add_m22 x y) z.
+Proof.
+  intros [x11 x12
+          x21 x22]
+         [y11 y12
+          y21 y22]
+         [z11 z12
+          z21 z22].
+  unfold add_m22.
+  rewrite ->4 Nat.add_assoc.
+  reflexivity.
+Qed.
+
+Lemma add_m22_0_l :
+  forall x : m22,
+    add_m22 zero_m22 x = 
+    x.
+Proof.
+  intros [x11 x12
+          x21 x22].
+  unfold add_m22, zero_m22.
+  rewrite ->4 Nat.add_0_l.
+  reflexivity.
+Qed.
+
+Lemma add_m22_0_r :
+  forall x : m22,
+    add_m22 x zero_m22 =
+    x.
+Proof.
+  intros [x11 x12
+          x21 x22].
+  unfold add_m22, zero_m22.
+  rewrite ->4 Nat.add_0_r.
+  reflexivity.
+Qed.
+
+(* ********** *)
+
+Inductive mm22 : Type := MM22 : m22 -> m22 -> m22 -> m22 -> mm22.
+
+Definition mul_m22 (x y : m22) :=
+  match (x, y) with
+    (M22 x11 x12
+         x21 x22,
+     M22 y11 y12
+         y21 y22) =>
+      M22 (x11 * y11 + x12 * y21) (x11 * y12 + x12 * y22)
+          (x21 * y11 + x22 * y21) (x21 * y12 + x22 * y22)
+      end.
+
+Property mul_m22_assoc :
+  forall (m1 m2 m3 : m22),
+    mul_m22 m1 (mul_m22 m2 m3) = (mul_m22 (mul_m22 m1 m2) m3).
+Proof.
+  intros [m1_11 m1_12 m1_21 m1_22]
+         [m2_11 m2_12 m2_21 m2_22]
+         [m3_11 m3_12 m3_21 m3_22].
+  unfold mul_m22.
+  rewrite -> 4 Nat.mul_add_distr_r.
+Qed.
+
+(* ********** *)
+
+(* week-09_formalizing-two-by-two-matrices.v *)

cs3234/labs/week-10_the-abstraction-and-instantiation-of-Eureka-lemmas-about-resetting-the-accumulator.v

@@ -0,0 +1,434 @@
+(* week-10_the-abstraction-and-instantiation-of-Eureka-lemmas-about-resetting-the-accumulator.v *)
+(* LPP 2024 - CS3234 2023-2024, Sem2 *)
+(* Olivier Danvy <danvy@yale-nus.edu.sg> *)
+(* Version of 04 Apr 2024 *)
+
+(* ********** *)
+
+Ltac fold_unfold_tactic name := intros; unfold name; fold name; reflexivity.
+
+Require Import Arith Bool List.
+
+(* ********** *)
+
+Definition make_Eureka_lemma (A : Type) (id_A : A) (combine_A : A -> A -> A) (c : A -> A) (a : A) : Prop :=
+  c a = combine_A (c id_A) a.
+
+
+(* ********** *)
+
+Fixpoint power_acc (x n a : nat) : nat :=
+  match n with
+    O =>
+    a
+  | S n' =>
+    power_acc x n' (x * a)
+  end.
+
+Definition power_alt (x n : nat) : nat :=
+  power_acc x n 1.
+
+
+Check (forall x n a : nat, make_Eureka_lemma nat 1 Nat.mul (power_acc x n) a).
+
+Lemma fold_unfold_power_acc_O :
+  forall x a : nat,
+    power_acc x 0 a =
+    a.
+Proof.
+  fold_unfold_tactic power_acc.
+Qed.
+
+Lemma fold_unfold_power_acc_S :
+  forall x n' a : nat,
+    power_acc x (S n') a =
+    power_acc x n' (x * a).
+Proof.
+  fold_unfold_tactic power_acc.
+Qed.
+
+Check (make_Eureka_lemma nat).
+Check (make_Eureka_lemma nat 1).
+Check (make_Eureka_lemma nat 1).
+Check (make_Eureka_lemma nat 1 Nat.mul).
+Check (forall x n a : nat, make_Eureka_lemma nat 1 Nat.mul (power_acc x n) a).
+
+Lemma about_power_acc :
+  forall x n a : nat,
+    power_acc x n a = power_acc x n 1 * a.
+Proof.
+  intros x n.
+  induction n as [ | n' IHn']; intro a.
+  - rewrite ->2 fold_unfold_power_acc_O.
+    exact (eq_sym (Nat.mul_1_l a)).
+  - rewrite ->2 fold_unfold_power_acc_S.
+    rewrite -> Nat.mul_1_r.
+    rewrite -> (IHn' (x * a)).
+    rewrite -> (IHn' x).
+    Check Nat.mul_assoc.
+    apply Nat.mul_assoc.
+Qed.
+
+Lemma about_power_acc_generically :
+  forall x n a : nat,
+    make_Eureka_lemma nat 1 Nat.mul (power_acc x n) a.
+Proof.
+  unfold make_Eureka_lemma.
+  exact about_power_acc.
+Qed.
+
+(* ********** *)
+
+Fixpoint add_acc (n a : nat) : nat :=
+  match n with
+    O =>
+    a
+  | S n' =>
+    add_acc n' (S a)
+  end.
+
+Definition add_alt (n m : nat) : nat :=
+  add_acc n m.
+
+Lemma fold_unfold_add_acc_O :
+  forall a : nat,
+    add_acc 0 a =
+    a.
+Proof.
+  fold_unfold_tactic add_acc.
+Qed.
+
+Lemma fold_unfold_add_acc_S :
+  forall n' a : nat,
+    add_acc (S n') a =
+    add_acc n' (S a).
+Proof.
+  fold_unfold_tactic add_acc.
+Qed.
+
+Lemma about_add_acc :
+  forall n a : nat,
+    add_acc n a = add_acc n 0 + a.
+Proof.
+  intro n.
+  induction n as [ | n' IHn']; intro a.
+  - rewrite ->2 fold_unfold_add_acc_O.
+    exact (eq_sym (Nat.add_0_l a)).
+  - rewrite ->2 fold_unfold_add_acc_S.
+    rewrite -> (IHn' (S a)).
+    rewrite -> (IHn' 1).
+    rewrite <- Nat.add_assoc.
+    rewrite -> (Nat.add_1_l a).
+    reflexivity.
+Qed.
+
+Lemma about_add_acc_generically :
+  forall n a : nat,
+    make_Eureka_lemma nat 0 Nat.add (add_acc n) a.
+Proof.
+  unfold make_Eureka_lemma.
+  exact about_add_acc.
+Qed.
+
+(* ********** *)
+
+(* Exercise 02 *)
+
+Fixpoint length_acc (V : Type) (vs : list V) (a : nat) : nat :=
+  match vs with
+    nil =>
+    a
+  | v :: vs' =>
+    length_acc V vs' (S a)
+  end.
+
+Definition length_alt (V : Type) (vs : list V) : nat :=
+  length_acc V vs 0.
+
+(*
+Lemma about_length_acc :
+*)
+
+(*
+Lemma about_length_acc_generically :
+*)
+
+(* ********** *)
+
+(* Exercise 03 *)
+
+Fixpoint list_append (V : Type) (v1s v2s : list V) : list V :=
+  match v1s with
+    nil =>
+    v2s
+  | v1 :: v1s' =>
+    v1 :: list_append V v1s' v2s
+  end.
+
+Fixpoint reverse_acc (V : Type) (vs a : list V) : list V :=
+  match vs with
+    nil =>
+    a
+  | v :: vs' =>
+    reverse_acc V vs' (v :: a)
+  end.
+
+Definition reverse_alt (V : Type) (vs : list V) : list V :=
+  reverse_acc V vs nil.
+
+(*
+Lemma about_reverse_acc :
+*)
+
+(*
+Lemma about_reverse_acc_generically :
+*)
+
+(* ********** *)
+
+(* Exercise 04 *)
+
+Fixpoint list_fold_left (V W : Type) (nil_case : W) (cons_case : V -> W -> W) (vs : list V) : W :=
+  match vs with
+    nil =>
+      nil_case
+  | v :: vs' =>
+      list_fold_left V W (cons_case v nil_case) cons_case vs'
+  end.
+
+(*
+Lemma about_list_fold_left :
+*)
+
+(*
+Lemma about_list_fold_left_generically :
+*)
+
+(* ********** *)
+
+(* Exercise 05 *)
+
+Fixpoint fac_acc (n a : nat) : nat :=
+  match n with
+  | O =>
+    a
+  | S n' =>
+    fac_acc n' (S n' * a)
+  end.
+
+Definition fac_alt (n : nat) : nat :=
+  fac_acc n 1.
+
+Lemma fold_unfold_fac_acc_O :
+  forall a : nat,
+    fac_acc 0 a =
+    a.
+Proof.
+  fold_unfold_tactic fac_acc.
+Qed.
+
+Lemma fold_unfold_fac_acc_S :
+  forall n' a : nat,
+    fac_acc (S n') a =
+    fac_acc n' (S n' * a).
+Proof.
+  fold_unfold_tactic fac_acc.
+Qed.
+
+(*
+Lemma about_fac_acc :
+*)
+
+(*
+Lemma about_fac_acc_generically :
+*)
+
+(* ********** *)
+
+(* Exercise 06 *)
+
+Inductive binary_tree : Type :=
+| Leaf : nat -> binary_tree
+| Node : binary_tree -> binary_tree -> binary_tree.
+
+(* ***** *)
+
+Fixpoint weight (t : binary_tree) : nat :=
+  match t with
+  | Leaf n =>
+    n
+  | Node t1 t2 =>
+    weight t1 + weight t2
+  end.
+
+Lemma fold_unfold_weight_Leaf :
+  forall n : nat,
+    weight (Leaf n) = n.
+Proof.
+  fold_unfold_tactic weight.
+Qed.
+
+Lemma fold_unfold_weight_Node :
+  forall t1 t2 : binary_tree,
+    weight (Node t1 t2) = weight t1 + weight t2.
+Proof.
+  fold_unfold_tactic weight.
+Qed.
+
+(* ***** *)
+
+Fixpoint weight_acc (t : binary_tree) (a : nat) : nat :=
+  match t with
+  | Leaf n =>
+    n + a
+  | Node t1 t2 =>
+    weight_acc t1 (weight_acc t2 a)
+  end.
+
+Definition weight_alt (t : binary_tree) : nat :=
+  weight_acc t 0.
+
+Lemma fold_unfold_weight_acc_Leaf :
+  forall n a : nat,
+    weight_acc (Leaf n) a = n + a.
+Proof.
+  fold_unfold_tactic weight_acc.
+Qed.
+
+Lemma fold_unfold_weight_acc_Node :
+  forall (t1 t2 : binary_tree)
+         (a : nat),
+    weight_acc (Node t1 t2) a = weight_acc t1 (weight_acc t2 a).
+Proof.
+  fold_unfold_tactic weight_acc.
+Qed.
+
+(* Nat fold right is a generic version of the non accumulator based iteration function *)
+Definition nat_fold_right (V: Type) (zero_case: V) (succ_case: V -> V) (n : nat) : V :=
+  let fix visit i :=
+    match i with
+      O =>
+        zero_case
+    | S n' =>
+        succ_case (visit n')
+    end
+  in visit n.
+
+(* Nat fold left is a generic version of the accumulator based iteration function *)
+(* This is tail recursive ? *)
+Definition nat_fold_left (V: Type) (zero_case: V) (succ_case: V -> V) (n : nat) : V :=
+  let fix visit i a :=
+    match i with
+      O =>
+        a
+    | S n' =>
+        visit n' (succ_case a)
+    end
+  in visit n zero_case.
+
+Definition nat_fold_left_with_right_1 (V: Type) (zero_case: V) (succ_case: V -> V) (n : nat) : V :=
+  let fix visit i := fun a =>
+    match i with
+      O =>
+        a
+    | S n' =>
+        visit n' (succ_case a)
+    end
+  in visit n zero_case.
+
+Definition nat_fold_left_with_right_2 (V: Type) (zero_case: V) (succ_case: V -> V) (n : nat) : V :=
+  let fix visit i :=
+    match i with
+      O =>
+        fun a => a
+    | S n' =>
+        fun a => visit n' (succ_case a)
+    end
+  in visit n zero_case.
+
+Definition nat_fold_left_with_right_3 (V: Type) (zero_case: V) (succ_case: V -> V) (n : nat) : V :=
+  (nat_fold_right
+    (V -> V)
+    (fun a => a)
+    (fun ih => fun a => ih (succ_case a))
+    n)
+    zero_case.
+
+Definition test_add (candidate : nat -> nat -> nat) :=
+  (Nat.eqb (candidate 0 0) 0) &&
+    (Nat.eqb (candidate 1 0) 1) &&
+    (Nat.eqb (candidate 0 1) 1) &&
+    (Nat.eqb (candidate 1 1) 2) &&
+    (Nat.eqb (candidate 1 2) 3) &&
+    (Nat.eqb (candidate 2 2) 4).
+
+Definition nat_add (a b : nat) :=
+  let fix visit i :=
+    match i with
+    | O => b
+    | S n' => S (visit n')
+    end
+  in visit a.
+
+Definition nat_add_acc (m n : nat) :=
+  let fix visit i a :=
+    match i with
+    | O => m
+    | S n' => visit n' (S a)
+    end
+  in visit m n.
+
+
+Compute test_add Nat.add.
+Compute test_add nat_add.
+Compute test_add nat_add_acc.
+
+Compute test_add (fun a b => nat_fold_left_with_right_3
+                    nat
+                    b
+                    S
+                    a).
+
+Definition nat_parafold_right (V: Type) (zero_case: V) (succ_case: nat -> V -> V) (n : nat) : V :=
+  let fix visit i :=
+    match i with
+      O =>
+        zero_case
+    | S i' =>
+        succ_case i' (visit i')
+    end
+  in visit n.
+
+Definition nat_parafold_right_1 (V: Type) (zero_case: V) (succ_case: nat -> V -> V) (n : nat) : V :=
+  nat_fold_right
+
+
+Definition r_fac (n : nat) : nat :=
+  let fix visit i :=
+    match i with
+      | O => 1
+      | S i' => match i' with
+        | O => 1
+        | S i'' => visit
+
+(* Nat fold left is a generic version of the accumulator based iteration function *)
+Definition nat_fold_left (V: Type) (zero_case: V) (succ_case: V -> V) (n : nat) : V :=
+  let fix visit i a :=
+    match i with
+      O =>
+        a
+    | S n' =>
+        visit n' (succ_case a)
+    end
+  in visit n zero_case.
+(*
+Lemma about_weight_acc :
+*)
+
+(*
+Lemma about_weight_acc_generically :
+*)
+
+(* ********** *)
+
+(* end of week-10_the-abstraction-and-instantiation-of-Eureka-lemmas-about-resetting-the-accumulator.v *)

cs3234/labs/week-11_induction-principles.v

@@ -0,0 +1,494 @@
+(* week-11_induction-principles.v *)
+(* LPP 2024 - CS3236 2023-2024, Sem2 *)
+(* Olivier Danvy <danvy@yale-nus.edu.sg> *)
+(* Version of 05 Apr 2024 *)
+
+(* ********** *)
+
+Ltac fold_unfold_tactic name := intros; unfold name; fold name; reflexivity.
+
+Require Import Arith Bool.
+
+(* ********** *)
+
+(* One goal of this lecture is to revisit the proof that
+   at most one function satisfies the following specification.
+*)
+
+Definition specification_of_the_fibonacci_function (fib : nat -> nat) :=
+  fib 0 = 0
+  /\
+  fib 1 = 1
+  /\
+  forall n'' : nat,
+    fib (S (S n'')) = fib n'' + fib (S n'').
+
+Fixpoint fib (n : nat) : nat :=
+  match n with
+  | 0 =>
+    0
+  | S n' =>
+    match n' with
+    | 0 =>
+      1
+    | S n'' =>
+      fib n'' + fib n'
+    end
+  end.
+
+Lemma fold_unfold_fib_O :
+  fib 0 =
+  0.
+Proof.
+  fold_unfold_tactic fib.
+Qed.
+
+Lemma fold_unfold_fib_S :
+  forall n' : nat,
+    fib (S n') =
+    match n' with
+    | 0 =>
+      1
+    | S n'' =>
+      fib n'' + fib n'
+    end.
+Proof.
+  fold_unfold_tactic fib.
+Qed.
+
+Corollary fold_unfold_fib_1 :
+  fib 1 =
+  1.
+Proof.
+  rewrite -> fold_unfold_fib_S.
+  reflexivity.
+Qed.
+
+Corollary fold_unfold_fib_SS :
+  forall n'' : nat,
+    fib (S (S n'')) =
+    fib n'' + fib (S n'').
+Proof.
+  intro n''.
+  rewrite -> fold_unfold_fib_S.
+  reflexivity.
+Qed.
+
+Proposition fib_satisfies_the_specification_of_fib :
+  specification_of_the_fibonacci_function fib.
+Proof.
+  unfold specification_of_the_fibonacci_function.
+  Check (conj fold_unfold_fib_O (conj fold_unfold_fib_1 fold_unfold_fib_SS)).
+  exact (conj fold_unfold_fib_O (conj fold_unfold_fib_1 fold_unfold_fib_SS)).
+Qed.
+
+(* ********** *)
+
+(* The mathematical induction principle already exists,
+   it is the structural induction principle associated to Peano numbers:
+*)
+
+Check nat_ind.
+
+(* But we can still express it ourselves.
+   We can also prove it using the resident mathematical induction principle,
+   either implicitly or explicitly:
+*)
+
+Lemma nat_ind1 :
+  forall P : nat -> Prop,
+    P 0 ->
+    (forall n : nat, P n -> P (S n)) ->
+    forall n : nat, P n.
+Proof.
+Abort.
+
+(* ********** *)
+
+(* We can also use nat_ind as an ordinary lemma
+   instead of using the induction tactic:
+*)
+
+Fixpoint r_add (i j : nat) : nat :=
+  match i with
+  | O =>
+    j
+  | S i' =>
+    S (r_add i' j)
+  end.
+
+Lemma fold_unfold_r_add_O :
+  forall j : nat,
+    r_add 0 j =
+    j.
+Proof.
+  fold_unfold_tactic r_add.
+Qed.
+
+Lemma fold_unfold_r_add_S :
+  forall i' j : nat,
+    r_add (S i') j =
+    S (r_add i' j).
+Proof.
+  fold_unfold_tactic r_add.
+Qed.
+
+Proposition r_add_0_r :
+  forall i : nat,
+    r_add i 0 = i.
+Proof.
+  (* First, a routine induction: *)
+  intro i.
+  induction i as [ | i' IHi'].
+  - exact (fold_unfold_r_add_O 0).
+  - rewrite -> fold_unfold_r_add_S.
+    Check f_equal.
+    Check (f_equal S). (* : forall x y : nat, x = y -> S x = S y *)
+    Check (f_equal S IHi').
+    exact (f_equal S IHi').
+
+  Restart.
+
+  (* And now for using nat_ind: *)
+  Check nat_ind.
+Abort.
+
+(* ********** *)
+
+Fixpoint fibfib (n : nat) : nat * nat :=
+  match n with
+  | O =>
+    (0, 1)
+  | S n' =>
+    let (fib_n', fib_succ_n') := fibfib n'
+    in (fib_succ_n', fib_n' + fib_succ_n')
+  end.
+
+Definition fib_lin (n : nat) : nat :=
+  let (fib_n, _) := fibfib n
+  in fib_n.
+
+Lemma fold_unfold_fibfib_O :
+  fibfib 0 =
+  (0, 1).
+Proof.
+  fold_unfold_tactic fibfib.
+Qed.
+
+Lemma fold_unfold_fibfib_S :
+  forall n' : nat,
+    fibfib (S n') =
+    let (fib_n', fib_succ_n') := fibfib n'
+    in (fib_succ_n', fib_n' + fib_succ_n').
+Proof.
+  fold_unfold_tactic fibfib.
+Qed.
+
+Lemma about_fibfib :
+  forall fib : nat -> nat,
+    specification_of_the_fibonacci_function fib ->
+    forall n : nat,
+      fibfib n = (fib n, fib (S n)).
+Proof.
+  unfold specification_of_the_fibonacci_function.
+  intros fib [S_fib_O [S_fib_1 S_fib_SS]] n.
+  induction n as [ | [ | n''] IH].
+  - rewrite -> fold_unfold_fibfib_O.
+    rewrite -> S_fib_O.
+    rewrite -> S_fib_1.
+    reflexivity.
+  - rewrite -> fold_unfold_fibfib_S.
+    rewrite -> fold_unfold_fibfib_O.
+    rewrite -> S_fib_1.
+    rewrite -> S_fib_SS.
+    rewrite -> S_fib_O.
+    rewrite -> S_fib_1.
+    reflexivity.
+  - rewrite -> fold_unfold_fibfib_S.
+    rewrite -> IH.
+    rewrite <- (S_fib_SS (S n'')).
+    reflexivity.
+Qed.
+
+Proposition fib_lin_satisfies_the_specification_of_fib :
+  specification_of_the_fibonacci_function fib_lin.
+Proof.
+  unfold specification_of_the_fibonacci_function, fib_lin.
+  split.
+  - rewrite -> fold_unfold_fibfib_O.
+    reflexivity.
+  - split.
+    + rewrite -> fold_unfold_fibfib_S.
+      rewrite -> fold_unfold_fibfib_O.
+      reflexivity.
+    + intro i.
+      Check (about_fibfib fib fib_satisfies_the_specification_of_fib (S (S i))).
+      rewrite -> (about_fibfib fib fib_satisfies_the_specification_of_fib (S (S i))).
+      rewrite -> (about_fibfib fib fib_satisfies_the_specification_of_fib i).
+      rewrite -> (about_fibfib fib fib_satisfies_the_specification_of_fib (S i)).
+      exact (fold_unfold_fib_SS i).
+Qed.
+
+(* ********** *)
+
+(* We can also express a mathematical induction principle
+   with two base cases and two induction hypotheses
+   that befits the structure of the Fibonacci function:
+*)
+
+Lemma nat_ind2 :
+  forall P : nat -> Prop,
+    P 0 ->
+    P 1 ->
+    (forall n : nat, P n -> P (S n) -> P (S (S n))) ->
+    forall n : nat, P n.
+Proof.
+  intros P H_P0 H_P1 H_PSS n.
+  induction n as [ | [ | n''] IHn'].
+Abort.
+
+(* Thus equipped, the following theorem is proved pretty directly: *)
+
+Theorem there_is_at_most_one_fibonacci_function :
+  forall fib1 fib2 : nat -> nat,
+    specification_of_the_fibonacci_function fib1 ->
+    specification_of_the_fibonacci_function fib2 ->
+    forall n : nat,
+      fib1 n = fib2 n.
+Proof.
+  intros fib1 fib2.
+  unfold specification_of_the_fibonacci_function.
+  intros [H_fib1_0 [H_fib1_1 H_fib1_SS]]
+         [H_fib2_0 [H_fib2_1 H_fib2_SS]]
+         n.
+  induction n as [ | | n'' IHn'' IHSn''] using nat_ind2.
+Abort.
+
+(* ***** *)
+
+Fixpoint evenp1 (n : nat) : bool :=
+  match n with
+  | 0 =>
+    true
+  | S n' =>
+    negb (evenp1 n')
+  end.
+
+Lemma fold_unfold_evenp1_O :
+  evenp1 0 =
+  true.
+Proof.
+  fold_unfold_tactic evenp1.
+Qed.
+
+Lemma fold_unfold_evenp1_S :
+  forall n' : nat,
+    evenp1 (S n') =
+    negb (evenp1 n').
+Proof.
+  fold_unfold_tactic evenp1.
+Qed.
+
+(* ***** *)
+
+(* The evenness predicate is often programmed tail-recursively
+   and with no accumulator, by peeling two layers of S at a time.
+   Its equivalence with evenp1 is messy to prove by mathematical induction
+   but effortless using nat_ind2:
+*)
+
+Fixpoint evenp2 (n : nat) : bool :=
+  match n with
+  | 0 =>
+    true
+  | S n' =>
+    match n' with
+    | 0 =>
+      false
+    | S n'' =>
+      evenp2 n''
+    end
+  end.
+
+Lemma fold_unfold_evenp2_O :
+  evenp2 0 =
+  true.
+Proof.
+  fold_unfold_tactic evenp2.
+Qed.
+
+Lemma fold_unfold_evenp2_S :
+  forall n' : nat,
+    evenp2 (S n') =
+    match n' with
+    | 0 =>
+      false
+    | S n'' =>
+      evenp2 n''
+    end.
+Proof.
+  fold_unfold_tactic evenp2.
+Qed.
+
+Corollary fold_unfold_evenp2_1 :
+  evenp2 1 =
+  false.
+Proof.
+  rewrite -> fold_unfold_evenp2_S.
+  reflexivity.
+Qed.
+
+Corollary fold_unfold_evenp2_SS :
+  forall n'' : nat,
+    evenp2 (S (S n'')) =
+    evenp2 n''.
+Proof.
+  intro n''.
+  rewrite -> fold_unfold_evenp2_S.
+  reflexivity.
+Qed.
+
+Theorem evenp1_and_evenp2_are_functionally_equal :
+  forall n : nat,
+    evenp1 n = evenp2 n.
+Proof.
+  intro n.
+  induction n as [ | n' IHn'].
+Abort.
+
+(* ***** *)
+
+Lemma two_times_S :
+  forall n : nat,
+    S (S (2 * n)) = 2 * S n.
+Proof.
+Admitted.
+
+Theorem soundness_and_completeness_of_evenp_using_nat_ind2 :
+  forall n : nat,
+    evenp2 n = true <-> exists m : nat, n = 2 * m.
+Proof.
+  intro n.
+  induction n as [ | | n' [IHn'_sound IHn'_complete] [IHSn'_sound IHSn'_complete]] using nat_ind2.
+Abort.
+
+(* ***** *)
+
+(* For another example, we can prove the mathematical induction principle using nat_ind2: *)
+
+Lemma nat_ind1' :
+  forall P : nat -> Prop,
+    P 0 ->
+    (forall n : nat, P n -> P (S n)) ->
+    forall n : nat, P n.
+Proof.
+  intros P H_P0 H_PS n.
+  induction n as [ | | n' IHn'] using nat_ind2.
+  - exact H_P0.
+  - Check (H_PS 0 H_P0).
+    exact (H_PS 0 H_P0).
+  - Check (H_PS (S n') IHn).
+    exact (H_PS (S n') IHn).
+Qed.
+
+(* We can also generalize nat_ind2 to an induction principle
+   with three base cases and three induction hypotheses: *)
+
+Lemma nat_ind3 :
+  forall P : nat -> Prop,
+    P 0 ->
+    P 1 ->
+    P 2 ->
+    (forall n : nat, P n -> P (S n) -> P (S (S n)) -> P (S (S (S n)))) ->
+    forall n : nat, P n.
+Proof.
+Abort.
+
+(* ***** *)
+
+Fixpoint ternaryp (n : nat) : bool :=
+  match n with
+  | 0 =>
+    true
+  | 1 =>
+    false
+  | 2 =>
+    false
+  | S (S (S n')) =>
+    ternaryp n'
+  end.
+
+Lemma fold_unfold_ternaryp_O :
+  ternaryp 0 =
+  true.
+Proof.
+  fold_unfold_tactic ternaryp.
+Qed.
+
+Lemma fold_unfold_ternaryp_1 :
+  ternaryp 1 =
+  false.
+Proof.
+  fold_unfold_tactic ternaryp.
+Qed.
+
+Lemma fold_unfold_ternaryp_2 :
+  ternaryp 2 =
+  false.
+Proof.
+  fold_unfold_tactic ternaryp.
+Qed.
+
+Lemma fold_unfold_ternaryp_SSS :
+  forall n' : nat,
+    ternaryp (S (S (S n'))) =
+    ternaryp n'.
+Proof.
+  fold_unfold_tactic ternaryp.
+Qed.
+
+Theorem soundness_and_completeness_of_ternaryp_using_nat_ind3 :
+  forall n : nat,
+    ternaryp n = true <-> exists m : nat, n = 3 * m.
+Proof.
+Abort.
+
+(* ********** *)
+
+Lemma three_times_S :
+  forall n : nat,
+    S (S (S (3 * n))) = 3 * S n.
+Proof.
+Admitted.
+
+Property threes_and_fives :
+  forall n : nat,
+  exists a b : nat,
+    8 + n = 3 * a + 5 * b.
+Proof.
+Abort.
+
+(* ********** *)
+
+Lemma four_times_S :
+  forall n : nat,
+    S (S (S (S (4 * n)))) = 4 * S n.
+Proof.
+Admitted.
+
+Lemma five_times_S :
+  forall n : nat,
+    S (S (S (S (S (5 * n))))) = 5 * S n.
+Proof.
+Admitted.
+
+Property fours_and_fives :
+  forall n : nat,
+  exists a b : nat,
+    12 + n = 4 * a + 5 * b.
+Proof.
+Abort.
+
+(* ********** *)
+
+(* end of week-10_induction-principles.v *)

cs3234/labs/week-13_a-continuation-based-interpreter.v

@@ -0,0 +1,193 @@
+(* week-13_a-continuation-based-interpreter.v *)
+(* LPP 2024 - CS3234 2023-2024, Sem2 *)
+(* Olivier Danvy <danvy@yale-nus.edu.sg> *)
+(* Version of 12 Apr 2024 *)
+
+(* ********** *)
+
+Ltac fold_unfold_tactic name := intros; unfold name; fold name; reflexivity.
+  
+Require Import Arith Bool List String Ascii.
+
+(* ***** *)
+
+Check (1 =? 2).
+Check Nat.eqb.
+Check (Nat.eqb 1 2).
+
+Check (1 <=? 2).
+Check Nat.leb.
+Check (Nat.leb 1 2).
+
+Check (1 <? 2).
+Check Nat.ltb.
+Check (Nat.ltb 1 2).
+
+(* caution: only use natural numbers up to 5000 -- caveat emptor *)
+Definition string_of_nat (q0 : nat) : string :=
+  let s0 := String (ascii_of_nat (48 + (q0 mod 10))) EmptyString
+  in if q0 <? 10
+     then s0
+     else let q1 := q0 / 10
+          in let s1 := String (ascii_of_nat (48 + (q1 mod 10))) s0
+             in if q1 <? 10
+                then s1
+                else let q2 := q1 / 10
+                     in let s2 := String (ascii_of_nat (48 + (q2 mod 10))) s1
+                        in if q2 <? 10
+                           then s2
+                           else let q3 := q2 / 10
+                                in let s2 := String (ascii_of_nat (48 + (q3 mod 10))) s2
+                        in if q3 <? 10
+                           then s2
+                           else "00000".
+
+(* ********** *)
+
+(* Arithmetic expressions: *)
+
+Inductive arithmetic_expression : Type :=
+  Literal : nat -> arithmetic_expression
+| Plus : arithmetic_expression -> arithmetic_expression -> arithmetic_expression
+| Minus : arithmetic_expression -> arithmetic_expression -> arithmetic_expression.
+
+(* Source programs: *)
+
+Inductive source_program : Type :=
+  Source_program : arithmetic_expression -> source_program.
+
+(* ********** *)
+
+(* Semantics: *)
+
+Inductive expressible_value : Type :=
+  Expressible_nat : nat -> expressible_value
+| Expressible_msg : string -> expressible_value.
+
+(* ********** *)
+
+Definition specification_of_evaluate (evaluate : arithmetic_expression -> expressible_value) :=
+  (forall n : nat,
+     evaluate (Literal n) = Expressible_nat n)
+  /\
+  ((forall (ae1 ae2 : arithmetic_expression)
+           (s1 : string),
+       evaluate ae1 = Expressible_msg s1 ->
+       evaluate (Plus ae1 ae2) = Expressible_msg s1)
+   /\
+   (forall (ae1 ae2 : arithmetic_expression)
+           (n1 : nat)
+           (s2 : string),
+       evaluate ae1 = Expressible_nat n1 ->
+       evaluate ae2 = Expressible_msg s2 ->
+       evaluate (Plus ae1 ae2) = Expressible_msg s2)
+   /\
+   (forall (ae1 ae2 : arithmetic_expression)
+           (n1 n2 : nat),
+       evaluate ae1 = Expressible_nat n1 ->
+       evaluate ae2 = Expressible_nat n2 ->
+       evaluate (Plus ae1 ae2) = Expressible_nat (n1 + n2)))
+  /\
+  ((forall (ae1 ae2 : arithmetic_expression)
+           (s1 : string),
+       evaluate ae1 = Expressible_msg s1 ->
+       evaluate (Minus ae1 ae2) = Expressible_msg s1)
+   /\
+   (forall (ae1 ae2 : arithmetic_expression)
+           (n1 : nat)
+           (s2 : string),
+       evaluate ae1 = Expressible_nat n1 ->
+       evaluate ae2 = Expressible_msg s2 ->
+       evaluate (Minus ae1 ae2) = Expressible_msg s2)
+   /\
+   (forall (ae1 ae2 : arithmetic_expression)
+           (n1 n2 : nat),
+       evaluate ae1 = Expressible_nat n1 ->
+       evaluate ae2 = Expressible_nat n2 ->
+       n1 <? n2 = true ->
+       evaluate (Minus ae1 ae2) = Expressible_msg (String.append "numerical underflow: -" (string_of_nat (n2 - n1))))
+   /\
+   (forall (ae1 ae2 : arithmetic_expression)
+           (n1 n2 : nat),
+       evaluate ae1 = Expressible_nat n1 ->
+       evaluate ae2 = Expressible_nat n2 ->
+       n1 <? n2 = false ->
+       evaluate (Minus ae1 ae2) = Expressible_nat (n1 - n2))).
+
+Definition specification_of_interpret (interpret : source_program -> expressible_value) :=
+  forall evaluate : arithmetic_expression -> expressible_value,
+    specification_of_evaluate evaluate ->
+    forall ae : arithmetic_expression,
+      interpret (Source_program ae) = evaluate ae.
+
+(* ********** *)
+
+(* An evaluation function in delimited continuation-passing style: *)
+
+Fixpoint evaluate_cb (ae : arithmetic_expression) (k : nat -> expressible_value) : expressible_value :=
+  Expressible_msg "not implemented yet".
+
+(*
+Lemma fold_unfold_evaluate_cb_Literal :
+  forall (n : nat)
+         (k : nat -> expressible_value),
+    evaluate_cb (Literal n) k =
+    ...
+Proof.
+  fold_unfold_tactic evaluate_cb.
+Qed.
+
+Lemma fold_unfold_evaluate_cb_Plus :
+  forall (ae1 ae2 : arithmetic_expression)
+         (k : nat -> expressible_value),
+    evaluate_cb (Plus ae1 ae2) k =
+    ...
+Proof.
+  fold_unfold_tactic evaluate_cb.
+Qed.
+
+Lemma fold_unfold_evaluate_cb_Minus :
+  forall (ae1 ae2 : arithmetic_expression)
+         (k : nat -> expressible_value),
+    evaluate_cb (Minus ae1 ae2) k =
+    ...
+Proof.
+  fold_unfold_tactic evaluate_cb.
+Qed.
+*)
+
+(* ***** *)
+
+Definition interpret (sp : source_program) : expressible_value :=
+  Expressible_msg "not implemented yet".
+
+(* ***** *)
+
+Lemma about_evaluate_cb :
+  forall evaluate : arithmetic_expression -> expressible_value,
+    specification_of_evaluate evaluate ->
+    forall ae : arithmetic_expression,
+      (exists n : nat,
+          evaluate ae = Expressible_nat n
+          /\
+          forall k : nat -> expressible_value,
+            evaluate_cb ae k = k n)
+      \/
+      (exists s : string,
+          evaluate ae = Expressible_msg s
+          /\
+          forall k : nat -> expressible_value,
+            evaluate_cb ae k = Expressible_msg s).
+Proof.
+Abort.
+
+(* ***** *)
+
+Theorem interpret_satisfies_specification_of_interpret :
+  specification_of_interpret interpret.
+Proof.
+Abort.
+
+(* ********** *)
+
+(* end of week-13_a-continuation-based-interpreter.v *)

ma1522/ch_04.typ

@@ -0,0 +1,146 @@
+#import "@preview/ctheorems:1.1.2": *
+#show: thmrules
+#let theorem = thmbox("theorem", "Theorem", fill: rgb("#eeffee"), padding: (top: 0em, bottom: 0em)).with(numbering: none)
+#let remark = thmbox("remark", "Remark", padding: (top: 0em, bottom: 0em)).with(numbering: none)
+#let definition = thmbox("definition", "Definition", inset: (x: 1.2em, top: 1em), padding: (top: 0em, bottom: 0em)).with(numbering: none)
+#let example = thmplain("example", "Example", padding: (top: 0em, bottom: 0em)).with(numbering: none)
+#let proof = thmproof("proof", "Proof", padding: (top: 0em, bottom: 0em))
+
+
+= Vector Spaces and Associated Matrices
+== Row Space and Column Space
+- Let $A = mat(a_11, dots, a_(1n);dots.v, dots.v, dots.v; a_(m 1), dots, a_(m n))$
+- $r_i = (a_(i 1) dots a_(i n))$
+- Row Space of $A$ is the vector space spanned by rows of $A$ : $"span"{r_1, dots, r_m}$
+- $c_j = vec(a_(1j),dots.v,a_(m j))$
+- Column space of $A$ is vector space spanned by columns of $A$ : $"span"{c_1, dots, c_n}$
+
+#example[Let $A = mat(1,2,3;4,5,6)$.
+- $r_1 = (1,2,3), r_2 = (4,5,6)$.
+- $c_1 = (1,4)^T, c_2 = (2,5)^T, c_3 = (3,6)^T$
+]
+#example[To find the basis of $A$
+- Row Space of $A$
+  - Gaussian elimination on the row-vectors of $A$ and the non-zero rows of $R$ are basis
+- Col space of $A$
+  - Gaussian elimination on row vectors of $A$ and the pivot columns of $A$ are the basis
+]
+
+=== Row Equivalence
+Let $A$ and $B$ be matrices of the same size. $A$ and $B$ are row equivalent if one can be obtained from another by ERO
+
+
+#theorem[If $A$ and $B$ are row equivalent, then $A$ and $B$ have same row spaces]
+
+#remark[Let $R$ be REF of $A$
+- Row space of $A$ = row space of $R$
+- Nonzero rows of $R$ are linearly independent
+  - Nonzero rows of $R$ form basis for row space of $A$
+  - No of nonzero rows $R$ = dim of row space of $A$
+]
+
+=== Row Operations to Columns
+- Let $A$ and $B$ be Row Equivalent Matrices : $A -> A_1 -> dots -> A_(k-1) -> B$
+- Exists $E_1, dots, E_k$ s.t. $E_k dots E_1 A = B$
+- $M = E_k dots E_1$, $M$ is invertible, $M A = B, A = M^(-1) B$
+
+#theorem[Row Equivalence Preserves the linear relations on the columns
+- Suppose $A = mat(a_1, dots, a_n)$ and $B = mat(b_1, dots, b_n)$
+- $a_j = c_1 a_1 + dots + c_n a_n arrow.l.r.double b_j = c_1 b_1 + dots + c_n b_n$
+]
+#remark[Let $R$ be REF of $A$
+- Pivot columns of $R$ form basis for column space of $R$
+- Columns of $A$ which correspond to pivot columns of $R$ form a basis for column space of $A$
+- No of pivot columns of $R$ is the dim of column space of $A$
+]
+
+#example[Find basis for a vector space V
+
+Let $V = "span"{v_1, v_2, v_3, v_4, v_5, v_6}, - v_1 = (1,2,2,1), v_2 = (3,6,6,3), "etc"$
+1. Method 1 (Row Form)
+  - View each $v_i$ as a row vector
+    - $mat(1, 2, 2, 1; 3, 6, 6, 3; 4,9,9,5;-2,-1,-1,1;5,8,9,4;4,2,7,3) attach(arrow.r.long, t: "Gaussian Elimination") mat(1,2,2,1;0,1,1,1;0,0,1,1;0,0,0,0;0,0,0,0;0,0,0,0)$
+  - $V$ has basis${(1,2,2,1), (0,1,1,1), (0,0,1,1)}$
+  - $dim(V) = 3$
+2. Method 2 (Column Form)
+  - View each $v_i$ as a column vector 
+    - $mat(1,3,4,-2,5,4;2,6,9,-1,8,2;2,6,9,-1,9,7;1,3,5,1,4,3) attach(arrow.r.long, t: "Gaussian Elimination") mat(1,3,4,-2,5,4;0,0,1,3,-2,-6;0,0,0,0,1,5;0,0,0,0,0,0)$
+  - Using Pivot columns (1,3,5), pick the corresponding vectors, $(v_1, v_3, v_5)$
+  - V has basis${(1,2,2,1), (4,9,9,5), (4,2,7,3)}$
+  - $dim(V) = 3$
+]
+
+#remark[Finding Basis TLDR
++ Method 1: View each $v_1, dots, v_k$ as a row vector
+  - Find row echelon form $R$ of $vec(v_1,dots.v,v_k)$
+  - Nonzero rows of $R$ form basis of $V$
++ Method 2: View each $v_1, dots, v_k$ as a column vector
+  - Find row echelon form $R$ of $mat(v_1,dots,v_k)$
+  - Find pivot columns of $R$
+  - Corresponding columns $v_j$ form basis for $V$
+]
+
+#example[Extend $S$ to a basis for $RR^n$
+- Find REF of $S$ as row vectors
+- Insert the $e_i$ vectors for each $i$ non-pivot column
+]
+
+#theorem[Consistency
+
+Let $A$ be a $m times n$ matrix
+- Column space of $A$ is ${A v | v in RR^n}$
+- Linear system $A x = b$ is consistent
+  - #sym.arrow.l.r.double $b$ lies in the column space of $A$
+]
+
+#theorem[Rank
+
+- Let $A$ be a matrix, then $dim("row space of " A) = dim("col space of " A)$
+- This is the rank of $A$, denoted by $"rank(A)"$
+]
+
+#remark[
+Let $A$ be an $m times n$ matrix
+- $"rank"(A) = "rank"(A^T)$
+- $"rank"(A) = 0 arrow.l.r.double A = 0$
+  - $"rank"(A) <= min{m,n}$
+  - Full rank if $"rank"(A) = min{m,n}$
+- Square Matrix $A$ is full rank #sym.arrow.l.r.double $A$ is invertible.
+]
+
+#remark[Rank and Consistency of Linear System
+
+$A x = b$ be linear system
+- $A x = b$ is consistent
+  - $arrow.l.r.double b in "span"{c_1,dots,c_n}$
+  - $arrow.l.r.double "span"{c_1,dots,c_n} = "span"{c_1,dots,c_n,b$
+  - $arrow.l.r.double dim("span"{c_1,dots,c_n}) = dim("span"{c_1,dots,c_n,b})$
+  - $arrow.l.r.double "rank"(A) = "rank"(A|b)$
+- $"rank"(A) <= "rank"(A | b) <= "rank"(A) + 1$
+]
+
+If $A B x = b$ has a solution, then $A x = b$ also has a solution
+
+
+#theorem[Let $A = m times n$ matrix and $B = n times p$
+
+- Column space of $A B subset.eq $ column space of $A$
+- Row space of $A B subset.eq $ row space of $B$
+- $"rank"(A B) <= min{"rank"(A), "rank"(B)}$
+]
+
+#definition[Nullspace and Nullity
+
+- Nullspace of $A$ is the solution space of $A x = 0$
+  - $v in RR^n | A v = 0$
+- Vectors in nullspace are viewed as column vectors
+
+- Let $R$ be a REF of $A$
+  - $A x = 0 arrow.l.r.double R x = 0$
+  - $"nullity"(A) = "nullity"(R)$
+]
+
+#theorem[Dimension Theorem
+Let $A$ be a $m times n$ matrix
+- $"rank"(A) + "nullity"(B) = n$ ($n$ is the number of columns)
+]

ma1522/ch_05.typ

@@ -0,0 +1,12 @@
+#import "@preview/ctheorems:1.1.2": *
+#show: thmrules
+#let theorem = thmbox("theorem", "Theorem", fill: rgb("#eeffee"), padding: (top: 0em, bottom: 0em)).with(numbering: none)
+#let remark = thmbox("remark", "Remark", padding: (top: 0em, bottom: 0em)).with(numbering: none)
+#let definition = thmbox("definition", "Definition", inset: (x: 1.2em, top: 1em), padding: (top: 0em, bottom: 0em)).with(numbering: none)
+#let example = thmplain("example", "Example", padding: (top: 0em, bottom: 0em)).with(numbering: none)
+#let proof = thmproof("proof", "Proof", padding: (top: 0em, bottom: 0em))
+
+#definition[Dot Product. Let $u, v = (u_1, u_2), (v_1, v_2) in RR^2$
+
+$u dot v = u_1 v_1 + u_2 v_2$
+]