---
source: libtlafmt/tests/format.rs
expression: output
input_file: libtlafmt/tests/corpus/WellFoundedInduction.tla
---
------------------------- MODULE WellFoundedInduction --------------------------
(***************************************************************************)
(* This module contains useful theorems for inductive proofs and recursive *)
(* definitions based on a well-founded ordering. *)
(* *)
(* Most of the statements of the theorems are decomposed in terms of *)
(* definitions. This is done for two reasons: *)
(* *)
(* - It makes it easier for the backends to instantiate the theorems *)
(* when those definitions are not expanded. In fact, at the moment *)
(* the provers can't prove any of those theorems from the theorem *)
(* itself if the definitions are made usable. *)
(* *)
(* - It can be convenient when writing proofs to use those definitions *)
(* rather than having to write out their expansions. *)
(* *)
(* A relation is represented as a set of ordered pairs, where we write *)
(* <<x, y>> \in R instead of x R y. It is more convenient to represent *)
(* relations this way rather than as operators such as < . *)
(* *)
(* Proofs of these theorems appear in module WellFoundedInduction_proofs. *)
(***************************************************************************)
EXTENDS NaturalsInduction
(***************************************************************************)
(* The following defines what it means for a relation R to be transitively *)
(* closed on a set S. In this and other definitions, we think of R as a *)
(* relation on S, meaning that it is a subset of S \X S. However, this is *)
(* not necessary. Our results do not require this as a hypothesis, and it *)
(* is often convenient to apply them when R is a relation on a set *)
(* containing S as a subset. They're even true (though uninteresting) if *)
(* R and S \X S are disjoint sets. *)
(***************************************************************************)
IsTransitivelyClosedOn(R, S) ==
\A i, j, k \in S: (<< i, j >> \in R) /\ (<< j, k >> \in R)
=> (<< i, k >> \in R)
(***************************************************************************)
(* If we think of R as a less-than relation, then R is well founded on S *)
(* iff there is no "infinitely descending" sequence of elements of S. The *)
(* canonical example of a well founded relation is the ordinary less-than *)
(* relation on the natural numbers. *)
(* *)
(* A S with a well-founded ordering is often called well-ordered. *)
(***************************************************************************)
IsWellFoundedOn(R, S) ==
~\E f \in [Nat -> S]: \A n \in Nat: << f[n + 1], f[n] >> \in R
LEMMA EmptyIsWellFounded == \A S : IsWellFoundedOn({}, S)
LEMMA IsWellFoundedOnSubset ==
ASSUME NEW R, NEW S, NEW T \in SUBSET S,
IsWellFoundedOn(R,S)
PROVE IsWellFoundedOn(R,T)
LEMMA IsWellFoundedOnSubrelation ==
ASSUME NEW S, NEW R, NEW RR, RR \cap (S \X S) \subseteq R,
IsWellFoundedOn(R,S)
PROVE IsWellFoundedOn(RR,S)
(***************************************************************************)
(* If we think of R as a less-than relation on S, then the following is *)
(* the set of elements of S that are less than x. *)
(***************************************************************************)
SetLessThan(x, R, S) == {y \in S: << y, x >> \in R}
(***************************************************************************)
(* If we think of R as a less-than relation on S, then R is well-founded *)
(* iff every non-empty subset of S has a minimal element. *)
(***************************************************************************)
THEOREM WFMin ==
ASSUME NEW R, NEW S,
IsWellFoundedOn(R, S),
NEW T, T \subseteq S, T # {}
PROVE \E x \in T : \A y \in T : ~ (<<y, x>> \in R)
THEOREM MinWF ==
ASSUME NEW R, NEW S,
\A T \in SUBSET S : T # {} => \E x \in T : \A y \in T : ~ (<<y, x>> \in R)
PROVE IsWellFoundedOn(R,S)
(***************************************************************************)
(* The two following lemmas are simple consequences of theorem WFMin. *)
(***************************************************************************)
LEMMA WellFoundedIsIrreflexive ==
ASSUME NEW R, NEW S, NEW x \in S,
IsWellFoundedOn(R, S)
PROVE <<x, x>> \notin R
LEMMA WellFoundedIsAsymmetric ==
ASSUME NEW R, NEW S, NEW x \in S, NEW y \in S,
IsWellFoundedOn(R,S),
<<x,y>> \in R, <<y,x>> \in R
PROVE FALSE
(***************************************************************************)
(* The following lemmas are simple facts about operator SetLessThan. *)
(***************************************************************************)
LEMMA WFSetLessThanIrreflexive ==
ASSUME NEW R, NEW S, NEW x \in S,
IsWellFoundedOn(R,S)
PROVE x \notin SetLessThan(x,R,S)
LEMMA SetLessTransitive ==
ASSUME NEW R, NEW S, NEW x \in S, NEW y \in SetLessThan(x,R,S),
IsTransitivelyClosedOn(R, S)
PROVE SetLessThan(y, R, S) \subseteq SetLessThan(x, R, S)
--------------------------------------------------------------------------------
(***************************************************************************)
(* The following theorem is the basis for proof by induction over a *)
(* well-founded set. It generalizes theorem GeneralNatInduction of module *)
(* NaturalsInduction. *)
(***************************************************************************)
THEOREM WFInduction ==
ASSUME NEW P(_), NEW R, NEW S,
IsWellFoundedOn(R, S),
\A x \in S : (\A y \in SetLessThan(x, R, S) : P(y))
=> P(x)
PROVE \A x \in S : P(x)
(***************************************************************************)
(* Theorem WFInductiveDef below justifies recursive definitions based on a *)
(* well-founded ordering. We first prove it with the hypothesis that the *)
(* ordering is transitively closed. We prove the theorem for an arbitrary *)
(* well-founded relation by applying the special case to its transitive *)
(* closure. *)
(***************************************************************************)
WFDefOn(R, S, Def(_,_) ) ==
\A g, h :
\A x \in S :
(\A y \in SetLessThan(x, R, S) : g[y] = h[y])
=> (Def(g,x) = Def(h,x))
OpDefinesFcn(f, S, Def(_,_) ) ==
f = CHOOSE g: g = [x \in S |-> Def(g, x)]
WFInductiveDefines(f, S, Def(_,_) ) ==
f = [x \in S |-> Def(f, x)]
WFInductiveUnique(S, Def(_,_) ) ==
\A g, h : /\ WFInductiveDefines(g, S, Def)
/\ WFInductiveDefines(h, S, Def)
=> (g = h)
THEOREM WFDefOnUnique ==
ASSUME NEW Def(_,_), NEW R, NEW S,
IsWellFoundedOn(R, S), WFDefOn(R, S, Def)
PROVE WFInductiveUnique(S, Def)
LEMMA WFInductiveDefLemma ==
ASSUME NEW Def(_,_), NEW R, NEW S, NEW f,
IsWellFoundedOn(R, S),
IsTransitivelyClosedOn(R, S),
WFDefOn(R, S, Def),
OpDefinesFcn(f, S, Def)
PROVE WFInductiveDefines(f, S, Def)
(***************************************************************************)
(* The following defines the transitive closure of the relation R on S. *)
(* More precisely, it is the transitive closure of the restriction of R *)
(* to S. We give an abstract definition of transitive closure as the *)
(* smallest relation that contains R (restricted to S \X S) and that is *)
(* transitively closed, then prove some relevant properties. *)
(***************************************************************************)
TransitiveClosureOn(R, S) ==
{ss \in S \X S:
\A U \in SUBSET (S \X S):
/\ R \intersect S \X S \subseteq U
/\ IsTransitivelyClosedOn(U, S)
=> ss \in U}
LEMMA TransitiveClosureThm ==
\A R, S :
/\ R \cap S \X S \subseteq TransitiveClosureOn(R, S)
/\ IsTransitivelyClosedOn(TransitiveClosureOn(R, S), S)
LEMMA TransitiveClosureMinimal ==
ASSUME NEW R, NEW S, NEW U \in SUBSET (S \X S),
R \cap S \X S \subseteq U,
IsTransitivelyClosedOn(U,S)
PROVE TransitiveClosureOn(R,S) \subseteq U
(***************************************************************************)
(* The following lemmas are consequences of the two previous ones. The *)
(* first three state closure properties of transitive closure, the fourth *)
(* lemma allows one to chop off a step in the underlying relation for any *)
(* pair in the transitive closure. *)
(***************************************************************************)
LEMMA TCTCTC ==
ASSUME NEW R, NEW S, NEW i \in S, NEW j \in S, NEW k \in S,
<<i,j>> \in TransitiveClosureOn(R,S),
<<j,k>> \in TransitiveClosureOn(R,S)
PROVE <<i,k>> \in TransitiveClosureOn(R,S)
LEMMA TCRTC ==
ASSUME NEW R, NEW S, NEW i \in S, NEW j \in S, NEW k \in S,
<<i,j>> \in TransitiveClosureOn(R,S), <<j,k>> \in R
PROVE <<i,k>> \in TransitiveClosureOn(R,S)
LEMMA RTCTC ==
ASSUME NEW R, NEW S, NEW i \in S, NEW j \in S, NEW k \in S,
<<i,j>> \in R, <<j,k>> \in TransitiveClosureOn(R,S)
PROVE <<i,k>> \in TransitiveClosureOn(R,S)
LEMMA TransitiveClosureChopLast ==
ASSUME NEW R, NEW S, NEW i \in S, NEW k \in S, <<i,k>> \in TransitiveClosureOn(R,S)
PROVE \E j \in S : /\ <<j,k>> \in R
/\ i = j \/ <<i,j>> \in TransitiveClosureOn(R,S)
THEOREM TransitiveClosureWF ==
ASSUME NEW R, NEW S, IsWellFoundedOn(R,S)
PROVE IsWellFoundedOn(TransitiveClosureOn(R, S), S)
THEOREM WFInductiveDef ==
ASSUME NEW Def(_,_), NEW R, NEW S, NEW f,
IsWellFoundedOn(R, S),
WFDefOn(R, S, Def),
OpDefinesFcn(f, S, Def)
PROVE WFInductiveDefines(f, S, Def)
(***************************************************************************)
(* Theorem WFInductiveDef allows us to conclude that a recursively defined *)
(* function satisfies its recursion equation. The following result allows *)
(* us to deduce the range of this function. *)
(***************************************************************************)
THEOREM WFInductiveDefType ==
ASSUME NEW Def(_,_), NEW f, NEW R, NEW S, NEW T,
T # {},
IsWellFoundedOn(R, S),
WFDefOn(R, S, Def),
WFInductiveDefines(f, S, Def),
\A g \in [S -> T], s \in S : Def(g, s) \in T
PROVE f \in [S -> T]
--------------------------------------------------------------------------------
(***************************************************************************)
(* Below are some theorems that allow us to derive some useful *)
(* well-founded relations from a given well-founded relation. First, we *)
(* define the operator OpToRel that constructs a relation (a set of *)
(* ordered pairs) from a relation expressed as an operator. *)
(***************************************************************************)
OpToRel( _\prec_ , S) == {ss \in S \X S: ss[1] \prec ss[2]}
(***************************************************************************)
(* To construct well-founded relations from the less-than relation on the *)
(* natural numbers, we first prove that it is well-founded. *)
(***************************************************************************)
THEOREM NatLessThanWellFounded == IsWellFoundedOn(OpToRel(<, Nat), Nat)
(***************************************************************************)
(* The next definition would be easier to read if we used the TLA+ *)
(* construct {<<x, y>> \in T : ... }. However, TLAPS does not support *)
(* that notation. (It's meaning is rather complicated in the general case *)
(* when T is not a Cartesian product of sets.) *)
(***************************************************************************)
PreImage( f(_) , S, R) == {ss \in S \X S: << f(ss[1]), f(ss[2]) >> \in R}
THEOREM PreImageWellFounded ==
ASSUME NEW S, NEW T, NEW R, NEW f(_),
\A s \in S : f(s) \in T,
IsWellFoundedOn(R, T)
PROVE IsWellFoundedOn(PreImage(f, S, R), S)
(***************************************************************************)
(* We now prove that the lexicographical ordering on the Cartesian product *)
(* of two well-ordered sets is well-ordered. *)
(***************************************************************************)
LexPairOrdering(R1, R2, S1, S2) ==
{ss \in (S1 \X S2) \X (S1 \X S2):
\/ << ss[1][1], ss[2][1] >> \in R1
\/
/\ ss[1][1] = ss[2][1]
/\ << ss[1][2], ss[2][2] >> \in R2}
THEOREM WFLexPairOrdering ==
ASSUME NEW R1, NEW R2, NEW S1, NEW S2,
IsWellFoundedOn(R1, S1),
IsWellFoundedOn(R2, S2)
PROVE IsWellFoundedOn(LexPairOrdering(R1, R2, S1, S2), S1 \X S2)
(***************************************************************************)
(* The preceding theorem generalizes in the obvious way to the Cartesian *)
(* product of a finite number of well-ordered sets. However, the *)
(* statement of the general theorem is rather complicated, so we state it *)
(* for the most useful case: the Cartesian product of n copies of the same *)
(* set. *)
(***************************************************************************)
LexProductOrdering(R, S, n) ==
{ff \in [1..n -> S] \X [1..n -> S]:
\E j \in 1..n:
/\ \A i \in 1..(j - 1): ff[1][i] = ff[2][i]
/\ << ff[1][j], ff[2][j] >> \in R}
THEOREM WFLexProductOrdering ==
ASSUME NEW R, NEW S, NEW n \in Nat,
IsWellFoundedOn(R, S)
PROVE IsWellFoundedOn(LexProductOrdering(R, S, n), [1..n -> S])
================================================================================
\* Modification History
\* Last modified Thu Feb 13 18:14:56 GMT-03:00 2014 by merz
\* Last modified Sun Jan 01 18:39:23 CET 2012 by merz
\* Last modified Wed Nov 23 10:13:18 PST 2011 by lamport