Merge branch 'main' into dev-hantao-autonumpy

alok · web-flow · commit 254a976765d5 · 2025-07-07T15:27:13.000-04:00
diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml
@@ -2,9 +2,10 @@ name: CI
 
 on:
   push:
-    branches: [ main, "*" ]
+    branches: [ "main", "*" ]
   pull_request:
-    branches: [ main, "*" ]
+    branches: [ "main", "*" ]
+
   workflow_dispatch:
 
 jobs:
@@ -118,4 +119,4 @@ jobs:
           path: |
             .lake/build/trace
             logs/
-            *.log
+            *.log
diff --git a/DafnySpecs/NpMax.lean b/DafnySpecs/NpMax.lean
@@ -0,0 +1,218 @@
+import Std.Do
+
+/-!
+# Array Maximum Specification
+
+Port of `np_max.dfy` to idiomatic Lean 4.
+
+This module demonstrates several approaches to finding the maximum element in an array:
+1. Runtime constraints via hypotheses (non-empty requirement)
+2. Compile-time constraints via dependent types
+3. Refinement types for non-empty arrays
+4. MPL-style specifications for future verification
+
+The Dafny specification requires:
+- Precondition: array length > 0
+- Postcondition 1: result equals some element in the array
+- Postcondition 2: result is greater than or equal to all elements
+-/
+
+namespace DafnySpecs.NpMax
+
+/-- Find maximum element in a non-empty array.
+    
+    The hypothesis `h` ensures the array is non-empty at the call site.
+    This mirrors the Dafny `requires a.Length > 0` clause.
+-/
+def max (a : Array Int) (h : a.size > 0) : Int :=
+  a.foldl (init := a[0]'(h)) max
+
+/-- Specification theorem: the maximum is an element of the array -/
+theorem max_exists (a : Array Int) (h : a.size > 0) :
+    ∃ i : Fin a.size, max a h = a[i] := by
+  sorry -- Proof would use properties of foldl and max
+
+/-- Specification theorem: the maximum is greater than or equal to all elements -/
+theorem max_universal (a : Array Int) (h : a.size > 0) :
+    ∀ i : Fin a.size, a[i] ≤ max a h := by
+  sorry -- Proof would use induction on foldl
+
+/-- Combined specification capturing both Dafny postconditions -/
+theorem max_spec (a : Array Int) (h : a.size > 0) :
+    (∃ i : Fin a.size, max a h = a[i]) ∧ 
+    (∀ i : Fin a.size, a[i] ≤ max a h) := by
+  constructor
+  · exact max_exists a h
+  · exact max_universal a h
+
+/-- MPL-style specification comment for future verification:
+    
+    ⦃ a.size > 0 ⦄ 
+      max a 
+    ⦃ λ res, (∃ i : Fin a.size, res = a[i]) ∧ (∀ i : Fin a.size, a[i] ≤ res) ⦄
+    
+    When MPL tactics are available, this can be proved using `mspec` or `mvcgen`.
+-/
+
+/- Alternative implementations with different trade-offs -/
+
+section AlternativeImplementations
+
+/-- Maximum using explicit recursion for clarity -/
+def maxRec (a : Array Int) (h : a.size > 0) : Int :=
+  go 1 a[0]'(h)
+where
+  go (i : Nat) (currMax : Int) : Int :=
+    if hi : i < a.size then
+      go (i + 1) (max currMax a[i])
+    else
+      currMax
+
+/-- Maximum that returns both the value and its index -/
+def maxWithIndex (a : Array Int) (h : a.size > 0) : Int × Fin a.size :=
+  a.foldlIdx (init := (a[0]'(h), ⟨0, h⟩)) fun i (currMax, idx) val =>
+    if val > currMax then (val, i) else (currMax, idx)
+
+/-- Theorem: maxWithIndex returns a valid maximum and witness index -/
+theorem maxWithIndex_correct (a : Array Int) (h : a.size > 0) :
+    let (m, idx) := maxWithIndex a h
+    m = a[idx] ∧ ∀ i : Fin a.size, a[i] ≤ m := by
+  sorry
+
+end AlternativeImplementations
+
+/- Vector approach using compile-time size checking -/
+
+section VectorApproach
+
+/-- Maximum for vectors with compile-time non-empty guarantee -/
+def maxVec {n : Nat} (a : Vector Int (n + 1)) : Int :=
+  a.toArray.foldl (init := a.get ⟨0, Nat.zero_lt_succ n⟩) max
+
+/-- Vector maximum satisfies the existence property -/
+theorem maxVec_exists {n : Nat} (a : Vector Int (n + 1)) :
+    ∃ i : Fin (n + 1), maxVec a = a.get i := by
+  sorry
+
+/-- Vector maximum satisfies the universal property -/
+theorem maxVec_universal {n : Nat} (a : Vector Int (n + 1)) :
+    ∀ i : Fin (n + 1), a.get i ≤ maxVec a := by
+  sorry
+
+end VectorApproach
+
+/- Refinement type approach -/
+
+section RefinementTypes
+
+/-- Non-empty array as a refinement type -/
+abbrev NonEmptyArray (α : Type) := {arr : Array α // arr.size > 0}
+
+/-- Maximum for non-empty arrays using refinement types -/
+def maxNonEmpty (a : NonEmptyArray Int) : Int :=
+  a.val.foldl (init := a.val[0]'(a.property)) max
+
+/-- Get an element from a non-empty array -/
+def NonEmptyArray.get (a : NonEmptyArray α) (i : Fin a.val.size) : α :=
+  a.val[i]
+
+/-- Refinement type version preserves specifications -/
+theorem maxNonEmpty_spec (a : NonEmptyArray Int) :
+    (∃ i : Fin a.val.size, maxNonEmpty a = a.get i) ∧ 
+    (∀ i : Fin a.val.size, a.get i ≤ maxNonEmpty a) := by
+  sorry
+
+end RefinementTypes
+
+/- Polymorphic versions -/
+
+section Polymorphic
+
+/-- Polymorphic maximum for any linearly ordered type -/
+def maxPoly {α : Type} [LinearOrder α] (a : Array α) (h : a.size > 0) : α :=
+  a.foldl (init := a[0]'(h)) max
+
+/-- Maximum with custom comparison function -/
+def maxBy {α : Type} (a : Array α) (h : a.size > 0) (cmp : α → α → Bool) : α :=
+  a.foldl (init := a[0]'(h)) fun x y => if cmp y x then y else x
+
+/-- Maximum by key extraction -/
+def maxByKey {α β : Type} [LinearOrder β] (a : Array α) (h : a.size > 0) (key : α → β) : α :=
+  a.foldl (init := a[0]'(h)) fun x y => if key y > key x then y else x
+
+end Polymorphic
+
+/- Properties and theorems -/
+
+section Properties
+
+/-- Maximum is idempotent -/
+theorem max_singleton (x : Int) :
+    max #[x] (by simp) = x := by
+  unfold max
+  simp
+
+/-- Maximum of two elements -/
+theorem max_pair (x y : Int) :
+    max #[x, y] (by simp) = Int.max x y := by
+  unfold max
+  simp [Int.max]
+
+/-- Maximum is preserved under array concatenation -/
+theorem max_append (a b : Array Int) (ha : a.size > 0) (hb : b.size > 0) :
+    max (a ++ b) (by simp [ha, hb]) = Int.max (max a ha) (max b hb) := by
+  sorry
+
+/-- Maximum respects monotone transformations -/
+theorem max_map_mono {f : Int → Int} (hf : Monotone f) (a : Array Int) (h : a.size > 0) :
+    f (max a h) = max (a.map f) (by simp [h]) := by
+  sorry
+
+end Properties
+
+/- Option-based API for more idiomatic Lean -/
+
+section OptionAPI
+
+/-- Safe maximum that returns None for empty arrays -/
+def maxOption (a : Array Int) : Option Int :=
+  if h : a.size > 0 then
+    some (max a h)
+  else
+    none
+
+/-- Option version specification -/
+theorem maxOption_spec (a : Array Int) :
+    match maxOption a with
+    | none => a.size = 0
+    | some m => a.size > 0 ∧ (∃ i : Fin a.size, m = a[i]) ∧ (∀ i : Fin a.size, a[i] ≤ m) := by
+  sorry
+
+/-- Maximum with default value for empty arrays -/
+def maxWithDefault (a : Array Int) (default : Int) : Int :=
+  maxOption a |>.getD default
+
+end OptionAPI
+
+section Examples
+
+/- Example usage:
+#eval max #[3, 1, 4, 1, 5, 9] (by simp)
+-- Output: 9
+
+#eval maxWithIndex #[3, 1, 4, 1, 5, 9] (by simp)
+-- Output: (9, 5)
+
+#eval maxOption #[]
+-- Output: none
+
+#eval maxOption #[42]
+-- Output: some 42
+
+#check maxVec ⟨#[1, 2, 3], rfl⟩
+-- Type: Int
+-/
+
+end Examples
+
+end DafnySpecs.NpMax
diff --git a/DafnySpecs/NpMultiply.lean b/DafnySpecs/NpMultiply.lean
@@ -0,0 +1,107 @@
+/-!
+# Array Multiplication Specification
+
+Port of `np_multiply.dfy` to idiomatic Lean 4.
+
+This module demonstrates several approaches to specifying element-wise array multiplication:
+1. Runtime constraints via hypotheses
+2. Compile-time constraints via dependent types
+3. MPL-style specifications for future verification
+-/
+
+namespace DafnySpecs.NpMultiply
+
+/-- Element-wise multiplication of arrays with runtime size checking.
+    
+    The hypothesis `h` ensures arrays have equal length at the call site.
+    This mirrors the Dafny `requires` clause.
+-/
+def multiply (a b : Array Int) (_ : a.size = b.size) : Array Int :=
+  Array.zipWith (· * ·) a b
+
+/-- Specification theorem: result has same length as inputs -/
+theorem multiply_length (a b : Array Int) (h : a.size = b.size) :
+    (multiply a b h).size = a.size := by
+  simp only [multiply, Array.size_zipWith, h, Nat.min_self]
+
+/-- Specification theorem: element-wise correctness -/
+theorem multiply_elem (a b : Array Int) (h : a.size = b.size) (i : Nat) (hi : i < a.size) :
+    (multiply a b h)[i]'(by simp [multiply_length, hi]) = a[i] * b[i] := by
+  sorry
+
+section VectorApproach
+
+/-- Multiplication using vectors with compile-time size checking.
+    
+    This approach eliminates the need for runtime hypotheses by encoding
+    the size constraint in the type system.
+-/
+def multiplyVec {n : Nat} (a b : Vector Int n) : Vector Int n :=
+  ⟨Array.zipWith (· * ·) a.toArray b.toArray, by simp [Array.size_zipWith]⟩
+
+/-- Vector multiplication preserves all elements correctly -/
+theorem multiplyVec_elem {n : Nat} (a b : Vector Int n) (i : Fin n) :
+    (multiplyVec a b).get i = a.get i * b.get i := by
+  simp [multiplyVec, Vector.get]
+
+end VectorApproach
+
+section GeneralizedApproach
+
+/-- Polymorphic multiplication for any type with a Mul instance -/
+def multiplyPoly {α : Type} [Mul α] (a b : Array α) (_ : a.size = b.size) : Array α :=
+  Array.zipWith (· * ·) a b
+
+/-- Multiplication for non-empty arrays (refinement type approach) -/
+def multiplyNonEmpty (a b : {arr : Array Int // arr.size > 0}) 
+    (h : a.val.size = b.val.size) : {arr : Array Int // arr.size > 0} :=
+  ⟨Array.zipWith (· * ·) a.val b.val, by
+    simp only [Array.size_zipWith, h, Nat.min_self]
+    exact b.property⟩
+
+end GeneralizedApproach
+
+section Properties
+
+/-- Multiplication is commutative when the element type is commutative -/
+theorem multiply_comm (a b : Array Int) (h : a.size = b.size) :
+    multiply a b h = multiply b a h.symm := by
+  sorry
+
+/-- Multiplication is associative (with appropriate size constraints) -/
+theorem multiply_assoc (a b c : Array Int) 
+    (hab : a.size = b.size) (hbc : b.size = c.size) :
+    multiply (multiply a b hab) c (sorry : (multiply a b hab).size = c.size) = 
+    multiply a (multiply b c hbc) (sorry : a.size = (multiply b c hbc).size) := by
+  sorry
+
+/-- One array is the identity element -/
+def ones (n : Nat) : Array Int := Array.replicate n 1
+
+theorem multiply_one (a : Array Int) :
+    multiply a (ones a.size) (by simp only [ones, Array.size_replicate]) = a := by
+  sorry
+
+/-- Zero array is the zero element (multiplication by zero) -/
+def zeros (n : Nat) : Array Int := Array.replicate n 0
+
+theorem multiply_zero (a : Array Int) :
+    multiply a (zeros a.size) (by simp only [zeros, Array.size_replicate]) = zeros a.size := by
+  sorry
+
+/-- Multiplication distributes over addition -/
+theorem multiply_add_distrib (a b c : Array Int) 
+    (hab : a.size = b.size) (hac : a.size = c.size) :
+    multiply a (Array.zipWith (· + ·) b c) (sorry : a.size = (Array.zipWith (· + ·) b c).size) =
+    Array.zipWith (· + ·) (multiply a b hab) (multiply a c hac) := by
+  sorry
+
+end Properties
+
+section Examples
+
+#check multiply #[1, 2, 3] #[4, 5, 6] rfl
+
+end Examples
+
+end DafnySpecs.NpMultiply
diff --git a/DafnySpecs/NpSum.lean b/DafnySpecs/NpSum.lean
