Definition: A-eval
A-eval(AModel) == snd(snd(snd(snd(snd(snd(snd(snd(snd(snd(AModel))))))))))
Definition: A-return
A-return(AModel) == fst(AModel)
Definition: A-pre-val
A-pre-val(AType;A;i) == idx(AType) i A
Definition: monad
This definition of monad is the one that functional programmers use.
There is a categorical definition of monad in the section on category theory,
and a proof that from a monad as defined here, one can construct a category
theoretical monad over the category of Types.⋅
Monad ==
M:Type ⟶ Type
× return:⋂T:Type. (T ⟶ (M T))
× bind:⋂T,S:Type. ((M T) ⟶ (T ⟶ (M S)) ⟶ (M S))
× leftunit:∀[T,S:Type]. ∀[x:T]. ∀[f:T ⟶ (M S)]. ((bind (return x) f) = (f x) ∈ (M S))
× rightunit:∀[T:Type]. ∀[m:M T]. ((bind m return) = m ∈ (M T))
× (∀[T,S,U:Type]. ∀[m:M T]. ∀[f:T ⟶ (M S)]. ∀[g:S ⟶ (M U)].
((bind (bind m f) g) = (bind m (λx.(bind (f x) g))) ∈ (M U)))
Lemma: monad_wf
Monad ∈ 𝕌'
Definition: M-map
M-map(mnd) == fst(mnd)
Lemma: M-map_wf
∀[Mnd:Monad]. (M-map(Mnd) ∈ Type ⟶ Type)
Definition: M-return
M-return(Mnd) == fst(snd(Mnd))
Lemma: M-return_wf
∀[Mnd:Monad]. (M-return(Mnd) ∈ ⋂T:Type. (T ⟶ (M-map(Mnd) T)))
Definition: M-bind
M-bind(Mnd) == fst(snd(snd(Mnd)))
Lemma: M-bind_wf
∀[Mnd:Monad]. (M-bind(Mnd) ∈ ⋂T,S:Type. ((M-map(Mnd) T) ⟶ (T ⟶ (M-map(Mnd) S)) ⟶ (M-map(Mnd) S)))
Lemma: M-leftunit
∀[Mnd:Monad]. ∀[T,S:Type]. ∀[x:T]. ∀[f:T ⟶ (M-map(Mnd) S)].
((M-bind(Mnd) (M-return(Mnd) x) f) = (f x) ∈ (M-map(Mnd) S))
Lemma: M-rightunit
∀[Mnd:Monad]. ∀[T:Type]. ∀[m:M-map(Mnd) T]. ((M-bind(Mnd) m M-return(Mnd)) = m ∈ (M-map(Mnd) T))
Lemma: M-associative
∀[Mnd:Monad]. ∀[T,S,U:Type]. ∀[m:M-map(Mnd) T]. ∀[f:T ⟶ (M-map(Mnd) S)]. ∀[g:S ⟶ (M-map(Mnd) U)].
((M-bind(Mnd) (M-bind(Mnd) m f) g) = (M-bind(Mnd) m (λx.(M-bind(Mnd) (f x) g))) ∈ (M-map(Mnd) U))
Definition: mk_monad
mk_monad(M;return;bind) == <M, return, bind, Ax, Ax, Ax>
Lemma: mk_monad_wf
∀[M:Type ⟶ Type]. ∀[return:⋂T:Type. (T ⟶ (M T))]. ∀[bind:⋂T,S:Type. ((M T) ⟶ (T ⟶ (M S)) ⟶ (M S))].
(mk_monad(M;return;bind) ∈ Monad) supposing
((∀[T,S,U:Type]. ∀[m:M T]. ∀[f:T ⟶ (M S)]. ∀[g:S ⟶ (M U)].
((bind (bind m f) g) = (bind m (λx.(bind (f x) g))) ∈ (M U))) and
(∀[T:Type]. ∀[m:M T]. ((bind m return) = m ∈ (M T))) and
(∀[T,S:Type]. ∀[x:T]. ∀f:T ⟶ (M S). ((bind (return x) f) = (f x) ∈ (M S))))
Lemma: member-concat-map
∀[T,S:Type]. ∀f:T ⟶ (S List). ∀L:T List. ∀x:S. ((x ∈ concat(map(f;L))) ⇐⇒ (∃t∈L. (x ∈ f t)))
Definition: list-monad
ListMonad == mk_monad(λT.(T List);λx.[x];λL,f. concat(map(f;L)))
Lemma: list-monad_wf
ListMonad ∈ Monad
Comment: Notes on arrays
An element of array(Val;n) is a structure that implements arrays of length n
holding values of type Val. It's a tuple containing a type (whose elements
are the array values) and operations
idx -- that returns the value at a given index
upd -- that returns an array with an updated entry
newarrray -- that returns an array with all values initialized
to a given value
These are the operations used for illustrative purposes in Wadlers' paper
"Monads for Functional Programming." Thus, we can treat an array as an
abstract datatype by simply carrying around an array(Val;n) as a parameter.
(Note: we'll need more if we want to model arrays that are only partially
filled -- and, e.g., be able to prove that we're not trying to access an
uninitialized slot.)
Following Wadler's paper we define two monads:
array-monad(AType)
takes as its argument an AType : array(Val;n) for someVal and n. This is
about operations that potentially transform the state of an array,
array-monad'(AType)
is just about reading, without transforming, an array.
Wadler then puts together an abstract data type from their operations,
together with a coercion function and some other operations defined in terms
of the array ops. Ideally, we'd make this into an abstract
data type, too -- but that's not so easy, because it doesn't seem to satisfy
simple first-order axioms. (And I'm not sure we'd gain anything by defining
the abstract data type by existential quantification.)
The signature of that abstract data type (plus some extra operations) is given by
array-model-type(AType;Val;n)
(Each of these takes an initial parameter that is an instance of an array-model.)
For members of this type we introduce the selectors that pluck out its
operations
A-return, A-bind, A-block, A-assign,
A-return', A-bind', A-fetch',
A-coerce
The extra operations are
A-map
A-map'
A-map and A-map' export the two monad "M" functions, but hide the underlying types.
As far as array-model-type is concerned, A-map and A-map' simply have the
type Type -> Type. (Note that the wf lemmas for the other eight operations
are expressed in terms of A-map and A-map', not the "M" functions implement
them.)
So now we ought to be able to write array programs using just these ten
operations. To make these readable we need good display forms -- which, for
now, is deferred.
Consider simple-swap-test. Given the computation prog, which returns a
value in Unit
simple-swap-test(...;prog;i;j)
is a computation that returns a value in Bool whose meaning is that prog has
swapped the values at indices i and j. (Oops -- I forgot to say that all other
indices have the same value.) The spec of a swap program is that
given any initial state A,
assert (pi1 (simple-swap-test(...;prog;i;j) A))
We can't do that application directly. We have to break the abstraction by
including anoperation
A-eval(AModel): isect{T:Type} (A-map(array-model(AType)) T) -> Arr(AType) -> T
defined as
eval(AModel) == \m,A. pi1(m A)
Then we the specification becomes
forall i,j,k: N_n. forall A:Arr(AType).
assert(A-eval(AModel) simple-swap-test(...;prog;i;j) A))
The eval operation would be purely a specification construct, not available
for writing programs. Or is there a better way to do this? (Maybe the problem here
is to have made the whole state a single array; thus, the initial state does not
really represent a single data object for the program to manipulate.)
Also ... how do we representthe return value of a?
⋅
Definition: array
array{i:l}(Val;n) ==
Arr:Type
× idx:ℕn ⟶ Arr ⟶ Val
× upd:ℕn ⟶ Val ⟶ Arr ⟶ Arr
× newarray:Val ⟶ Arr
× ∀[i:ℕn]. ∀[v:Val]. ((idx i (newarray v)) = v ∈ Val)
× (∀[i,j:ℕn]. ∀[x:Arr]. ∀[v:Val]. ((idx i (upd j v x)) = if (i =z j) then v else idx i x fi ∈ Val))
Lemma: array_wf
∀[Val:Type]. ∀[n:ℕ]. (array{i:l}(Val;n) ∈ 𝕌')
Lemma: array_subtype
∀[Val1,Val2:Type]. ∀[m,n:ℕ].
(array{i:l}(Val1;m) ⊆r array{i:l}(Val2;n)) supposing ((n ≤ m) and ((Val1 ⊆r Val2) ∧ (Val2 ⊆r Val1)))
Definition: Arr
Arr(AType) == fst(AType)
Lemma: Arr_wf
∀[Val:Type]. ∀[n:ℕ]. ∀[AType:array{i:l}(Val;n)]. (Arr(AType) ∈ Type)
Definition: idx
idx(AType) == fst(snd(AType))
Lemma: idx_wf
∀[Val:Type]. ∀[n:ℕ]. ∀[AType:array{i:l}(Val;n)]. (idx(AType) ∈ ℕn ⟶ Arr(AType) ⟶ Val)
Definition: upd
upd(AType) == fst(snd(snd(AType)))
Lemma: upd_wf
∀[Val:Type]. ∀[n:ℕ]. ∀[AType:array{i:l}(Val;n)]. (upd(AType) ∈ ℕn ⟶ Val ⟶ Arr(AType) ⟶ Arr(AType))
Definition: newarray
newarray(AType) == fst(snd(snd(snd(AType))))
Lemma: newarray_wf
∀[Val:Type]. ∀[n:ℕ]. ∀[AType:array{i:l}(Val;n)]. (newarray(AType) ∈ Val ⟶ Arr(AType))
Definition: mk_array
mk_array(Arr;idx;upd;newarray) == <Arr, idx, upd, newarray, Ax, Ax>
Lemma: mk_array_wf
∀[Val:Type]. ∀[n:ℕ]. ∀[Arr:Type]. ∀[idx:ℕn ⟶ Arr ⟶ Val]. ∀[upd:ℕn ⟶ Val ⟶ Arr ⟶ Arr]. ∀[newarray:Val ⟶ Arr].
mk_array(Arr;idx;upd;newarray) ∈ array{i:l}(Val;n)
supposing (∀i:ℕn. ∀v:Val. ((idx i (newarray v)) = v ∈ Val))
∧ (∀i,j:ℕn. ∀x:Arr. ∀v:Val. ((idx i (upd j v x)) = if (i =z j) then v else idx i x fi ∈ Val))
Definition: fn_array
fn_array{i:l}(Val;n) == mk_array(ℕn ⟶ Val;λi,f. (f i);λi,v,f,k. if (k =z i) then v else f k fi ;λv,i. v)
Lemma: fn_array_wf
∀[Val:Type]. ∀[n:ℕ]. (fn_array{i:l}(Val;n) ∈ array{i:l}(Val;n))
Definition: array-monad
array-monad(AType) ==
mk_monad(λT.(Arr(AType) ⟶ (T × Arr(AType)));λv,A. <v, A>;λm,k,A. let v = fst((m A)) in let A' = snd((m A)) in k v A')
Lemma: array-monad_wf
∀[Val:Type]. ∀[n:ℕ]. ∀[AType:array{i:l}(Val;n)]. (array-monad(AType) ∈ Monad)
Definition: array-monad'
array-monad'(AType) == mk_monad(λT.(Arr(AType) ⟶ T);λv,A. v;λm,k,A. (k (m A) A))
Lemma: array-monad'_wf
∀[Val:Type]. ∀[n:ℕ]. ∀[AType:array{i:l}(Val;n)]. (array-monad'(AType) ∈ Monad)
Definition: array-model-type
array-model-type{i:l}(AType;Val;n) ==
let Mnd = array-monad(AType) in
let Mnd' = array-monad'(AType) in
⋂T:Type. (T ⟶ (M-map(Mnd) T))
× ⋂T,S:Type. ((M-map(Mnd) T) ⟶ (T ⟶ (M-map(Mnd) S)) ⟶ (M-map(Mnd) S))
× ⋂T:Type. (Val ⟶ (M-map(Mnd) T) ⟶ T)
× ℕn ⟶ Val ⟶ (M-map(Mnd) Unit)
× ⋂T:Type. (T ⟶ (M-map(Mnd') T))
× ⋂T,S:Type. ((M-map(Mnd') T) ⟶ (T ⟶ (M-map(Mnd') S)) ⟶ (M-map(Mnd') S))
× ℕn ⟶ (M-map(Mnd') Val)
× ⋂T:Type. ((M-map(Mnd') T) ⟶ (M-map(Mnd) T))
× Type ⟶ Type
× Type ⟶ Type
× (⋂T:Type. ((Arr(AType) ⟶ (T × Arr(AType))) ⟶ Arr(AType) ⟶ T))
Lemma: array-model-type_wf
∀[Val:Type]. ∀[n:ℕ]. ∀[AType:array{i:l}(Val;n)]. (array-model-type{i:l}(AType;Val;n) ∈ 𝕌')
Definition: array-model
array-model(AType) ==
<M-return(array-monad(AType))
, M-bind(array-monad(AType))
, λv,m. (fst((m (newarray(AType) v))))
, λi,v,A. <⋅, upd(AType) i v A>
, M-return(array-monad'(AType))
, M-bind(array-monad'(AType))
, λi,A. (idx(AType) i A)
, λm,A. <m A, A>
, M-map(array-monad(AType))
, M-map(array-monad'(AType))
, λm,A. (fst((m A)))>
Lemma: array-model_wf
∀[Val:Type]. ∀[n:ℕ]. ∀[AType:array{i:l}(Val;n)]. (array-model(AType) ∈ array-model-type{i:l}(AType;Val;n))
Definition: A-map
A-map == fst(snd(snd(snd(snd(snd(snd(snd(snd(AModel)))))))))
Lemma: A-map_wf
∀[Val:Type]. ∀[n:ℕ]. ∀[AType:array{i:l}(Val;n)]. (A-map ∈ Type ⟶ Type)
Definition: A-map'
A-map'(AModel) == fst(snd(snd(snd(snd(snd(snd(snd(snd(snd(AModel))))))))))
Lemma: A-map'_wf
∀[Val:Type]. ∀[n:ℕ]. ∀[AType:array{i:l}(Val;n)]. (A-map'(array-model(AType)) ∈ Type ⟶ Type)
Lemma: A-eval_wf
∀[Val:Type]. ∀[n:ℕ]. ∀[AType:array{i:l}(Val;n)]. (A-eval(array-model(AType)) ∈ ⋂T:Type. ((A-map T) ⟶ Arr(AType) ⟶ T))
Lemma: A-eval_wf2
∀[Val:Type]. ∀[n:ℕ]. ∀[AType:array{i:l}(Val;n)]. ∀[T:Type]. ∀[m:A-map T]. ∀[A:Arr(AType)].
(A-eval(array-model(AType)) m A ∈ T)
Lemma: A-return_wf
∀[Val:Type]. ∀[n:ℕ]. ∀[AType:array{i:l}(Val;n)]. (A-return(array-model(AType)) ∈ ⋂T:Type. (T ⟶ (A-map T)))
Definition: A-bind
A-bind(AModel) == fst(snd(AModel))
Lemma: A-bind_wf
∀[Val:Type]. ∀[n:ℕ]. ∀[AType:array{i:l}(Val;n)]. ∀[T,S:Type].
(A-bind(array-model(AType)) ∈ (A-map T) ⟶ (T ⟶ (A-map S)) ⟶ (A-map S))
Lemma: A-bind_wf2
∀[Val:Type]. ∀[n:ℕ]. ∀[AType:array{i:l}(Val;n)].
(A-bind(array-model(AType)) ∈ ⋂T,S:Type. ((A-map T) ⟶ (T ⟶ (A-map S)) ⟶ (A-map S)))
Lemma: A-bind_wf3
∀[AType:⋃Val:Type.⋃n:ℕ.array{i:l}(Val;n)]
(A-bind(array-model(AType)) ∈ ⋂T,S:Type. ((A-map T) ⟶ (T ⟶ (A-map S)) ⟶ (A-map S)))
Definition: A-block
A-block(AModel) == fst(snd(snd(AModel)))
Lemma: A-block_wf
∀[Val:Type]. ∀[n:ℕ]. ∀[AType:array{i:l}(Val;n)]. ∀[T:Type].
(A-block(array-model(AType)) ∈ ⋂T:Type. (Val ⟶ (A-map T) ⟶ T))
Definition: A-assign
A-assign(AModel) == fst(snd(snd(snd(AModel))))
Lemma: A-assign_wf
∀[Val:Type]. ∀[n:ℕ]. ∀[AType:array{i:l}(Val;n)]. (A-assign(array-model(AType)) ∈ ℕn ⟶ Val ⟶ (A-map Unit))
Definition: A-return'
A-return'(AModel) == fst(snd(snd(snd(snd(AModel)))))
Lemma: A-return'_wf
∀[Val:Type]. ∀[n:ℕ]. ∀[AType:array{i:l}(Val;n)].
(A-return'(array-model(AType)) ∈ ⋂T:Type. (T ⟶ (A-map'(array-model(AType)) T)))
Definition: A-bind'
A-bind'(AModel) == fst(snd(snd(snd(snd(snd(AModel))))))
Lemma: A-bind'_wf
∀[Val:Type]. ∀[n:ℕ]. ∀[AType:array{i:l}(Val;n)]. ∀[T,S:Type].
(A-bind'(array-model(AType)) ∈ (A-map'(array-model(AType)) T)
⟶ (T ⟶ (A-map'(array-model(AType)) S))
⟶ (A-map'(array-model(AType)) S))
Definition: A-fetch'
A-fetch'(AModel) == fst(snd(snd(snd(snd(snd(snd(AModel)))))))
Lemma: A-fetch'_wf
∀[Val:Type]. ∀[n:ℕ]. ∀[AType:array{i:l}(Val;n)].
(A-fetch'(array-model(AType)) ∈ ℕn ⟶ (A-map'(array-model(AType)) Val))
Definition: A-coerce
A-coerce(AModel) == fst(snd(snd(snd(snd(snd(snd(snd(AModel))))))))
Lemma: A-coerce_wf
∀[Val:Type]. ∀[n:ℕ]. ∀[AType:array{i:l}(Val;n)].
(A-coerce(array-model(AType)) ∈ ⋂T:Type. ((A-map'(array-model(AType)) T) ⟶ (A-map T)))
Definition: A-fetch
A-fetch(AModel) == λi.(A-coerce(AModel) (A-fetch'(AModel) i))
Lemma: A-fetch_wf
∀[Val:Type]. ∀[n:ℕ]. ∀[AType:array{i:l}(Val;n)]. (A-fetch(array-model(AType)) ∈ ℕn ⟶ (A-map Val))
Lemma: A-leftunit
∀[Val:Type]. ∀[n:ℕ]. ∀[AType:array{i:l}(Val;n)]. ∀[T,S:Type]. ∀[x:T]. ∀[f:T ⟶ (A-map S)].
((A-bind(array-model(AType)) (A-return(array-model(AType)) x) f) = (f x) ∈ (A-map S))
Lemma: A-leftunit'
∀[Val:Type]. ∀[n:ℕ]. ∀[AType:array{i:l}(Val;n)]. ∀[T,S:Type]. ∀[x:T]. ∀[f:T ⟶ (A-map'(array-model(AType)) S)].
((A-bind'(array-model(AType)) (A-return'(array-model(AType)) x) f) = (f x) ∈ (A-map'(array-model(AType)) S))
Lemma: A-rightunit
∀Val:Type. ∀n:ℕ. ∀AType:array{i:l}(Val;n). ∀T:Type. ∀m:A-map T.
((A-bind(array-model(AType)) m A-return(array-model(AType))) = m ∈ (A-map T))
Lemma: A-rightunit'
∀Val:Type. ∀n:ℕ. ∀AType:array{i:l}(Val;n). ∀T:Type. ∀m:A-map'(array-model(AType)) T.
((A-bind'(array-model(AType)) m A-return'(array-model(AType))) = m ∈ (A-map'(array-model(AType)) T))
Lemma: A-associative
∀[Val:Type]. ∀[n:ℕ]. ∀[AType:array{i:l}(Val;n)]. ∀[T,S,U:Type]. ∀[m:A-map T]. ∀[f:T ⟶ (A-map S)]. ∀[g:S ⟶ (A-map U)].
((A-bind(array-model(AType)) (A-bind(array-model(AType)) m f) g)
= (A-bind(array-model(AType)) m (λx.(A-bind(array-model(AType)) (f x) g)))
∈ (A-map U))
Lemma: A-associative'
∀[Val:Type]. ∀[n:ℕ]. ∀[AType:array{i:l}(Val;n)]. ∀[T,S,U:Type]. ∀[m:A-map'(array-model(AType)) T].
∀[f:T ⟶ (A-map'(array-model(AType)) S)]. ∀[g:S ⟶ (A-map'(array-model(AType)) U)].
((A-bind'(array-model(AType)) (A-bind'(array-model(AType)) m f) g)
= (A-bind'(array-model(AType)) m (λx.(A-bind'(array-model(AType)) (f x) g)))
∈ (A-map'(array-model(AType)) U))
Definition: A-post-val
A-post-val(AType;prog;A;i) ==
A-eval(array-model(AType))
(A-bind(array-model(AType)) prog (λx.(A-coerce(array-model(AType)) (A-fetch'(array-model(AType)) i))))
A
Lemma: A-post-val_wf
∀[Val:Type]. ∀[n:ℕ]. ∀[AType:array{i:l}(Val;n)]. ∀[prog:A-map Unit]. ∀[A:Arr(AType)]. ∀[i:ℕn].
(A-post-val(AType;prog;A;i) ∈ Val)
Lemma: A-pre-val_wf
∀[Val:Type]. ∀[n:ℕ]. ∀[AType:array{i:l}(Val;n)]. ∀[A:Arr(AType)]. ∀[i:ℕn]. (A-pre-val(AType;A;i) ∈ Val)
Definition: A-null
A-null(AType) == A-return(array-model(AType)) ⋅
Lemma: A-null_wf
∀[Val:Type]. ∀[n:ℕ]. ∀[AType:array{i:l}(Val;n)]. (A-null(AType) ∈ A-map Unit)
Lemma: A-null-property
∀[Val:Type]. ∀[n:ℕ]. ∀[AType:array{i:l}(Val;n)].
∀A:Arr(AType). ∀k:ℕn. (A-post-val(AType;A-null(AType);A;k) = A-pre-val(AType;A;k) ∈ Val)
Lemma: fetch'-commutes
∀[Val,S:Type]. ∀[n:ℕ]. ∀[AType:array{i:l}(Val;n)]. ∀[prog:Val ⟶ Val ⟶ (A-map'(array-model(AType)) S)].
∀j,k:ℕn.
((A-bind'(array-model(AType)) (A-fetch'(array-model(AType)) k)
(λval@k.(A-bind'(array-model(AType)) (A-fetch'(array-model(AType)) j) (λval@j.(prog val@k val@j)))))
= (A-bind'(array-model(AType)) (A-fetch'(array-model(AType)) j)
(λval@j.(A-bind'(array-model(AType)) (A-fetch'(array-model(AType)) k) (λval@k.(prog val@k val@j)))))
∈ (A-map'(array-model(AType)) S))
Lemma: coerce-fetch'-commutes
∀[Val,S:Type]. ∀[n:ℕ]. ∀[AType:array{i:l}(Val;n)]. ∀[prog:Val ⟶ Val ⟶ (A-map S)].
∀j,k:ℕn.
((A-bind(array-model(AType)) (A-coerce(array-model(AType)) (A-fetch'(array-model(AType)) k))
(λval@k.(A-bind(array-model(AType)) (A-coerce(array-model(AType)) (A-fetch'(array-model(AType)) j))
(λval@j.(prog val@k val@j)))))
= (A-bind(array-model(AType)) (A-coerce(array-model(AType)) (A-fetch'(array-model(AType)) j))
(λval@j.(A-bind(array-model(AType)) (A-coerce(array-model(AType)) (A-fetch'(array-model(AType)) k))
(λval@k.(prog val@k val@j)))))
∈ (A-map S))
Definition: A-loop
A-loop(AType;lo;hi;body) ==
fix((λA-loop,hi. if hi ≤z lo
then A-null(AType)
else A-bind(array-model(AType)) (A-loop (hi - 1)) (λx.(body (hi - 1)))
fi ))
hi
Lemma: A-loop_wf
∀[Val:Type]. ∀[n:ℕ]. ∀[AType:array{i:l}(Val;n)].
∀lo:ℕn. ∀k:ℕ. (k < n - lo ⇒ (∀[body:{lo..lo + k-} ⟶ (A-map Unit)]. (A-loop(AType;lo;lo + k;body) ∈ A-map Unit)))
Lemma: A-loop_wf2
∀[Val:Type]. ∀[n:ℕ]. ∀[AType:array{i:l}(Val;n)].
∀lo,hi:ℕn. ∀[body:{lo..hi-} ⟶ (A-map Unit)]. (A-loop(AType;lo;hi;body) ∈ A-map Unit)
Lemma: A-null-loop
∀[Val:Type]. ∀[n:ℕ]. ∀[AType:array{i:l}(Val;n)].
∀lo,hi:ℕn. ∀body:{lo..hi-} ⟶ (A-map Unit). ((hi ≤ lo) ⇒ (A-loop(AType;lo;hi;body) = A-null(AType) ∈ (A-map Unit)))
Definition: simple-swap-test
simple-swap-test(AModel;prog;i;j) ==
A-bind(AModel) (A-coerce(AModel) (A-fetch'(AModel) i))
(λin@i.(A-bind(AModel) (A-coerce(AModel) (A-fetch'(AModel) j))
(λin@j.(A-bind(AModel) prog
(λx.(A-bind(AModel) (A-coerce(AModel) (A-fetch'(AModel) i))
(λout@i.(A-bind(AModel) (A-coerce(AModel) (A-fetch'(AModel) j))
(λout@j.(A-return(AModel) ((out@i =z in@j) ∧b (out@j =z in@i))))))))))))
Lemma: simple-swap-test_wf
∀[n:ℕ]. ∀[AType:array{i:l}(ℤ;n)].
let AModel = array-model(AType) in
∀[prog:A-map Unit]. ∀[i,j:ℕn]. (simple-swap-test(AModel;prog;i;j) ∈ A-map 𝔹)
Definition: simple-swap-test2
simple-swap-test2(AModel;prog;i;j;k) ==
A-bind(AModel) (A-coerce(AModel) (A-fetch'(AModel) i))
(λin@i.(A-bind(AModel) (A-coerce(AModel) (A-fetch'(AModel) j))
(λin@j.(A-bind(AModel) (A-coerce(AModel) (A-fetch'(AModel) k))
(λin@k.(A-bind(AModel) prog
(λx.(A-bind(AModel) (A-coerce(AModel) (A-fetch'(AModel) i))
(λout@i.(A-bind(AModel) (A-coerce(AModel) (A-fetch'(AModel) j))
(λout@j.(A-bind(AModel) (A-coerce(AModel) (A-fetch'(AModel) k))
(λout@k.(A-return(AModel)
(((out@i =z in@j) ∧b (out@j =z in@i))
∧b ((¬b(k =z i))
∧b (¬b(k =z j)) ⇒b (out@k =z in@k)))))))))))))))))
Lemma: simple-swap-test2_wf
∀[n:ℕ]. ∀[AType:array{i:l}(ℤ;n)]. ∀[prog:A-map Unit]. ∀[i,j,k:ℕn].
(simple-swap-test2(array-model(AType);prog;i;j;k) ∈ A-map 𝔹)
Definition: simple-swap-specification
simple-swap-specification(AType;n;prog;i;j) ==
∀k:ℕn. ∀A:Arr(AType). (↑(A-eval(array-model(AType)) simple-swap-test2(array-model(AType);prog;i;j;k) A))
Lemma: simple-swap-specification_wf
∀[n:ℕ]. ∀[AType:array{i:l}(ℤ;n)]. ∀[prog:A-map Unit]. ∀i,j:ℕn. (simple-swap-specification(AType;n;prog;i;j) ∈ ℙ)
Definition: simple-swap
simple-swap(AModel;i;j) ==
A-bind(AModel) (A-coerce(AModel) (A-fetch'(AModel) i))
(λin@i.(A-bind(AModel) (A-coerce(AModel) (A-fetch'(AModel) j))
(λin@j.(A-bind(AModel) (A-assign(AModel) i in@j) (λx.(A-assign(AModel) j in@i))))))
Lemma: simple-swap_wf
∀[n:ℕ]. ∀[AType:array{i:l}(ℤ;n)]. ∀[i,j:ℕn]. (simple-swap(array-model(AType);i;j) ∈ A-map Unit)
Lemma: simple-swap-correct
∀[n:ℕ]. ∀[AType:array{i:l}(ℤ;n)]. ∀[prog:A-map Unit].
∀i,j:ℕn. simple-swap-specification(AType;n;simple-swap(array-model(AType);i;j);i;j)
Definition: simple-swap2
simple-swap2(AModel;i;j) ==
A-bind(AModel) (A-fetch(AModel) i)
(λin@i.(A-bind(AModel) (A-fetch(AModel) j)
(λin@j.(A-bind(AModel) (A-assign(AModel) i in@j) (λx.(A-assign(AModel) j in@i))))))
Lemma: simple-swap2_wf
∀[n:ℕ]. ∀[AType:array{i:l}(ℤ;n)]. ∀[i,j:ℕn]. (simple-swap2(array-model(AType);i;j) ∈ A-map Unit)
Definition: A-bind2
m >> \x.k[x] == A-bind(AModel) m (λy.k[y])
Lemma: A-bind2_wf
∀[Val:Type]. ∀[n:ℕ]. ∀[AType:array{i:l}(Val;n)]. ∀[T,S:Type]. ∀[m:A-map T]. ∀[k:T ⟶ (A-map S)].
(m >> \x.
k[x] ∈ A-map S)
Definition: A-fetch2
A-fetch2(AModel;i) == A-fetch(AModel) i
Lemma: A-fetch2_wf
∀[Val:Type]. ∀[n:ℕ]. ∀[AType:array{i:l}(Val;n)]. ∀[i:ℕn]. (A-fetch2(array-model(AType);i) ∈ A-map Val)
Definition: A-assign2
A-assign2(AModel;i;v) == A-assign(AModel) i v
Lemma: A-assign2_wf
∀[Val:Type]. ∀[n:ℕ]. ∀[AType:array{i:l}(Val;n)]. ∀[i:ℕn]. ∀[v:Val]. (A-assign2(array-model(AType);i;v) ∈ A-map Unit)
Definition: simple-swap3
simple-swap3(AModel;i;j) ==
A-fetch2(AModel;i) >> \in@i.
A-fetch2(AModel;j) >> \in@j.
A-assign2(AModel;i;in@j) >> \%1.
A-assign2(AModel;j;in@i)
Lemma: simple-swap3_wf
∀[n:ℕ]. ∀[AType:array{i:l}(ℤ;n)]. ∀[i,j:ℕn]. (simple-swap3(array-model(AType);i;j) ∈ A-map Unit)
Definition: alt-swap-spec
alt-swap-spec(AType;n;prog) ==
∀A:Arr(AType). ∀i,j,k:ℕn.
(((A-post-val(AType;prog i j;A;j) = A-pre-val(AType;A;i) ∈ ℤ)
∧ (A-post-val(AType;prog i j;A;i) = A-pre-val(AType;A;j) ∈ ℤ))
∧ (((¬(k = i ∈ ℤ)) ∧ (¬(k = j ∈ ℤ))) ⇒ (A-post-val(AType;prog i j;A;k) = A-pre-val(AType;A;k) ∈ ℤ)))
Lemma: alt-swap-spec_wf2
∀[n:ℕ]. ∀[AType:array{i:l}(ℤ;n)]. ∀[prog:ℕn ⟶ ℕn ⟶ (A-map Unit)]. ∀[i,j:ℕn]. (alt-swap-spec(AType;n;prog) ∈ ℙ)
Lemma: swap-exists
∀n:ℕ. ∀AType:array{i:l}(ℤ;n). ∃prog:ℕn ⟶ ℕn ⟶ (A-map Unit). ∀[i,j:ℕn]. alt-swap-spec(AType;n;prog)
Definition: A-shift-spec
A-shift-spec(AType; Val; n; prog) ==
∀A:Arr(AType). ∀i:ℕn.
((i < n - 2 ⇒ (A-post-val(AType;prog;A;i) = A-pre-val(AType;A;i + 1) ∈ Val))
∧ (A-post-val(AType;prog;A;n - 1) = A-pre-val(AType;A;0) ∈ Val))
Lemma: A-shift-spec_wf
∀[Val:Type]. ∀[n:ℕ]. ∀[AType:array{i:l}(Val;n)]. ∀[prog:A-map Unit]. (A-shift-spec(AType; Val; n; prog) ∈ ℙ)
Definition: A-shift-upto-spec
A-shift-upto-spec(AType; Val; n; prog; j) ==
∀A:Arr(AType). ∀i:ℕn.
if i <z j - 1
then A-post-val(AType;prog;A;i) = A-pre-val(AType;A;i + 1) ∈ Val
else A-post-val(AType;prog;A;i) = A-pre-val(AType;A;i) ∈ Val
fi
Lemma: A-shift-upto-spec_wf
∀[Val:Type]. ∀[n:ℕ]. ∀[AType:array{i:l}(Val;n)]. ∀[prog:A-map Unit]. ∀[j:ℕn].
(A-shift-upto-spec(AType; Val; n; prog; j) ∈ ℙ)
Definition: A-shift-upto
A-shift-upto(AType;j) ==
let AModel = array-model(AType) in
A-loop(AType;1;j;λi.(A-bind(AModel) (A-coerce(AModel) (A-fetch'(AModel) i))
(λin@i.(A-assign(AModel) (i - 1) in@i))))
Lemma: A-shift-upto_wf
∀[Val:Type]. ∀[n:ℕ]. (1 < n ⇒ (∀[AType:array{i:l}(Val;n)]. ∀[j:ℕn]. (A-shift-upto(AType;j) ∈ A-map Unit)))
Definition: mtype
mtype(M) == fst(M)
Lemma: mtype_wf
∀[Mn:Monad]. (mtype(Mn) ∈ Type ⟶ Type)
Lemma: provisional-equiv
∀[T:𝕌']. EquivRel(ok:ℙ × T supposing ↓ok;x,y.(↓fst(x) ⇐⇒ ↓fst(y)) ∧ ((↓fst(x)) ⇒ ((snd(x)) = (snd(y)) ∈ T)))
Definition: provisional-type
Provisional(T) == x,y:ok:ℙ × T supposing ↓ok//((↓fst(x) ⇐⇒ ↓fst(y)) ∧ ((↓fst(x)) ⇒ ((snd(x)) = (snd(y)) ∈ T)))
Lemma: provisional-type_wf
∀[T:𝕌']. (Provisional(T) ∈ 𝕌')
Lemma: provisional-type-cumulativity
∀[T:𝕌']. (Provisional(T) ⊆r Provisional'(T))
Definition: provision
provision(ok; v) == <ok, v>
Lemma: provision_wf
∀[T:𝕌']. ∀[ok:ℙ]. ∀[v:T supposing ok]. (provision(ok; v) ∈ Provisional(T))
Lemma: provision-equality
∀[T:𝕌']. ∀[ok1,ok2:ℙ]. ∀[v1:⋂:↓ok1. T]. ∀[v2:⋂:↓ok2. T].
(provision(ok1; v1) = provision(ok2; v2) ∈ Provisional(T)) supposing (((↓ok1) ⇒ (v1 = v2 ∈ T)) and (↓ok1 ⇐⇒ ↓ok2))
Definition: allowed
allowed(x) == usquash(fst(x))
Lemma: allowed_wf
∀[T:𝕌']. ∀[x:Provisional(T)]. (allowed(x) ∈ ℙ)
Lemma: sq_stable__allowed
∀[T:𝕌']. ∀[x:Provisional(T)]. SqStable(allowed(x))
Lemma: allowed-trivial-iff
∀[T:𝕌']. ∀[x:Provisional(T)]. ∀[X:ℙ]. (SqStable(X) ⇒ allowed(x) ⇐⇒ usquash(allowed(x) ∧ X) supposing X)
Definition: allow
allow(x) == snd(x)
Lemma: allow_wf
∀[T:𝕌']. ∀[x:Provisional(T)]. allow(x) ∈ T supposing allowed(x)
Lemma: provisional-type-equality
∀[T:𝕌']. ∀[x,y:Provisional(T)].
(x = y ∈ Provisional(T)) supposing ((allowed(x) ⇒ (allow(x) = allow(y) ∈ T)) and (allowed(x) ⇐⇒ allowed(y)))
Definition: bind-provision
bind-provision(x;t.f[t]) == provision(allowed(x) ∧ allowed(f[allow(x)]); allow(f[allow(x)]))
Lemma: bind-provision_wf
∀[T,S:𝕌']. ∀[x:Provisional(T)]. ∀[f:{t:T| allowed(x) ∧ (t = allow(x) ∈ T)} ⟶ Provisional(S)].
(bind-provision(x;t.f[t]) ∈ Provisional(S))
Definition: provisional-monad
provisional-monad{i:l}() == mk_monad(λT.Provisional(T);λx.OK(x);λx,f. bind-provision(x;u.f u))
Lemma: provisional-monad_wf
provisional-monad{i:l}() ∈ Monad'
Lemma: provisional-type-wf2
∀[T:𝕌'']. (Provisional(T) ∈ 𝕌'')
Lemma: provisional-subtype
∀[T,S:𝕌']. Provisional(T) ⊆r Provisional(S) supposing T ⊆r S
Lemma: allowed_provision_lemma
∀v,ok:Top. (allowed(provision(ok; v)) ~ usquash(ok))
Lemma: allow_provision_lemma
∀v,ok:Top. (allow(provision(ok; v)) ~ v)
Definition: provisional-apply2
provisional-apply2(f;a;b) == provision(allowed(a) ∧ allowed(b); f allow(a) allow(b))
Lemma: provisional-apply2_wf
∀[A,B,C:Type]. ∀[f:A ⟶ B ⟶ C]. ∀[a:Provisional(A)]. ∀[b:Provisional(B)]. (provisional-apply2(f;a;b) ∈ Provisional(C))
Home
Index