diff --git a/modules/FiniteSetsExt.tla b/modules/FiniteSetsExt.tla index 795bfe9..1b077f7 100644 --- a/modules/FiniteSetsExt.tla +++ b/modules/FiniteSetsExt.tla @@ -1,7 +1,7 @@ --------------------------- MODULE FiniteSetsExt --------------------------- -EXTENDS Folds, Functions \* Replace with LOCAL INSTANCE when https://github.com/tlaplus/tlapm/issues/119 is resolved. -LOCAL INSTANCE Integers -LOCAL INSTANCE FiniteSets +EXTENDS Integers, FiniteSets, Folds, Functions \* Replace with LOCAL INSTANCE when https://github.com/tlaplus/tlapm/issues/119 is resolved. +\* LOCAL INSTANCE Integers +\* LOCAL INSTANCE FiniteSets (*************************************************************************) (* Fold op over the elements of set using base as starting value. *) diff --git a/modules/FiniteSetsExtTheorems.tla b/modules/FiniteSetsExtTheorems.tla index 38e91db..7c07b29 100644 --- a/modules/FiniteSetsExtTheorems.tla +++ b/modules/FiniteSetsExtTheorems.tla @@ -283,4 +283,79 @@ THEOREM MapThenSumSetStrictlyMonotonic == NEW s \in S, f(s) < g(s) PROVE MapThenSumSet(f, S) < MapThenSumSet(g, S) +--------------------------------------------------------------------------- + +(*************************************************************************) +(* Theorems about Min and Max of sets of integers. *) +(*************************************************************************) + +(*************************************************************************) +(* If a set of integers contains an upper bound, it is the maximum. *) +(*************************************************************************) +THEOREM MaxInt == + ASSUME NEW S \in SUBSET Int, NEW x \in S, \A y \in S : x >= y + PROVE Max(S) = x + +(*************************************************************************) +(* Any finite non-empty set of integers has a maximum. *) +(*************************************************************************) +THEOREM MaxIntFinite == + ASSUME NEW S \in SUBSET Int, S # {}, IsFiniteSet(S) + PROVE /\ Max(S) \in S + /\ \A y \in S : Max(S) >= y + +(*************************************************************************) +(* Any non-empty set of integers that has an upper bound has a maximum. *) +(*************************************************************************) +THEOREM MaxIntBounded == + ASSUME NEW S \in SUBSET Int, S # {}, NEW x \in Int, \A y \in S : x >= y + PROVE /\ Max(S) \in S + /\ \A y \in S : Max(S) >= y + +(*************************************************************************) +(* The maximum of a non-empty interval is its upper bound. *) +(*************************************************************************) +THEOREM MaxInterval == + ASSUME NEW a \in Int, NEW b \in Int, a <= b + PROVE Max(a..b) = b + +(*************************************************************************) +(* If a set of integers contains an lower bound, it is the minimum. *) +(*************************************************************************) +THEOREM MinInt == + ASSUME NEW S \in SUBSET Int, NEW x \in S, \A y \in S : x <= y + PROVE Min(S) = x + +(*************************************************************************) +(* Any finite non-empty set of integers has a minimum. *) +(*************************************************************************) +THEOREM MinIntFinite == + ASSUME NEW S \in SUBSET Int, S # {}, IsFiniteSet(S) + PROVE /\ Min(S) \in S + /\ \A y \in S : Min(S) <= y + +(*************************************************************************) +(* Any non-empty set of integers that has a lower bound has a minimum. *) +(*************************************************************************) +THEOREM MinIntBounded == + ASSUME NEW S \in SUBSET Int, S # {}, NEW x \in Int, \A y \in S : x <= y + PROVE /\ Min(S) \in S + /\ \A y \in S : Min(S) <= y + +(*************************************************************************) +(* The minimum of a non-empty interval is its lower bound. *) +(*************************************************************************) +THEOREM MinInterval == + ASSUME NEW a \in Int, NEW b \in Int, a <= b + PROVE Min(a..b) = a + +(*************************************************************************) +(* Any non-empty set of natural numbers has a minimum. *) +(*************************************************************************) +THEOREM MinNat == + ASSUME NEW S \in SUBSET Nat, S # {} + PROVE /\ Min(S) \in S + /\ \A y \in S : Min(S) <= y + + =========================================================================== diff --git a/modules/FiniteSetsExtTheorems_proofs.tla b/modules/FiniteSetsExtTheorems_proofs.tla index e7b370e..2cfa0a9 100644 --- a/modules/FiniteSetsExtTheorems_proofs.tla +++ b/modules/FiniteSetsExtTheorems_proofs.tla @@ -493,4 +493,124 @@ THEOREM MapThenSumSetStrictlyMonotonic == BY <1>3, MapThenSumSetInt, Isa <1>. QED BY <1>1, <1>2, <1>4, <1>5 +(***************************************************************************) +(* Theorems about Max and Min. *) +(***************************************************************************) + +THEOREM MaxInt == + ASSUME NEW S \in SUBSET Int, NEW x \in S, \A y \in S : x >= y + PROVE Max(S) = x +BY DEF Max + +THEOREM MaxIntFinite == + ASSUME NEW S \in SUBSET Int, S # {}, IsFiniteSet(S) + PROVE /\ Max(S) \in S + /\ \A y \in S : Max(S) >= y +<1>. DEFINE P(T) == T # {} => /\ Max(T) \in T + /\ \A y \in T : Max(T) >= y +<1>1. P({}) + OBVIOUS +<1>2. ASSUME NEW T \in SUBSET S, P(T), NEW a \in S \ T + PROVE P(T \union {a}) + <2>1. CASE \A y \in T : a >= y + BY <1>1, <2>1 DEF Max + <2>2. CASE \E y \in T : ~(a >= y) + <3>. DEFINE m == Max(T) + <3>1. /\ m \in T \union {a} + /\ \A y \in T \union {a} : m >= y + BY <1>2, <2>2 + <3>. QED BY <3>1, Zenon DEF Max + <2>. QED BY <2>1, <2>2 +<1>3. P(S) + <2>. HIDE DEF P + <2>. QED BY <1>1, <1>2, FS_Induction, IsaM("blast") +<1>. QED BY <1>3 + +THEOREM MaxIntBounded == + ASSUME NEW S \in SUBSET Int, S # {}, NEW x \in Int, \A y \in S : x >= y + PROVE /\ Max(S) \in S + /\ \A y \in S : Max(S) >= y +<1>1. PICK s \in S : TRUE + OBVIOUS +<1>2. IsFiniteSet(s .. x) + BY FS_Interval +<1>. DEFINE T == (s .. x) \cap S +<1>3. /\ T \in SUBSET Int + /\ T # {} + /\ IsFiniteSet(T) + BY <1>2, FS_Subset +<1>4. /\ Max(T) \in T + /\ \A y \in T : Max(T) >= y + BY <1>3, MaxIntFinite +<1>5. /\ Max(T) \in S + /\ \A y \in S : Max(T) >= y + BY <1>4 +<1>. QED BY <1>5, Zenon DEF Max + +THEOREM MaxInterval == + ASSUME NEW a \in Int, NEW b \in Int, a <= b + PROVE Max(a..b) = b +BY DEF Max + +THEOREM MinInt == + ASSUME NEW S \in SUBSET Int, NEW x \in S, \A y \in S : x <= y + PROVE Min(S) = x +BY DEF Min + +THEOREM MinIntFinite == + ASSUME NEW S \in SUBSET Int, S # {}, IsFiniteSet(S) + PROVE /\ Min(S) \in S + /\ \A y \in S : Min(S) <= y +<1>. DEFINE P(T) == T # {} => /\ Min(T) \in T + /\ \A y \in T : Min(T) <= y +<1>1. P({}) + OBVIOUS +<1>2. ASSUME NEW T \in SUBSET S, P(T), NEW a \in S \ T + PROVE P(T \union {a}) + <2>1. CASE \A y \in T : a <= y + BY <1>1, <2>1 DEF Min + <2>2. CASE \E y \in T : ~(a <= y) + <3>. DEFINE m == Min(T) + <3>1. /\ m \in T \union {a} + /\ \A y \in T \union {a} : m <= y + BY <1>2, <2>2 + <3>. QED BY <3>1, Zenon DEF Min + <2>. QED BY <2>1, <2>2 +<1>3. P(S) + <2>. HIDE DEF P + <2>. QED BY <1>1, <1>2, FS_Induction, IsaM("blast") +<1>. QED BY <1>3 + +THEOREM MinIntBounded == + ASSUME NEW S \in SUBSET Int, S # {}, NEW x \in Int, \A y \in S : x <= y + PROVE /\ Min(S) \in S + /\ \A y \in S : Min(S) <= y +<1>1. PICK s \in S : TRUE + OBVIOUS +<1>2. IsFiniteSet(x .. s) + BY FS_Interval +<1>. DEFINE T == (x .. s) \cap S +<1>3. /\ T \in SUBSET Int + /\ T # {} + /\ IsFiniteSet(T) + BY <1>2, FS_Subset +<1>4. /\ Min(T) \in T + /\ \A y \in T : Min(T) <= y + BY <1>3, MinIntFinite +<1>5. /\ Min(T) \in S + /\ \A y \in S : Min(T) <= y + BY <1>4 +<1>. QED BY <1>5, Zenon DEF Min + +THEOREM MinInterval == + ASSUME NEW a \in Int, NEW b \in Int, a <= b + PROVE Min(a..b) = a +BY DEF Min + +THEOREM MinNat == + ASSUME NEW S \in SUBSET Nat, S # {} + PROVE /\ Min(S) \in S + /\ \A y \in S : Min(S) <= y +BY MinIntBounded, \A y \in S : 0 <= y + ================================================================================ diff --git a/modules/FoldsTheorems.tla b/modules/FoldsTheorems.tla index afc1a9e..a51f79c 100644 --- a/modules/FoldsTheorems.tla +++ b/modules/FoldsTheorems.tla @@ -36,6 +36,37 @@ THEOREM MapThenFoldSetNonempty == LET x == choose(S) IN op(f(x), MapThenFoldSet(op, base, f, choose, S \ {x})) +(*************************************************************************) +(* Folding over two finite sets S and T that are related by a bijection *) +(* that is compatible with the choice and mapping functions yields the *) +(* same result. *) +(*************************************************************************) +THEOREM MapThenFoldSetBijection == + ASSUME NEW op(_,_), NEW base, + NEW S, IsFiniteSet(S), NEW fS(_), NEW chS(_), + \A U \in SUBSET S : U # {} => chS(U) \in U, + NEW T, IsFiniteSet(T), NEW fT(_), NEW chT(_), + \A U \in SUBSET T : U # {} => chT(U) \in U, + NEW bij(_), + \A s \in S : bij(s) \in T, + \A t \in T : \E s \in S : bij(s) = t, + \A s1, s2 \in S : bij(s1) = bij(s2) => s1 = s2, + \A s \in S : fS(s) = fT(bij(s)), + \A U \in SUBSET S : U # {} => bij(chS(U)) = chT({bij(s) : s \in U}) + PROVE MapThenFoldSet(op, base, fS, chS, S) = MapThenFoldSet(op, base, fT, chT, T) + +(*************************************************************************) +(* In particular, folding over the same set, using two mapping functions *) +(* that agree over the elements of the set, yields the same result. *) +(*************************************************************************) +THEOREM MapThenFoldSetEqual == + ASSUME NEW op(_,_), NEW base, NEW choose(_), NEW S, IsFiniteSet(S), + \A T \in SUBSET S : T # {} => choose(T) \in T, + NEW f(_), NEW g(_), + \A s \in S : f(s) = g(s) + PROVE MapThenFoldSet(op, base, f, choose, S) = + MapThenFoldSet(op, base, g, choose, S) + (*************************************************************************) (* The type of a fold corresponds to the type associated with the binary *) (* operator that underlies the fold. *) diff --git a/modules/FoldsTheorems_proofs.tla b/modules/FoldsTheorems_proofs.tla index 274557f..68cca64 100644 --- a/modules/FoldsTheorems_proofs.tla +++ b/modules/FoldsTheorems_proofs.tla @@ -4,6 +4,7 @@ (*************************************************************************) EXTENDS Folds, FiniteSets, TLAPS LOCAL INSTANCE FiniteSetTheorems +LOCAL INSTANCE FunctionTheorems LOCAL INSTANCE WellFoundedInduction \* MapThenFoldSet is well-defined @@ -95,6 +96,82 @@ THEOREM MapThenFoldSetNonempty == IN op(f(x), MapThenFoldSet(op, base, f, choose, S \ {x})) BY MapThenFoldSetDef, Isa +\* equality of MapThenFoldSet for a bijection that behaves homomorphically +THEOREM MapThenFoldSetBijection == + ASSUME NEW op(_,_), NEW base, + NEW S, IsFiniteSet(S), NEW fS(_), NEW chS(_), + \A U \in SUBSET S : U # {} => chS(U) \in U, + NEW T, IsFiniteSet(T), NEW fT(_), NEW chT(_), + \A U \in SUBSET T : U # {} => chT(U) \in U, + NEW bij(_), + \A s \in S : bij(s) \in T, + \A t \in T : \E s \in S : bij(s) = t, + \A s1, s2 \in S : bij(s1) = bij(s2) => s1 = s2, + \A s \in S : fS(s) = fT(bij(s)), + \A U \in SUBSET S : U # {} => bij(chS(U)) = chT({bij(s) : s \in U}) + PROVE MapThenFoldSet(op, base, fS, chS, S) = MapThenFoldSet(op, base, fT, chT, T) +<1>. DEFINE P(U) == MapThenFoldSet(op, base, fS, chS, U) = + MapThenFoldSet(op, base, fT, chT, {bij(s) : s \in U}) +<1>1. ASSUME NEW U \in SUBSET S, \A V \in (SUBSET U) \ {U} : P(V) + PROVE P(U) + <2>1. CASE U = {} + BY <2>1, MapThenFoldSetEmpty, Isa + <2>2. CASE U # {} + <3>. DEFINE BU == {bij(s) : s \in U} + xS == chS(U) xT == chT(BU) + VS == U \ {xS} VT == BU \ {xT} + <3>. SUFFICES MapThenFoldSet(op, base, fS, chS, U) = + MapThenFoldSet(op, base, fT, chT, BU) + OBVIOUS + <3>1. /\ IsFiniteSet(U) + /\ \A V \in SUBSET U : V # {} => chS(V) \in V + BY <2>2, FS_Subset + <3>2. MapThenFoldSet(op, base, fS, chS, U) = + op(fS(xS), MapThenFoldSet(op, base, fS, chS, VS)) + BY <2>2, <3>1, MapThenFoldSetNonempty, Isa + <3>3. IsFiniteSet(BU) + BY <3>1, FS_Image, Isa + <3>4. /\ BU # {} + /\ \A V \in SUBSET BU : V # {} => chT(V) \in V + BY <2>2 + <3>5. MapThenFoldSet(op, base, fT, chT, BU) = + op(fT(xT), MapThenFoldSet(op, base, fT, chT, VT)) + <4>. HIDE DEF BU + <4>. QED BY <3>3, <3>4, MapThenFoldSetNonempty, Isa + <3>6. /\ xS \in U + /\ xT = bij(xS) + /\ fS(xS) = fT(xT) + /\ VT = {bij(s) : s \in VS} + BY <2>2, <3>1 + <3>7. P(VS) + BY <1>1, <3>6 + <3>. HIDE DEF BU, xS, xT, VS, VT + <3>. QED BY <3>2, <3>5, <3>6, <3>7 + <2>. QED BY <2>1, <2>2 +<1>2. P(S) + BY <1>1, FS_WFInduction, IsaM("iprover") +<1>3. {bij(s) : s \in S} = T + OBVIOUS +<1>. QED BY <1>2, <1>3 + +\* special case when the bijection is the identity +THEOREM MapThenFoldSetEqual == + ASSUME NEW op(_,_), NEW base, NEW choose(_), NEW S, IsFiniteSet(S), + \A T \in SUBSET S : T # {} => choose(T) \in T, + NEW f(_), NEW g(_), + \A s \in S : f(s) = g(s) + PROVE MapThenFoldSet(op, base, f, choose, S) = + MapThenFoldSet(op, base, g, choose, S) +<1>. DEFINE id(s) == s +<1>1. /\ \A s \in S : id(s) \in S + /\ \A t \in S : \E s \in S : id(s) = t + /\ \A s1, s2 \in S : id(s1) = id(s2) => s1 = s2 + /\ \A s \in S : f(s) = g(id(s)) + /\ \A U \in SUBSET S : U # {} => id(choose(U)) = choose({id(s) : s \in U}) + BY Zenon +<1>. HIDE DEF id +<1>. QED BY <1>1, MapThenFoldSetBijection, IsaM("iprover") + \* type of a fold THEOREM MapThenFoldSetType == ASSUME NEW S, IsFiniteSet(S), diff --git a/modules/FunctionTheorems.tla b/modules/FunctionTheorems.tla new file mode 100644 index 0000000..b75e408 --- /dev/null +++ b/modules/FunctionTheorems.tla @@ -0,0 +1,844 @@ +------------------------ MODULE FunctionTheorems ---------------------------- +(***************************************************************************) +(* `^{\large \vspace{12pt} *) +(* Proofs of facts about functions. *) +(* Originally contributed by Tom Rodeheffer, MSR. *) +(* \vspace{12pt}}^' *) +(***************************************************************************) + +EXTENDS Functions, Integers, FiniteSets + +(***************************************************************************) +(* `. .' *) +(* *) +(* Function restriction. *) +(* *) +(* `. .' *) +(***************************************************************************) +THEOREM Fun_RestrictProperties == + ASSUME NEW S, NEW T, NEW f \in [S -> T], NEW A \in SUBSET S + PROVE /\ Restrict(f,A) \in [A -> T] + /\ \A x \in A : Restrict(f,A)[x] = f[x] + +(***************************************************************************) +(* `. .' *) +(* *) +(* Range of a function. *) +(* *) +(* `. .' *) +(***************************************************************************) +THEOREM Fun_RangeProperties == + ASSUME NEW S, NEW T, NEW f \in [S -> T] + PROVE /\ Range(f) \subseteq T + /\ \A y \in Range(f) : \E x \in S : f[x] = y + /\ f \in Surjection(S, Range(f)) + + +(***************************************************************************) +(* `. .' *) +(* *) +(* Inverse of a function. *) +(* *) +(* `. .' *) +(***************************************************************************) +THEOREM Fun_InverseProperties == + ASSUME NEW S, NEW T, NEW f \in [S -> T] + PROVE /\ (S = {} => T = {}) => Inverse(f,S,T) \in [T -> S] + /\ \A y \in Range(f) : f[Inverse(f,S,T)[y]] = y + + +(***************************************************************************) +(* `. .' *) +(* *) +(* Introduction rules for injections, surjections, bijections. *) +(* *) +(* `. .' *) +(***************************************************************************) +THEOREM Fun_IsInj == + ASSUME NEW S, NEW T, NEW F \in [S -> T], + \A a,b \in S : F[a] = F[b] => a = b + PROVE F \in Injection(S,T) + +THEOREM Fun_IsSurj == + ASSUME NEW S, NEW T, NEW F \in [S -> T], + \A t \in T : \E s \in S : F[s] = t + PROVE F \in Surjection(S,T) + +THEOREM Fun_IsBij == + ASSUME NEW S, NEW T, NEW F, + \/ F \in Injection(S,T) + \/ (F \in [S -> T] /\ \A a,b \in S : F[a] = F[b] => a = b), + + \/ F \in Surjection(S,T) + \/ (F \in [S -> T] /\ \A t \in T : \E s \in S : F[s] = t) + PROVE F \in Bijection(S,T) + + + +(***************************************************************************) +(* `. .' *) +(* *) +(* Properties of injections, surjections, and bijections. *) +(* *) +(* `. .' *) +(***************************************************************************) +THEOREM Fun_InjectionProperties == + ASSUME NEW S, NEW T, NEW F \in Injection(S,T) + PROVE /\ F \in [S -> T] + /\ \A a,b \in S : F[a] = F[b] => a = b + +THEOREM Fun_SurjectionProperties == + ASSUME NEW S, NEW T, NEW F \in Surjection(S,T) + PROVE /\ F \in [S -> T] + /\ \A t \in T : \E s \in S : F[s] = t + /\ Range(F) = T + +THEOREM Fun_BijectionProperties == + ASSUME NEW S, NEW T, NEW F \in Bijection(S,T) + PROVE /\ F \in [S -> T] + /\ F \in Injection(S,T) + /\ F \in Surjection(S,T) + /\ \A a,b \in S : F[a] = F[b] => a = b + /\ \A t \in T : \E s \in S : F[s] = t + + +(***************************************************************************) +(* `. .' *) +(* *) +(* A surjection in [S -> T] such that there is no surjection from any *) +(* subset of S to T is a bijection. *) +(* *) +(* `. .' *) +(***************************************************************************) +THEOREM Fun_SmallestSurjectionIsBijection == + ASSUME NEW S, NEW T, NEW f \in Surjection(S,T), + \A U \in SUBSET S : U # S => Surjection(U,T) = {} + PROVE f \in Bijection(S,T) + + +(***************************************************************************) +(* `. .' *) +(* *) +(* Transitivity of injections, surjections, bijections. *) +(* *) +(* `. .' *) +(***************************************************************************) +THEOREM Fun_InjTransitive == + ASSUME NEW S, NEW T, NEW U, + NEW F \in Injection(S,T), + NEW G \in Injection(T,U) + PROVE [s \in S |-> G[F[s]]] \in Injection(S,U) + +THEOREM Fun_SurjTransitive == + ASSUME NEW S, NEW T, NEW U, + NEW F \in Surjection(S,T), + NEW G \in Surjection(T,U) + PROVE [s \in S |-> G[F[s]]] \in Surjection(S,U) + +THEOREM Fun_BijTransitive == + ASSUME NEW S, NEW T, NEW U, + NEW F \in Bijection(S,T), + NEW G \in Bijection(T,U) + PROVE [s \in S |-> G[F[s]]] \in Bijection(S,U) + + +(***************************************************************************) +(* `. .' *) +(* *) +(* The inverse of a surjection is an injection and vice versa. *) +(* *) +(* `. .' *) +(***************************************************************************) +THEOREM Fun_SurjInverse == + ASSUME NEW S, NEW T, NEW f \in Surjection(S,T) + PROVE Inverse(f,S,T) \in Injection(T,S) + +THEOREM Fun_InjInverse == + ASSUME NEW S, NEW T, NEW f \in Injection(S,T), S = {} => T = {} + PROVE Inverse(f,S,T) \in Surjection(T,S) + + +(***************************************************************************) +(* `. .' *) +(* *) +(* Properties of the inverse of a bijection. *) +(* *) +(* `. .' *) +(***************************************************************************) +THEOREM Fun_BijInverse == + ASSUME NEW S, NEW T, NEW f \in Bijection(S,T) + PROVE /\ Inverse(f,S,T) \in Bijection(T,S) + /\ \A s \in S : Inverse(f,S,T)[f[s]] = s + /\ Inverse(Inverse(f,S,T), T,S) = f + +(***************************************************************************) +(* We cannot conclude that a function f is a bijection if its inverse is *) +(* a bijection, and the following is a counter-example. *) +(* *) +(* S = {1,2} T = {3,4} *) +(* f = [x \in S |-> 3] *) +(* *) +(* Then, Inverse(f,S,T) can very well be (3 :> 1) @@ (4 :> 2), which is a *) +(* bijection although f is not. *) +(***************************************************************************) + +(***************************************************************************) +(* `. .' *) +(* *) +(* The restriction of a bijection is a bijection. *) +(* *) +(* `. .' *) +(***************************************************************************) +THEOREM Fun_BijRestrict == + ASSUME NEW S, NEW T, NEW F \in Bijection(S,T), + NEW R \in SUBSET S + PROVE Restrict(F, R) \in Bijection(R, Range(Restrict(F, R))) + + +(***************************************************************************) +(* `. .' *) +(* *) +(* Given F an injection from S to T, then F is a bijection from S to F(S). *) +(* *) +(* `. .' *) +(***************************************************************************) +THEOREM Fun_InjMeansBijImage == + ASSUME NEW S, NEW T, NEW F \in Injection(S,T) + PROVE F \in Bijection(S, Range(F)) + + +----------------------------------------------------------------------------- +(***************************************************************************) +(* `^{\large \vspace{12pt} *) +(* Facts about exists jections. *) +(* \vspace{12pt}}^' *) +(***************************************************************************) + + + +(***************************************************************************) +(* `. .' *) +(* *) +(* Definitions restated as facts. *) +(* *) +(* `. .' *) +(***************************************************************************) +THEOREM Fun_ExistsInj == + \A S,T : ExistsInjection(S,T) <=> Injection(S,T) # {} + +THEOREM Fun_ExistsSurj == + \A S,T : ExistsSurjection(S,T) <=> Surjection(S,T) # {} + +THEOREM Fun_ExistsBij == + \A S,T : ExistsBijection(S,T) <=> Bijection(S,T) # {} + + +(***************************************************************************) +(* `. .' *) +(* *) +(* There is a surjection from any set S to any non-empty subset T of S. *) +(* (Note that there cannot be a surjection to {} except if S is empty.) *) +(* *) +(* `. .' *) +(***************************************************************************) +THEOREM Fun_ExistsSurjSubset == + ASSUME NEW S, NEW T \in SUBSET S, T # {} + PROVE ExistsSurjection(S,T) + + +(***************************************************************************) +(* `. .' *) +(* *) +(* If there is a surjection from S to T, then there is an injection from T *) +(* to S. *) +(* *) +(* `. .' *) +(***************************************************************************) +THEOREM Fun_ExistsSurjMeansExistsRevInj == + ASSUME NEW S, NEW T, ExistsSurjection(S,T) + PROVE ExistsInjection(T,S) + + +(***************************************************************************) +(* `. .' *) +(* *) +(* ExistsBijection is reflexive, symmetric, and transitive. *) +(* *) +(* `. .' *) +(***************************************************************************) +THEOREM Fun_ExistsBijReflexive == + ASSUME NEW S + PROVE ExistsBijection(S,S) + +THEOREM Fun_ExistsBijSymmetric == + ASSUME NEW S, NEW T, ExistsBijection(S,T) + PROVE ExistsBijection(T,S) + +THEOREM Fun_ExistsBijTransitive == + ASSUME NEW S, NEW T, NEW U, ExistsBijection(S,T), ExistsBijection(T,U) + PROVE ExistsBijection(S,U) + + +(***************************************************************************) +(* `. .' *) +(* *) +(* Existence of injections and surjections is reflexive and transitive. *) +(* *) +(* `. .' *) +(***************************************************************************) +THEOREM Fun_ExistsInjReflexive == + ASSUME NEW S + PROVE ExistsInjection(S,S) + +THEOREM Fun_ExistsSurjReflexive == + ASSUME NEW S + PROVE ExistsSurjection(S,S) + +THEOREM Fun_ExistsInjTransitive == + ASSUME NEW S, NEW T, NEW U, + ExistsInjection(S,T), ExistsInjection(T,U) + PROVE ExistsInjection(S,U) + +THEOREM Fun_ExistsSurjTransitive == + ASSUME NEW S, NEW T, NEW U, + ExistsSurjection(S,T), ExistsSurjection(T,U) + PROVE ExistsSurjection(S,U) + + +----------------------------------------------------------------------------- +(***************************************************************************) +(* `^{\large \vspace{12pt} *) +(* The Cantor-Bernstein-Schroeder theorem. *) +(* \vspace{12pt}}^' *) +(***************************************************************************) + + +(***************************************************************************) +(* `. .' *) +(* *) +(* If there exists an injection from S to T, where T is a subset of S, *) +(* then there exists a bijection from S to T. *) +(* *) +(* A lemma for the Cantor-Bernstein-Schroeder theorem. *) +(* *) +(* This proof is formalized from *) +(* `^\url{http://www.proofwiki.org/wiki/Cantor-Bernstein-Schroeder\_Theorem/Lemma}^' *) +(* retrieved April 29, 2013. *) +(* *) +(* `. .' *) +(***************************************************************************) +THEOREM Fun_CantorBernsteinSchroeder_Lemma == + ASSUME NEW S, NEW T, T \subseteq S, ExistsInjection(S,T) + PROVE ExistsBijection(S,T) + + +(***************************************************************************) +(* `. .' *) +(* *) +(* If an injection exists from S to T and an injection exists from T to S, *) +(* then there is a bijection from S to T. *) +(* *) +(* This is the Cantor-Bernstein-Schroeder theorem. *) +(* *) +(* This proof is formalized from *) +(* `^\url{http://www.proofwiki.org/wiki/Cantor-Bernstein-Schroeder_Theorem/Proof_5}^' *) +(* retrieved April 29, 2013. *) +(* *) +(* `. .' *) +(***************************************************************************) +THEOREM Fun_CantorBernsteinSchroeder == + ASSUME NEW S, NEW T, + ExistsInjection(S,T), ExistsInjection(T,S) + PROVE ExistsBijection(S,T) + + +(***************************************************************************) +(* `. .' *) +(* *) +(* Applications of the Cantor-Bernstein-Schroeder Theorem. *) +(* If there exists an injection f: A->B and a surjection g: A->B, then *) +(* there exists a bijection between A and B. *) +(* Also, if there are surjections between A and B, then there is a *) +(* bijection. *) +(* *) +(* `. .' *) +(***************************************************************************) + +THEOREM Fun_ExistInjAndSurjThenBij == + ASSUME NEW S, NEW T, + ExistsInjection(S,T), ExistsSurjection(S,T) + PROVE ExistsBijection(S,T) + +THEOREM Fun_ExistSurjAndSurjThenBij == + ASSUME NEW S, NEW T, + ExistsSurjection(S,T), ExistsSurjection(T,S) + PROVE ExistsBijection(S,T) + + +(***************************************************************************) +(* `. .' *) +(* *) +(* Equivalences for ExistsBijection. *) +(* *) +(* `. .' *) +(***************************************************************************) +THEOREM Fun_ExistsBijEquiv == + ASSUME NEW S, NEW T + PROVE /\ ExistsBijection(S,T) <=> ExistsBijection(T,S) + /\ ExistsBijection(S,T) <=> ExistsInjection(S,T) /\ ExistsInjection(T,S) + /\ ExistsBijection(S,T) <=> ExistsInjection(S,T) /\ ExistsSurjection(S,T) + /\ ExistsBijection(S,T) <=> ExistsInjection(T,S) /\ ExistsSurjection(T,S) + /\ ExistsBijection(S,T) <=> ExistsSurjection(S,T) /\ ExistsSurjection(T,S) + + +----------------------------------------------------------------------------- +(***************************************************************************) +(* `^{\large \vspace{12pt} *) +(* Facts about jections involving 1..n. *) +(* \vspace{12pt}}^' *) +(***************************************************************************) + + +(***************************************************************************) +(* `. .' *) +(* *) +(* There is a bijection from 1..b-a+1 to a..b for integers a,b with a <= b.*) +(* *) +(* `. .' *) +(***************************************************************************) +THEOREM Fun_ExistsBijInterval == + ASSUME NEW a \in Int, NEW b \in Int, a <= b + PROVE ExistsBijection(1 .. b-a+1, a .. b) + + +(***************************************************************************) +(* `. .' *) +(* *) +(* There is an injection from 1..n to 1..m iff n \leq m. *) +(* *) +(* `. .' *) +(***************************************************************************) +THEOREM Fun_NatInjLeq == + ASSUME NEW n \in Nat, NEW m \in Nat + PROVE ExistsInjection(1..n,1..m) <=> n \leq m + + +(***************************************************************************) +(* `. .' *) +(* *) +(* If a surjection from 1..n to S exists (for some n \in Nat) then a *) +(* bijection from 1..m to S exists (for some m \in Nat) and m \leq n. *) +(* *) +(* `. .' *) +(***************************************************************************) +THEOREM Fun_NatSurjImpliesNatBij == + ASSUME NEW S, NEW n \in Nat, ExistsSurjection(1..n,S) + PROVE \E m \in Nat : ExistsBijection(1..m,S) /\ m \leq n + + +(***************************************************************************) +(* Simple corollary. *) +(***************************************************************************) +THEOREM Fun_NatSurjEquivNatBij == + ASSUME NEW S + PROVE (\E n \in Nat : ExistsSurjection(1..n,S)) + <=> (\E m \in Nat : ExistsBijection(1..m,S)) + + +(***************************************************************************) +(* `. .' *) +(* *) +(* For any set S, given n, m \in Nat such that bijections exist from 1..n *) +(* to S and from 1..m to S, then it must be the case that n = m. *) +(* *) +(* `. .' *) +(***************************************************************************) +THEOREM Fun_NatBijSame == + ASSUME NEW S, + NEW n \in Nat, ExistsBijection(1..n,S), + NEW m \in Nat, ExistsBijection(1..m,S) + PROVE n = m + + +(***************************************************************************) +(* `. .' *) +(* *) +(* S is empty iff there exists a bijection from 1..0 to S. *) +(* *) +(* `. .' *) +(***************************************************************************) +THEOREM Fun_NatBijEmpty == + ASSUME NEW S + PROVE ExistsBijection(1..0,S) <=> S = {} + + +(***************************************************************************) +(* `. .' *) +(* *) +(* S is a singleton iff there exists a bijection from 1..1 to S. *) +(* *) +(* `. .' *) +(***************************************************************************) +THEOREM Fun_NatBijSingleton == + ASSUME NEW S + PROVE ExistsBijection(1..1,S) <=> \E s : S = {s} + + +(***************************************************************************) +(* `. .' *) +(* *) +(* If there exists a bijection from 1..m to S (for some m \in Nat), then *) +(* there exists a bijection from 1..n to T (for some n \in Nat), where T *) +(* is a subset of S. Furthermore n \leq m. *) +(* *) +(* `. .' *) +(***************************************************************************) +THEOREM Fun_NatBijSubset == + ASSUME NEW S, NEW m \in Nat, ExistsBijection(1..m,S), + NEW T \in SUBSET S + PROVE \E n \in Nat : ExistsBijection(1..n,T) /\ n \leq m + + +(***************************************************************************) +(* `. .' *) +(* *) +(* If there exists a bijection from 1..m to S (for some m \in Nat), then *) +(* there exists a bijection from 1..(m+1) to S \cup {x}, where x \notin S. *) +(* *) +(* *) +(* `. .' *) +(***************************************************************************) +THEOREM Fun_NatBijAddElem == + ASSUME NEW S, NEW m \in Nat, ExistsBijection(1..m,S), + NEW x, x \notin S + PROVE ExistsBijection(1..(m+1), S \cup {x}) + + +(***************************************************************************) +(* `. .' *) +(* *) +(* If there exists a bijection from 1..m to S (for some m \in Nat), then *) +(* there exists a bijection from 1..(m-1) to S \ {x}, where x \in S. *) +(* *) +(* *) +(* `. .' *) +(***************************************************************************) +THEOREM Fun_NatBijSubElem == + ASSUME NEW S, NEW m \in Nat, ExistsBijection(1..m,S), + NEW x, x \in S + PROVE ExistsBijection(1..(m-1), S \ {x}) + +----------------------------------------------------------------------------- + +(***************************************************************************) +(* Folding a function for an empty set of indices yields the base value. *) +(***************************************************************************) +THEOREM FoldFunctionOnSetEmpty == + ASSUME NEW op(_,_), NEW base, NEW fun + PROVE FoldFunctionOnSet(op, base, fun, {}) = base + +(***************************************************************************) +(* Folding a function for a non-empty set of indices corresponds to *) +(* applying the binary operator to f[i], for some i \in indices, and the *) +(* result of recursing for the set indices \ {i}. *) +(***************************************************************************) +THEOREM FoldFunctionOnSetNonempty == + ASSUME NEW op(_,_), NEW base, NEW fun, + NEW indices, indices # {}, IsFiniteSet(indices) + PROVE \E i \in indices : FoldFunctionOnSet(op, base, fun, indices) = + op(fun[i], FoldFunctionOnSet(op, base, fun, indices \ {i})) + +(***************************************************************************) +(* The type of folding a function corresponds to the type associated with *) +(* the binary operator that underlies the fold. *) +(***************************************************************************) +THEOREM FoldFunctionOnSetType == + ASSUME NEW Typ, NEW op(_,_), NEW base \in Typ, + \A t,u \in Typ : op(t,u) \in Typ, + NEW indices, IsFiniteSet(indices), NEW fun, + \A i \in indices : fun[i] \in Typ + PROVE FoldFunctionOnSet(op, base, fun, indices) \in Typ + +(***************************************************************************) +(* Folding two functions that agree on every element of the set of indices *) +(* yields the same value. *) +(***************************************************************************) +THEOREM FoldFunctionOnSetEqual == + ASSUME NEW op(_,_), NEW base, NEW f, NEW g, + NEW indices, IsFiniteSet(indices), + \A i \in indices : f[i] = g[i] + PROVE FoldFunctionOnSet(op, base, f, indices) = + FoldFunctionOnSet(op, base, g, indices) + +(***************************************************************************) +(* If the binary operator is associative and commutative, the result of *) +(* folding a function over a non-empty set corresponds to applying the *) +(* operator to an arbitrary element of the set and the result of folding *) +(* the function over the remainder of the set. *) +(***************************************************************************) +THEOREM FoldFunctionOnSetAC == + ASSUME NEW Typ, NEW op(_,_), NEW base \in Typ, + \A t,u \in Typ : op(t,u) \in Typ, + \A t,u \in Typ : op(t,u) = op(u,t), + \A t,u,v \in Typ : op(t, op(u,v)) = op(op(t,u),v), + NEW indices, IsFiniteSet(indices), NEW i \in indices, NEW fun, + \A j \in indices : fun[j] \in Typ + PROVE FoldFunctionOnSet(op, base, fun, indices) = + op(fun[i], FoldFunctionOnSet(op, base, fun, indices \ {i})) + +\* reformulation in terms of adding an index to the set +THEOREM FoldFunctionOnSetACAddIndex == + ASSUME NEW Typ, NEW op(_,_), NEW base \in Typ, + \A t,u \in Typ : op(t,u) \in Typ, + \A t,u \in Typ : op(t,u) = op(u,t), + \A t,u,v \in Typ : op(t, op(u,v)) = op(op(t,u),v), + NEW indices, IsFiniteSet(indices), NEW i, i \notin indices, + NEW fun, \A j \in indices \union {i} : fun[j] \in Typ + PROVE FoldFunctionOnSet(op, base, fun, indices \union {i}) = + op(fun[i], FoldFunctionOnSet(op, base, fun, indices)) + +(*************************************************************************) +(* For an AC operator, folding an EXCEPT construction can be reduced to *) +(* folding the original function. *) +(*************************************************************************) +THEOREM FoldFunctionOnSetACExcept == + ASSUME NEW Typ, NEW op(_,_), NEW base \in Typ, + \A t,u \in Typ : op(t,u) \in Typ, + \A t,u \in Typ : op(t,u) = op(u,t), + \A t,u,v \in Typ : op(t, op(u,v)) = op(op(t,u),v), + NEW fun, NEW i, NEW y \in Typ, + NEW indices \in SUBSET (DOMAIN fun), IsFiniteSet(indices), + \A j \in indices : fun[j] \in Typ + PROVE FoldFunctionOnSet(op, base, [fun EXCEPT ![i] = y], indices) = + IF i \in indices + THEN op(y, FoldFunctionOnSet(op, base, fun, indices \ {i})) + ELSE FoldFunctionOnSet(op, base, fun, indices) + +(*************************************************************************) +(* For an AC operator `op` for which `base` is the neutral element, *) +(* folding a function commutes with set union, for disjoint sets. *) +(*************************************************************************) +THEOREM FoldFunctionOnSetDisjointUnion == + ASSUME NEW Typ, NEW op(_,_), NEW base \in Typ, + \A t,u \in Typ : op(t,u) \in Typ, + \A t,u \in Typ : op(t,u) = op(u,t), + \A t,u,v \in Typ : op(t, op(u,v)) = op(op(t,u),v), + \A t \in Typ : op(base, t) = t, + NEW S, IsFiniteSet(S), NEW T, IsFiniteSet(T), S \cap T = {}, + NEW fun, \A i \in S \union T : fun[i] \in Typ + PROVE FoldFunctionOnSet(op, base, fun, S \union T) = + op(FoldFunctionOnSet(op, base, fun, S), FoldFunctionOnSet(op, base, fun, T)) + +(*************************************************************************) +(* Analogous theorems for FoldFunction. Note that the theorems about *) +(* adding an index and about disjoint union do not make sense here. *) +(*************************************************************************) +THEOREM FoldFunctionEmpty == + ASSUME NEW op(_,_), NEW base, NEW fun, DOMAIN fun = {} + PROVE FoldFunction(op, base, fun) = base + +THEOREM FoldFunctionNonempty == + ASSUME NEW op(_,_), NEW base, NEW fun, + DOMAIN fun # {}, IsFiniteSet(DOMAIN fun) + PROVE \E i \in DOMAIN fun : FoldFunction(op, base, fun) = + op(fun[i], FoldFunctionOnSet(op, base, fun, DOMAIN fun \ {i})) + +THEOREM FoldFunctionType == + ASSUME NEW Typ, NEW op(_,_), NEW base \in Typ, + \A t,u \in Typ : op(t,u) \in Typ, + NEW fun, IsFiniteSet(DOMAIN fun), + \A i \in DOMAIN fun : fun[i] \in Typ + PROVE FoldFunction(op, base, fun) \in Typ + +THEOREM FoldFunctionAC == + ASSUME NEW Typ, NEW op(_,_), NEW base \in Typ, + \A t,u \in Typ : op(t,u) \in Typ, + \A t,u \in Typ : op(t,u) = op(u,t), + \A t,u,v \in Typ : op(t, op(u,v)) = op(op(t,u),v), + NEW fun, IsFiniteSet(DOMAIN fun), NEW i \in DOMAIN fun, + \A j \in DOMAIN fun : fun[j] \in Typ + PROVE FoldFunction(op, base, fun) = + op(fun[i], FoldFunctionOnSet(op, base, fun, (DOMAIN fun) \ {i})) + +THEOREM FoldFunctionACExcept == + ASSUME NEW Typ, NEW op(_,_), NEW base \in Typ, + \A t,u \in Typ : op(t,u) \in Typ, + \A t,u \in Typ : op(t,u) = op(u,t), + \A t,u,v \in Typ : op(t, op(u,v)) = op(op(t,u),v), + NEW fun, NEW i, NEW y \in Typ, + IsFiniteSet(DOMAIN fun), + \A j \in DOMAIN fun : fun[j] \in Typ + PROVE FoldFunction(op, base, [fun EXCEPT ![i] = y]) = + IF i \in DOMAIN fun + THEN op(y, FoldFunctionOnSet(op, base, fun, (DOMAIN fun) \ {i})) + ELSE FoldFunction(op, base, fun) + +(*************************************************************************) +(* Summing a function that returns natural numbers, resp. integers, *) +(* yields a natural number, resp. an integer. *) +(*************************************************************************) +THEOREM SumFunctionOnSetNat == + ASSUME NEW fun, NEW indices, IsFiniteSet(indices), + \A i \in indices : fun[i] \in Nat + PROVE SumFunctionOnSet(fun, indices) \in Nat + +THEOREM SumFunctionOnSetInt == + ASSUME NEW fun, NEW indices, IsFiniteSet(indices), + \A i \in indices : fun[i] \in Int + PROVE SumFunctionOnSet(fun, indices) \in Int + +(*************************************************************************) +(* Summing two functions that agree on all relevant indices yields the *) +(* same result. *) +(*************************************************************************) +THEOREM SumFunctionOnSetEqual == + ASSUME NEW f, NEW g, NEW indices, IsFiniteSet(indices), + \A i \in indices : f[i] = g[i] + PROVE SumFunctionOnSet(f, indices) = SumFunctionOnSet(g, indices) + +(*************************************************************************) +(* Summing a function over the empty set is 0. *) +(*************************************************************************) +THEOREM SumFunctionOnSetEmpty == + ASSUME NEW fun + PROVE SumFunctionOnSet(fun, {}) = 0 + +(*************************************************************************) +(* Summing a function over a non-empty set corresponds to the sum of *) +(* element of the set and the sum of the function over the remainder. *) +(*************************************************************************) +THEOREM SumFunctionOnSetNonempty == + ASSUME NEW fun, NEW indices, IsFiniteSet(indices), NEW i \in indices, + \A j \in indices : fun[j] \in Int + PROVE SumFunctionOnSet(fun, indices) = + fun[i] + SumFunctionOnSet(fun, indices \ {i}) + +\* reformulation in terms of adding an index +THEOREM SumFunctionOnSetAddIndex == + ASSUME NEW fun, NEW indices, IsFiniteSet(indices), + NEW i, i \notin indices, + \A j \in indices \union {i} : fun[j] \in Int + PROVE SumFunctionOnSet(fun, indices \union {i}) = + fun[i] + SumFunctionOnSet(fun, indices) + +\* corresponding lemma for removing an index +THEOREM SumFunctionOnSetRemoveIndex == + ASSUME NEW fun, NEW indices, IsFiniteSet(indices), NEW i \in indices, + \A j \in indices : fun[j] \in Int + PROVE SumFunctionOnSet(fun, indices \ {i}) = + SumFunctionOnSet(fun, indices) - fun[i] + +(*************************************************************************) +(* Reduce the sum of an EXCEPT to the sum of the original function. *) +(*************************************************************************) +THEOREM SumFunctionOnSetExcept == + ASSUME NEW fun, NEW i, NEW y \in Int, + NEW indices \in SUBSET (DOMAIN fun), IsFiniteSet(indices), + \A j \in indices : fun[j] \in Int + PROVE SumFunctionOnSet([fun EXCEPT ![i] = y], indices) = + IF i \in indices + THEN SumFunctionOnSet(fun, indices) + y - fun[i] + ELSE SumFunctionOnSet(fun, indices) + +(*************************************************************************) +(* Summing a function distributes over disjoint union. *) +(*************************************************************************) +THEOREM SumFunctionOnSetDisjointUnion == + ASSUME NEW S, IsFiniteSet(S), + NEW T, IsFiniteSet(T), S \cap T = {}, + NEW fun, \A x \in S \union T : fun[x] \in Int + PROVE SumFunctionOnSet(fun, S \union T) = + SumFunctionOnSet(fun, S) + SumFunctionOnSet(fun, T) + +(*************************************************************************) +(* Summing a Nat-valued function is monotonic in the subset relation. *) +(*************************************************************************) +THEOREM SumFunctionNatOnSubset == + ASSUME NEW S, IsFiniteSet(S), NEW T \in SUBSET S, + NEW fun, \A s \in S : fun[s] \in Nat + PROVE SumFunctionOnSet(fun, T) <= SumFunctionOnSet(fun, S) + +(*************************************************************************) +(* The sum of a Nat-valued function is zero iff all relevant function *) +(* values are zero. *) +(*************************************************************************) +THEOREM SumFunctionOnSetZero == + ASSUME NEW S, IsFiniteSet(S), + NEW fun, \A x \in S : fun[x] \in Nat + PROVE SumFunctionOnSet(fun, S) = 0 <=> \A x \in S : fun[x] = 0 + +(*************************************************************************) +(* Summing a function is monotonic in the function argument. *) +(*************************************************************************) +THEOREM SumFunctionOnSetMonotonic == + ASSUME NEW S, IsFiniteSet(S), + NEW f, \A s \in S : f[s] \in Int, + NEW g, \A s \in S : g[s] \in Int, + \A s \in S : f[s] <= g[s] + PROVE SumFunctionOnSet(f, S) <= SumFunctionOnSet(g, S) + +(*************************************************************************) +(* The sum over function f is strictly smaller than the sum over g if *) +(* f[x] <= g[x] for all x \in S and f[x] < g[s] holds for at least some *) +(* element s \in S. *) +(*************************************************************************) +THEOREM SumFunctionOnSetStrictlyMonotonic == + ASSUME NEW S, IsFiniteSet(S), + NEW f, \A s \in S : f[s] \in Int, + NEW g, \A s \in S : g[s] \in Int, + \A x \in S : f[x] <= g[x], + NEW s \in S, f[s] < g[s] + PROVE SumFunctionOnSet(f, S) < SumFunctionOnSet(g, S) + +(*************************************************************************) +(* Similar theorems for SumFunction. *) +(*************************************************************************) +THEOREM SumFunctionNat == + ASSUME NEW fun, IsFiniteSet(DOMAIN fun), + \A x \in DOMAIN fun : fun[x] \in Nat + PROVE SumFunction(fun) \in Nat + +THEOREM SumFunctionInt == + ASSUME NEW fun, IsFiniteSet(DOMAIN fun), + \A x \in DOMAIN fun : fun[x] \in Int + PROVE SumFunction(fun) \in Int + +THEOREM SumFunctionEmpty == + ASSUME NEW fun, DOMAIN fun = {} + PROVE SumFunction(fun) = 0 + +THEOREM SumFunctionNonempty == + ASSUME NEW fun, IsFiniteSet(DOMAIN fun), NEW x \in DOMAIN fun, + \A i \in DOMAIN fun : fun[i] \in Int + PROVE SumFunction(fun) = fun[x] + SumFunctionOnSet(fun, (DOMAIN fun) \ {x}) + +THEOREM SumFunctionExcept == + ASSUME NEW fun, NEW i, NEW y \in Int, IsFiniteSet(DOMAIN fun), + \A x \in DOMAIN fun : fun[x] \in Int + PROVE SumFunction([fun EXCEPT ![i] = y]) = + IF i \in DOMAIN fun + THEN SumFunction(fun) + y - fun[i] + ELSE SumFunction(fun) + +THEOREM SumFunctionZero == + ASSUME NEW fun, IsFiniteSet(DOMAIN fun), + \A x \in DOMAIN fun : fun[x] \in Nat + PROVE SumFunction(fun) = 0 <=> \A x \in DOMAIN fun : fun[x] = 0 + +THEOREM SumFunctionMonotonic == + ASSUME NEW f, IsFiniteSet(DOMAIN f), NEW g, DOMAIN g = DOMAIN f, + \A x \in DOMAIN f : f[x] \in Int, + \A x \in DOMAIN f : g[x] \in Int, + \A x \in DOMAIN f : f[x] <= g[x] + PROVE SumFunction(f) <= SumFunction(g) + +THEOREM SumFunctionStrictlyMonotonic == + ASSUME NEW f, IsFiniteSet(DOMAIN f), NEW g, DOMAIN g = DOMAIN f, + \A x \in DOMAIN f : f[x] \in Int, + \A x \in DOMAIN f : g[x] \in Int, + \A x \in DOMAIN f : f[x] <= g[x], + NEW s \in DOMAIN f, f[s] < g[s] + PROVE SumFunction(f) < SumFunction(g) + +============================================================================= +\* Created Thu Apr 11 10:36:10 PDT 2013 by tomr diff --git a/modules/FunctionTheorems_proofs.tla b/modules/FunctionTheorems_proofs.tla new file mode 100644 index 0000000..f1f1965 --- /dev/null +++ b/modules/FunctionTheorems_proofs.tla @@ -0,0 +1,1413 @@ +--------------------- MODULE FunctionTheorems_proofs ------------------------ +(***************************************************************************) +(* `^{\large \vspace{12pt} *) +(* Proofs of facts about functions. *) +(* Originally contributed by Tom Rodeheffer, MSR. *) +(* \vspace{12pt}}^' *) +(***************************************************************************) + +EXTENDS Functions, Integers, NaturalsInduction, WellFoundedInduction, + FiniteSetTheorems, FoldsTheorems, TLAPS + +(***************************************************************************) +(* `. .' *) +(* *) +(* Function restriction. *) +(* *) +(* `. .' *) +(***************************************************************************) +THEOREM Fun_RestrictProperties == + ASSUME NEW S, NEW T, NEW f \in [S -> T], NEW A \in SUBSET S + PROVE /\ Restrict(f,A) \in [A -> T] + /\ \A x \in A : Restrict(f,A)[x] = f[x] +BY DEF Restrict + +(***************************************************************************) +(* `. .' *) +(* *) +(* Range of a function. *) +(* *) +(* `. .' *) +(***************************************************************************) +THEOREM Fun_RangeProperties == + ASSUME NEW S, NEW T, NEW f \in [S -> T] + PROVE /\ Range(f) \subseteq T + /\ \A y \in Range(f) : \E x \in S : f[x] = y + /\ f \in Surjection(S, Range(f)) +BY DEF Range, Surjection + + +(***************************************************************************) +(* `. .' *) +(* *) +(* Inverse of a function. *) +(* *) +(* `. .' *) +(***************************************************************************) +THEOREM Fun_InverseProperties == + ASSUME NEW S, NEW T, NEW f \in [S -> T] + PROVE /\ (S = {} => T = {}) => Inverse(f,S,T) \in [T -> S] + /\ \A y \in Range(f) : f[Inverse(f,S,T)[y]] = y +BY DEF Inverse, Range + + +(***************************************************************************) +(* `. .' *) +(* *) +(* Introduction rules for injections, surjections, bijections. *) +(* *) +(* `. .' *) +(***************************************************************************) +THEOREM Fun_IsInj == + ASSUME NEW S, NEW T, NEW F \in [S -> T], + \A a,b \in S : F[a] = F[b] => a = b + PROVE F \in Injection(S,T) +BY DEF Injection, IsInjective + + +THEOREM Fun_IsSurj == + ASSUME NEW S, NEW T, NEW F \in [S -> T], + \A t \in T : \E s \in S : F[s] = t + PROVE F \in Surjection(S,T) +BY DEF Surjection + + +THEOREM Fun_IsBij == + ASSUME NEW S, NEW T, NEW F, + \/ F \in Injection(S,T) + \/ (F \in [S -> T] /\ \A a,b \in S : F[a] = F[b] => a = b), + + \/ F \in Surjection(S,T) + \/ (F \in [S -> T] /\ \A t \in T : \E s \in S : F[s] = t) + PROVE F \in Bijection(S,T) +BY DEF Bijection, Injection, IsInjective, Surjection + + + + +(***************************************************************************) +(* `. .' *) +(* *) +(* Properties of injections, surjections, and bijections. *) +(* *) +(* `. .' *) +(***************************************************************************) +THEOREM Fun_InjectionProperties == + ASSUME NEW S, NEW T, NEW F \in Injection(S,T) + PROVE /\ F \in [S -> T] + /\ \A a,b \in S : F[a] = F[b] => a = b +BY DEF Injection, IsInjective + + +THEOREM Fun_SurjectionProperties == + ASSUME NEW S, NEW T, NEW F \in Surjection(S,T) + PROVE /\ F \in [S -> T] + /\ \A t \in T : \E s \in S : F[s] = t + /\ Range(F) = T +BY DEF Surjection, Range + + +THEOREM Fun_BijectionProperties == + ASSUME NEW S, NEW T, NEW F \in Bijection(S,T) + PROVE /\ F \in [S -> T] + /\ F \in Injection(S,T) + /\ F \in Surjection(S,T) + /\ \A a,b \in S : F[a] = F[b] => a = b + /\ \A t \in T : \E s \in S : F[s] = t +BY DEF Bijection, Injection, IsInjective, Surjection + + + +(***************************************************************************) +(* `. .' *) +(* *) +(* A surjection in [S -> T] such that there is no surjection from any *) +(* subset of S to T is a bijection. *) +(* *) +(* `. .' *) +(***************************************************************************) +THEOREM Fun_SmallestSurjectionIsBijection == + ASSUME NEW S, NEW T, NEW f \in Surjection(S,T), + \A U \in SUBSET S : U # S => Surjection(U,T) = {} + PROVE f \in Bijection(S,T) +<1>1. f \in [S -> T] + BY Fun_SurjectionProperties +<1>2. SUFFICES ASSUME f \notin Injection(S,T) PROVE FALSE + BY Fun_IsBij +<1>3. PICK a,b \in S : a # b /\ f[a] = f[b] + BY <1>1, <1>2, Fun_IsInj +<1>. DEFINE U == S \ {b} +<1>4. U \in SUBSET S /\ U # S + OBVIOUS +<1>. DEFINE g == [x \in U |-> f[x]] +<1>5. g \in Surjection(U,T) + <2>1. g \in [U -> T] BY <1>1 + <2>2. ASSUME NEW t \in T PROVE \E u \in U : g[u] = t + <3>1. CASE t = f[b] BY <1>3, <3>1 + <3>2. CASE t # f[b] + <4>1. PICK s \in S : f[s] = t + BY Fun_SurjectionProperties + <4>2. s \in U BY <3>2, <4>1 + <4>. QED BY <4>1, <4>2 + <3>3. QED BY <3>1, <3>2 + <2>3. QED BY <2>1, <2>2, Fun_IsSurj +<1>. QED BY <1>4, <1>5 + + + +(***************************************************************************) +(* `. .' *) +(* *) +(* Transitivity of injections, surjections, bijections. *) +(* *) +(* `. .' *) +(***************************************************************************) +THEOREM Fun_InjTransitive == + ASSUME NEW S, NEW T, NEW U, + NEW F \in Injection(S,T), + NEW G \in Injection(T,U) + PROVE [s \in S |-> G[F[s]]] \in Injection(S,U) +BY DEF Injection, IsInjective + + +THEOREM Fun_SurjTransitive == + ASSUME NEW S, NEW T, NEW U, + NEW F \in Surjection(S,T), + NEW G \in Surjection(T,U) + PROVE [s \in S |-> G[F[s]]] \in Surjection(S,U) +BY Zenon DEF Surjection + + +THEOREM Fun_BijTransitive == + ASSUME NEW S, NEW T, NEW U, + NEW F \in Bijection(S,T), + NEW G \in Bijection(T,U) + PROVE [s \in S |-> G[F[s]]] \in Bijection(S,U) +BY Fun_SurjTransitive, Fun_InjTransitive, Zenon DEF Bijection + + + +(***************************************************************************) +(* `. .' *) +(* *) +(* The inverse of a surjection is an injection and vice versa. *) +(* *) +(* `. .' *) +(***************************************************************************) +THEOREM Fun_SurjInverse == + ASSUME NEW S, NEW T, NEW f \in Surjection(S,T) + PROVE Inverse(f,S,T) \in Injection(T,S) +BY DEF Inverse, Surjection, Injection, IsInjective, Range + + +THEOREM Fun_InjInverse == + ASSUME NEW S, NEW T, NEW f \in Injection(S,T), S = {} => T = {} + PROVE Inverse(f,S,T) \in Surjection(T,S) +<1>. DEFINE g == Inverse(f,S,T) +<1>1. f \in [S -> T] BY DEF Injection, IsInjective +<1>2. g \in [T -> S] BY <1>1, Fun_InverseProperties, Zenon +<1>3. ASSUME NEW s \in S PROVE \E t \in T : g[t] = s + <2>10. g[f[s]] = s BY DEF Inverse, Range, Injection, IsInjective + <2>. QED BY <2>10, <1>1 +<1>. QED BY <1>2, <1>3 DEF Surjection + + +(***************************************************************************) +(* `. .' *) +(* *) +(* Properties of the inverse of a bijection. *) +(* *) +(* `. .' *) +(***************************************************************************) +THEOREM Fun_BijInverse == + ASSUME NEW S, NEW T, NEW f \in Bijection(S,T) + PROVE /\ Inverse(f,S,T) \in Bijection(T,S) + /\ \A s \in S : Inverse(f,S,T)[f[s]] = s + /\ Inverse(Inverse(f,S,T), T,S) = f + +<1>. DEFINE g == Inverse(f,S,T) +<1>1. f \in [S -> T] BY DEF Bijection, Injection +<1>2. f \in Surjection(S,T) BY DEF Bijection +<1>3. \A a,b \in S : f[a] = f[b] => a = b BY DEF Bijection, Injection, IsInjective +<1>4. g \in Injection(T,S) BY <1>2, Fun_SurjInverse + +<1>5. \A t \in T : f[g[t]] = t BY <1>2 DEF Surjection, Inverse, Range +<1>6. \A s \in S : g[f[s]] = s BY <1>1, <1>3 DEF Inverse, Range + +<1>7. \A a,b \in T : g[a] = g[b] => a = b BY <1>5 +<1>8. \A s \in S : \E t \in T : g[t] = s BY <1>1, <1>6 + +<1>9. g \in Bijection(T,S) BY <1>4, <1>8 DEF Bijection, Injection, Surjection + +<1>10. Inverse(g,T,S) = f + <2>1. ASSUME NEW s \in S PROVE f[s] = CHOOSE t \in T : s \in Range(g) => g[t] = s + <3>1. PICK a \in T : g[a] = s BY <1>9 DEF Bijection, Surjection + <3>2. \A b \in T : g[b] = s => a = b BY <3>1, <1>7 + <3>3. f[s] = a BY <3>1, <1>5 + <3>4. s \in Range(g) BY <3>1, <1>4 DEF Injection, Range + <3>. QED BY <3>1, <3>2, <3>3, <3>4 + <2>. QED BY <2>1, <1>1 DEF Inverse +<1>. QED BY <1>9, <1>6, <1>10 + +(***************************************************************************) +(* We cannot conclude that a function f is a bijection if its inverse is *) +(* a bijection, and the following is a counter-example. *) +(* *) +(* S = {1,2} T = {3,4} *) +(* f = [x \in S |-> 3] *) +(* *) +(* Then, Inverse(f,S,T) can very well be (3 :> 1) @@ (4 :> 2), which is a *) +(* bijection although f is not. *) +(***************************************************************************) + + +(***************************************************************************) +(* `. .' *) +(* *) +(* The restriction of a bijection is a bijection. *) +(* *) +(* `. .' *) +(***************************************************************************) +THEOREM Fun_BijRestrict == + ASSUME NEW S, NEW T, NEW F \in Bijection(S,T), + NEW R \in SUBSET S + PROVE Restrict(F, R) \in Bijection(R, Range(Restrict(F, R))) +BY DEF Bijection, Injection, IsInjective, Surjection, Range, Restrict + + + +(***************************************************************************) +(* `. .' *) +(* *) +(* Given F an injection from S to T, then F is a bijection from S to F(S). *) +(* *) +(* `. .' *) +(***************************************************************************) +THEOREM Fun_InjMeansBijImage == + ASSUME NEW S, NEW T, NEW F \in Injection(S,T) + PROVE F \in Bijection(S, Range(F)) +BY DEF Bijection, Injection, IsInjective, Surjection, Range + + + + +----------------------------------------------------------------------------- +(***************************************************************************) +(* `^{\large \vspace{12pt} *) +(* Facts about exists jections. *) +(* \vspace{12pt}}^' *) +(***************************************************************************) + + + +(***************************************************************************) +(* `. .' *) +(* *) +(* Definitions restated as facts. *) +(* *) +(* `. .' *) +(***************************************************************************) +THEOREM Fun_ExistsInj == + \A S,T : ExistsInjection(S,T) <=> Injection(S,T) # {} +BY DEF ExistsInjection + + +THEOREM Fun_ExistsSurj == + \A S,T : ExistsSurjection(S,T) <=> Surjection(S,T) # {} +BY DEF ExistsSurjection + + +THEOREM Fun_ExistsBij == + \A S,T : ExistsBijection(S,T) <=> Bijection(S,T) # {} +BY DEF ExistsBijection + + + + +(***************************************************************************) +(* `. .' *) +(* *) +(* There is a surjection from any set S to any non-empty subset T of S. *) +(* (Note that there cannot be a surjection to {} except if S is empty.) *) +(* *) +(* `. .' *) +(***************************************************************************) +THEOREM Fun_ExistsSurjSubset == + ASSUME NEW S, NEW T \in SUBSET S, T # {} + PROVE ExistsSurjection(S,T) +<1>. PICK x \in T : TRUE OBVIOUS +<1>. [s \in S |-> IF s \in T THEN s ELSE x] \in Surjection(S,T) + BY DEF Surjection +<1>. QED BY DEF ExistsSurjection + + + + +(***************************************************************************) +(* `. .' *) +(* *) +(* If there is a surjection from S to T, then there is an injection from T *) +(* to S. *) +(* *) +(* `. .' *) +(***************************************************************************) +THEOREM Fun_ExistsSurjMeansExistsRevInj == + ASSUME NEW S, NEW T, ExistsSurjection(S,T) + PROVE ExistsInjection(T,S) +BY Fun_SurjInverse DEF ExistsSurjection, ExistsInjection + + + +(***************************************************************************) +(* `. .' *) +(* *) +(* ExistsBijection is reflexive, symmetric, and transitive. *) +(* *) +(* `. .' *) +(***************************************************************************) +THEOREM Fun_ExistsBijReflexive == + ASSUME NEW S + PROVE ExistsBijection(S,S) +<1>. [s \in S |-> s] \in Bijection(S,S) BY DEF Bijection, Injection, IsInjective, Surjection +<1>. QED BY DEF ExistsBijection + + +THEOREM Fun_ExistsBijSymmetric == + ASSUME NEW S, NEW T, ExistsBijection(S,T) + PROVE ExistsBijection(T,S) +BY Fun_BijInverse DEF ExistsBijection + + +THEOREM Fun_ExistsBijTransitive == + ASSUME NEW S, NEW T, NEW U, ExistsBijection(S,T), ExistsBijection(T,U) + PROVE ExistsBijection(S,U) +BY Fun_BijTransitive, Zenon DEF ExistsBijection + + + +(***************************************************************************) +(* `. .' *) +(* *) +(* Existence of injections and surjections is reflexive and transitive. *) +(* *) +(* `. .' *) +(***************************************************************************) +THEOREM Fun_ExistsInjReflexive == + ASSUME NEW S + PROVE ExistsInjection(S,S) +BY Fun_ExistsBijReflexive DEF ExistsBijection, ExistsInjection, Bijection + + +THEOREM Fun_ExistsSurjReflexive == + ASSUME NEW S + PROVE ExistsSurjection(S,S) +BY Fun_ExistsBijReflexive DEF ExistsBijection, ExistsSurjection, Bijection + + +THEOREM Fun_ExistsInjTransitive == + ASSUME NEW S, NEW T, NEW U, + ExistsInjection(S,T), ExistsInjection(T,U) + PROVE ExistsInjection(S,U) +BY Fun_InjTransitive, Zenon DEF ExistsInjection + + +THEOREM Fun_ExistsSurjTransitive == + ASSUME NEW S, NEW T, NEW U, + ExistsSurjection(S,T), ExistsSurjection(T,U) + PROVE ExistsSurjection(S,U) +BY Fun_SurjTransitive, Zenon DEF ExistsSurjection + + +----------------------------------------------------------------------------- +(***************************************************************************) +(* `^{\large \vspace{12pt} *) +(* The Cantor-Bernstein-Schroeder theorem. *) +(* \vspace{12pt}}^' *) +(***************************************************************************) + +(***************************************************************************) +(* `. .' *) +(* *) +(* If there exists an injection from S to T, where T is a subset of S, *) +(* then there exists a bijection from S to T. *) +(* *) +(* A lemma for the Cantor-Bernstein-Schroeder theorem. *) +(* *) +(* This proof is formalized from *) +(* `^\url{http://www.proofwiki.org/wiki/Cantor-Bernstein-Schroeder\_Theorem/Lemma}^' *) +(* retrieved April 29, 2013. *) +(* *) +(* `. .' *) +(***************************************************************************) +THEOREM Fun_CantorBernsteinSchroeder_Lemma == + ASSUME NEW S, NEW T, T \subseteq S, ExistsInjection(S,T) + PROVE ExistsBijection(S,T) +<1> PICK F \in Injection(S,T) : TRUE BY Fun_ExistsInj + +<1>1. /\ F \in [S -> T] + /\ \A a,b \in S : F[a] = F[b] => a = b + BY Fun_InjectionProperties + +(*************************************************************************) +(* Pick Y as S excluding T. *) +(*************************************************************************) +<1>2. PICK Y : Y = S \ T BY Zenon + +(*************************************************************************) +(* Define Ci[0] as Y, and Ci[i+1] as the image of Ci[i] under F. *) +(*************************************************************************) +<1> DEFINE Ci[i \in Nat] == + IF i = 0 THEN Y ELSE {F[s] : s \in Ci[i-1]} +<1> HIDE DEF Ci + +<1>3. \A i \in Nat : Ci[i] = IF i = 0 THEN Y ELSE {F[s] : s \in Ci[i-1]} + (***********************************************************************) + (* Use NatInductiveDef to prove that Ci equals its definition. *) + (***********************************************************************) + <2> DEFINE + f0 == Y + Def(v,i) == {F[s] : s \in v} + f == CHOOSE f : f = [i \in Nat |-> IF i = 0 THEN f0 ELSE Def(f[i-1],i)] + <2> SUFFICES \A i \in Nat : f[i] = IF i = 0 THEN f0 ELSE Def(f[i-1],i) BY DEF Ci + <2> HIDE DEF f0, Def, f + <2> SUFFICES NatInductiveDefConclusion(f,f0,Def) BY DEF NatInductiveDefConclusion + <2> SUFFICES NatInductiveDefHypothesis(f,f0,Def) BY NatInductiveDef, Zenon + <2> QED BY Zenon DEF NatInductiveDefHypothesis, f + +(*************************************************************************) +(* Applying F to an element of Ci[i] produces an element of Ci[i+1]. *) +(*************************************************************************) +<1>4. ASSUME NEW i \in Nat, NEW s \in Ci[i] + PROVE F[s] \in Ci[i+1] + BY <1>3 + +(*************************************************************************) +(* Each element of Ci[i+1] is the application of F to some element in *) +(* Ci[i]. *) +(*************************************************************************) +<1>5. ASSUME NEW i \in Nat, NEW t \in Ci[i+1] + PROVE \E s \in Ci[i] : F[s] = t + <2>1. Ci[i+1] = {F[s] : s \in Ci[i]} + BY <1>3, i+1 \in Nat \ {0}, (i+1)-1 = i, Zenon + <2>. QED BY <2>1 + +(*************************************************************************) +(* Each Ci[i] \subseteq S. *) +(*************************************************************************) +<1>6. \A i \in Nat : Ci[i] \subseteq S + <2> DEFINE Prop(i) == Ci[i] \subseteq S + <2> SUFFICES \A i \in Nat : Prop(i) OBVIOUS + <2>1. Prop(0) BY <1>2, <1>3, Zenon + <2>2. ASSUME NEW i \in Nat, Prop(i) PROVE Prop(i+1) + <3> SUFFICES ASSUME NEW t \in Ci[i+1] PROVE t \in S OBVIOUS + <3>1. PICK s \in Ci[i] : F[s] = t BY <1>5 + <3>2. s \in S BY <2>2 + <3> QED BY <3>1, <3>2, <1>1 + <2> HIDE DEF Prop + <2> QED BY <2>1, <2>2, NatInduction, Isa + +(*************************************************************************) +(* Pick C as the union of all Ci[i]. *) +(*************************************************************************) +<1>7. PICK C : C = UNION {Ci[i] : i \in Nat} OBVIOUS +<1>8. C \subseteq S BY <1>6, <1>7 + +(*************************************************************************) +(* Pick FC as the image of C under F. *) +(*************************************************************************) +<1>9. PICK FC : FC = {F[c] : c \in C} BY Zenon +<1>10. FC \subseteq T BY <1>1, <1>8, <1>9 + +(*************************************************************************) +(* C = Y \cup FC because Ci[0] = Y and Ci[i+1] = image of Ci[i] under F. *) +(*************************************************************************) +<1>11. C = Y \cup FC + <2>1. ASSUME NEW c \in C PROVE c \in Y \cup FC + <3>1. PICK i \in Nat : c \in Ci[i] BY <1>7 + <3>2. CASE i = 0 BY <3>1, <3>2, <1>3, Zenon + <3>3. CASE i > 0 + <4>0. i-1 \in Nat + BY <3>3 + <4>1. PICK s \in Ci[i-1] : F[s] = c + BY <4>0, <3>1, <1>5 + <4>2. s \in C BY <3>3, <1>7 + <4> QED BY <4>1, <4>2, <1>9 + <3> QED BY <3>2, <3>3 + <2>2. ASSUME NEW c \in Y \cup FC PROVE c \in C + <3>1. CASE c \in Y BY <3>1, <1>3, <1>7, Zenon + <3>2. CASE c \in FC + <4>1. PICK s \in C : F[s] = c BY <3>2, <1>9 + <4>2. PICK i \in Nat : s \in Ci[i] BY <4>1, <1>7 + <4>3. F[s] \in Ci[i+1] BY <4>2, <1>4 + <4> QED BY <4>1, <4>3, <1>7 + <3> QED BY <3>1, <3>2 + <2> QED BY <2>1, <2>2 + +(*************************************************************************) +(* S \ C is the same as T \ FC. *) +(*************************************************************************) +<1>12. S \ C = T \ FC BY <1>2, <1>11 + +(*************************************************************************) +(* Pick H as F on C and the identity on S \ C. Since F (restricted to *) +(* C) is a bijection from C to FC and S \ C = T \ FC, this makes H a *) +(* bijection from S to T. *) +(*************************************************************************) +<1>13. PICK H : H = [s \in S |-> IF s \in C THEN F[s] ELSE s] OBVIOUS +<1>14. H \in Bijection(S,T) + (***********************************************************************) + (* A useful lemma. If a \in C and b \notin C, then H[a] # H[b]. *) + (***********************************************************************) + <2>1. ASSUME NEW a \in S, NEW b \in S, a \in C, b \notin C PROVE H[a] # H[b] + <3>1. H[a] \in FC BY <2>1, <1>1, <1>9, <1>13 + <3>2. H[b] \in T \ FC BY <2>1, <1>12, <1>13 + <3> QED BY <3>1, <3>2 + + <2>2. H \in [S -> T] + <3> SUFFICES ASSUME NEW s \in S PROVE H[s] \in T BY <1>13 + <3>1. CASE s \in C BY <3>1, <1>1, <1>10, <1>13 + <3>2. CASE s \notin C BY <3>2, <1>12, <1>13 + <3> QED BY <3>1, <3>2 + + <2>3. ASSUME NEW a \in S, NEW b \in S, H[a] = H[b] PROVE a = b + <3> H[a] = H[b] BY <2>3 + <3>1. CASE a \in C /\ b \in C BY <3>1, <1>1, <1>13 + <3>2. CASE a \in C /\ b \notin C BY <3>2, <2>1 (* impossible by lemma *) + <3>3. CASE a \notin C /\ b \in C BY <3>3, <2>1 (* impossible by lemma *) + <3>4. CASE a \notin C /\ b \notin C BY <3>4, <1>13 + <3> QED BY <3>1, <3>2, <3>3, <3>4 + + <2>4. ASSUME NEW t \in T PROVE \E s \in S : H[s] = t + <3>1. CASE t \in FC BY <3>1, <1>8, <1>9, <1>13 + <3>2. CASE t \notin FC BY <3>2, <1>12, <1>13 + <3> QED BY <3>1, <3>2 + + <2> QED BY <2>2, <2>3, <2>4, Fun_IsBij + +<1> QED BY <1>14, Fun_ExistsBij + + + + + +(***************************************************************************) +(* `. .' *) +(* *) +(* If an injection exists from S to T and an injection exists from T to S, *) +(* then there is a bijection from S to T. *) +(* *) +(* This is the Cantor-Bernstein-Schroeder theorem. *) +(* *) +(* This proof is formalized from *) +(* `^\url{http://www.proofwiki.org/wiki/Cantor-Bernstein-Schroeder_Theorem/Proof_5}^' *) +(* retrieved April 29, 2013. *) +(* *) +(* `. .' *) +(***************************************************************************) +THEOREM Fun_CantorBernsteinSchroeder == + ASSUME NEW S, NEW T, + ExistsInjection(S,T), ExistsInjection(T,S) + PROVE ExistsBijection(S,T) + +<1>1. PICK F : F \in Injection(S,T) BY DEF ExistsInjection +<1>2. PICK G : G \in Injection(T,S) BY DEF ExistsInjection +<1>. DEFINE GF == [s \in S |-> G[F[s]]] +<1>3. Range(G) \subseteq S BY <1>2, Fun_RangeProperties DEF Injection +<1>4. GF \in Injection(S, Range(G)) BY <1>1, <1>2 DEF Injection, IsInjective, Range +<1>5. ExistsBijection(S, Range(G)) + BY <1>3, <1>4, Fun_CantorBernsteinSchroeder_Lemma DEF ExistsInjection +<1>6. ExistsBijection(T, Range(G)) + BY <1>2, Fun_InjMeansBijImage DEF ExistsBijection +<1>. QED BY <1>5, <1>6, Fun_ExistsBijSymmetric, Fun_ExistsBijTransitive + + + +(***************************************************************************) +(* `. .' *) +(* *) +(* Applications of the Cantor-Bernstein-Schroeder Theorem. *) +(* If there exists an injection f: A->B and a surjection g: A->B, then *) +(* there exists a bijection between A and B. *) +(* Also, if there are surjections between A and B, then there is a *) +(* bijection. *) +(* *) +(* `. .' *) +(***************************************************************************) + +THEOREM Fun_ExistInjAndSurjThenBij == + ASSUME NEW S, NEW T, + ExistsInjection(S,T), ExistsSurjection(S,T) + PROVE ExistsBijection(S,T) +<1>. ExistsInjection(T,S) BY Fun_SurjInverse DEF ExistsInjection, ExistsSurjection +<1>. QED BY Fun_CantorBernsteinSchroeder + + + +THEOREM Fun_ExistSurjAndSurjThenBij == + ASSUME NEW S, NEW T, + ExistsSurjection(S,T), ExistsSurjection(T,S) + PROVE ExistsBijection(S,T) +<1>. ExistsInjection(S,T) BY Fun_SurjInverse DEF ExistsInjection, ExistsSurjection +<1>2. QED BY Fun_ExistInjAndSurjThenBij + + + + +(***************************************************************************) +(* `. .' *) +(* *) +(* Equivalences for ExistsBijection. *) +(* *) +(* `. .' *) +(***************************************************************************) +THEOREM Fun_ExistsBijEquiv == + ASSUME NEW S, NEW T + PROVE /\ ExistsBijection(S,T) <=> ExistsBijection(T,S) + /\ ExistsBijection(S,T) <=> ExistsInjection(S,T) /\ ExistsInjection(T,S) + /\ ExistsBijection(S,T) <=> ExistsInjection(S,T) /\ ExistsSurjection(S,T) + /\ ExistsBijection(S,T) <=> ExistsInjection(T,S) /\ ExistsSurjection(T,S) + /\ ExistsBijection(S,T) <=> ExistsSurjection(S,T) /\ ExistsSurjection(T,S) + +<1>1. ExistsBijection(S,T) <=> ExistsBijection(T,S) + BY Fun_ExistsBijSymmetric +<1>2. ExistsInjection(S,T) /\ ExistsInjection(T,S) => ExistsBijection(S,T) + BY Fun_CantorBernsteinSchroeder +<1>3. \A S1, T1 : ExistsBijection(S1,T1) => ExistsSurjection(S1,T1) + BY DEF ExistsBijection, ExistsSurjection, Bijection +<1>4. \A S1,T1 : ExistsSurjection(S1,T1) => ExistsInjection(T1,S1) + BY Fun_ExistsSurjMeansExistsRevInj +<1> QED BY <1>1, <1>2, <1>3, <1>4 + + +----------------------------------------------------------------------------- +(***************************************************************************) +(* `^{\large \vspace{12pt} *) +(* Facts about jections involving 1..n. *) +(* \vspace{12pt}}^' *) +(***************************************************************************) + + +(***************************************************************************) +(* `. .' *) +(* *) +(* There is a bijection from 1..b-a+1 to a..b for integers a,b with a <= b.*) +(* *) +(* `. .' *) +(***************************************************************************) +THEOREM Fun_ExistsBijInterval == + ASSUME NEW a \in Int, NEW b \in Int, a <= b + PROVE ExistsBijection(1 .. b-a+1, a .. b) + +<1>. DEFINE f == [i \in 1 .. b-a+1 |-> i+a-1] +<1>1. f \in [1 .. b-a+1 -> a .. b] BY SMT +<1>2. f \in Injection(1 .. b-a+1, a .. b) BY DEF Injection, IsInjective +<1>3. \A t \in a..b : + /\ t-a+1 \in 1 .. (b-a+1) + /\ f[t-a+1] = t + OBVIOUS +<1>4. f \in Surjection(1 .. b-a+1, a .. b) + BY <1>3, <1>1, Zenon DEF Surjection +<1>. QED BY <1>1, <1>2, <1>4 DEF ExistsBijection, Bijection + + +(***************************************************************************) +(* `. .' *) +(* *) +(* There is an injection from 1..n to 1..m iff n \leq m. *) +(* *) +(* `. .' *) +(***************************************************************************) +THEOREM Fun_NatInjLeq == + ASSUME NEW n \in Nat, NEW m \in Nat + PROVE ExistsInjection(1..n,1..m) <=> n \leq m +(*************************************************************************) +(* n \leq m means Injection exists. This part is easy. *) +(*************************************************************************) +<1>1. ASSUME n \leq m PROVE [i \in 1..n |-> i] \in Injection(1..n, 1..m) + BY <1>1 DEF Injection, IsInjective + +(*************************************************************************) +(* Injection exists means n \leq m. This part is harder. *) +(*************************************************************************) +<1>2. ASSUME ExistsInjection(1..n,1..m) PROVE n \leq m + <2>. DEFINE P(mm) == \A nn \in Nat : nn > mm => Injection(1..nn, 1..mm) = {} + <2>1. SUFFICES \A mm \in Nat : P(mm) + BY <1>2 DEF ExistsInjection + <2>2. P(0) + <3>. SUFFICES ASSUME NEW nn \in Nat, nn > 0 + PROVE Injection(1..nn, 1..0) = {} + OBVIOUS + <3>1. /\ 1 .. nn # {} + /\ 1 .. 0 = {} + BY Isa + <3>. QED BY <3>1 DEF Injection + <2>3. ASSUME NEW mm \in Nat, P(mm) PROVE P(mm+1) + <3>1. SUFFICES ASSUME NEW nn \in Nat, nn > mm+1, + NEW f \in Injection(1..nn, 1..mm+1) + PROVE FALSE + OBVIOUS + <3>2. ASSUME NEW i \in 1..nn, f[i] = mm+1 PROVE FALSE + <4>. DEFINE g == [j \in 1..nn-1 |-> IF j1. nn-1 \in Nat /\ nn-1 > mm BY <3>1 + <4>2. g \in Injection(1..nn-1, 1..mm) BY <3>2 DEF Injection, IsInjective + <4>. QED BY <4>1, <4>2, P(mm), Zenon DEF Injection + <3>3. ASSUME ~\E i \in 1..nn : f[i] = mm+1 PROVE FALSE + <4>. f \in Injection(1..nn, 1..mm) BY <3>3 DEF Injection + <4>. QED BY <3>1, P(mm) + <3>. QED BY <3>2, <3>3 + <2>. QED BY NatInduction, <2>2, <2>3, Isa + +<1> QED BY <1>1, <1>2 DEF ExistsInjection + + + + + + +(***************************************************************************) +(* `. .' *) +(* *) +(* If a surjection from 1..n to S exists (for some n \in Nat) then a *) +(* bijection from 1..m to S exists (for some m \in Nat) and m \leq n. *) +(* *) +(* `. .' *) +(***************************************************************************) +THEOREM Fun_NatSurjImpliesNatBij == + ASSUME NEW S, NEW n \in Nat, ExistsSurjection(1..n,S) + PROVE \E m \in Nat : ExistsBijection(1..m,S) /\ m \leq n + + (*************************************************************************) + (* Pick the smallest m \in Nat for which there is a surjection from *) + (* 1..m to S. *) + (*************************************************************************) +<1>1. PICK m \in Nat : + /\ ExistsSurjection(1..m, S) + /\ \A k \in Nat : k < m => ~ExistsSurjection(1..k, S) + <2>. DEFINE NN == { m \in Nat : ExistsSurjection(1..m, S) } + <2>1. PICK m \in NN : \A k \in NN : <> \notin OpToRel(<, Nat) + BY WFMin, NatLessThanWellFounded, Zenon + <2>. QED + BY <2>1, Zenon DEF OpToRel + +<1>2. m <= n BY <1>1 + (*************************************************************************) + (* Any surjection from 1..m to S is bijective. *) + (*************************************************************************) +<1>3. PICK f \in Surjection(1..m, S) : TRUE BY <1>1 DEF ExistsSurjection +<1>4. ASSUME f \notin Injection(1..m, S) PROVE FALSE + <2>1. f \in [1..m -> S] BY <1>3 DEF Surjection + <2>2. PICK i,j \in 1..m : i < j /\ f[i] = f[j] + <3>1. PICK ii,jj \in 1..m : ii # jj /\ f[ii] = f[jj] + BY <2>1, <1>4 DEF Injection, IsInjective + <3>2. CASE ii < jj BY <3>1, <3>2 + <3>3. CASE jj < ii BY <3>1, <3>3 + <3>. QED BY SMT, <3>1, <3>2, <3>3 + <2>3. m-1 \in Nat BY <2>2 + <2>. DEFINE g == [k \in 1..m-1 |-> IF k=j THEN f[m] ELSE f[k]] + <2>4. g \in Surjection(1..m-1, S) + <3>1. g \in [1..m-1 -> S] BY <2>1 + <3>2. ASSUME NEW s \in S PROVE \E k \in 1..m-1 : g[k] = s + <4>. PICK l \in 1..m : f[l] = s BY <1>3 DEF Surjection + <4>1. CASE l = j + BY <2>2, <4>1, i \in 1 .. m-1 + <4>2. CASE l # j /\ l = m + BY <4>2, j \in 1 .. m-1 + <4>3. CASE l # j /\ l # m + BY <4>3 + <4>. QED BY <4>1, <4>2, <4>3 + <3>. QED BY <3>1, <3>2, Zenon DEF Surjection + <2>. QED BY SMT, <2>3, <2>4, <1>1 DEF ExistsSurjection + +<1>. QED BY <1>2, <1>3, <1>4 DEF ExistsBijection, Bijection + + +(***************************************************************************) +(* Simple corollary. *) +(***************************************************************************) +THEOREM Fun_NatSurjEquivNatBij == + ASSUME NEW S + PROVE (\E n \in Nat : ExistsSurjection(1..n,S)) + <=> (\E m \in Nat : ExistsBijection(1..m,S)) +BY Fun_NatSurjImpliesNatBij, Fun_ExistsBijEquiv + + + +(***************************************************************************) +(* `. .' *) +(* *) +(* For any set S, given n, m \in Nat such that bijections exist from 1..n *) +(* to S and from 1..m to S, then it must be the case that n = m. *) +(* *) +(* `. .' *) +(***************************************************************************) +THEOREM Fun_NatBijSame == + ASSUME NEW S, + NEW n \in Nat, ExistsBijection(1..n,S), + NEW m \in Nat, ExistsBijection(1..m,S) + PROVE n = m +BY Fun_NatInjLeq, Fun_ExistsBijEquiv, Fun_ExistsBijTransitive + + + +(***************************************************************************) +(* `. .' *) +(* *) +(* S is empty iff there exists a bijection from 1..0 to S. *) +(* *) +(* `. .' *) +(***************************************************************************) +THEOREM Fun_NatBijEmpty == + ASSUME NEW S + PROVE ExistsBijection(1..0,S) <=> S = {} + +<1>1. ASSUME ExistsBijection(1..0, S), S # {} PROVE FALSE + <2>. ExistsInjection(S, 1..0) BY <1>1, Fun_ExistsBijEquiv + <2>. QED BY <1>1 DEF ExistsInjection, Injection +<1>2. ASSUME S = {} PROVE ExistsBijection(1..0, S) + BY <1>2, Fun_ExistsBijReflexive, Isa +<1>3. QED BY <1>1, <1>2 + + +(***************************************************************************) +(* `. .' *) +(* *) +(* S is a singleton iff there exists a bijection from 1..1 to S. *) +(* *) +(* `. .' *) +(***************************************************************************) +THEOREM Fun_NatBijSingleton == + ASSUME NEW S + PROVE ExistsBijection(1..1,S) <=> \E s : S = {s} +<1>1. ASSUME NEW f \in Bijection(1..1, S) PROVE \E s : S = {s} + BY 1..1 = {1} DEF Bijection, Surjection +<1>2. ASSUME NEW s, S = {s} PROVE [i \in 1..1 |-> s] \in Bijection(1..1, S) + BY <1>2 DEF Bijection, Injection, IsInjective, Surjection +<1>. QED BY <1>1, <1>2 DEF ExistsBijection + + +(***************************************************************************) +(* `. .' *) +(* *) +(* If there exists a bijection from 1..m to S (for some m \in Nat), then *) +(* there exists a bijection from 1..n to T (for some n \in Nat), where T *) +(* is a subset of S. Furthermore n \leq m. *) +(* *) +(* `. .' *) +(***************************************************************************) +THEOREM Fun_NatBijSubset == + ASSUME NEW S, NEW m \in Nat, ExistsBijection(1..m,S), + NEW T \in SUBSET S + PROVE \E n \in Nat : ExistsBijection(1..n,T) /\ n \leq m + +<1>1. CASE T = {} BY <1>1, Fun_NatBijEmpty +<1>2. CASE T # {} + <2>0. ExistsSurjection(1..m, S) BY Fun_ExistsBijEquiv + <2>1. ExistsSurjection(S, T) BY <1>2, Fun_ExistsSurjSubset + <2>2. ExistsSurjection(1..m, T) BY <2>0, <2>1, Fun_ExistsSurjTransitive + <2>. QED BY <2>2, Fun_NatSurjImpliesNatBij +<1> QED BY <1>1, <1>2 + + + + +(***************************************************************************) +(* `. .' *) +(* *) +(* If there exists a bijection from 1..m to S (for some m \in Nat), then *) +(* there exists a bijection from 1..(m+1) to S \cup {x}, where x \notin S. *) +(* *) +(* *) +(* `. .' *) +(***************************************************************************) +THEOREM Fun_NatBijAddElem == + ASSUME NEW S, NEW m \in Nat, ExistsBijection(1..m,S), + NEW x, x \notin S + PROVE ExistsBijection(1..(m+1), S \cup {x}) + +<1>1. PICK F \in Bijection(1..m, S) : TRUE BY DEF ExistsBijection +<1>2. F \in [1..m -> S] BY <1>1 DEF Bijection, Injection +<1>3. \A s \in S : \E i \in 1..m : F[i] = s BY <1>1 DEF Bijection, Surjection +<1>4. \A i,j \in 1..m : F[i] = F[j] => i = j BY <1>1 DEF Bijection, Injection, IsInjective + +<1>. DEFINE G == [i \in 1..m+1 |-> IF i <= m THEN F[i] ELSE x] +<1>10. G \in [1..m+1 -> S \cup {x}] BY SMT, <1>2 +<1>20. ASSUME NEW t \in S \cup {x} PROVE \E i \in 1..m+1 : G[i] = t + <2>1. CASE t \in S + BY <1>3, <2>1, 1..m \subseteq 1 .. m+1 + <2>2. CASE t = x + BY <2>2, m+1 \in 1 .. m+1 + <2>. QED BY <2>1, <2>2 +<1>30. ASSUME NEW i \in 1..m+1, NEW j \in 1..m+1, G[i] = G[j] PROVE i = j + BY <1>2, <1>4, <1>30 +<1>40. G \in Bijection(1..m+1, S \cup {x}) + BY <1>10, <1>20, <1>30, Zenon DEF Bijection, Injection, IsInjective, Surjection +<1>. QED BY <1>40, Zenon DEF ExistsBijection + + + + +(***************************************************************************) +(* `. .' *) +(* *) +(* If there exists a bijection from 1..m to S (for some m \in Nat), then *) +(* there exists a bijection from 1..(m-1) to S \ {x}, where x \in S. *) +(* *) +(* *) +(* `. .' *) +(***************************************************************************) +THEOREM Fun_NatBijSubElem == + ASSUME NEW S, NEW m \in Nat, ExistsBijection(1..m,S), + NEW x, x \in S + PROVE ExistsBijection(1..(m-1), S \ {x}) + +<1>1. PICK n \in Nat : ExistsBijection(1..n, S \ {x}) BY Fun_NatBijSubset, Zenon +<1>2. ExistsBijection(1..n+1, (S \ {x}) \cup {x}) BY <1>1, Fun_NatBijAddElem, Zenon +<1>3. ExistsBijection(1..n+1, S) BY <1>2, Zenon +<1>4. n = m-1 BY <1>3, Fun_NatBijSame +<1>. QED BY <1>1, <1>4 + +(***************************************************************************) +(* Folding a function for an empty set of indices yields the base value. *) +(***************************************************************************) +THEOREM FoldFunctionOnSetEmpty == + ASSUME NEW op(_,_), NEW base, NEW fun + PROVE FoldFunctionOnSet(op, base, fun, {}) = base +BY MapThenFoldSetEmpty, Zenon DEF FoldFunctionOnSet + +(***************************************************************************) +(* Folding a function for a non-empty set of indices corresponds to *) +(* applying the binary operator to f[i], for some i \in indices, and the *) +(* result of recursing for the set indices \ {i}. *) +(***************************************************************************) +THEOREM FoldFunctionOnSetNonempty == + ASSUME NEW op(_,_), NEW base, NEW fun, + NEW indices, indices # {}, IsFiniteSet(indices) + PROVE \E i \in indices : FoldFunctionOnSet(op, base, fun, indices) = + op(fun[i], FoldFunctionOnSet(op, base, fun, indices \ {i})) +<1>1. \A T : T # {} => (CHOOSE t \in T : TRUE) \in T + OBVIOUS +<1>. QED BY <1>1, MapThenFoldSetNonempty, Isa DEF FoldFunctionOnSet + +(***************************************************************************) +(* The type of folding a function corresponds to the type associated with *) +(* the binary operator that underlies the fold. *) +(***************************************************************************) +THEOREM FoldFunctionOnSetType == + ASSUME NEW Typ, NEW op(_,_), NEW base \in Typ, + \A t,u \in Typ : op(t,u) \in Typ, + NEW indices, IsFiniteSet(indices), NEW fun, + \A i \in indices : fun[i] \in Typ + PROVE FoldFunctionOnSet(op, base, fun, indices) \in Typ +<1>1. \A T : T # {} => (CHOOSE t \in T : TRUE) \in T + OBVIOUS +<1>. QED BY <1>1, MapThenFoldSetType, Isa DEF FoldFunctionOnSet + +(***************************************************************************) +(* Folding two functions that agree on every element of the set of indices *) +(* yields the same value. *) +(***************************************************************************) +THEOREM FoldFunctionOnSetEqual == + ASSUME NEW op(_,_), NEW base, NEW f, NEW g, + NEW indices, IsFiniteSet(indices), + \A i \in indices : f[i] = g[i] + PROVE FoldFunctionOnSet(op, base, f, indices) = + FoldFunctionOnSet(op, base, g, indices) +<1>1. \A T : T # {} => (CHOOSE t \in T : TRUE) \in T + OBVIOUS +<1>. QED BY <1>1, MapThenFoldSetEqual, Isa DEF FoldFunctionOnSet + +(***************************************************************************) +(* If the binary operator is associative and commutative, the result of *) +(* folding a function over a non-empty set corresponds to applying the *) +(* operator to an arbitrary element of the set and the result of folding *) +(* the function over the remainder of the set. *) +(***************************************************************************) +THEOREM FoldFunctionOnSetAC == + ASSUME NEW Typ, NEW op(_,_), NEW base \in Typ, + \A t,u \in Typ : op(t,u) \in Typ, + \A t,u \in Typ : op(t,u) = op(u,t), + \A t,u,v \in Typ : op(t, op(u,v)) = op(op(t,u),v), + NEW indices, IsFiniteSet(indices), NEW i \in indices, NEW fun, + \A j \in indices : fun[j] \in Typ + PROVE FoldFunctionOnSet(op, base, fun, indices) = + op(fun[i], FoldFunctionOnSet(op, base, fun, indices \ {i})) +<1>1. \A T : T # {} => (CHOOSE t \in T : TRUE) \in T + OBVIOUS +<1>. QED BY <1>1, MapThenFoldSetAC, Isa DEF FoldFunctionOnSet + +\* reformulation in terms of adding an index to the set +THEOREM FoldFunctionOnSetACAddIndex == + ASSUME NEW Typ, NEW op(_,_), NEW base \in Typ, + \A t,u \in Typ : op(t,u) \in Typ, + \A t,u \in Typ : op(t,u) = op(u,t), + \A t,u,v \in Typ : op(t, op(u,v)) = op(op(t,u),v), + NEW indices, IsFiniteSet(indices), NEW i, i \notin indices, + NEW fun, \A j \in indices \union {i} : fun[j] \in Typ + PROVE FoldFunctionOnSet(op, base, fun, indices \union {i}) = + op(fun[i], FoldFunctionOnSet(op, base, fun, indices)) +<1>1. \A T : T # {} => (CHOOSE t \in T : TRUE) \in T + OBVIOUS +<1>. QED BY <1>1, MapThenFoldSetACAddElement, Isa DEF FoldFunctionOnSet + +(*************************************************************************) +(* For an AC operator, folding an EXCEPT construction can be reduced to *) +(* folding the original function. *) +(*************************************************************************) +THEOREM FoldFunctionOnSetACExcept == + ASSUME NEW Typ, NEW op(_,_), NEW base \in Typ, + \A t,u \in Typ : op(t,u) \in Typ, + \A t,u \in Typ : op(t,u) = op(u,t), + \A t,u,v \in Typ : op(t, op(u,v)) = op(op(t,u),v), + NEW fun, NEW i, NEW y \in Typ, + NEW indices \in SUBSET (DOMAIN fun), IsFiniteSet(indices), + \A j \in indices : fun[j] \in Typ + PROVE FoldFunctionOnSet(op, base, [fun EXCEPT ![i] = y], indices) = + IF i \in indices + THEN op(y, FoldFunctionOnSet(op, base, fun, indices \ {i})) + ELSE FoldFunctionOnSet(op, base, fun, indices) +<1>. DEFINE g == [fun EXCEPT ![i] = y] +<1>1. \A j \in indices \ {i} : g[j] = fun[j] + OBVIOUS +<1>2. IsFiniteSet(indices \ {i}) + BY FS_RemoveElement +<1>3. CASE i \in indices + <2>1. \A j \in indices : g[j] \in Typ + BY <1>3 + <2>2. FoldFunctionOnSet(op, base, g, indices) = + op(g[i], FoldFunctionOnSet(op, base, g, indices \ {i})) + BY <1>3, <2>1, FoldFunctionOnSetAC, Isa + <2>. QED BY <1>1, <1>2, <1>3, <2>2, FoldFunctionOnSetEqual, Isa +<1>4. CASE i \notin indices + <2>. QED BY <1>1, <1>2, <1>4, indices = indices \ {i}, FoldFunctionOnSetEqual, Isa +<1>. QED BY <1>3, <1>4 + +(*************************************************************************) +(* For an AC operator `op` for which `base` is the neutral element, *) +(* folding a function commutes with set union, for disjoint sets. *) +(*************************************************************************) +THEOREM FoldFunctionOnSetDisjointUnion == + ASSUME NEW Typ, NEW op(_,_), NEW base \in Typ, + \A t,u \in Typ : op(t,u) \in Typ, + \A t,u \in Typ : op(t,u) = op(u,t), + \A t,u,v \in Typ : op(t, op(u,v)) = op(op(t,u),v), + \A t \in Typ : op(base, t) = t, + NEW S, IsFiniteSet(S), NEW T, IsFiniteSet(T), S \cap T = {}, + NEW fun, \A i \in S \union T : fun[i] \in Typ + PROVE FoldFunctionOnSet(op, base, fun, S \union T) = + op(FoldFunctionOnSet(op, base, fun, S), FoldFunctionOnSet(op, base, fun, T)) +<1>1. \A U : U # {} => (CHOOSE u \in U : TRUE) \in U + OBVIOUS +<1>. QED BY <1>1, MapThenFoldSetDisjointUnion, Isa DEF FoldFunctionOnSet + +(*************************************************************************) +(* Analogous theorems for FoldFunction. Note that the theorems about *) +(* adding an index and about disjoint union do not make sense here. *) +(*************************************************************************) +THEOREM FoldFunctionEmpty == + ASSUME NEW op(_,_), NEW base, NEW fun, DOMAIN fun = {} + PROVE FoldFunction(op, base, fun) = base +BY FoldFunctionOnSetEmpty, Zenon DEF FoldFunction + +THEOREM FoldFunctionNonempty == + ASSUME NEW op(_,_), NEW base, NEW fun, + DOMAIN fun # {}, IsFiniteSet(DOMAIN fun) + PROVE \E i \in DOMAIN fun : FoldFunction(op, base, fun) = + op(fun[i], FoldFunctionOnSet(op, base, fun, DOMAIN fun \ {i})) +BY FoldFunctionOnSetNonempty, Isa DEF FoldFunction + +THEOREM FoldFunctionType == + ASSUME NEW Typ, NEW op(_,_), NEW base \in Typ, + \A t,u \in Typ : op(t,u) \in Typ, + NEW fun, IsFiniteSet(DOMAIN fun), + \A i \in DOMAIN fun : fun[i] \in Typ + PROVE FoldFunction(op, base, fun) \in Typ +BY FoldFunctionOnSetType, Isa DEF FoldFunction + +THEOREM FoldFunctionAC == + ASSUME NEW Typ, NEW op(_,_), NEW base \in Typ, + \A t,u \in Typ : op(t,u) \in Typ, + \A t,u \in Typ : op(t,u) = op(u,t), + \A t,u,v \in Typ : op(t, op(u,v)) = op(op(t,u),v), + NEW fun, IsFiniteSet(DOMAIN fun), NEW i \in DOMAIN fun, + \A j \in DOMAIN fun : fun[j] \in Typ + PROVE FoldFunction(op, base, fun) = + op(fun[i], FoldFunctionOnSet(op, base, fun, (DOMAIN fun) \ {i})) +BY FoldFunctionOnSetAC, Isa DEF FoldFunction + +THEOREM FoldFunctionACExcept == + ASSUME NEW Typ, NEW op(_,_), NEW base \in Typ, + \A t,u \in Typ : op(t,u) \in Typ, + \A t,u \in Typ : op(t,u) = op(u,t), + \A t,u,v \in Typ : op(t, op(u,v)) = op(op(t,u),v), + NEW fun, NEW i, NEW y \in Typ, + IsFiniteSet(DOMAIN fun), + \A j \in DOMAIN fun : fun[j] \in Typ + PROVE FoldFunction(op, base, [fun EXCEPT ![i] = y]) = + IF i \in DOMAIN fun + THEN op(y, FoldFunctionOnSet(op, base, fun, (DOMAIN fun) \ {i})) + ELSE FoldFunction(op, base, fun) +BY FoldFunctionOnSetACExcept, Isa DEF FoldFunction + +(*************************************************************************) +(* Summing a function that returns natural numbers, resp. integers, *) +(* yields a natural number, resp. an integer. *) +(*************************************************************************) +LEMMA IntegersAC == + /\ 0 \in Int + /\ \A x,y \in Int : x+y \in Int + /\ \A x,y \in Int : x+y = y+x + /\ \A x,y,z \in Int : x + (y+z) = (x+y) + z + /\ \A x \in Int : 0 + x = x +OBVIOUS + +THEOREM SumFunctionOnSetNat == + ASSUME NEW fun, NEW indices, IsFiniteSet(indices), + \A i \in indices : fun[i] \in Nat + PROVE SumFunctionOnSet(fun, indices) \in Nat +<1>. /\ 0 \in Nat + /\ \A x,y \in Nat : x + y \in Nat + OBVIOUS +<1>. QED BY FoldFunctionOnSetType, IsaM("iprover") DEF SumFunctionOnSet + +THEOREM SumFunctionOnSetInt == + ASSUME NEW fun, NEW indices, IsFiniteSet(indices), + \A i \in indices : fun[i] \in Int + PROVE SumFunctionOnSet(fun, indices) \in Int +BY FoldFunctionOnSetType, IntegersAC, IsaM("iprover") DEF SumFunctionOnSet + +(*************************************************************************) +(* Summing two functions that agree on all relevant indices yields the *) +(* same result. *) +(*************************************************************************) +THEOREM SumFunctionOnSetEqual == + ASSUME NEW f, NEW g, NEW indices, IsFiniteSet(indices), + \A i \in indices : f[i] = g[i] + PROVE SumFunctionOnSet(f, indices) = SumFunctionOnSet(g, indices) +BY FoldFunctionOnSetEqual, Zenon DEF SumFunctionOnSet + +(*************************************************************************) +(* Summing a function over the empty set is 0. *) +(*************************************************************************) +THEOREM SumFunctionOnSetEmpty == + ASSUME NEW fun + PROVE SumFunctionOnSet(fun, {}) = 0 +BY FoldFunctionOnSetEmpty, Zenon DEF SumFunctionOnSet + +(*************************************************************************) +(* Summing a function over a non-empty set corresponds to the sum of *) +(* element of the set and the sum of the function over the remainder. *) +(*************************************************************************) +THEOREM SumFunctionOnSetNonempty == + ASSUME NEW fun, NEW indices, IsFiniteSet(indices), NEW i \in indices, + \A j \in indices : fun[j] \in Int + PROVE SumFunctionOnSet(fun, indices) = + fun[i] + SumFunctionOnSet(fun, indices \ {i}) + BY FoldFunctionOnSetAC, IntegersAC, IsaM("iprover") DEF SumFunctionOnSet + +\* reformulation in terms of adding an index +THEOREM SumFunctionOnSetAddIndex == + ASSUME NEW fun, NEW indices, IsFiniteSet(indices), + NEW i, i \notin indices, + \A j \in indices \union {i} : fun[j] \in Int + PROVE SumFunctionOnSet(fun, indices \union {i}) = + fun[i] + SumFunctionOnSet(fun, indices) +BY FoldFunctionOnSetACAddIndex, IntegersAC, IsaM("iprover") DEF SumFunctionOnSet + +\* corresponding lemma for removing an index +THEOREM SumFunctionOnSetRemoveIndex == + ASSUME NEW fun, NEW indices, IsFiniteSet(indices), NEW i \in indices, + \A j \in indices : fun[j] \in Int + PROVE SumFunctionOnSet(fun, indices \ {i}) = + SumFunctionOnSet(fun, indices) - fun[i] +<1>. IsFiniteSet(indices \ {i}) + BY FS_RemoveElement +<1>. QED BY SumFunctionOnSetNonempty, SumFunctionOnSetInt + +(*************************************************************************) +(* Reduce the sum of an EXCEPT to the sum of the original function. *) +(*************************************************************************) +THEOREM SumFunctionOnSetExcept == + ASSUME NEW fun, NEW i, NEW y \in Int, + NEW indices \in SUBSET (DOMAIN fun), IsFiniteSet(indices), + \A j \in indices : fun[j] \in Int + PROVE SumFunctionOnSet([fun EXCEPT ![i] = y], indices) = + IF i \in indices + THEN SumFunctionOnSet(fun, indices) + y - fun[i] + ELSE SumFunctionOnSet(fun, indices) +<1>1. SumFunctionOnSet([fun EXCEPT ![i] = y], indices) = + IF i \in indices + THEN y + SumFunctionOnSet(fun, indices \ {i}) + ELSE SumFunctionOnSet(fun, indices) + BY FoldFunctionOnSetACExcept, IntegersAC, IsaM("iprover") DEF SumFunctionOnSet +<1>2. i \in indices => + SumFunctionOnSet(fun, indices \ {i}) = SumFunctionOnSet(fun, indices) - fun[i] + BY SumFunctionOnSetRemoveIndex +<1>3. SumFunctionOnSet(fun, indices) \in Int + BY SumFunctionOnSetInt +<1>. QED BY <1>1, <1>2, <1>3 + +(*************************************************************************) +(* Summing a function distributes over disjoint union. *) +(*************************************************************************) +THEOREM SumFunctionOnSetDisjointUnion == + ASSUME NEW S, IsFiniteSet(S), + NEW T, IsFiniteSet(T), S \cap T = {}, + NEW fun, \A x \in S \union T : fun[x] \in Int + PROVE SumFunctionOnSet(fun, S \union T) = + SumFunctionOnSet(fun, S) + SumFunctionOnSet(fun, T) +BY FoldFunctionOnSetDisjointUnion, IntegersAC, IsaM("iprover") DEF SumFunctionOnSet + +(*************************************************************************) +(* Summing a Nat-valued function is monotonic in the subset relation. *) +(*************************************************************************) +THEOREM SumFunctionNatOnSubset == + ASSUME NEW S, IsFiniteSet(S), NEW T \in SUBSET S, + NEW fun, \A s \in S : fun[s] \in Nat + PROVE SumFunctionOnSet(fun, T) <= SumFunctionOnSet(fun, S) +<1>. DEFINE U == S \ T +<1>1. /\ IsFiniteSet(T) + /\ IsFiniteSet(U) + /\ T \cap U = {} + /\ S = T \union U + /\ \A x \in T \union U : fun[x] \in Int + BY FS_Subset +<1>2. SumFunctionOnSet(fun, S) = SumFunctionOnSet(fun, T) + SumFunctionOnSet(fun, U) + BY <1>1, SumFunctionOnSetDisjointUnion +<1>3. /\ SumFunctionOnSet(fun, T) \in Nat + /\ SumFunctionOnSet(fun, U) \in Nat + BY <1>1, SumFunctionOnSetNat +<1>. QED BY <1>2, <1>3 + +(*************************************************************************) +(* The sum of a Nat-valued function is zero iff all relevant function *) +(* values are zero. *) +(*************************************************************************) +THEOREM SumFunctionOnSetZero == + ASSUME NEW S, IsFiniteSet(S), + NEW fun, \A x \in S : fun[x] \in Nat + PROVE SumFunctionOnSet(fun, S) = 0 <=> \A x \in S : fun[x] = 0 +<1>. DEFINE P(T) == SumFunctionOnSet(fun, T) = 0 <=> \A x \in T : fun[x] = 0 +<1>1. P({}) + BY SumFunctionOnSetEmpty +<1>2. ASSUME NEW T \in SUBSET S, IsFiniteSet(T), P(T), NEW x \in S \ T + PROVE P(T \union {x}) + <2>1. SumFunctionOnSet(fun, T \union {x}) = fun[x] + SumFunctionOnSet(fun, T) + BY <1>2, SumFunctionOnSetAddIndex + <2>2. SumFunctionOnSet(fun, T) \in Nat + BY <1>2, SumFunctionOnSetNat + <2>. QED BY <1>2, <2>1, <2>2 +<1>. QED + <2>. HIDE DEF P + <2>. P(S) BY <1>1, <1>2, FS_Induction, IsaM("iprover") + <2>. QED BY DEF P + +(*************************************************************************) +(* Summing a function is monotonic in the function argument. *) +(*************************************************************************) +THEOREM SumFunctionOnSetMonotonic == + ASSUME NEW S, IsFiniteSet(S), + NEW f, \A s \in S : f[s] \in Int, + NEW g, \A s \in S : g[s] \in Int, + \A s \in S : f[s] <= g[s] + PROVE SumFunctionOnSet(f, S) <= SumFunctionOnSet(g, S) +<1>. DEFINE P(T) == SumFunctionOnSet(f, T) <= SumFunctionOnSet(g, T) +<1>1. P({}) + BY SumFunctionOnSetEmpty +<1>2. ASSUME NEW T \in SUBSET S, IsFiniteSet(T), P(T), NEW x \in S \ T + PROVE P(T \union {x}) + <2>1. /\ SumFunctionOnSet(f, T \union {x}) = f[x] + SumFunctionOnSet(f, T) + /\ SumFunctionOnSet(g, T \union {x}) = g[x] + SumFunctionOnSet(g, T) + BY <1>2, SumFunctionOnSetAddIndex + <2>2. /\ SumFunctionOnSet(f, T) \in Int + /\ SumFunctionOnSet(g, T) \in Int + BY <1>2, SumFunctionOnSetInt + <2>. QED BY <1>2, <2>1, <2>2 +<1>. QED + <2>. HIDE DEF P + <2>. P(S) BY <1>1, <1>2, FS_Induction, IsaM("iprover") + <2>. QED BY DEF P + +(*************************************************************************) +(* The sum over function f is strictly smaller than the sum over g if *) +(* f[x] <= g[x] for all x \in S and f[x] < g[s] holds for at least some *) +(* element s \in S. *) +(*************************************************************************) +THEOREM SumFunctionOnSetStrictlyMonotonic == + ASSUME NEW S, IsFiniteSet(S), + NEW f, \A s \in S : f[s] \in Int, + NEW g, \A s \in S : g[s] \in Int, + \A x \in S : f[x] <= g[x], + NEW s \in S, f[s] < g[s] + PROVE SumFunctionOnSet(f, S) < SumFunctionOnSet(g, S) +<1>1. /\ SumFunctionOnSet(f, S) = f[s] + SumFunctionOnSet(f, S \ {s}) + /\ SumFunctionOnSet(g, S) = g[s] + SumFunctionOnSet(g, S \ {s}) + BY SumFunctionOnSetNonempty +<1>2. IsFiniteSet(S \ {s}) + BY FS_RemoveElement +<1>3. SumFunctionOnSet(f, S \ {s}) <= SumFunctionOnSet(g, S \ {s}) + BY <1>2, SumFunctionOnSetMonotonic +<1>4. /\ SumFunctionOnSet(f, S \ {s}) \in Int + /\ SumFunctionOnSet(g, S \ {s}) \in Int + BY <1>2, SumFunctionOnSetInt +<1>. QED BY <1>1, <1>3, <1>4 + +(*************************************************************************) +(* Similar theorems for SumFunction. *) +(*************************************************************************) +THEOREM SumFunctionNat == + ASSUME NEW fun, IsFiniteSet(DOMAIN fun), + \A x \in DOMAIN fun : fun[x] \in Nat + PROVE SumFunction(fun) \in Nat +BY SumFunctionOnSetNat DEF SumFunction + +THEOREM SumFunctionInt == + ASSUME NEW fun, IsFiniteSet(DOMAIN fun), + \A x \in DOMAIN fun : fun[x] \in Int + PROVE SumFunction(fun) \in Int +BY SumFunctionOnSetInt DEF SumFunction + +THEOREM SumFunctionEmpty == + ASSUME NEW fun, DOMAIN fun = {} + PROVE SumFunction(fun) = 0 +BY SumFunctionOnSetEmpty DEF SumFunction + +THEOREM SumFunctionNonempty == + ASSUME NEW fun, IsFiniteSet(DOMAIN fun), NEW x \in DOMAIN fun, + \A i \in DOMAIN fun : fun[i] \in Int + PROVE SumFunction(fun) = fun[x] + SumFunctionOnSet(fun, (DOMAIN fun) \ {x}) +BY SumFunctionOnSetNonempty DEF SumFunction + +THEOREM SumFunctionExcept == + ASSUME NEW fun, NEW i, NEW y \in Int, IsFiniteSet(DOMAIN fun), + \A x \in DOMAIN fun : fun[x] \in Int + PROVE SumFunction([fun EXCEPT ![i] = y]) = + IF i \in DOMAIN fun + THEN SumFunction(fun) + y - fun[i] + ELSE SumFunction(fun) +BY SumFunctionOnSetExcept DEF SumFunction + +THEOREM SumFunctionZero == + ASSUME NEW fun, IsFiniteSet(DOMAIN fun), + \A x \in DOMAIN fun : fun[x] \in Nat + PROVE SumFunction(fun) = 0 <=> \A x \in DOMAIN fun : fun[x] = 0 +BY SumFunctionOnSetZero DEF SumFunction + +THEOREM SumFunctionMonotonic == + ASSUME NEW f, IsFiniteSet(DOMAIN f), NEW g, DOMAIN g = DOMAIN f, + \A x \in DOMAIN f : f[x] \in Int, + \A x \in DOMAIN f : g[x] \in Int, + \A x \in DOMAIN f : f[x] <= g[x] + PROVE SumFunction(f) <= SumFunction(g) +BY SumFunctionOnSetMonotonic DEF SumFunction + +THEOREM SumFunctionStrictlyMonotonic == + ASSUME NEW f, IsFiniteSet(DOMAIN f), NEW g, DOMAIN g = DOMAIN f, + \A x \in DOMAIN f : f[x] \in Int, + \A x \in DOMAIN f : g[x] \in Int, + \A x \in DOMAIN f : f[x] <= g[x], + NEW s \in DOMAIN f, f[s] < g[s] + PROVE SumFunction(f) < SumFunction(g) +BY SumFunctionOnSetStrictlyMonotonic DEF SumFunction + +============================================================================= +\* Created Thu Apr 11 10:36:10 PDT 2013 by tomr diff --git a/modules/Functions.tla b/modules/Functions.tla index 1128c80..f80d28d 100644 --- a/modules/Functions.tla +++ b/modules/Functions.tla @@ -6,7 +6,7 @@ (* \vspace{12pt}}^' *) (***************************************************************************) -LOCAL INSTANCE Folds +EXTENDS Integers, Folds (***************************************************************************) (* Restriction of a function to a set (should be a subset of the domain). *) @@ -137,40 +137,41 @@ ExistsBijection(S,T) == Bijection(S,T) # {} -------------------------------------------------------------------------------- (***************************************************************************) -(* Applies the binary function op on all elements of fun in arbitrary *) -(* order starting with op(f[k], base). The resulting function is: *) +(* Applies the binary operator op on the elements f[i] for i \in indices, *) +(* a subset of DOMAIN f, in an unspecified order, starting from value *) +(* base. The result is *) (* op(f[i],op(f[j], ..., op(f[k],base) ...)) *) +(* where i,j,k range over the sets indices. *) (* *) -(* op must be associative and commutative, because we can not assume a *) +(* op should be associative and commutative, because we can not assume a *) (* particular ordering of i, j, and k *) (* *) (* Example: *) +(* FoldFunctionOnSet(LAMBDA x,y: {x} \cup y, {}, <<1,2>>, {}) = {} *) +(***************************************************************************) +FoldFunctionOnSet(op(_,_), base, fun, indices) == + MapThenFoldSet(op, base, LAMBDA i : fun[i], LAMBDA s: CHOOSE x \in s : TRUE, indices) + +(***************************************************************************) +(* Special case of the above where indices = DOMAIN fun. In other words, *) +(* the values f[i] for all i \in DOMAIN fun, are combined using the binary *) +(* operator op, in an unspecified order. *) +(* *) +(* Example: *) (* FoldFunction(LAMBDA x,y: {x} \cup y, {}, <<1,2,1>>) = {1,2} *) (***************************************************************************) FoldFunction(op(_,_), base, fun) == - MapThenFoldSet(op, base, LAMBDA i : fun[i], LAMBDA s: CHOOSE x \in s : TRUE, DOMAIN fun) - + FoldFunctionOnSet(op, base, fun, DOMAIN fun) (***************************************************************************) -(* Applies the binary function op on the given indices of fun in arbitrary *) -(* order starting with op(f[k], base). The resulting function is: *) -(* op(f[i],op(f[j], ..., op(f[k],base) ...)) *) -(* *) -(* op must be associative and commutative, because we can not assume a *) -(* particular ordering of i, j, and k *) -(* *) -(* indices must be a subset of DOMAIN(fun) *) +(* Sum the values f[i] for i \in indices, a subset of DOMAIN f. *) (* *) (* Example: *) -(* FoldFunctionOnSet(LAMBDA x,y: {x} \cup y, {}, <<1,2>>, {}) = {} *) +(* SumFunctionOnSet(<<4,5,6>>, {1,2}) = 9 *) +(* SumFunction(<<4,5,6>>) = 15 *) (***************************************************************************) -FoldFunctionOnSet(op(_,_), base, fun, indices) == - MapThenFoldSet(op, base, LAMBDA i : fun[i], LAMBDA s: CHOOSE x \in s : TRUE, indices) +SumFunctionOnSet(fun, indices) == FoldFunctionOnSet(+, 0, fun, indices) +SumFunction(fun) == SumFunctionOnSet(fun, DOMAIN fun) ============================================================================= -\* Modification History -\* Last modified Tue Nov 01 08:46:11 CET 2022 by merz -\* Last modified Mon Apr 05 03:25:53 CEST 2021 by marty -\* Last modified Wed Jun 05 12:14:19 CEST 2013 by bhargav -\* Last modified Fri May 03 12:55:35 PDT 2013 by tomr \* Created Thu Apr 11 10:30:48 PDT 2013 by tomr diff --git a/modules/SequencesExt.tla b/modules/SequencesExt.tla index f8b6e2f..40ee14a 100644 --- a/modules/SequencesExt.tla +++ b/modules/SequencesExt.tla @@ -1,10 +1,13 @@ ---------------------------- MODULE SequencesExt ---------------------------- -LOCAL INSTANCE Sequences -LOCAL INSTANCE Naturals -LOCAL INSTANCE FiniteSets -LOCAL INSTANCE FiniteSetsExt -LOCAL INSTANCE Functions -LOCAL INSTANCE Folds +EXTENDS Sequences, Naturals, FiniteSets, FiniteSetsExt, Folds, Functions +\* TLAPM does not play well with LOCAL INSTANCE, reinstate the following +\* when that issue is fixed. +\* LOCAL INSTANCE Sequences +\* LOCAL INSTANCE Naturals +\* LOCAL INSTANCE FiniteSets +\* LOCAL INSTANCE FiniteSetsExt +\* LOCAL INSTANCE Folds +\* LOCAL INSTANCE Functions LOCAL INSTANCE TLC (*************************************************************************) (* Imports the definitions from the modules, but doesn't export them. *) @@ -297,11 +300,11 @@ SeqMod(a, b) == (***************************************************************************) -(* An alias of FoldFunction that op on all elements of seq an arbitrary *) -(* order. The resulting function is: *) -(* op(f[i],op(f[j], ..., op(f[k],base) ...)) *) +(* An alias of FoldFunction that combines all elements of seq using op, *) +(* in an unspecified order. The result is *) +(* op(seq[i],op(seq[j], ..., op(seq[k],base) ...)) *) (* *) -(* op must be associative and commutative, because we can not assume a *) +(* op should be associative and commutative, because we can not assume a *) (* particular ordering of i, j, and k *) (* *) (* Example: *) diff --git a/modules/SequencesExtTheorems.tla b/modules/SequencesExtTheorems.tla new file mode 100644 index 0000000..ef2baaa --- /dev/null +++ b/modules/SequencesExtTheorems.tla @@ -0,0 +1,521 @@ +----------------------- MODULE SequencesExtTheorems ------------------------ +(**************************************************************************) +(* This module contains theorems about the operators on sequences defined *) +(* in module SequencesExt. *) +(* The proofs are given in module SequencesExtTheorems_proofs. *) +(**************************************************************************) +EXTENDS Sequences, SequencesExt, Functions, Integers, WellFoundedInduction + +(***************************************************************************) +(* Theorems about Cons. *) +(* Cons(elt, seq) == <> \o seq *) +(***************************************************************************) + +THEOREM ConsProperties == + ASSUME NEW S, NEW seq \in Seq(S), NEW elt \in S + PROVE /\ Cons(elt, seq) \in Seq(S) + /\ Cons(elt, seq) # <<>> + /\ Len(Cons(elt, seq)) = Len(seq)+1 + /\ Head(Cons(elt, seq)) = elt + /\ Tail(Cons(elt, seq)) = seq + /\ Cons(elt, seq)[1] = elt + /\ \A i \in 1 .. Len(seq) : Cons(elt, seq)[i+1] = seq[i] + /\ \A i \in 2 .. Len(seq)+1 : Cons(elt, seq)[i] = seq[i-1] + +THEOREM ConsEmpty == + \A x : Cons(x, << >>) = << x >> + +THEOREM ConsHeadTail == + ASSUME NEW S, NEW seq \in Seq(S), seq # << >> + PROVE Cons(Head(seq), Tail(seq)) = seq + +THEOREM ConsAppend == + ASSUME NEW S, NEW seq \in Seq(S), NEW x \in S, NEW y \in S + PROVE Cons(x, Append(seq, y)) = Append(Cons(x,seq), y) + +THEOREM ConsInjective == + ASSUME NEW S, NEW e \in S, NEW s \in Seq(S), NEW f \in S, NEW t \in Seq(S) + PROVE Cons(e,s) = Cons(f,t) <=> e = f /\ s = t + +THEOREM SequencesInductionCons == + ASSUME NEW P(_), NEW S, + P(<< >>), + \A s \in Seq(S), e \in S : P(s) => P(Cons(e,s)) + PROVE \A seq \in Seq(S) : P(seq) + +(***************************************************************************) +(* Theorems about InsertAt and RemoveAt. *) +(* InsertAt(seq,i,elt) == *) +(* SubSeq(seq, 1, i-1) \o <> \o SubSeq(seq, i, Len(seq)) *) +(* RemoveAt(seq, i) == SubSeq(seq, 1, i-1) \o SubSeq(seq, i+1, Len(seq)) *) +(***************************************************************************) + +THEOREM InsertAtProperties == + ASSUME NEW S, NEW seq \in Seq(S), NEW i \in 1 .. Len(seq)+1, NEW elt \in S + PROVE /\ InsertAt(seq,i,elt) \in Seq(S) + /\ Len(InsertAt(seq,i,elt)) = Len(seq)+1 + /\ \A j \in 1 .. Len(seq)+1 : InsertAt(seq,i,elt)[j] = + IF j> THEN 0 ELSE Len(seq)-1 + /\ \A i \in 1 .. Len(seq)-1 : Front(seq)[i] = seq[i] + +THEOREM FrontOfEmpty == Front(<< >>) = << >> + +THEOREM LastProperties == + ASSUME NEW S, NEW seq \in Seq(S), seq # << >> + PROVE /\ Last(seq) \in S + /\ Append(Front(seq), Last(seq)) = seq + +THEOREM FrontLastOfSubSeq == + ASSUME NEW S, NEW seq \in Seq(S), + NEW m \in 1 .. Len(seq), NEW n \in m .. Len(seq) + PROVE /\ Front(SubSeq(seq,m,n)) = SubSeq(seq, m, n-1) + /\ Last(SubSeq(seq,m,n)) = seq[n] + +THEOREM FrontLastAppend == + ASSUME NEW S, NEW seq \in Seq(S), NEW e \in S + PROVE /\ Front(Append(seq, e)) = seq + /\ Last(Append(seq, e)) = e + +LEMMA FrontInjectiveSeq == + ASSUME NEW S, NEW seq \in Seq(S), IsInjective(seq), seq # << >> + PROVE /\ IsInjective(Front(seq)) + /\ Range(Front(seq)) = Range(seq) \ {Last(seq)} + +THEOREM SequencesInductionFront == + ASSUME NEW S, NEW P(_), + P(<< >>), + \A s \in Seq(S) : (s # << >>) /\ P(Front(s)) => P(s) + PROVE \A s \in Seq(S) : P(s) + +(***************************************************************************) +(* Theorems about Reverse. *) +(* Reverse(seq) == [j \in 1 .. Len(seq) |-> seq[Len(seq)-j+1] ] *) +(***************************************************************************) + +THEOREM ReverseProperties == + ASSUME NEW S, NEW seq \in Seq(S) + PROVE /\ Reverse(seq) \in Seq(S) + /\ Len(Reverse(seq)) = Len(seq) + /\ Reverse(Reverse(seq)) = seq + +THEOREM ReverseEmpty == Reverse(<< >>) = << >> + +THEOREM ReverseEqual == + ASSUME NEW S, NEW s \in Seq(S), NEW t \in Seq(S), Reverse(s) = Reverse(t) + PROVE s = t + +THEOREM ReverseEmptyIffEmpty == + ASSUME NEW S, NEW seq \in Seq(S), Reverse(seq) = <<>> + PROVE seq = <<>> + +THEOREM ReverseConcat == + ASSUME NEW S, NEW s1 \in Seq(S), NEW s2 \in Seq(S) + PROVE Reverse(s1 \o s2) = Reverse(s2) \o Reverse(s1) + +THEOREM ReverseAppend == + ASSUME NEW S, NEW seq \in Seq(S), NEW e \in S + PROVE Reverse(Append(seq,e)) = Cons(e, Reverse(seq)) + +THEOREM ReverseCons == + ASSUME NEW S, NEW seq \in Seq(S), NEW e \in S + PROVE Reverse(Cons(e,seq)) = Append(Reverse(seq), e) + +THEOREM ReverseSingleton == \A x : Reverse(<< x >>) = << x >> + +THEOREM ReverseSubSeq == + ASSUME NEW S, NEW seq \in Seq(S), + NEW m \in 1..Len(seq), NEW n \in 0..Len(seq) + PROVE Reverse(SubSeq(seq, m , n)) = SubSeq(Reverse(seq), Len(seq)-n+1, Len(seq)-m+1) + +THEOREM ReversePalindrome == + ASSUME NEW S, NEW seq \in Seq(S), + Reverse(seq) = seq + PROVE Reverse(seq \o seq) = seq \o seq + +THEOREM LastEqualsHeadReverse == + ASSUME NEW S, NEW seq \in Seq(S), seq # << >> + PROVE Last(seq) = Head(Reverse(seq)) + +THEOREM ReverseFrontEqualsTailReverse == + ASSUME NEW S, NEW seq \in Seq(S), seq # << >> + PROVE Reverse(Front(seq)) = Tail(Reverse(seq)) + +(* The range of the reverse sequence equals that of the original one. *) +THEOREM RangeReverse == + ASSUME NEW S, NEW seq \in Seq(S) + PROVE /\ DOMAIN Reverse(seq) = DOMAIN seq + /\ Range(Reverse(seq)) = Range(seq) + +(***************************************************************************) +(* The following theorem gives three alternative characterizations of *) +(* prefixes. It also implies that any prefix of a sequence t is at most *) +(* as long as t. *) +(***************************************************************************) +THEOREM IsPrefixProperties == + ASSUME NEW S, NEW s \in Seq(S), NEW t \in Seq(S) + PROVE /\ IsPrefix(s,t) <=> \E u \in Seq(S) : t = s \o u + /\ IsPrefix(s,t) <=> Len(s) <= Len(t) /\ s = SubSeq(t, 1, Len(s)) + /\ IsPrefix(s,t) <=> Len(s) <= Len(t) /\ s = Restrict(t, DOMAIN s) + +THEOREM IsStrictPrefixProperties == + ASSUME NEW S, NEW s \in Seq(S), NEW t \in Seq(S) + PROVE /\ IsStrictPrefix(s,t) <=> \E u \in Seq(S) : u # << >> /\ t = s \o u + /\ IsStrictPrefix(s,t) <=> Len(s) < Len(t) /\ s = SubSeq(t, 1, Len(s)) + /\ IsStrictPrefix(s,t) <=> Len(s) < Len(t) /\ s = Restrict(t, DOMAIN s) + /\ IsStrictPrefix(s,t) <=> IsPrefix(s,t) /\ Len(s) < Len(t) + +THEOREM IsPrefixElts == + ASSUME NEW S, NEW s \in Seq(S), NEW t \in Seq(S), NEW i \in 1 .. Len(s), + IsPrefix(s,t) + PROVE s[i] = t[i] + +THEOREM EmptyIsPrefix == + ASSUME NEW S, NEW s \in Seq(S) + PROVE /\ IsPrefix(<<>>, s) + /\ IsPrefix(s, <<>>) <=> s = <<>> + /\ IsStrictPrefix(<<>>, s) <=> s # <<>> + /\ ~ IsStrictPrefix(s, <<>>) + +THEOREM IsPrefixConcat == + ASSUME NEW S, NEW s \in Seq(S), NEW t \in Seq(S) + PROVE IsPrefix(s, s \o t) + +THEOREM IsStrictPrefixAppend == + ASSUME NEW S, NEW s \in Seq(S), NEW e \in S + PROVE IsStrictPrefix(s, Append(s,e)) + +THEOREM FrontIsPrefix == + ASSUME NEW S, NEW s \in Seq(S) + PROVE /\ IsPrefix(Front(s), s) + /\ s # <<>> => IsStrictPrefix(Front(s), s) + +(***************************************************************************) +(* (Strict) prefixes on sequences form a (strict) partial order, and *) +(* the strict ordering is well-founded. *) +(***************************************************************************) +THEOREM IsPrefixPartialOrder == + ASSUME NEW S + PROVE /\ \A s \in Seq(S) : IsPrefix(s,s) + /\ \A s,t \in Seq(S) : IsPrefix(s,t) /\ IsPrefix(t,s) => s = t + /\ \A s,t,u \in Seq(S) : IsPrefix(s,t) /\ IsPrefix(t,u) => IsPrefix(s,u) + +THEOREM ConcatIsPrefix == + ASSUME NEW S, NEW s \in Seq(S), NEW t \in Seq(S), NEW u \in Seq(S), + IsPrefix(s \o t, u) + PROVE IsPrefix(s, u) + +THEOREM ConcatIsPrefixCancel == + ASSUME NEW S, NEW s \in Seq(S), NEW t \in Seq(S), NEW u \in Seq(S) + PROVE /\ IsPrefix(s \o t, s \o u) <=> IsPrefix(t, u) + +THEOREM ConsIsPrefixCancel == + ASSUME NEW S, NEW e \in S, NEW s \in Seq(S), NEW t \in Seq(S) + PROVE IsPrefix(Cons(e,s), Cons(e,t)) <=> IsPrefix(s,t) + +THEOREM ConsIsPrefix == + ASSUME NEW S, NEW e \in S, NEW s \in Seq(S), NEW u \in Seq(S), + IsPrefix(Cons(e,s), u) + PROVE /\ e = Head(u) + /\ IsPrefix(s, Tail(u)) + +THEOREM IsStrictPrefixStrictPartialOrder == + ASSUME NEW S + PROVE /\ \A s \in Seq(S) : ~ IsStrictPrefix(s,s) + /\ \A s,t \in Seq(S) : IsStrictPrefix(s,t) => ~ IsStrictPrefix(t,s) + /\ \A s,t,u \in Seq(S) : IsStrictPrefix(s,t) /\ IsStrictPrefix(t,u) => IsStrictPrefix(s,u) + +THEOREM IsStrictPrefixWellFounded == + ASSUME NEW S + PROVE IsWellFoundedOn(OpToRel(IsStrictPrefix, Seq(S)), Seq(S)) + +THEOREM SeqStrictPrefixInduction == + ASSUME NEW P(_), NEW S, + \A t \in Seq(S) : (\A s \in Seq(S) : IsStrictPrefix(s,t) => P(s)) => P(t) + PROVE \A s \in Seq(S) : P(s) + +(***************************************************************************) +(* Similar theorems about suffixes. *) +(***************************************************************************) + +THEOREM IsSuffixProperties == + ASSUME NEW S, NEW s \in Seq(S), NEW t \in Seq(S) + PROVE /\ IsSuffix(s,t) <=> \E u \in Seq(S) : t = u \o s + /\ IsSuffix(s,t) <=> Len(s) <= Len(t) /\ s = SubSeq(t, Len(t)-Len(s)+1, Len(t)) + +THEOREM IsStrictSuffixProperties == + ASSUME NEW S, NEW s \in Seq(S), NEW t \in Seq(S) + PROVE /\ IsStrictSuffix(s,t) <=> \E u \in Seq(S) : u # << >> /\ t = u \o s + /\ IsStrictSuffix(s,t) <=> Len(s) < Len(t) /\ IsSuffix(s,t) + /\ IsStrictSuffix(s,t) <=> Len(s) < Len(t) /\ s = SubSeq(t, Len(t)-Len(s)+1, Len(t)) + /\ IsStrictSuffix(s,t) <=> IsStrictPrefix(Reverse(s), Reverse(t)) + +THEOREM IsSuffixElts == + ASSUME NEW S, NEW s \in Seq(S), NEW t \in Seq(S), NEW i \in 1 .. Len(s), + IsSuffix(s,t) + PROVE s[i] = t[Len(t) - Len(s) + i] + +THEOREM EmptyIsSuffix == + ASSUME NEW S, NEW s \in Seq(S) + PROVE /\ IsSuffix(<<>>, s) + /\ IsSuffix(s, <<>>) <=> s = <<>> + /\ IsStrictSuffix(<<>>, s) <=> s # <<>> + /\ ~ IsStrictSuffix(s, <<>>) + +THEOREM IsSuffixConcat == + ASSUME NEW S, NEW s \in Seq(S), NEW t \in Seq(S) + PROVE IsSuffix(s, t \o s) + +THEOREM IsStrictSuffixCons == + ASSUME NEW S, NEW s \in Seq(S), NEW e \in S + PROVE IsStrictSuffix(s, Cons(e,s)) + +THEOREM TailIsSuffix == + ASSUME NEW S, NEW s \in Seq(S), s # << >> + PROVE IsStrictSuffix(Tail(s), s) + +THEOREM IsSuffixPartialOrder == + ASSUME NEW S + PROVE /\ \A s \in Seq(S) : IsSuffix(s,s) + /\ \A s,t \in Seq(S) : IsSuffix(s,t) /\ IsSuffix(t,s) => s = t + /\ \A s,t,u \in Seq(S) : IsSuffix(s,t) /\ IsSuffix(t,u) => IsSuffix(s,u) + +THEOREM ConcatIsSuffix == + ASSUME NEW S, NEW s \in Seq(S), NEW t \in Seq(S), NEW u \in Seq(S), + IsSuffix(s \o t, u) + PROVE IsSuffix(t, u) + +THEOREM ConcatIsSuffixCancel == + ASSUME NEW S, NEW s \in Seq(S), NEW t \in Seq(S), NEW u \in Seq(S) + PROVE IsSuffix(s \o t, u \o t) <=> IsSuffix(s, u) + +THEOREM AppendIsSuffixCancel == + ASSUME NEW S, NEW e \in S, NEW s \in Seq(S), NEW t \in Seq(S) + PROVE IsSuffix(Append(s,e), Append(t,e)) <=> IsSuffix(s,t) + +THEOREM AppendIsSuffix == + ASSUME NEW S, NEW e \in S, NEW s \in Seq(S), NEW u \in Seq(S), + IsSuffix(Append(s,e), u) + PROVE /\ e = Last(u) + /\ IsSuffix(s, Front(u)) + +THEOREM IsStrictSuffixStrictPartialOrder == + ASSUME NEW S + PROVE /\ \A s \in Seq(S) : ~ IsStrictSuffix(s,s) + /\ \A s,t \in Seq(S) : IsStrictSuffix(s,t) => ~ IsStrictSuffix(t,s) + /\ \A s,t,u \in Seq(S) : IsStrictSuffix(s,t) /\ IsStrictSuffix(t,u) => IsStrictSuffix(s,u) + +THEOREM IsStrictSuffixWellFounded == + ASSUME NEW S + PROVE IsWellFoundedOn(OpToRel(IsStrictSuffix, Seq(S)), Seq(S)) + +THEOREM SeqStrictSuffixInduction == + ASSUME NEW P(_), NEW S, + \A t \in Seq(S) : (\A s \in Seq(S) : IsStrictSuffix(s,t) => P(s)) => P(t) + PROVE \A s \in Seq(S) : P(s) + +(***************************************************************************) +(* Since the (strict) prefix and suffix orderings on sequences are *) +(* well-founded, they can be used for defining recursive functions. *) +(* The operators OpDefinesFcn, WFInductiveDefines, and WFInductiveUnique *) +(* are defined in module WellFoundedInduction. *) +(***************************************************************************) + +StrictPrefixesDetermineDef(S, Def(_,_)) == + \A g,h : \A seq \in Seq(S) : + (\A pre \in Seq(S) : IsStrictPrefix(pre,seq) => g[pre] = h[pre]) + => Def(g, seq) = Def(h, seq) + +LEMMA StrictPrefixesDetermineDef_WFDefOn == + ASSUME NEW S, NEW Def(_,_), StrictPrefixesDetermineDef(S, Def) + PROVE WFDefOn(OpToRel(IsStrictPrefix, Seq(S)), Seq(S), Def) + +THEOREM PrefixRecursiveSequenceFunctionUnique == + ASSUME NEW S, NEW Def(_,_), StrictPrefixesDetermineDef(S, Def) + PROVE WFInductiveUnique(Seq(S), Def) + +THEOREM PrefixRecursiveSequenceFunctionDef == + ASSUME NEW S, NEW Def(_,_), NEW f, + StrictPrefixesDetermineDef(S, Def), + OpDefinesFcn(f, Seq(S), Def) + PROVE WFInductiveDefines(f, Seq(S), Def) + +THEOREM PrefixRecursiveSequenceFunctionType == + ASSUME NEW S, NEW T, NEW Def(_,_), NEW f, + T # {}, + StrictPrefixesDetermineDef(S, Def), + WFInductiveDefines(f, Seq(S), Def), + \A g \in [Seq(S) -> T], s \in Seq(S) : Def(g,s) \in T + PROVE f \in [Seq(S) -> T] + +StrictSuffixesDetermineDef(S, Def(_,_)) == + \A g,h : \A seq \in Seq(S) : + (\A suf \in Seq(S) : IsStrictSuffix(suf,seq) => g[suf] = h[suf]) + => Def(g, seq) = Def(h, seq) + +LEMMA StrictSuffixesDetermineDef_WFDefOn == + ASSUME NEW S, NEW Def(_,_), StrictSuffixesDetermineDef(S, Def) + PROVE WFDefOn(OpToRel(IsStrictSuffix, Seq(S)), Seq(S), Def) + +THEOREM SuffixRecursiveSequenceFunctionUnique == + ASSUME NEW S, NEW Def(_,_), StrictSuffixesDetermineDef(S, Def) + PROVE WFInductiveUnique(Seq(S), Def) + +THEOREM SuffixRecursiveSequenceFunctionDef == + ASSUME NEW S, NEW Def(_,_), NEW f, + StrictSuffixesDetermineDef(S, Def), + OpDefinesFcn(f, Seq(S), Def) + PROVE WFInductiveDefines(f, Seq(S), Def) + +THEOREM SuffixRecursiveSequenceFunctionType == + ASSUME NEW S, NEW T, NEW Def(_,_), NEW f, + T # {}, + StrictSuffixesDetermineDef(S, Def), + WFInductiveDefines(f, Seq(S), Def), + \A g \in [Seq(S) -> T], s \in Seq(S) : Def(g,s) \in T + PROVE f \in [Seq(S) -> T] + +(***************************************************************************) +(* The following theorems justify ``primitive recursive'' functions over *) +(* sequences, with a base case for the empty sequence and recursion along *) +(* either the Tail or the Front of a non-empty sequence. *) +(***************************************************************************) + +TailInductiveDefHypothesis(f, S, f0, Def(_,_)) == + f = CHOOSE g : g = [s \in Seq(S) |-> IF s = <<>> THEN f0 ELSE Def(g[Tail(s)], s)] + +TailInductiveDefConclusion(f, S, f0, Def(_,_)) == + f = [s \in Seq(S) |-> IF s = <<>> THEN f0 ELSE Def(f[Tail(s)], s)] + +THEOREM TailInductiveDef == + ASSUME NEW S, NEW Def(_,_), NEW f, NEW f0, + TailInductiveDefHypothesis(f, S, f0, Def) + PROVE TailInductiveDefConclusion(f, S, f0, Def) + +THEOREM TailInductiveDefType == + ASSUME NEW S, NEW Def(_,_), NEW f, NEW f0, NEW T, + TailInductiveDefConclusion(f, S, f0, Def), + f0 \in T, + \A v \in T, s \in Seq(S) : s # <<>> => Def(v,s) \in T + PROVE f \in [Seq(S) -> T] + +FrontInductiveDefHypothesis(f, S, f0, Def(_,_)) == + f = CHOOSE g : g = [s \in Seq(S) |-> IF s = <<>> THEN f0 ELSE Def(g[Front(s)], s)] + +FrontInductiveDefConclusion(f, S, f0, Def(_,_)) == + f = [s \in Seq(S) |-> IF s = <<>> THEN f0 ELSE Def(f[Front(s)], s)] + +THEOREM FrontInductiveDef == + ASSUME NEW S, NEW Def(_,_), NEW f, NEW f0, + FrontInductiveDefHypothesis(f, S, f0, Def) + PROVE FrontInductiveDefConclusion(f, S, f0, Def) + +THEOREM FrontInductiveDefType == + ASSUME NEW S, NEW Def(_,_), NEW f, NEW f0, NEW T, + FrontInductiveDefConclusion(f, S, f0, Def), + f0 \in T, + \A v \in T, s \in Seq(S) : s # <<>> => Def(v,s) \in T + PROVE f \in [Seq(S) -> T] + +---------------------------------------------------------------------------- + +(**************************************************************************) +(* Recursive characterization of FoldLeft. *) +(**************************************************************************) +THEOREM FoldLeftRecursion == + ASSUME NEW op(_,_), NEW base, NEW S, NEW seq \in Seq(S) + PROVE FoldLeft(op, base, seq) = + IF seq = << >> THEN base + ELSE op(FoldLeft(op, base, Front(seq)), Last(seq)) + +THEOREM FoldLeftEmpty == + ASSUME NEW op(_,_), NEW base + PROVE FoldLeft(op, base, <<>>) = base + +THEOREM FoldLeftNonempty == + ASSUME NEW op(_,_), NEW base, NEW S, NEW seq \in Seq(S), seq # << >> + PROVE FoldLeft(op, base, seq) = op(FoldLeft(op, base, Front(seq)), Last(seq)) + +(**************************************************************************) +(* Interaction of FoldLeft and Append. *) +(**************************************************************************) +THEOREM FoldLeftAppend == + ASSUME NEW op(_,_), NEW base, NEW S, NEW seq \in Seq(S), NEW s \in S + PROVE FoldLeft(op, base, Append(seq,s)) = op(FoldLeft(op, base, seq), s) + +(**************************************************************************) +(* Type of FoldLeft. *) +(**************************************************************************) +THEOREM FoldLeftType == + ASSUME NEW Typ, NEW op(_,_), NEW base \in Typ, NEW seq \in Seq(Typ), + \A t,u \in Typ : op(t,u) \in Typ + PROVE FoldLeft(op, base, seq) \in Typ + +(**************************************************************************) +(* Recursive characterization of FoldRight. *) +(**************************************************************************) +THEOREM FoldRightRecursion == + ASSUME NEW op(_,_), NEW base, NEW S, NEW seq \in Seq(S) + PROVE FoldRight(op, seq, base) = + IF seq = << >> THEN base + ELSE op(Head(seq), FoldRight(op, Tail(seq), base)) + +THEOREM FoldRightEmpty == + ASSUME NEW op(_,_), NEW base + PROVE FoldRight(op, <<>>, base) = base + +THEOREM FoldRightNonempty == + ASSUME NEW op(_,_), NEW base, NEW S, NEW seq \in Seq(S), seq # << >> + PROVE FoldRight(op, seq, base) = op(Head(seq), FoldRight(op, Tail(seq), base)) + +(**************************************************************************) +(* Interaction of FoldRight and Cons. *) +(**************************************************************************) +THEOREM FoldRightCons == + ASSUME NEW op(_,_), NEW base, NEW S, NEW seq \in Seq(S), NEW s \in S + PROVE FoldRight(op, Cons(s, seq), base) = op(s, FoldRight(op, seq, base)) + +(**************************************************************************) +(* Type of FoldRight. *) +(**************************************************************************) +THEOREM FoldRightType == + ASSUME NEW Typ, NEW op(_,_), NEW base \in Typ, NEW seq \in Seq(Typ), + \A t,u \in Typ : op(t,u) \in Typ + PROVE FoldRight(op, seq, base) \in Typ + +(**************************************************************************) +(* FoldLeftDomain and FoldRightDomain cannot be characterized recursively *) +(* in terms of the same operators, we reduce them to MapThenFoldSet. *) +(**************************************************************************) +THEOREM FoldLeftDomainIsMFS == + ASSUME NEW op(_,_), NEW base, NEW S, NEW seq \in Seq(S) + PROVE FoldLeftDomain(op, base, seq) = + MapThenFoldSet(LAMBDA x,y : op(y,x), base, + LAMBDA i : i, LAMBDA T : Max(T), 1 .. Len(seq)) + +THEOREM FoldRightDomainIsMFS == + ASSUME NEW op(_,_), NEW base, NEW S, NEW seq \in Seq(S) + PROVE FoldRightDomain(op, seq, base) = + MapThenFoldSet(op, base, + LAMBDA i : i, LAMBDA T : Min(T), 1 .. Len(seq)) + +============================================================================ diff --git a/modules/SequencesExtTheorems_proofs.tla b/modules/SequencesExtTheorems_proofs.tla new file mode 100644 index 0000000..0000099 --- /dev/null +++ b/modules/SequencesExtTheorems_proofs.tla @@ -0,0 +1,1152 @@ +-------------------- MODULE SequencesExtTheorems_proofs -------------------- +(**************************************************************************) +(* This module contains theorems about the operators on sequences defined *) +(* in module SequencesExt. *) +(**************************************************************************) +EXTENDS Sequences, SequencesExt, FiniteSetsExt, Functions, Integers, + SequenceTheorems, NaturalsInduction, WellFoundedInduction, + FiniteSetTheorems, FiniteSetsExtTheorems, FoldsTheorems, TLAPS + +(***************************************************************************) +(* Theorems about Cons. *) +(* Cons(elt, seq) == <> \o seq *) +(***************************************************************************) + +THEOREM ConsProperties == + ASSUME NEW S, NEW seq \in Seq(S), NEW elt \in S + PROVE /\ Cons(elt, seq) \in Seq(S) + /\ Cons(elt, seq) # <<>> + /\ Len(Cons(elt, seq)) = Len(seq)+1 + /\ Head(Cons(elt, seq)) = elt + /\ Tail(Cons(elt, seq)) = seq + /\ Cons(elt, seq)[1] = elt + /\ \A i \in 1 .. Len(seq) : Cons(elt, seq)[i+1] = seq[i] + /\ \A i \in 2 .. Len(seq)+1 : Cons(elt, seq)[i] = seq[i-1] +BY DEF Cons + +THEOREM ConsEmpty == + ASSUME NEW x + PROVE Cons(x, << >>) = << x >> +BY <> \in Seq({x}) DEF Cons + +THEOREM ConsHeadTail == + ASSUME NEW S, NEW seq \in Seq(S), seq # << >> + PROVE Cons(Head(seq), Tail(seq)) = seq +BY DEF Cons + +THEOREM ConsAppend == + ASSUME NEW S, NEW seq \in Seq(S), NEW x \in S, NEW y \in S + PROVE Cons(x, Append(seq, y)) = Append(Cons(x,seq), y) +BY DEF Cons + +THEOREM ConsInjective == + ASSUME NEW S, NEW e \in S, NEW s \in Seq(S), NEW f \in S, NEW t \in Seq(S) + PROVE Cons(e,s) = Cons(f,t) <=> e = f /\ s = t +<1>1. ASSUME Cons(e,s) = Cons(f,t) PROVE e = f /\ s = t + <2>1. /\ Head(Cons(e,s)) = e /\ Tail(Cons(e,s)) = s + /\ Head(Cons(f,t)) = f /\ Tail(Cons(f,t)) = t + BY DEF Cons + <2>. QED BY <1>1, <2>1 +<1>. QED BY <1>1 + +THEOREM SequencesInductionCons == + ASSUME NEW P(_), NEW S, + P(<< >>), + \A s \in Seq(S), e \in S : P(s) => P(Cons(e,s)) + PROVE \A seq \in Seq(S) : P(seq) +<1>. DEFINE Q(n) == \A seq \in Seq(S) : Len(seq) = n => P(seq) +<1>1. SUFFICES \A k \in Nat : Q(k) + OBVIOUS +<1>2. Q(0) + OBVIOUS +<1>3. ASSUME NEW n \in Nat, Q(n) + PROVE Q(n+1) + <2>1. ASSUME NEW s \in Seq(S), Len(s) = n+1 + PROVE P(s) + <3>1. /\ Tail(s) \in Seq(S) + /\ Head(s) \in S + /\ Len(Tail(s)) = n + /\ Cons(Head(s), Tail(s)) = s + BY <2>1, ConsHeadTail + <3>2. P(Tail(s)) + BY <1>3, <3>1, Zenon + <3>. QED BY <3>1, <3>2, Zenon + <2>. QED BY <2>1 +<1>. QED BY <1>2, <1>3, NatInduction, Isa + +(***************************************************************************) +(* Theorems about InsertAt and RemoveAt. *) +(* InsertAt(seq,i,elt) == *) +(* SubSeq(seq, 1, i-1) \o <> \o SubSeq(seq, i, Len(seq)) *) +(* RemoveAt(seq, i) == SubSeq(seq, 1, i-1) \o SubSeq(seq, i+1, Len(seq)) *) +(***************************************************************************) + +THEOREM InsertAtProperties == + ASSUME NEW S, NEW seq \in Seq(S), NEW i \in 1 .. Len(seq)+1, NEW elt \in S + PROVE /\ InsertAt(seq,i,elt) \in Seq(S) + /\ Len(InsertAt(seq,i,elt)) = Len(seq)+1 + /\ \A j \in 1 .. Len(seq)+1 : InsertAt(seq,i,elt)[j] = + IF j> THEN 0 ELSE Len(seq)-1 + /\ \A i \in 1 .. Len(seq)-1 : Front(seq)[i] = seq[i] +BY DEF Front + +THEOREM FrontOfEmpty == Front(<< >>) = << >> +BY DEF Front + +THEOREM LastProperties == + ASSUME NEW S, NEW seq \in Seq(S), seq # << >> + PROVE /\ Last(seq) \in S + /\ Append(Front(seq), Last(seq)) = seq +BY DEF Front, Last + +THEOREM FrontLastOfSubSeq == + ASSUME NEW S, NEW seq \in Seq(S), + NEW m \in 1 .. Len(seq), NEW n \in m .. Len(seq) + PROVE /\ Front(SubSeq(seq,m,n)) = SubSeq(seq, m, n-1) + /\ Last(SubSeq(seq,m,n)) = seq[n] +BY DEF Front, Last + +THEOREM FrontLastAppend == + ASSUME NEW S, NEW seq \in Seq(S), NEW e \in S + PROVE /\ Front(Append(seq, e)) = seq + /\ Last(Append(seq, e)) = e +BY DEF Front, Last + +LEMMA FrontInjectiveSeq == + ASSUME NEW S, NEW seq \in Seq(S), IsInjective(seq), seq # << >> + PROVE /\ IsInjective(Front(seq)) + /\ Range(Front(seq)) = Range(seq) \ {Last(seq)} +<1>. DEFINE ft == Front(seq) +<1>1. IsInjective(ft) + BY DEF IsInjective, Front +<1>2. ASSUME NEW e \in Range(ft) + PROVE e \in Range(seq) \ {Last(seq)} + BY DEF Range, IsInjective, Front, Last +<1>3. ASSUME NEW e \in Range(seq) \ {Last(seq)} + PROVE e \in Range(ft) + <2>1. PICK i \in 1 .. Len(seq)-1 : e = seq[i] + BY DEF Range, Last + <2>. QED BY <2>1 DEF Range, Front +<1>. QED BY <1>1, <1>2, <1>3 + +THEOREM SequencesInductionFront == + ASSUME NEW S, NEW P(_), + P(<< >>), + \A s \in Seq(S) : (s # << >>) /\ P(Front(s)) => P(s) + PROVE \A s \in Seq(S) : P(s) +<1>. DEFINE Q(n) == \A s \in Seq(S) : Len(s) = n => P(s) +<1>. SUFFICES \A k \in Nat : Q(k) + OBVIOUS +<1>1. Q(0) + OBVIOUS +<1>2. ASSUME NEW n \in Nat, Q(n) + PROVE Q(n+1) + <2>. SUFFICES ASSUME NEW s \in Seq(S), Len(s) = n+1 + PROVE P(s) + OBVIOUS + <2>1. /\ Front(s) \in Seq(S) + /\ Len(Front(s)) = n + BY FrontProperties + <2>. QED BY <2>1, <1>2 +<1>3. QED BY <1>1, <1>2, NatInduction, Isa + +(***************************************************************************) +(* Theorems about Reverse. *) +(* Reverse(seq) == [j \in 1 .. Len(seq) |-> seq[Len(seq)-j+1] ] *) +(***************************************************************************) + +THEOREM ReverseProperties == + ASSUME NEW S, NEW seq \in Seq(S) + PROVE /\ Reverse(seq) \in Seq(S) + /\ Len(Reverse(seq)) = Len(seq) + /\ Reverse(Reverse(seq)) = seq +BY DEF Reverse + +THEOREM ReverseEmpty == Reverse(<< >>) = << >> +BY DEF Reverse + +THEOREM ReverseSingleton == \A x : Reverse(<< x >>) = << x >> +BY DEF Reverse + +THEOREM ReverseEqual == + ASSUME NEW S, NEW s \in Seq(S), NEW t \in Seq(S), Reverse(s) = Reverse(t) + PROVE s = t +<1>1. Len(s) = Len(t) BY DEF Reverse +<1>2. ASSUME NEW i \in 1 .. Len(s) + PROVE s[i] = t[i] + <2>. /\ s[i] = Reverse(s)[Len(s)-i+1] + /\ t[i] = Reverse(t)[Len(s)-i+1] + BY DEF Reverse + <2>. QED OBVIOUS +<1>. QED BY <1>1, <1>2, SeqEqual + +THEOREM ReverseEmptyIffEmpty == + ASSUME NEW S, NEW seq \in Seq(S), Reverse(seq) = <<>> + PROVE seq = <<>> +BY DEF Reverse + +THEOREM ReverseConcat == + ASSUME NEW S, NEW s1 \in Seq(S), NEW s2 \in Seq(S) + PROVE Reverse(s1 \o s2) = Reverse(s2) \o Reverse(s1) +<1>1. /\ Reverse(s1) \in Seq(S) /\ Reverse(s2) \in Seq(S) + /\ Reverse(s1 \o s2) \in Seq(S) + /\ Len(Reverse(s1 \o s2)) = Len(Reverse(s2) \o Reverse(s1)) + BY ReverseProperties +<1>2. ASSUME NEW i \in 1 .. Len(Reverse(s1 \o s2)) + PROVE Reverse(s1 \o s2)[i] = (Reverse(s2) \o Reverse(s1))[i] + BY DEF Reverse +<1>. QED BY <1>1, <1>2 + +THEOREM ReverseAppend == + ASSUME NEW S, NEW seq \in Seq(S), NEW e \in S + PROVE Reverse(Append(seq,e)) = Cons(e, Reverse(seq)) +BY DEF Reverse, Cons + +THEOREM ReverseCons == + ASSUME NEW S, NEW seq \in Seq(S), NEW e \in S + PROVE Reverse(Cons(e,seq)) = Append(Reverse(seq), e) +<1>1. Reverse(seq) \in Seq(S) + BY ReverseProperties +<1>2. Reverse(Cons(e, seq)) = Reverse(seq) \o <> + BY ReverseConcat, ReverseSingleton DEF Cons +<1>3. @ = Append(Reverse(seq), e) + BY <1>1 +<1>. QED BY <1>2, <1>3 + + +THEOREM ReverseSubSeq == + ASSUME NEW S, NEW seq \in Seq(S), + NEW m \in 1..Len(seq), NEW n \in 0..Len(seq) + PROVE Reverse(SubSeq(seq, m , n)) = SubSeq(Reverse(seq), Len(seq)-n+1, Len(seq)-m+1) +<1>. /\ Reverse(seq) \in Seq(S) + /\ Len(seq)-n+1 \in 1 .. Len(Reverse(seq))+1 + /\ Len(seq)-m+1 \in 1 .. Len(Reverse(seq)) + BY ReverseProperties +<1>. QED BY DEF Reverse + +THEOREM ReversePalindrome == + ASSUME NEW S, NEW seq \in Seq(S), + Reverse(seq) = seq + PROVE Reverse(seq \o seq) = seq \o seq +BY ReverseConcat + +THEOREM LastEqualsHeadReverse == + ASSUME NEW S, NEW seq \in Seq(S), seq # << >> + PROVE Last(seq) = Head(Reverse(seq)) +BY DEF Last, Reverse + +THEOREM ReverseFrontEqualsTailReverse == + ASSUME NEW S, NEW seq \in Seq(S), seq # << >> + PROVE Reverse(Front(seq)) = Tail(Reverse(seq)) +<1>1. Reverse(seq) \in Seq(S) /\ Len(Reverse(seq)) = Len(seq) + BY ReverseProperties +<1>2. Reverse(Front(seq)) = SubSeq(Reverse(seq), 2, Len(seq)) + BY ReverseSubSeq DEF Front +<1>. QED BY <1>1, <1>2 + +(* The range of the reverse sequence equals that of the original one. *) +THEOREM RangeReverse == + ASSUME NEW S, NEW seq \in Seq(S) + PROVE /\ DOMAIN Reverse(seq) = DOMAIN seq + /\ Range(Reverse(seq)) = Range(seq) +<1>1. /\ DOMAIN seq = 1 .. Len(seq) + /\ DOMAIN Reverse(seq) = 1 .. Len(seq) + /\ Reverse(seq) \in Seq(S) + BY DEF Reverse +<1>2. ASSUME NEW i \in 1 .. Len(seq) + PROVE seq[i] = Reverse(seq)[Len(seq)-i+1] + BY DEF Reverse +<1>. QED BY <1>1, <1>2 DEF Range + +(***************************************************************************) +(* Theorems about prefixes and suffixes of sequences. *) +(* IsPrefix(s,t) == \E u \in Seq(Range(t)) : t = s \o u *) +(* IsStrictPrefix(s,t) == IsPrefix(s,t) /\ s # t *) +(* IsSuffix(s,t) == \E u \in Seq(Range(t)) : t = u \o s *) +(* IsStrictSuffix(s,t) == IsSuffix(s,t) /\ s # t *) +(***************************************************************************) + +(***************************************************************************) +(* The following theorem gives three alternative characterizations of *) +(* prefixes. It also implies that any prefix of a sequence t is at most *) +(* as long as t. *) +(***************************************************************************) +THEOREM IsPrefixProperties == + ASSUME NEW S, NEW s \in Seq(S), NEW t \in Seq(S) + PROVE /\ IsPrefix(s,t) <=> \E u \in Seq(S) : t = s \o u + /\ IsPrefix(s,t) <=> Len(s) <= Len(t) /\ s = SubSeq(t, 1, Len(s)) + /\ IsPrefix(s,t) <=> Len(s) <= Len(t) /\ s = Restrict(t, DOMAIN s) +<1>1. IsPrefix(s,t) <=> (Len(s) <= Len(t) /\ s = SubSeq(t, 1, Len(s))) + <2>1. IsPrefix(s,t) => Len(s) =< Len(t) BY DEF IsPrefix + <2>2. IsPrefix(s,t) => s = SubSeq(t, 1, Len(s)) BY <2>1 DEF IsPrefix + <2>3. (Len(s) <= Len(t) /\ s = SubSeq(t, 1, Len(s))) => IsPrefix(s, t) BY DEF IsPrefix + <2>q. QED BY <2>1, <2>2, <2>3 +<1>2. IsPrefix(s,t) <=> \E u \in Seq(S) : t = s \o u + <2>1. ASSUME IsPrefix(s,t) PROVE \E u \in Seq(S) : t = s \o u + <3>1. Len(s) <= Len(t) /\ s = SubSeq(t, 1, Len(s)) + BY <1>1, <2>1 + <3>2. /\ SubSeq(t, Len(s)+1, Len(t)) \in Seq(S) + /\ t = s \o SubSeq(t, Len(s)+1, Len(t)) + BY <3>1 + <3>. QED BY <3>2 + <2>2. ASSUME NEW u \in Seq(S), t = s \o u PROVE IsPrefix(s,t) + BY <2>2 DEF IsPrefix + <2>. QED BY <2>1, <2>2 +<1>3. IsPrefix(s,t) <=> Len(s) <= Len(t) /\ s = Restrict(t, DOMAIN s) + BY DEF IsPrefix, Restrict +<1>. QED BY <1>1, <1>2, <1>3 + +THEOREM IsStrictPrefixProperties == + ASSUME NEW S, NEW s \in Seq(S), NEW t \in Seq(S) + PROVE /\ IsStrictPrefix(s,t) <=> \E u \in Seq(S) : u # << >> /\ t = s \o u + /\ IsStrictPrefix(s,t) <=> Len(s) < Len(t) /\ s = SubSeq(t, 1, Len(s)) + /\ IsStrictPrefix(s,t) <=> Len(s) < Len(t) /\ s = Restrict(t, DOMAIN s) + /\ IsStrictPrefix(s,t) <=> IsPrefix(s,t) /\ Len(s) < Len(t) +<1>1. IsStrictPrefix(s,t) => Len(s) < Len(t) + BY IsPrefixProperties DEF IsStrictPrefix +<1>2. IsStrictPrefix(s,t) <=> \E u \in Seq(S) : u # << >> /\ t = s \o u + <2>1. ASSUME IsStrictPrefix(s,t) + PROVE \E u \in Seq(S) : u # << >> /\ t = s \o u + \* the following doesn't seem to work everywhere + \* BY <2>1, IsPrefixProperties DEF IsStrictPrefix + <3>1. IsPrefix(s,t) /\ s # t + BY <2>1 DEF IsStrictPrefix + <3>2. PICK u \in Seq(S): t = s \o u + BY <3>1, IsPrefixProperties + <3>. QED BY <3>1, <3>2 + + <2>2. ASSUME NEW u \in Seq(S), u # << >>, t = s \o u + PROVE IsStrictPrefix(s,t) + <3>1. IsPrefix(s,t) + BY <2>2, IsPrefixProperties, Zenon + <3>2. s # t + BY <2>2 + <3>. QED BY <3>1, <3>2 DEF IsStrictPrefix + <2>. QED BY <2>1, <2>2, Zenon +<1>3. /\ IsStrictPrefix(s,t) <=> Len(s) < Len(t) /\ s = SubSeq(t, 1, Len(s)) + /\ IsStrictPrefix(s,t) <=> Len(s) < Len(t) /\ s = Restrict(t, DOMAIN s) + /\ IsStrictPrefix(s,t) <=> IsPrefix(s,t) /\ Len(s) < Len(t) + BY <1>1, IsPrefixProperties DEF IsStrictPrefix +<1>. QED BY <1>1, <1>2, <1>3 + +THEOREM IsPrefixElts == + ASSUME NEW S, NEW s \in Seq(S), NEW t \in Seq(S), NEW i \in 1 .. Len(s), + IsPrefix(s,t) + PROVE s[i] = t[i] +BY IsPrefixProperties + +THEOREM EmptyIsPrefix == + ASSUME NEW S, NEW s \in Seq(S) + PROVE /\ IsPrefix(<<>>, s) + /\ IsPrefix(s, <<>>) <=> s = <<>> + /\ IsStrictPrefix(<<>>, s) <=> s # <<>> + /\ ~ IsStrictPrefix(s, <<>>) +BY IsPrefixProperties, IsStrictPrefixProperties + +THEOREM IsPrefixConcat == + ASSUME NEW S, NEW s \in Seq(S), NEW t \in Seq(S) + PROVE IsPrefix(s, s \o t) +BY IsPrefixProperties, ConcatProperties + +THEOREM IsStrictPrefixAppend == + ASSUME NEW S, NEW s \in Seq(S), NEW e \in S + PROVE IsStrictPrefix(s, Append(s,e)) +<1>1. /\ Append(s,e) = s \o <> + /\ Append(s,e) \in Seq(S) + /\ <> \in Seq(S) + /\ <> # << >> + OBVIOUS +<1>. QED BY <1>1, IsStrictPrefixProperties + +THEOREM FrontIsPrefix == + ASSUME NEW S, NEW s \in Seq(S) + PROVE /\ IsPrefix(Front(s), s) + /\ s # <<>> => IsStrictPrefix(Front(s), s) +<1>1. /\ Front(s) \in Seq(S) + /\ Len(Front(s)) <= Len(s) + /\ Front(s) = SubSeq(s, 1, Len(Front(s))) + /\ s # << >> => Len(Front(s)) < Len(s) + BY DEF Front +<1>. QED BY <1>1, IsPrefixProperties, IsStrictPrefixProperties + +(***************************************************************************) +(* (Strict) prefixes on sequences form a (strict) partial order, and *) +(* the strict ordering is well-founded. *) +(***************************************************************************) +THEOREM IsPrefixPartialOrder == + ASSUME NEW S + PROVE /\ \A s \in Seq(S) : IsPrefix(s,s) + /\ \A s,t \in Seq(S) : IsPrefix(s,t) /\ IsPrefix(t,s) => s = t + /\ \A s,t,u \in Seq(S) : IsPrefix(s,t) /\ IsPrefix(t,u) => IsPrefix(s,u) +BY DEF IsPrefix + +THEOREM ConcatIsPrefix == + ASSUME NEW S, NEW s \in Seq(S), NEW t \in Seq(S), NEW u \in Seq(S), + IsPrefix(s \o t, u) + PROVE IsPrefix(s, u) +BY DEF IsPrefix + +THEOREM ConcatIsPrefixCancel == + ASSUME NEW S, NEW s \in Seq(S), NEW t \in Seq(S), NEW u \in Seq(S) + PROVE /\ IsPrefix(s \o t, s \o u) <=> IsPrefix(t, u) +<1>1. ASSUME IsPrefix(t,u) PROVE IsPrefix(s \o t, s \o u) + <2>1. PICK v \in Seq(S) : u = t \o v BY <1>1, IsPrefixProperties + <2>2. s \o u = (s \o t) \o v BY <2>1 + <2>. QED BY <2>2, IsPrefixProperties, s \o u \in Seq(S), s \o t \in Seq(S) +<1>2. ASSUME IsPrefix(s \o t, s \o u) PROVE IsPrefix(t,u) + <2>1. PICK v \in Seq(S) : s \o u = (s \o t) \o v + BY <1>2, s \o t \in Seq(S), s \o u \in Seq(S), IsPrefixProperties + <2>2. s \o u = s \o (t \o v) + BY <2>1 + <2>3. u = t \o v + BY t \o v \in Seq(S), <2>2, ConcatSimplifications + <2>. QED BY <2>3, IsPrefixProperties +<1>. QED BY <1>1, <1>2 + +THEOREM ConsIsPrefixCancel == + ASSUME NEW S, NEW e \in S, NEW s \in Seq(S), NEW t \in Seq(S) + PROVE IsPrefix(Cons(e,s), Cons(e,t)) <=> IsPrefix(s,t) +BY <> \in Seq(S), ConcatIsPrefixCancel, Zenon DEF Cons + +THEOREM ConsIsPrefix == + ASSUME NEW S, NEW e \in S, NEW s \in Seq(S), NEW u \in Seq(S), + IsPrefix(Cons(e,s), u) + PROVE /\ e = Head(u) + /\ IsPrefix(s, Tail(u)) +<1>. <> \in Seq(S) + OBVIOUS +<1>1. IsPrefix(<>, u) + BY ConcatIsPrefix, Zenon DEF Cons +<1>2. PICK v \in Seq(S) : u = Cons(e, v) + BY <1>1, IsPrefixProperties DEF Cons +<1>3. /\ e = Head(u) + /\ v = Tail(u) + /\ IsPrefix(Cons(e,s), Cons(e, Tail(u))) + BY <1>2, ConsProperties +<1>. QED + BY <1>3, ConsIsPrefixCancel + +THEOREM IsStrictPrefixStrictPartialOrder == + ASSUME NEW S + PROVE /\ \A s \in Seq(S) : ~ IsStrictPrefix(s,s) + /\ \A s,t \in Seq(S) : IsStrictPrefix(s,t) => ~ IsStrictPrefix(t,s) + /\ \A s,t,u \in Seq(S) : IsStrictPrefix(s,t) /\ IsStrictPrefix(t,u) => IsStrictPrefix(s,u) +<1>1. ASSUME NEW s \in Seq(S) + PROVE ~ IsStrictPrefix(s,s) + BY <1>1, IsStrictPrefixProperties +<1>2. ASSUME NEW s \in Seq(S), NEW t \in Seq(S), IsStrictPrefix(s,t), IsStrictPrefix(t,s) + PROVE FALSE + BY <1>2, IsStrictPrefixProperties +<1>3. ASSUME NEW s \in Seq(S), NEW t \in Seq(S), NEW u \in Seq(S), + IsStrictPrefix(s,t), IsStrictPrefix(t,u) + PROVE IsStrictPrefix(s,u) + <2>1. PICK st \in Seq(S) \ {<<>>} : t = s \o st + BY <1>3, IsStrictPrefixProperties + <2>2. PICK tu \in Seq(S) \ {<<>>} : u = t \o tu + BY <1>3, IsStrictPrefixProperties + <2>3. u = s \o (st \o tu) + BY <2>1, <2>2 + <2>. QED BY <2>3, IsStrictPrefixProperties +<1> QED BY <1>1, <1>2, <1>3 + + +THEOREM IsStrictPrefixWellFounded == + ASSUME NEW S + PROVE IsWellFoundedOn(OpToRel(IsStrictPrefix, Seq(S)), Seq(S)) +<1>1. IsWellFoundedOn(PreImage(Len, Seq(S), OpToRel(<, Nat)), Seq(S)) + BY NatLessThanWellFounded, PreImageWellFounded, IsaM("blast") +<1>2. OpToRel(IsStrictPrefix, Seq(S)) \subseteq PreImage(Len, Seq(S), OpToRel(<, Nat)) + BY IsStrictPrefixProperties DEF PreImage, OpToRel +<1>. QED + BY <1>1, <1>2, IsWellFoundedOnSubrelation, Zenon + +THEOREM SeqStrictPrefixInduction == + ASSUME NEW P(_), NEW S, + \A t \in Seq(S) : (\A s \in Seq(S) : IsStrictPrefix(s,t) => P(s)) => P(t) + PROVE \A s \in Seq(S) : P(s) +<1>1. \A t \in Seq(S) : + (\A s \in SetLessThan(t, OpToRel(IsStrictPrefix, Seq(S)), Seq(S)) : P(s)) + => P(t) + BY Zenon DEF SetLessThan, OpToRel +<1>. QED BY WFInduction, IsStrictPrefixWellFounded, <1>1, IsaM("blast") + +(***************************************************************************) +(* Similar theorems about suffixes. *) +(***************************************************************************) + +THEOREM IsSuffixProperties == + ASSUME NEW S, NEW s \in Seq(S), NEW t \in Seq(S) + PROVE /\ IsSuffix(s,t) <=> \E u \in Seq(S) : t = u \o s + /\ IsSuffix(s,t) <=> Len(s) <= Len(t) /\ s = SubSeq(t, Len(t)-Len(s)+1, Len(t)) +<1>. Reverse(s) \in Seq(S) /\ Reverse(t) \in Seq(S) + BY DEF Reverse +<1>1. IsSuffix(s,t) <=> \E u \in Seq(S) : t = u \o s + <2>1. ASSUME IsSuffix(s,t) + PROVE \E u \in Seq(S) : t = u \o s + <3>1. PICK u \in Seq(S) : Reverse(t) = Reverse(s) \o u + BY <2>1, IsPrefixProperties, Isa DEF IsSuffix + <3>2. Reverse(u) \in Seq(S) + BY DEF Reverse + <3>3. Reverse(Reverse(t)) = Reverse(u) \o Reverse(Reverse(s)) + BY <3>1, ReverseConcat + <3>4. t = Reverse(u) \o s + BY <3>3, ReverseProperties + <3>. QED BY <3>2, <3>4 DEF Reverse + <2>2. ASSUME NEW u \in Seq(S), t = u \o s + PROVE IsSuffix(s,t) + <3>. Reverse(u) \in Seq(S) + BY ReverseProperties + <3>1. Reverse(t) = Reverse(s) \o Reverse(u) + BY <2>2, ReverseConcat + <3>2. IsPrefix(Reverse(s), Reverse(t)) + BY <3>1, IsPrefixProperties, Zenon + <3>. QED BY <3>2 DEF IsSuffix + <2>. QED BY <2>1, <2>2, Zenon +<1>2. IsSuffix(s,t) <=> Len(s) <= Len(t) /\ s = SubSeq(t, Len(t)-Len(s)+1, Len(t)) + <2>1. ASSUME IsSuffix(s,t) + PROVE Len(s) <= Len(t) /\ s = SubSeq(t, Len(t)-Len(s)+1, Len(t)) + <3>1. PICK u \in Seq(S) : t = u \o s + BY <1>1, <2>1 + <3>. QED BY <3>1 + <2>2. ASSUME Len(s) <= Len(t), s = SubSeq(t, Len(t)-Len(s)+1, Len(t)) + PROVE IsSuffix(s,t) + <3>1. t = SubSeq(t, 1, Len(t) - Len(s)) \o s + BY <2>2 + <3>2. SubSeq(t, 1, Len(t) - Len(s)) \in Seq(S) + OBVIOUS + <3>. QED BY <3>1, <3>2, <1>1, Zenon + <2>. QED BY <2>1, <2>2 +<1>. QED BY <1>1, <1>2, Zenon + +THEOREM IsStrictSuffixProperties == + ASSUME NEW S, NEW s \in Seq(S), NEW t \in Seq(S) + PROVE /\ IsStrictSuffix(s,t) <=> \E u \in Seq(S) : u # << >> /\ t = u \o s + /\ IsStrictSuffix(s,t) <=> Len(s) < Len(t) /\ IsSuffix(s,t) + /\ IsStrictSuffix(s,t) <=> Len(s) < Len(t) /\ s = SubSeq(t, Len(t)-Len(s)+1, Len(t)) + /\ IsStrictSuffix(s,t) <=> IsStrictPrefix(Reverse(s), Reverse(t)) +<1>1. IsStrictSuffix(s,t) <=> IsStrictPrefix(Reverse(s), Reverse(t)) + BY ReverseEqual DEF IsStrictSuffix, IsSuffix, IsStrictPrefix +<1>2. IsStrictSuffix(s,t) => Len(s) < Len(t) + BY <1>1, IsStrictPrefixProperties, ReverseProperties, Zenon +<1>3. IsStrictSuffix(s,t) <=> \E u \in Seq(S) : u # << >> /\ t = u \o s + <2>1. ASSUME IsStrictSuffix(s,t) + PROVE \E u \in Seq(S) : u # << >> /\ t = u \o s + <3>1. PICK u \in Seq(S) : t = u \o s + BY <2>1, IsSuffixProperties DEF IsStrictSuffix + <3>2. u # << >> + BY <2>1, <3>1 DEF IsStrictSuffix + <3>. QED BY <3>1, <3>2 + <2>2. ASSUME NEW u \in Seq(S), u # << >> /\ t = u \o s + PROVE IsStrictSuffix(s,t) + <3>1. IsSuffix(s,t) + BY <2>2, IsSuffixProperties, Zenon + <3>2. s # t + BY <2>2 + <3>. QED BY <3>1, <3>2 DEF IsStrictSuffix + <2>. QED BY <2>1, <2>2, Zenon +<1>4. IsStrictSuffix(s,t) <=> Len(s) < Len(t) /\ IsSuffix(s,t) + BY <1>2, IsSuffixProperties DEF IsStrictSuffix +<1>5. IsStrictSuffix(s,t) <=> Len(s) < Len(t) /\ s = SubSeq(t, Len(t)-Len(s)+1, Len(t)) + BY <1>2, IsSuffixProperties DEF IsStrictSuffix +<1>. QED BY <1>1, <1>3, <1>4, <1>5, Zenon + +THEOREM IsSuffixElts == + ASSUME NEW S, NEW s \in Seq(S), NEW t \in Seq(S), NEW i \in 1 .. Len(s), + IsSuffix(s,t) + PROVE s[i] = t[Len(t) - Len(s) + i] +BY IsSuffixProperties + +THEOREM EmptyIsSuffix == + ASSUME NEW S, NEW s \in Seq(S) + PROVE /\ IsSuffix(<<>>, s) + /\ IsSuffix(s, <<>>) <=> s = <<>> + /\ IsStrictSuffix(<<>>, s) <=> s # <<>> + /\ ~ IsStrictSuffix(s, <<>>) +BY IsSuffixProperties, IsStrictSuffixProperties + +THEOREM IsSuffixConcat == + ASSUME NEW S, NEW s \in Seq(S), NEW t \in Seq(S) + PROVE IsSuffix(s, t \o s) +BY IsSuffixProperties, ConcatProperties, Zenon + +THEOREM IsStrictSuffixCons == + ASSUME NEW S, NEW s \in Seq(S), NEW e \in S + PROVE IsStrictSuffix(s, Cons(e,s)) +<1>. /\ <> \in Seq(S) + /\ <> \o s \in Seq(S) + OBVIOUS +<1>. QED BY IsStrictSuffixProperties, Zenon DEF Cons + +THEOREM TailIsSuffix == + ASSUME NEW S, NEW s \in Seq(S), s # << >> + PROVE IsStrictSuffix(Tail(s), s) +BY ConsHeadTail, IsStrictSuffixCons, Head(s) \in S, Tail(s) \in Seq(S), Zenon + +THEOREM IsSuffixPartialOrder == + ASSUME NEW S + PROVE /\ \A s \in Seq(S) : IsSuffix(s,s) + /\ \A s,t \in Seq(S) : IsSuffix(s,t) /\ IsSuffix(t,s) => s = t + /\ \A s,t,u \in Seq(S) : IsSuffix(s,t) /\ IsSuffix(t,u) => IsSuffix(s,u) +<1>1. ASSUME NEW s \in Seq(S) PROVE IsSuffix(s,s) + BY s = s \o <<>>, IsSuffixProperties +<1>2. ASSUME NEW s \in Seq(S), NEW t \in Seq(S), IsSuffix(s,t), IsSuffix(t,s) + PROVE s = t + BY <1>2, IsPrefixPartialOrder, ReverseProperties, ReverseEqual DEF IsSuffix +<1>3. ASSUME NEW s \in Seq(S), NEW t \in Seq(S), NEW u \in Seq(S), + IsSuffix(s,t), IsSuffix(t,u) + PROVE IsSuffix(s,u) + BY <1>3, IsPrefixPartialOrder, ReverseProperties DEF IsSuffix +<1>. QED BY <1>1, <1>2, <1>3 + +THEOREM ConcatIsSuffix == + ASSUME NEW S, NEW s \in Seq(S), NEW t \in Seq(S), NEW u \in Seq(S), + IsSuffix(s \o t, u) + PROVE IsSuffix(t, u) +<1>1. /\ s \o t \in Seq(S) + /\ IsSuffix(t, s \o t) + BY IsSuffixConcat +<1>. QED BY <1>1, IsSuffixPartialOrder + +THEOREM ConcatIsSuffixCancel == + ASSUME NEW S, NEW s \in Seq(S), NEW t \in Seq(S), NEW u \in Seq(S) + PROVE IsSuffix(s \o t, u \o t) <=> IsSuffix(s, u) +<1>1. ASSUME IsSuffix(s, u) PROVE IsSuffix(s \o t, u \o t) + <2>1. PICK v \in Seq(S) : u = v \o s BY <1>1, IsSuffixProperties + <2>2. u \o t = v \o (s \o t) BY <2>1 + <2>. QED BY s \o t \in Seq(S), u \o t \in Seq(S), <2>2, IsSuffixProperties +<1>2. ASSUME IsSuffix(s \o t, u \o t) PROVE IsSuffix(s, u) + <2>1. PICK v \in Seq(S) : u \o t = v \o (s \o t) + BY <1>2, s \o t \in Seq(S), u \o t \in Seq(S), IsSuffixProperties + <2>2. u \o t = (v \o s) \o t + BY <2>1 + <2>3. u = v \o s + BY <2>2, ConcatSimplifications(*!cancelRight*), v \o s \in Seq(S) + <2>. QED BY <2>3, IsSuffixProperties +<1>. QED BY <1>1, <1>2 + +THEOREM AppendIsSuffixCancel == + ASSUME NEW S, NEW e \in S, NEW s \in Seq(S), NEW t \in Seq(S) + PROVE IsSuffix(Append(s,e), Append(t,e)) <=> IsSuffix(s,t) +<1>1. IsSuffix(Append(s,e), Append(t,e)) <=> IsSuffix(s \o <>, t \o <>) + BY AppendIsConcat +<1>2. @ <=> IsSuffix(s,t) + BY <> \in Seq(S), ConcatIsSuffixCancel, Zenon +<1>. QED BY <1>1, <1>2 + +THEOREM AppendIsSuffix == + ASSUME NEW S, NEW e \in S, NEW s \in Seq(S), NEW u \in Seq(S), + IsSuffix(Append(s,e), u) + PROVE /\ e = Last(u) + /\ IsSuffix(s, Front(u)) +<1>. <> \in Seq(S) + OBVIOUS +<1>1. IsSuffix(<>, u) + BY ConcatIsSuffix, AppendIsConcat, Zenon +<1>2. PICK v \in Seq(S) : u = Append(v,e) + BY <1>1, IsSuffixProperties, AppendIsConcat +<1>3. /\ e = Last(u) + /\ v = Front(u) + /\ IsSuffix(Append(s,e), Append(Front(u),e)) + BY <1>2, FrontLastAppend +<1>. QED + BY <1>3, AppendIsSuffixCancel, Zenon + +THEOREM IsStrictSuffixStrictPartialOrder == + ASSUME NEW S + PROVE /\ \A s \in Seq(S) : ~ IsStrictSuffix(s,s) + /\ \A s,t \in Seq(S) : IsStrictSuffix(s,t) => ~ IsStrictSuffix(t,s) + /\ \A s,t,u \in Seq(S) : IsStrictSuffix(s,t) /\ IsStrictSuffix(t,u) => IsStrictSuffix(s,u) +<1>1. ASSUME NEW s \in Seq(S) + PROVE ~ IsStrictSuffix(s,s) + BY <1>1, IsStrictSuffixProperties +<1>2. ASSUME NEW s \in Seq(S), NEW t \in Seq(S), IsStrictSuffix(s,t), IsStrictSuffix(t,s) + PROVE FALSE + BY <1>2, IsStrictSuffixProperties +<1>3. ASSUME NEW s \in Seq(S), NEW t \in Seq(S), NEW u \in Seq(S), + IsStrictSuffix(s,t), IsStrictSuffix(t,u) + PROVE IsStrictSuffix(s,u) + <2>1. PICK st \in Seq(S) \ {<<>>} : t = st \o s + BY <1>3, IsStrictSuffixProperties + <2>2. PICK tu \in Seq(S) \ {<<>>} : u = tu \o t + BY <1>3, IsStrictSuffixProperties + <2>3. u = (tu \o st) \o s + BY <2>1, <2>2 + <2>. QED BY <2>3, tu \o st # <<>>, IsStrictSuffixProperties +<1> QED BY <1>1, <1>2, <1>3 + +THEOREM IsStrictSuffixWellFounded == + ASSUME NEW S + PROVE IsWellFoundedOn(OpToRel(IsStrictSuffix, Seq(S)), Seq(S)) +<1>1. IsWellFoundedOn(PreImage(Len, Seq(S), OpToRel(<, Nat)), Seq(S)) + BY NatLessThanWellFounded, PreImageWellFounded, IsaM("blast") +<1>2. OpToRel(IsStrictSuffix, Seq(S)) \subseteq PreImage(Len, Seq(S), OpToRel(<, Nat)) + BY IsStrictSuffixProperties DEF PreImage, OpToRel +<1>. QED + BY <1>1, <1>2, IsWellFoundedOnSubrelation, Zenon + +THEOREM SeqStrictSuffixInduction == + ASSUME NEW P(_), NEW S, + \A t \in Seq(S) : (\A s \in Seq(S) : IsStrictSuffix(s,t) => P(s)) => P(t) + PROVE \A s \in Seq(S) : P(s) +<1>1. \A t \in Seq(S) : + (\A s \in SetLessThan(t, OpToRel(IsStrictSuffix, Seq(S)), Seq(S)) : P(s)) + => P(t) + BY Zenon DEF SetLessThan, OpToRel +<1>. QED BY WFInduction, IsStrictSuffixWellFounded, <1>1, IsaM("blast") + +(***************************************************************************) +(* Since the (strict) prefix and suffix orderings on sequences are *) +(* well-founded, they can be used for defining recursive functions. *) +(* The operators OpDefinesFcn, WFInductiveDefines, and WFInductiveUnique *) +(* are defined in module WellFoundedInduction. *) +(***************************************************************************) + +StrictPrefixesDetermineDef(S, Def(_,_)) == + \A g,h : \A seq \in Seq(S) : + (\A pre \in Seq(S) : IsStrictPrefix(pre,seq) => g[pre] = h[pre]) + => Def(g, seq) = Def(h, seq) + +LEMMA StrictPrefixesDetermineDef_WFDefOn == + ASSUME NEW S, NEW Def(_,_), StrictPrefixesDetermineDef(S, Def) + PROVE WFDefOn(OpToRel(IsStrictPrefix, Seq(S)), Seq(S), Def) +BY Isa DEF StrictPrefixesDetermineDef, WFDefOn, OpToRel, SetLessThan + +THEOREM PrefixRecursiveSequenceFunctionUnique == + ASSUME NEW S, NEW Def(_,_), StrictPrefixesDetermineDef(S, Def) + PROVE WFInductiveUnique(Seq(S), Def) +BY StrictPrefixesDetermineDef_WFDefOn, IsStrictPrefixWellFounded, WFDefOnUnique, Zenon + +THEOREM PrefixRecursiveSequenceFunctionDef == + ASSUME NEW S, NEW Def(_,_), NEW f, + StrictPrefixesDetermineDef(S, Def), + OpDefinesFcn(f, Seq(S), Def) + PROVE WFInductiveDefines(f, Seq(S), Def) +BY StrictPrefixesDetermineDef_WFDefOn, IsStrictPrefixWellFounded, WFInductiveDef, Zenon + +THEOREM PrefixRecursiveSequenceFunctionType == + ASSUME NEW S, NEW T, NEW Def(_,_), NEW f, + T # {}, + StrictPrefixesDetermineDef(S, Def), + WFInductiveDefines(f, Seq(S), Def), + \A g \in [Seq(S) -> T], s \in Seq(S) : Def(g,s) \in T + PROVE f \in [Seq(S) -> T] +<1>1. IsWellFoundedOn(OpToRel(IsStrictPrefix, Seq(S)), Seq(S)) + BY IsStrictPrefixWellFounded, Zenon +<1>2. WFDefOn(OpToRel(IsStrictPrefix, Seq(S)), Seq(S), Def) + BY StrictPrefixesDetermineDef_WFDefOn, Zenon +<1>. QED + BY <1>1, <1>2, WFInductiveDefType, Isa + +StrictSuffixesDetermineDef(S, Def(_,_)) == + \A g,h : \A seq \in Seq(S) : + (\A suf \in Seq(S) : IsStrictSuffix(suf,seq) => g[suf] = h[suf]) + => Def(g, seq) = Def(h, seq) + +LEMMA StrictSuffixesDetermineDef_WFDefOn == + ASSUME NEW S, NEW Def(_,_), StrictSuffixesDetermineDef(S, Def) + PROVE WFDefOn(OpToRel(IsStrictSuffix, Seq(S)), Seq(S), Def) +BY Isa DEF StrictSuffixesDetermineDef, WFDefOn, OpToRel, SetLessThan + +THEOREM SuffixRecursiveSequenceFunctionUnique == + ASSUME NEW S, NEW Def(_,_), StrictSuffixesDetermineDef(S, Def) + PROVE WFInductiveUnique(Seq(S), Def) +BY StrictSuffixesDetermineDef_WFDefOn, IsStrictSuffixWellFounded, WFDefOnUnique, Zenon + +THEOREM SuffixRecursiveSequenceFunctionDef == + ASSUME NEW S, NEW Def(_,_), NEW f, + StrictSuffixesDetermineDef(S, Def), + OpDefinesFcn(f, Seq(S), Def) + PROVE WFInductiveDefines(f, Seq(S), Def) +BY StrictSuffixesDetermineDef_WFDefOn, IsStrictSuffixWellFounded, WFInductiveDef, Zenon + +THEOREM SuffixRecursiveSequenceFunctionType == + ASSUME NEW S, NEW T, NEW Def(_,_), NEW f, + T # {}, + StrictSuffixesDetermineDef(S, Def), + WFInductiveDefines(f, Seq(S), Def), + \A g \in [Seq(S) -> T], s \in Seq(S) : Def(g,s) \in T + PROVE f \in [Seq(S) -> T] +<1>1. IsWellFoundedOn(OpToRel(IsStrictSuffix, Seq(S)), Seq(S)) + BY IsStrictSuffixWellFounded, Zenon +<1>2. WFDefOn(OpToRel(IsStrictSuffix, Seq(S)), Seq(S), Def) + BY StrictSuffixesDetermineDef_WFDefOn, Zenon +<1>. QED + BY <1>1, <1>2, WFInductiveDefType, Isa + +(***************************************************************************) +(* The following theorems justify ``primitive recursive'' functions over *) +(* sequences, with a base case for the empty sequence and recursion along *) +(* either the Tail or the Front of a non-empty sequence. *) +(***************************************************************************) + +TailInductiveDefHypothesis(f, S, f0, Def(_,_)) == + f = CHOOSE g : g = [s \in Seq(S) |-> IF s = <<>> THEN f0 ELSE Def(g[Tail(s)], s)] + +TailInductiveDefConclusion(f, S, f0, Def(_,_)) == + f = [s \in Seq(S) |-> IF s = <<>> THEN f0 ELSE Def(f[Tail(s)], s)] + +THEOREM TailInductiveDef == + ASSUME NEW S, NEW Def(_,_), NEW f, NEW f0, + TailInductiveDefHypothesis(f, S, f0, Def) + PROVE TailInductiveDefConclusion(f, S, f0, Def) +<1>. DEFINE Op(h,s) == IF s = <<>> THEN f0 ELSE Def(h[Tail(s)], s) +<1>1. StrictSuffixesDetermineDef(S, Op) + <2>. SUFFICES ASSUME NEW g, NEW h, NEW seq \in Seq(S), + \A suf \in Seq(S) : IsStrictSuffix(suf, seq) => g[suf] = h[suf] + PROVE Op(g, seq) = Op(h, seq) + BY Zenon DEF StrictSuffixesDetermineDef + <2>1. CASE seq = <<>> + BY <2>1 + <2>2. CASE seq # <<>> + BY <2>2, TailIsSuffix, Tail(seq) \in Seq(S), Zenon + <2>. QED BY <2>1, <2>2, Zenon +<1>2. OpDefinesFcn(f, Seq(S), Op) + BY Zenon DEF OpDefinesFcn, TailInductiveDefHypothesis +<1>3. WFInductiveDefines(f, Seq(S), Op) + BY <1>1, <1>2, SuffixRecursiveSequenceFunctionDef, Zenon +<1>. QED BY <1>3, Zenon DEF WFInductiveDefines, TailInductiveDefConclusion + +THEOREM TailInductiveDefType == + ASSUME NEW S, NEW Def(_,_), NEW f, NEW f0, NEW T, + TailInductiveDefConclusion(f, S, f0, Def), + f0 \in T, + \A v \in T, s \in Seq(S) : s # <<>> => Def(v,s) \in T + PROVE f \in [Seq(S) -> T] +<1>. SUFFICES \A s \in Seq(S) : f[s] \in T + BY DEF TailInductiveDefConclusion +<1>1. f[<<>>] \in T + BY <<>> \in Seq(S), Zenon DEF TailInductiveDefConclusion +<1>2. ASSUME NEW seq \in Seq(S), NEW e \in S, f[seq] \in T + PROVE f[Cons(e, seq)] \in T + <2>1. /\ Cons(e, seq) \in Seq(S) + /\ Cons(e, seq) # <<>> + /\ Tail(Cons(e, seq)) = seq + BY ConsProperties, Zenon + <2>2. f[Cons(e, seq)] = Def(f[seq], Cons(e,seq)) + BY <2>1, Zenon DEF TailInductiveDefConclusion + <2>. QED BY <1>2, <2>1, <2>2, Zenon +<1>. QED BY <1>1, <1>2, SequencesInductionCons, Isa + +FrontInductiveDefHypothesis(f, S, f0, Def(_,_)) == + f = CHOOSE g : g = [s \in Seq(S) |-> IF s = <<>> THEN f0 ELSE Def(g[Front(s)], s)] + +FrontInductiveDefConclusion(f, S, f0, Def(_,_)) == + f = [s \in Seq(S) |-> IF s = <<>> THEN f0 ELSE Def(f[Front(s)], s)] + +THEOREM FrontInductiveDef == + ASSUME NEW S, NEW Def(_,_), NEW f, NEW f0, + FrontInductiveDefHypothesis(f, S, f0, Def) + PROVE FrontInductiveDefConclusion(f, S, f0, Def) +<1>. DEFINE Op(h,s) == IF s = <<>> THEN f0 ELSE Def(h[Front(s)], s) +<1>1. StrictPrefixesDetermineDef(S, Op) + <2>. SUFFICES ASSUME NEW g, NEW h, NEW seq \in Seq(S), + \A pre \in Seq(S) : IsStrictPrefix(pre, seq) => g[pre] = h[pre] + PROVE Op(g, seq) = Op(h, seq) + BY Zenon DEF StrictPrefixesDetermineDef, Zenon + <2>1. CASE seq = <<>> + BY <2>1 + <2>2. CASE seq # <<>> + BY <2>2, FrontIsPrefix, FrontProperties + <2>. QED BY <2>1, <2>2, Zenon +<1>2. OpDefinesFcn(f, Seq(S), Op) + BY Zenon DEF OpDefinesFcn, FrontInductiveDefHypothesis +<1>3. WFInductiveDefines(f, Seq(S), Op) + BY <1>1, <1>2, PrefixRecursiveSequenceFunctionDef, Zenon +<1>. QED BY <1>3, Zenon DEF WFInductiveDefines, FrontInductiveDefConclusion + +THEOREM FrontInductiveDefType == + ASSUME NEW S, NEW Def(_,_), NEW f, NEW f0, NEW T, + FrontInductiveDefConclusion(f, S, f0, Def), + f0 \in T, + \A v \in T, s \in Seq(S) : s # <<>> => Def(v,s) \in T + PROVE f \in [Seq(S) -> T] +<1>. SUFFICES \A s \in Seq(S) : f[s] \in T + BY DEF FrontInductiveDefConclusion +<1>1. f[<<>>] \in T + BY <<>> \in Seq(S), Zenon DEF FrontInductiveDefConclusion +<1>2. ASSUME NEW seq \in Seq(S), NEW e \in S, f[seq] \in T + PROVE f[Append(seq, e)] \in T + <2>1. /\ Append(seq, e) \in Seq(S) + /\ Append(seq, e) # <<>> + /\ Front(Append(seq, e)) = seq + BY AppendProperties, FrontLastAppend + <2>2. f[Append(seq, e)] = Def(f[seq], Append(seq, e)) + BY <2>1, Zenon DEF FrontInductiveDefConclusion + <2>. QED BY <1>2, <2>1, <2>2, Zenon +<1>. QED BY <1>1, <1>2, SequencesInductionAppend, Isa + +(**************************************************************************) +(* Recursive characterization of FoldLeft. *) +(**************************************************************************) +THEOREM FoldLeftRecursion == + ASSUME NEW op(_,_), NEW base, NEW S, NEW seq \in Seq(S) + PROVE FoldLeft(op, base, seq) = + IF seq = << >> THEN base + ELSE op(FoldLeft(op, base, Front(seq)), Last(seq)) +<1>1. CASE seq = << >> + BY <1>1, DOMAIN << >> = {}, MapThenFoldSetEmpty, Zenon DEF FoldLeft +<1>2. CASE seq # << >> + <2>. DEFINE f(i) == seq[i] g(i) == Front(seq)[i] + I == 1 .. Len(seq)-1 choose(T) == Max(T) + <2>1. ASSUME NEW T \in SUBSET (DOMAIN seq), T # {} + PROVE choose(T) \in T + BY <2>1, FS_Interval, FS_Subset, MaxIntFinite + <2>2. /\ DOMAIN seq = 1 .. Len(seq) + /\ 1 <= Len(seq) + /\ IsFiniteSet(DOMAIN seq) + BY <1>2, FS_Interval + <2>a. /\ 1 .. Len(seq) # {} + /\ choose(DOMAIN seq) = Len(seq) + /\ (DOMAIN seq) \ {choose(DOMAIN seq)} = I + BY <2>2, 1 \in 1 .. Len(seq), MaxInterval + <2>3. FoldLeft(op, base, seq) = + op(MapThenFoldSet(LAMBDA x,y : op(y,x), base, f, choose, I), + seq[Len(seq)]) + BY <2>1, <2>2, <2>a, MapThenFoldSetNonempty, Isa DEF FoldLeft + <2>4. (DOMAIN Front(seq)) = I + BY <1>2 DEF Front + <2>5. FoldLeft(op, base, Front(seq)) = + MapThenFoldSet(LAMBDA x,y : op(y,x), base, g, choose, I) + BY <2>4 DEF FoldLeft + <2>6. IsFiniteSet(I) + BY FS_Interval + <2>7. \A T \in SUBSET I : T # {} => choose(T) \in T + BY <2>6, FS_Subset, MaxIntFinite + <2>8. \A i \in I : f(i) = g(i) + BY <2>7 DEF Front + <2>. HIDE DEF f, g, choose, I + <2>. QED BY <1>2, <2>3, <2>5, <2>6, <2>7, <2>8, MapThenFoldSetEqual, Isa DEF Last +<1>. QED BY <1>1, <1>2 + +(**************************************************************************) +(* Left folding the empty sequence yields the base value. *) +(**************************************************************************) +THEOREM FoldLeftEmpty == + ASSUME NEW op(_,_), NEW base + PROVE FoldLeft(op, base, <<>>) = base +BY (DOMAIN << >>) = {}, MapThenFoldSetEmpty, Zenon DEF FoldLeft + +(**************************************************************************) +(* Left folding a non-empty sequence recurses on the front, then combines *) +(* the last element of the sequence. *) +(**************************************************************************) +THEOREM FoldLeftNonempty == + ASSUME NEW op(_,_), NEW base, NEW S, NEW seq \in Seq(S), seq # << >> + PROVE FoldLeft(op, base, seq) = op(FoldLeft(op, base, Front(seq)), Last(seq)) +BY FoldLeftRecursion, Isa + +(**************************************************************************) +(* Interaction of FoldLeft and Append. *) +(**************************************************************************) +THEOREM FoldLeftAppend == + ASSUME NEW op(_,_), NEW base, NEW S, NEW seq \in Seq(S), NEW s \in S + PROVE FoldLeft(op, base, Append(seq,s)) = op(FoldLeft(op, base, seq), s) +<1>. DEFINE app == Append(seq, s) +<1>1. /\ app \in Seq(S) + /\ app # << >> + /\ Front(app) = seq + /\ Last(app) = s + BY DEF Front, Last +<1>. HIDE DEF app +<1>2. FoldLeft(op, base, app) = op(FoldLeft(op, base, seq), s) + BY <1>1, FoldLeftNonempty, Isa +<1>. QED BY <1>2 DEF app + +(**************************************************************************) +(* Type of FoldLeft. *) +(**************************************************************************) +THEOREM FoldLeftType == + ASSUME NEW Typ, NEW op(_,_), NEW base \in Typ, NEW seq \in Seq(Typ), + \A t,u \in Typ : op(t,u) \in Typ + PROVE FoldLeft(op, base, seq) \in Typ +<1>. DEFINE P(sq) == FoldLeft(op, base, sq) \in Typ +<1>1. P(<< >>) + BY FoldLeftEmpty, Zenon +<1>2. \A sq \in Seq(Typ), e \in Typ : P(sq) => P(Append(sq, e)) + BY FoldLeftAppend, Isa +<1>. HIDE DEF P +<1>3. \A sq \in Seq(Typ) : P(seq) + BY <1>1, <1>2, SequencesInductionAppend, IsaM("blast") +<1>. QED BY <1>3 DEF P + +(**************************************************************************) +(* Recursive characterization of FoldRight. *) +(**************************************************************************) +THEOREM FoldRightRecursion == + ASSUME NEW op(_,_), NEW base, NEW S, NEW seq \in Seq(S) + PROVE FoldRight(op, seq, base) = + IF seq = << >> THEN base + ELSE op(Head(seq), FoldRight(op, Tail(seq), base)) +<1>1. CASE seq = << >> + BY <1>1, DOMAIN << >> = {}, MapThenFoldSetEmpty, Zenon DEF FoldRight +<1>2. CASE seq # << >> + <2>. DEFINE f(i) == seq[i] g(i) == Tail(seq)[i] + I == 2 .. Len(seq) J == 1 .. Len(seq)-1 + choose(T) == Min(T) bij(j) == j+1 + <2>1. ASSUME NEW T \in SUBSET (DOMAIN seq), T # {} + PROVE choose(T) \in T + BY <2>1, FS_Interval, FS_Subset, MinIntFinite + <2>2. /\ DOMAIN seq = 1 .. Len(seq) + /\ 1 <= Len(seq) + /\ IsFiniteSet(DOMAIN seq) + BY <1>2, FS_Interval + <2>a. /\ 1 .. Len(seq) # {} + /\ choose(DOMAIN seq) = 1 + /\ (DOMAIN seq) \ {choose(DOMAIN seq)} = I + BY <2>2, 1 \in 1 .. Len(seq), MinInterval + <2>3. FoldRight(op, seq, base) = + op(seq[1], MapThenFoldSet(op, base, f, choose, I)) + BY <2>1, <2>2, <2>a, MapThenFoldSetNonempty, Isa DEF FoldRight + <2>4. (DOMAIN Tail(seq)) = J + BY <1>2 + <2>5. FoldRight(op, Tail(seq), base) = + MapThenFoldSet(op, base, g, choose, J) + BY <2>4 DEF FoldRight + <2>6. /\ IsFiniteSet(J) + /\ IsFiniteSet(I) + BY FS_Interval + <2>7. /\ \A T \in SUBSET J : T # {} => choose(T) \in T + /\ \A T \in SUBSET I : T # {} => choose(T) \in T + BY <2>6, FS_Subset, MinIntFinite + <2>8. /\ \A j \in J : bij(j) \in I + /\ \A j1, j2 \in J : bij(j1) = bij(j2) => j1 = j2 + /\ \A j \in J : g(j) = f(bij(j)) + BY <1>2 + <2>9. ASSUME NEW i \in I + PROVE \E j \in J : bij(j) = i + BY <1>2, i-1 \in J + <2>10. ASSUME NEW U \in SUBSET J, U # {} + PROVE bij(choose(U)) = choose({bij(j) : j \in U}) + <3>. DEFINE BU == {bij(j) : j \in U} + <3>1. /\ choose(U) \in U + /\ \A u \in U : choose(U) <= u + BY <2>6, <2>10, FS_Subset, MinIntFinite + <3>2. /\ bij(choose(U)) \in BU + /\ \A u \in BU : bij(choose(U)) <= u + BY <3>1 + <3>. QED BY <3>2, MinInt + <2>. HIDE DEF f, g, choose, I, J, bij + <2>11. MapThenFoldSet(op, base, g, choose, J) = + MapThenFoldSet(op, base, f, choose, I) + BY <2>6, <2>7, <2>8, <2>9, <2>10, MapThenFoldSetBijection, Isa + <2>. QED BY <1>2, <2>3, <2>5, <2>11 +<1>. QED BY <1>1, <1>2 + +(**************************************************************************) +(* Right folding the empty sequence yields the base value. *) +(**************************************************************************) +THEOREM FoldRightEmpty == + ASSUME NEW op(_,_), NEW base + PROVE FoldRight(op, <<>>, base) = base +BY (DOMAIN << >>) = {}, MapThenFoldSetEmpty, Zenon DEF FoldRight + +(**************************************************************************) +(* Right folding a non-empty sequence combines the head of the sequence *) +(* with the result of folding the tail. *) +(**************************************************************************) +THEOREM FoldRightNonempty == + ASSUME NEW op(_,_), NEW base, NEW S, NEW seq \in Seq(S), seq # << >> + PROVE FoldRight(op, seq, base) = op(Head(seq), FoldRight(op, Tail(seq), base)) +BY FoldRightRecursion, Isa + +(**************************************************************************) +(* Interaction of FoldRight and Cons. *) +(**************************************************************************) +THEOREM FoldRightCons == + ASSUME NEW op(_,_), NEW base, NEW S, NEW seq \in Seq(S), NEW s \in S + PROVE FoldRight(op, Cons(s, seq), base) = op(s, FoldRight(op, seq, base)) +<1>. DEFINE cns == Cons(s, seq) +<1>1. /\ cns \in Seq(S) + /\ cns # << >> + /\ Tail(cns) = seq + /\ Head(cns) = s + BY DEF Cons +<1>. HIDE DEF cns +<1>2. FoldRight(op, cns, base) = op(s, FoldRight(op, seq, base)) + BY <1>1, FoldRightNonempty, Isa +<1>. QED BY <1>2 DEF cns + +(**************************************************************************) +(* Type of FoldRight. *) +(**************************************************************************) +THEOREM FoldRightType == + ASSUME NEW Typ, NEW op(_,_), NEW base \in Typ, NEW seq \in Seq(Typ), + \A t,u \in Typ : op(t,u) \in Typ + PROVE FoldRight(op, seq, base) \in Typ +<1>. DEFINE P(sq) == FoldRight(op, sq, base) \in Typ +<1>1. P(<< >>) + BY FoldRightEmpty, Zenon +<1>2. \A sq \in Seq(Typ), e \in Typ : P(sq) => P(Cons(e, sq)) + BY FoldRightCons, Isa +<1>. HIDE DEF P +<1>3. \A sq \in Seq(Typ) : P(seq) + BY <1>1, <1>2, SequencesInductionCons, IsaM("blast") +<1>. QED BY <1>3 DEF P + +(**************************************************************************) +(* FoldLeftDomain and FoldRightDomain cannot be characterized recursively *) +(* in terms of the same operators, we reduce them to MapThenFoldSet. *) +(**************************************************************************) +THEOREM FoldLeftDomainIsMFS == + ASSUME NEW op(_,_), NEW base, NEW S, NEW seq \in Seq(S) + PROVE FoldLeftDomain(op, base, seq) = + MapThenFoldSet(LAMBDA x,y : op(y,x), base, + LAMBDA i : i, LAMBDA T : Max(T), 1 .. Len(seq)) +<1>. DEFINE f(i) == [j \in DOMAIN seq |-> j][i] g(i) == i + choose(T) == Max(T) rop(x,y) == op(y,x) +<1>1. /\ (DOMAIN [i \in DOMAIN seq |-> i]) = 1 .. Len(seq) + /\ \A i \in 1 .. Len(seq) : f(i) = g(i) + OBVIOUS +<1>2. IsFiniteSet(1 .. Len(seq)) + BY FS_Interval +<1>3. \A T \in SUBSET (1 .. Len(seq)) : T # {} => choose(T) \in T + BY <1>2, FS_Subset, MaxIntFinite +<1>. HIDE DEF f, g +<1>4. MapThenFoldSet(rop, base, f, choose, 1 .. Len(seq)) = + MapThenFoldSet(rop, base, g, choose, 1 .. Len(seq)) + BY <1>1, <1>2, <1>3, MapThenFoldSetEqual, Isa +<1>. QED BY <1>1, <1>4 DEF FoldLeftDomain, FoldLeft, f, g + +THEOREM FoldRightDomainIsMFS == + ASSUME NEW op(_,_), NEW base, NEW S, NEW seq \in Seq(S) + PROVE FoldRightDomain(op, seq, base) = + MapThenFoldSet(op, base, + LAMBDA i : i, LAMBDA T : Min(T), 1 .. Len(seq)) +<1>. DEFINE f(i) == [j \in DOMAIN seq |-> j][i] g(i) == i + choose(T) == Min(T) +<1>1. /\ (DOMAIN [i \in DOMAIN seq |-> i]) = 1 .. Len(seq) + /\ \A i \in 1 .. Len(seq) : f(i) = g(i) + OBVIOUS +<1>2. IsFiniteSet(1 .. Len(seq)) + BY FS_Interval +<1>3. \A T \in SUBSET (1 .. Len(seq)) : T # {} => choose(T) \in T + BY <1>2, FS_Subset, MinIntFinite +<1>. HIDE DEF f, g +<1>4. MapThenFoldSet(op, base, f, choose, 1 .. Len(seq)) = + MapThenFoldSet(op, base, g, choose, 1 .. Len(seq)) + BY <1>1, <1>2, <1>3, MapThenFoldSetEqual, Isa +<1>. QED BY <1>1, <1>4 DEF FoldRightDomain, FoldRight, f, g + +============================================================================