Skip to content

more theorems about folds #118

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
muenchnerkindl wants to merge 3 commits into
base: master
Choose a base branch
from
Open

more theorems about folds #118

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
3 commits
Select commit Hold shift + click to select a range
a4cb7fc
more theorems about folds
muenchnerkindl Dec 22, 2025
af9d9ef
more theorems on folds
muenchnerkindl Jan 5, 2026
86c8cd7
theorems for SumFunction
muenchnerkindl Jan 5, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
6 changes: 3 additions & 3 deletions modules/FiniteSetsExt.tla
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -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. *)
Expand Down
75 changes: 75 additions & 0 deletions modules/FiniteSetsExtTheorems.tla
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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


===========================================================================
120 changes: 120 additions & 0 deletions modules/FiniteSetsExtTheorems_proofs.tla
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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

================================================================================
31 changes: 31 additions & 0 deletions modules/FoldsTheorems.tla
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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. *)
Expand Down
77 changes: 77 additions & 0 deletions modules/FoldsTheorems_proofs.tla
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -4,6 +4,7 @@
(*************************************************************************)
EXTENDS Folds, FiniteSets, TLAPS
LOCAL INSTANCE FiniteSetTheorems
LOCAL INSTANCE FunctionTheorems
LOCAL INSTANCE WellFoundedInduction

\* MapThenFoldSet is well-defined
Expand Down Expand Up @@ -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),
Expand Down
Loading
Loading