feat: Rename Std.List.Zipper to List.Cursor (#9911)
This PR renames `Std.List.Zipper` to `List.Cursor`, with slight changes to the implementation (no `reverse`) and use in loop specification lemmas.
This commit is contained in:
Sebastian Graf
GitHub
parent
535435955b
commit
0c39a50337
6 changed files with 164 additions and 144 deletions
|
|
@ -1084,6 +1084,12 @@ theorem getLast?_tail {l : List α} : (tail l).getLast? = if l.length = 1 then n
|
|||
rw [if_neg]
|
||||
rintro ⟨⟩
|
||||
|
||||
@[simp, grind =]
|
||||
theorem cons_head_tail (h : l ≠ []) : l.head h :: l.tail = l := by
|
||||
induction l with
|
||||
| nil => contradiction
|
||||
| cons ih => simp_all
|
||||
|
||||
/-! ## Basic operations -/
|
||||
|
||||
/-! ### map -/
|
||||
|
|
|
|||
|
|
@ -31,6 +31,35 @@ end Std.Range
|
|||
|
||||
namespace List
|
||||
|
||||
@[ext]
|
||||
structure Cursor {α : Type u} (l : List α) : Type u where
|
||||
«prefix» : List α
|
||||
suffix : List α
|
||||
property : «prefix» ++ suffix = l
|
||||
|
||||
def Cursor.at (l : List α) (n : Nat) : Cursor l := ⟨l.take n, l.drop n, by simp⟩
|
||||
abbrev Cursor.begin (l : List α) : Cursor l := .at l 0
|
||||
abbrev Cursor.end (l : List α) : Cursor l := .at l l.length
|
||||
|
||||
def Cursor.current {α} {l : List α} (c : Cursor l) (h : 0 < c.suffix.length := by get_elem_tactic) : α :=
|
||||
c.suffix[0]'(by simp [h])
|
||||
|
||||
def Cursor.tail (s : Cursor l) (h : 0 < s.suffix.length := by get_elem_tactic) : Cursor l :=
|
||||
{ «prefix» := s.prefix ++ [s.current]
|
||||
, suffix := s.suffix.tail
|
||||
, property := by
|
||||
have : s.suffix ≠ [] := by simp only [List.ne_nil_iff_length_pos, h]
|
||||
simp [current, ←List.head_eq_getElem this, s.property] }
|
||||
|
||||
@[simp, grind =] theorem Cursor.prefix_at (l : List α) : (Cursor.at l n).prefix = l.take n := rfl
|
||||
@[simp, grind =] theorem Cursor.suffix_at (l : List α) : (Cursor.at l n).suffix = l.drop n := rfl
|
||||
@[simp, grind =] theorem Cursor.current_at (l : List α) (h : n < l.length) :
|
||||
(Cursor.at l n).current (by simpa using Nat.sub_lt_sub_right (Nat.le_refl n) h) = l[n] := by
|
||||
induction n with simp_all [Cursor.current]
|
||||
@[simp, grind =] theorem Cursor.tail_at (l : List α) (h : n < l.length) :
|
||||
(Cursor.at l n).tail (by simpa using Nat.sub_lt_sub_right (Nat.le_refl n) h) = Cursor.at l (n + 1) := by
|
||||
simp [Cursor.tail, Cursor.at, Cursor.current]
|
||||
|
||||
@[grind →]
|
||||
theorem eq_of_range'_eq_append_cons (h : range' s n step = xs ++ cur :: ys) :
|
||||
cur = s + step * xs.length := by
|
||||
|
|
@ -71,24 +100,6 @@ theorem lt_of_range'_eq_append_cons (h : range' s n step = xs ++ i :: ys) (hstep
|
|||
|
||||
end List
|
||||
|
||||
namespace Std.List
|
||||
|
||||
@[ext]
|
||||
structure Zipper {α : Type u} (l : List α) : Type u where
|
||||
rpref : List α
|
||||
suff : List α
|
||||
property : rpref.reverse ++ suff = l
|
||||
|
||||
@[simp]
|
||||
abbrev Zipper.pref {α} {l : List α} (s : List.Zipper l) : List α := s.rpref.reverse
|
||||
|
||||
abbrev Zipper.begin (l : List α) : Zipper l := ⟨[],l,rfl⟩
|
||||
abbrev Zipper.end (l : List α) : Zipper l := ⟨l.reverse,[],by simp⟩
|
||||
abbrev Zipper.tail (s : Zipper l) (h : s.suff = hd::tl) : Zipper l :=
|
||||
{ rpref := hd::s.rpref, suff := tl, property := by simp [s.property, ←h] }
|
||||
|
||||
end Std.List
|
||||
|
||||
namespace Std.Do
|
||||
|
||||
-- We override the `Triple` notation in `Std.Do.Triple.Basic` just in this module.
|
||||
|
|
@ -339,7 +350,7 @@ theorem Spec.tryCatch_ExceptT_lift [WP m ps] [Monad m] [MonadExceptOf ε m] (Q :
|
|||
The type of loop invariants used by the specifications of `for ... in ...` loops.
|
||||
A loop invariant is a `PostCond` that takes as parameters
|
||||
|
||||
* A `List.Zipper xs` representing the iteration state of the loop. It is parameterized by the list
|
||||
* A `List.Cursor xs` representing the iteration state of the loop. It is parameterized by the list
|
||||
of elements `xs` that the `for` loop iterates over.
|
||||
* A state tuple of type `β`, which will be a nesting of `MProd`s representing the elaboration of
|
||||
`let mut` variables and early return.
|
||||
|
|
@ -351,7 +362,7 @@ During the induction step, the invariant holds for a suffix with head element `x
|
|||
After running the loop body, the invariant then holds after shifting `x` to the prefix.
|
||||
-/
|
||||
abbrev Invariant {α : Type u} (xs : List α) (β : Type u) (ps : PostShape) :=
|
||||
PostCond (List.Zipper xs × β) ps
|
||||
PostCond (List.Cursor xs × β) ps
|
||||
|
||||
/--
|
||||
Helper definition for specifying loop invariants for loops with early return.
|
||||
|
|
@ -365,20 +376,20 @@ It is `none` as long as there was no early return and `some r` if the loop retur
|
|||
|
||||
This function allows to specify different invariants for the loop body depending on whether the loop
|
||||
terminated early or not. When there was an early return, the loop has effectively finished, which is
|
||||
encoded by the additional `⌜xs.suff = []⌝` assertion in the invariant. This assertion is vital for
|
||||
encoded by the additional `⌜xs.suffix = []⌝` assertion in the invariant. This assertion is vital for
|
||||
successfully proving the induction step, as it contradicts with the assumption that
|
||||
`xs.suff = x::rest` of the inductive hypothesis at the start of the loop body, meaning that users
|
||||
`xs.suffix = x::rest` of the inductive hypothesis at the start of the loop body, meaning that users
|
||||
won't need to prove anything about the bogus case where the loop has returned early yet takes
|
||||
another iteration of the loop body.
|
||||
-/
|
||||
abbrev Invariant.withEarlyReturn
|
||||
(onContinue : List.Zipper xs → β → Assertion ps)
|
||||
(onContinue : List.Cursor xs → β → Assertion ps)
|
||||
(onReturn : γ → β → Assertion ps)
|
||||
(onExcept : ExceptConds ps := ExceptConds.false) :
|
||||
Invariant xs (MProd (Option γ) β) ps :=
|
||||
⟨fun ⟨xs, x, b⟩ => spred(
|
||||
(⌜x = none⌝ ∧ onContinue xs b)
|
||||
∨ (∃ r, ⌜x = some r⌝ ∧ ⌜xs.suff = []⌝ ∧ onReturn r b)),
|
||||
∨ (∃ r, ⌜x = some r⌝ ∧ ⌜xs.suffix = []⌝ ∧ onReturn r b)),
|
||||
onExcept⟩
|
||||
|
||||
@[spec]
|
||||
|
|
@ -386,32 +397,32 @@ theorem Spec.forIn'_list {α β : Type u}
|
|||
[Monad m] [WPMonad m ps]
|
||||
{xs : List α} {init : β} {f : (a : α) → a ∈ xs → β → m (ForInStep β)}
|
||||
(inv : Invariant xs β ps)
|
||||
(step : ∀ b rpref x (hx : x ∈ xs) suff (h : xs = rpref.reverse ++ x :: suff),
|
||||
⦃inv.1 (⟨rpref, x::suff, by simp [h]⟩, b)}
|
||||
f x hx b
|
||||
(step : ∀ pref cur suff (h : xs = pref ++ cur :: suff) b,
|
||||
⦃inv.1 (⟨pref, cur::suff, h.symm⟩, b)}
|
||||
f cur (by simp [h]) b
|
||||
⦃(fun r => match r with
|
||||
| .yield b' => inv.1 (⟨x::rpref, suff, by simp [h]⟩, b')
|
||||
| .done b' => inv.1 (⟨xs.reverse, [], by simp⟩, b'), inv.2)}) :
|
||||
⦃inv.1 (⟨[], xs, by simp⟩, init)} forIn' xs init f ⦃(fun b => inv.1 (⟨xs.reverse, [], by simp⟩, b), inv.2)} := by
|
||||
suffices h : ∀ rpref suff (h : xs = rpref.reverse ++ suff),
|
||||
⦃inv.1 (⟨rpref, suff, by simp [h]⟩, init)}
|
||||
forIn' (m:=m) suff init (fun a ha => f a (by simp[h,ha]))
|
||||
⦃(fun b => inv.1 (⟨xs.reverse, [], by simp [h]⟩, b), inv.2)}
|
||||
from h [] xs rfl
|
||||
intro rpref suff h
|
||||
induction suff generalizing rpref init
|
||||
case nil => apply Triple.pure; simp [h]
|
||||
| .yield b' => inv.1 (⟨pref ++ [cur], suff, by simp [h]⟩, b')
|
||||
| .done b' => inv.1 (⟨xs, [], by simp⟩, b'), inv.2)}) :
|
||||
⦃inv.1 (⟨[], xs, rfl⟩, init)} forIn' xs init f ⦃(fun b => inv.1 (⟨xs, [], by simp⟩, b), inv.2)} := by
|
||||
suffices h : ∀ c,
|
||||
⦃inv.1 (c, init)}
|
||||
forIn' (m:=m) c.suffix init (fun a ha => f a (by simp [←c.property, ha]))
|
||||
⦃(fun b => inv.1 (⟨xs, [], by simp⟩, b), inv.2)}
|
||||
from h ⟨[], xs, rfl⟩
|
||||
rintro ⟨pref, suff, h⟩
|
||||
induction suff generalizing pref init
|
||||
case nil => apply Triple.pure; simp [←h]
|
||||
case cons x suff ih =>
|
||||
simp only [List.forIn'_cons]
|
||||
apply Triple.bind
|
||||
case hx => exact step init rpref x (by simp[h]) suff h
|
||||
case hx => exact step _ _ _ h.symm init
|
||||
case hf =>
|
||||
intro r
|
||||
split
|
||||
next => apply Triple.pure; simp [h]
|
||||
next => apply Triple.pure; simp
|
||||
next b =>
|
||||
simp
|
||||
have := @ih b (x::rpref) (by simp [h])
|
||||
have := @ih b (pref ++ [x]) (by simp [h])
|
||||
simp at this
|
||||
exact this
|
||||
|
||||
|
|
@ -425,22 +436,22 @@ theorem Spec.forIn'_list_const_inv {α β : Type u}
|
|||
f x hx b
|
||||
⦃(fun r => match r with | .yield b' => inv.1 b' | .done b' => inv.1 b', inv.2)}) :
|
||||
⦃inv.1 init} forIn' xs init f ⦃inv} :=
|
||||
Spec.forIn'_list (fun p => inv.1 p.2, inv.2) (fun b _ x hx _ _ => step x hx b)
|
||||
Spec.forIn'_list (fun p => inv.1 p.2, inv.2) (fun _p c _s h b => step c (by simp [h]) b)
|
||||
|
||||
@[spec]
|
||||
theorem Spec.forIn_list {α β : Type u}
|
||||
[Monad m] [WPMonad m ps]
|
||||
{xs : List α} {init : β} {f : α → β → m (ForInStep β)}
|
||||
(inv : Invariant xs β ps)
|
||||
(step : ∀ b rpref x suff (h : xs = rpref.reverse ++ x :: suff),
|
||||
⦃inv.1 (⟨rpref, x::suff, by simp [h]⟩, b)}
|
||||
f x b
|
||||
(step : ∀ pref cur suff (h : xs = pref ++ cur :: suff) b,
|
||||
⦃inv.1 (⟨pref, cur::suff, h.symm⟩, b)}
|
||||
f cur b
|
||||
⦃(fun r => match r with
|
||||
| .yield b' => inv.1 (⟨x::rpref, suff, by simp [h]⟩, b')
|
||||
| .done b' => inv.1 (⟨xs.reverse, [], by simp⟩, b'), inv.2)}) :
|
||||
⦃inv.1 (⟨[], xs, by simp⟩, init)} forIn xs init f ⦃(fun b => inv.1 (⟨xs.reverse, [], by simp⟩, b), inv.2)} := by
|
||||
| .yield b' => inv.1 (⟨pref ++ [cur], suff, by simp [h]⟩, b')
|
||||
| .done b' => inv.1 (⟨xs, [], by simp⟩, b'), inv.2)}) :
|
||||
⦃inv.1 (⟨[], xs, rfl⟩, init)} forIn xs init f ⦃(fun b => inv.1 (⟨xs, [], by simp⟩, b), inv.2)} := by
|
||||
simp only [← forIn'_eq_forIn]
|
||||
exact Spec.forIn'_list inv (fun b rpref x _ suff h => step b rpref x suff h)
|
||||
exact Spec.forIn'_list inv step
|
||||
|
||||
-- using the postcondition as a constant invariant:
|
||||
theorem Spec.forIn_list_const_inv {α β : Type u}
|
||||
|
|
@ -452,18 +463,18 @@ theorem Spec.forIn_list_const_inv {α β : Type u}
|
|||
f hd b
|
||||
⦃(fun r => match r with | .yield b' => inv.1 b' | .done b' => inv.1 b', inv.2)}) :
|
||||
⦃inv.1 init} forIn xs init f ⦃inv} :=
|
||||
Spec.forIn_list (fun p => inv.1 p.2, inv.2) (fun b _ hd _ _ => step hd b)
|
||||
Spec.forIn_list (fun p => inv.1 p.2, inv.2) (fun _p c _s _h b => step c b)
|
||||
|
||||
@[spec]
|
||||
theorem Spec.foldlM_list {α β : Type u}
|
||||
[Monad m] [WPMonad m ps]
|
||||
{xs : List α} {init : β} {f : β → α → m β}
|
||||
(inv : Invariant xs β ps)
|
||||
(step : ∀ b rpref x suff (h : xs = rpref.reverse ++ x :: suff),
|
||||
⦃inv.1 (⟨rpref, x::suff, by simp [h]⟩, b)}
|
||||
f b x
|
||||
⦃(fun b' => inv.1 (⟨x::rpref, suff, by simp [h]⟩, b'), inv.2)}) :
|
||||
⦃inv.1 (⟨[], xs, by simp⟩, init)} List.foldlM f init xs ⦃(fun b => inv.1 (⟨xs.reverse, [], by simp⟩, b), inv.2)} := by
|
||||
(step : ∀ pref cur suff (h : xs = pref ++ cur :: suff) b,
|
||||
⦃inv.1 (⟨pref, cur::suff, h.symm⟩, b)}
|
||||
f b cur
|
||||
⦃(fun b' => inv.1 (⟨pref ++ [cur], suff, by simp [h]⟩, b'), inv.2)}) :
|
||||
⦃inv.1 (⟨[], xs, rfl⟩, init)} List.foldlM f init xs ⦃(fun b => inv.1 (⟨xs, [], by simp⟩, b), inv.2)} := by
|
||||
have : xs.foldlM f init = forIn xs init (fun a b => .yield <$> f b a) := by
|
||||
simp only [List.forIn_yield_eq_foldlM, id_map']
|
||||
rw[this]
|
||||
|
|
@ -481,35 +492,35 @@ theorem Spec.foldlM_list_const_inv {α β : Type u}
|
|||
f b hd
|
||||
⦃(fun b' => inv.1 b', inv.2)}) :
|
||||
⦃inv.1 init} List.foldlM f init xs ⦃inv} :=
|
||||
Spec.foldlM_list (fun p => inv.1 p.2, inv.2) (fun b _ hd _ _ => step hd b)
|
||||
Spec.foldlM_list (fun p => inv.1 p.2, inv.2) (fun _p c _s _h b => step c b)
|
||||
|
||||
@[spec]
|
||||
theorem Spec.forIn'_range {β : Type} {m : Type → Type v} {ps : PostShape}
|
||||
[Monad m] [WPMonad m ps]
|
||||
{xs : Std.Range} {init : β} {f : (a : Nat) → a ∈ xs → β → m (ForInStep β)}
|
||||
(inv : Invariant xs.toList β ps)
|
||||
(step : ∀ b rpref x (hx : x ∈ xs) suff (h : xs.toList = rpref.reverse ++ x :: suff),
|
||||
⦃inv.1 (⟨rpref, x::suff, by simp [h]⟩, b)}
|
||||
f x hx b
|
||||
(step : ∀ pref cur suff (h : xs.toList = pref ++ cur :: suff) b,
|
||||
⦃inv.1 (⟨pref, cur::suff, h.symm⟩, b)}
|
||||
f cur (by simp [Std.Range.mem_of_mem_range', h]) b
|
||||
⦃(fun r => match r with
|
||||
| .yield b' => inv.1 (⟨x::rpref, suff, by simp [h]⟩, b')
|
||||
| .done b' => inv.1 (⟨xs.toList.reverse, [], by simp⟩, b'), inv.2)}) :
|
||||
⦃inv.1 (⟨[], xs.toList, by simp⟩, init)} forIn' xs init f ⦃(fun b => inv.1 (⟨xs.toList.reverse, [], by simp⟩, b), inv.2)} := by
|
||||
| .yield b' => inv.1 (⟨pref ++ [cur], suff, by simp [h]⟩, b')
|
||||
| .done b' => inv.1 (⟨xs.toList, [], by simp⟩, b'), inv.2)}) :
|
||||
⦃inv.1 (⟨[], xs.toList, rfl⟩, init)} forIn' xs init f ⦃(fun b => inv.1 (⟨xs.toList, [], by simp⟩, b), inv.2)} := by
|
||||
simp only [Std.Range.forIn'_eq_forIn'_range', Std.Range.size, Std.Range.size.eq_1]
|
||||
apply Spec.forIn'_list inv (fun b rpref x hx suff h => step b rpref x (Std.Range.mem_of_mem_range' hx) suff h)
|
||||
apply Spec.forIn'_list inv (fun c hcur b => step c hcur b)
|
||||
|
||||
@[spec]
|
||||
theorem Spec.forIn_range {β : Type} {m : Type → Type v} {ps : PostShape}
|
||||
[Monad m] [WPMonad m ps]
|
||||
{xs : Std.Range} {init : β} {f : Nat → β → m (ForInStep β)}
|
||||
(inv : Invariant xs.toList β ps)
|
||||
(step : ∀ b rpref x suff (h : xs.toList = rpref.reverse ++ x :: suff),
|
||||
⦃inv.1 (⟨rpref, x::suff, by simp [h]⟩, b)}
|
||||
f x b
|
||||
(step : ∀ pref cur suff (h : xs.toList = pref ++ cur :: suff) b,
|
||||
⦃inv.1 (⟨pref, cur::suff, h.symm⟩, b)}
|
||||
f cur b
|
||||
⦃(fun r => match r with
|
||||
| .yield b' => inv.1 (⟨x::rpref, suff, by simp [h]⟩, b')
|
||||
| .done b' => inv.1 (⟨xs.toList.reverse, [], by simp⟩, b'), inv.2)}) :
|
||||
⦃inv.1 (⟨[], xs.toList, by simp⟩, init)} forIn xs init f ⦃(fun b => inv.1 (⟨xs.toList.reverse, [], by simp⟩, b), inv.2)} := by
|
||||
| .yield b' => inv.1 (⟨pref ++ [cur], suff, by simp [h]⟩, b')
|
||||
| .done b' => inv.1 (⟨xs.toList, [], by simp⟩, b'), inv.2)}) :
|
||||
⦃inv.1 (⟨[], xs.toList, rfl⟩, init)} forIn xs init f ⦃(fun b => inv.1 (⟨xs.toList, [], by simp⟩, b), inv.2)} := by
|
||||
simp only [Std.Range.forIn_eq_forIn_range', Std.Range.size]
|
||||
apply Spec.forIn_list inv step
|
||||
|
||||
|
|
@ -523,15 +534,15 @@ theorem Spec.forIn'_prange {α β : Type u}
|
|||
[LawfulUpwardEnumerableLowerBound sl α] [LawfulUpwardEnumerableUpperBound su α]
|
||||
{xs : PRange ⟨sl, su⟩ α} {init : β} {f : (a : α) → a ∈ xs → β → m (ForInStep β)}
|
||||
(inv : Invariant xs.toList β ps)
|
||||
(step : ∀ b rpref x (hx : x ∈ xs) suff (h : xs.toList = rpref.reverse ++ x :: suff),
|
||||
⦃inv.1 (⟨rpref, x::suff, by simp [h]⟩, b)}
|
||||
f x hx b
|
||||
(step : ∀ pref cur suff (h : xs.toList = pref ++ cur :: suff) b,
|
||||
⦃inv.1 (⟨pref, cur::suff, h.symm⟩, b)}
|
||||
f cur (by simp [←mem_toList_iff_mem, h]) b
|
||||
⦃(fun r => match r with
|
||||
| .yield b' => inv.1 (⟨x::rpref, suff, by simp [h]⟩, b')
|
||||
| .done b' => inv.1 (⟨xs.toList.reverse, [], by simp⟩, b'), inv.2)}) :
|
||||
⦃inv.1 (⟨[], xs.toList, by simp⟩, init)} forIn' xs init f ⦃(fun b => inv.1 (⟨xs.toList.reverse, [], by simp⟩, b), inv.2)} := by
|
||||
| .yield b' => inv.1 (⟨pref ++ [cur], suff, by simp [h]⟩, b')
|
||||
| .done b' => inv.1 (⟨xs.toList, [], by simp⟩, b'), inv.2)}) :
|
||||
⦃inv.1 (⟨[], xs.toList, rfl⟩, init)} forIn' xs init f ⦃(fun b => inv.1 (⟨xs.toList, [], by simp⟩, b), inv.2)} := by
|
||||
simp only [forIn'_eq_forIn'_toList]
|
||||
apply Spec.forIn'_list inv (fun b rpref x hx suff h => step b rpref x (mem_toList_iff_mem.mp hx) suff h)
|
||||
apply Spec.forIn'_list inv step
|
||||
|
||||
open Std.PRange in
|
||||
@[spec]
|
||||
|
|
@ -543,44 +554,44 @@ theorem Spec.forIn_prange {α β : Type u}
|
|||
[LawfulUpwardEnumerableLowerBound sl α] [LawfulUpwardEnumerableUpperBound su α]
|
||||
{xs : PRange ⟨sl, su⟩ α} {init : β} {f : α → β → m (ForInStep β)}
|
||||
(inv : Invariant xs.toList β ps)
|
||||
(step : ∀ b rpref x suff (h : xs.toList = rpref.reverse ++ x :: suff),
|
||||
⦃inv.1 (⟨rpref, x::suff, by simp [h]⟩, b)}
|
||||
f x b
|
||||
(step : ∀ pref cur suff (h : xs.toList = pref ++ cur :: suff) b,
|
||||
⦃inv.1 (⟨pref, cur::suff, h.symm⟩, b)}
|
||||
f cur b
|
||||
⦃(fun r => match r with
|
||||
| .yield b' => inv.1 (⟨x::rpref, suff, by simp [h]⟩, b')
|
||||
| .done b' => inv.1 (⟨xs.toList.reverse, [], by simp⟩, b'), inv.2)}) :
|
||||
⦃inv.1 (⟨[], xs.toList, by simp⟩, init)} forIn xs init f ⦃(fun b => inv.1 (⟨xs.toList.reverse, [], by simp⟩, b), inv.2)} := by
|
||||
| .yield b' => inv.1 (⟨pref ++ [cur], suff, by simp [h]⟩, b')
|
||||
| .done b' => inv.1 (⟨xs.toList, [], by simp⟩, b'), inv.2)}) :
|
||||
⦃inv.1 (⟨[], xs.toList, rfl⟩, init)} forIn xs init f ⦃(fun b => inv.1 (⟨xs.toList, [], by simp⟩, b), inv.2)} := by
|
||||
simp only [forIn]
|
||||
apply Spec.forIn'_prange inv (fun b rpref x _hx suff h => step b rpref x suff h)
|
||||
apply Spec.forIn'_prange inv step
|
||||
|
||||
@[spec]
|
||||
theorem Spec.forIn'_array {α β : Type u}
|
||||
[Monad m] [WPMonad m ps]
|
||||
{xs : Array α} {init : β} {f : (a : α) → a ∈ xs → β → m (ForInStep β)}
|
||||
(inv : Invariant xs.toList β ps)
|
||||
(step : ∀ b rpref x (hx : x ∈ xs) suff (h : xs.toList = rpref.reverse ++ x :: suff),
|
||||
⦃inv.1 (⟨rpref, x::suff, by simp [h]⟩, b)}
|
||||
f x hx b
|
||||
(step : ∀ pref cur suff (h : xs.toList = pref ++ cur :: suff) b,
|
||||
⦃inv.1 (⟨pref, cur::suff, h.symm⟩, b)}
|
||||
f cur (by simp [←Array.mem_toList_iff, h]) b
|
||||
⦃(fun r => match r with
|
||||
| .yield b' => inv.1 (⟨x::rpref, suff, by simp [h]⟩, b')
|
||||
| .done b' => inv.1 (⟨xs.toList.reverse, [], by simp⟩, b'), inv.2)}) :
|
||||
⦃inv.1 (⟨[], xs.toList, by simp⟩, init)} forIn' xs init f ⦃(fun b => inv.1 (⟨xs.toList.reverse, [], by simp⟩, b), inv.2)} := by
|
||||
| .yield b' => inv.1 (⟨pref ++ [cur], suff, by simp [h]⟩, b')
|
||||
| .done b' => inv.1 (⟨xs.toList, [], by simp⟩, b'), inv.2)}) :
|
||||
⦃inv.1 (⟨[], xs.toList, rfl⟩, init)} forIn' xs init f ⦃(fun b => inv.1 (⟨xs.toList, [], by simp⟩, b), inv.2)} := by
|
||||
cases xs
|
||||
simp
|
||||
apply Spec.forIn'_list inv (fun b rpref x hx suff h => step b rpref x (by simp[hx]) suff h)
|
||||
apply Spec.forIn'_list inv step
|
||||
|
||||
@[spec]
|
||||
theorem Spec.forIn_array {α β : Type u}
|
||||
[Monad m] [WPMonad m ps]
|
||||
{xs : Array α} {init : β} {f : α → β → m (ForInStep β)}
|
||||
(inv : Invariant xs.toList β ps)
|
||||
(step : ∀ b rpref x suff (h : xs.toList = rpref.reverse ++ x :: suff),
|
||||
⦃inv.1 (⟨rpref, x::suff, by simp [h]⟩, b)}
|
||||
f x b
|
||||
(step : ∀ pref cur suff (h : xs.toList = pref ++ cur :: suff) b,
|
||||
⦃inv.1 (⟨pref, cur::suff, h.symm⟩, b)}
|
||||
f cur b
|
||||
⦃(fun r => match r with
|
||||
| .yield b' => inv.1 (⟨x::rpref, suff, by simp [h]⟩, b')
|
||||
| .done b' => inv.1 (⟨xs.toList.reverse, [], by simp⟩, b'), inv.2)}) :
|
||||
⦃inv.1 (⟨[], xs.toList, by simp⟩, init)} forIn xs init f ⦃(fun b => inv.1 (⟨xs.toList.reverse, [], by simp⟩, b), inv.2)} := by
|
||||
| .yield b' => inv.1 (⟨pref ++ [cur], suff, by simp [h]⟩, b')
|
||||
| .done b' => inv.1 (⟨xs.toList, [], by simp⟩, b'), inv.2)}) :
|
||||
⦃inv.1 (⟨[], xs.toList, rfl⟩, init)} forIn xs init f ⦃(fun b => inv.1 (⟨xs.toList, [], by simp⟩, b), inv.2)} := by
|
||||
cases xs
|
||||
simp
|
||||
apply Spec.forIn_list inv step
|
||||
|
|
@ -590,11 +601,11 @@ theorem Spec.foldlM_array {α β : Type u}
|
|||
[Monad m] [WPMonad m ps]
|
||||
{xs : Array α} {init : β} {f : β → α → m β}
|
||||
(inv : Invariant xs.toList β ps)
|
||||
(step : ∀ b rpref x suff (h : xs.toList = rpref.reverse ++ x :: suff),
|
||||
⦃inv.1 (⟨rpref, x::suff, by simp [h]⟩, b)}
|
||||
f b x
|
||||
⦃(fun b' => inv.1 (⟨x::rpref, suff, by simp [h]⟩, b'), inv.2)}) :
|
||||
⦃inv.1 (⟨[], xs.toList, by simp⟩, init)} Array.foldlM f init xs ⦃(fun b => inv.1 (⟨xs.toList.reverse, [], by simp⟩, b), inv.2)} := by
|
||||
(step : ∀ pref cur suff (h : xs.toList = pref ++ cur :: suff) b,
|
||||
⦃inv.1 (⟨pref, cur::suff, h.symm⟩, b)}
|
||||
f b cur
|
||||
⦃(fun b' => inv.1 (⟨pref ++ [cur], suff, by simp [h]⟩, b'), inv.2)}) :
|
||||
⦃inv.1 (⟨[], xs.toList, rfl⟩, init)} Array.foldlM f init xs ⦃(fun b => inv.1 (⟨xs.toList, [], by simp⟩, b), inv.2)} := by
|
||||
cases xs
|
||||
simp
|
||||
apply Spec.foldlM_list inv step
|
||||
|
|
|
|||
|
|
@ -160,7 +160,10 @@ macro (name := mleave) "mleave" : tactic =>
|
|||
$(mkIdent ``Std.Do.ExceptConds.entails_false):term,
|
||||
$(mkIdent ``ULift.down_ite):term,
|
||||
$(mkIdent ``ULift.down_dite):term,
|
||||
$(mkIdent ``Std.List.Zipper.pref):term,
|
||||
$(mkIdent ``List.Cursor.prefix_at):term,
|
||||
$(mkIdent ``List.Cursor.suffix_at):term,
|
||||
$(mkIdent ``List.Cursor.current_at):term,
|
||||
$(mkIdent ``List.Cursor.tail_at):term,
|
||||
$(mkIdent ``and_imp):term,
|
||||
$(mkIdent ``and_true):term,
|
||||
$(mkIdent ``dite_eq_ite):term,
|
||||
|
|
|
|||
|
|
@ -152,16 +152,16 @@ theorem sampler_correct {m : Type → Type u} {k h} [Monad m] [WPMonad m ps] :
|
|||
sampler (m:=m) n k h
|
||||
⦃⇓ xs => ⌜xs.toList.Nodup⌝⦄ := by
|
||||
mvcgen -leave [sampler]
|
||||
case inv1 => exact (⇓ (xs, midway) => ⌜Midway.valid midway xs.rpref.length⌝)
|
||||
case vc1 rpref x _ _ _ _ _ _ r _ _ _ =>
|
||||
case inv1 => exact (⇓ (xs, midway) => ⌜Midway.valid midway xs.prefix.length⌝)
|
||||
case vc1 pref cur _ _ _ _ _ _ r _ _ _ =>
|
||||
dsimp
|
||||
mframe
|
||||
rename_i hinv
|
||||
mpure_intro
|
||||
change Midway.valid (next _ x _ r.val) (rpref.length + 1)
|
||||
have : x = rpref.length := sorry -- by grind -- wishful thinking :(
|
||||
simp only [List.length_append, List.length_cons, List.length_nil, Nat.zero_add]
|
||||
have : cur = pref.length := sorry -- by grind -- wishful thinking :(
|
||||
subst this
|
||||
apply Midway.valid_next _ rpref.length _ r.val r.property.1 r.property.2 hinv
|
||||
apply Midway.valid_next _ pref.length _ r.val r.property.1 r.property.2 hinv
|
||||
case vc2 =>
|
||||
mpure_intro
|
||||
exact valid_init
|
||||
|
|
|
|||
|
|
@ -87,7 +87,7 @@ theorem sum_loop_spec :
|
|||
mintro -
|
||||
unfold sum_loop
|
||||
mspec
|
||||
case inv => exact (⇓ (xs, r) => ⌜(∀ x, x ∈ xs.suff → x ≤ 5) ∧ r + xs.suff.length * 5 ≤ 25⌝)
|
||||
case inv => exact (⇓ (xs, r) => ⌜(∀ x ∈ xs.suffix, x ≤ 5) ∧ r + xs.suffix.length * 5 ≤ 25⌝)
|
||||
all_goals simp_all +decide; try omega
|
||||
intros
|
||||
mintro _
|
||||
|
|
@ -136,11 +136,11 @@ theorem mkFreshPair_spec_no_eta :
|
|||
mspec
|
||||
intro _; simp_all
|
||||
|
||||
example : PostCond (Nat × Std.List.Zipper (List.range' 1 3 1)) (PostShape.except Nat (PostShape.arg Nat PostShape.pure)) :=
|
||||
⟨fun (r, xs) s => ⌜r ≤ 4 ∧ s = 4 ∧ r + xs.suff.sum > 4⌝, fun e s => ⌜e = 42 ∧ s = 4⌝, ()⟩
|
||||
example : PostCond (Nat × List.Cursor (List.range' 1 3 1)) (PostShape.except Nat (PostShape.arg Nat PostShape.pure)) :=
|
||||
⟨fun (r, xs) s => ⌜r ≤ 4 ∧ s = 4 ∧ r + xs.suffix.sum > 4⌝, fun e s => ⌜e = 42 ∧ s = 4⌝, ()⟩
|
||||
|
||||
example : PostCond (Nat × Std.List.Zipper (List.range' 1 3 1)) (PostShape.except Nat (PostShape.arg Nat PostShape.pure)) :=
|
||||
post⟨fun (r, xs) s => ⌜r ≤ 4 ∧ s = 4 ∧ r + xs.suff.sum > 4⌝, fun e s => ⌜e = 42 ∧ s = 4⌝⟩
|
||||
example : PostCond (Nat × List.Cursor (List.range' 1 3 1)) (PostShape.except Nat (PostShape.arg Nat PostShape.pure)) :=
|
||||
post⟨fun (r, xs) s => ⌜r ≤ 4 ∧ s = 4 ∧ r + xs.suffix.sum > 4⌝, fun e s => ⌜e = 42 ∧ s = 4⌝⟩
|
||||
|
||||
theorem throwing_loop_spec :
|
||||
⦃fun s => ⌜s = 4⌝⦄
|
||||
|
|
@ -152,7 +152,7 @@ theorem throwing_loop_spec :
|
|||
mspec
|
||||
mspec
|
||||
mspec
|
||||
case inv => exact post⟨fun (xs, r) s => ⌜r ≤ 4 ∧ s = 4 ∧ r + xs.suff.sum > 4⌝, fun e s => ⌜e = 42 ∧ s = 4⌝⟩
|
||||
case inv => exact post⟨fun (xs, r) s => ⌜r ≤ 4 ∧ s = 4 ∧ r + xs.suffix.sum > 4⌝, fun e s => ⌜e = 42 ∧ s = 4⌝⟩
|
||||
case post.success =>
|
||||
mspec
|
||||
mspec
|
||||
|
|
@ -178,7 +178,7 @@ theorem beaking_loop_spec :
|
|||
dsimp only [breaking_loop, get, getThe, instMonadStateOfOfMonadLift, liftM, monadLift]
|
||||
mspec
|
||||
mspec
|
||||
case inv => exact (⇓ (xs, r) s => ⌜(r ≤ 4 ∧ r = xs.rpref.sum ∨ r > 4) ∧ s = 42⌝)
|
||||
case inv => exact (⇓ (xs, r) s => ⌜(r ≤ 4 ∧ r = xs.prefix.sum ∨ r > 4) ∧ s = 42⌝)
|
||||
all_goals simp_all
|
||||
case post => grind
|
||||
case step =>
|
||||
|
|
@ -196,7 +196,7 @@ theorem returning_loop_spec :
|
|||
dsimp only [returning_loop, get, getThe, instMonadStateOfOfMonadLift, liftM, monadLift]
|
||||
mspec
|
||||
mspec
|
||||
case inv => exact (⇓ (xs, r) s => ⌜(r.1 = none ∧ r.2 = xs.rpref.sum ∧ r.2 ≤ 4 ∨ r.1 = some 42 ∧ r.2 > 4) ∧ s = 4⌝)
|
||||
case inv => exact (⇓ (xs, r) s => ⌜(r.1 = none ∧ r.2 = xs.prefix.sum ∧ r.2 ≤ 4 ∨ r.1 = some 42 ∧ r.2 > 4) ∧ s = 4⌝)
|
||||
all_goals simp_all [-SPred.entails_1]
|
||||
case post =>
|
||||
split
|
||||
|
|
@ -235,8 +235,8 @@ theorem fib_triple : ⦃⌜True⌝⦄ fib_impl n ⦃⇓ r => ⌜r = fib_spec n
|
|||
if h : n = 0 then simp [h] else
|
||||
simp only [h, reduceIte]
|
||||
mspec -- Spec.pure
|
||||
mspec Spec.forIn_range (⇓ ⟨xs, a, b⟩ => ⌜a = fib_spec xs.rpref.length ∧ b = fib_spec (xs.rpref.length + 1)⌝) ?step
|
||||
case step => dsimp; intros; mintro _; simp_all
|
||||
mspec Spec.forIn_range (⇓ ⟨xs, a, b⟩ => ⌜a = fib_spec xs.prefix.length ∧ b = fib_spec (xs.prefix.length + 1)⌝) ?step
|
||||
case step => intros; mintro _; simp_all
|
||||
simp_all [Nat.sub_one_add_one]
|
||||
|
||||
theorem fib_triple_cases : ⦃⌜True⌝⦄ fib_impl n ⦃⇓ r => ⌜r = fib_spec n⌝⦄ := by
|
||||
|
|
@ -246,8 +246,8 @@ theorem fib_triple_cases : ⦃⌜True⌝⦄ fib_impl n ⦃⇓ r => ⌜r = fib_sp
|
|||
mintro -
|
||||
simp only [fib_impl, h, reduceIte]
|
||||
mspec
|
||||
mspec Spec.forIn_range (⇓ ⟨xs, a, b⟩ => ⌜a = fib_spec xs.rpref.length ∧ b = fib_spec (xs.rpref.length + 1)⌝) ?step
|
||||
case step => dsimp; intros; mintro _; mspec; mspec; simp_all
|
||||
mspec Spec.forIn_range (⇓ ⟨xs, a, b⟩ => ⌜a = fib_spec xs.prefix.length ∧ b = fib_spec (xs.prefix.length + 1)⌝) ?step
|
||||
case step => intros; mintro _; mspec; mspec; simp_all
|
||||
simp_all [Nat.sub_one_add_one]
|
||||
|
||||
theorem fib_impl_vcs
|
||||
|
|
@ -255,10 +255,10 @@ theorem fib_impl_vcs
|
|||
(I : (n : Nat) → (_ : ¬n = 0) →
|
||||
Invariant [1:n].toList (MProd Nat Nat) PostShape.pure)
|
||||
(ret : ⊢ₛ (Q 0).1 0)
|
||||
(loop_pre : ∀ n (hn : ¬n = 0), ⊢ₛ (I n hn).1 ⟨Std.List.Zipper.begin _, 0, 1⟩)
|
||||
(loop_post : ∀ n (hn : ¬n = 0) r, (I n hn).1 ⟨Std.List.Zipper.end _, r⟩ ⊢ₛ (Q n).1 r.2)
|
||||
(loop_step : ∀ n (hn : ¬n = 0) r rpref x suff (h : [1:n].toList = rpref.reverse ++ x :: suff),
|
||||
(I n hn).1 ⟨⟨rpref, x::suff, by simp[h]⟩, r⟩ ⊢ₛ (I n hn).1 ⟨⟨x::rpref, suff, by simp[h]⟩, r.2, r.1+r.2⟩)
|
||||
(loop_pre : ∀ n (hn : ¬n = 0), ⊢ₛ (I n hn).1 ⟨⟨[], [1:n].toList, rfl⟩, 0, 1⟩)
|
||||
(loop_post : ∀ n (hn : ¬n = 0) r, (I n hn).1 ⟨⟨[1:n].toList, [], by simp⟩, r⟩ ⊢ₛ (Q n).1 r.2)
|
||||
(loop_step : ∀ n (hn : ¬n = 0) r pref cur suff (h : [1:n].toList = pref ++ cur :: suff),
|
||||
(I n hn).1 ⟨⟨pref, cur::suff, by simp[h]⟩, r⟩ ⊢ₛ (I n hn).1 ⟨⟨pref ++ [cur], suff, by simp[h]⟩, r.2, r.1+r.2⟩)
|
||||
: ⊢ₛ wp⟦fib_impl n⟧ (Q n) := by
|
||||
apply fib_impl.fun_cases n _ ?case1 ?case2
|
||||
case case1 => intro h; simp only [fib_impl, h, ↓reduceIte]; mstart; mspec
|
||||
|
|
@ -279,7 +279,7 @@ theorem fib_impl_vcs
|
|||
|
||||
theorem fib_triple_vcs : ⦃⌜True⌝⦄ fib_impl n ⦃⇓ r => ⌜r = fib_spec n⌝⦄ := by
|
||||
apply fib_impl_vcs
|
||||
case I => intro n hn; exact (⇓ ⟨xs, a, b⟩ => ⌜a = fib_spec xs.rpref.length ∧ b = fib_spec (xs.rpref.length + 1)⌝)
|
||||
case I => intro n hn; exact (⇓ ⟨xs, a, b⟩ => ⌜a = fib_spec xs.prefix.length ∧ b = fib_spec (xs.prefix.length + 1)⌝)
|
||||
case ret => mpure_intro; rfl
|
||||
case loop_pre => intros; mpure_intro; trivial
|
||||
case loop_post => simp_all [Nat.sub_one_add_one]
|
||||
|
|
@ -394,14 +394,14 @@ theorem fib_triple : ⦃⌜True⌝⦄ fib_impl n ⦃⇓ r => ⌜r = fib_spec n
|
|||
unfold fib_impl
|
||||
mvcgen
|
||||
case inv1 => exact ⇓ (xs, ⟨a, b⟩) =>
|
||||
⌜a = fib_spec xs.rpref.length ∧ b = fib_spec (xs.rpref.length + 1)⌝
|
||||
⌜a = fib_spec xs.prefix.length ∧ b = fib_spec (xs.prefix.length + 1)⌝
|
||||
all_goals simp_all +zetaDelta [Nat.sub_one_add_one]
|
||||
|
||||
theorem fib_triple_step : ⦃⌜True⌝⦄ fib_impl n ⦃⇓ r => ⌜r = fib_spec n⌝⦄ := by
|
||||
unfold fib_impl
|
||||
mvcgen (stepLimit := some 14) -- 13 still has a wp⟦·⟧
|
||||
case inv1 => exact ⇓ ⟨xs, a, b⟩ =>
|
||||
⌜a = fib_spec xs.rpref.length ∧ b = fib_spec (xs.rpref.length + 1)⌝
|
||||
⌜a = fib_spec xs.prefix.length ∧ b = fib_spec (xs.prefix.length + 1)⌝
|
||||
all_goals simp_all +zetaDelta [Nat.sub_one_add_one]
|
||||
|
||||
attribute [local spec] fib_triple in
|
||||
|
|
@ -419,10 +419,10 @@ theorem fib_impl_vcs
|
|||
(I : (n : Nat) → (_ : ¬n = 0) →
|
||||
Invariant [1:n].toList (MProd Nat Nat) PostShape.pure)
|
||||
(ret : ⊢ₛ (Q 0).1 0)
|
||||
(loop_pre : ∀ n (hn : ¬n = 0), ⊢ₛ (I n hn).1 ⟨Std.List.Zipper.begin _, 0, 1⟩)
|
||||
(loop_post : ∀ n (hn : ¬n = 0) r, (I n hn).1 ⟨Std.List.Zipper.end _, r⟩ ⊢ₛ (Q n).1 r.2)
|
||||
(loop_step : ∀ n (hn : ¬n = 0) r rpref x suff (h : [1:n].toList = rpref.reverse ++ x :: suff),
|
||||
(I n hn).1 ⟨⟨rpref, x::suff, by simp[h]⟩, r⟩ ⊢ₛ (I n hn).1 ⟨⟨x::rpref, suff, by simp[h]⟩, r.2, r.1+r.2⟩)
|
||||
(loop_pre : ∀ n (hn : ¬n = 0), ⊢ₛ (I n hn).1 ⟨⟨[], [1:n].toList, rfl⟩, 0, 1⟩)
|
||||
(loop_post : ∀ n (hn : ¬n = 0) r, (I n hn).1 ⟨⟨[1:n].toList, [], by simp⟩, r⟩ ⊢ₛ (Q n).1 r.2)
|
||||
(loop_step : ∀ n (hn : ¬n = 0) r pref cur suff (h : [1:n].toList = pref ++ cur :: suff),
|
||||
(I n hn).1 ⟨⟨pref, cur::suff, by simp[h]⟩, r⟩ ⊢ₛ (I n hn).1 ⟨⟨pref ++ [cur], suff, by simp[h]⟩, r.2, r.1+r.2⟩)
|
||||
: ⊢ₛ wp⟦fib_impl n⟧ (Q n) := by
|
||||
unfold fib_impl
|
||||
mvcgen
|
||||
|
|
@ -467,7 +467,7 @@ theorem sum_loop_spec :
|
|||
-- cf. `ByHand.sum_loop_spec`
|
||||
mintro -
|
||||
mvcgen [sum_loop]
|
||||
case inv1 => exact (⇓ (xs, r) => ⌜(∀ x, x ∈ xs.suff → x ≤ 5) ∧ r + xs.suff.length * 5 ≤ 25⌝)
|
||||
case inv1 => exact (⇓ (xs, r) => ⌜r + xs.suffix.length * 5 ≤ 25⌝)
|
||||
all_goals simp_all; try grind
|
||||
|
||||
theorem throwing_loop_spec :
|
||||
|
|
@ -476,7 +476,7 @@ theorem throwing_loop_spec :
|
|||
⦃post⟨fun _ _ => ⌜False⌝,
|
||||
fun e s => ⌜e = 42 ∧ s = 4⌝⟩⦄ := by
|
||||
mvcgen [throwing_loop]
|
||||
case inv1 => exact post⟨fun (xs, r) s => ⌜r ≤ 4 ∧ s = 4 ∧ r + xs.suff.sum > 4⌝,
|
||||
case inv1 => exact post⟨fun (xs, r) s => ⌜r ≤ 4 ∧ s = 4 ∧ r + xs.suffix.sum > 4⌝,
|
||||
fun e s => ⌜e = 42 ∧ s = 4⌝⟩
|
||||
all_goals mleave; try (subst_vars; grind)
|
||||
|
||||
|
|
@ -485,7 +485,7 @@ theorem test_loop_break :
|
|||
breaking_loop
|
||||
⦃⇓ r s => ⌜r > 4 ∧ s = 1⌝⦄ := by
|
||||
mvcgen [breaking_loop]
|
||||
case inv1 => exact (⇓ (xs, r) s => ⌜(r ≤ 4 ∧ r = xs.rpref.sum ∨ r > 4) ∧ s = 42⌝)
|
||||
case inv1 => exact (⇓ (xs, r) s => ⌜(r ≤ 4 ∧ r = xs.prefix.sum ∨ r > 4) ∧ s = 42⌝)
|
||||
all_goals mleave; try grind
|
||||
|
||||
theorem test_loop_early_return :
|
||||
|
|
@ -493,7 +493,7 @@ theorem test_loop_early_return :
|
|||
returning_loop
|
||||
⦃⇓ r s => ⌜r = 42 ∧ s = 4⌝⦄ := by
|
||||
mvcgen [returning_loop]
|
||||
case inv1 => exact (⇓ (xs, r) s => ⌜(r.1 = none ∧ r.2 = xs.rpref.sum ∧ r.2 ≤ 4 ∨ r.1 = some 42 ∧ r.2 > 4) ∧ s = 4⌝)
|
||||
case inv1 => exact (⇓ (xs, r) s => ⌜(r.1 = none ∧ r.2 = xs.prefix.sum ∧ r.2 ≤ 4 ∨ r.1 = some 42 ∧ r.2 > 4) ∧ s = 4⌝)
|
||||
all_goals simp_all; try grind
|
||||
|
||||
theorem unfold_to_expose_match_spec :
|
||||
|
|
@ -521,7 +521,7 @@ theorem test_sum :
|
|||
pure (f := Id) x
|
||||
⦃⇓r => ⌜r < 30⌝⦄ := by
|
||||
mvcgen
|
||||
case inv1 => exact (⇓ (xs, r) => ⌜(∀ x, x ∈ xs.suff → x ≤ 5) ∧ r + xs.suff.length * 5 ≤ 25⌝)
|
||||
case inv1 => exact (⇓ (xs, r) => ⌜r + xs.suffix.length * 5 ≤ 25⌝)
|
||||
all_goals simp_all; try grind
|
||||
|
||||
/--
|
||||
|
|
@ -555,7 +555,7 @@ example (p : Nat → Prop) [DecidablePred p] (n : Nat) :
|
|||
case inv1 =>
|
||||
exact Invariant.withEarlyReturn
|
||||
(onReturn := fun ret _ => ⌜ret = false ∧ ¬ ∀ i < n, p i⌝)
|
||||
(onContinue := fun xs _ => ⌜∀ i, i ∈ xs.pref → p i⌝)
|
||||
(onContinue := fun xs _ => ⌜∀ i, i ∈ xs.prefix → p i⌝)
|
||||
all_goals simp_all [-Classical.not_forall]; try grind
|
||||
|
||||
end Automated
|
||||
|
|
@ -704,7 +704,7 @@ def max_and_sum (xs : Array Nat) : Id (Nat × Nat) := do
|
|||
theorem max_and_sum_spec (xs : Array Nat) :
|
||||
⦃⌜∀ i, (h : i < xs.size) → xs[i] ≥ 0⌝⦄ max_and_sum xs ⦃⇓ (m, s) => ⌜s ≤ m * xs.size⌝⦄ := by
|
||||
mvcgen [max_and_sum]
|
||||
case inv1 => exact (⇓ ⟨xs, m, s⟩ => ⌜s ≤ m * xs.rpref.length⌝)
|
||||
case inv1 => exact (⇓ ⟨xs, m, s⟩ => ⌜s ≤ m * xs.prefix.length⌝)
|
||||
all_goals simp_all
|
||||
· rw [Nat.left_distrib]
|
||||
simp +zetaDelta only [Nat.mul_one, Nat.add_le_add_iff_right]
|
||||
|
|
@ -851,20 +851,20 @@ theorem naive_expo_correct (x n : Nat) : naive_expo x n = x^n := by
|
|||
generalize h : naive_expo x n = r
|
||||
apply Id.of_wp_run_eq h
|
||||
mvcgen
|
||||
case inv1 => exact ⇓⟨xs, r⟩ => ⌜r = x^xs.rpref.length⌝
|
||||
case inv1 => exact ⇓⟨xs, r⟩ => ⌜r = x^xs.prefix.length⌝
|
||||
all_goals simp_all [Nat.pow_add_one]
|
||||
|
||||
theorem fast_expo_correct (x n : Nat) : fast_expo x n = x^n := by
|
||||
generalize h : fast_expo x n = r
|
||||
apply Id.of_wp_run_eq h
|
||||
mvcgen
|
||||
case inv1 => exact ⇓⟨xs, e, x', y⟩ => ⌜x' ^ e * y = x ^ n ∧ e ≤ n - xs.rpref.length⌝
|
||||
case inv1 => exact ⇓⟨xs, e, x', y⟩ => ⌜x' ^ e * y = x ^ n ∧ e ≤ n - xs.prefix.length⌝
|
||||
all_goals simp_all
|
||||
case vc1 b _ _ _ _ _ _ _ _ _ _ ih =>
|
||||
case vc1 b _ _ _ _ _ _ ih =>
|
||||
obtain ⟨e, y, x'⟩ := b
|
||||
subst_vars
|
||||
grind
|
||||
case vc2 b _ _ _ _ _ _ _ _ _ _ ih _ =>
|
||||
case vc2 b _ _ _ _ _ _ ih _ =>
|
||||
obtain ⟨e, y, x'⟩ := b
|
||||
simp at *
|
||||
constructor
|
||||
|
|
@ -872,7 +872,7 @@ theorem fast_expo_correct (x n : Nat) : fast_expo x n = x^n := by
|
|||
have : e - 1 + 1 = e := by grind
|
||||
rw [this]
|
||||
· grind
|
||||
case vc3 b _ _ _ _ _ _ _ _ _ _ ih _ =>
|
||||
case vc3 b _ _ _ _ _ _ ih _ =>
|
||||
obtain ⟨e, y, x'⟩ := b
|
||||
simp at *
|
||||
constructor
|
||||
|
|
@ -909,7 +909,7 @@ theorem nodup_correct (l : List Int) : nodup l ↔ l.Nodup := by
|
|||
exact Invariant.withEarlyReturn
|
||||
(onReturn := fun ret seen => ⌜ret = false ∧ ¬l.Nodup⌝)
|
||||
(onContinue := fun traversalState seen =>
|
||||
⌜(∀ x, x ∈ seen ↔ x ∈ traversalState.pref) ∧ traversalState.pref.Nodup⌝)
|
||||
⌜(∀ x, x ∈ seen ↔ x ∈ traversalState.prefix) ∧ traversalState.prefix.Nodup⌝)
|
||||
all_goals mleave; grind
|
||||
|
||||
theorem nodup_correct_directly (l : List Int) : nodup l ↔ l.Nodup := by
|
||||
|
|
|
|||
|
|
@ -75,7 +75,7 @@ theorem pairsSumToZero_correct (l : List Int) : pairsSumToZero l ↔ l.ExistsPai
|
|||
exact Invariant.withEarlyReturn
|
||||
(onReturn := fun r b => ⌜r = true ∧ l.ExistsPair (fun a b => a + b = 0)⌝)
|
||||
(onContinue := fun traversalState seen =>
|
||||
⌜(∀ x, x ∈ seen ↔ x ∈ traversalState.rpref) ∧ ¬traversalState.pref.ExistsPair (fun a b => a + b = 0)⌝)
|
||||
⌜(∀ x, x ∈ seen ↔ x ∈ traversalState.prefix) ∧ ¬traversalState.prefix.ExistsPair (fun a b => a + b = 0)⌝)
|
||||
|
||||
all_goals simp_all <;> grind
|
||||
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue