Merge branch 'main' of github.com:IUDataStructuresCourse/course-web-page-spring-2025

Author: HalflingHelper

ListSearch.md

@@ -1,7 +1,7 @@
 # Lab: List Search
 
 Prove the following theorem about the variant of linear `search` that
-you implemented in lab last week.
+you implemented in lab.
 
 ```
 theorem search_correct: all y: Nat. all xs: List<Nat>.

QuickReverse.md

@@ -11,3 +11,8 @@ proof
 end
 ```
 
+The file you submit to the autograder must be named `QuickRevCorrect.pf`
+and it should include the above theorem and the definition of `quick_rev`
+and any helper functions that you created to use in `quick_rev`.
+Your `QuickRevCorrect.pf` should only import files from the Deduce
+`lib` directory.

index.md

@@ -97,16 +97,17 @@ Jan. 23 or 24 |                                                     |
 Jan. 28 | [Programming in Deduce with Linked Lists](./lectures/deduce-programming.md) | [Programming in Deduce](https://jsiek.github.io/deduce/pages/deduce-programming.html) | Project FloodIt! due | [code](https://autograder.luddy.indiana.edu/web/project/1509)
 Jan. 30 | [Writing Proofs in Deduce](./lectures/deduce-intro-proof.md)                                | [Proofs in Deduce](https://jsiek.github.io/deduce/pages/deduce-proofs.html)
 Jan. 30 or 31 |                                                     |              | [Lab: Linked Lists in Deduce](./LabDeduceProg) | [code](https://autograder.luddy.indiana.edu/web/project/1614)
-Feb. 4  | [Proof by Induction](./lectures/InductionOnLists.md) | | Lab Linked Lists in Deduce due
-Feb. 6  | [Discovering and Generalizing Lemmas](./lectures/RevRev.md)                       |              | [Proof Exercises](./ProofExercises.md) | [submit](https://autograder.luddy.indiana.edu/web/project/1623)
-Feb. 6 or 7 |                                                       |              | [Lab: List Search](./ListSearch.md)
-Feb. 11 | Insertion Sort                                            | Ch.7 Sec. 2  | | Lab List Search due
-Feb. 13 | Merge Sort, Quick Sort                                    | Ch.7 Sec. 6,7 | [Proof: Quick Reverse Correct](./QuickReverse.md)
-Feb. 13 or 14 |                                                     |              | [Lab: Insertion Sort](./LabInsertionSort.md)
-Feb. 18 | [Binary Trees](./lectures/binary-trees.md)                | Ch. 4 Sec. 1-2 | Lab Insertion Sort due
+Feb. 4  | [Writing Proofs and Induction](./lectures/deduce-more-proof.md) | | Lab Linked Lists in Deduce due
+Feb. 6  | [Logical And, Or, Not, and Sets](./lectures/LogicAndSets.md)                        |              |   | 
+Feb. 6 or 7 |                                                       |              | [Lab: Proof Exercises](./ProofExercises.md) 
+Feb. 11 | [Discovering and Generalizing Lemmas](./lectures/RevRev.md)                                            |  | Lab Proof Exercises due | [submit](https://autograder.luddy.indiana.edu/web/project/1623)
+Feb. 13 | [Insertion Sort, Merge Sort, Quick Sort](./lectures/sorting.md)                    | Ch.7 Sec. 2,6,7 | 
+Feb. 13 or 14 |                                                     |              | [Lab: Quick Reverse Correct](./QuickReverse.md)
+Feb. 14 |                                                           |              | 
+Feb. 18 | [Binary Trees](./lectures/binary-trees.md)                | Ch. 4 Sec. 1-2 | [Lab: Quick Reverse Correct](./QuickReverse.md) due | [submit](https://autograder.luddy.indiana.edu/web/project/1632)
 Feb. 20 | [Binary Search Trees](./lectures/binary-search-trees.md)  | Ch. 4 Sec. 3
-Feb. 20 or 21 |                                                     |              | [Lab: Binary Tree Search](./LabBinarySearchTree.md)
-Feb. 25 | [Balanced Search Trees (AVL)](./lectures/balanced-search-trees.md) | Ch. 4 Sec. 4 | Lab Binary Tree Search due
+Feb. 20 or 21 |                                                     |              |  [Lab: List Search](./ListSearch.md)
+Feb. 25 | [Balanced Search Trees (AVL)](./lectures/balanced-search-trees.md) | Ch. 4 Sec. 4 | Lab List Search due
 Feb. 27 | [More AVL](./lectures/more-avl-trees.md)
 Feb. 27 or 28 | | | Lab: work on [Project 2: Segment Intersection](./SegmentIntersection.md) | [code](https://autograder.luddy.indiana.edu/web/project/1530), [test](https://autograder.luddy.indiana.edu/web/project/1529)
 March 4 | [Recipes for Time Analysis and Testing](./lectures/analysis-and-testing-recipes.md)

lectures/Feb11.pf

@@ -0,0 +1,44 @@
+import Nat
+import List
+
+
+lemma reverse_helper: <U> all x:U, ls:List<U>, xs:List<U>.
+  reverse(ls ++ xs) = reverse(xs) ++ reverse(ls)
+proof
+  arbitrary U:type
+  arbitrary x:U
+  induction List<U>
+  case [] {
+    arbitrary xs:List<U>
+    suffices reverse(xs) = reverse(xs) ++ [] by evaluate
+    rewrite append_empty<U>
+  }
+  case node(y, ls') assume IH {
+    arbitrary xs:List<U>
+    equations
+          reverse(node(y, ls') ++ xs)
+        = reverse(node(y, ls' ++ xs)) by definition operator++
+    ... = reverse(ls' ++ xs) ++ [y]   by definition reverse
+    ... = (reverse(xs) ++ reverse(ls')) ++ [y] by rewrite IH
+    ... = reverse(xs) ++ (reverse(ls') ++ [y]) by rewrite append_assoc<U>
+    ... = reverse(xs) ++ #reverse(node(y, ls'))# by definition reverse
+  }
+end
+
+theorem reverse_reverse: all U :type. all ls :List<U>.
+  reverse(reverse(ls)) = ls
+proof
+  arbitrary U:type
+  induction List<U>
+  case [] {
+    definition reverse
+  }
+  case node(x, ls') assume IH: reverse(reverse(ls')) = ls' {
+    suffices reverse(reverse(ls') ++ [x]) = node(x, ls') by evaluate
+    equations
+          reverse(reverse(ls') ++ [x])
+        = reverse([x]) ++ reverse(reverse(ls'))   by reverse_helper<U>
+    ... = reverse([x]) ++ ls'   by rewrite IH
+    ... = node(x, ls')  by evaluate
+  }
+end

lectures/Feb4.pf

@@ -0,0 +1,70 @@
+import Nat
+import List
+import Pair
+import Jan28
+import Jan30
+
+theorem len_42: 1 = len(Node(42, Empty)) and len(Node(25, Empty)) = 1
+proof
+  rewrite len_one
+  /*have eq1: len(Node(42, Empty)) = 1  by len_one[42]
+  have eq3: len(Node(25, Empty)) = 1  by len_one[25]
+  rewrite eq1 | eq3 //suffices len(Node(25, Empty)) = 1 by rewrite eq1
+  */
+  //symmetric len_one[42]
+  //have eq: len(Node(42, Empty)) = 1  by len_one[42]
+  //rewrite eq
+  // goal: 1 = len(Node(42, Empty))
+  // rewrite: 1 = 1
+  // true
+end
+
+theorem algebra_example: all x:Nat. (1 + x) * x = x * x + x
+proof
+  arbitrary x:Nat
+  equations
+        (1 + x) * x
+      = 1 * x + x * x   by dist_mult_add_right[1,x,x]
+  ... = x + x * x       by rewrite one_mult[x]
+  ... = x * x + x       by add_commute[x,x*x]
+end
+
+theorem modus_ponens_example: all x:Nat. max(x, 1 + x) = 1 + x
+proof
+  arbitrary x:Nat
+  have lt: x ≤ 1 + x by less_equal_add_left
+  apply max_equal_greater_right[x, 1+x] to lt
+end
+
+theorem assume_example: all xs:NatList. if len(xs) = 0 then xs = Empty
+proof
+  arbitrary xs:NatList
+  assume lenz: len(xs) = 0
+  // Goal: xs = Empty
+  switch xs {
+    case Empty {
+      .  // Goal: Empty = Empty
+    }
+    case Node(x, xs2) assume eq {
+      have eq2: len(Node(x,xs2)) = 0 by rewrite eq in lenz
+      have eq3: 1 + len(xs2) = 0 by definition len in eq2
+      have eq4: suc(0 + len(xs2)) = 0 by definition operator+ in eq3
+      conclude false by eq4
+    }
+  }
+end
+
+theorem list_append_empty: <U> all xs :List<U>.
+  xs ++ [] = xs
+proof
+  arbitrary U:type
+  induction List<U>
+  case empty {
+    definition operator++
+  }
+  case node(T1, L2) assume IH: L2 ++ [] = L2 {
+    suffices node(T1, L2 ++ @[]<U>) = node(T1, L2)
+      by definition operator++
+    rewrite IH
+  }
+end

lectures/Feb6.pf

@@ -0,0 +1,115 @@
+import Nat
+import List
+import Base
+
+define isEven : fn Nat -> bool = fun n { some m:Nat. n = 2 * m }
+define isOdd : fn Nat -> bool = fun n { some m:Nat. n = suc (2 * m) }
+
+theorem addition_of_evens_example:
+  all x:Nat, y:Nat.
+  if isEven(x) and isEven(y) then isEven(x + y)
+proof
+  arbitrary x:Nat, y:Nat
+  assume even_xy: isEven(x) and isEven(y)
+	suffices some m:Nat. x + y = 2 * m
+		by definition {isEven}
+  have ex: some m:Nat. x = 2 * m by definition isEven in even_xy
+  have ey: some m:Nat. y = 2 * m by definition isEven in even_xy
+  obtain a where x_2a: x = 2*a from ex
+  obtain b where y_2b: y = 2*b from ey
+  choose (a + b)
+  suffices 2 * a + 2 * b = 2 * (a + b) by rewrite x_2a | y_2b
+  rewrite dist_mult_add
+end
+
+
+
+theorem exercise_demorgan: all A:bool, B:bool.
+  if (not A) or (not B) then not (A and B)
+proof
+  arbitrary A:bool, B:bool
+  assume premise: (not A) or (not B)
+  cases premise
+  case nA: not A {
+    //rewrite (apply eq_false to nA)
+    assume ab: A and B
+    have: A by ab
+    conclude false by apply nA to recall A
+  }
+  case nB: not B {
+    assume ab: A and B
+    conclude false by apply nB to ab
+  }
+end
+
+
+
+/*
+theorem add_to_zero_is_zero: all n:Nat, m:Nat.
+  if n + m = 0
+  then n = 0 and m = 0
+proof
+  arbitrary n:Nat, m:Nat
+  switch n {
+    case 0 {
+      assume premise: 0 + m = 0
+      have f1: 0 + 0 = 0 by definition operator+
+      have f2: m = 0 by definition operator+ in premise
+      f1, f2
+    }
+    case suc(n') {
+      assume premise: suc(n') + m = 0
+      sorry
+    }
+  }
+  
+end
+
+theorem example: all T:type, xs:List<T>, ys:List<T>.
+  if length(xs ++ ys) = 0
+  then length(xs) = 0
+proof
+  arbitrary T:type, xs:List<T>, ys:List<T>
+  assume premise: length(xs ++ ys) = 0
+  have f1: length(xs) + length(ys) = 0
+    by rewrite length_append<T>[xs,ys] in premise
+  apply add_to_zero_is_zero[length(xs), length(ys)] to f1
+end
+*/
+
+theorem intro_dichotomy:  all x:Nat, y:Nat.  x ≤ y  or  y < x
+proof
+  arbitrary x:Nat, y:Nat
+  have tri: x < y or x = y or y < x by trichotomy[x][y]
+  cases tri
+  case: x < y {
+    have: x ≤ y by apply less_implies_less_equal[x][y] to recall x < y
+    conclude x ≤ y or y < x by recall x ≤ y
+  }
+  case: x = y {
+    have: x ≤ y by
+        suffices y ≤ y  by rewrite (recall x = y)
+        less_equal_refl[y]
+    conclude x ≤ y or y < x by recall x ≤ y
+  }
+  case: y < x {
+    conclude x ≤ y or y < x by recall y < x
+  }
+end
+
+theorem prove_not_example: not (0 = 1)
+proof
+  assume z1: 0 = 1
+  conclude false by recall 0 = 1
+end
+
+theorem use_not_example: all P:bool. if P and not P then false
+proof
+  arbitrary P:bool
+  assume premise: P and not P
+  have np: not P by premise
+  have p: P by premise
+  conclude false by apply np to p
+end
+
+