add examples for tutuorial

Author: volodeyka

CaseStudies/Velvet/VelvetExamples/Demo/InsertionSort.lean

@@ -0,0 +1,150 @@
+----------------------------------------------------
+-- Example 1: Velvet basics
+----------------------------------------------------
+
+import Mathlib.Algebra.BigOperators.Intervals
+import Mathlib.Algebra.Ring.Int.Defs
+
+import CaseStudies.Velvet.Std
+import CaseStudies.TestingUtil
+
+section squareRoot
+
+set_option loom.semantics.termination "partial"
+set_option loom.semantics.choice "demonic"
+set_option loom.solver "cvc5"
+
+-- (1) Proving things with SMT
+-- partial correctness version of square root
+method sqrt (x: ℕ) return (res: ℕ)
+  ensures res * res ≤ x
+  ensures ∀ i, i ≤ res → i * i ≤ x
+  ensures ∀ i, i * i ≤ x → i ≤ res
+  do
+    if x = 0 then
+      return 0
+    else
+      let mut i := 0
+      while i * i  ≤ x
+      invariant ∀ j, j < i → j * j ≤ x
+      do
+        i := i + 1
+      return i - 1
+prove_correct sqrt by
+  loom_solve
+  -- all_goals loom_smt [*]
+
+end squareRoot
+
+-- (2) Insertion sort
+section insertionSort
+
+/-
+
+Dafny code below for reference
+
+method insertionSort(arr: array<int>)
+  modifies arr
+  ensures forall i, j :: 0 <= i < j < arr.Length ==> arr[i] <= arr[j]
+  ensures multiset(arr[..]) == old(multiset(arr[..]))
+{
+  if arr.Length <= 1 {
+    return;
+  }
+  var n := 1;
+  while n != arr.Length
+  invariant 0 <= n <= arr.Length
+  invariant forall i, j :: 0 <= i < j <= n - 1 ==> arr[i] <= arr[j]
+  invariant multiset(arr[..]) == old(multiset(arr[..]))
+  {
+    var mind := n;
+    while mind != 0
+    invariant 0 <= mind <= n
+    invariant multiset(arr[..]) == old(multiset(arr[..]))
+    invariant forall i, j :: 0 <= i < j <= n && (j != mind)==> arr[i] <= arr[j]
+    {
+      if arr[mind] <= arr[mind - 1] {
+        arr[mind], arr[mind - 1] := arr[mind - 1], arr[mind];
+      }
+      mind := mind - 1;
+    }
+    n := n + 1;
+  }
+}
+-/
+
+attribute [grind] Array.multiset_swap
+
+
+set_option loom.semantics.termination "partial"
+-- set_option loom.semantics.termination "total"
+set_option loom.semantics.choice "demonic"
+
+--partial correctness version of insertionSort
+-- uncomment termination measures for total correctness
+method insertionSort
+  (mut arr: Array Int) return (u: Unit)
+  require 1 ≤ arr.size
+  ensures forall i j, 0 ≤ i ∧ i ≤ j ∧ j < arr.size → arr[i]! ≤ arr[j]!
+  ensures arr.toMultiset = arr.toMultiset
+  do
+    let arr₀ := arr
+    let arr_size := arr.size
+    let mut n := 1
+    while n ≠ arr.size
+    invariant arr.size = arr_size
+    invariant 1 ≤ n ∧ n ≤ arr.size
+    invariant forall i j, 0 ≤ i ∧ i < j ∧ j <= n - 1 → arr[i]! ≤ arr[j]!
+    invariant arr.toMultiset = arr₀.toMultiset
+    -- decreasing size arr - n
+    do
+      let mut mind := n
+      while mind ≠ 0
+      invariant arr.size = arr_size
+      invariant mind ≤ n
+      invariant forall i j, 0 ≤ i ∧ i < j ∧ j ≤ n ∧ j ≠ mind → arr[i]! ≤ arr[j]!
+      invariant arr.toMultiset = arr₀.toMultiset
+      -- decreasing mind
+      do
+        if arr[mind]! < arr[mind - 1]! then
+          swap! arr[mind - 1]! arr[mind]!
+        mind := mind - 1
+      -- n := n + 1 -- try commenting this out for termination
+    return
+
+-- Let's test this stuff
+extract_program_for insertionSort
+
+-- Determinising the execution
+-- #print insertionSortExec
+
+-- Prove decidability as we need to check them
+prove_precondition_decidable_for insertionSort
+-- #print insertionSortPreDecidable
+prove_postcondition_decidable_for insertionSort
+derive_tester_for insertionSort
+
+-- (2.1) Doing simple testing
+-- See here where the postcondition is violated
+
+-- run_elab do
+--   -- Generate random arrays
+--   let g : Plausible.Gen (_ × Bool) := do
+--     let arr ← Plausible.SampleableExt.interpSample (Array Int)
+--     let res := insertionSortTester arr
+--     pure (arr, res)
+--   for _ in [1: 500] do
+--     let res ← Plausible.Gen.run g 10
+--     unless res.2 do
+--       IO.println s!"postcondition violated for input {res.1}"
+--       break
+
+-- (2.2) This just works
+
+set_option maxHeartbeats 1000000
+
+prove_correct insertionSort by
+  -- loom_solve
+  loom_solve_async
+
+end insertionSort

CaseStudies/Velvet/VelvetExamples/Demo/OneThird.lean

@@ -0,0 +1,65 @@
+----------------------------------------------------
+-- Example 2: Combining Velvet and non-trivial math
+----------------------------------------------------
+
+import Auto
+
+import CaseStudies.Velvet.Std
+import CaseStudies.TestingUtil
+
+import Mathlib.Tactic
+
+set_option loom.semantics.termination "total"
+set_option loom.semantics.choice "demonic"
+
+open Filter Topology
+
+/- noncomputable is needed because we use operations on ℝ -/
+-- This function computers a sum of series
+noncomputable method oneThird (n: Nat) return (res: ℝ)
+  require n > 0
+  ensures res = ∑ j ∈ Finset.range n, (j^2/n^3 : ℝ)
+  do
+    let mut res : Real := 0
+    let mut i := 0
+    while i < n
+    invariant i <= n
+    invariant res = ∑ j ∈ Finset.range i, (j^2/n^3 : ℝ)
+    decreasing n - i
+    do
+      let x : ℝ := i / n
+      res := res + (x * x) / n
+      i := i + 1
+    return res
+
+grind_pattern Finset.sum_range_succ => Finset.sum (Finset.range (n + 1)) f
+grind_pattern Finset.sum_range_zero => Finset.sum (Finset.range 0) f
+
+/- half a second! -/
+prove_correct oneThird by loom_solve
+
+-- Proving the closed form for the sum of series: (n * (n + 1) * (2 * n + 1)) / 6
+theorem tends_to_third' :
+  Tendsto (fun n ↦ ∑ i ∈ Finset.range (n + 1), (Nat.cast (R := ℝ) i) ^ 2 / (n + 1) ^ 3) atTop (𝓝 (1 / 3)) := by
+    -- We'll use the fact that $\sum_{i=0}^{n} i^2 = \frac{n(n+1)(2n+1)}{6}$ to simplify the expression.
+    have h_sum : ∀ n : ℕ, (∑ i ∈ Finset.range (n + 1), (i : ℝ) ^ 2) = (n * (n + 1) * (2 * n + 1) : ℝ) / 6 := by
+      exact fun n => by induction n <;> norm_num [ Finset.sum_range_succ ] at * ; linarith;
+    -- Substitute the formula for the sum of squares into the expression.
+    suffices h_suff : Filter.Tendsto (fun n : ℕ => ((n * (n + 1) * (2 * n + 1) : ℝ) / 6) / ((n + 1) ^ 3)) Filter.atTop (𝓝 (1 / 3)) by
+      -- Substitute the formula for the sum of squares into the expression and simplify.
+      simp_all +decide [ ← Finset.sum_div ];
+    -- We can divide the numerator and the denominator by $n^3$ and then take the limit as $n$ approaches infinity.
+    suffices h_div : Filter.Tendsto (fun n : ℕ => ((1 : ℝ) * (1 + 1 / (n : ℝ)) * (2 + 1 / (n : ℝ)) / 6) / ((1 + 1 / (n : ℝ)) ^ 3)) Filter.atTop (𝓝 (1 / 3)) by
+      refine h_div.congr' ( by filter_upwards [ Filter.eventually_gt_atTop 0 ] with n hn; rw [ div_eq_div_iff ] <;> first | positivity | field_simp [ -one_div, hn.ne' ] );
+    convert Filter.Tendsto.div ( Filter.Tendsto.div_const ( Filter.Tendsto.mul ( tendsto_const_nhds.mul ( tendsto_const_nhds.add ( tendsto_one_div_atTop_nhds_zero_nat ) ) ) ( tendsto_const_nhds.add ( tendsto_one_div_atTop_nhds_zero_nat ) ) ) _ ) ( Filter.Tendsto.pow ( tendsto_const_nhds.add ( tendsto_one_div_atTop_nhds_zero_nat ) ) _ ) _ using 2 <;> norm_num
+
+-- Proving that (n * (n + 1) * (2 * n + 1)) / 6 tends to 1/3 when n goes to
+-- infinity
+--
+/- main theorem: `oneThird (n + 1) |>.extract` is pure extraction of the `oneThird`
+  Such extraction is guaranteed to converge and obey the same specification as
+  the original `oneThird` as we have proven _total correctness_ of the `oneThird` method -/
+lemma tends_to_third :
+  Tendsto (fun n ↦ oneThird (n + 1) |>.extract) atTop (𝓝 (1 / 3)) := by
+  apply Tendsto.congr _ tends_to_third'; intro n;
+  erw [VelvetM.extract_spec _ _ (oneThird_correct _)] <;> grind