import Std.Tactic.Do

open Std.Do

set_option mvcgen.warning false

abbrev gns : SVal ((List Nat)::[]) (List Nat) := fun s => SVal.pure s

noncomputable def setZeroHead : StateM (List Nat) Unit := do
  modify fun _ => [1, 0, 1, 2, 3, 4, 5]
  pure ()
  modify fun s => s.tail
  pure ()

theorem setZeroHead_spec :
   ⦃⌜True⌝⦄
   setZeroHead
   ⦃⇓ _ => ⌜∃ ns', #gns = 0 :: ns'⌝⦄ := by
  mvcgen [setZeroHead]
  -- Goal:
  --
  -- s✝ : List Nat
  -- ⊢ 
  -- h✝ : ⌜True⌝ s✝
  -- ⊢ₛ
  -- have t := (PUnit.unit, [1, 0, 1, 2, 3, 4, 5]);
  -- (fun a =>
  --       wp⟦do
  --           pure ()
  --           MonadStateOf.modifyGet fun s => (PUnit.unit, s.tail)
  --           pure ()⟧
  --         ⇓x => ⌜∃ ns', #gns tuple = 0 :: ns'⌝,
  --       (⇓x => ⌜∃ ns', #gns tuple = 0 :: ns'⌝).snd).fst
  --   t.fst t.snd
  mintro t
  mvcgen
  mintro t
  mvcgen
  mleave
  exists t.2.tail