ex_double_the_differencemade with verso-snippets
View
def double_the_difference := fun (lst : List Int) ↦
  (do
    let mut ans : Int := (0 : Int)
    for num in (PastaLean.pyIter lst)do
      let _ := Libraries.passta.pyPassInvariant (decide (ans ≥ (0 : Int)))
      if h_1 :
          (num %ₚ (2 : Int) = (1 : Int) ∧ num > (0 : Int)) ∧
            !(PastaLean.pyStrContainsSubstr (PastaLean.pyStr num) ".") then
        
        ans := ans +ₚ num ^ₚ (2 : Int)
      else
        let _ := ()
    let _ := Libraries.passta.pyPassAssert (decide (ans ≥ (0 : Int)))
    return ans : Id _)

private theorem pyMod_two (a : Int) : a %ₚ (2 : Int) = a % 2 := bya:ℤ⊢ a %ₚ 2 = a % 2
  show PastaLean.pyMod a 2 = a % 2a:ℤ⊢ pyMod a 2 = a % 2
  have h1 : 0 ≤ a % 2 := Int.emod_nonneg a (bya:ℤ⊢ 2 ≠ 0 decideAll goals completed! 🐙)a:ℤh1:0 ≤ a % 2⊢ pyMod a 2 = a % 2
  unfold PastaLean.pyModa:ℤh1:0 ≤ a % 2⊢ (if (2 == 0) = true then a
  else
    have r := a % 2;
    if (decide (r < 0) && decide (2 > 0) || decide (r > 0) && decide (2 < 0)) = true then r + 2 else r) =
  a % 2; split_ifsposa:ℤh1:0 ≤ a % 2h✝:(2 == 0) = true⊢ a = a % 2nega:ℤh1:0 ≤ a % 2h✝:¬(2 == 0) = true⊢ (have r := a % 2;
  if (decide (r < 0) && decide (2 > 0) || decide (r > 0) && decide (2 < 0)) = true then r + 2 else r) =
  a % 2 <;>posa:ℤh1:0 ≤ a % 2h✝:(2 == 0) = true⊢ a = a % 2nega:ℤh1:0 ≤ a % 2h✝:¬(2 == 0) = true⊢ (have r := a % 2;
  if (decide (r < 0) && decide (2 > 0) || decide (r > 0) && decide (2 < 0)) = true then r + 2 else r) =
  a % 2 simp_allAll goals completed! 🐙

private theorem foldl_padd_shift (l : List Int) (s : Int) :
    l.foldl (fun acc x => acc +ₚ x) s = s + l.foldl (fun acc x => acc +ₚ x) 0 := byl:List ℤs:ℤ⊢ List.foldl (fun acc x => acc +ₚ x) s l = s + List.foldl (fun acc x => acc +ₚ x) 0 l
  induction l generalizing s with
  | nil =>nils:ℤ⊢ List.foldl (fun acc x => acc +ₚ x) s [] = s + List.foldl (fun acc x => acc +ₚ x) 0 [] simpAll goals completed! 🐙
  | cons h t ih =>consh:ℤt:List ℤih:∀ (s : ℤ), List.foldl (fun acc x => acc +ₚ x) s t = s + List.foldl (fun acc x => acc +ₚ x) 0 ts:ℤ⊢ List.foldl (fun acc x => acc +ₚ x) s (h :: t) = s + List.foldl (fun acc x => acc +ₚ x) 0 (h :: t)
    simp only [List.foldl_cons]consh:ℤt:List ℤih:∀ (s : ℤ), List.foldl (fun acc x => acc +ₚ x) s t = s + List.foldl (fun acc x => acc +ₚ x) 0 ts:ℤ⊢ List.foldl (fun acc x => acc +ₚ x) (s +ₚ h) t = s + List.foldl (fun acc x => acc +ₚ x) (0 +ₚ h) t
    rw [ih (s +ₚ h),consh:ℤt:List ℤih:∀ (s : ℤ), List.foldl (fun acc x => acc +ₚ x) s t = s + List.foldl (fun acc x => acc +ₚ x) 0 ts:ℤ⊢ s +ₚ h + List.foldl (fun acc x => acc +ₚ x) 0 t = s + List.foldl (fun acc x => acc +ₚ x) (0 +ₚ h) t ih (0 +ₚ h)consh:ℤt:List ℤih:∀ (s : ℤ), List.foldl (fun acc x => acc +ₚ x) s t = s + List.foldl (fun acc x => acc +ₚ x) 0 ts:ℤ⊢ s +ₚ h + List.foldl (fun acc x => acc +ₚ x) 0 t = s + (0 +ₚ h + List.foldl (fun acc x => acc +ₚ x) 0 t)]consh:ℤt:List ℤih:∀ (s : ℤ), List.foldl (fun acc x => acc +ₚ x) s t = s + List.foldl (fun acc x => acc +ₚ x) 0 ts:ℤ⊢ s +ₚ h + List.foldl (fun acc x => acc +ₚ x) 0 t = s + (0 +ₚ h + List.foldl (fun acc x => acc +ₚ x) 0 t)
    simp only [show ∀ x y : Int, x +ₚ y = x + y from fun _ _ => rfl]consh:ℤt:List ℤih:∀ (s : ℤ), List.foldl (fun acc x => acc +ₚ x) s t = s + List.foldl (fun acc x => acc +ₚ x) 0 ts:ℤ⊢ s + h + List.foldl (fun acc x => acc + x) 0 t = s + (0 + h + List.foldl (fun acc x => acc + x) 0 t)
    ringAll goals completed! 🐙

private theorem pySum_int_append (a b : List Int) :
    PastaLean.pySum (a ++ b) = PastaLean.pySum a + PastaLean.pySum b := bya:List ℤb:List ℤ⊢ pySum (a ++ b) = pySum a + pySum b
  simp only [PastaLean.pySum, PastaLean.pyIter_list, PySummand.toSummand, id_eq, List.foldl_append]a:List ℤb:List ℤ⊢ List.foldl (fun acc x => acc +ₚ x) (List.foldl (fun acc x => acc +ₚ x) 0 a) b =
  List.foldl (fun acc x => acc +ₚ x) 0 a + List.foldl (fun acc x => acc +ₚ x) 0 b
  rw [foldl_padd_shift b (a.foldl (fun acc x => acc +ₚ x) 0)a:List ℤb:List ℤ⊢ List.foldl (fun acc x => acc +ₚ x) 0 a + List.foldl (fun acc x => acc +ₚ x) 0 b =
  List.foldl (fun acc x => acc +ₚ x) 0 a + List.foldl (fun acc x => acc +ₚ x) 0 b]All goals completed! 🐙

private theorem pySum_int_singleton (x : Int) : PastaLean.pySum [x] = x := byx:ℤ⊢ pySum [x] = x
  simp only [PastaLean.pySum, PastaLean.pyIter_list, PySummand.toSummand, id_eq,
    List.foldl_cons, List.foldl_nil]x:ℤ⊢ 0 +ₚ x = x
  rw [show (0 : Int) +ₚ x = 0 + x from rfl,x:ℤ⊢ 0 + x = x zero_addx:ℤ⊢ x = x]All goals completed! 🐙

private theorem sq_odd_emod_two {c : Int} (h : c % 2 = 1) : c * c % 2 = 1 := byc:ℤh:c % 2 = 1⊢ c * c % 2 = 1
  rw [Int.mul_emod,c:ℤh:c % 2 = 1⊢ c % 2 * (c % 2) % 2 = 1 hc:ℤh:c % 2 = 1⊢ 1 * 1 % 2 = 1]c:ℤh:c % 2 = 1⊢ 1 * 1 % 2 = 1; decideAll goals completed! 🐙

private theorem pySum_int_nil : PastaLean.pySum ([] : List Int) = 0 := rfl

@[spec]
theorem double_the_difference_spec :
    ⦃⌜True⌝⦄ double_the_difference lst ⦃⇓ans =>
      ⌜(ans =
              PastaLean.pySum
                ((List.filter
                      (fun v =>
                        (v %ₚ (2 : Int) = (1 : Int) ∧ v > (0 : Int)) ∧
                          !(PastaLean.pyStrContainsSubstr (PastaLean.pyStr v) "."))
                      (PastaLean.pyIter lst)).map
                  fun v => v *ₚ v) ∧
            ans %ₚ (2 : Int) =
              PastaLean.pyLen
                  ((List.filter
                        (fun v =>
                          (v %ₚ (2 : Int) = (1 : Int) ∧ v > (0 : Int)) ∧
                            !(PastaLean.pyStrContainsSubstr (PastaLean.pyStr v) "."))
                        (PastaLean.pyIter lst)).map
                    fun v => v) %ₚ
                (2 : Int)) ∧
          ans ≥ (0 : Int)⌝⦄ :=
  bylst:List ℤ⊢ ⦃⌜True⌝⦄
  double_the_difference
    lst ⦃PostCond.noThrow fun ans =>
    ⌜(ans =
            pySum
              (List.map (fun v => v *ₚ v)
                (List.filter (fun v => decide ((v %ₚ 2 = 1 ∧ v > 0) ∧ (!pyStrContainsSubstr (pyStr v) ".") = true))
                  (pyIter lst))) ∧
          ans %ₚ 2 =
            pyLen
                (List.map (fun v => v)
                  (List.filter (fun v => decide ((v %ₚ 2 = 1 ∧ v > 0) ∧ (!pyStrContainsSubstr (pyStr v) ".") = true))
                    (pyIter lst))) %ₚ
              2) ∧
        ans ≥ 0⌝⦄
  mvcgen [double_the_difference, PastaLean.pyRange_forIn, PastaLean.pyRange_forIn_start] invariants
    · ⇓⟨cur, ans⟩ =>
      ⌜(ans =
              PastaLean.pySum
                ((List.filter
                      (fun v =>
                        (v %ₚ (2 : Int) = (1 : Int) ∧ v > (0 : Int)) ∧
                          !(PastaLean.pyStrContainsSubstr (PastaLean.pyStr v) "."))
                      cur.prefix).map
                  fun v => v *ₚ v) ∧
            ans %ₚ (2 : Int) =
              PastaLean.pyLen
                  ((List.filter
                        (fun v =>
                          (v %ₚ (2 : Int) = (1 : Int) ∧ v > (0 : Int)) ∧
                            !(PastaLean.pyStrContainsSubstr (PastaLean.pyStr v) "."))
                        cur.prefix).map
                    fun v => v) %ₚ
                (2 : Int)) ∧
          ans ≥ (0 : Int)⌝vc1.step.isTruelst:List ℤpref✝:List ℤcur✝:ℤsuff✝:List ℤh✝²:pyIter lst = pref✝ ++ cur✝ :: suff✝b✝:ℤh✝¹:(cur✝ %ₚ 2 = 1 ∧ cur✝ > 0) ∧ (!pyStrContainsSubstr (pyStr cur✝) ".") = trueans✝:ℤ := b✝ +ₚ cur✝ ^ₚ 2h✝:(b✝ =
      pySum
        (List.map (fun v => v *ₚ v)
          (List.filter (fun v => decide ((v %ₚ 2 = 1 ∧ v > 0) ∧ (!pyStrContainsSubstr (pyStr v) ".") = true)) pref✝)) ∧
    b✝ %ₚ 2 =
      pyLen
          (List.map (fun v => v)
            (List.filter (fun v => decide ((v %ₚ 2 = 1 ∧ v > 0) ∧ (!pyStrContainsSubstr (pyStr v) ".") = true))
              pref✝)) %ₚ
        2) ∧
  b✝ ≥ 0⊢ (ans✝ =
      pySum
        (List.map (fun v => v *ₚ v)
          (List.filter (fun v => decide ((v %ₚ 2 = 1 ∧ v > 0) ∧ (!pyStrContainsSubstr (pyStr v) ".") = true))
            (pref✝ ++ [cur✝]))) ∧
    ans✝ %ₚ 2 =
      pyLen
          (List.map (fun v => v)
            (List.filter (fun v => decide ((v %ₚ 2 = 1 ∧ v > 0) ∧ (!pyStrContainsSubstr (pyStr v) ".") = true))
              (pref✝ ++ [cur✝]))) %ₚ
        2) ∧
  ans✝ ≥ 0vc2.step.isFalselst:List ℤpref✝:List ℤcur✝:ℤsuff✝:List ℤh✝²:pyIter lst = pref✝ ++ cur✝ :: suff✝b✝:ℤh✝¹:¬((cur✝ %ₚ 2 = 1 ∧ cur✝ > 0) ∧ (!pyStrContainsSubstr (pyStr cur✝) ".") = true)h✝:(b✝ =
      pySum
        (List.map (fun v => v *ₚ v)
          (List.filter (fun v => decide ((v %ₚ 2 = 1 ∧ v > 0) ∧ (!pyStrContainsSubstr (pyStr v) ".") = true)) pref✝)) ∧
    b✝ %ₚ 2 =
      pyLen
          (List.map (fun v => v)
            (List.filter (fun v => decide ((v %ₚ 2 = 1 ∧ v > 0) ∧ (!pyStrContainsSubstr (pyStr v) ".") = true))
              pref✝)) %ₚ
        2) ∧
  b✝ ≥ 0⊢ (b✝ =
      pySum
        (List.map (fun v => v *ₚ v)
          (List.filter (fun v => decide ((v %ₚ 2 = 1 ∧ v > 0) ∧ (!pyStrContainsSubstr (pyStr v) ".") = true))
            (pref✝ ++ [cur✝]))) ∧
    b✝ %ₚ 2 =
      pyLen
          (List.map (fun v => v)
            (List.filter (fun v => decide ((v %ₚ 2 = 1 ∧ v > 0) ∧ (!pyStrContainsSubstr (pyStr v) ".") = true))
              (pref✝ ++ [cur✝]))) %ₚ
        2) ∧
  b✝ ≥ 0
  all_goals
    simp only [PastaLean.pyIter_list, List.filter_append, List.map_append, pySum_int_append,
      List.filter_cons, List.filter_nil, List.map_cons, List.map_nil, List.append_nil,
      pySum_int_singleton, pyHPow_two, PastaLean.pyLen, PastaLean.PyLen.pyLen,
      List.length_append, List.length_cons, List.length_nil, List.length_map, pyMod_two,
      show ∀ x y : Int, x +ₚ y = x + y from fun _ _ => rfl,
      show ∀ x y : Int, x *ₚ y = x * y from fun _ _ => rfl] at *vc2.step.isFalselst:List ℤpref✝:List ℤcur✝:ℤsuff✝:List ℤh✝²:lst = pref✝ ++ cur✝ :: suff✝b✝:ℤh✝¹:¬((cur✝ % 2 = 1 ∧ cur✝ > 0) ∧ (!pyStrContainsSubstr (pyStr cur✝) ".") = true)h✝:(b✝ =
      pySum
        (List.map (fun v => v * v)
          (List.filter (fun v => decide ((v % 2 = 1 ∧ v > 0) ∧ (!pyStrContainsSubstr (pyStr v) ".") = true)) pref✝)) ∧
    b✝ % 2 =
      ↑(List.filter (fun v => decide ((v % 2 = 1 ∧ v > 0) ∧ (!pyStrContainsSubstr (pyStr v) ".") = true))
              pref✝).length %
        2) ∧
  b✝ ≥ 0⊢ (b✝ =
      pySum
          (List.map (fun v => v * v)
            (List.filter (fun v => decide ((v % 2 = 1 ∧ v > 0) ∧ (!pyStrContainsSubstr (pyStr v) ".") = true)) pref✝)) +
        pySum
          (List.map (fun v => v * v)
            (if decide ((cur✝ % 2 = 1 ∧ cur✝ > 0) ∧ (!pyStrContainsSubstr (pyStr cur✝) ".") = true) = true then [cur✝]
            else [])) ∧
    b✝ % 2 =
      ↑((List.filter (fun v => decide ((v % 2 = 1 ∧ v > 0) ∧ (!pyStrContainsSubstr (pyStr v) ".") = true))
                pref✝).length +
            (if decide ((cur✝ % 2 = 1 ∧ cur✝ > 0) ∧ (!pyStrContainsSubstr (pyStr cur✝) ".") = true) = true then [cur✝]
              else []).length) %
        2) ∧
  b✝ ≥ 0
  ·vc1.step.isTruelst:List ℤpref✝:List ℤcur✝:ℤsuff✝:List ℤh✝²:lst = pref✝ ++ cur✝ :: suff✝b✝:ℤans✝:ℤ := b✝ +ₚ cur✝ ^ₚ 2h✝¹:(cur✝ % 2 = 1 ∧ cur✝ > 0) ∧ (!pyStrContainsSubstr (pyStr cur✝) ".") = trueh✝:(b✝ =
      pySum
        (List.map (fun v => v * v)
          (List.filter (fun v => decide ((v % 2 = 1 ∧ v > 0) ∧ (!pyStrContainsSubstr (pyStr v) ".") = true)) pref✝)) ∧
    b✝ % 2 =
      ↑(List.filter (fun v => decide ((v % 2 = 1 ∧ v > 0) ∧ (!pyStrContainsSubstr (pyStr v) ".") = true))
              pref✝).length %
        2) ∧
  b✝ ≥ 0⊢ (ans✝ =
      pySum
          (List.map (fun v => v * v)
            (List.filter (fun v => decide ((v % 2 = 1 ∧ v > 0) ∧ (!pyStrContainsSubstr (pyStr v) ".") = true)) pref✝)) +
        pySum
          (List.map (fun v => v * v)
            (if decide ((cur✝ % 2 = 1 ∧ cur✝ > 0) ∧ (!pyStrContainsSubstr (pyStr cur✝) ".") = true) = true then [cur✝]
            else [])) ∧
    ans✝ % 2 =
      ↑((List.filter (fun v => decide ((v % 2 = 1 ∧ v > 0) ∧ (!pyStrContainsSubstr (pyStr v) ".") = true))
                pref✝).length +
            (if decide ((cur✝ % 2 = 1 ∧ cur✝ > 0) ∧ (!pyStrContainsSubstr (pyStr cur✝) ".") = true) = true then [cur✝]
              else []).length) %
        2) ∧
  ans✝ ≥ 0 -- vc1.step.isTrue: contributing element
    obtain ⟨⟨hsum, hpar⟩, hpos⟩ := ‹(_ = PastaLean.pySum _ ∧ _) ∧ _ ≥ (0:Int)›vc1.step.isTruelst:List ℤpref✝:List ℤcur✝:ℤsuff✝:List ℤh✝²:lst = pref✝ ++ cur✝ :: suff✝b✝:ℤans✝:ℤ := b✝ +ₚ cur✝ ^ₚ 2h✝¹:(cur✝ % 2 = 1 ∧ cur✝ > 0) ∧ (!pyStrContainsSubstr (pyStr cur✝) ".") = trueh✝:(b✝ =
      pySum
        (List.map (fun v => v * v)
          (List.filter (fun v => decide ((v % 2 = 1 ∧ v > 0) ∧ (!pyStrContainsSubstr (pyStr v) ".") = true)) pref✝)) ∧
    b✝ % 2 =
      ↑(List.filter (fun v => decide ((v % 2 = 1 ∧ v > 0) ∧ (!pyStrContainsSubstr (pyStr v) ".") = true))
              pref✝).length %
        2) ∧
  b✝ ≥ 0hpos:b✝ ≥ 0hsum:b✝ =
  pySum
    (List.map (fun v => v * v)
      (List.filter (fun v => decide ((v % 2 = 1 ∧ v > 0) ∧ (!pyStrContainsSubstr (pyStr v) ".") = true)) pref✝))hpar:b✝ % 2 =
  ↑(List.filter (fun v => decide ((v % 2 = 1 ∧ v > 0) ∧ (!pyStrContainsSubstr (pyStr v) ".") = true)) pref✝).length % 2⊢ (ans✝ =
      pySum
          (List.map (fun v => v * v)
            (List.filter (fun v => decide ((v % 2 = 1 ∧ v > 0) ∧ (!pyStrContainsSubstr (pyStr v) ".") = true)) pref✝)) +
        pySum
          (List.map (fun v => v * v)
            (if decide ((cur✝ % 2 = 1 ∧ cur✝ > 0) ∧ (!pyStrContainsSubstr (pyStr cur✝) ".") = true) = true then [cur✝]
            else [])) ∧
    ans✝ % 2 =
      ↑((List.filter (fun v => decide ((v % 2 = 1 ∧ v > 0) ∧ (!pyStrContainsSubstr (pyStr v) ".") = true))
                pref✝).length +
            (if decide ((cur✝ % 2 = 1 ∧ cur✝ > 0) ∧ (!pyStrContainsSubstr (pyStr cur✝) ".") = true) = true then [cur✝]
              else []).length) %
        2) ∧
  ans✝ ≥ 0
    have hg := ‹(((_:Int) % 2 = 1 ∧ (_:Int) > 0) ∧
      (!PastaLean.pyStrContainsSubstr (PastaLean.pyStr (_:Int)) ".") = true)›vc1.step.isTruelst:List ℤpref✝:List ℤcur✝:ℤsuff✝:List ℤh✝²:lst = pref✝ ++ cur✝ :: suff✝b✝:ℤans✝:ℤ := b✝ +ₚ cur✝ ^ₚ 2h✝¹:(cur✝ % 2 = 1 ∧ cur✝ > 0) ∧ (!pyStrContainsSubstr (pyStr cur✝) ".") = trueh✝:(b✝ =
      pySum
        (List.map (fun v => v * v)
          (List.filter (fun v => decide ((v % 2 = 1 ∧ v > 0) ∧ (!pyStrContainsSubstr (pyStr v) ".") = true)) pref✝)) ∧
    b✝ % 2 =
      ↑(List.filter (fun v => decide ((v % 2 = 1 ∧ v > 0) ∧ (!pyStrContainsSubstr (pyStr v) ".") = true))
              pref✝).length %
        2) ∧
  b✝ ≥ 0hpos:b✝ ≥ 0hsum:b✝ =
  pySum
    (List.map (fun v => v * v)
      (List.filter (fun v => decide ((v % 2 = 1 ∧ v > 0) ∧ (!pyStrContainsSubstr (pyStr v) ".") = true)) pref✝))hpar:b✝ % 2 =
  ↑(List.filter (fun v => decide ((v % 2 = 1 ∧ v > 0) ∧ (!pyStrContainsSubstr (pyStr v) ".") = true)) pref✝).length % 2hg:(cur✝ % 2 = 1 ∧ cur✝ > 0) ∧ (!pyStrContainsSubstr (pyStr cur✝) ".") = true⊢ (ans✝ =
      pySum
          (List.map (fun v => v * v)
            (List.filter (fun v => decide ((v % 2 = 1 ∧ v > 0) ∧ (!pyStrContainsSubstr (pyStr v) ".") = true)) pref✝)) +
        pySum
          (List.map (fun v => v * v)
            (if decide ((cur✝ % 2 = 1 ∧ cur✝ > 0) ∧ (!pyStrContainsSubstr (pyStr cur✝) ".") = true) = true then [cur✝]
            else [])) ∧
    ans✝ % 2 =
      ↑((List.filter (fun v => decide ((v % 2 = 1 ∧ v > 0) ∧ (!pyStrContainsSubstr (pyStr v) ".") = true))
                pref✝).length +
            (if decide ((cur✝ % 2 = 1 ∧ cur✝ > 0) ∧ (!pyStrContainsSubstr (pyStr cur✝) ".") = true) = true then [cur✝]
              else []).length) %
        2) ∧
  ans✝ ≥ 0
    have hsq := sq_odd_emod_two hg.1.1vc1.step.isTruelst:List ℤpref✝:List ℤcur✝:ℤsuff✝:List ℤh✝²:lst = pref✝ ++ cur✝ :: suff✝b✝:ℤans✝:ℤ := b✝ +ₚ cur✝ ^ₚ 2h✝¹:(cur✝ % 2 = 1 ∧ cur✝ > 0) ∧ (!pyStrContainsSubstr (pyStr cur✝) ".") = trueh✝:(b✝ =
      pySum
        (List.map (fun v => v * v)
          (List.filter (fun v => decide ((v % 2 = 1 ∧ v > 0) ∧ (!pyStrContainsSubstr (pyStr v) ".") = true)) pref✝)) ∧
    b✝ % 2 =
      ↑(List.filter (fun v => decide ((v % 2 = 1 ∧ v > 0) ∧ (!pyStrContainsSubstr (pyStr v) ".") = true))
              pref✝).length %
        2) ∧
  b✝ ≥ 0hpos:b✝ ≥ 0hsum:b✝ =
  pySum
    (List.map (fun v => v * v)
      (List.filter (fun v => decide ((v % 2 = 1 ∧ v > 0) ∧ (!pyStrContainsSubstr (pyStr v) ".") = true)) pref✝))hpar:b✝ % 2 =
  ↑(List.filter (fun v => decide ((v % 2 = 1 ∧ v > 0) ∧ (!pyStrContainsSubstr (pyStr v) ".") = true)) pref✝).length % 2hg:(cur✝ % 2 = 1 ∧ cur✝ > 0) ∧ (!pyStrContainsSubstr (pyStr cur✝) ".") = truehsq:cur✝ * cur✝ % 2 = 1⊢ (ans✝ =
      pySum
          (List.map (fun v => v * v)
            (List.filter (fun v => decide ((v % 2 = 1 ∧ v > 0) ∧ (!pyStrContainsSubstr (pyStr v) ".") = true)) pref✝)) +
        pySum
          (List.map (fun v => v * v)
            (if decide ((cur✝ % 2 = 1 ∧ cur✝ > 0) ∧ (!pyStrContainsSubstr (pyStr cur✝) ".") = true) = true then [cur✝]
            else [])) ∧
    ans✝ % 2 =
      ↑((List.filter (fun v => decide ((v % 2 = 1 ∧ v > 0) ∧ (!pyStrContainsSubstr (pyStr v) ".") = true))
                pref✝).length +
            (if decide ((cur✝ % 2 = 1 ∧ cur✝ > 0) ∧ (!pyStrContainsSubstr (pyStr cur✝) ".") = true) = true then [cur✝]
              else []).length) %
        2) ∧
  ans✝ ≥ 0
    simp (config := { zetaDelta := true }) only [decide_eq_true_eq, hg, and_self, true_and,
      and_true, if_true, List.map_cons, List.map_nil, pySum_int_singleton, List.length_cons,
      List.length_nil, pyHPow_two, pow_two,
      show ∀ x y : Int, x +ₚ y = x + y from fun _ _ => rfl,
      show ∀ x y : Int, x *ₚ y = x * y from fun _ _ => rfl] at *vc1.step.isTruelst:List ℤpref✝:List ℤcur✝:ℤsuff✝:List ℤh✝²:lst = pref✝ ++ cur✝ :: suff✝b✝:ℤans✝:ℤ := b✝ +ₚ cur✝ ^ₚ 2h✝¹:(b✝ =
      pySum
        (List.map (fun v => v * v)
          (List.filter (fun v => decide ((v % 2 = 1 ∧ v > 0) ∧ (!pyStrContainsSubstr (pyStr v) ".") = true)) pref✝)) ∧
    b✝ % 2 =
      ↑(List.filter (fun v => decide ((v % 2 = 1 ∧ v > 0) ∧ (!pyStrContainsSubstr (pyStr v) ".") = true))
              pref✝).length %
        2) ∧
  b✝ ≥ 0hpos:b✝ ≥ 0hsum:b✝ =
  pySum
    (List.map (fun v => v * v)
      (List.filter (fun v => decide ((v % 2 = 1 ∧ v > 0) ∧ (!pyStrContainsSubstr (pyStr v) ".") = true)) pref✝))hpar:b✝ % 2 =
  ↑(List.filter (fun v => decide ((v % 2 = 1 ∧ v > 0) ∧ (!pyStrContainsSubstr (pyStr v) ".") = true)) pref✝).length % 2hsq:cur✝ * cur✝ % 2 = 1h✝:Truehg:True⊢ (b✝ + cur✝ * cur✝ =
      pySum
          (List.map (fun v => v * v)
            (List.filter (fun v => decide ((v % 2 = 1 ∧ v > 0) ∧ (!pyStrContainsSubstr (pyStr v) ".") = true)) pref✝)) +
        cur✝ * cur✝ ∧
    (b✝ + cur✝ * cur✝) % 2 =
      ↑((List.filter (fun v => decide ((v % 2 = 1 ∧ v > 0) ∧ (!pyStrContainsSubstr (pyStr v) ".") = true))
                pref✝).length +
            (0 + 1)) %
        2) ∧
  b✝ + cur✝ * cur✝ ≥ 0
    refine ⟨⟨bylst:List ℤpref✝:List ℤcur✝:ℤsuff✝:List ℤh✝²:lst = pref✝ ++ cur✝ :: suff✝b✝:ℤans✝:ℤ := b✝ +ₚ cur✝ ^ₚ 2h✝¹:(b✝ =
      pySum
        (List.map (fun v => v * v)
          (List.filter (fun v => decide ((v % 2 = 1 ∧ v > 0) ∧ (!pyStrContainsSubstr (pyStr v) ".") = true)) pref✝)) ∧
    b✝ % 2 =
      ↑(List.filter (fun v => decide ((v % 2 = 1 ∧ v > 0) ∧ (!pyStrContainsSubstr (pyStr v) ".") = true))
              pref✝).length %
        2) ∧
  b✝ ≥ 0hpos:b✝ ≥ 0hsum:b✝ =
  pySum
    (List.map (fun v => v * v)
      (List.filter (fun v => decide ((v % 2 = 1 ∧ v > 0) ∧ (!pyStrContainsSubstr (pyStr v) ".") = true)) pref✝))hpar:b✝ % 2 =
  ↑(List.filter (fun v => decide ((v % 2 = 1 ∧ v > 0) ∧ (!pyStrContainsSubstr (pyStr v) ".") = true)) pref✝).length % 2hsq:cur✝ * cur✝ % 2 = 1h✝:Truehg:True⊢ b✝ + cur✝ * cur✝ =
  pySum
      (List.map (fun v => v * v)
        (List.filter (fun v => decide ((v % 2 = 1 ∧ v > 0) ∧ (!pyStrContainsSubstr (pyStr v) ".") = true)) pref✝)) +
    cur✝ * cur✝ omegaAll goals completed! 🐙, bylst:List ℤpref✝:List ℤcur✝:ℤsuff✝:List ℤh✝²:lst = pref✝ ++ cur✝ :: suff✝b✝:ℤans✝:ℤ := b✝ +ₚ cur✝ ^ₚ 2h✝¹:(b✝ =
      pySum
        (List.map (fun v => v * v)
          (List.filter (fun v => decide ((v % 2 = 1 ∧ v > 0) ∧ (!pyStrContainsSubstr (pyStr v) ".") = true)) pref✝)) ∧
    b✝ % 2 =
      ↑(List.filter (fun v => decide ((v % 2 = 1 ∧ v > 0) ∧ (!pyStrContainsSubstr (pyStr v) ".") = true))
              pref✝).length %
        2) ∧
  b✝ ≥ 0hpos:b✝ ≥ 0hsum:b✝ =
  pySum
    (List.map (fun v => v * v)
      (List.filter (fun v => decide ((v % 2 = 1 ∧ v > 0) ∧ (!pyStrContainsSubstr (pyStr v) ".") = true)) pref✝))hpar:b✝ % 2 =
  ↑(List.filter (fun v => decide ((v % 2 = 1 ∧ v > 0) ∧ (!pyStrContainsSubstr (pyStr v) ".") = true)) pref✝).length % 2hsq:cur✝ * cur✝ % 2 = 1h✝:Truehg:True⊢ (b✝ + cur✝ * cur✝) % 2 =
  ↑((List.filter (fun v => decide ((v % 2 = 1 ∧ v > 0) ∧ (!pyStrContainsSubstr (pyStr v) ".") = true)) pref✝).length +
        (0 + 1)) %
    2 omegaAll goals completed! 🐙⟩, bylst:List ℤpref✝:List ℤcur✝:ℤsuff✝:List ℤh✝²:lst = pref✝ ++ cur✝ :: suff✝b✝:ℤans✝:ℤ := b✝ +ₚ cur✝ ^ₚ 2h✝¹:(b✝ =
      pySum
        (List.map (fun v => v * v)
          (List.filter (fun v => decide ((v % 2 = 1 ∧ v > 0) ∧ (!pyStrContainsSubstr (pyStr v) ".") = true)) pref✝)) ∧
    b✝ % 2 =
      ↑(List.filter (fun v => decide ((v % 2 = 1 ∧ v > 0) ∧ (!pyStrContainsSubstr (pyStr v) ".") = true))
              pref✝).length %
        2) ∧
  b✝ ≥ 0hpos:b✝ ≥ 0hsum:b✝ =
  pySum
    (List.map (fun v => v * v)
      (List.filter (fun v => decide ((v % 2 = 1 ∧ v > 0) ∧ (!pyStrContainsSubstr (pyStr v) ".") = true)) pref✝))hpar:b✝ % 2 =
  ↑(List.filter (fun v => decide ((v % 2 = 1 ∧ v > 0) ∧ (!pyStrContainsSubstr (pyStr v) ".") = true)) pref✝).length % 2hsq:cur✝ * cur✝ % 2 = 1h✝:Truehg:True⊢ b✝ + cur✝ * cur✝ ≥ 0 nlinarith [hpos]All goals completed! 🐙⟩
  ·vc2.step.isFalselst:List ℤpref✝:List ℤcur✝:ℤsuff✝:List ℤh✝²:lst = pref✝ ++ cur✝ :: suff✝b✝:ℤh✝¹:¬((cur✝ % 2 = 1 ∧ cur✝ > 0) ∧ (!pyStrContainsSubstr (pyStr cur✝) ".") = true)h✝:(b✝ =
      pySum
        (List.map (fun v => v * v)
          (List.filter (fun v => decide ((v % 2 = 1 ∧ v > 0) ∧ (!pyStrContainsSubstr (pyStr v) ".") = true)) pref✝)) ∧
    b✝ % 2 =
      ↑(List.filter (fun v => decide ((v % 2 = 1 ∧ v > 0) ∧ (!pyStrContainsSubstr (pyStr v) ".") = true))
              pref✝).length %
        2) ∧
  b✝ ≥ 0⊢ (b✝ =
      pySum
          (List.map (fun v => v * v)
            (List.filter (fun v => decide ((v % 2 = 1 ∧ v > 0) ∧ (!pyStrContainsSubstr (pyStr v) ".") = true)) pref✝)) +
        pySum
          (List.map (fun v => v * v)
            (if decide ((cur✝ % 2 = 1 ∧ cur✝ > 0) ∧ (!pyStrContainsSubstr (pyStr cur✝) ".") = true) = true then [cur✝]
            else [])) ∧
    b✝ % 2 =
      ↑((List.filter (fun v => decide ((v % 2 = 1 ∧ v > 0) ∧ (!pyStrContainsSubstr (pyStr v) ".") = true))
                pref✝).length +
            (if decide ((cur✝ % 2 = 1 ∧ cur✝ > 0) ∧ (!pyStrContainsSubstr (pyStr cur✝) ".") = true) = true then [cur✝]
              else []).length) %
        2) ∧
  b✝ ≥ 0 -- vc2.step.isFalse: non-contributing element
    obtain ⟨⟨hsum, hpar⟩, hpos⟩ := ‹(_ = PastaLean.pySum _ ∧ _) ∧ _ ≥ (0:Int)›vc2.step.isFalselst:List ℤpref✝:List ℤcur✝:ℤsuff✝:List ℤh✝²:lst = pref✝ ++ cur✝ :: suff✝b✝:ℤh✝¹:¬((cur✝ % 2 = 1 ∧ cur✝ > 0) ∧ (!pyStrContainsSubstr (pyStr cur✝) ".") = true)h✝:(b✝ =
      pySum
        (List.map (fun v => v * v)
          (List.filter (fun v => decide ((v % 2 = 1 ∧ v > 0) ∧ (!pyStrContainsSubstr (pyStr v) ".") = true)) pref✝)) ∧
    b✝ % 2 =
      ↑(List.filter (fun v => decide ((v % 2 = 1 ∧ v > 0) ∧ (!pyStrContainsSubstr (pyStr v) ".") = true))
              pref✝).length %
        2) ∧
  b✝ ≥ 0hpos:b✝ ≥ 0hsum:b✝ =
  pySum
    (List.map (fun v => v * v)
      (List.filter (fun v => decide ((v % 2 = 1 ∧ v > 0) ∧ (!pyStrContainsSubstr (pyStr v) ".") = true)) pref✝))hpar:b✝ % 2 =
  ↑(List.filter (fun v => decide ((v % 2 = 1 ∧ v > 0) ∧ (!pyStrContainsSubstr (pyStr v) ".") = true)) pref✝).length % 2⊢ (b✝ =
      pySum
          (List.map (fun v => v * v)
            (List.filter (fun v => decide ((v % 2 = 1 ∧ v > 0) ∧ (!pyStrContainsSubstr (pyStr v) ".") = true)) pref✝)) +
        pySum
          (List.map (fun v => v * v)
            (if decide ((cur✝ % 2 = 1 ∧ cur✝ > 0) ∧ (!pyStrContainsSubstr (pyStr cur✝) ".") = true) = true then [cur✝]
            else [])) ∧
    b✝ % 2 =
      ↑((List.filter (fun v => decide ((v % 2 = 1 ∧ v > 0) ∧ (!pyStrContainsSubstr (pyStr v) ".") = true))
                pref✝).length +
            (if decide ((cur✝ % 2 = 1 ∧ cur✝ > 0) ∧ (!pyStrContainsSubstr (pyStr cur✝) ".") = true) = true then [cur✝]
              else []).length) %
        2) ∧
  b✝ ≥ 0
    have hg := ‹¬(((_:Int) % 2 = 1 ∧ (_:Int) > 0) ∧
      (!PastaLean.pyStrContainsSubstr (PastaLean.pyStr (_:Int)) ".") = true)›vc2.step.isFalselst:List ℤpref✝:List ℤcur✝:ℤsuff✝:List ℤh✝²:lst = pref✝ ++ cur✝ :: suff✝b✝:ℤh✝¹:¬((cur✝ % 2 = 1 ∧ cur✝ > 0) ∧ (!pyStrContainsSubstr (pyStr cur✝) ".") = true)h✝:(b✝ =
      pySum
        (List.map (fun v => v * v)
          (List.filter (fun v => decide ((v % 2 = 1 ∧ v > 0) ∧ (!pyStrContainsSubstr (pyStr v) ".") = true)) pref✝)) ∧
    b✝ % 2 =
      ↑(List.filter (fun v => decide ((v % 2 = 1 ∧ v > 0) ∧ (!pyStrContainsSubstr (pyStr v) ".") = true))
              pref✝).length %
        2) ∧
  b✝ ≥ 0hpos:b✝ ≥ 0hsum:b✝ =
  pySum
    (List.map (fun v => v * v)
      (List.filter (fun v => decide ((v % 2 = 1 ∧ v > 0) ∧ (!pyStrContainsSubstr (pyStr v) ".") = true)) pref✝))hpar:b✝ % 2 =
  ↑(List.filter (fun v => decide ((v % 2 = 1 ∧ v > 0) ∧ (!pyStrContainsSubstr (pyStr v) ".") = true)) pref✝).length % 2hg:¬((cur✝ % 2 = 1 ∧ cur✝ > 0) ∧ (!pyStrContainsSubstr (pyStr cur✝) ".") = true)⊢ (b✝ =
      pySum
          (List.map (fun v => v * v)
            (List.filter (fun v => decide ((v % 2 = 1 ∧ v > 0) ∧ (!pyStrContainsSubstr (pyStr v) ".") = true)) pref✝)) +
        pySum
          (List.map (fun v => v * v)
            (if decide ((cur✝ % 2 = 1 ∧ cur✝ > 0) ∧ (!pyStrContainsSubstr (pyStr cur✝) ".") = true) = true then [cur✝]
            else [])) ∧
    b✝ % 2 =
      ↑((List.filter (fun v => decide ((v % 2 = 1 ∧ v > 0) ∧ (!pyStrContainsSubstr (pyStr v) ".") = true))
                pref✝).length +
            (if decide ((cur✝ % 2 = 1 ∧ cur✝ > 0) ∧ (!pyStrContainsSubstr (pyStr cur✝) ".") = true) = true then [cur✝]
              else []).length) %
        2) ∧
  b✝ ≥ 0
    simp (config := { zetaDelta := true }) only [decide_eq_true_eq, hg, and_false, false_and,
      if_false, List.append_nil, List.map_nil, pySum_int_nil, add_zero, List.length_nil,
      Nat.add_zero] at *vc2.step.isFalselst:List ℤpref✝:List ℤcur✝:ℤsuff✝:List ℤh✝²:lst = pref✝ ++ cur✝ :: suff✝b✝:ℤh✝¹:(b✝ =
      pySum
        (List.map (fun v => v * v)
          (List.filter (fun v => decide ((v % 2 = 1 ∧ v > 0) ∧ (!pyStrContainsSubstr (pyStr v) ".") = true)) pref✝)) ∧
    b✝ % 2 =
      ↑(List.filter (fun v => decide ((v % 2 = 1 ∧ v > 0) ∧ (!pyStrContainsSubstr (pyStr v) ".") = true))
              pref✝).length %
        2) ∧
  b✝ ≥ 0hpos:b✝ ≥ 0hsum:b✝ =
  pySum
    (List.map (fun v => v * v)
      (List.filter (fun v => decide ((v % 2 = 1 ∧ v > 0) ∧ (!pyStrContainsSubstr (pyStr v) ".") = true)) pref✝))hpar:b✝ % 2 =
  ↑(List.filter (fun v => decide ((v % 2 = 1 ∧ v > 0) ∧ (!pyStrContainsSubstr (pyStr v) ".") = true)) pref✝).length % 2h✝:¬Falsehg:¬False⊢ (b✝ =
      pySum
        (List.map (fun v => v * v)
          (List.filter (fun v => decide ((v % 2 = 1 ∧ v > 0) ∧ (!pyStrContainsSubstr (pyStr v) ".") = true)) pref✝)) ∧
    b✝ % 2 =
      ↑(List.filter (fun v => decide ((v % 2 = 1 ∧ v > 0) ∧ (!pyStrContainsSubstr (pyStr v) ".") = true))
              pref✝).length %
        2) ∧
  b✝ ≥ 0
    exact ⟨⟨hsum, hpar⟩, hpos⟩All goals completed! 🐙

theorem double_the_difference_correct :
    ∀ (lst : List Int),
      let ans := (double_the_difference lst).run;
      (ans =
            PastaLean.pySum
              ((List.filter
                    (fun v =>
                      (v %ₚ (2 : Int) = (1 : Int) ∧ v > (0 : Int)) ∧
                        !(PastaLean.pyStrContainsSubstr (PastaLean.pyStr v) "."))
                    (PastaLean.pyIter lst)).map
                fun v => v *ₚ v) ∧
          ans %ₚ (2 : Int) =
            PastaLean.pyLen
                ((List.filter
                      (fun v =>
                        (v %ₚ (2 : Int) = (1 : Int) ∧ v > (0 : Int)) ∧
                          !(PastaLean.pyStrContainsSubstr (PastaLean.pyStr v) "."))
                      (PastaLean.pyIter lst)).map
                  fun v => v) %ₚ
              (2 : Int)) ∧
        ans ≥ (0 : Int) :=
  by⊢ ∀ (lst : List ℤ),
  let ans := (double_the_difference lst).run;
  (ans =
        pySum
          (List.map (fun v => v *ₚ v)
            (List.filter (fun v => decide ((v %ₚ 2 = 1 ∧ v > 0) ∧ (!pyStrContainsSubstr (pyStr v) ".") = true))
              (pyIter lst))) ∧
      ans %ₚ 2 =
        pyLen
            (List.map (fun v => v)
              (List.filter (fun v => decide ((v %ₚ 2 = 1 ∧ v > 0) ∧ (!pyStrContainsSubstr (pyStr v) ".") = true))
                (pyIter lst))) %ₚ
          2) ∧
    ans ≥ 0
  intro lstlst:List ℤ⊢ let ans := (double_the_difference lst).run;
(ans =
      pySum
        (List.map (fun v => v *ₚ v)
          (List.filter (fun v => decide ((v %ₚ 2 = 1 ∧ v > 0) ∧ (!pyStrContainsSubstr (pyStr v) ".") = true))
            (pyIter lst))) ∧
    ans %ₚ 2 =
      pyLen
          (List.map (fun v => v)
            (List.filter (fun v => decide ((v %ₚ 2 = 1 ∧ v > 0) ∧ (!pyStrContainsSubstr (pyStr v) ".") = true))
              (pyIter lst))) %ₚ
        2) ∧
  ans ≥ 0
  exact double_the_difference_spec True.introAll goals completed! 🐙