[tlaplus] Proving properties of recursive function

--------------------------- MODULE BagWellFounded ---------------------------
EXTENDS TLC, Integers, FiniteSets, Sequences, Bags, TLAPS

\* Definitions

\* Define a finite set of edges
Set_of_all_possible_edges(N) == (1..N) \X (1..N)

\* derive a set of possible multisets (bags) with Set_of_all_possible_edges as (finite) domain
Set_of_all_possible_bags(N) == UNION {[SB -> {n \in Nat : n > 0}] : SB \in SUBSET Set_of_all_possible_edges(N)}

\* this is the original definition of BagSum
LOCAL Bag_sum_zipper(S) ==
LET iter[s \in SUBSET S] ==
IF s = {} THEN 0
ELSE LET x == CHOOSE x \in s : TRUE
IN iter[s \ {x}] + x[2]
IN iter[S]

\* This operator transforms a bag into a set of pairs to work with the function definitions
LOCAL Bag_zip_up(bag) == { <<x, bag[x] * (x[1] + x[2])>> : x \in BagToSet(bag) }

\* This is the function we are using
BagSum(bag) == Bag_sum_zipper(Bag_zip_up(bag))

\* Zipper Set
LOCAL Zipper_Set(N) == { Bag_zip_up(y) : y \in Set_of_all_possible_bags(N) }

\* translation of proofs from WellFoundedInduction to ternary operators
LOCAL DefBagZipSum(fun, xset) == IF xset = {}
THEN 0
ELSE LET x == CHOOSE x \in xset : TRUE
IN fun[xset \ {x}] + x[2]

\* define the subset operator
A \subset B == /\ A \subseteq B
/\ A # B

\* Lemmas
\* We first assure that our definition of the Set_of_all_possible_edges is actually finite
----
LEMMA EdgeSetIsFinite ==
ASSUME NEW N \in Nat
PROVE IsFiniteSet(Set_of_all_possible_edges(N))
BY FS_Interval, FS_Product
DEF Set_of_all_possible_edges

----
\* Then go on and show that subset is actually well founded
LEMMA SubSetIsWellFounded ==
ASSUME NEW N \in Nat,
NEW S, S = Set_of_all_possible_edges(N),
NEW T, T = SUBSET S
PROVE
IsWellFoundedOn(OpToRel(\subset, T), T)
<1>1. T = FiniteSubsetsOf(S) BY FS_FiniteSubsetsOfFinite, EdgeSetIsFinite DEF FiniteSubsetsOf
<1>2. OpToRel(\subset, T) = StrictSubsetOrdering(S)
BY DEF OpToRel, \subset, StrictSubsetOrdering
<1>3. QED
BY <1>1, <1>2, FS_StrictSubsetOrderingWellFounded

----
\* Proof, that bag sum of EmptyBag is zero
LEMMA EmptyBagSumZero == BagSum(EmptyBag) = 0
BY DEF BagSum, EmptyBag, SetToBag , BagToSet, Bag_sum_zipper, Bag_zip_up

\* Proof, that a single element bag sums to this single element
LEMMA _OneElementBagSum_ ==
ASSUME NEW N \in Nat,
NEW S, S = Zipper_Set(N),
NEW x_edge \in Set_of_all_possible_edges(N),
NEW fun,
OpDefinesFcn(fun, S, DefBagZipSum),
WFInductiveDefines(fun, S, DefBagZipSum), \* ASSUME THIS FOR DEVELOPING THE PROOF
fun \in [S -> Nat] \* ASSUME THIS FOR DEVELOPING THE PROOF
PROVE BagSum(SetToBag({x_edge})) = x_edge[1] + x_edge[2]
PROOF
<1> DEFINE ZipElement(edge) == Bag_zip_up(SetToBag({x_edge}))
<1>1. ZipElement(x_edge) = {<<x_edge, x_edge[1] + x_edge[2]>>}
BY DEF Bag_zip_up, SetToBag, BagToSet, Set_of_all_possible_edges
<1>2. ZipElement(x_edge) \in S
BY DEF Zipper_Set, SetToBag, BagToSet, Set_of_all_possible_edges,
Set_of_all_possible_bags
<1>3. fun[ZipElement(x_edge)] \in Nat BY <1>2
<1>4. \A s_elem \in S: Bag_sum_zipper(s_elem) = DefBagZipSum(fun,s_elem)
BY DEF Bag_sum_zipper, DefBagZipSum, OpDefinesFcn, WFInductiveDefines
<1>10. QED BY
DEF BagSum, SetToBag, BagToSet, Set_of_all_possible_edges, Bag_sum_zipper, Bag_zip_up

\* Proof, that addition works
LEMMA SumOfBagsAdditive ==
ASSUME NEW N \in Nat,
NEW A \in Set_of_all_possible_bags(N),
NEW B \in Set_of_all_possible_bags(N)
PROVE
BagSum(A (+) B) = BagSum(A) + BagSum(B)
OMITTED

=============================================================================
\* Modification History
\* Last modified Sun Dec 04 22:20:56 CET 2022 by andreas
\* Created Sun Dec 04 13:44:16 CET 2022 by andreas