зеркало из https://github.com/microsoft/ivy.git
144 строки
2.6 KiB
XML
144 строки
2.6 KiB
XML
#lang ivy1.6
|
|
|
|
type t
|
|
type r
|
|
type s
|
|
|
|
axiom (T:t < U & U < V) -> (T < V)
|
|
axiom ~(T:t < U & U < T)
|
|
axiom T:t < U | T = U | U < T
|
|
|
|
relation succ(X:t,Y:t)
|
|
|
|
|
|
# schema rec[t] = {
|
|
# type q
|
|
# function base(X:t) : q
|
|
# function step(X:q,Y:t) : q
|
|
# function fun(X:t) : q
|
|
# #---------------------------------------------------------
|
|
# definition fun(X:t) = base(X) if X <= 0 else step(fun(X-1),X)
|
|
# }
|
|
|
|
# schema lep[t] = {
|
|
# function p(X:t) : bool
|
|
# #---------------------------------------------------------
|
|
# property exists L. (L >= 0 & forall B. (B >= 0 & p(B)-> p(L) & L <= B))
|
|
# }
|
|
|
|
relation member(X:t,S:s)
|
|
|
|
function cnt(X:t):r
|
|
function card(S:s) : r
|
|
function cardUpTo(S:s,B:t) : r
|
|
individual n : t
|
|
axiom n > 0
|
|
|
|
isolate successor = {
|
|
|
|
object spec = {
|
|
|
|
property succ(X,Y) -> X < Y
|
|
property ~(X < Y & Y < Z & succ(X,Z))
|
|
|
|
}
|
|
|
|
object impl = {
|
|
interpret t -> int
|
|
}
|
|
|
|
}
|
|
with counting.impl.succ_def
|
|
|
|
isolate counting = {
|
|
|
|
object spec = {
|
|
|
|
property [cnt_base] cnt(0) = 0
|
|
property [cnt_step] F > 0 & succ(E,F) -> cnt(F) = cnt(E) + 1
|
|
|
|
property [cardUpTo_base] cardUpTo(S,0) = 0
|
|
property [cardUpTo_step] succ(B,BS) & BS > 0 ->
|
|
cardUpTo(S,BS) = cardUpTo(S,B)+1 if member(B,S) else cardUpTo(S,B)
|
|
}
|
|
|
|
object impl = {
|
|
|
|
definition cnt(X) = 0 if X <= 0 else cnt(X-1) + 1
|
|
proof rec[t]
|
|
|
|
definition cardUpTo(S,B) =
|
|
0 if B <= 0 else (cardUpTo(S,B-1)+1 if member(B-1,S) else cardUpTo(S,B-1))
|
|
proof rec[t]
|
|
|
|
object succ_def = {
|
|
definition succ(X:t,Y:t) = (Y-1 = X)
|
|
}
|
|
|
|
}
|
|
}
|
|
|
|
|
|
isolate disjointness = {
|
|
|
|
object spec = {
|
|
|
|
relation disjoint(X:s,Y:s)
|
|
|
|
definition disjoint(X,Y) = forall E. ~(member(E,X) & member(E,Y))
|
|
|
|
derived inv(X,Y,B) =
|
|
disjoint(X,Y) -> cardUpTo(X,B) + cardUpTo(Y,B) <= cnt(B)
|
|
|
|
property exists L. (L >= 0 & forall B. (B >= 0 & ~inv(X,Y,B) -> ~inv(X,Y,L) & L <= B))
|
|
named lerr(X,Y)
|
|
proof lep[t]
|
|
|
|
object succ_lemma = {
|
|
object spec = {
|
|
property [induc] exists E. succ(E,lerr(X,Y))
|
|
}
|
|
isolate iso = spec with counting.impl.succ_def
|
|
}
|
|
|
|
definition card(S) = cardUpTo(S,n)
|
|
|
|
property disjoint(X,Y) -> card(X) + card(Y) <= cnt(n)
|
|
|
|
interpret r->int
|
|
}
|
|
|
|
}
|
|
with counting,successor
|
|
|
|
|
|
# fun(X) = bif(X)
|
|
# base(X) = 0
|
|
# step(fun(X-1)) = bif(X-1) + 1
|
|
|
|
|
|
# step(bif(X-1)) -> bif(X-1) + 1
|
|
|
|
# discharge[(Y1,bif(X-1))](bif(X-1) + 1) = Y1 + 1
|
|
|
|
# step |-> lambda Y1.Y1 + 1
|
|
|
|
# base(X) if X <= 0 else step(fun(X-1))
|
|
# --> 0 if X <= 0 else bif(X-1) + 1
|
|
|
|
# base(X) -> 0
|
|
|
|
# discharge[(Y1,X)](0) = 0
|
|
# {base |-> labmda Y1. 0}
|
|
|
|
# X <= 0 -> X <= 0
|
|
|
|
# {}
|
|
|
|
|
|
# f 3 --> 3 + 3
|
|
|
|
# discharge[(Y1,3)](3+3) = Y1 + Y1
|
|
# {f |-> lambda Y1. Y1 + Y1}
|
|
|