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.