def add := fun (lst : List Int) ↦
(do
let mut s : Int := (0 : Int)
for i in (PastaLean.pyRange (PastaLean.pyLen lst) (1 : Int) (2 : Int))do
-- The running sum stays even: it starts at 0 and only ever gains an even summand.
let _ := Libraries.passta.pyPassInvariant (s %ₚ (2 : Int) == (0 : Int))
-- Index bounds, so `lst[i]` is well-defined.
let _ := Libraries.passta.pyPassInvariant (decide ((1 : Int) ≤ i))
let _ := Libraries.passta.pyPassInvariant (decide (i < PastaLean.pyLen lst))
-- `range(1, _, 2)` only yields odd indices — the "at odd indices" half of the spec.
let _ := Libraries.passta.pyPassInvariant (i %ₚ (2 : Int) == (1 : Int))
if h_1 : lst⦋i⦌ %ₚ (2 : Int) = (0 : Int) then
s := s +ₚ lst⦋i⦌
else
let _ := ()
let _ := Libraries.passta.pyPassAssert (s %ₚ (2 : Int) == (0 : Int))
return s : Id _)
@[spec]
theorem add_spec : ⦃⌜PastaLean.pyLen lst > (0 : Int)⌝⦄ add lst ⦃⇓s => ⌜s %ₚ (2 : Int) = (0 : Int)⌝⦄ :=
lst:List ℤ⊢ ⦃⌜pyLen lst > 0⌝⦄ add lst ⦃PostCond.noThrow fun s => ⌜s %ₚ 2 = 0⌝⦄
lst:List ℤh✝³:pyLen lst > 0pref✝:List ℤcur✝:ℤsuff✝:List ℤh✝²:pyRange (pyLen lst) 1 2 = pref✝ ++ cur✝ :: suff✝b✝:ℤh✝¹:lst⦋cur✝⦌ %ₚ 2 = 0s✝:ℤ := b✝ +ₚ lst⦋cur✝⦌h✝:b✝ %ₚ 2 = 0⊢ s✝ %ₚ 2 = 0
all_goals (lst:List ℤpref✝:List ℤcur✝:ℤsuff✝:List ℤb✝:ℤs✝:ℤ := b✝ +ₚ lst⦋cur✝⦌h✝³:0 < pyLen lsth✝²:pyRange (pyLen lst) 1 2 = pref✝ ++ cur✝ :: suff✝h✝¹:(if lst⦋cur✝⦌ % 2 < 0 then lst⦋cur✝⦌ % 2 + 2 else lst⦋cur✝⦌ % 2) = 0h✝:(if b✝ % 2 < 0 then b✝ % 2 + 2 else b✝ % 2) = 0⊢ (if (b✝ + lst⦋cur✝⦌) % 2 < 0 then (b✝ + lst⦋cur✝⦌) % 2 + 2 else (b✝ + lst⦋cur✝⦌) % 2) = 0 lst:List ℤpref✝:List ℤcur✝:ℤsuff✝:List ℤb✝:ℤs✝:ℤ := b✝ +ₚ lst⦋cur✝⦌h✝³:0 < pyLen lsth✝²:pyRange (pyLen lst) 1 2 = pref✝ ++ cur✝ :: suff✝h✝¹:(if lst⦋cur✝⦌ % 2 < 0 then lst⦋cur✝⦌ % 2 + 2 else lst⦋cur✝⦌ % 2) = 0h✝:(if b✝ % 2 < 0 then b✝ % 2 + 2 else b✝ % 2) = 0⊢ (if (b✝ + lst⦋cur✝⦌) % 2 < 0 then (b✝ + lst⦋cur✝⦌) % 2 + 2 else (b✝ + lst⦋cur✝⦌) % 2) = 0 (first | All goals completed! 🐙 | grind | (split_ifs <;> omega) | grind +locals))
theorem add_correct :
∀ (lst : List Int),
PastaLean.pyLen lst > (0 : Int) →
let s := (add lst).run;
s %ₚ (2 : Int) = (0 : Int) :=
⊢ ∀ (lst : List ℤ),
pyLen lst > 0 →
let s := (add lst).run;
s %ₚ 2 = 0
lst:List ℤhpre:pyLen lst > 0⊢ let s := (add lst).run;
s %ₚ 2 = 0
All goals completed! 🐙