Hi,
I am again stuck with proving properties of a recursive function.
I pretty much digged into the wellfounded induction proofs lib, but I do not know how to "connect" the Def(_,_) operator with the function I want to work with.
I tried to derive something from the fold functions, but actually the proofs of the wellfounded induction lib do not include ternary functions like Def(sum.fun,set, transform) which wouldbe necessary to do something like a "transform reduce" operation on a set.
Therefore I just transformed the set I want to process into a set of 2-tuples (like a zip iterator). But this is just to explain the code below.
What I do not understand is how I can make TLAPS understand that my DefBagZipSum actually does what is behind the BagSum. These CHOOSE constructs that appear when expanded by TLAPS are really tricky.
I am stuck in LEMMA OneElementBagSum step <1>4.
I expect that the solution of this will problem will also help with the
LEMM SumOfBagsAdditive.
My BagSum is meant to summarize the indices of graph edges of a graph.
Thank you in advance,
Andreas
--------------------------- 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
--
You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to
tlaplus+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion on the web visit
https://groups.google.com/d/msgid/tlaplus/04d2b7a9-2938-494a-9c0d-be68803dbbd9n%40googlegroups.com.