The Iris Tutorial in Lean

7. Linked Lists🔗

7.1. Introduction🔗

In this chapter, we study several functions on linked lists. To do this, we must first agree on what a linked list is. In HeapLang, we can implement linked lists as chains of pointers. We define this formally with a predicate, which we denote isList. This predicate turns a list of values xs into a predicate describing the structure of the linked list in the heap.

open Iris Iris.BI Iris.HeapLang namespace LinkedLists variable {hlc} {GF : BundledGFunctors} [HeapLangGS hlc GF]

A linked list is either empty — represented by the value none() — or a pointer to a node. A node is a location hd storing a pair (x, l'): the head value x and the rest of the list l'. We capture this as a predicate defined by recursion on the Lean-level list xs of values it represents.

def isList (l : Val) : List Val → IProp GF | [] => iprop% ⌜l = hl_val(none())⌝ | x :: xs => iprop% ∃ hd l', ⌜l = hl_val(some(#(.loc hd)))⌝ ∗ hd ↦ some hl_val((&x, &l')) ∗ isList l' xs

Because isList is defined by pattern matching, the two cases hold definitionally. We record them as proof-mode lemmas, which lets us unfold and refold the predicate during proofs.

theorem isList_nil {l} : isList (GF := GF) l [] ⊣⊢ iprop(⌜l = hl_val(none())⌝) := .rfl theorem isList_cons {l x xs} : isList (GF := GF) l (x :: xs) ⊣⊢ iprop(∃ hd l', ⌜l = hl_val(some(#(.loc hd)))⌝ ∗ hd ↦ some hl_val((&x, &l')) ∗ isList l' xs) := .rfl

Here some(_) / none() are the value-level injections, and #(.loc hd) turns a heap location hd : Loc into a HeapLang value.

7.2. Append🔗

The append function recursively descends l1, updating the links in place. Eventually it reaches the tail none(), where it returns l2.

def append : Val := hl_val% rec append l1 l2 := match l1 with | none() => l2 | some(hd) => let x := fst(!hd); let l1' := snd(!hd); let r := append l1' l2; hd ← (x, r); some(hd)

If l1 and l2 represent the lists xs and ys respectively, then append l1 l2 returns a list representing xs ++ ys.

Following the convention from the specifications chapter, we state the specification as a Hoare triple and use wp_apply at recursive calls.

theorem append_spec (l1 l2 : Val) (xs ys : List Val) : {{ isList (GF := GF) l1 xs ∗ isList l2 ys }} hl(&append &l1 &l2) {{ v, RET v; isList v (xs ++ ys) }} := hlc:HasLCGF:BundledGFunctorsinst✝:HeapLangGS hlc GFl1:Vall2:Valxs:List Valys:List Val⊢ ⊢ ∀ Φ, isList l1 xs ∗ isList l2 ys -∗ (▷ ∀ v, isList v (xs ++ ys) -∗ Φ v) -∗ WP hl(v(&append) v(&l1) v(&l2)) {{ Φ }} hlc:HasLCGF:BundledGFunctorsinst✝:HeapLangGS hlc GFl1:Vall2:Valxs:List Valys:List ValΦ:Val → IProp GF⊢ ∗Hl1 : isList l1 xs ∗Hl2 : isList l2 ys ∗HΦ : ▷ ∀ v, isList v (xs ++ ys) -∗ Φ v ⊢ WP hl(v(&append) v(&l1) v(&l2)) {{ Φ }} hlc:HasLCGF:BundledGFunctorsinst✝:HeapLangGS hlc GFl2:Valys:List Vall1:Valxs:List ValΦ:Val → IProp GF⊢ □IH : ▷ ∀ l1 xs Φ, isList l1 xs -∗ isList l2 ys -∗ (▷ ∀ v, isList v (xs ++ ys) -∗ Φ v) -∗ WP hl(v(&append) v(&l1) v(&l2)) {{ Φ }} ∗Hl1 : isList l1 xs ∗Hl2 : isList l2 ys ∗HΦ : ▷ ∀ v, isList v (xs ++ ys) -∗ Φ v ⊢ WP hl(v(&append) v(&l1) v(&l2)) {{ Φ }} hlc:HasLCGF:BundledGFunctorsinst✝:HeapLangGS hlc GFl2:Valys:List Vall1:Valxs:List ValΦ:Val → IProp GF⊢ □IH : ▷ ∀ l1 xs Φ, isList l1 xs -∗ isList l2 ys -∗ (▷ ∀ v, isList v (xs ++ ys) -∗ Φ v) -∗ WP hl(v(&append) v(&l1) v(&l2)) {{ Φ }} ∗Hl1 : isList l1 xs ∗Hl2 : isList l2 ys ∗HΦ : ▷ ∀ v, isList v (xs ++ ys) -∗ Φ v ⊢ WP hl(v(&append) v(&l1)) {{ v, WP hl(v(&v) v(&l2)) {{ Φ }} }} hlc:HasLCGF:BundledGFunctorsinst✝:HeapLangGS hlc GFl2:Valys:List Vall1:Valxs:List ValΦ:Val → IProp GF⊢ □IH : ∀ l1 xs Φ, isList l1 xs -∗ isList l2 ys -∗ (▷ ∀ v, isList v (xs ++ ys) -∗ Φ v) -∗ WP hl(v(&append) v(&l1) v(&l2)) {{ Φ }} ∗Hl1 : isList l1 xs ∗Hl2 : isList l2 ys ∗HΦ : ∀ v, isList v (xs ++ ys) -∗ Φ v ⊢ WP hl((λ l2, match v(&l1) with | injl(_) => l2 | injr(hd) => let x := fst(!hd); let l1' := snd(!hd); let r := v(&append) l1' l2; hd ← (x, r); injr(hd))) {{ v, WP hl(v(&v) v(&l2)) {{ Φ }} }} cases xs with hlc:HasLCGF:BundledGFunctorsinst✝:HeapLangGS hlc GFl2:Valys:List Vall1:ValΦ:Val → IProp GF⊢ □IH : ∀ l1 xs Φ, isList l1 xs -∗ isList l2 ys -∗ (▷ ∀ v, isList v (xs ++ ys) -∗ Φ v) -∗ WP hl(v(&append) v(&l1) v(&l2)) {{ Φ }} ∗Hl1 : isList l1 [] ∗Hl2 : isList l2 ys ∗HΦ : ∀ v, isList v ([] ++ ys) -∗ Φ v ⊢ WP hl((λ l2, match v(&l1) with | injl(_) => l2 | injr(hd) => let x := fst(!hd); let l1' := snd(!hd); let r := v(&append) l1' l2; hd ← (x, r); injr(hd))) {{ v, WP hl(v(&v) v(&l2)) {{ Φ }} }} hlc:HasLCGF:BundledGFunctorsinst✝:HeapLangGS hlc GFl2:Valys:List Vall1:ValΦ:Val → IProp GFheq:l1 = hl_val(injl(#()))⊢ □IH : ∀ l1 xs Φ, isList l1 xs -∗ isList l2 ys -∗ (▷ ∀ v, isList v (xs ++ ys) -∗ Φ v) -∗ WP hl(v(&append) v(&l1) v(&l2)) {{ Φ }} ∗Hl1 : isList l1 [] ∗Hl2 : isList l2 ys ∗HΦ : ∀ v, isList v ([] ++ ys) -∗ Φ v ⊢ WP hl((λ l2, match v(&l1) with | injl(_) => l2 | injr(hd) => let x := fst(!hd); let l1' := snd(!hd); let r := v(&append) l1' l2; hd ← (x, r); injr(hd))) {{ v, WP hl(v(&v) v(&l2)) {{ Φ }} }}; hlc:HasLCGF:BundledGFunctorsinst✝:HeapLangGS hlc GFl2:Valys:List ValΦ:Val → IProp GF⊢ □IH : ∀ l1 xs Φ, isList l1 xs -∗ isList l2 ys -∗ (▷ ∀ v, isList v (xs ++ ys) -∗ Φ v) -∗ WP hl(v(&append) v(&l1) v(&l2)) {{ Φ }} ∗Hl1 : isList (hl_val(injl(#()))) [] ∗Hl2 : isList l2 ys ∗HΦ : ∀ v, isList v ([] ++ ys) -∗ Φ v ⊢ WP hl((λ l2, match v(injl(#())) with | injl(_) => l2 | injr(hd) => let x := fst(!hd); let l1' := snd(!hd); let r := v(&append) l1' l2; hd ← (x, r); injr(hd))) {{ v, WP hl(v(&v) v(&l2)) {{ Φ }} }} hlc:HasLCGF:BundledGFunctorsinst✝:HeapLangGS hlc GFl2:Valys:List ValΦ:Val → IProp GF⊢ □IH : ∀ l1 xs Φ, isList l1 xs -∗ isList l2 ys -∗ (▷ ∀ v, isList v (xs ++ ys) -∗ Φ v) -∗ WP hl(v(&append) v(&l1) v(&l2)) {{ Φ }} ∗Hl1 : isList (hl_val(injl(#()))) [] ∗Hl2 : isList l2 ys ∗HΦ : ∀ v, isList v ([] ++ ys) -∗ Φ v ⊢ |={⊤}=> Φ l2; hlc:HasLCGF:BundledGFunctorsinst✝:HeapLangGS hlc GFl2:Valys:List ValΦ:Val → IProp GF⊢ □IH : ∀ l1 xs Φ, isList l1 xs -∗ isList l2 ys -∗ (▷ ∀ v, isList v (xs ++ ys) -∗ Φ v) -∗ WP hl(v(&append) v(&l1) v(&l2)) {{ Φ }} ∗Hl1 : isList (hl_val(injl(#()))) [] ∗Hl2 : isList l2 ys ∗HΦ : ∀ v, isList v ([] ++ ys) -∗ Φ v ⊢ Φ l2 hlc:HasLCGF:BundledGFunctorsinst✝:HeapLangGS hlc GFl2:Valys:List ValΦ:Val → IProp GF⊢ □IH : ∀ l1 xs Φ, isList l1 xs -∗ isList l2 ys -∗ (▷ ∀ v, isList v (xs ++ ys) -∗ Φ v) -∗ WP hl(v(&append) v(&l1) v(&l2)) {{ Φ }} ∗Hl1 : isList (hl_val(injl(#()))) [] ∗Hl2 : isList l2 ys ∗HΦ : ∀ v, isList v ys -∗ Φ v ⊢ Φ l2 All goals completed! 🐙 hlc:HasLCGF:BundledGFunctorsinst✝:HeapLangGS hlc GFl2:Valys:List Vall1:ValΦ:Val → IProp GFx:Valxs:List Val⊢ □IH : ∀ l1 xs Φ, isList l1 xs -∗ isList l2 ys -∗ (▷ ∀ v, isList v (xs ++ ys) -∗ Φ v) -∗ WP hl(v(&append) v(&l1) v(&l2)) {{ Φ }} ∗Hl1 : isList l1 (x :: xs) ∗Hl2 : isList l2 ys ∗HΦ : ∀ v, isList v (x :: xs ++ ys) -∗ Φ v ⊢ WP hl((λ l2, match v(&l1) with | injl(_) => l2 | injr(hd) => let x := fst(!hd); let l1' := snd(!hd); let r := v(&append) l1' l2; hd ← (x, r); injr(hd))) {{ v, WP hl(v(&v) v(&l2)) {{ Φ }} }} hlc:HasLCGF:BundledGFunctorsinst✝:HeapLangGS hlc GFl2:Valys:List Vall1:ValΦ:Val → IProp GFx:Valxs:List Valhd:Locl':Valheq:l1 = hl_val(injr(#hd))⊢ □IH : ∀ l1 xs Φ, isList l1 xs -∗ isList l2 ys -∗ (▷ ∀ v, isList v (xs ++ ys) -∗ Φ v) -∗ WP hl(v(&append) v(&l1) v(&l2)) {{ Φ }} ∗Hl2 : isList l2 ys ∗HΦ : ∀ v, isList v (x :: xs ++ ys) -∗ Φ v ∗Hpt : hd ↦ some hl_val((&x, &l')) ∗Hl : isList l' xs ⊢ WP hl((λ l2, match v(&l1) with | injl(_) => l2 | injr(hd) => let x := fst(!hd); let l1' := snd(!hd); let r := v(&append) l1' l2; hd ← (x, r); injr(hd))) {{ v, WP hl(v(&v) v(&l2)) {{ Φ }} }} hlc:HasLCGF:BundledGFunctorsinst✝:HeapLangGS hlc GFl2:Valys:List ValΦ:Val → IProp GFx:Valxs:List Valhd:Locl':Val⊢ □IH : ∀ l1 xs Φ, isList l1 xs -∗ isList l2 ys -∗ (▷ ∀ v, isList v (xs ++ ys) -∗ Φ v) -∗ WP hl(v(&append) v(&l1) v(&l2)) {{ Φ }} ∗Hl2 : isList l2 ys ∗HΦ : ∀ v, isList v (x :: xs ++ ys) -∗ Φ v ∗Hpt : hd ↦ some hl_val((&x, &l')) ∗Hl : isList l' xs ⊢ WP hl((λ l2, match v(injr(#hd)) with | injl(_) => l2 | injr(hd) => let x := fst(!hd); let l1' := snd(!hd); let r := v(&append) l1' l2; hd ← (x, r); injr(hd))) {{ v, WP hl(v(&v) v(&l2)) {{ Φ }} }}; hlc:HasLCGF:BundledGFunctorsinst✝:HeapLangGS hlc GFl2:Valys:List ValΦ:Val → IProp GFx:Valxs:List Valhd:Locl':Val⊢ □IH : ∀ l1 xs Φ, isList l1 xs -∗ isList l2 ys -∗ (▷ ∀ v, isList v (xs ++ ys) -∗ Φ v) -∗ WP hl(v(&append) v(&l1) v(&l2)) {{ Φ }} ∗Hl2 : isList l2 ys ∗HΦ : ∀ v, isList v (x :: xs ++ ys) -∗ Φ v ∗Hpt : hd ↦ some hl_val((&x, &l')) ∗Hl : isList l' xs ⊢ WP hl(let x := fst(!#hd); let l1' := snd(!#hd); let r := v(&append) l1' v(&l2); #hd ← (x, r); injr(#hd)) {{ Φ }} hlc:HasLCGF:BundledGFunctorsinst✝:HeapLangGS hlc GFl2:Valys:List ValΦ:Val → IProp GFx:Valxs:List Valhd:Locl':Val⊢ □IH : ∀ l1 xs Φ, isList l1 xs -∗ isList l2 ys -∗ (▷ ∀ v, isList v (xs ++ ys) -∗ Φ v) -∗ WP hl(v(&append) v(&l1) v(&l2)) {{ Φ }} ∗Hl2 : isList l2 ys ∗HΦ : ∀ v, isList v (x :: xs ++ ys) -∗ Φ v ∗Hpt : hd ↦ some hl_val((&x, &l')) ∗Hl : isList l' xs ⊢ WP hl(let x := fst(v((&x, &l'))); let l1' := snd(!#hd); let r := v(&append) l1' v(&l2); #hd ← (x, r); injr(#hd)) {{ Φ }} hlc:HasLCGF:BundledGFunctorsinst✝:HeapLangGS hlc GFl2:Valys:List ValΦ:Val → IProp GFx:Valxs:List Valhd:Locl':Val⊢ □IH : ∀ l1 xs Φ, isList l1 xs -∗ isList l2 ys -∗ (▷ ∀ v, isList v (xs ++ ys) -∗ Φ v) -∗ WP hl(v(&append) v(&l1) v(&l2)) {{ Φ }} ∗Hl2 : isList l2 ys ∗HΦ : ∀ v, isList v (x :: xs ++ ys) -∗ Φ v ∗Hpt : hd ↦ some hl_val((&x, &l')) ∗Hl : isList l' xs ⊢ WP hl(let l1' := snd(!#hd); let r := v(&append) l1' v(&l2); #hd ← (v(&x), r); injr(#hd)) {{ Φ }} hlc:HasLCGF:BundledGFunctorsinst✝:HeapLangGS hlc GFl2:Valys:List ValΦ:Val → IProp GFx:Valxs:List Valhd:Locl':Val⊢ □IH : ∀ l1 xs Φ, isList l1 xs -∗ isList l2 ys -∗ (▷ ∀ v, isList v (xs ++ ys) -∗ Φ v) -∗ WP hl(v(&append) v(&l1) v(&l2)) {{ Φ }} ∗Hl2 : isList l2 ys ∗HΦ : ∀ v, isList v (x :: xs ++ ys) -∗ Φ v ∗Hpt : hd ↦ some hl_val((&x, &l')) ∗Hl : isList l' xs ⊢ WP hl(let l1' := snd(v((&x, &l'))); let r := v(&append) l1' v(&l2); #hd ← (v(&x), r); injr(#hd)) {{ Φ }} hlc:HasLCGF:BundledGFunctorsinst✝:HeapLangGS hlc GFl2:Valys:List ValΦ:Val → IProp GFx:Valxs:List Valhd:Locl':Val⊢ □IH : ∀ l1 xs Φ, isList l1 xs -∗ isList l2 ys -∗ (▷ ∀ v, isList v (xs ++ ys) -∗ Φ v) -∗ WP hl(v(&append) v(&l1) v(&l2)) {{ Φ }} ∗Hl2 : isList l2 ys ∗HΦ : ∀ v, isList v (x :: xs ++ ys) -∗ Φ v ∗Hpt : hd ↦ some hl_val((&x, &l')) ∗Hl : isList l' xs ⊢ WP hl(let r := v(&append) v(&l') v(&l2); #hd ← (v(&x), r); injr(#hd)) {{ Φ }} hlc:HasLCGF:BundledGFunctorsinst✝:HeapLangGS hlc GFl2:Valys:List ValΦ:Val → IProp GFx:Valxs:List Valhd:Locl':Valr:Val⊢ □IH : ∀ l1 xs Φ, isList l1 xs -∗ isList l2 ys -∗ (▷ ∀ v, isList v (xs ++ ys) -∗ Φ v) -∗ WP hl(v(&append) v(&l1) v(&l2)) {{ Φ }} ∗HΦ : ∀ v, isList v (x :: xs ++ ys) -∗ Φ v ∗Hpt : hd ↦ some hl_val((&x, &l')) ∗Hr : isList r (xs ++ ys) ⊢ WP hl(let r := v(&r); #hd ← (v(&x), r); injr(#hd)) {{ Φ }} hlc:HasLCGF:BundledGFunctorsinst✝:HeapLangGS hlc GFl2:Valys:List ValΦ:Val → IProp GFx:Valxs:List Valhd:Locl':Valr:Val⊢ □IH : ∀ l1 xs Φ, isList l1 xs -∗ isList l2 ys -∗ (▷ ∀ v, isList v (xs ++ ys) -∗ Φ v) -∗ WP hl(v(&append) v(&l1) v(&l2)) {{ Φ }} ∗HΦ : ∀ v, isList v (x :: xs ++ ys) -∗ Φ v ∗Hpt : hd ↦ some hl_val((&x, &l')) ∗Hr : isList r (xs ++ ys) ⊢ WP hl(#hd ← v((&x, &r)); injr(#hd)) {{ Φ }} hlc:HasLCGF:BundledGFunctorsinst✝:HeapLangGS hlc GFl2:Valys:List ValΦ:Val → IProp GFx:Valxs:List Valhd:Locl':Valr:Val⊢ □IH : ∀ l1 xs Φ, isList l1 xs -∗ isList l2 ys -∗ (▷ ∀ v, isList v (xs ++ ys) -∗ Φ v) -∗ WP hl(v(&append) v(&l1) v(&l2)) {{ Φ }} ∗HΦ : ∀ v, isList v (x :: xs ++ ys) -∗ Φ v ∗Hr : isList r (xs ++ ys) ∗Hpt : hd ↦ some hl_val((&x, &r)) ⊢ WP hl(injr(#hd)) {{ Φ }} hlc:HasLCGF:BundledGFunctorsinst✝:HeapLangGS hlc GFl2:Valys:List ValΦ:Val → IProp GFx:Valxs:List Valhd:Locl':Valr:Val⊢ □IH : ∀ l1 xs Φ, isList l1 xs -∗ isList l2 ys -∗ (▷ ∀ v, isList v (xs ++ ys) -∗ Φ v) -∗ WP hl(v(&append) v(&l1) v(&l2)) {{ Φ }} ∗HΦ : ∀ v, isList v (x :: xs ++ ys) -∗ Φ v ∗Hr : isList r (xs ++ ys) ∗Hpt : hd ↦ some hl_val((&x, &r)) ⊢ |={⊤}=> Φ (hl_val(injr(#hd))) hlc:HasLCGF:BundledGFunctorsinst✝:HeapLangGS hlc GFl2:Valys:List ValΦ:Val → IProp GFx:Valxs:List Valhd:Locl':Valr:Val⊢ □IH : ∀ l1 xs Φ, isList l1 xs -∗ isList l2 ys -∗ (▷ ∀ v, isList v (xs ++ ys) -∗ Φ v) -∗ WP hl(v(&append) v(&l1) v(&l2)) {{ Φ }} ∗HΦ : ∀ v, isList v (x :: xs ++ ys) -∗ Φ v ∗Hr : isList r (xs ++ ys) ∗Hpt : hd ↦ some hl_val((&x, &r)) ⊢ Φ (hl_val(injr(#hd))) hlc:HasLCGF:BundledGFunctorsinst✝:HeapLangGS hlc GFl2:Valys:List ValΦ:Val → IProp GFx:Valxs:List Valhd:Locl':Valr:Val⊢ □IH : ∀ l1 xs Φ, isList l1 xs -∗ isList l2 ys -∗ (▷ ∀ v, isList v (xs ++ ys) -∗ Φ v) -∗ WP hl(v(&append) v(&l1) v(&l2)) {{ Φ }} ∗Hr : isList r (xs ++ ys) ∗Hpt : hd ↦ some hl_val((&x, &r)) ⊢ isList (hl_val(injr(#hd))) (x :: xs ++ ys) hlc:HasLCGF:BundledGFunctorsinst✝:HeapLangGS hlc GFl2:Valys:List ValΦ:Val → IProp GFx:Valxs:List Valhd:Locl':Valr:Val⊢ □IH : ∀ l1 xs Φ, isList l1 xs -∗ isList l2 ys -∗ (▷ ∀ v, isList v (xs ++ ys) -∗ Φ v) -∗ WP hl(v(&append) v(&l1) v(&l2)) {{ Φ }} ∗Hr : isList r (xs ++ ys) ∗Hpt : hd ↦ some hl_val((&x, &r)) ⊢ isList (hl_val(injr(#hd))) (x :: (xs ++ ys)) hlc:HasLCGF:BundledGFunctorsinst✝:HeapLangGS hlc GFl2:Valys:List ValΦ:Val → IProp GFx:Valxs:List Valhd:Locl':Valr:Val⊢ □IH : ∀ l1 xs Φ, isList l1 xs -∗ isList l2 ys -∗ (▷ ∀ v, isList v (xs ++ ys) -∗ Φ v) -∗ WP hl(v(&append) v(&l1) v(&l2)) {{ Φ }} ∗Hr : isList r (xs ++ ys) ∗Hpt : hd ↦ some hl_val((&x, &r)) ⊢ ∃ hd_1 l', ⌜hl_val(injr(#hd)) = hl_val(injr(#hd_1))⌝ ∗ hd_1 ↦ some hl_val((&x, &l')) ∗ isList l' (xs ++ ys) hlc:HasLCGF:BundledGFunctorsinst✝:HeapLangGS hlc GFl2:Valys:List ValΦ:Val → IProp GFx:Valxs:List Valhd:Locl':Valr:Val⊢ □IH : ∀ l1 xs Φ, isList l1 xs -∗ isList l2 ys -∗ (▷ ∀ v, isList v (xs ++ ys) -∗ Φ v) -∗ WP hl(v(&append) v(&l1) v(&l2)) {{ Φ }} ∗Hr : isList r (xs ++ ys) ∗Hpt : hd ↦ some hl_val((&x, &r)) ⊢ ⌜hl_val(injr(#hd)) = hl_val(injr(#hd))⌝ ∗ hd ↦ some hl_val((&x, &r)) ∗ isList r (xs ++ ys) hlc:HasLCGF:BundledGFunctorsinst✝:HeapLangGS hlc GFl2:Valys:List ValΦ:Val → IProp GFx:Valxs:List Valhd:Locl':Valr:Val⊢ □IH : ∀ l1 xs Φ, isList l1 xs -∗ isList l2 ys -∗ (▷ ∀ v, isList v (xs ++ ys) -∗ Φ v) -∗ WP hl(v(&append) v(&l1) v(&l2)) {{ Φ }} ⊢ ⌜hl_val(injr(#hd)) = hl_val(injr(#hd))⌝ All goals completed! 🐙

The proof proceeds by Löb induction (iloeb), generalising over l1, xs, and Φ so the induction hypothesis IH is strong enough for the recursive call. The curried recursive function is stepped with wp_bind (&append _) followed by wp_rec, which unfolds one call and β-reduces past the first argument. At the recursive call we focus the sub-expression with wp_apply IH, which also applies the induction hypothesis.

7.3. Reverse🔗

We implement reverse using a helper, reverse_append, which takes l and acc and returns the list rev l ++ acc — reversing l onto the front of acc by re-threading the existing nodes.

def reverse_append : Val := hl_val% rec reverse_append l acc := match l with | none() => acc | some(hd) => let x := fst(!hd); let l' := snd(!hd); hd ← (x, acc); reverse_append l' (some(hd)) def reverse : Val := hl_val% λ l, &reverse_append l (none())

The specification of the helper threads the accumulator through the induction. Unlike append, the accumulator acc and its list ys change on every recursive call, so we generalise over them too.

theorem reverse_append_spec (l acc : Val) (xs ys : List Val) : {{ isList (GF := GF) l xs ∗ isList acc ys }} hl(&reverse_append &l &acc) {{ v, RET v; isList v (xs.reverse ++ ys) }} := hlc:HasLCGF:BundledGFunctorsinst✝:HeapLangGS hlc GFl:Valacc:Valxs:List Valys:List Val⊢ ⊢ ∀ Φ, isList l xs ∗ isList acc ys -∗ (▷ ∀ v, isList v (xs.reverse ++ ys) -∗ Φ v) -∗ WP hl(v(&reverse_append) v(&l) v(&acc)) {{ Φ }} hlc:HasLCGF:BundledGFunctorsinst✝:HeapLangGS hlc GFl:Valacc:Valxs:List Valys:List ValΦ:Val → IProp GF⊢ ∗Hl : isList l xs ∗Hacc : isList acc ys ∗HΦ : ▷ ∀ v, isList v (xs.reverse ++ ys) -∗ Φ v ⊢ WP hl(v(&reverse_append) v(&l) v(&acc)) {{ Φ }} hlc:HasLCGF:BundledGFunctorsinst✝:HeapLangGS hlc GFl:Valacc:Valxs:List Valys:List ValΦ:Val → IProp GF⊢ □IH : ▷ ∀ l acc xs ys Φ, isList l xs -∗ isList acc ys -∗ (▷ ∀ v, isList v (xs.reverse ++ ys) -∗ Φ v) -∗ WP hl(v(&reverse_append) v(&l) v(&acc)) {{ Φ }} ∗Hl : isList l xs ∗Hacc : isList acc ys ∗HΦ : ▷ ∀ v, isList v (xs.reverse ++ ys) -∗ Φ v ⊢ WP hl(v(&reverse_append) v(&l) v(&acc)) {{ Φ }} hlc:HasLCGF:BundledGFunctorsinst✝:HeapLangGS hlc GFl:Valacc:Valxs:List Valys:List ValΦ:Val → IProp GF⊢ □IH : ▷ ∀ l acc xs ys Φ, isList l xs -∗ isList acc ys -∗ (▷ ∀ v, isList v (xs.reverse ++ ys) -∗ Φ v) -∗ WP hl(v(&reverse_append) v(&l) v(&acc)) {{ Φ }} ∗Hl : isList l xs ∗Hacc : isList acc ys ∗HΦ : ▷ ∀ v, isList v (xs.reverse ++ ys) -∗ Φ v ⊢ WP hl(v(&reverse_append) v(&l)) {{ v, WP hl(v(&v) v(&acc)) {{ Φ }} }} hlc:HasLCGF:BundledGFunctorsinst✝:HeapLangGS hlc GFl:Valacc:Valxs:List Valys:List ValΦ:Val → IProp GF⊢ □IH : ∀ l acc xs ys Φ, isList l xs -∗ isList acc ys -∗ (▷ ∀ v, isList v (xs.reverse ++ ys) -∗ Φ v) -∗ WP hl(v(&reverse_append) v(&l) v(&acc)) {{ Φ }} ∗Hl : isList l xs ∗Hacc : isList acc ys ∗HΦ : ∀ v, isList v (xs.reverse ++ ys) -∗ Φ v ⊢ WP hl((λ acc, match v(&l) with | injl(_) => acc | injr(hd) => let x := fst(!hd); let l' := snd(!hd); hd ← (x, acc); v(&reverse_append) l' (injr(hd)))) {{ v, WP hl(v(&v) v(&acc)) {{ Φ }} }} cases xs with hlc:HasLCGF:BundledGFunctorsinst✝:HeapLangGS hlc GFl:Valacc:Valys:List ValΦ:Val → IProp GF⊢ □IH : ∀ l acc xs ys Φ, isList l xs -∗ isList acc ys -∗ (▷ ∀ v, isList v (xs.reverse ++ ys) -∗ Φ v) -∗ WP hl(v(&reverse_append) v(&l) v(&acc)) {{ Φ }} ∗Hl : isList l [] ∗Hacc : isList acc ys ∗HΦ : ∀ v, isList v ([].reverse ++ ys) -∗ Φ v ⊢ WP hl((λ acc, match v(&l) with | injl(_) => acc | injr(hd) => let x := fst(!hd); let l' := snd(!hd); hd ← (x, acc); v(&reverse_append) l' (injr(hd)))) {{ v, WP hl(v(&v) v(&acc)) {{ Φ }} }} hlc:HasLCGF:BundledGFunctorsinst✝:HeapLangGS hlc GFl:Valacc:Valys:List ValΦ:Val → IProp GFheq:l = hl_val(injl(#()))⊢ □IH : ∀ l acc xs ys Φ, isList l xs -∗ isList acc ys -∗ (▷ ∀ v, isList v (xs.reverse ++ ys) -∗ Φ v) -∗ WP hl(v(&reverse_append) v(&l) v(&acc)) {{ Φ }} ∗Hl : isList l [] ∗Hacc : isList acc ys ∗HΦ : ∀ v, isList v ([].reverse ++ ys) -∗ Φ v ⊢ WP hl((λ acc, match v(&l) with | injl(_) => acc | injr(hd) => let x := fst(!hd); let l' := snd(!hd); hd ← (x, acc); v(&reverse_append) l' (injr(hd)))) {{ v, WP hl(v(&v) v(&acc)) {{ Φ }} }}; hlc:HasLCGF:BundledGFunctorsinst✝:HeapLangGS hlc GFacc:Valys:List ValΦ:Val → IProp GF⊢ □IH : ∀ l acc xs ys Φ, isList l xs -∗ isList acc ys -∗ (▷ ∀ v, isList v (xs.reverse ++ ys) -∗ Φ v) -∗ WP hl(v(&reverse_append) v(&l) v(&acc)) {{ Φ }} ∗Hl : isList (hl_val(injl(#()))) [] ∗Hacc : isList acc ys ∗HΦ : ∀ v, isList v ([].reverse ++ ys) -∗ Φ v ⊢ WP hl((λ acc, match v(injl(#())) with | injl(_) => acc | injr(hd) => let x := fst(!hd); let l' := snd(!hd); hd ← (x, acc); v(&reverse_append) l' (injr(hd)))) {{ v, WP hl(v(&v) v(&acc)) {{ Φ }} }} hlc:HasLCGF:BundledGFunctorsinst✝:HeapLangGS hlc GFacc:Valys:List ValΦ:Val → IProp GF⊢ □IH : ∀ l acc xs ys Φ, isList l xs -∗ isList acc ys -∗ (▷ ∀ v, isList v (xs.reverse ++ ys) -∗ Φ v) -∗ WP hl(v(&reverse_append) v(&l) v(&acc)) {{ Φ }} ∗Hl : isList (hl_val(injl(#()))) [] ∗Hacc : isList acc ys ∗HΦ : ∀ v, isList v ([].reverse ++ ys) -∗ Φ v ⊢ |={⊤}=> Φ acc; hlc:HasLCGF:BundledGFunctorsinst✝:HeapLangGS hlc GFacc:Valys:List ValΦ:Val → IProp GF⊢ □IH : ∀ l acc xs ys Φ, isList l xs -∗ isList acc ys -∗ (▷ ∀ v, isList v (xs.reverse ++ ys) -∗ Φ v) -∗ WP hl(v(&reverse_append) v(&l) v(&acc)) {{ Φ }} ∗Hl : isList (hl_val(injl(#()))) [] ∗Hacc : isList acc ys ∗HΦ : ∀ v, isList v ([].reverse ++ ys) -∗ Φ v ⊢ Φ acc hlc:HasLCGF:BundledGFunctorsinst✝:HeapLangGS hlc GFacc:Valys:List ValΦ:Val → IProp GF⊢ □IH : ∀ l acc xs ys Φ, isList l xs -∗ isList acc ys -∗ (▷ ∀ v, isList v (xs.reverse ++ ys) -∗ Φ v) -∗ WP hl(v(&reverse_append) v(&l) v(&acc)) {{ Φ }} ∗Hl : isList (hl_val(injl(#()))) [] ∗Hacc : isList acc ys ∗HΦ : ∀ v, isList v ys -∗ Φ v ⊢ Φ acc All goals completed! 🐙 hlc:HasLCGF:BundledGFunctorsinst✝:HeapLangGS hlc GFl:Valacc:Valys:List ValΦ:Val → IProp GFx:Valxs:List Val⊢ □IH : ∀ l acc xs ys Φ, isList l xs -∗ isList acc ys -∗ (▷ ∀ v, isList v (xs.reverse ++ ys) -∗ Φ v) -∗ WP hl(v(&reverse_append) v(&l) v(&acc)) {{ Φ }} ∗Hl : isList l (x :: xs) ∗Hacc : isList acc ys ∗HΦ : ∀ v, isList v ((x :: xs).reverse ++ ys) -∗ Φ v ⊢ WP hl((λ acc, match v(&l) with | injl(_) => acc | injr(hd) => let x := fst(!hd); let l' := snd(!hd); hd ← (x, acc); v(&reverse_append) l' (injr(hd)))) {{ v, WP hl(v(&v) v(&acc)) {{ Φ }} }} hlc:HasLCGF:BundledGFunctorsinst✝:HeapLangGS hlc GFl:Valacc:Valys:List ValΦ:Val → IProp GFx:Valxs:List Valhd:Locl':Valheq:l = hl_val(injr(#hd))⊢ □IH : ∀ l acc xs ys Φ, isList l xs -∗ isList acc ys -∗ (▷ ∀ v, isList v (xs.reverse ++ ys) -∗ Φ v) -∗ WP hl(v(&reverse_append) v(&l) v(&acc)) {{ Φ }} ∗Hacc : isList acc ys ∗HΦ : ∀ v, isList v ((x :: xs).reverse ++ ys) -∗ Φ v ∗Hpt : hd ↦ some hl_val((&x, &l')) ∗Hl : isList l' xs ⊢ WP hl((λ acc, match v(&l) with | injl(_) => acc | injr(hd) => let x := fst(!hd); let l' := snd(!hd); hd ← (x, acc); v(&reverse_append) l' (injr(hd)))) {{ v, WP hl(v(&v) v(&acc)) {{ Φ }} }} hlc:HasLCGF:BundledGFunctorsinst✝:HeapLangGS hlc GFacc:Valys:List ValΦ:Val → IProp GFx:Valxs:List Valhd:Locl':Val⊢ □IH : ∀ l acc xs ys Φ, isList l xs -∗ isList acc ys -∗ (▷ ∀ v, isList v (xs.reverse ++ ys) -∗ Φ v) -∗ WP hl(v(&reverse_append) v(&l) v(&acc)) {{ Φ }} ∗Hacc : isList acc ys ∗HΦ : ∀ v, isList v ((x :: xs).reverse ++ ys) -∗ Φ v ∗Hpt : hd ↦ some hl_val((&x, &l')) ∗Hl : isList l' xs ⊢ WP hl((λ acc, match v(injr(#hd)) with | injl(_) => acc | injr(hd) => let x := fst(!hd); let l' := snd(!hd); hd ← (x, acc); v(&reverse_append) l' (injr(hd)))) {{ v, WP hl(v(&v) v(&acc)) {{ Φ }} }}; hlc:HasLCGF:BundledGFunctorsinst✝:HeapLangGS hlc GFacc:Valys:List ValΦ:Val → IProp GFx:Valxs:List Valhd:Locl':Val⊢ □IH : ∀ l acc xs ys Φ, isList l xs -∗ isList acc ys -∗ (▷ ∀ v, isList v (xs.reverse ++ ys) -∗ Φ v) -∗ WP hl(v(&reverse_append) v(&l) v(&acc)) {{ Φ }} ∗Hacc : isList acc ys ∗HΦ : ∀ v, isList v ((x :: xs).reverse ++ ys) -∗ Φ v ∗Hpt : hd ↦ some hl_val((&x, &l')) ∗Hl : isList l' xs ⊢ WP hl(let x := fst(!#hd); let l' := snd(!#hd); #hd ← (x, v(&acc)); v(&reverse_append) l' (injr(#hd))) {{ Φ }} hlc:HasLCGF:BundledGFunctorsinst✝:HeapLangGS hlc GFacc:Valys:List ValΦ:Val → IProp GFx:Valxs:List Valhd:Locl':Val⊢ □IH : ∀ l acc xs ys Φ, isList l xs -∗ isList acc ys -∗ (▷ ∀ v, isList v (xs.reverse ++ ys) -∗ Φ v) -∗ WP hl(v(&reverse_append) v(&l) v(&acc)) {{ Φ }} ∗Hacc : isList acc ys ∗HΦ : ∀ v, isList v ((x :: xs).reverse ++ ys) -∗ Φ v ∗Hpt : hd ↦ some hl_val((&x, &l')) ∗Hl : isList l' xs ⊢ WP hl(let x := fst(v((&x, &l'))); let l' := snd(!#hd); #hd ← (x, v(&acc)); v(&reverse_append) l' (injr(#hd))) {{ Φ }} hlc:HasLCGF:BundledGFunctorsinst✝:HeapLangGS hlc GFacc:Valys:List ValΦ:Val → IProp GFx:Valxs:List Valhd:Locl':Val⊢ □IH : ∀ l acc xs ys Φ, isList l xs -∗ isList acc ys -∗ (▷ ∀ v, isList v (xs.reverse ++ ys) -∗ Φ v) -∗ WP hl(v(&reverse_append) v(&l) v(&acc)) {{ Φ }} ∗Hacc : isList acc ys ∗HΦ : ∀ v, isList v ((x :: xs).reverse ++ ys) -∗ Φ v ∗Hpt : hd ↦ some hl_val((&x, &l')) ∗Hl : isList l' xs ⊢ WP hl(let l' := snd(!#hd); #hd ← (v(&x), v(&acc)); v(&reverse_append) l' (injr(#hd))) {{ Φ }} hlc:HasLCGF:BundledGFunctorsinst✝:HeapLangGS hlc GFacc:Valys:List ValΦ:Val → IProp GFx:Valxs:List Valhd:Locl':Val⊢ □IH : ∀ l acc xs ys Φ, isList l xs -∗ isList acc ys -∗ (▷ ∀ v, isList v (xs.reverse ++ ys) -∗ Φ v) -∗ WP hl(v(&reverse_append) v(&l) v(&acc)) {{ Φ }} ∗Hacc : isList acc ys ∗HΦ : ∀ v, isList v ((x :: xs).reverse ++ ys) -∗ Φ v ∗Hpt : hd ↦ some hl_val((&x, &l')) ∗Hl : isList l' xs ⊢ WP hl(let l' := snd(v((&x, &l'))); #hd ← (v(&x), v(&acc)); v(&reverse_append) l' (injr(#hd))) {{ Φ }} hlc:HasLCGF:BundledGFunctorsinst✝:HeapLangGS hlc GFacc:Valys:List ValΦ:Val → IProp GFx:Valxs:List Valhd:Locl':Val⊢ □IH : ∀ l acc xs ys Φ, isList l xs -∗ isList acc ys -∗ (▷ ∀ v, isList v (xs.reverse ++ ys) -∗ Φ v) -∗ WP hl(v(&reverse_append) v(&l) v(&acc)) {{ Φ }} ∗Hacc : isList acc ys ∗HΦ : ∀ v, isList v ((x :: xs).reverse ++ ys) -∗ Φ v ∗Hpt : hd ↦ some hl_val((&x, &l')) ∗Hl : isList l' xs ⊢ WP hl(#hd ← v((&x, &acc)); v(&reverse_append) v(&l') (injr(#hd))) {{ Φ }} hlc:HasLCGF:BundledGFunctorsinst✝:HeapLangGS hlc GFacc:Valys:List ValΦ:Val → IProp GFx:Valxs:List Valhd:Locl':Val⊢ □IH : ∀ l acc xs ys Φ, isList l xs -∗ isList acc ys -∗ (▷ ∀ v, isList v (xs.reverse ++ ys) -∗ Φ v) -∗ WP hl(v(&reverse_append) v(&l) v(&acc)) {{ Φ }} ∗Hacc : isList acc ys ∗HΦ : ∀ v, isList v ((x :: xs).reverse ++ ys) -∗ Φ v ∗Hl : isList l' xs ∗Hpt : hd ↦ some hl_val((&x, &acc)) ⊢ WP hl(v(&reverse_append) v(&l') (injr(#hd))) {{ Φ }} hlc:HasLCGF:BundledGFunctorsinst✝:HeapLangGS hlc GFacc:Valys:List ValΦ:Val → IProp GFx:Valxs:List Valhd:Locl':Val⊢ □IH : ∀ l acc xs ys Φ, isList l xs -∗ isList acc ys -∗ (▷ ∀ v, isList v (xs.reverse ++ ys) -∗ Φ v) -∗ WP hl(v(&reverse_append) v(&l) v(&acc)) {{ Φ }} ∗Hacc : isList acc ys ∗HΦ : ∀ v, isList v ((x :: xs).reverse ++ ys) -∗ Φ v ∗Hl : isList l' xs ∗Hpt : hd ↦ some hl_val((&x, &acc)) ⊢ WP hl(v(&reverse_append) v(&l') (v(injr(#hd)))) {{ Φ }} hlc:HasLCGF:BundledGFunctorsinst✝:HeapLangGS hlc GFacc:Valys:List ValΦ:Val → IProp GFx:Valxs:List Valhd:Locl':Val⊢ □IH : ∀ l acc xs ys Φ, isList l xs -∗ isList acc ys -∗ (▷ ∀ v, isList v (xs.reverse ++ ys) -∗ Φ v) -∗ WP hl(v(&reverse_append) v(&l) v(&acc)) {{ Φ }} ∗Hacc : isList acc ys ∗Hpt : hd ↦ some hl_val((&x, &acc)) ⊢ isList (hl_val(injr(#hd))) (x :: ys)hlc:HasLCGF:BundledGFunctorsinst✝:HeapLangGS hlc GFacc:Valys:List ValΦ:Val → IProp GFx:Valxs:List Valhd:Locl':Val⊢ □IH : ∀ l acc xs ys Φ, isList l xs -∗ isList acc ys -∗ (▷ ∀ v, isList v (xs.reverse ++ ys) -∗ Φ v) -∗ WP hl(v(&reverse_append) v(&l) v(&acc)) {{ Φ }} ∗HΦ : ∀ v, isList v ((x :: xs).reverse ++ ys) -∗ Φ v ∗Hl : isList l' xs ∗Hnode : isList (hl_val(injr(#hd))) (x :: ys) ⊢ WP hl(v(&reverse_append) v(&l') (v(injr(#hd)))) {{ Φ }} hlc:HasLCGF:BundledGFunctorsinst✝:HeapLangGS hlc GFacc:Valys:List ValΦ:Val → IProp GFx:Valxs:List Valhd:Locl':Val⊢ □IH : ∀ l acc xs ys Φ, isList l xs -∗ isList acc ys -∗ (▷ ∀ v, isList v (xs.reverse ++ ys) -∗ Φ v) -∗ WP hl(v(&reverse_append) v(&l) v(&acc)) {{ Φ }} ∗Hacc : isList acc ys ∗Hpt : hd ↦ some hl_val((&x, &acc)) ⊢ isList (hl_val(injr(#hd))) (x :: ys) hlc:HasLCGF:BundledGFunctorsinst✝:HeapLangGS hlc GFacc:Valys:List ValΦ:Val → IProp GFx:Valxs:List Valhd:Locl':Val⊢ □IH : ∀ l acc xs ys Φ, isList l xs -∗ isList acc ys -∗ (▷ ∀ v, isList v (xs.reverse ++ ys) -∗ Φ v) -∗ WP hl(v(&reverse_append) v(&l) v(&acc)) {{ Φ }} ∗Hacc : isList acc ys ∗Hpt : hd ↦ some hl_val((&x, &acc)) ⊢ ∃ hd_1 l', ⌜hl_val(injr(#hd)) = hl_val(injr(#hd_1))⌝ ∗ hd_1 ↦ some hl_val((&x, &l')) ∗ isList l' ys hlc:HasLCGF:BundledGFunctorsinst✝:HeapLangGS hlc GFacc:Valys:List ValΦ:Val → IProp GFx:Valxs:List Valhd:Locl':Val⊢ □IH : ∀ l acc xs ys Φ, isList l xs -∗ isList acc ys -∗ (▷ ∀ v, isList v (xs.reverse ++ ys) -∗ Φ v) -∗ WP hl(v(&reverse_append) v(&l) v(&acc)) {{ Φ }} ∗Hacc : isList acc ys ∗Hpt : hd ↦ some hl_val((&x, &acc)) ⊢ ⌜hl_val(injr(#hd)) = hl_val(injr(#hd))⌝ ∗ hd ↦ some hl_val((&x, &acc)) ∗ isList acc ys hlc:HasLCGF:BundledGFunctorsinst✝:HeapLangGS hlc GFacc:Valys:List ValΦ:Val → IProp GFx:Valxs:List Valhd:Locl':Val⊢ □IH : ∀ l acc xs ys Φ, isList l xs -∗ isList acc ys -∗ (▷ ∀ v, isList v (xs.reverse ++ ys) -∗ Φ v) -∗ WP hl(v(&reverse_append) v(&l) v(&acc)) {{ Φ }} ⊢ ⌜hl_val(injr(#hd)) = hl_val(injr(#hd))⌝ All goals completed! 🐙 hlc:HasLCGF:BundledGFunctorsinst✝:HeapLangGS hlc GFacc:Valys:List ValΦ:Val → IProp GFx:Valxs:List Valhd:Locl':Valv:Val⊢ □IH : ∀ l acc xs ys Φ, isList l xs -∗ isList acc ys -∗ (▷ ∀ v, isList v (xs.reverse ++ ys) -∗ Φ v) -∗ WP hl(v(&reverse_append) v(&l) v(&acc)) {{ Φ }} ∗HΦ : ∀ v, isList v ((x :: xs).reverse ++ ys) -∗ Φ v ∗Hv : isList v (xs.reverse ++ x :: ys) ⊢ Φ v hlc:HasLCGF:BundledGFunctorsinst✝:HeapLangGS hlc GFacc:Valys:List ValΦ:Val → IProp GFx:Valxs:List Valhd:Locl':Valv:Val⊢ □IH : ∀ l acc xs ys Φ, isList l xs -∗ isList acc ys -∗ (▷ ∀ v, isList v (xs.reverse ++ ys) -∗ Φ v) -∗ WP hl(v(&reverse_append) v(&l) v(&acc)) {{ Φ }} ∗HΦ : ∀ v, isList v (xs.reverse ++ x :: ys) -∗ Φ v ∗Hv : isList v (xs.reverse ++ x :: ys) ⊢ Φ v All goals completed! 🐙

Now we use the helper's specification to prove reverse. The empty accumulator represents the empty list, so reverse l returns the reverse of l.

theorem reverse_spec (l : Val) (xs : List Val) : {{ isList (GF := GF) l xs }} hl(&reverse &l) {{ v, RET v; isList v xs.reverse }} := hlc:HasLCGF:BundledGFunctorsinst✝:HeapLangGS hlc GFl:Valxs:List Val⊢ ⊢ ∀ Φ, isList l xs -∗ (▷ ∀ v, isList v xs.reverse -∗ Φ v) -∗ WP hl(v(&reverse) v(&l)) {{ Φ }} hlc:HasLCGF:BundledGFunctorsinst✝:HeapLangGS hlc GFl:Valxs:List ValΦ:Val → IProp GF⊢ ∗Hl : isList l xs ∗HΦ : ▷ ∀ v, isList v xs.reverse -∗ Φ v ⊢ WP hl(v(&reverse) v(&l)) {{ Φ }} hlc:HasLCGF:BundledGFunctorsinst✝:HeapLangGS hlc GFl:Valxs:List ValΦ:Val → IProp GF⊢ ∗Hl : isList l xs ∗HΦ : ∀ v, isList v xs.reverse -∗ Φ v ⊢ WP hl(v(&reverse_append) v(&l) (injl(#()))) {{ Φ }} hlc:HasLCGF:BundledGFunctorsinst✝:HeapLangGS hlc GFl:Valxs:List ValΦ:Val → IProp GF⊢ ∗Hl : isList l xs ∗HΦ : ∀ v, isList v xs.reverse -∗ Φ v ⊢ WP hl(v(&reverse_append) v(&l) (v(injl(#())))) {{ Φ }} hlc:HasLCGF:BundledGFunctorsinst✝:HeapLangGS hlc GFl:Valxs:List ValΦ:Val → IProp GF⊢ ⊢ isList (hl_val(injl(#()))) []hlc:HasLCGF:BundledGFunctorsinst✝:HeapLangGS hlc GFl:Valxs:List ValΦ:Val → IProp GF⊢ ∗Hl : isList l xs ∗HΦ : ∀ v, isList v xs.reverse -∗ Φ v ∗Hacc : isList (hl_val(injl(#()))) [] ⊢ WP hl(v(&reverse_append) v(&l) (v(injl(#())))) {{ Φ }} hlc:HasLCGF:BundledGFunctorsinst✝:HeapLangGS hlc GFl:Valxs:List ValΦ:Val → IProp GF⊢ ⊢ isList (hl_val(injl(#()))) [] hlc:HasLCGF:BundledGFunctorsinst✝:HeapLangGS hlc GFl:Valxs:List ValΦ:Val → IProp GF⊢ ⊢ ⌜hl_val(injl(#())) = hl_val(injl(#()))⌝ All goals completed! 🐙 hlc:HasLCGF:BundledGFunctorsinst✝:HeapLangGS hlc GFl:Valxs:List ValΦ:Val → IProp GF⊢ ∗Hl : isList l xs ∗Hacc : isList (hl_val(injl(#()))) [] ⊢ isList l ?xs ∗ isList (hl_val(injl(#()))) ?yshlc:HasLCGF:BundledGFunctorsinst✝:HeapLangGS hlc GFl:Valxs:List ValΦ:Val → IProp GFv:Val⊢ ∗HΦ : ∀ v, isList v xs.reverse -∗ Φ v ∗Hv : isList v (List.reverse ?xs ++ ?ys) ⊢ Φ vhlc:HasLCGF:BundledGFunctorsinst✝:HeapLangGS hlc GFl:Valxs:List ValΦ:Val → IProp GF⊢ List Valhlc:HasLCGF:BundledGFunctorsinst✝:HeapLangGS hlc GFl:Valxs:List ValΦ:Val → IProp GF⊢ List Valhlc:HasLCGF:BundledGFunctorsinst✝:HeapLangGS hlc GFl:Valxs:List ValΦ:Val → IProp GF⊢ List Valhlc:HasLCGF:BundledGFunctorsinst✝:HeapLangGS hlc GFl:Valxs:List ValΦ:Val → IProp GF⊢ List Valhlc:HasLCGF:BundledGFunctorsinst✝:HeapLangGS hlc GFl:Valxs:List ValΦ:Val → IProp GF⊢ List Valhlc:HasLCGF:BundledGFunctorsinst✝:HeapLangGS hlc GFl:Valxs:List ValΦ:Val → IProp GF⊢ List Val hlc:HasLCGF:BundledGFunctorsinst✝:HeapLangGS hlc GFl:Valxs:List ValΦ:Val → IProp GF⊢ ∗Hl : isList l xs ∗Hacc : isList (hl_val(injl(#()))) [] ⊢ isList l ?xs ∗ isList (hl_val(injl(#()))) ?ys All goals completed! 🐙 hlc:HasLCGF:BundledGFunctorsinst✝:HeapLangGS hlc GFl:Valxs:List ValΦ:Val → IProp GFv:Val⊢ ∗HΦ : ∀ v, isList v xs.reverse -∗ Φ v ∗Hv : isList v (xs.reverse ++ []) ⊢ Φ v hlc:HasLCGF:BundledGFunctorsinst✝:HeapLangGS hlc GFl:Valxs:List ValΦ:Val → IProp GFv:Val⊢ ∗HΦ : ∀ v, isList v xs.reverse -∗ Φ v ∗Hv : isList v xs.reverse ⊢ Φ v All goals completed! 🐙

7.4. Folding Over a List🔗

The specifications so far have been rather concrete. Now we give a very general specification for fold_right.

def fold_right : Val := hl_val% rec fold_right f v l := match l with | none() => v | some(hd) => let x := fst(!hd); let l' := snd(!hd); f x (fold_right f v l')

The specification has many moving parts, so let us go through them.

  • l is a linked list representing xs, as stated by isList l xs in the precondition.

  • P is a predicate that all values in xs should satisfy, written as the big separating conjunction [∗list] _k ↦ x ∈ xs, P x (the index _k is unused here).

  • I (think invariant) relates a list to the result of the fold; the base value satisfies I [] a.

  • f is the folding function, assumed to satisfy a (persistent) Hoare triple: given P x and I ys a', the call f x a' returns r with I (x :: ys) r.

  • The result r of the whole fold satisfies I xs r.

  • Importantly, the original list is left unchanged, so isList l xs reappears in the postcondition.

The assumption for f is a family of Hoare triples. These are persistent, so #Hf can be reused at every step of the induction.

theorem fold_right_spec (P : Val → IProp GF) (I : List Val → Val → IProp GF) (f a l : Val) (xs : List Val) : (∀ (x a' : Val) ys, {{ P x ∗ I ys a' }} hl(&f &x &a') {{ r, RET r; I (x :: ys) r }}) -∗ {{ isList (GF := GF) l xs ∗ ([∗list] _k ↦ x ∈ xs, P x) ∗ I [] a }} hl(&fold_right &f &a &l) {{ r, RET r; isList l xs ∗ I xs r }} := hlc:HasLCGF:BundledGFunctorsinst✝:HeapLangGS hlc GFP:Val → IProp GFI:List Val → Val → IProp GFf:Vala:Vall:Valxs:List Val⊢ ⊢ (∀ x a' ys, □ ∀ Φ, P x ∗ I ys a' -∗ (▷ ∀ r, I (x :: ys) r -∗ Φ r) -∗ WP hl(v(&f) v(&x) v(&a')) {{ Φ }} ) -∗ □ ∀ Φ, isList l xs ∗ ([∗list] x ∈ xs, P x) ∗ I [] a -∗ (▷ ∀ r, isList l xs ∗ I xs r -∗ Φ r) -∗ WP hl(v(&fold_right) v(&f) v(&a) v(&l)) {{ Φ }} hlc:HasLCGF:BundledGFunctorsinst✝:HeapLangGS hlc GFP:Val → IProp GFI:List Val → Val → IProp GFf:Vala:Vall:Valxs:List ValΦ:Val → IProp GF⊢ □Hf : ∀ x a' ys, □ ∀ Φ, P x ∗ I ys a' -∗ (▷ ∀ r, I (x :: ys) r -∗ Φ r) -∗ WP hl(v(&f) v(&x) v(&a')) {{ Φ }} ∗Hl : isList l xs ∗HP : [∗list] x ∈ xs, P x ∗HI : I [] a ∗HΦ : ▷ ∀ r, isList l xs ∗ I xs r -∗ Φ r ⊢ WP hl(v(&fold_right) v(&f) v(&a) v(&l)) {{ Φ }} hlc:HasLCGF:BundledGFunctorsinst✝:HeapLangGS hlc GFP:Val → IProp GFI:List Val → Val → IProp GFf:Vall:Vala:Valxs:List ValΦ:Val → IProp GF⊢ □Hf : ∀ x a' ys, □ ∀ Φ, P x ∗ I ys a' -∗ (▷ ∀ r, I (x :: ys) r -∗ Φ r) -∗ WP hl(v(&f) v(&x) v(&a')) {{ Φ }} □IH : ▷ ∀ l a xs Φ, isList l xs -∗ ([∗list] x ∈ xs, P x) -∗ I [] a -∗ (▷ ∀ r, isList l xs ∗ I xs r -∗ Φ r) -∗ WP hl(v(&fold_right) v(&f) v(&a) v(&l)) {{ Φ }} ∗Hl : isList l xs ∗HP : [∗list] x ∈ xs, P x ∗HI : I [] a ∗HΦ : ▷ ∀ r, isList l xs ∗ I xs r -∗ Φ r ⊢ WP hl(v(&fold_right) v(&f) v(&a) v(&l)) {{ Φ }} hlc:HasLCGF:BundledGFunctorsinst✝:HeapLangGS hlc GFP:Val → IProp GFI:List Val → Val → IProp GFf:Vall:Vala:Valxs:List ValΦ:Val → IProp GF⊢ □Hf : ∀ x a' ys, □ ∀ Φ, P x ∗ I ys a' -∗ (▷ ∀ r, I (x :: ys) r -∗ Φ r) -∗ WP hl(v(&f) v(&x) v(&a')) {{ Φ }} □IH : ▷ ∀ l a xs Φ, isList l xs -∗ ([∗list] x ∈ xs, P x) -∗ I [] a -∗ (▷ ∀ r, isList l xs ∗ I xs r -∗ Φ r) -∗ WP hl(v(&fold_right) v(&f) v(&a) v(&l)) {{ Φ }} ∗Hl : isList l xs ∗HP : [∗list] x ∈ xs, P x ∗HI : I [] a ∗HΦ : ▷ ∀ r, isList l xs ∗ I xs r -∗ Φ r ⊢ WP hl(v(&fold_right) v(&f)) {{ v, WP hl(v(&v) v(&a) v(&l)) {{ Φ }} }} hlc:HasLCGF:BundledGFunctorsinst✝:HeapLangGS hlc GFP:Val → IProp GFI:List Val → Val → IProp GFf:Vall:Vala:Valxs:List ValΦ:Val → IProp GF⊢ □Hf : ∀ x a' ys, □ ∀ Φ, P x ∗ I ys a' -∗ (▷ ∀ r, I (x :: ys) r -∗ Φ r) -∗ WP hl(v(&f) v(&x) v(&a')) {{ Φ }} □IH : ∀ l a xs Φ, isList l xs -∗ ([∗list] x ∈ xs, P x) -∗ I [] a -∗ (▷ ∀ r, isList l xs ∗ I xs r -∗ Φ r) -∗ WP hl(v(&fold_right) v(&f) v(&a) v(&l)) {{ Φ }} ∗Hl : isList l xs ∗HP : [∗list] x ∈ xs, P x ∗HI : I [] a ∗HΦ : ∀ r, isList l xs ∗ I xs r -∗ Φ r ⊢ WP hl((λ v l, match l with | injl(_) => v | injr(hd) => let x := fst(!hd); let l' := snd(!hd); v(&f) x (v(&fold_right) v(&f) v l'))) {{ v, WP hl(v(&v) v(&a) v(&l)) {{ Φ }} }} cases xs with hlc:HasLCGF:BundledGFunctorsinst✝:HeapLangGS hlc GFP:Val → IProp GFI:List Val → Val → IProp GFf:Vall:Vala:ValΦ:Val → IProp GF⊢ □Hf : ∀ x a' ys, □ ∀ Φ, P x ∗ I ys a' -∗ (▷ ∀ r, I (x :: ys) r -∗ Φ r) -∗ WP hl(v(&f) v(&x) v(&a')) {{ Φ }} □IH : ∀ l a xs Φ, isList l xs -∗ ([∗list] x ∈ xs, P x) -∗ I [] a -∗ (▷ ∀ r, isList l xs ∗ I xs r -∗ Φ r) -∗ WP hl(v(&fold_right) v(&f) v(&a) v(&l)) {{ Φ }} ∗Hl : isList l [] ∗HP : [∗list] x ∈ [], P x ∗HI : I [] a ∗HΦ : ∀ r, isList l [] ∗ I [] r -∗ Φ r ⊢ WP hl((λ v l, match l with | injl(_) => v | injr(hd) => let x := fst(!hd); let l' := snd(!hd); v(&f) x (v(&fold_right) v(&f) v l'))) {{ v, WP hl(v(&v) v(&a) v(&l)) {{ Φ }} }} hlc:HasLCGF:BundledGFunctorsinst✝:HeapLangGS hlc GFP:Val → IProp GFI:List Val → Val → IProp GFf:Vall:Vala:ValΦ:Val → IProp GFheq:l = hl_val(injl(#()))⊢ □Hf : ∀ x a' ys, □ ∀ Φ, P x ∗ I ys a' -∗ (▷ ∀ r, I (x :: ys) r -∗ Φ r) -∗ WP hl(v(&f) v(&x) v(&a')) {{ Φ }} □IH : ∀ l a xs Φ, isList l xs -∗ ([∗list] x ∈ xs, P x) -∗ I [] a -∗ (▷ ∀ r, isList l xs ∗ I xs r -∗ Φ r) -∗ WP hl(v(&fold_right) v(&f) v(&a) v(&l)) {{ Φ }} ∗Hl : isList l [] ∗HP : [∗list] x ∈ [], P x ∗HI : I [] a ∗HΦ : ∀ r, isList l [] ∗ I [] r -∗ Φ r ⊢ WP hl((λ v l, match l with | injl(_) => v | injr(hd) => let x := fst(!hd); let l' := snd(!hd); v(&f) x (v(&fold_right) v(&f) v l'))) {{ v, WP hl(v(&v) v(&a) v(&l)) {{ Φ }} }}; hlc:HasLCGF:BundledGFunctorsinst✝:HeapLangGS hlc GFP:Val → IProp GFI:List Val → Val → IProp GFf:Vala:ValΦ:Val → IProp GF⊢ □Hf : ∀ x a' ys, □ ∀ Φ, P x ∗ I ys a' -∗ (▷ ∀ r, I (x :: ys) r -∗ Φ r) -∗ WP hl(v(&f) v(&x) v(&a')) {{ Φ }} □IH : ∀ l a xs Φ, isList l xs -∗ ([∗list] x ∈ xs, P x) -∗ I [] a -∗ (▷ ∀ r, isList l xs ∗ I xs r -∗ Φ r) -∗ WP hl(v(&fold_right) v(&f) v(&a) v(&l)) {{ Φ }} ∗Hl : isList (hl_val(injl(#()))) [] ∗HP : [∗list] x ∈ [], P x ∗HI : I [] a ∗HΦ : ∀ r, isList (hl_val(injl(#()))) [] ∗ I [] r -∗ Φ r ⊢ WP hl((λ v l, match l with | injl(_) => v | injr(hd) => let x := fst(!hd); let l' := snd(!hd); v(&f) x (v(&fold_right) v(&f) v l'))) {{ v, WP hl(v(&v) v(&a) (v(injl(#())))) {{ Φ }} }} hlc:HasLCGF:BundledGFunctorsinst✝:HeapLangGS hlc GFP:Val → IProp GFI:List Val → Val → IProp GFf:Vala:ValΦ:Val → IProp GF⊢ □Hf : ∀ x a' ys, □ ∀ Φ, P x ∗ I ys a' -∗ (▷ ∀ r, I (x :: ys) r -∗ Φ r) -∗ WP hl(v(&f) v(&x) v(&a')) {{ Φ }} □IH : ∀ l a xs Φ, isList l xs -∗ ([∗list] x ∈ xs, P x) -∗ I [] a -∗ (▷ ∀ r, isList l xs ∗ I xs r -∗ Φ r) -∗ WP hl(v(&fold_right) v(&f) v(&a) v(&l)) {{ Φ }} ∗Hl : isList (hl_val(injl(#()))) [] ∗HP : [∗list] x ∈ [], P x ∗HI : I [] a ∗HΦ : ∀ r, isList (hl_val(injl(#()))) [] ∗ I [] r -∗ Φ r ⊢ |={⊤}=> Φ a; hlc:HasLCGF:BundledGFunctorsinst✝:HeapLangGS hlc GFP:Val → IProp GFI:List Val → Val → IProp GFf:Vala:ValΦ:Val → IProp GF⊢ □Hf : ∀ x a' ys, □ ∀ Φ, P x ∗ I ys a' -∗ (▷ ∀ r, I (x :: ys) r -∗ Φ r) -∗ WP hl(v(&f) v(&x) v(&a')) {{ Φ }} □IH : ∀ l a xs Φ, isList l xs -∗ ([∗list] x ∈ xs, P x) -∗ I [] a -∗ (▷ ∀ r, isList l xs ∗ I xs r -∗ Φ r) -∗ WP hl(v(&fold_right) v(&f) v(&a) v(&l)) {{ Φ }} ∗Hl : isList (hl_val(injl(#()))) [] ∗HP : [∗list] x ∈ [], P x ∗HI : I [] a ∗HΦ : ∀ r, isList (hl_val(injl(#()))) [] ∗ I [] r -∗ Φ r ⊢ Φ a hlc:HasLCGF:BundledGFunctorsinst✝:HeapLangGS hlc GFP:Val → IProp GFI:List Val → Val → IProp GFf:Vala:ValΦ:Val → IProp GF⊢ □Hf : ∀ x a' ys, □ ∀ Φ, P x ∗ I ys a' -∗ (▷ ∀ r, I (x :: ys) r -∗ Φ r) -∗ WP hl(v(&f) v(&x) v(&a')) {{ Φ }} □IH : ∀ l a xs Φ, isList l xs -∗ ([∗list] x ∈ xs, P x) -∗ I [] a -∗ (▷ ∀ r, isList l xs ∗ I xs r -∗ Φ r) -∗ WP hl(v(&fold_right) v(&f) v(&a) v(&l)) {{ Φ }} ∗Hl : isList (hl_val(injl(#()))) [] ∗HP : [∗list] x ∈ [], P x ∗HI : I [] a ⊢ isList (hl_val(injl(#()))) [] ∗ I [] a hlc:HasLCGF:BundledGFunctorsinst✝:HeapLangGS hlc GFP:Val → IProp GFI:List Val → Val → IProp GFf:Vala:ValΦ:Val → IProp GF⊢ □Hf : ∀ x a' ys, □ ∀ Φ, P x ∗ I ys a' -∗ (▷ ∀ r, I (x :: ys) r -∗ Φ r) -∗ WP hl(v(&f) v(&x) v(&a')) {{ Φ }} □IH : ∀ l a xs Φ, isList l xs -∗ ([∗list] x ∈ xs, P x) -∗ I [] a -∗ (▷ ∀ r, isList l xs ∗ I xs r -∗ Φ r) -∗ WP hl(v(&fold_right) v(&f) v(&a) v(&l)) {{ Φ }} ∗Hl : isList (hl_val(injl(#()))) [] ∗HP : [∗list] x ∈ [], P x ⊢ isList (hl_val(injl(#()))) [] hlc:HasLCGF:BundledGFunctorsinst✝:HeapLangGS hlc GFP:Val → IProp GFI:List Val → Val → IProp GFf:Vala:ValΦ:Val → IProp GF⊢ □Hf : ∀ x a' ys, □ ∀ Φ, P x ∗ I ys a' -∗ (▷ ∀ r, I (x :: ys) r -∗ Φ r) -∗ WP hl(v(&f) v(&x) v(&a')) {{ Φ }} □IH : ∀ l a xs Φ, isList l xs -∗ ([∗list] x ∈ xs, P x) -∗ I [] a -∗ (▷ ∀ r, isList l xs ∗ I xs r -∗ Φ r) -∗ WP hl(v(&fold_right) v(&f) v(&a) v(&l)) {{ Φ }} ∗Hl : isList (hl_val(injl(#()))) [] ∗HP : [∗list] x ∈ [], P x ⊢ ⌜hl_val(injl(#())) = hl_val(injl(#()))⌝ All goals completed! 🐙 hlc:HasLCGF:BundledGFunctorsinst✝:HeapLangGS hlc GFP:Val → IProp GFI:List Val → Val → IProp GFf:Vall:Vala:ValΦ:Val → IProp GFx:Valxs:List Val⊢ □Hf : ∀ x a' ys, □ ∀ Φ, P x ∗ I ys a' -∗ (▷ ∀ r, I (x :: ys) r -∗ Φ r) -∗ WP hl(v(&f) v(&x) v(&a')) {{ Φ }} □IH : ∀ l a xs Φ, isList l xs -∗ ([∗list] x ∈ xs, P x) -∗ I [] a -∗ (▷ ∀ r, isList l xs ∗ I xs r -∗ Φ r) -∗ WP hl(v(&fold_right) v(&f) v(&a) v(&l)) {{ Φ }} ∗Hl : isList l (x :: xs) ∗HP : [∗list] x ∈ x :: xs, P x ∗HI : I [] a ∗HΦ : ∀ r, isList l (x :: xs) ∗ I (x :: xs) r -∗ Φ r ⊢ WP hl((λ v l, match l with | injl(_) => v | injr(hd) => let x := fst(!hd); let l' := snd(!hd); v(&f) x (v(&fold_right) v(&f) v l'))) {{ v, WP hl(v(&v) v(&a) v(&l)) {{ Φ }} }} hlc:HasLCGF:BundledGFunctorsinst✝:HeapLangGS hlc GFP:Val → IProp GFI:List Val → Val → IProp GFf:Vall:Vala:ValΦ:Val → IProp GFx:Valxs:List Valhd:Locl':Valheq:l = hl_val(injr(#hd))⊢ □Hf : ∀ x a' ys, □ ∀ Φ, P x ∗ I ys a' -∗ (▷ ∀ r, I (x :: ys) r -∗ Φ r) -∗ WP hl(v(&f) v(&x) v(&a')) {{ Φ }} □IH : ∀ l a xs Φ, isList l xs -∗ ([∗list] x ∈ xs, P x) -∗ I [] a -∗ (▷ ∀ r, isList l xs ∗ I xs r -∗ Φ r) -∗ WP hl(v(&fold_right) v(&f) v(&a) v(&l)) {{ Φ }} ∗HP : [∗list] x ∈ x :: xs, P x ∗HI : I [] a ∗HΦ : ∀ r, isList l (x :: xs) ∗ I (x :: xs) r -∗ Φ r ∗Hpt : hd ↦ some hl_val((&x, &l')) ∗Hl : isList l' xs ⊢ WP hl((λ v l, match l with | injl(_) => v | injr(hd) => let x := fst(!hd); let l' := snd(!hd); v(&f) x (v(&fold_right) v(&f) v l'))) {{ v, WP hl(v(&v) v(&a) v(&l)) {{ Φ }} }} hlc:HasLCGF:BundledGFunctorsinst✝:HeapLangGS hlc GFP:Val → IProp GFI:List Val → Val → IProp GFf:Vala:ValΦ:Val → IProp GFx:Valxs:List Valhd:Locl':Val⊢ □Hf : ∀ x a' ys, □ ∀ Φ, P x ∗ I ys a' -∗ (▷ ∀ r, I (x :: ys) r -∗ Φ r) -∗ WP hl(v(&f) v(&x) v(&a')) {{ Φ }} □IH : ∀ l a xs Φ, isList l xs -∗ ([∗list] x ∈ xs, P x) -∗ I [] a -∗ (▷ ∀ r, isList l xs ∗ I xs r -∗ Φ r) -∗ WP hl(v(&fold_right) v(&f) v(&a) v(&l)) {{ Φ }} ∗HP : [∗list] x ∈ x :: xs, P x ∗HI : I [] a ∗HΦ : ∀ r, isList (hl_val(injr(#hd))) (x :: xs) ∗ I (x :: xs) r -∗ Φ r ∗Hpt : hd ↦ some hl_val((&x, &l')) ∗Hl : isList l' xs ⊢ WP hl((λ v l, match l with | injl(_) => v | injr(hd) => let x := fst(!hd); let l' := snd(!hd); v(&f) x (v(&fold_right) v(&f) v l'))) {{ v, WP hl(v(&v) v(&a) (v(injr(#hd)))) {{ Φ }} }} hlc:HasLCGF:BundledGFunctorsinst✝:HeapLangGS hlc GFP:Val → IProp GFI:List Val → Val → IProp GFf:Vala:ValΦ:Val → IProp GFx:Valxs:List Valhd:Locl':Val⊢ □Hf : ∀ x a' ys, □ ∀ Φ, P x ∗ I ys a' -∗ (▷ ∀ r, I (x :: ys) r -∗ Φ r) -∗ WP hl(v(&f) v(&x) v(&a')) {{ Φ }} □IH : ∀ l a xs Φ, isList l xs -∗ ([∗list] x ∈ xs, P x) -∗ I [] a -∗ (▷ ∀ r, isList l xs ∗ I xs r -∗ Φ r) -∗ WP hl(v(&fold_right) v(&f) v(&a) v(&l)) {{ Φ }} ∗HI : I [] a ∗HΦ : ∀ r, isList (hl_val(injr(#hd))) (x :: xs) ∗ I (x :: xs) r -∗ Φ r ∗Hpt : hd ↦ some hl_val((&x, &l')) ∗Hl : isList l' xs ∗HP0 : P x ∗HPs : [∗list] y ∈ xs, P y ⊢ WP hl((λ v l, match l with | injl(_) => v | injr(hd) => let x := fst(!hd); let l' := snd(!hd); v(&f) x (v(&fold_right) v(&f) v l'))) {{ v, WP hl(v(&v) v(&a) (v(injr(#hd)))) {{ Φ }} }} hlc:HasLCGF:BundledGFunctorsinst✝:HeapLangGS hlc GFP:Val → IProp GFI:List Val → Val → IProp GFf:Vala:ValΦ:Val → IProp GFx:Valxs:List Valhd:Locl':Val⊢ □Hf : ∀ x a' ys, □ ∀ Φ, P x ∗ I ys a' -∗ (▷ ∀ r, I (x :: ys) r -∗ Φ r) -∗ WP hl(v(&f) v(&x) v(&a')) {{ Φ }} □IH : ∀ l a xs Φ, isList l xs -∗ ([∗list] x ∈ xs, P x) -∗ I [] a -∗ (▷ ∀ r, isList l xs ∗ I xs r -∗ Φ r) -∗ WP hl(v(&fold_right) v(&f) v(&a) v(&l)) {{ Φ }} ∗HI : I [] a ∗HΦ : ∀ r, isList (hl_val(injr(#hd))) (x :: xs) ∗ I (x :: xs) r -∗ Φ r ∗Hpt : hd ↦ some hl_val((&x, &l')) ∗Hl : isList l' xs ∗HP0 : P x ∗HPs : [∗list] y ∈ xs, P y ⊢ WP hl(let x := fst(!#hd); let l' := snd(!#hd); v(&f) x (v(&fold_right) v(&f) v(&a) l')) {{ Φ }} hlc:HasLCGF:BundledGFunctorsinst✝:HeapLangGS hlc GFP:Val → IProp GFI:List Val → Val → IProp GFf:Vala:ValΦ:Val → IProp GFx:Valxs:List Valhd:Locl':Val⊢ □Hf : ∀ x a' ys, □ ∀ Φ, P x ∗ I ys a' -∗ (▷ ∀ r, I (x :: ys) r -∗ Φ r) -∗ WP hl(v(&f) v(&x) v(&a')) {{ Φ }} □IH : ∀ l a xs Φ, isList l xs -∗ ([∗list] x ∈ xs, P x) -∗ I [] a -∗ (▷ ∀ r, isList l xs ∗ I xs r -∗ Φ r) -∗ WP hl(v(&fold_right) v(&f) v(&a) v(&l)) {{ Φ }} ∗HI : I [] a ∗HΦ : ∀ r, isList (hl_val(injr(#hd))) (x :: xs) ∗ I (x :: xs) r -∗ Φ r ∗Hpt : hd ↦ some hl_val((&x, &l')) ∗Hl : isList l' xs ∗HP0 : P x ∗HPs : [∗list] y ∈ xs, P y ⊢ WP hl(let x := fst(v((&x, &l'))); let l' := snd(!#hd); v(&f) x (v(&fold_right) v(&f) v(&a) l')) {{ Φ }} hlc:HasLCGF:BundledGFunctorsinst✝:HeapLangGS hlc GFP:Val → IProp GFI:List Val → Val → IProp GFf:Vala:ValΦ:Val → IProp GFx:Valxs:List Valhd:Locl':Val⊢ □Hf : ∀ x a' ys, □ ∀ Φ, P x ∗ I ys a' -∗ (▷ ∀ r, I (x :: ys) r -∗ Φ r) -∗ WP hl(v(&f) v(&x) v(&a')) {{ Φ }} □IH : ∀ l a xs Φ, isList l xs -∗ ([∗list] x ∈ xs, P x) -∗ I [] a -∗ (▷ ∀ r, isList l xs ∗ I xs r -∗ Φ r) -∗ WP hl(v(&fold_right) v(&f) v(&a) v(&l)) {{ Φ }} ∗HI : I [] a ∗HΦ : ∀ r, isList (hl_val(injr(#hd))) (x :: xs) ∗ I (x :: xs) r -∗ Φ r ∗Hpt : hd ↦ some hl_val((&x, &l')) ∗Hl : isList l' xs ∗HP0 : P x ∗HPs : [∗list] y ∈ xs, P y ⊢ WP hl(let l' := snd(!#hd); v(&f) v(&x) (v(&fold_right) v(&f) v(&a) l')) {{ Φ }} hlc:HasLCGF:BundledGFunctorsinst✝:HeapLangGS hlc GFP:Val → IProp GFI:List Val → Val → IProp GFf:Vala:ValΦ:Val → IProp GFx:Valxs:List Valhd:Locl':Val⊢ □Hf : ∀ x a' ys, □ ∀ Φ, P x ∗ I ys a' -∗ (▷ ∀ r, I (x :: ys) r -∗ Φ r) -∗ WP hl(v(&f) v(&x) v(&a')) {{ Φ }} □IH : ∀ l a xs Φ, isList l xs -∗ ([∗list] x ∈ xs, P x) -∗ I [] a -∗ (▷ ∀ r, isList l xs ∗ I xs r -∗ Φ r) -∗ WP hl(v(&fold_right) v(&f) v(&a) v(&l)) {{ Φ }} ∗HI : I [] a ∗HΦ : ∀ r, isList (hl_val(injr(#hd))) (x :: xs) ∗ I (x :: xs) r -∗ Φ r ∗Hpt : hd ↦ some hl_val((&x, &l')) ∗Hl : isList l' xs ∗HP0 : P x ∗HPs : [∗list] y ∈ xs, P y ⊢ WP hl(let l' := snd(v((&x, &l'))); v(&f) v(&x) (v(&fold_right) v(&f) v(&a) l')) {{ Φ }} hlc:HasLCGF:BundledGFunctorsinst✝:HeapLangGS hlc GFP:Val → IProp GFI:List Val → Val → IProp GFf:Vala:ValΦ:Val → IProp GFx:Valxs:List Valhd:Locl':Val⊢ □Hf : ∀ x a' ys, □ ∀ Φ, P x ∗ I ys a' -∗ (▷ ∀ r, I (x :: ys) r -∗ Φ r) -∗ WP hl(v(&f) v(&x) v(&a')) {{ Φ }} □IH : ∀ l a xs Φ, isList l xs -∗ ([∗list] x ∈ xs, P x) -∗ I [] a -∗ (▷ ∀ r, isList l xs ∗ I xs r -∗ Φ r) -∗ WP hl(v(&fold_right) v(&f) v(&a) v(&l)) {{ Φ }} ∗HI : I [] a ∗HΦ : ∀ r, isList (hl_val(injr(#hd))) (x :: xs) ∗ I (x :: xs) r -∗ Φ r ∗Hpt : hd ↦ some hl_val((&x, &l')) ∗Hl : isList l' xs ∗HP0 : P x ∗HPs : [∗list] y ∈ xs, P y ⊢ WP hl(v(&f) v(&x) (v(&fold_right) v(&f) v(&a) v(&l'))) {{ Φ }} hlc:HasLCGF:BundledGFunctorsinst✝:HeapLangGS hlc GFP:Val → IProp GFI:List Val → Val → IProp GFf:Vala:ValΦ:Val → IProp GFx:Valxs:List Valhd:Locl':Valr:Val⊢ □Hf : ∀ x a' ys, □ ∀ Φ, P x ∗ I ys a' -∗ (▷ ∀ r, I (x :: ys) r -∗ Φ r) -∗ WP hl(v(&f) v(&x) v(&a')) {{ Φ }} □IH : ∀ l a xs Φ, isList l xs -∗ ([∗list] x ∈ xs, P x) -∗ I [] a -∗ (▷ ∀ r, isList l xs ∗ I xs r -∗ Φ r) -∗ WP hl(v(&fold_right) v(&f) v(&a) v(&l)) {{ Φ }} ∗HΦ : ∀ r, isList (hl_val(injr(#hd))) (x :: xs) ∗ I (x :: xs) r -∗ Φ r ∗Hpt : hd ↦ some hl_val((&x, &l')) ∗HP0 : P x ∗Hl : isList l' xs ∗Hr : I xs r ⊢ WP hl(v(&f) v(&x) v(&r)) {{ Φ }} hlc:HasLCGF:BundledGFunctorsinst✝:HeapLangGS hlc GFP:Val → IProp GFI:List Val → Val → IProp GFf:Vala:ValΦ:Val → IProp GFx:Valxs:List Valhd:Locl':Valr:Val⊢ □Hf : ∀ x a' ys, □ ∀ Φ, P x ∗ I ys a' -∗ (▷ ∀ r, I (x :: ys) r -∗ Φ r) -∗ WP hl(v(&f) v(&x) v(&a')) {{ Φ }} □IH : ∀ l a xs Φ, isList l xs -∗ ([∗list] x ∈ xs, P x) -∗ I [] a -∗ (▷ ∀ r, isList l xs ∗ I xs r -∗ Φ r) -∗ WP hl(v(&fold_right) v(&f) v(&a) v(&l)) {{ Φ }} ∗HP0 : P x ∗Hr : I xs r ⊢ P x ∗ I ?m.2461 rhlc:HasLCGF:BundledGFunctorsinst✝:HeapLangGS hlc GFP:Val → IProp GFI:List Val → Val → IProp GFf:Vala:ValΦ:Val → IProp GFx:Valxs:List Valhd:Locl':Valr:Valr':Val⊢ □Hf : ∀ x a' ys, □ ∀ Φ, P x ∗ I ys a' -∗ (▷ ∀ r, I (x :: ys) r -∗ Φ r) -∗ WP hl(v(&f) v(&x) v(&a')) {{ Φ }} □IH : ∀ l a xs Φ, isList l xs -∗ ([∗list] x ∈ xs, P x) -∗ I [] a -∗ (▷ ∀ r, isList l xs ∗ I xs r -∗ Φ r) -∗ WP hl(v(&fold_right) v(&f) v(&a) v(&l)) {{ Φ }} ∗HΦ : ∀ r, isList (hl_val(injr(#hd))) (x :: xs) ∗ I (x :: xs) r -∗ Φ r ∗Hpt : hd ↦ some hl_val((&x, &l')) ∗Hl : isList l' xs ∗Hr' : I (x :: ?m.2461) r' ⊢ Φ r'hlc:HasLCGF:BundledGFunctorsinst✝:HeapLangGS hlc GFP:Val → IProp GFI:List Val → Val → IProp GFf:Vala:ValΦ:Val → IProp GFx:Valxs:List Valhd:Locl':Valr:Val⊢ List Valhlc:HasLCGF:BundledGFunctorsinst✝:HeapLangGS hlc GFP:Val → IProp GFI:List Val → Val → IProp GFf:Vala:ValΦ:Val → IProp GFx:Valxs:List Valhd:Locl':Valr:Val⊢ List Valhlc:HasLCGF:BundledGFunctorsinst✝:HeapLangGS hlc GFP:Val → IProp GFI:List Val → Val → IProp GFf:Vala:ValΦ:Val → IProp GFx:Valxs:List Valhd:Locl':Valr:Val⊢ List Val hlc:HasLCGF:BundledGFunctorsinst✝:HeapLangGS hlc GFP:Val → IProp GFI:List Val → Val → IProp GFf:Vala:ValΦ:Val → IProp GFx:Valxs:List Valhd:Locl':Valr:Val⊢ □Hf : ∀ x a' ys, □ ∀ Φ, P x ∗ I ys a' -∗ (▷ ∀ r, I (x :: ys) r -∗ Φ r) -∗ WP hl(v(&f) v(&x) v(&a')) {{ Φ }} □IH : ∀ l a xs Φ, isList l xs -∗ ([∗list] x ∈ xs, P x) -∗ I [] a -∗ (▷ ∀ r, isList l xs ∗ I xs r -∗ Φ r) -∗ WP hl(v(&fold_right) v(&f) v(&a) v(&l)) {{ Φ }} ∗HP0 : P x ∗Hr : I xs r ⊢ P x ∗ I ?m.2461 r All goals completed! 🐙 hlc:HasLCGF:BundledGFunctorsinst✝:HeapLangGS hlc GFP:Val → IProp GFI:List Val → Val → IProp GFf:Vala:ValΦ:Val → IProp GFx:Valxs:List Valhd:Locl':Valr:Valr':Val⊢ □Hf : ∀ x a' ys, □ ∀ Φ, P x ∗ I ys a' -∗ (▷ ∀ r, I (x :: ys) r -∗ Φ r) -∗ WP hl(v(&f) v(&x) v(&a')) {{ Φ }} □IH : ∀ l a xs Φ, isList l xs -∗ ([∗list] x ∈ xs, P x) -∗ I [] a -∗ (▷ ∀ r, isList l xs ∗ I xs r -∗ Φ r) -∗ WP hl(v(&fold_right) v(&f) v(&a) v(&l)) {{ Φ }} ∗HΦ : ∀ r, isList (hl_val(injr(#hd))) (x :: xs) ∗ I (x :: xs) r -∗ Φ r ∗Hpt : hd ↦ some hl_val((&x, &l')) ∗Hl : isList l' xs ∗Hr' : I (x :: xs) r' ⊢ Φ r' hlc:HasLCGF:BundledGFunctorsinst✝:HeapLangGS hlc GFP:Val → IProp GFI:List Val → Val → IProp GFf:Vala:ValΦ:Val → IProp GFx:Valxs:List Valhd:Locl':Valr:Valr':Val⊢ □Hf : ∀ x a' ys, □ ∀ Φ, P x ∗ I ys a' -∗ (▷ ∀ r, I (x :: ys) r -∗ Φ r) -∗ WP hl(v(&f) v(&x) v(&a')) {{ Φ }} □IH : ∀ l a xs Φ, isList l xs -∗ ([∗list] x ∈ xs, P x) -∗ I [] a -∗ (▷ ∀ r, isList l xs ∗ I xs r -∗ Φ r) -∗ WP hl(v(&fold_right) v(&f) v(&a) v(&l)) {{ Φ }} ∗Hpt : hd ↦ some hl_val((&x, &l')) ∗Hl : isList l' xs ∗Hr' : I (x :: xs) r' ⊢ isList (hl_val(injr(#hd))) (x :: xs) ∗ I (x :: xs) r' hlc:HasLCGF:BundledGFunctorsinst✝:HeapLangGS hlc GFP:Val → IProp GFI:List Val → Val → IProp GFf:Vala:ValΦ:Val → IProp GFx:Valxs:List Valhd:Locl':Valr:Valr':Val⊢ □Hf : ∀ x a' ys, □ ∀ Φ, P x ∗ I ys a' -∗ (▷ ∀ r, I (x :: ys) r -∗ Φ r) -∗ WP hl(v(&f) v(&x) v(&a')) {{ Φ }} □IH : ∀ l a xs Φ, isList l xs -∗ ([∗list] x ∈ xs, P x) -∗ I [] a -∗ (▷ ∀ r, isList l xs ∗ I xs r -∗ Φ r) -∗ WP hl(v(&fold_right) v(&f) v(&a) v(&l)) {{ Φ }} ∗Hpt : hd ↦ some hl_val((&x, &l')) ∗Hl : isList l' xs ⊢ isList (hl_val(injr(#hd))) (x :: xs) hlc:HasLCGF:BundledGFunctorsinst✝:HeapLangGS hlc GFP:Val → IProp GFI:List Val → Val → IProp GFf:Vala:ValΦ:Val → IProp GFx:Valxs:List Valhd:Locl':Valr:Valr':Val⊢ □Hf : ∀ x a' ys, □ ∀ Φ, P x ∗ I ys a' -∗ (▷ ∀ r, I (x :: ys) r -∗ Φ r) -∗ WP hl(v(&f) v(&x) v(&a')) {{ Φ }} □IH : ∀ l a xs Φ, isList l xs -∗ ([∗list] x ∈ xs, P x) -∗ I [] a -∗ (▷ ∀ r, isList l xs ∗ I xs r -∗ Φ r) -∗ WP hl(v(&fold_right) v(&f) v(&a) v(&l)) {{ Φ }} ∗Hpt : hd ↦ some hl_val((&x, &l')) ∗Hl : isList l' xs ⊢ ∃ hd_1 l', ⌜hl_val(injr(#hd)) = hl_val(injr(#hd_1))⌝ ∗ hd_1 ↦ some hl_val((&x, &l')) ∗ isList l' xs hlc:HasLCGF:BundledGFunctorsinst✝:HeapLangGS hlc GFP:Val → IProp GFI:List Val → Val → IProp GFf:Vala:ValΦ:Val → IProp GFx:Valxs:List Valhd:Locl':Valr:Valr':Val⊢ □Hf : ∀ x a' ys, □ ∀ Φ, P x ∗ I ys a' -∗ (▷ ∀ r, I (x :: ys) r -∗ Φ r) -∗ WP hl(v(&f) v(&x) v(&a')) {{ Φ }} □IH : ∀ l a xs Φ, isList l xs -∗ ([∗list] x ∈ xs, P x) -∗ I [] a -∗ (▷ ∀ r, isList l xs ∗ I xs r -∗ Φ r) -∗ WP hl(v(&fold_right) v(&f) v(&a) v(&l)) {{ Φ }} ∗Hpt : hd ↦ some hl_val((&x, &l')) ∗Hl : isList l' xs ⊢ ⌜hl_val(injr(#hd)) = hl_val(injr(#hd))⌝ ∗ hd ↦ some hl_val((&x, &l')) ∗ isList l' xs hlc:HasLCGF:BundledGFunctorsinst✝:HeapLangGS hlc GFP:Val → IProp GFI:List Val → Val → IProp GFf:Vala:ValΦ:Val → IProp GFx:Valxs:List Valhd:Locl':Valr:Valr':Val⊢ □Hf : ∀ x a' ys, □ ∀ Φ, P x ∗ I ys a' -∗ (▷ ∀ r, I (x :: ys) r -∗ Φ r) -∗ WP hl(v(&f) v(&x) v(&a')) {{ Φ }} □IH : ∀ l a xs Φ, isList l xs -∗ ([∗list] x ∈ xs, P x) -∗ I [] a -∗ (▷ ∀ r, isList l xs ∗ I xs r -∗ Φ r) -∗ WP hl(v(&fold_right) v(&f) v(&a) v(&l)) {{ Φ }} ⊢ ⌜hl_val(injr(#hd)) = hl_val(injr(#hd))⌝ All goals completed! 🐙

7.5. Arithmetic-dependent specifications🔗

Two further functions on lists are worth defining: inc, which increments every element in place, and sum_list, which sums a list by folding addition over it.

def inc : Val := hl_val% rec inc l := match l with | none() => #0 | some(hd) => let x := fst(!hd); let l' := snd(!hd); hd ← (x + #1, l'); inc l' def sum_list : Val := hl_val% λ l, let f := (λ x y, x + y); &fold_right f #0 l

Both functions use integer arithmetic, which wp_pures can execute. As further exercises, specify and prove that inc increments every integer in the list and that sum_list returns their sum. The load/store and fold specifications above provide the building blocks.

end LinkedLists