Definition: index-min
index-min(zs) ==
rec-case(zs) of
[] => <0, 0>
z::more =>
p.if more = Ax then <0, z> otherwise let i,x = p
in if (z) < (x) then <0, z> else eval j = i + 1 in <j, x>
Lemma: index-min_wf
∀[zs:ℤ List+]. (index-min(zs) ∈ i:ℕ||zs|| × {x:ℤ| (x = zs[i] ∈ ℤ) ∧ (∀z:ℤ. ((z ∈ zs) ⇒ (x ≤ z)))} )
Definition: index-of-min
index-of-min(zs) == fst(index-min(zs))
Lemma: index-of-min_wf
∀[zs:ℤ List+]. (index-of-min(zs) ∈ {i:ℕ||zs||| ∀x:ℤ. ((x ∈ zs) ⇒ (zs[i] ≤ x))} )
Lemma: rev-append-property
∀[as,bs:Top]. (rev(as) + bs ~ rev(as) + [] @ bs)
Lemma: rev-append-as-reverse
∀[as,bs:Top]. (rev(as) + bs ~ rev(as) @ bs)
Lemma: member-rev-append
∀[T:Type]. ∀x:T. ∀as,bs:T List. ((x ∈ rev(as) + bs) ⇐⇒ (x ∈ as) ∨ (x ∈ bs))
Lemma: eager_product_map_nil_lemma
∀bs,f:Top. (eager-product-map(f;[];bs) ~ [])
Lemma: eager_product_map_cons_lemma
∀L,as,a,f:Top. (eager-product-map(f;[a / as];L) ~ eager-map-append(f a;L;eager-product-map(f;as;L)))
Lemma: eager-product-map-nil
∀[f:Top]. ∀[as:Top List]. (eager-product-map(f;as;[]) ~ [])
Lemma: l_all_eager_product-map
∀T:Type
∀A,B:Type. ∀Pa:A ⟶ ℙ. ∀Pb:B ⟶ ℙ. ∀Pt:T ⟶ ℙ. ∀f:A ⟶ B ⟶ T.
((∀a:A. ∀b:B. (Pa[a] ⇒ Pb[b] ⇒ Pt[f a b]))
⇒ (∀as:A List. ∀bs:B List. ((∀a∈as.Pa[a]) ⇒ (∀b∈bs.Pb[b]) ⇒ (∀t∈eager-product-map(f;as;bs).Pt[t]))))
supposing value-type(T)
Lemma: map-map2
∀[as,f,g:Top]. (map(g;map(f;as)) ~ map(g o f;as))
Lemma: map-id-map
∀[as,f:Top]. (map(λx.x;map(f;as)) ~ map(f;as))
Definition: accumulate_abort
accumulate_abort(x,sofar.F[x; sofar];s;L) == eager-accum(r,x.case r of inl(sofar) => F[x; sofar] | inr(_) => r;s;L)
Lemma: accumulate_abort_wf
∀[A,B:Type]. ∀[s:B?]. ∀[F:A ⟶ B ⟶ (B?)]. ∀[L:A List].
accumulate_abort(x,sofar.F[x;sofar];s;L) ∈ B? supposing valueall-type(B)
Lemma: accumulate_abort_nil_lemma
∀s,F:Top. (accumulate_abort(x,y.F[x;y];s;[]) ~ s)
Lemma: accumulate_abort_cons_lemma
∀v,u,s,F:Top.
(accumulate_abort(x,y.F[x;y];s;[u / v]) ~ let s' ⟵ case s of inl(y) => F[u;y] | inr(_) => s
in accumulate_abort(x,y.F[x;y];s';v))
Lemma: accumulate_abort-aborted
∀[z:Unit]. ∀[F:Top]. ∀[L:Top List]. (accumulate_abort(x,sofar.F[x;sofar];inr z ;L) ~ inr z )
Lemma: assert-list-deq
∀[A:Type]. ∀[eq:EqDecider(A)]. ∀[as,bs:A List]. uiff(↑(list-deq(eq) as bs);as = bs ∈ (A List))
Definition: integer-dot-product
as ⋅ bs
==r if as = Ax then 0 otherwise if bs = Ax then 0 otherwise let a,as2 = as
in let b,bs2 = bs
in (a * b) + as2 ⋅ bs2
Lemma: int_dot_nil_left_lemma
∀bs:Top. ([] ⋅ bs ~ 0)
Lemma: int_dot_cons_nil_lemma
∀as,a:Top. ([a / as] ⋅ [] ~ 0)
Lemma: int_dot_cons_lemma
∀bs,b,as,a:Top. ([a / as] ⋅ [b / bs] ~ (a * b) + as ⋅ bs)
Lemma: integer-dot-product_wf
∀[as,bs:ℤ List]. (as ⋅ bs ∈ ℤ)
Lemma: integer-dot-product-comm
∀[as,bs:ℤ List]. (as ⋅ bs ~ bs ⋅ as)
Definition: satisfies-integer-equality
xs ⋅ as =0 == (||xs|| = ||as|| ∈ ℤ) ∧ 0 < ||xs|| ∧ (hd(xs) = 1 ∈ ℤ) ∧ (as ⋅ xs = 0 ∈ ℤ)
Lemma: satisfies-integer-equality_wf
∀[xs,as:ℤ List]. (xs ⋅ as =0 ∈ ℙ)
Definition: satisfies-integer-inequality
xs ⋅ as ≥0 == (||xs|| = ||as|| ∈ ℤ) ∧ 0 < ||xs|| ∧ (hd(xs) = 1 ∈ ℤ) ∧ (as ⋅ xs ≥ 0 )
Lemma: satisfies-integer-inequality_wf
∀[xs,as:ℤ List]. (xs ⋅ as ≥0 ∈ ℙ)
Lemma: trivial-unsat-integer-inequality
∀[xs:ℤ List]. (¬xs ⋅ [-1] ≥0)
Definition: list-delete
as\i==r if as = Ax then as otherwise let a,as2 = as in if (i) < (1) then as2 else [a / as2\i - 1]
Lemma: list-delete_wf
∀[T:Type]. ∀[as:T List]. ∀[i:ℤ]. (as\i ∈ T List)
Lemma: length-list-delete
∀[T:Type]. ∀[as:T List]. ∀[i:ℕ]. ||as\i|| = (||as|| - 1) ∈ ℤ supposing i < ||as||
Definition: int-vec-mul
a * as == map(λx.(a * x);as)
Lemma: int-vec-mul_wf
∀[a:ℤ]. ∀[as:ℤ List]. (a * as ∈ ℤ List)
Lemma: int-vec-mul-mul
∀[a,b:ℤ]. ∀[as:ℤ List]. (a * b * as ~ a * b * as)
Lemma: length-int-vec-mul
∀[a,as:Top]. (||a * as|| ~ ||as||)
Definition: int-vec-add
as + bs
==r if as = Ax then as otherwise if bs = Ax then bs otherwise let a,as2 = as
in let b,bs2 = bs
in [a + b / as2 + bs2]
Lemma: int-vec-add_wf
∀[as,bs:ℤ List]. (as + bs ∈ ℤ List)
Lemma: length-int-vec-add
∀[as,bs:ℤ List]. ||as + bs|| = ||bs|| ∈ ℤ supposing ||as|| = ||bs|| ∈ ℤ
Lemma: select-int-vec-add
∀[as,bs:ℤ List]. ∀[i:ℕ]. as + bs[i] ~ as[i] + bs[i] supposing i < ||as|| ∧ i < ||bs||
Lemma: select-int-vec-mul
∀[x:ℤ]. ∀[as:ℤ List]. ∀[i:ℕ||as||]. (x * as[i] ~ x * as[i])
Lemma: int-dot-mul-left
∀[x:ℤ]. ∀[as,bs:ℤ List]. (x * as ⋅ bs ~ x * as ⋅ bs)
Lemma: int-dot-mul-right
∀[x:ℤ]. ∀[as,bs:ℤ List]. (as ⋅ x * bs ~ x * as ⋅ bs)
Lemma: int-dot-add-left
∀[as,bs,cs:ℤ List]. as + bs ⋅ cs ~ as ⋅ cs + bs ⋅ cs supposing ||as|| = ||bs|| ∈ ℤ
Lemma: int-dot-add-right
∀[cs,as,bs:ℤ List]. cs ⋅ as + bs ~ cs ⋅ as + cs ⋅ bs supposing ||as|| = ||bs|| ∈ ℤ
Lemma: int-dot-select
∀[as,bs:ℤ List]. ∀[i:ℕ]. as ⋅ bs ~ (as[i] * bs[i]) + as\i ⋅ bs\i supposing i < ||as|| ∧ i < ||bs||
Lemma: int-dot-reduce-dim
∀[as,bs:ℤ List]. ∀[i:ℕ].
∀[cs:ℤ List]. (as ⋅ bs ~ as[i] * cs + as\i ⋅ bs\i) supposing ((bs[i] = cs ⋅ bs\i ∈ ℤ) and (||cs|| = (||as|| - 1) ∈ ℤ))\000C
supposing i < ||as|| ∧ i < ||bs||
Lemma: int-eq-constraint-factor
∀[a:ℤ]. ∀[g:ℤ-o]. ∀[xs,L:ℤ List].
uiff([1 / xs] ⋅ [a / g * L] = 0 ∈ ℤ;((a rem g) = 0 ∈ ℤ) ∧ ([1 / xs] ⋅ [a ÷ g / L] = 0 ∈ ℤ))
Lemma: int-eq-constraint-factor-sym
∀[a:ℤ]. ∀[g:ℤ-o]. ∀[xs,L:ℤ List].
uiff([a / g * L] ⋅ [1 / xs] = 0 ∈ ℤ;((a rem g) = 0 ∈ ℤ) ∧ ([a ÷ g / L] ⋅ [1 / xs] = 0 ∈ ℤ))
Lemma: int-ineq-constraint-factor
∀[a:ℤ]. ∀[g:ℕ+]. ∀[xs,L:ℤ List]. uiff(0 ≤ [1 / xs] ⋅ [a / g * L];0 ≤ [1 / xs] ⋅ [a ÷↓ g / L])
Lemma: int-ineq-constraint-factor-sym
∀[a:ℤ]. ∀[g:ℕ+]. ∀[xs,L:ℤ List]. uiff(0 ≤ [a / g * L] ⋅ [1 / xs];0 ≤ [a ÷↓ g / L] ⋅ [1 / xs])
Lemma: gcd-list-property
∀L:ℤ List+
((∃R:ℤ List. (L = gcd-list(L) * R ∈ (ℤ List))) ∧ (∃S:ℤ List. ((||S|| = ||L|| ∈ ℤ) ∧ (gcd-list(L) = S ⋅ L ∈ ℤ))))
Definition: shadow-vec
shadow-vec(i;as;bs) ==
eval bs' = evalall(as[i] * bs) in
eval as' = evalall(-bs[i] * as) in
eval L = evalall(bs' + as') in
evalall(L\i)
Lemma: shadow-vec_wf
∀[as,bs:ℤ List]. ∀[i:ℕ||as||]. shadow-vec(i;as;bs) ∈ ℤ List supposing ||as|| = ||bs|| ∈ ℤ
Lemma: length-shadow-vec
∀[as,bs:ℤ List]. ∀[i:ℕ||as||]. ||shadow-vec(i;as;bs)|| = (||as|| - 1) ∈ ℤ supposing ||as|| = ||bs|| ∈ ℤ
Lemma: shadow-vec-property
∀[as,bs:ℤ List]. ∀[i:ℕ||as||].
(∀[xs:ℤ List]
0 ≤ shadow-vec(i;as;bs) ⋅ xs\i supposing (||xs|| = ||as|| ∈ ℤ) ∧ (0 ≤ as ⋅ xs) ∧ (0 ≤ bs ⋅ xs)) supposing
((bs[i] ≤ 0) and
(0 ≤ as[i]) and
(||as|| = ||bs|| ∈ ℤ))
Definition: int_termco
int_termco() ==
corec(X.lbl:Atom × if lbl =a "Constant" then ℤ
if lbl =a "Var" then ℤ
if lbl =a "Add" then left:X × X
if lbl =a "Subtract" then left:X × X
if lbl =a "Multiply" then left:X × X
if lbl =a "Minus" then X
else Void
fi )
Lemma: int_termco_wf
int_termco() ∈ Type
Lemma: int_termco-ext
int_termco() ≡ lbl:Atom × if lbl =a "Constant" then ℤ
if lbl =a "Var" then ℤ
if lbl =a "Add" then left:int_termco() × int_termco()
if lbl =a "Subtract" then left:int_termco() × int_termco()
if lbl =a "Multiply" then left:int_termco() × int_termco()
if lbl =a "Minus" then int_termco()
else Void
fi
Definition: int_termco_size
int_termco_size(p) ==
fix((λsize,p. let lbl,x = p
in if lbl =a "Constant" then 0
if lbl =a "Var" then 0
if lbl =a "Add" then 1 + (size (fst(x))) + (size (snd(x)))
if lbl =a "Subtract" then 1 + (size (fst(x))) + (size (snd(x)))
if lbl =a "Multiply" then 1 + (size (fst(x))) + (size (snd(x)))
if lbl =a "Minus" then 1 + (size x)
else 0
fi ))
p
Lemma: int_termco_size_wf
∀[p:int_termco()]. (int_termco_size(p) ∈ partial(ℕ))
Definition: int_term
int_term() == {p:int_termco()| (int_termco_size(p))↓}
Lemma: int_term_wf
int_term() ∈ Type
Definition: int_term_size
int_term_size(p) ==
fix((λsize,p. let lbl,x = p
in if lbl =a "Constant" then 0
if lbl =a "Var" then 0
if lbl =a "Add" then 1 + (size (fst(x))) + (size (snd(x)))
if lbl =a "Subtract" then 1 + (size (fst(x))) + (size (snd(x)))
if lbl =a "Multiply" then 1 + (size (fst(x))) + (size (snd(x)))
if lbl =a "Minus" then 1 + (size x)
else 0
fi ))
p
Lemma: int_term_size_wf
∀[p:int_term()]. (int_term_size(p) ∈ ℕ)
Lemma: int_term-ext
int_term() ≡ lbl:Atom × if lbl =a "Constant" then ℤ
if lbl =a "Var" then ℤ
if lbl =a "Add" then left:int_term() × int_term()
if lbl =a "Subtract" then left:int_term() × int_term()
if lbl =a "Multiply" then left:int_term() × int_term()
if lbl =a "Minus" then int_term()
else Void
fi
Definition: itermConstant
"const" == <"Constant", const>
Lemma: itermConstant_wf
∀[const:ℤ]. ("const" ∈ int_term())
Definition: itermVar
vvar == <"Var", var>
Lemma: itermVar_wf
∀[var:ℤ]. (vvar ∈ int_term())
Definition: itermAdd
left (+) right == <"Add", left, right>
Lemma: itermAdd_wf
∀[left,right:int_term()]. (left (+) right ∈ int_term())
Definition: itermSubtract
left (-) right == <"Subtract", left, right>
Lemma: itermSubtract_wf
∀[left,right:int_term()]. (left (-) right ∈ int_term())
Definition: itermMultiply
left (*) right == <"Multiply", left, right>
Lemma: itermMultiply_wf
∀[left,right:int_term()]. (left (*) right ∈ int_term())
Definition: itermMinus
"-"num == <"Minus", num>
Lemma: itermMinus_wf
∀[num:int_term()]. ("-"num ∈ int_term())
Definition: itermConstant?
itermConstant?(v) == fst(v) =a "Constant"
Lemma: itermConstant?_wf
∀[v:int_term()]. (itermConstant?(v) ∈ 𝔹)
Definition: itermConstant-const
itermConstant-const(v) == snd(v)
Lemma: itermConstant-const_wf
∀[v:int_term()]. itermConstant-const(v) ∈ ℤ supposing ↑itermConstant?(v)
Definition: itermVar?
itermVar?(v) == fst(v) =a "Var"
Lemma: itermVar?_wf
∀[v:int_term()]. (itermVar?(v) ∈ 𝔹)
Definition: itermVar-var
itermVar-var(v) == snd(v)
Lemma: itermVar-var_wf
∀[v:int_term()]. itermVar-var(v) ∈ ℤ supposing ↑itermVar?(v)
Definition: itermAdd?
itermAdd?(v) == fst(v) =a "Add"
Lemma: itermAdd?_wf
∀[v:int_term()]. (itermAdd?(v) ∈ 𝔹)
Definition: itermAdd-left
itermAdd-left(v) == fst(snd(v))
Lemma: itermAdd-left_wf
∀[v:int_term()]. itermAdd-left(v) ∈ int_term() supposing ↑itermAdd?(v)
Definition: itermAdd-right
itermAdd-right(v) == snd(snd(v))
Lemma: itermAdd-right_wf
∀[v:int_term()]. itermAdd-right(v) ∈ int_term() supposing ↑itermAdd?(v)
Definition: itermSubtract?
itermSubtract?(v) == fst(v) =a "Subtract"
Lemma: itermSubtract?_wf
∀[v:int_term()]. (itermSubtract?(v) ∈ 𝔹)
Definition: itermSubtract-left
itermSubtract-left(v) == fst(snd(v))
Lemma: itermSubtract-left_wf
∀[v:int_term()]. itermSubtract-left(v) ∈ int_term() supposing ↑itermSubtract?(v)
Definition: itermSubtract-right
itermSubtract-right(v) == snd(snd(v))
Lemma: itermSubtract-right_wf
∀[v:int_term()]. itermSubtract-right(v) ∈ int_term() supposing ↑itermSubtract?(v)
Definition: itermMultiply?
itermMultiply?(v) == fst(v) =a "Multiply"
Lemma: itermMultiply?_wf
∀[v:int_term()]. (itermMultiply?(v) ∈ 𝔹)
Definition: itermMultiply-left
itermMultiply-left(v) == fst(snd(v))
Lemma: itermMultiply-left_wf
∀[v:int_term()]. itermMultiply-left(v) ∈ int_term() supposing ↑itermMultiply?(v)
Definition: itermMultiply-right
itermMultiply-right(v) == snd(snd(v))
Lemma: itermMultiply-right_wf
∀[v:int_term()]. itermMultiply-right(v) ∈ int_term() supposing ↑itermMultiply?(v)
Definition: itermMinus?
itermMinus?(v) == fst(v) =a "Minus"
Lemma: itermMinus?_wf
∀[v:int_term()]. (itermMinus?(v) ∈ 𝔹)
Definition: itermMinus-num
itermMinus-num(v) == snd(v)
Lemma: itermMinus-num_wf
∀[v:int_term()]. itermMinus-num(v) ∈ int_term() supposing ↑itermMinus?(v)
Lemma: int_term-induction
∀[P:int_term() ⟶ ℙ]
((∀const:ℤ. P["const"])
⇒ (∀var:ℤ. P[vvar])
⇒ (∀left,right:int_term(). (P[left] ⇒ P[right] ⇒ P[left (+) right]))
⇒ (∀left,right:int_term(). (P[left] ⇒ P[right] ⇒ P[left (-) right]))
⇒ (∀left,right:int_term(). (P[left] ⇒ P[right] ⇒ P[left (*) right]))
⇒ (∀num:int_term(). (P[num] ⇒ P["-"num]))
⇒ {∀v:int_term(). P[v]})
Lemma: int_term-definition
∀[A:Type]. ∀[R:A ⟶ int_term() ⟶ ℙ].
((∀const:ℤ. {x:A| R[x;"const"]} )
⇒ (∀var:ℤ. {x:A| R[x;vvar]} )
⇒ (∀left,right:int_term(). ({x:A| R[x;left]} ⇒ {x:A| R[x;right]} ⇒ {x:A| R[x;left (+) right]} ))
⇒ (∀left,right:int_term(). ({x:A| R[x;left]} ⇒ {x:A| R[x;right]} ⇒ {x:A| R[x;left (-) right]} ))
⇒ (∀left,right:int_term(). ({x:A| R[x;left]} ⇒ {x:A| R[x;right]} ⇒ {x:A| R[x;left (*) right]} ))
⇒ (∀num:int_term(). ({x:A| R[x;num]} ⇒ {x:A| R[x;"-"num]} ))
⇒ {∀v:int_term(). {x:A| R[x;v]} })
Definition: int_term_ind
int_term_ind(v;
itermConstant(const)⇒ Constant[const];
itermVar(var)⇒ Var[var];
itermAdd(left,right)⇒ rec1,rec2.Add[left;
right;
rec1;
rec2];
itermSubtract(left,right)⇒ rec3,rec4.Subtract[left;
right;
rec3;
rec4];
itermMultiply(left,right)⇒ rec5,rec6.Multiply[left;
right;
rec5;
rec6];
itermMinus(num)⇒ rec7.Minus[num; rec7]) ==
fix((λint_term_ind,v. let lbl,v1 = v
in if lbl="Constant" then Constant[v1]
if lbl="Var" then Var[v1]
if lbl="Add"
then let left,v2 = v1
in Add[left;
v2;
int_term_ind left;
int_term_ind v2]
if lbl="Subtract"
then let left,v2 = v1
in Subtract[left;
v2;
int_term_ind left;
int_term_ind v2]
if lbl="Multiply"
then let left,v2 = v1
in Multiply[left;
v2;
int_term_ind left;
int_term_ind v2]
if lbl="Minus" then Minus[v1; int_term_ind v1]
else Ax
fi ))
v
Lemma: int_term_ind_wf
∀[A:Type]. ∀[R:A ⟶ int_term() ⟶ ℙ]. ∀[v:int_term()]. ∀[Constant:const:ℤ ⟶ {x:A| R[x;"const"]} ].
∀[Var:var:ℤ ⟶ {x:A| R[x;vvar]} ]. ∀[Add:left:int_term()
⟶ right:int_term()
⟶ {x:A| R[x;left]}
⟶ {x:A| R[x;right]}
⟶ {x:A| R[x;left (+) right]} ]. ∀[Subtract:left:int_term()
⟶ right:int_term()
⟶ {x:A| R[x;left]}
⟶ {x:A| R[x;right]}
⟶ {x:A| R[x;left (-) right]} ].
∀[Multiply:left:int_term() ⟶ right:int_term() ⟶ {x:A| R[x;left]} ⟶ {x:A| R[x;right]} ⟶ {x:A| R[x;left (*) right]} \000C].
∀[Minus:num:int_term() ⟶ {x:A| R[x;num]} ⟶ {x:A| R[x;"-"num]} ].
(int_term_ind(v;
itermConstant(const)⇒ Constant[const];
itermVar(var)⇒ Var[var];
itermAdd(left,right)⇒ rec1,rec2.Add[left;right;rec1;rec2];
itermSubtract(left,right)⇒ rec3,rec4.Subtract[left;right;rec3;rec4];
itermMultiply(left,right)⇒ rec5,rec6.Multiply[left;right;rec5;rec6];
itermMinus(num)⇒ rec7.Minus[num;rec7]) ∈ {x:A| R[x;v]} )
Lemma: int_term_ind_wf_simple
∀[A:Type]. ∀[v:int_term()]. ∀[Constant,Var:var:ℤ ⟶ A]. ∀[Add,Subtract,Multiply:left:int_term()
⟶ right:int_term()
⟶ A
⟶ A
⟶ A].
∀[Minus:num:int_term() ⟶ A ⟶ A].
(int_term_ind(v;
itermConstant(const)⇒ Constant[const];
itermVar(var)⇒ Var[var];
itermAdd(left,right)⇒ rec1,rec2.Add[left;right;rec1;rec2];
itermSubtract(left,right)⇒ rec3,rec4.Subtract[left;right;rec3;rec4];
itermMultiply(left,right)⇒ rec5,rec6.Multiply[left;right;rec5;rec6];
itermMinus(num)⇒ rec7.Minus[num;rec7]) ∈ A)
Lemma: int_term_subtype_base
int_term() ⊆r Base
Definition: int-term-ind-fun
int-term-ind-fun(c.C[c];
v.V[v];
l,r,rl,rr.A[l;
r;
rl;
rr];
l,r,rl,rr.S[l;
r;
rl;
rr];
l,r,rl,rr.M[l;
r;
rl;
rr];
x,rx.MN[x; rx]) ==
λt.int_term_ind(t;
itermConstant(c)⇒ C[c];
itermVar(v)⇒ V[v];
itermAdd(l,r)⇒ rl,rr.A[l;
r;
rl;
rr];
itermSubtract(l,r)⇒ rl,rr.S[l;
r;
rl;
rr];
itermMultiply(l,r)⇒ rl,rr.M[l;
r;
rl;
rr];
itermMinus(x)⇒ rx.MN[x; rx])
Lemma: int-term-ind-fun_wf
∀[A:Type]. ∀[v:int_term()]. ∀[Constant,Var:var:ℤ ⟶ A]. ∀[Add,Subtract,Multiply:left:int_term()
⟶ right:int_term()
⟶ A
⟶ A
⟶ A].
∀[Minus:num:int_term() ⟶ A ⟶ A].
(int-term-ind-fun(c.Constant[c];
v.Var[v];
l,r,rl,rr.Add[l;r;rl;rr];
l,r,rl,rr.Subtract[l;r;rl;rr];
l,r,rl,rr.Multiply[l;r;rl;rr];
x,rx.Minus[x;rx]) ∈ int_term() ⟶ A)
Lemma: int_term_ind-var
∀[C,V,A,S,M,MN,k:Top].
(int-term-ind-fun(c.C[c];
v.V[v];
l,r,rl,rr.A[l;r;rl;rr];
l,r,rl,rr.S[l;r;rl;rr];
l,r,rl,rr.M[l;r;rl;rr];
x,rx.MN[x;rx])
vk ~ V[k])
Lemma: int_term_ind-const
∀[C,V,A,S,M,MN,c:Top].
(int-term-ind-fun(c.C[c];
v.V[v];
l,r,rl,rr.A[l;r;rl;rr];
l,r,rl,rr.S[l;r;rl;rr];
l,r,rl,rr.M[l;r;rl;rr];
x,rx.MN[x;rx])
"c" ~ C[c])
Lemma: int_term_ind-add
∀[C,V,A,S,M,MN,a,b:Top].
(int-term-ind-fun(c.C[c];
v.V[v];
l,r,rl,rr.A[l;r;rl;rr];
l,r,rl,rr.S[l;r;rl;rr];
l,r,rl,rr.M[l;r;rl;rr];
x,rx.MN[x;rx])
(a (+) b) ~ A[a;b;int-term-ind-fun(c.C[c];
v.V[v];
l,r,rl,rr.A[l;r;rl;rr];
l,r,rl,rr.S[l;r;rl;rr];
l,r,rl,rr.M[l;r;rl;rr];
x,rx.MN[x;rx])
a;int-term-ind-fun(c.C[c];
v.V[v];
l,r,rl,rr.A[l;r;rl;rr];
l,r,rl,rr.S[l;r;rl;rr];
l,r,rl,rr.M[l;r;rl;rr];
x,rx.MN[x;rx])
b])
Lemma: int_term_ind-sub
∀[C,V,A,S,M,MN,a,b:Top].
(int-term-ind-fun(c.C[c];
v.V[v];
l,r,rl,rr.A[l;r;rl;rr];
l,r,rl,rr.S[l;r;rl;rr];
l,r,rl,rr.M[l;r;rl;rr];
x,rx.MN[x;rx])
(a (-) b) ~ S[a;b;int-term-ind-fun(c.C[c];
v.V[v];
l,r,rl,rr.A[l;r;rl;rr];
l,r,rl,rr.S[l;r;rl;rr];
l,r,rl,rr.M[l;r;rl;rr];
x,rx.MN[x;rx])
a;int-term-ind-fun(c.C[c];
v.V[v];
l,r,rl,rr.A[l;r;rl;rr];
l,r,rl,rr.S[l;r;rl;rr];
l,r,rl,rr.M[l;r;rl;rr];
x,rx.MN[x;rx])
b])
Lemma: int_term_ind-mul
∀[C,V,A,S,M,MN,a,b:Top].
(int-term-ind-fun(c.C[c];
v.V[v];
l,r,rl,rr.A[l;r;rl;rr];
l,r,rl,rr.S[l;r;rl;rr];
l,r,rl,rr.M[l;r;rl;rr];
x,rx.MN[x;rx])
(a (*) b) ~ M[a;b;int-term-ind-fun(c.C[c];
v.V[v];
l,r,rl,rr.A[l;r;rl;rr];
l,r,rl,rr.S[l;r;rl;rr];
l,r,rl,rr.M[l;r;rl;rr];
x,rx.MN[x;rx])
a;int-term-ind-fun(c.C[c];
v.V[v];
l,r,rl,rr.A[l;r;rl;rr];
l,r,rl,rr.S[l;r;rl;rr];
l,r,rl,rr.M[l;r;rl;rr];
x,rx.MN[x;rx])
b])
Lemma: int_term_ind-minus
∀[C,V,A,S,M,MN,x:Top].
(int-term-ind-fun(c.C[c];
v.V[v];
l,r,rl,rr.A[l;r;rl;rr];
l,r,rl,rr.S[l;r;rl;rr];
l,r,rl,rr.M[l;r;rl;rr];
x,rx.MN[x;rx])
"-"x ~ MN[x;int-term-ind-fun(c.C[c];
v.V[v];
l,r,rl,rr.A[l;r;rl;rr];
l,r,rl,rr.S[l;r;rl;rr];
l,r,rl,rr.M[l;r;rl;rr];
x,rx.MN[x;rx])
x])
Definition: int_term_value
int_term_value(f;t) ==
int_term_ind(t;
itermConstant(n)⇒ n;
itermVar(v)⇒ f v;
itermAdd(l,r)⇒ rl,rr.rl + rr;
itermSubtract(l,r)⇒ rl,rr.rl - rr;
itermMultiply(l,r)⇒ rl,rr.rl * rr;
itermMinus(x)⇒ r.-r)
Lemma: int_term_value_wf
∀[f:ℤ ⟶ ℤ]. ∀[t:int_term()]. (int_term_value(f;t) ∈ ℤ)
Lemma: int_term_value_add_lemma
∀y,x,f:Top. (int_term_value(f;x (+) y) ~ int_term_value(f;x) + int_term_value(f;y))
Lemma: int_term_value_mul_lemma
∀y,x,f:Top. (int_term_value(f;x (*) y) ~ int_term_value(f;x) * int_term_value(f;y))
Lemma: int_term_value_subtract_lemma
∀y,x,f:Top. (int_term_value(f;x (-) y) ~ int_term_value(f;x) - int_term_value(f;y))
Lemma: int_term_value_minus_lemma
∀x,f:Top. (int_term_value(f;"-"x) ~ -int_term_value(f;x))
Lemma: int_term_value_constant_lemma
∀x,f:Top. (int_term_value(f;"x") ~ x)
Lemma: int_term_value_var_lemma
∀x,f:Top. (int_term_value(f;vx) ~ f x)
Definition: equiv_int_terms
t1 ≡ t2 == ∀f:ℤ ⟶ ℤ. (int_term_value(f;t1) = int_term_value(f;t2) ∈ ℤ)
Lemma: equiv_int_terms_wf
∀[t1,t2:int_term()]. (t1 ≡ t2 ∈ ℙ)
Lemma: equiv_int_terms_weakening
∀[t1,t2:int_term()]. t1 ≡ t2 supposing t1 = t2 ∈ int_term()
Lemma: equiv_int_terms_transitivity
∀[t1,t2,t3:int_term()]. (t1 ≡ t3) supposing (t2 ≡ t3 and t1 ≡ t2)
Lemma: equiv_int_terms_inversion
∀[t1,t2:int_term()]. t1 ≡ t2 supposing t2 ≡ t1
Lemma: equiv_int_terms_functionality
∀[x1,x2,y1,y2:int_term()]. (uiff(x1 ≡ y1;x2 ≡ y2)) supposing (y1 ≡ y2 and x1 ≡ x2)
Lemma: int_term_value_functionality
∀[f:ℤ ⟶ ℤ]. ∀[t1,t2:int_term()]. int_term_value(f;t1) = int_term_value(f;t2) ∈ ℤ supposing t1 ≡ t2
Lemma: itermAdd_functionality
∀[a,b,c,d:int_term()]. (a (+) c ≡ b (+) d) supposing (a ≡ b and c ≡ d)
Lemma: itermSubtract_functionality
∀[a,b,c,d:int_term()]. (a (-) c ≡ b (-) d) supposing (a ≡ b and c ≡ d)
Lemma: itermMultiply_functionality
∀[a,b,c,d:int_term()]. (a (*) c ≡ b (*) d) supposing (a ≡ b and c ≡ d)
Lemma: itermMinus_functionality
∀[a,b:int_term()]. "-"a ≡ "-"b supposing a ≡ b
Definition: iMonomial
iMonomial() == ℤ-o × {vs:ℤ List| sorted(vs)}
Lemma: iMonomial_wf
iMonomial() ∈ Type
Definition: isMonomialOne
isMonomialOne(m) == let a,vs = m in null(vs) ∧b (a =z 1)
Lemma: isMonomialOne_wf
∀[m:iMonomial()]. (isMonomialOne(m) ∈ 𝔹)
Lemma: iMonomial-value-type
value-type(iMonomial())
Definition: imonomial-le
imonomial-le(m1;m2) == snd(m1) ≤_lex snd(m2)
Lemma: imonomial-le_wf
∀[m1,m2:iMonomial()]. (imonomial-le(m1;m2) ∈ 𝔹)
Definition: imonomial-less
imonomial-less(m1;m2) == (¬((snd(m1)) = (snd(m2)) ∈ (ℤ List))) ∧ (↑imonomial-le(m1;m2))
Lemma: imonomial-less_wf
∀[m1,m2:iMonomial()]. (imonomial-less(m1;m2) ∈ ℙ)
Lemma: imonomial-less-transitive
∀[m1,m2,m3:iMonomial()]. (imonomial-less(m1;m3)) supposing (imonomial-less(m2;m3) and imonomial-less(m1;m2))
Lemma: not-imonomial-le
∀a,b:iMonomial(). ((¬↑imonomial-le(a;b)) ⇒ imonomial-less(b;a))
Definition: iPolynomial
iPolynomial() == {L:iMonomial() List| ∀i:ℕ||L||. ∀j:ℕi. imonomial-less(L[j];L[i])}
Lemma: iPolynomial_wf
iPolynomial() ∈ Type
Definition: isPolyOne
isPolyOne(p) == if p is a pair then let m,more = p in null(more) ∧b isMonomialOne(m) otherwise ff
Lemma: isPolyOne_wf
∀[p:iPolynomial()]. (isPolyOne(p) ∈ 𝔹)
Definition: imonomial-term
imonomial-term(m) ==
let c,vs = m
in accumulate (with value t and list item v):
t (*) vv
over list:
vs
with starting value:
"c")
Lemma: imonomial-term_wf
∀[m:ℤ × (ℤ List)]. (imonomial-term(m) ∈ int_term())
Lemma: imonomial-cons
∀v:ℤ List. ∀u,a:ℤ. ∀f:ℤ ⟶ ℤ. (int_term_value(f;imonomial-term(<a, [u / v]>)) = int_term_value(f;imonomial-term(<a * (f\000C u), v>)) ∈ ℤ)
Lemma: imonomial-term-linear
∀f:ℤ ⟶ ℤ. ∀ws:ℤ List. ∀c:ℤ. (int_term_value(f;imonomial-term(<c, ws>)) = (c * int_term_value(f;imonomial-term(<1, ws>)\000C)) ∈ ℤ)
Lemma: imonomial-term-add
∀vs:ℤ List. ∀a,b:ℤ-o. ∀f:ℤ ⟶ ℤ. ((int_term_value(f;imonomial-term(<a, vs>)) + int_term_value(f;imonomial-term(<b, vs>)\000C)) = int_term_value(f;imonomial-term(<a + b, vs>)) ∈ ℤ)
Definition: ipolynomial-term
ipolynomial-term(p) ==
if null(p)
then "0"
else let m1,ms = p
in accumulate (with value t and list item m):
t (+) imonomial-term(m)
over list:
ms
with starting value:
imonomial-term(m1))
fi
Lemma: ipolynomial-term_wf
∀[p:iMonomial() List]. (ipolynomial-term(p) ∈ int_term())
Lemma: ipolynomial-term-cons
∀[m:iMonomial()]. ∀[p:iMonomial() List]. ipolynomial-term([m / p]) ≡ imonomial-term(m) (+) ipolynomial-term(p)
Lemma: ipolynomial-term-cons-value
∀[m:iMonomial()]. ∀[p:iMonomial() List].
∀f:ℤ ⟶ ℤ
(int_term_value(f;ipolynomial-term([m / p]))
= (int_term_value(f;imonomial-term(m)) + int_term_value(f;ipolynomial-term(p)))
∈ ℤ)
Definition: add-ipoly
add-ipoly(p;q)
==r eval pp = p in
eval qq = q in
if null(pp) then qq
if null(qq) then pp
else let p1,ps = pp
in let q1,qs = qq
in if imonomial-le(p1;q1)
then if imonomial-le(q1;p1)
then let x ⟵ add-ipoly(ps;qs)
in let cp,vs = p1
in eval c = cp + (fst(q1)) in
if c=0 then x else [<c, vs> / x]
else let x ⟵ add-ipoly(ps;[q1 / qs])
in [p1 / x]
fi
else let x ⟵ add-ipoly([p1 / ps];qs)
in [q1 / x]
fi
fi
Lemma: add-ipoly_wf1
∀[p,q:iMonomial() List]. (add-ipoly(p;q) ∈ iMonomial() List)
Definition: add-ipoly1
add-ipoly1(p;q) == add-ipoly(p;q)
Lemma: add-poly-lemma1
∀p,q:iMonomial() List. ∀m:iMonomial().
((∀i:ℕ||p||. ∀j:ℕi. imonomial-less(p[j];p[i]))
⇒ (∀i:ℕ||q||. ∀j:ℕi. imonomial-less(q[j];q[i]))
⇒ (0 < ||p|| ⇒ imonomial-less(m;p[0]))
⇒ (0 < ||q|| ⇒ imonomial-less(m;q[0]))
⇒ 0 < ||add-ipoly(p;q)||
⇒ imonomial-less(m;add-ipoly(p;q)[0]))
Lemma: add-ipoly-equiv
∀p,q:iMonomial() List. ipolynomial-term(add-ipoly(p;q)) ≡ ipolynomial-term(p) (+) ipolynomial-term(q)
Lemma: add-ipoly_wf
∀[p,q:iPolynomial()]. (add-ipoly(p;q) ∈ iPolynomial())
Definition: add-ipoly-prepend
add-ipoly-prepend(p;q;l)
==r eval pp = p in
eval qq = q in
if pp = Ax then rev(l) + qq
otherwise if qq = Ax then rev(l) + pp otherwise let p1,ps = pp
in let q1,qs = qq
in if imonomial-le(p1;q1)
then if imonomial-le(q1;p1)
then let cp,vs = p1
in eval c = cp + (fst(q1)) in
eval l' = if c=0 then l else [<c, vs> / l] in
add-ipoly-prepend(ps;qs;l')
else add-ipoly-prepend(ps;[q1 / qs];[p1 / l])
fi
else add-ipoly-prepend([p1 / ps];qs;[q1 / l])
fi
Lemma: add-ipoly-wf1
∀p,q:(ℤ × (ℤ List)) List. (add-ipoly(p;q) ∈ (ℤ × (ℤ List)) List)
Lemma: add-ipoly1_wf
∀p,q:(ℤ × (ℤ List)) List. (add-ipoly1(p;q) ∈ (ℤ × (ℤ List)) List)
Lemma: add-poly-prepend-sq1
∀[p,q,l:(ℤ × (ℤ List)) List]. (add-ipoly-prepend(p;q;l) ~ rev(l) + add-ipoly(p;q))
Lemma: add-poly-prepend-sq
∀[p,q,l:iMonomial() List]. (add-ipoly-prepend(p;q;l) ~ rev(l) + add-ipoly(p;q))
Lemma: add-ipoly-prepend_wf
∀[p,q,l:iMonomial() List]. (add-ipoly-prepend(p;q;l) ∈ iMonomial() List)
Definition: add_ipoly
add_ipoly(p;q) == add-ipoly-prepend(p;q;[])
Lemma: add_ipoly-sq
∀[p,q:iMonomial() List]. (add_ipoly(p;q) ~ add-ipoly(p;q))
Lemma: add_ipoly_wf
∀[p,q:iPolynomial()]. (add_ipoly(p;q) ∈ iPolynomial())
Definition: minus-monomial
minus-monomial(m) == let c,vs = m in <-c, vs>
Lemma: minus-monomial_wf
∀[m:iMonomial()]. (minus-monomial(m) ∈ iMonomial())
Definition: minus-poly
minus-poly(p) == map(λm.minus-monomial(m);p)
Lemma: minus-poly_wf
∀[p:iPolynomial()]. (minus-poly(p) ∈ iPolynomial())
Lemma: minus-poly-equiv
∀p:iPolynomial(). ipolynomial-term(minus-poly(p)) ≡ "-"ipolynomial-term(p)
Definition: mul-monomials
mul-monomials(m1;m2) == let a,vs = m1 in let b,ws = m2 in eval c = a * b in eval u = merge-int-accum(vs;ws) in <c, u>
Lemma: mul-monomials_wf
∀[m1,m2:iMonomial()]. (mul-monomials(m1;m2) ∈ iMonomial())
Lemma: mul-monomials-equiv
∀[m1,m2:iMonomial()]. imonomial-term(mul-monomials(m1;m2)) ≡ imonomial-term(m1) (*) imonomial-term(m2)
Definition: even-int-list
even-int-list(L) == null(L) ∨b((¬bnull(tl(L))) ∧b (hd(L) =z hd(tl(L))) ∧b even-int-list(tl(tl(L))))
Lemma: even-int-list_wf
∀[L:ℤ List]. (even-int-list(L) ∈ 𝔹)
Definition: nonneg-monomial
nonneg-monomial(m) == let c,L = m in 0 ≤z c ∧b even-int-list(L)
Lemma: nonneg-monomial_wf
∀[m:iMonomial()]. (nonneg-monomial(m) ∈ 𝔹)
Lemma: assert-nonneg-monomial
∀m:iMonomial(). ((↑nonneg-monomial(m)) ⇒ (∃m':iMonomial(). ∃k:ℕ+. (mul-monomials(m';m') = mul-monomials(m;<k, []>) ∈ iM\000Conomial())))
Definition: mul-mono-poly
mul-mono-poly(m;p) == rec-case(p) of [] => [] | h::t => r.eval m = mul-monomials(m;h) in eval l = r in [m / l]
Lemma: mul-mono-poly_wf1
∀[m:iMonomial()]. ∀[p:iMonomial() List]. (mul-mono-poly(m;p) ∈ iMonomial() List)
Lemma: mul-mono-poly_wf
∀[m:iMonomial()]. ∀[p:iPolynomial()]. (mul-mono-poly(m;p) ∈ iPolynomial())
Lemma: mul-mono-poly-equiv
∀[m:iMonomial()]. ∀[p:iMonomial() List].
ipolynomial-term(mul-mono-poly(m;p)) ≡ imonomial-term(m) (*) ipolynomial-term(p)
Definition: mul-ipoly
mul-ipoly(p;q) ==
let pp ⟵ p
in if null(pp)
then []
else let p1,ps = pp
in let qq ⟵ q
in if null(qq)
then []
else eager-accum(sofar,m.add-ipoly(sofar;mul-mono-poly(m;qq));mul-mono-poly(p1;qq);ps)
fi
fi
Lemma: mul-ipoly_wf
∀[p,q:iPolynomial()]. (mul-ipoly(p;q) ∈ iPolynomial())
Lemma: mul-ipoly-equiv
∀[p,q:iMonomial() List]. ipolynomial-term(mul-ipoly(p;q)) ≡ ipolynomial-term(p) (*) ipolynomial-term(q)
Definition: cbv_list_accum
cbv_list_accum(x,a.f[x; a];y;L) ==
fix((λcbv_list_accum,y,L. eval v = L in
if v is a pair then let h,t = v
in eval y' = f[y; h] in
cbv_list_accum y' t otherwise if v = Ax then y otherwise ⊥))
y
L
Lemma: cbv_list_accum_wf
∀[T,T':Type]. ∀[l:T List]. ∀[y:T']. ∀[f:T' ⟶ T ⟶ T']. cbv_list_accum(x,a.f[x;a];y;l) ∈ T' supposing value-type(T')
Lemma: cbv_list_accum-is-list_accum
∀[T,T':Type]. ∀[l:T List]. ∀[y:T']. ∀[f:T' ⟶ T ⟶ T'].
cbv_list_accum(x,a.f[x;a];y;l) ~ accumulate (with value x and list item a):
f[x;a]
over list:
l
with starting value:
y)
supposing value-type(T')
Definition: mul_ipoly
mul_ipoly(p;q) ==
eval pp = p in
if pp = Ax then []
otherwise let p1,ps = pp
in eval qq = q in
if qq = Ax then []
otherwise cbv_list_accum(sofar,m.add_ipoly(sofar;mul-mono-poly(m;qq));mul-mono-poly(p1;qq);ps)
Lemma: mul_poly-sq
∀[p,q:iMonomial() List]. (mul_ipoly(p;q) ~ mul-ipoly(p;q))
Lemma: mul_ipoly_wf
∀[p,q:iPolynomial()]. (mul_ipoly(p;q) ∈ iPolynomial())
Definition: int_term_to_ipoly
int_term_to_ipoly(t) ==
int_term_ind(t;
itermConstant(c)⇒ if c=0 then [] else [<c, []>];
itermVar(v)⇒ [<1, [v]>];
itermAdd(l,r)⇒ rl,rr.add_ipoly(rl;rr);
itermSubtract(l,r)⇒ rl,rr.add_ipoly(rl;minus-poly(rr));
itermMultiply(l,r)⇒ rl,rr.mul_ipoly(rl;rr);
itermMinus(x)⇒ rx.minus-poly(rx))
Lemma: int_term_to_ipoly_wf
∀[t:int_term()]. (int_term_to_ipoly(t) ∈ iPolynomial())
Definition: int_term_to_rP
int_term_to_rP(t) ==
int_term_ind(t;
itermConstant(c)⇒ [1; c];
itermVar(v)⇒ [2; v];
itermAdd(l,r)⇒ rl,rr.eager-append(rl;eager-append(rr;[3]));
itermSubtract(l,r)⇒ rl,rr.eager-append(rl;eager-append(rr;[4]));
itermMultiply(l,r)⇒ rl,rr.eager-append(rl;eager-append(rr;[5]));
itermMinus(x)⇒ rx.eager-append(rx;[6]))
Lemma: int_term_to_rP_wf
∀[t:int_term()]. (int_term_to_rP(t) ∈ ℤ List)
Definition: rP_to_poly
rP_to_poly(stack;L)
==r if L = Ax then stack otherwise let op,more = L
in if op=1
then let c,evenmore = more
in rP_to_poly([if c=0 then [] else [<c, []>] / stack];evenmore)
else if op=2
then let v,evenmore = more
in rP_to_poly(<[<1, [v]>], stack>;evenmore)
else if op=3
then let q,p,s = stack in
rP_to_poly([add_ipoly(p;q) / s];more)
else if op=4
then let q,p,s = stack in
rP_to_poly([add_ipoly(p;minus-poly(q)) / s];more)
else if op=5
then let q,p,s = stack in
rP_to_poly([mul_ipoly(p;q) / s];more)
else let p,s = stack
in rP_to_poly([minus-poly(p) / s];more)
Lemma: rP_to_poly-int_term_to_rP
∀[t:int_term()]. ∀[s:iPolynomial() List]. (rP_to_poly(s;int_term_to_rP(t)) ~ [int_term_to_ipoly(t) / s])
Definition: rP_to_term
rP_to_term(stack;L)
==r if L = Ax then stack otherwise let op,more = L
in if op=1
then let c,evenmore = more
in rP_to_term(["c" / stack];evenmore)
else if op=2
then let v,evenmore = more
in rP_to_term([vv / stack];evenmore)
else if op=3
then let q,p,s = stack in
rP_to_term([p (+) q / s];more)
else if op=4
then let q,p,s = stack in
rP_to_term([p (-) q / s];more)
else if op=5
then let q,p,s = stack in
rP_to_term([p (*) q / s];more)
else let p,s = stack
in rP_to_term(["-"p / s];more)
Lemma: rP_to_term-int_term_to_rP
∀[t:int_term()]. ∀[s:int_term() List]. (rP_to_term(s;int_term_to_rP(t)) ~ [t / s])
Lemma: int_term_to_ipoly-add
∀[a,b:Top]. (int_term_to_ipoly(a (+) b) ~ add_ipoly(int_term_to_ipoly(a);int_term_to_ipoly(b)))
Lemma: int_term_to_ipoly-sub
∀[a,b:Top]. (int_term_to_ipoly(a (-) b) ~ add_ipoly(int_term_to_ipoly(a);minus-poly(int_term_to_ipoly(b))))
Lemma: int_term_to_ipoly-minus
∀[b:Top]. (int_term_to_ipoly("-"b) ~ minus-poly(int_term_to_ipoly(b)))
Lemma: int_term_to_ipoly-mul
∀[a,b:Top]. (int_term_to_ipoly(a (*) b) ~ mul_ipoly(int_term_to_ipoly(a);int_term_to_ipoly(b)))
Lemma: int_term_to_ipoly-const
∀[c:Top]. (int_term_to_ipoly("c") ~ if c=0 then [] else [<c, []>])
Lemma: int_term_to_ipoly-var
∀[c:Top]. (int_term_to_ipoly(vc) ~ [<1, [c]>])
Lemma: int_term_polynomial
∀t:int_term(). ipolynomial-term(int_term_to_ipoly(t)) ≡ t
Definition: const-poly
const-poly(n) == [<n, []>]
Lemma: const-poly_wf
∀[n:ℤ-o]. (const-poly(n) ∈ iPolynomial())
Lemma: const-poly-value
∀[n,f:Top]. (int_term_value(f;ipolynomial-term(const-poly(n))) ~ n)
Definition: int_formulaco
int_formulaco() ==
corec(X.lbl:Atom × if lbl =a "less" then left:int_term() × int_term()
if lbl =a "le" then left:int_term() × int_term()
if lbl =a "eq" then left:int_term() × int_term()
if lbl =a "and" then left:X × X
if lbl =a "or" then left:X × X
if lbl =a "implies" then left:X × X
if lbl =a "not" then X
else Void
fi )
Lemma: int_formulaco_wf
int_formulaco() ∈ Type
Lemma: int_formulaco-ext
int_formulaco() ≡ lbl:Atom × if lbl =a "less" then left:int_term() × int_term()
if lbl =a "le" then left:int_term() × int_term()
if lbl =a "eq" then left:int_term() × int_term()
if lbl =a "and" then left:int_formulaco() × int_formulaco()
if lbl =a "or" then left:int_formulaco() × int_formulaco()
if lbl =a "implies" then left:int_formulaco() × int_formulaco()
if lbl =a "not" then int_formulaco()
else Void
fi
Definition: int_formulaco_size
int_formulaco_size(p) ==
fix((λsize,p. let lbl,x = p
in if lbl =a "less" then 0
if lbl =a "le" then 0
if lbl =a "eq" then 0
if lbl =a "and" then 1 + (size (fst(x))) + (size (snd(x)))
if lbl =a "or" then 1 + (size (fst(x))) + (size (snd(x)))
if lbl =a "implies" then 1 + (size (fst(x))) + (size (snd(x)))
if lbl =a "not" then 1 + (size x)
else 0
fi ))
p
Lemma: int_formulaco_size_wf
∀[p:int_formulaco()]. (int_formulaco_size(p) ∈ partial(ℕ))
Definition: int_formula
int_formula() == {p:int_formulaco()| (int_formulaco_size(p))↓}
Lemma: int_formula_wf
int_formula() ∈ Type
Definition: int_formula_size
int_formula_size(p) ==
fix((λsize,p. let lbl,x = p
in if lbl =a "less" then 0
if lbl =a "le" then 0
if lbl =a "eq" then 0
if lbl =a "and" then 1 + (size (fst(x))) + (size (snd(x)))
if lbl =a "or" then 1 + (size (fst(x))) + (size (snd(x)))
if lbl =a "implies" then 1 + (size (fst(x))) + (size (snd(x)))
if lbl =a "not" then 1 + (size x)
else 0
fi ))
p
Lemma: int_formula_size_wf
∀[p:int_formula()]. (int_formula_size(p) ∈ ℕ)
Lemma: int_formula-ext
int_formula() ≡ lbl:Atom × if lbl =a "less" then left:int_term() × int_term()
if lbl =a "le" then left:int_term() × int_term()
if lbl =a "eq" then left:int_term() × int_term()
if lbl =a "and" then left:int_formula() × int_formula()
if lbl =a "or" then left:int_formula() × int_formula()
if lbl =a "implies" then left:int_formula() × int_formula()
if lbl =a "not" then int_formula()
else Void
fi
Definition: intformless
(left "<" right) == <"less", left, right>
Lemma: intformless_wf
∀[left,right:int_term()]. ((left "<" right) ∈ int_formula())
Definition: intformle
left "≤" right == <"le", left, right>
Lemma: intformle_wf
∀[left,right:int_term()]. (left "≤" right ∈ int_formula())
Definition: intformeq
left "=" right == <"eq", left, right>
Lemma: intformeq_wf
∀[left,right:int_term()]. (left "=" right ∈ int_formula())
Definition: intformand
left "∧" right == <"and", left, right>
Lemma: intformand_wf
∀[left,right:int_formula()]. (left "∧" right ∈ int_formula())
Definition: intformor
left "or" right == <"or", left, right>
Lemma: intformor_wf
∀[left,right:int_formula()]. (left "or" right ∈ int_formula())
Definition: intformimplies
left "=>" right == <"implies", left, right>
Lemma: intformimplies_wf
∀[left,right:int_formula()]. (left "=>" right ∈ int_formula())
Definition: intformnot
"¬"form == <"not", form>
Lemma: intformnot_wf
∀[form:int_formula()]. ("¬"form ∈ int_formula())
Definition: intformless?
intformless?(v) == fst(v) =a "less"
Lemma: intformless?_wf
∀[v:int_formula()]. (intformless?(v) ∈ 𝔹)
Definition: intformless-left
intformless-left(v) == fst(snd(v))
Lemma: intformless-left_wf
∀[v:int_formula()]. intformless-left(v) ∈ int_term() supposing ↑intformless?(v)
Definition: intformless-right
intformless-right(v) == snd(snd(v))
Lemma: intformless-right_wf
∀[v:int_formula()]. intformless-right(v) ∈ int_term() supposing ↑intformless?(v)
Definition: intformle?
intformle?(v) == fst(v) =a "le"
Lemma: intformle?_wf
∀[v:int_formula()]. (intformle?(v) ∈ 𝔹)
Definition: intformle-left
intformle-left(v) == fst(snd(v))
Lemma: intformle-left_wf
∀[v:int_formula()]. intformle-left(v) ∈ int_term() supposing ↑intformle?(v)
Definition: intformle-right
intformle-right(v) == snd(snd(v))
Lemma: intformle-right_wf
∀[v:int_formula()]. intformle-right(v) ∈ int_term() supposing ↑intformle?(v)
Definition: intformeq?
intformeq?(v) == fst(v) =a "eq"
Lemma: intformeq?_wf
∀[v:int_formula()]. (intformeq?(v) ∈ 𝔹)
Definition: intformeq-left
intformeq-left(v) == fst(snd(v))
Lemma: intformeq-left_wf
∀[v:int_formula()]. intformeq-left(v) ∈ int_term() supposing ↑intformeq?(v)
Definition: intformeq-right
intformeq-right(v) == snd(snd(v))
Lemma: intformeq-right_wf
∀[v:int_formula()]. intformeq-right(v) ∈ int_term() supposing ↑intformeq?(v)
Definition: intformand?
intformand?(v) == fst(v) =a "and"
Lemma: intformand?_wf
∀[v:int_formula()]. (intformand?(v) ∈ 𝔹)
Definition: intformand-left
intformand-left(v) == fst(snd(v))
Lemma: intformand-left_wf
∀[v:int_formula()]. intformand-left(v) ∈ int_formula() supposing ↑intformand?(v)
Definition: intformand-right
intformand-right(v) == snd(snd(v))
Lemma: intformand-right_wf
∀[v:int_formula()]. intformand-right(v) ∈ int_formula() supposing ↑intformand?(v)
Definition: intformor?
intformor?(v) == fst(v) =a "or"
Lemma: intformor?_wf
∀[v:int_formula()]. (intformor?(v) ∈ 𝔹)
Definition: intformor-left
intformor-left(v) == fst(snd(v))
Lemma: intformor-left_wf
∀[v:int_formula()]. intformor-left(v) ∈ int_formula() supposing ↑intformor?(v)
Definition: intformor-right
intformor-right(v) == snd(snd(v))
Lemma: intformor-right_wf
∀[v:int_formula()]. intformor-right(v) ∈ int_formula() supposing ↑intformor?(v)
Definition: intformimplies?
intformimplies?(v) == fst(v) =a "implies"
Lemma: intformimplies?_wf
∀[v:int_formula()]. (intformimplies?(v) ∈ 𝔹)
Definition: intformimplies-left
intformimplies-left(v) == fst(snd(v))
Lemma: intformimplies-left_wf
∀[v:int_formula()]. intformimplies-left(v) ∈ int_formula() supposing ↑intformimplies?(v)
Definition: intformimplies-right
intformimplies-right(v) == snd(snd(v))
Lemma: intformimplies-right_wf
∀[v:int_formula()]. intformimplies-right(v) ∈ int_formula() supposing ↑intformimplies?(v)
Definition: intformnot?
intformnot?(v) == fst(v) =a "not"
Lemma: intformnot?_wf
∀[v:int_formula()]. (intformnot?(v) ∈ 𝔹)
Definition: intformnot-form
intformnot-form(v) == snd(v)
Lemma: intformnot-form_wf
∀[v:int_formula()]. intformnot-form(v) ∈ int_formula() supposing ↑intformnot?(v)
Lemma: int_formula-induction
∀[P:int_formula() ⟶ ℙ]
((∀left,right:int_term(). P[(left "<" right)])
⇒ (∀left,right:int_term(). P[left "≤" right])
⇒ (∀left,right:int_term(). P[left "=" right])
⇒ (∀left,right:int_formula(). (P[left] ⇒ P[right] ⇒ P[left "∧" right]))
⇒ (∀left,right:int_formula(). (P[left] ⇒ P[right] ⇒ P[left "or" right]))
⇒ (∀left,right:int_formula(). (P[left] ⇒ P[right] ⇒ P[left "=>" right]))
⇒ (∀form:int_formula(). (P[form] ⇒ P["¬"form]))
⇒ {∀v:int_formula(). P[v]})
Lemma: int_formula-definition
∀[A:Type]. ∀[R:A ⟶ int_formula() ⟶ ℙ].
((∀left,right:int_term(). {x:A| R[x;(left "<" right)]} )
⇒ (∀left,right:int_term(). {x:A| R[x;left "≤" right]} )
⇒ (∀left,right:int_term(). {x:A| R[x;left "=" right]} )
⇒ (∀left,right:int_formula(). ({x:A| R[x;left]} ⇒ {x:A| R[x;right]} ⇒ {x:A| R[x;left "∧" right]} ))
⇒ (∀left,right:int_formula(). ({x:A| R[x;left]} ⇒ {x:A| R[x;right]} ⇒ {x:A| R[x;left "or" right]} ))
⇒ (∀left,right:int_formula(). ({x:A| R[x;left]} ⇒ {x:A| R[x;right]} ⇒ {x:A| R[x;left "=>" right]} ))
⇒ (∀form:int_formula(). ({x:A| R[x;form]} ⇒ {x:A| R[x;"¬"form]} ))
⇒ {∀v:int_formula(). {x:A| R[x;v]} })
Definition: int_formula_ind
int_formula_ind(v;
intformless(left,right)⇒ less[left; right];
intformle(left,right)⇒ le[left; right];
intformeq(left,right)⇒ eq[left; right];
intformand(left,right)⇒ rec1,rec2.and[left;
right;
rec1;
rec2];
intformor(left,right)⇒ rec3,rec4.or[left;
right;
rec3;
rec4];
intformimplies(left,right)⇒ rec5,rec6.implies[left;
right;
rec5;
rec6];
intformnot(form)⇒ rec7.not[form; rec7]) ==
fix((λint_formula_ind,v. let lbl,v1 = v
in if lbl="less" then let left,v2 = v1 in less[left; v2]
if lbl="le" then let left,v2 = v1 in le[left; v2]
if lbl="eq" then let left,v2 = v1 in eq[left; v2]
if lbl="and"
then let left,v2 = v1
in and[left;
v2;
int_formula_ind left;
int_formula_ind v2]
if lbl="or"
then let left,v2 = v1
in or[left;
v2;
int_formula_ind left;
int_formula_ind v2]
if lbl="implies"
then let left,v2 = v1
in implies[left;
v2;
int_formula_ind left;
int_formula_ind v2]
if lbl="not" then not[v1; int_formula_ind v1]
else Ax
fi ))
v
Lemma: int_formula_ind_wf
∀[A:Type]. ∀[R:A ⟶ int_formula() ⟶ ℙ]. ∀[v:int_formula()]. ∀[less:left:int_term()
⟶ right:int_term()
⟶ {x:A| R[x;(left "<" right)]} ].
∀[le:left:int_term() ⟶ right:int_term() ⟶ {x:A| R[x;left "≤" right]} ]. ∀[eq:left:int_term()
⟶ right:int_term()
⟶ {x:A| R[x;left "=" right]} ].
∀[and:left:int_formula() ⟶ right:int_formula() ⟶ {x:A| R[x;left]} ⟶ {x:A| R[x;right]} ⟶ {x:A| R[x;left "∧" right]}\000C ].
∀[or:left:int_formula() ⟶ right:int_formula() ⟶ {x:A| R[x;left]} ⟶ {x:A| R[x;right]} ⟶ {x:A| R[x;left "or" right]}\000C ].
∀[implies:left:int_formula()
⟶ right:int_formula()
⟶ {x:A| R[x;left]}
⟶ {x:A| R[x;right]}
⟶ {x:A| R[x;left "=>" right]} ]. ∀[not:form:int_formula() ⟶ {x:A| R[x;form]} ⟶ {x:A| R[x;"¬"form]} ].
(int_formula_ind(v;
intformless(left,right)⇒ less[left;right];
intformle(left,right)⇒ le[left;right];
intformeq(left,right)⇒ eq[left;right];
intformand(left,right)⇒ rec1,rec2.and[left;right;rec1;rec2];
intformor(left,right)⇒ rec3,rec4.or[left;right;rec3;rec4];
intformimplies(left,right)⇒ rec5,rec6.implies[left;right;rec5;rec6];
intformnot(form)⇒ rec7.not[form;rec7]) ∈ {x:A| R[x;v]} )
Lemma: int_formula_ind_wf_simple
∀[A:Type]. ∀[v:int_formula()]. ∀[less,le,eq:left:int_term() ⟶ right:int_term() ⟶ A].
∀[and,or,implies:left:int_formula() ⟶ right:int_formula() ⟶ A ⟶ A ⟶ A]. ∀[not:form:int_formula() ⟶ A ⟶ A].
(int_formula_ind(v;
intformless(left,right)⇒ less[left;right];
intformle(left,right)⇒ le[left;right];
intformeq(left,right)⇒ eq[left;right];
intformand(left,right)⇒ rec1,rec2.and[left;right;rec1;rec2];
intformor(left,right)⇒ rec3,rec4.or[left;right;rec3;rec4];
intformimplies(left,right)⇒ rec5,rec6.implies[left;right;rec5;rec6];
intformnot(form)⇒ rec7.not[form;rec7]) ∈ A)
Definition: int_formula_prop
int_formula_prop(f;fmla) ==
int_formula_ind(fmla;
a,b.int_term_value(f;a) < int_term_value(f;b);
a,b.int_term_value(f;a) ≤ int_term_value(f;b);
a,b.int_term_value(f;a) = int_term_value(f;b) ∈ ℤ;
X,Y,PX,PY.PX ∧ PY;
X,Y,PX,PY.PX ∨ PY;
X,Y,PX,PY.PX ⇒ PY;
X,PX.¬PX)
Lemma: int_formula_prop_wf
∀[f:ℤ ⟶ ℤ]. ∀[fmla:int_formula()]. (int_formula_prop(f;fmla) ∈ ℙ)
Lemma: istype-int_formula_prop
∀[f:ℤ ⟶ ℤ]. ∀[fmla:int_formula()]. istype(int_formula_prop(f;fmla))
Lemma: int_formula_prop_and_lemma
∀y,x,f:Top. (int_formula_prop(f;x "∧" y) ~ int_formula_prop(f;x) ∧ int_formula_prop(f;y))
Lemma: int_formula_prop_or_lemma
∀y,x,f:Top. (int_formula_prop(f;x "or" y) ~ int_formula_prop(f;x) ∨ int_formula_prop(f;y))
Lemma: int_formual_prop_imp_lemma
∀y,x,f:Top. (int_formula_prop(f;x "=>" y) ~ int_formula_prop(f;x) ⇒ int_formula_prop(f;y))
Lemma: int_formula_prop_not_lemma
∀x,f:Top. (int_formula_prop(f;"¬"x) ~ ¬int_formula_prop(f;x))
Lemma: int_formula_prop_le_lemma
∀y,x,f:Top. (int_formula_prop(f;x "≤" y) ~ int_term_value(f;x) ≤ int_term_value(f;y))
Lemma: int_formula_prop_less_lemma
∀y,x,f:Top. (int_formula_prop(f;(x "<" y)) ~ int_term_value(f;x) < int_term_value(f;y))
Lemma: int_formula_prop_eq_lemma
∀y,x,f:Top. (int_formula_prop(f;x "=" y) ~ int_term_value(f;x) = int_term_value(f;y) ∈ ℤ)
Lemma: int_formula-subtype-base
int_formula() ⊆r Base
Definition: satisfiable_int_formula
satisfiable_int_formula(fmla) == ∃f:ℤ ⟶ ℤ. int_formula_prop(f;fmla)
Lemma: satisfiable_int_formula_wf
∀[fmla:int_formula()]. (satisfiable_int_formula(fmla) ∈ ℙ)
Definition: polynomial-constraints
polynomial-constraints() == iPolynomial() List × (iPolynomial() List)
Lemma: polynomial-constraints_wf
polynomial-constraints() ∈ Type
Definition: satisfies-poly-constraints
satisfies-poly-constraints(f;X) ==
let eqs,ineqs = X
in (∀p∈eqs.int_term_value(f;ipolynomial-term(p)) = 0 ∈ ℤ) ∧ (∀p∈ineqs.0 ≤ int_term_value(f;ipolynomial-term(p)))
Lemma: satisfies-poly-constraints_wf
∀[f:ℤ ⟶ ℤ]. ∀[X:polynomial-constraints()]. (satisfies-poly-constraints(f;X) ∈ ℙ)
Definition: satisfiable_polynomial_constraints
satisfiable_polynomial_constraints(X) == ∃f:ℤ ⟶ ℤ. satisfies-poly-constraints(f;X)
Lemma: satisfiable_polynomial_constraints_wf
∀[X:polynomial-constraints()]. (satisfiable_polynomial_constraints(X) ∈ ℙ)
Definition: combine-pcs
combine-pcs(X;Y) == let eqsX,ineqsX = X in let eqsY,ineqsY = Y in <eqsX @ eqsY, ineqsX @ ineqsY>
Lemma: combine-pcs_wf
∀[X,Y:polynomial-constraints()]. (combine-pcs(X;Y) ∈ polynomial-constraints())
Lemma: satisfies-combine-pcs
∀f:ℤ ⟶ ℤ. ∀A,B:polynomial-constraints().
(satisfies-poly-constraints(f;combine-pcs(A;B)) ⇐⇒ satisfies-poly-constraints(f;A) ∧ satisfies-poly-constraints(f;B))
Definition: and-poly-constraints
and-poly-constraints(Xs;Ys) ==
accumulate (with value sofar and list item Y):
accumulate (with value sofar' and list item X):
[combine-pcs(X;Y) / sofar']
over list:
Xs
with starting value:
sofar)
over list:
Ys
with starting value:
[])
Lemma: and-poly-constraints_wf
∀[Xs,Ys:polynomial-constraints() List]. (and-poly-constraints(Xs;Ys) ∈ polynomial-constraints() List)
Lemma: member-and-poly-constraints
∀L1,L2:polynomial-constraints() List. ∀X:polynomial-constraints().
((X ∈ and-poly-constraints(L1;L2)) ⇐⇒ (∃A∈L1. (∃B∈L2. X = combine-pcs(A;B) ∈ polynomial-constraints())))
Lemma: satisfies-and-poly-constraints
∀f:ℤ ⟶ ℤ. ∀L2,L1:polynomial-constraints() List.
((∃X∈L1. satisfies-poly-constraints(f;X)) ∧ (∃X∈L2. satisfies-poly-constraints(f;X))
⇐⇒ (∃X∈and-poly-constraints(L1;L2). satisfies-poly-constraints(f;X)))
Definition: negate-poly-constraint
negate-poly-constraint(X) ==
let eqs,ineqs = X
in accumulate (with value pcs and list item e):
[<[], [minus-poly(add-ipoly(e;const-poly(1)))]>; [<[], [add-ipoly(e;const-poly(-1))]> / pcs]]
over list:
eqs
with starting value:
map(λineq.<[], [minus-poly(add-ipoly(ineq;const-poly(1)))]>;ineqs))
Lemma: negate-poly-constraint_wf
∀[X:polynomial-constraints()]. (negate-poly-constraint(X) ∈ polynomial-constraints() List)
Lemma: satisfies-negate-poly-constraint
∀X:polynomial-constraints(). ∀f:ℤ ⟶ ℤ.
((∃Z∈negate-poly-constraint(X). satisfies-poly-constraints(f;Z)) ⇐⇒ ¬satisfies-poly-constraints(f;X))
Definition: negate-poly-constraints
negate-poly-constraints(Xs) ==
if null(Xs)
then [<[], []>]
else let x,more = Xs
in accumulate (with value sofar and list item X):
and-poly-constraints(sofar;negate-poly-constraint(X))
over list:
more
with starting value:
negate-poly-constraint(x))
fi
Lemma: negate-poly-constraints_wf
∀[Xs:polynomial-constraints() List]. (negate-poly-constraints(Xs) ∈ polynomial-constraints() List)
Lemma: satisfies-negate-poly-constraints
∀f:ℤ ⟶ ℤ. ∀L:polynomial-constraints() List.
((∀X∈L.¬satisfies-poly-constraints(f;X)) ⇐⇒ (∃X∈negate-poly-constraints(L). satisfies-poly-constraints(f;X)))
Definition: int_formula_dnf
int_formula_dnf(fmla) ==
int_formula_ind(fmla;
a,b.[<[], [int_term_to_ipoly(b (-) a (+) "1")]>];
a,b.[<[], [int_term_to_ipoly(b (-) a)]>];
a,b.[<[int_term_to_ipoly(b (-) a)], []>];
X,Y,nfX,nfY.and-poly-constraints(nfX;nfY);
X,Y,nfX,nfY.nfX @ nfY;
X,Y,nfX,nfY.negate-poly-constraints(nfX) @ nfY;
X,nfX.negate-poly-constraints(nfX))
Lemma: int_formula_dnf_wf
∀[fmla:int_formula()]. (int_formula_dnf(fmla) ∈ polynomial-constraints() List)
Lemma: satisfies_int_formula_dnf
∀fmla:int_formula(). ∀f:ℤ ⟶ ℤ.
(int_formula_prop(f;fmla) ⇐⇒ (∃X∈int_formula_dnf(fmla). satisfies-poly-constraints(f;X)))
Lemma: satisfiable_int_formula_dnf
∀fmla:int_formula()
(satisfiable_int_formula(fmla) ⇐⇒ (∃X∈int_formula_dnf(fmla). satisfiable_polynomial_constraints(X)))
Definition: polynomial-mon-vars
polynomial-mon-vars(init;p) ==
accumulate (with value vss and list item m):
let c,vs = m
in insert(vs;vss)
over list:
p
with starting value:
init)
Lemma: polynomial-mon-vars_wf
∀[init:ℤ List List]. ∀[p:(Top × (ℤ List)) List]. (polynomial-mon-vars(init;p) ∈ ℤ List List)
Lemma: member-polynomial-mon-vars
∀p:iMonomial() List. ∀L:ℤ List List. ∀vs:ℤ List.
((vs ∈ polynomial-mon-vars(L;p)) ⇐⇒ (vs ∈ L) ∨ (∃m∈p. vs = (snd(m)) ∈ (ℤ List)))
Lemma: no_repeats-polynomial-mon-vars
∀p:iMonomial() List. ∀L:ℤ List List. (no_repeats(ℤ List;L) ⇒ no_repeats(ℤ List;polynomial-mon-vars(L;p)))
Definition: pcs-mon-vars
pcs-mon-vars(X) ==
let eqs,ineqs = X
in accumulate (with value vs and list item p):
polynomial-mon-vars(vs;p)
over list:
ineqs
with starting value:
accumulate (with value vs and list item p):
polynomial-mon-vars(vs;p)
over list:
eqs
with starting value:
[[]]))
Lemma: pcs-mon-vars_wf
∀[X:polynomial-constraints()]. (pcs-mon-vars(X) ∈ ℤ List List)
Lemma: member-pcs-mon-vars
∀X:polynomial-constraints(). ∀vs:ℤ List.
((vs ∈ pcs-mon-vars(X))
⇐⇒ (vs = [] ∈ (ℤ List))
∨ (∃p∈fst(X). (∃m∈p. vs = (snd(m)) ∈ (ℤ List)))
∨ (∃p∈snd(X). (∃m∈p. vs = (snd(m)) ∈ (ℤ List))))
Lemma: no_repeats-pcs-mon-vars
∀X:polynomial-constraints(). no_repeats(ℤ List;pcs-mon-vars(X))
Lemma: hd-rev-pcs-mon-vars
∀X:polynomial-constraints(). (0 < ||rev(pcs-mon-vars(X))|| ∧ (hd(rev(pcs-mon-vars(X))) = [] ∈ (ℤ List)))
Definition: poly-coeff-of
poly-coeff-of(vs;p) ==
rec-case(p) of
[] => 0
m::ps2 =>
r.let c,ws = m
in if ws ≤_lex vs then if vs ≤_lex ws then c else r fi else 0 fi
Lemma: poly-coeff-of_wf
∀[vs:ℤ List]. ∀[p:iPolynomial()]. (poly-coeff-of(vs;p) ∈ ℤ)
Definition: linearization
linearization(p;L) == map(λvs.poly-coeff-of(vs;p);L)
Lemma: linearization_wf
∀[p:iPolynomial()]. ∀[L:ℤ List List]. (linearization(p;L) ∈ {cs:ℤ List| ||cs|| = ||L|| ∈ ℤ} )
Lemma: linearization-value
∀[L:ℤ List List]. ∀[p:iPolynomial()].
∀f:ℤ ⟶ ℤ
(int_term_value(f;ipolynomial-term(p))
= linearization(p;L) ⋅ map(λvs.accumulate (with value x and list item v):
x * (f v)
over list:
vs
with starting value:
1);L)
∈ ℤ)
supposing (∀m∈p.(snd(m) ∈ L)) ∧ no_repeats(ℤ List;L)
Definition: pcs-to-integer-problem
pcs-to-integer-problem(X) ==
eval L = rev(pcs-mon-vars(X)) in
let polyeqs,polyineqs = X
in eval eqs = evalall(eager-map(λp.linearization(p;L);polyeqs)) in
eval ineqs = evalall(eager-map(λp.linearization(p;L);polyineqs)) in
<eqs, ineqs>
Lemma: pcs-to-integer-problem_wf
∀[X:polynomial-constraints()]
(pcs-to-integer-problem(X) ∈ ⋃n:ℕ.({L:ℤ List| ||L|| = (n + 1) ∈ ℤ} List × ({L:ℤ List| ||L|| = (n + 1) ∈ ℤ} List)))
Definition: satisfies-integer-problem
satisfies-integer-problem(eqs;ineqs;xs) == (∀as∈eqs.xs ⋅ as =0) ∧ (∀bs∈ineqs.xs ⋅ bs ≥0)
Lemma: satisfies-integer-problem_wf
∀[eqs,ineqs:ℤ List List]. ∀[xs:ℤ List]. (satisfies-integer-problem(eqs;ineqs;xs) ∈ ℙ)
Definition: satisfiable-integer-problem
satisfiable(eqs;ineqs) == ∃xs:ℤ List. satisfies-integer-problem(eqs;ineqs;xs)
Lemma: satisfiable-integer-problem_wf
∀[eqs,ineqs:ℤ List List]. (satisfiable(eqs;ineqs) ∈ ℙ)
Lemma: satisfiable-pcs-to-integer-problem
∀X:polynomial-constraints()
(satisfiable_polynomial_constraints(X) ⇒ satisfiable(fst(pcs-to-integer-problem(X));snd(pcs-to-integer-problem(X))))
Lemma: satisfies-integer-problem-length
∀[eqs,ineqs:ℤ List List]. ∀[xs:ℤ List].
{(∀e∈eqs.||e|| = ||xs|| ∈ ℤ) ∧ (∀e∈ineqs.||e|| = ||xs|| ∈ ℤ)} supposing satisfies-integer-problem(eqs;ineqs;xs)
Definition: exact-eq-constraint
exact-eq-constraint(eqs;i;j) == |eqs[i][j]| = 1 ∈ ℤ
Lemma: exact-eq-constraint_wf
∀[eqs:ℤ List List]. ∀[i:ℕ||eqs||]. ∀[j:ℕ||eqs[i]||]. (exact-eq-constraint(eqs;i;j) ∈ ℙ)
Lemma: exact-eq-constraint-implies
∀[eqs:ℤ List List]. ∀[i:ℕ||eqs||]. ∀[j:ℕ||eqs[i]||].
∀ineqs:ℤ List List. ∀xs:ℤ List.
(satisfies-integer-problem(eqs;ineqs;xs)
⇒ (xs[j] = if (eqs[i][j] =z 1) then -1 * eqs[i]\j ⋅ xs\j else eqs[i]\j ⋅ xs\j fi ∈ ℤ))
supposing exact-eq-constraint(eqs;i;j)
Definition: exact-reduce-constraints
exact-reduce-constraints(w;j;L) == evalall(map(λv.-(w[j] * v[j]) * w\j + v\j;L))
Lemma: exact-reduce-constraints_wf
∀[w:ℤ List]. ∀[j:ℕ||w||]. ∀[L:{l:ℤ List| ||l|| = ||w|| ∈ ℤ} List].
(exact-reduce-constraints(w;j;L) ∈ {l:ℤ List| ||l|| = (||w|| - 1) ∈ ℤ} List)
Lemma: exact-reduce-constraints-sqequal
∀[w:ℤ List]. ∀[j:ℕ||w||]. ∀[L:{l:ℤ List| ||l|| = ||w|| ∈ ℤ} List].
(exact-reduce-constraints(w;j;L) ~ map(λv.-(w[j] * v[j]) * w\j + v\j;L))
Lemma: satisfiable-exact-reduce-constraints
∀eqs:ℤ List List. ∀i:ℕ||eqs||. ∀j:ℕ+||eqs[i]||.
∀ineqs:ℤ List List
(satisfiable(eqs;ineqs)
⇒ satisfiable(exact-reduce-constraints(eqs[i];j;eqs);exact-reduce-constraints(eqs[i];j;ineqs)))
supposing exact-eq-constraint(eqs;i;j)
Lemma: satisfiable-elim-eq-constraints
∀eqs,ineqs:ℤ List List. ∀xs:ℤ List.
(satisfies-integer-problem(eqs;ineqs;xs)
⇒ satisfies-integer-problem([];(eager-map(λeq.eager-map(λx.(-x);eq);eqs) @ eqs) @ ineqs;xs))
Definition: gcd-reduce-eq-constraints
Each equality constraint is a list [c,a1,a2,...] and represents the
constraint c + a1*v1 + a2*v2 + .... = 0 (on variables v1, v2, ...).
If g = gcd(a1,a2,...) is greater than 1, then if c is not divisible by g
then the constraint is unsatisfiable.
Otherwise we can divide c and all the a1,a2,... by g and preserve
satisfiability.⋅
gcd-reduce-eq-constraints(sat;LL) ==
accumulate_abort(L,Ls.let h,t = L
in if t = Ax then if h=0 then inl [L / Ls] else (inr ⋅ )
otherwise eval g = |gcd-list(t)| in
if (1) < (g)
then if h rem g=0
then eval L' = eager-map(λx.(x ÷ g);L) in
inl [L' / Ls]
else (inr ⋅ )
else (inl [L / Ls]);inl sat;LL)
Lemma: gcd-reduce-eq-constraints_wf
∀[LL,sat:ℤ List+ List]. (gcd-reduce-eq-constraints(sat;LL) ∈ ℤ List+ List?)
Lemma: member-gcd-reduce-constraints
∀n:ℕ+. ∀eqs,sat:{L:ℤ List| ||L|| = n ∈ ℤ} List. ∀cc:{L:ℤ List| ||L|| = n ∈ ℤ} .
((↑isl(gcd-reduce-eq-constraints(sat;eqs))) ⇒ (cc ∈ sat) ⇒ (cc ∈ outl(gcd-reduce-eq-constraints(sat;eqs))))
Lemma: satisfies-gcd-reduce-eq-constraints
∀[n:ℕ+]. ∀[eqs,sat:{L:ℤ List| ||L|| = n ∈ ℤ} List]. ∀[xs:{L:ℤ List| ||L|| = n ∈ ℤ} ].
uiff((∀as∈eqs.xs ⋅ as =0);(↑isl(gcd-reduce-eq-constraints(sat;eqs)))
∧ (∀as∈outl(gcd-reduce-eq-constraints(sat;eqs)).xs ⋅ as =0))
supposing (∀as∈sat.xs ⋅ as =0) ∧ 0 < ||xs|| ∧ (hd(xs) = 1 ∈ ℤ)
Definition: gcd-reduce-ineq-constraints
Each inequality constraint is a list [c,a1,a2,...] and represents the
constraint c + a1*v1 + a2*v2 + .... >= 0 (on variables v1, v2, ...).
If g = gcd(a1,a2,...) is greater than 1 then we
divide all the a1,a2,... by g and replace c by the "floor" of ⌜c ÷ g⌝.
This preserves the satisfiability of the inequality.⋅
gcd-reduce-ineq-constraints(sat;LL) ==
accumulate_abort(L,Ls.let h,t = L
in if t = Ax then if (h) < (0) then inr ⋅ else (inl [L / Ls])
otherwise eval g = |gcd-list(t)| in
if (1) < (g)
then eval h' = h ÷↓ g in
eval t' = eager-map(λx.(x ÷ g);t) in
inl [[h' / t'] / Ls]
else (inl [L / Ls]);inl sat;LL)
Lemma: gcd-reduce-ineq-constraints_wf
∀[LL,sat:ℤ List+ List]. (gcd-reduce-ineq-constraints(sat;LL) ∈ ℤ List+ List?)
Lemma: member-gcd-reduce-ineq-constraints
∀n:ℕ+. ∀ineqs,sat:{L:ℤ List| ||L|| = n ∈ ℤ} List. ∀cc:{L:ℤ List| ||L|| = n ∈ ℤ} .
((↑isl(gcd-reduce-ineq-constraints(sat;ineqs))) ⇒ (cc ∈ sat) ⇒ (cc ∈ outl(gcd-reduce-ineq-constraints(sat;ineqs))))
Lemma: satisfies-gcd-reduce-ineq-constraints
∀[n:ℕ+]. ∀[ineqs,sat:{L:ℤ List| ||L|| = n ∈ ℤ} List]. ∀[xs:{L:ℤ List| ||L|| = n ∈ ℤ} ].
uiff((∀as∈ineqs.xs ⋅ as ≥0);(↑isl(gcd-reduce-ineq-constraints(sat;ineqs)))
∧ (∀as∈outl(gcd-reduce-ineq-constraints(sat;ineqs)).xs ⋅ as ≥0))
supposing (∀as∈sat.xs ⋅ as ≥0) ∧ 0 < ||xs|| ∧ (hd(xs) = 1 ∈ ℤ)
Definition: shadow-inequalities
For the given index, i, divide the inequality constraints into ,
those where the i-th coefficient is >0, and those where it is <0
(and ignore -- hence delete -- those where the i-th coefficient is =0)
For each as in the first part and each bs in the second part, form the
"shadow-vec". The list of all of these is the new set of constraints
in which the i-th variable has been eliminated.
In the worst case, N constraints in k+1 variables can result in
(N/2)*(N/2) = N^2/4 constraints in k variables. But this does not seem
to happen in practice for typical theorem proving applications.⋅
shadow-inequalities(i;ineqs) ==
eval Z = evalall(map(λL.L\i;filter(λL.(L[i] =z 0);ineqs))) in
eager-append(eager-product-map(λas,bs. shadow-vec(i;as;bs);filter(λL.0 <z L[i];ineqs);filter(λL.L[i] <z 0;ineqs));Z)
Lemma: shadow-inequalities_wf
∀[n:ℕ]. ∀[ineqs:{L:ℤ List| ||L|| = n ∈ ℤ} List]. ∀[i:ℕn].
(shadow-inequalities(i;ineqs) ∈ {L:ℤ List| ||L|| = (n - 1) ∈ ℤ} List)
Lemma: satisfies-shadow-inequalities
∀[n:ℕ]. ∀[ineqs:{L:ℤ List| ||L|| = n ∈ ℤ} List]. ∀[i:ℕ+n]. ∀[xs:ℤ List].
(∀as∈shadow-inequalities(i;ineqs).xs\i ⋅ as ≥0) supposing (∀as∈ineqs.xs ⋅ as ≥0)
Definition: max_tl_coeffs
max_tl_coeffs(ineqs) == eager-accum(L1,ineq.map2(λx,y. imax(x;|y|);L1;tl(ineq));map(λx.|x|;tl(hd(ineqs)));tl(ineqs))
Lemma: max_tl_coeffs_wf
∀[n:ℕ+]. ∀[ineqs:{L:ℤ List| ||L|| = n ∈ ℤ} List+]. (max_tl_coeffs(ineqs) ∈ {L:ℤ List| ||L|| = (n - 1) ∈ ℤ} )
Definition: shadow_inequalities
Find the variable whose maximum coefficient (in any of the constraints) is
the least, and eliminate that variable by computing its
"shadow inequalities". This the the heuristic used by Bill Pugh in the
original version of the omega test.⋅
shadow_inequalities(ineqs) ==
if ineqs = Ax then ineqs otherwise eval i = index-of-min(max_tl_coeffs(ineqs)) + 1 in
shadow-inequalities(i;ineqs)
Lemma: shadow_inequalities_wf
∀[n:{2...}]. ∀[ineqs:{L:ℤ List| ||L|| = n ∈ ℤ} List]. (shadow_inequalities(ineqs) ∈ {L:ℤ List| ||L|| = (n - 1) ∈ ℤ} L\000Cist)
Lemma: satisfies-shadow_inequalities
∀[n:{2...}]
∀ineqs:{L:ℤ List| ||L|| = n ∈ ℤ} List
((∃xs:ℤ List. (∀as∈ineqs.xs ⋅ as ≥0)) ⇒ (∃xs:ℤ List. (∀as∈shadow_inequalities(ineqs).xs ⋅ as ≥0)))
Definition: test-exact-eq-constraint
test-exact-eq-constraint(L) ==
rec-case(L) of
[] => inr ⋅
a::as =>
r.if (|a| =z 1) then inl 0 else case r of inl(n) => inl (n + 1) | inr(x) => inr x fi
Lemma: test-exact-eq-constraint_wf
∀[L:ℤ List]. (test-exact-eq-constraint(L) ∈ ∃i:ℕ||L|| [(|L[i]| = 1 ∈ ℤ)]?)
Definition: find-exact-eq-constraint
find-exact-eq-constraint(L) ==
let a,as = L
in case test-exact-eq-constraint(as) of inl(n) => inl <L, n + 1> | inr(x) => inr x
Lemma: find-exact-eq-constraint_wf
∀[L:ℤ List]. find-exact-eq-constraint(L) ∈ x:{x:ℤ List| x = L ∈ (ℤ List)} × {i:ℕ+||L||| |L[i]| = 1 ∈ ℤ} ? supposing 0 <\000C ||L||
Definition: int-constraint-problem
IntConstraints == ⋃n:ℕ.({L:ℤ List| ||L|| = (n + 1) ∈ ℤ} List × ({L:ℤ List| ||L|| = (n + 1) ∈ ℤ} List))?
Lemma: int-constraint-problem_wf
IntConstraints ∈ Type
Definition: satisfies-int-constraint-problem
xs |= p == case p of inl(q) => let eqs,ineqs = q in (∀as∈eqs.xs ⋅ as =0) ∧ (∀bs∈ineqs.xs ⋅ bs ≥0) | inr(_) => False
Lemma: satisfies-int-constraint-problem_wf
∀[p:IntConstraints]. ∀[xs:ℤ List]. (xs |= p ∈ ℙ)
Definition: unsat-int-problem
unsat(p) == ∀xs:ℤ List. (¬xs |= p)
Lemma: unsat-int-problem_wf
∀[p:IntConstraints]. (unsat(p) ∈ ℙ)
Definition: int-problem-dimension
If the integer problem is known to be unsatisfiable (the inr case) then
it has dimension 0. Otherwise, all the constraints are lists of the
same length, [c,a1,a2,...] representing the linear form
c+ a1*v1 + a2*v2 + ...., so the dimension is the length of (any of) these
lists decremented by 1.⋅
dim(p) ==
case p
of inl(q) =>
let eqs,ineqs = q
in if eqs = Ax then if ineqs = Ax then 0 otherwise ||hd(ineqs)|| - 1 otherwise ||hd(eqs)|| - 1
| inr(_) =>
0
Lemma: int-problem-dimension_wf
∀[p:IntConstraints]. (dim(p) ∈ ℕ)
Definition: num-eq-constraints
num-eq-constraints(p) == case p of inl(q) => ||fst(q)|| | inr(_) => 0
Lemma: num-eq-constraints_wf
∀[p:IntConstraints]. (num-eq-constraints(p) ∈ ℕ)
Definition: rep_int_constraint_step
Keep applying f as long as the dimension of the "integer problem" p is
greater than 0.⋅
rep_int_constraint_step(f;p)==r if (0) < (dim(p)) then let p' ⟵ f p in rep_int_constraint_step(f;p') else p
Lemma: rep_int_constraint_step_wf
∀[f:IntConstraints ⟶ IntConstraints]. ∀[p:IntConstraints].
rep_int_constraint_step(f;p) ∈ {p:IntConstraints| dim(p) = 0 ∈ ℤ}
supposing ∀p:IntConstraints
(0 < dim(p)
⇒ (dim(f p) < dim(p) ∨ ((dim(f p) = dim(p) ∈ ℤ) ∧ num-eq-constraints(f p) < num-eq-constraints(p))))
Lemma: isr-rep_int_constraint_step
∀[f:IntConstraints ⟶ IntConstraints]. ∀[p:IntConstraints].
(unsat(p)) supposing
((↑isr(rep_int_constraint_step(f;p))) and
((∀p:IntConstraints
(0 < dim(p)
⇒ (dim(f p) < dim(p) ∨ ((dim(f p) = dim(p) ∈ ℤ) ∧ num-eq-constraints(f p) < num-eq-constraints(p)))))
∧ (∀p:IntConstraints. (unsat(f p) ⇒ unsat(p)))))
Lemma: gcd-reduce-ineq-constraints_wf2
∀[n:ℕ]. ∀[LL,sat:{L:ℤ List| ||L|| = (n + 1) ∈ ℤ} List].
(gcd-reduce-ineq-constraints(sat;LL) ∈ {L:ℤ List| ||L|| = (n + 1) ∈ ℤ} List?)
Lemma: gcd-reduce-eq-constraints_wf2
∀[n:ℕ]. ∀[LL,sat:{L:ℤ List| ||L|| = (n + 1) ∈ ℤ} List].
(gcd-reduce-eq-constraints(sat;LL) ∈ {L:ℤ List| ||L|| = (n + 1) ∈ ℤ} List?)
Lemma: exact-reduce-constraints_wf2
∀[n:ℕ]. ∀[w:{l:ℤ List| ||l|| = (n + 1) ∈ ℤ} ]. ∀[j:ℕ||w||]. ∀[L:{l:ℤ List| ||l|| = (n + 1) ∈ ℤ} List].
(exact-reduce-constraints(w;j;L) ∈ {l:ℤ List| ||l|| = ((n - 1) + 1) ∈ ℤ} List)
Definition: omega_step
The "omega step" first searches for an "exact" equality constraint (one where
the coefficient of a variable is 1 or -1). In that case, the constraint can
be solved exactly for that variable, and the variable can be eliminated.
(If that happens, we then run the "gcd-reduce" operations on the resulting
constraints.)
If there is no exact equality constraint, but there are still equality
constraints, then we convert each remaining equality constraints into
two inequality constraints. (Bill Pugh has a better procedure for
dealing with in-exact equality constraints, but we haven't implemented it.)
If there are no more equality constraints, then omega computes the
"shadow inequalities" for a chosen variable -- which eliminates that variable.
⋅
omega_step(p) ==
if (dim(p)) < (1)
then p
else case p
of inl(q) =>
let eqs,ineqs = q
in case first-success(λL.find-exact-eq-constraint(L);eqs)
of inl(tr) =>
let i,wj = tr
in let w,j = wj
in case gcd-reduce-eq-constraints([];exact-reduce-constraints(w;j;eqs))
of inl(eqs') =>
case gcd-reduce-ineq-constraints([];exact-reduce-constraints(w;j;ineqs))
of inl(ineqs') =>
inl <eqs', ineqs'>
| inr(x) =>
inr x
| inr(x) =>
inr x
| inr(_) =>
if null(eqs)
then case gcd-reduce-ineq-constraints([];shadow_inequalities(ineqs))
of inl(ineqs') =>
inl <[], ineqs'>
| inr(x) =>
inr x
else inl <[], (eager-map(λeq.eager-map(λx.(-x);eq);eqs) @ eqs) @ ineqs>
fi
| inr(_) =>
p
Lemma: omega_step_wf
∀[p:IntConstraints]. (omega_step(p) ∈ IntConstraints)
Lemma: omega_step_measure
∀p:IntConstraints
(0 < dim(p)
⇒ (dim((λp.omega_step(p)) p) < dim(p)
∨ ((dim((λp.omega_step(p)) p) = dim(p) ∈ ℤ) ∧ num-eq-constraints((λp.omega_step(p)) p) < num-eq-constraints(p))))
Lemma: unsat-omega_step
∀p:IntConstraints. (unsat(omega_step(p)) ⇒ unsat(p))
Definition: omega_start
To create starting state of omega, we "gcd-reduce" the constraints.
This can sometimes detect that the equality constraints are unsatisfiable.⋅
omega_start(eqs;ineqs) ==
case gcd-reduce-eq-constraints([];eqs)
of inl(eqs') =>
case gcd-reduce-ineq-constraints([];ineqs) of inl(ineqs') => inl <eqs', ineqs'> | inr(x) => inr x
| inr(x) =>
inr x
Lemma: omega_start_wf
∀[n:ℕ]. ∀[eqs,ineqs:{L:ℤ List| ||L|| = (n + 1) ∈ ℤ} List]. (omega_start(eqs;ineqs) ∈ IntConstraints)
Lemma: unsat-omega_start
∀n:ℕ. ∀eqs,ineqs:{L:ℤ List| ||L|| = (n + 1) ∈ ℤ} List. (unsat(omega_start(eqs;ineqs)) ⇒ (¬satisfiable(eqs;ineqs)))
Definition: omega
omega works on an "integer problem" that is a set of equality constraints
and a set of inequality constraints. It start by normalizing the constraints.
Then it repeats the "omega_step". On each step, either the number of
equality constraints decreases, or the dimension of the problem (the number
of variables) decreases. Thus the algorithm terminates.
Each step preserves satisfiablity of the constraints, meaning that if
the resulting problem is unsatisfiable then the original problem is
unsatisfiable. Because we have not implemented Bill Pugh's "dark shadow"
test, the reverse is not true in general (the reduced problem could be
satisfiable even though the original problem was unsatisfiable).⋅
omega(eqs;ineqs) == let s ⟵ omega_start(eqs;ineqs) in rep_int_constraint_step(λp.omega_step(p);s)
Lemma: omega_wf
∀[n:ℕ]. ∀[eqs,ineqs:{L:ℤ List| ||L|| = (n + 1) ∈ ℤ} List]. (omega(eqs;ineqs) ∈ {p:IntConstraints| dim(p) = 0 ∈ ℤ} )
Lemma: isr-omega
∀[n:ℕ]. ∀[eqs,ineqs:{L:ℤ List| ||L|| = (n + 1) ∈ ℤ} List]. ¬satisfiable(eqs;ineqs) supposing ↑isr(omega(eqs;ineqs))
Definition: full-omega
full-omega works on "integer formulas". It first puts the formula
into a disjunctive-normal-form where each disjunct is a collection
of "polynomial constraints" (a polynomial in the "atoms" of the formula
which is either =0 or >= 0).
Each set of polynomial constraints is "linearized" to a (linear)
"integer problem", a set of linear forms =0 or >= 0.
omega is run on each of these problems, and if all the results are ff
then the formula is unsatisfiable. If any of the results are tt
then the formlua might be satisfiable, but is not guaranteed to be.
That is because we have not implemented Bill Pugh's "dark shadow" test.
However, for theorem proving, a "semi decision" that can guarantees that
a formula is unsatisfiable seems to be good enough.⋅
full-omega(fmla) ==
eval dnf = evalall(int_formula_dnf(fmla)) in
eager-accum(sat,pc.sat
∨blet eqs,ineqs = pcs-to-integer-problem(pc)
in case omega(eqs;ineqs) of inl(x) => tt | inr(_) => ff;ff;dnf)
Lemma: full-omega_wf
∀[fmla:int_formula()]. (full-omega(fmla) ∈ {b:𝔹| b = ff ⇒ (¬satisfiable_int_formula(fmla))} )
Lemma: satisfiable-full-omega-tt
∀[fmla:int_formula()]. ↑isl(full-omega(fmla)) supposing satisfiable_int_formula(fmla)
Lemma: full-omega-unsat
∀[fmla:int_formula()]. ¬satisfiable_int_formula(fmla) supposing inr Ax ≤ full-omega(fmla)
Lemma: test-omega
∀x,y,z:ℤ. ((1 ≤ ((2 * x) + (2 * y))) ⇒ ((2 * x) ≤ ((2 * y) + 1)) ⇒ (2 ≤ (3 * y)))
Lemma: test-omega2
∀p0,p1,q0,q1,r0,r1,t0,t1:ℤ.
((((p0 * q1) + (q0 * r1) + (r0 * p1)) - (p1 * q0) + (q1 * r0) + (r1 * p0))
= ((((t0 * q1) + (q0 * r1) + (r0 * t1)) - (t1 * q0) + (q1 * r0) + (r1 * t0))
+ (((p0 * t1) + (t0 * r1) + (r0 * p1)) - (p1 * t0) + (t1 * r0) + (r1 * p0))
+ (((p0 * q1) + (q0 * t1) + (t0 * p1)) - (p1 * q0) + (q1 * t0) + (t1 * p0)))
∈ ℤ)
Lemma: test-omega-auto-split
∀n:ℤ. (if 2 <z n then if 1 <z n then 1 else 2 fi if n ≤z 3 then 3 else 4 fi ~ if 2 <z n then 1 else 3 fi )
Definition: ml-int-vec-mul
ml-int-vec-mul(a;as) == ml-map(λx.(a * x);as)
Lemma: ml-int-vec-mul_wf
∀[a:ℤ]. ∀[as:ℤ List]. (ml-int-vec-mul(a;as) ∈ ℤ List)
Lemma: ml-int-vec-mul-sq
∀[a:ℤ]. ∀[as:ℤ List]. (ml-int-vec-mul(a;as) ~ a * as)
Definition: ml-int-vec-add
ml-int-vec-add(as;bs) ==
fix((λivadd,as,bs. if null(as) ∨bnull(bs)
then []
else let a.as2 = as
in let b.bs2 = bs
in [a + b / ivadd(as2)(bs2)]
fi ))(as)(bs)
Lemma: ml-int-vec-add-sq
∀[as,bs:ℤ List]. (ml-int-vec-add(as;bs) ~ as + bs)
Lemma: ml-int-vec-add_wf
∀[as,bs:ℤ List]. (ml-int-vec-add(as;bs) ∈ ℤ List)
Definition: ml-list-delete
ml-list-delete(as;i) ==
fix((λlistdel,as,i. if null(as)
then []
else let a.more = as
in if i <z 1 then more else [a / listdel(more)(i - 1)] fi
fi ))(as)(i)
Lemma: ml-list-delete-sq
∀[T:Type]. ∀[L:T List]. ∀[i:ℤ]. (ml-list-delete(L;i) ~ L\i) supposing valueall-type(T)
Lemma: ml-list-delete_wf
∀[T:Type]. ∀[L:T List]. ∀[i:ℤ]. (ml-list-delete(L;i) ∈ T List) supposing valueall-type(T)
Definition: ml-accum-abort
ml-accum-abort(f;sofar;L) ==
fix((λacca,f,sofar,L. if null(L) ∨bisr(sofar) then sofar else let x.y = L in acca(f)(f(x)(outl(sofar)))(y) fi ))(f)(so\000Cfar)(L)
Lemma: ml-accum-abort-sq
∀[A,B:Type]. ∀[F:A ⟶ B ⟶ (B?)].
∀[L:A List]. ∀[s:B?]. (ml-accum-abort(F;s;L) ~ accumulate_abort(x,sofar.F x sofar;s;L))
supposing valueall-type(A) ∧ valueall-type(B) ∧ A ∧ B
Lemma: ml-accum-abort_wf
∀[A,B:Type]. ∀[s:B?]. ∀[F:A ⟶ B ⟶ (B?)]. ∀[L:A List].
ml-accum-abort(F;s;L) ∈ B? supposing valueall-type(A) ∧ valueall-type(B) ∧ A ∧ B
Definition: ml-gcd-reduce-eq-constraints
ml-gcd-reduce-eq-constraints(sat;LL) ==
ml-accum-abort(λL,Ls. let h.t = L
in if null(t)
then if (h =z 0) then inl [L / Ls] else inr ⋅ fi
else let g = ml-absval(ml-gcd-list(t)) in
if 1 <z g
then if (h rem g =z 0) then inl [ml-map(λx.(x ÷ g);L) / Ls] else inr ⋅ fi
else inl [L / Ls]
fi
fi ;inl sat;LL)
Definition: ml-shadow-vec
ml-shadow-vec(i;as;bs) ==
ml-list-delete(ml-int-vec-add(ml-int-vec-mul(ml-select(i;as);bs);ml-int-vec-mul(-ml-select(i;bs);as));i)
Home
Index