Inductively Defined Sets and Relations
Inductive Definition
We can define sets by giving a start set and some rules on how to add elements depending on the already available elements in the set.
E.g. we can define the set of even numbers by saying the 0 is an even number
and for every even number n the number n + 2 is an even number as well.
Albatross has a special syntax to define sets inductively. E.g. the set of even numbers as defined above in words can be defined as
{(p:{NATURAL}): -- type annotation optional
0 in p,
all(n) n in p ==> n + 2 in p}
The general syntax is
{(p): rule_1, rule_2, ... }
Such an inductive definition defines the least set which satisfies all the
rules. The name of the set (here p) can be chosen arbitrarily.
As opposed to predicate expressions which have the form {x: exp} to define
the set of all elements which satisfy exp, an inductively defined set puts
the name in parentheses and the name does not represent an element, it
represents the whole set.
Usually an inductive definition of a set is used in a function or a constant declaration.
even_numbers: ghost {NATURAL}
-- The set of even numbers.
= {(p): 0 in p, all(n) n in p ==> n + 2 in p}
odd_numbers: ghost {NATURAL}
-- The set of odd numbers.
= {(p): 1 in p, all(n) n in p ==> n + 2 in p}
The two constants even_numbers and odd_numbers must be ghost constants
because no algorithm is given to decide if an element is in the set or not.
There are many sets which satisfy all the rules. E.g. the set of all natural
numbers satisfy all the rules of even_numbers and odd_numbers. The
important thing to remember is that an inductive definition defines
the least set which satisfies the rules.
An important consequence of this fact is that an element can be in an
inductively defined set only if it is in the set because of one of the rules
which define the set. E.g. 1 cannot be in the set of even numbers because it
is not 0 nor is there be any number n so that n + 2 = 1.
Form of the Rules
Each rule of an inductive set definition is an implication chain of the form
all(x,y...) c1 ==> c2 ==> ... ==> e in p
which states that a certain element e is in the set p. The variables
x,y,... and the premises c1, c2, ... are optional. The rule says that
e is in p either unconditionally or under certain conditions.
In the following we define some inductive sets using rules.
A: ANY
(+) (r:{A,A}): ghost {A,A}
-- The transitive closure of 'r'.
-> {(s): all(a,b)
r(a,b) ==> s(a,b)
,
all(a,b,c)
s(a,b) ==> r(b,c) ==> s(a,c)
}
(*) (r:{A,A}): ghost {A,A}
-- The reflexive transitive closure of 'r'.
-> {(s): all(a)
a in r.carrier ==> s(a,a)
,
all(a,b)
r(a,b) ==> s(a,b)
,
all(a,b,c)
s(a,b) ==> r(b,c) ==> s(a,c)
}
path(a:A, f:A->A): ghost {A}
-- The path starting with element 'a' and following the function 'f'.
-> {(p): a in p
,
all(a)
a in p ==> a in f.domain ==> f(a) in p
}
The target always states that a certain element (maybe formed by an expression) is in the inductive set (or relation). The conditions under which the element is in the set might be that other elements are in the set as well or some general conditions not referring to other elements of the set.
The conditions ci in a rule all(x,y,...) c1 ==> c2 ==> ... ==> e in p
might themselves be complete implication chains of the form all(a,b,...) di1
==> di2 ==> ... ei in p where the target always states that some other
element is in the set, possibly under the conditions di1, di2, ... which
must not contain the set p.
I.e. a rule in an inductive set has the general form
all(x,y,...) c1 ==> c2 ==> ... ==> e in p
where each ci is either a general condition not referring to the defined set
or it has the form (or a degenerate variant)
all(a,b,...) di1 ==> di2 ==> ... ==> ei in p
-- di1, di2, ... must not contain p
Using the general form we can define the set of all accessible elements of a relation.
accessibles(r:{A,A}): ghost {A}
-- The set of accessible elements of the relation 'r'.
-> {(p): all(y) (all(x) r(x,y) ==> x in p) ==> y in p}
This definition looks strange at first sight (a) because there are no start elements for the set and (b) because it has some strange nesting of quantifiers. However the definition of this set satisfies the general form of an inductive definition of a set.
Let us try to understand this definition step by step.
The rule all(y) ... ==> y in p states that all y are in the set which
satisfy some condition.
The condition under which y is in p is that all(x) r(x,y) ==> x in p is
valid. I.e. y in p is valid only if all predecessors of y under the
relation r are in p as well.
Reading this carefully uncovers the secret. If an element y in the carrier
of r has no predecessors, then y must be in the set, because all its
predecessors (there are none) are in the set.
Now all elements can be added whose predecessors have no predecessors. This process can be iterated until all accessible elements are exhausted.
If a relation has no elements which have no predecessors i.e. if all elements have predecessors then the set of accessible elements of this relation is empty.
If all elements of the carrier of a relation are accessible then there are no infinitely descending chains in the relation i.e. the relation is wellfounded.
Using the Rules
We know that 2 is an even number. Since it is not 0 there has to be some
n so that n + 2 = 2 is valid. Obviously this n must be zero.
However the proof engine cannot prove 2 in even_numbers fully automatically,
because it is unable to find this n so that n + 2 = 2 is valid. In order
to prove 2 in even_numbers we have to give the proof engine this number
explicitely.
all -- no variables needed
ensure
2 in even_numbers
assert
0 + 2 in even_numbers
end
If the proof engine tries to prove 0 + 2 in even_numbers it realizes that it
can use the second rule of the definition of even_numbers in backward
direction and try to prove 0 in even_numbers which immediately succeeds by
the first rule. Having proved the assertion 0 + 2 in even_numbers the proof
engine evaluates 0 + 2 to 2 and is therefore able to proof the goal 2 in
even_numbers.
The proof engine is able to use the second rule of the definition of
even_numbers iteratively in backward direction because the rule is a
backward rule and it does not create subgoals which are more complicated than
the goal (details see chapter Proof Engine). Therefore the
following theorem is proved automatically by applying the second rule
iteratively in backward direction.
all(n:NATURAL)
require
n in even_numbers
ensure
n + 2 + 2 + 2 in even_numbers
end
In order to prove n + 2 + 2 + 2 in even_numbers it tries to prove n + 2 +
2 in even_numbers, then n + 2 in even_numbers and then n in even_numbers
which is identical to the precondition.
The second rule of the transitive closure all(a,b,c) s(a,b) ==> r(b,c) ==>
s(a,c) cannot be used in backward direction, because the target s(a,c) does
not contain all variables of the rule and the proof engine is unable to
guess missing variables.
However it can be used in forward direction. As soon as there is some s(a,b)
in the context, the proof engine partially specializes the rule to all(c)
r(b,c) ==> s(a,c) which can be used in backward direction.
Assume that we know r(a,b), r(b,c) and r(c,d). This is sufficient to
conclude that (a,d) must be in the transitive closure of r i.e. that
(+r)(a,d) is valid. We can conclude this stepwise by using the following
proof.
all(a,b,c,d:A)
require
r(a,b)
r(b,c)
r(c,d)
ensure
(+r)(a,d)
assert
(+r)(a,b) -- 'r(a,b)' and the first rule
(+r)(a,c) -- partially specialized second rule and 'r(b,c)'
(+r)(a,d) -- partially specialized second rule and 'r(c,d)'
end
Each of the intermediate steps (+r)(a,b) and (+r)(b,c) creates a partial
specialization of the second rule which can be used to prove the next step.
Induction Proof
Inductively defined sets (and relations) can be used to do induction proofs.
Above we made an inductive definition of the set of even numbers by stating
that 0 is an even number and for all even numbers n the number n + 2 is
an even number as well.
However it is also possible to define a recursive function which calculates if a number is even.
is_even(n:NATURAL): BOOLEAN
-- Is the number 'n' even?
-> inspect
n
case 0 then
true
case 0.successor then
false
case n.successor.successor then
n.is_even
Now we want to prove that for all numbers in the set even_numbers the
recursive function evaluates to true.
Let's analyze the situation. If n in even_numbers is valid then n has to
be in this set because of one of the rules which define the set
even_numbers.
The first rule states that n can be in the set if n is zero. In this case the
function is_even evaluates to true.
The second rule states that n can be in the set if there is another number
m which is in the set and n is m + 2. We can use the induction
hypothesis that m.is_even evaluates to true. Then (m + 2).is_even
evaluates to true as well by definition of is_even. Since n is m + 2
we have proved that n.is_even is valid.
The induction proof
all(n:NATURAL)
require
n in even_numbers
ensure
n.is_even
inspect
n in even_numbers
end
does exactly this reasoning automatically. The proof expression inspect n in
even_numbers instructs the compiler to analyze the different cases (rules)
under which n can be in this set.
Even if the proof engine of Albatross does the proof automatically we can provide more details to make the steps more explicit. In the following proof we trigger the different cases explicitely and mention the induction hypothesis and the goals.
all(n:NATURAL)
require
n in even_numbers
ensure
n.is_even
inspect
n in even_numbers
case 0 in even_numbers
-- 'n' is in 'even_numbers because it is zero.
assert
0 in even_numbers -- that is the case
0.is_even -- goal
case all(m) m in even_numbers ==> m + 2 in even_numbers
-- 'n' is in 'even_numbers' because there is some 'm' in
-- 'even_numbers' and 'n' happens to be 'm + 2'.
assert
m in even_numbers -- because of the case
(m + 2) in even_numbers -- because of the case
m.is_even -- induction hypothesis
(m + 2).is_even -- goal
end
This example demonstrates on how to write an induction proof on an inductively defined set with explicit case analysis.
An analysis of a specific case is triggered by case rule where rule spells
out a specific rule of the inductive set. The programmer can freely choose the
names of the variables.
Within a case branch the compiler puts you in an environment with the variables of the rule, all the facts which constitute the rule and for each element which is already in the set because of some condition of the rule a corresponding induction hypothesis.
Induction Principle
Each inductively defined set has an induction principle which is a little bit more complicated to understand than the induction principle associated with an inductive class.
The induction principle of an inductively defined set can be used to prove
that all elements of the set satisfy a certain property. In the following we
use the set p as a representant of the inductively defined set and the set
q as the set of all elements which satisfy the desired property.
If we want to prove that all elements of p satisfy q we basically want to
prove that p is a subset of q.
The set p is an inductively defined set i.e. the set p satisfies all rules
of the definition of p. We say that p is closed under the rules r1, r2,
....
The induction principle states that if the intersection p * q is closed
under the rules then p is a subset of q. Let's understand why this is the
case.
Firstly p * q is certainly a subset of p because every intersection of
sets is a subset of both sets.
Secondly by definition the set p is closed under the rules which define the
set, i.e. p is the least set which satisfies all rules. If p * q satisfies
the rules as well then p * q must be a superset of p.
If p * q is a subset and a superset of p then p = p * q is valid which
implies that p is a subset of q i.e. all elements of p satisfy the
predicate q.
Now let's look at the general form of a definition of an inductively defined set.
{(p): r1, r2, ... }
ri: all(x,y,...) c1 ==> c2 ==> ... ==> e in p
ci: all(a,b,...) d1 ==> d2 ==> ... ==> f in p
I.e. we can regard all rules ri and all conditions cj, dk as functions of
p.
If we want to prove that p * q satisfies the rules we have to prove for all
rules that
all(x,y,...) c1(p*q) ==> c2(p*q) ==> e in p*q
is valid. Because of the form of the ci this condition is equivalent to
all(x,y,...) c1(p) ==> c2(p) ==> ... ==> e in p
==> c1(q) ==> c2(q) ==> ... ==> e in q
using the fact that a and b ==> c is equivalent to a ==> b ==> c and that
by definition p satisfies the rule i.e. e in p does not need to be proved
but can be assumed having c1(p), c2(p), ...
The conditions c1(q), c2(q), ... are induction hypotheses since they state
that we can assume that some other elements f already satisfy the predicate
q and we have to derive that e satisfies q from all premises in this
implication chain.
The clause case all(x,y,...) c1 ==> c2 ==> ... ==> e in p instructs the
compiler to analyze the case that e is in the inductively defined set p
because of this specific rule. The compiler the defines the variables
x,y,... of this specific rule and shifts the conditions c1(p), c2(p),
..., e in p and the induction hypotheses c1(q), c2(q), ... into to
context as assumptions and tries to prove the goal e in q from it.
Note that the goal predicate is of the form {x: goal} i.e. e in q is
by beta reduction equivalent to the goal where the induction variable x is
replaced by e.
Remember the example of the previous chapter where we wanted to prove x in
even_numbers ==> x.is_even. In this case the inductively defined set p is
even_numbers and the goal predicate q is {x: x.is_even}.
Recall the definition of even_numbers: {(p): 0 in p, all(n) n in p ==> n +
2 in p}.
The first case is trivial where the only assumption is 0 in even_numbers and
the corresponding goal is 0 in {x: x.is_even} i.e. 0.is_even.
In the second case we have one variable n and one condition n in p. For
the condition we get a corresponding induction hypothesis of the form n in
q. I.e. for the second case we have to prove
all(n)
require
n in even_numbers -- c1(p)
(n + 2) in even_numbers -- e in p
n.is_even -- c1(q)
ensure
(n + 2).is_even -- e in q
end
More on Induction
In this section we use the following definitions for the set of even numbers and the set of odd numbers.
even_numbers: ghost {NATURAL}
-> {(p): 0 in p, all(n) n in p ==> n + 2 in p}
odd_numbers: ghost {NATURAL}
-> {(p): 1 in p, all(n) n in p ==> n + 2 in p}
If we these definitions are inline with our understanding of even and odd
numbers we should be able to prove that both sets are disjoint i.e. we should
be able to prove all(n,m:NATURAL) n in even_numbers ==> m in odd_numbers ==>
n /= m.
In that example we have a number n which is in the set of even numbers and a
number m which is in the set of odd numbers. We can do induction on either
variable and in order to prove the claim that n and m are different we
have to do induction on both.
Let's use n for the outer induction proof and m for the inner induction
proof. Here is the skeleton if the outer induction proof.
all(n,m:NATURAL)
require
n in even_numbers
m in odd_numbers
ensure
n /= m
inspect
n in even_numbers
case 0 in even_numbers
...
case all(k) k in even_numbers ==> k + 2 in even_numbers
...
end
In doing induction proofs with inductively defined sets it is very important to know the generated goal predicate. For the outer proof the compiler generates the generalized goal
all(m) m in odd_numbers ==> n /= m
and the corresponding goal predicate q
{n: all(m) m in odd_numbers ==> n /= m}
The second rule in the definition of even_numbers has the form all(...) c1
==> e in p. In this case we have c1(p) = k in p where p is
even_numbers.
In order to get the induction hypothesis we have to replace p by q and we
get
k in {n: all(m) m in odd_numbers ==> n /= m}
which evaluates to
all(m) m in odd_numbers ==> k /= m
We can fill the induction hypothesis into the skeleton of the proof.
all(n,m:NATURAL)
require
n in even_numbers
m in odd_numbers
ensure
n /= m
inspect
n in even_numbers
case 0 in even_numbers
...
case all(k) k in even_numbers ==> k + 2 in even_numbers
assert
all(m) m in odd_numbers ==> k /= m -- outer induction
-- hypothesis
m in odd_numbers -- shifted into the context
-- with a fresh variable 'm'
-- goal: k + 2 /= m
...
end
As already explained in the chapter Inductive Types the compiler generates a generalized goal and a corresponding goal predicate but in the cases of the induction prove it provides us with the corresponding variables and the premises shifted into the context.
In our case the goal predicate is {n: all(m) m in odd_numbers ==> n /= m}
which generates for the second case the generalized goal k + 2 in {n:
all(m) m in odd_numbers ==> n /= m} or in evaluated form all(m) m in
odd_numbers ==> k + 2 /= m.
The compiler generates a fresh variable m which shadows the outer one,
shifts the premise m in odd_numbers into the context and tries to prove the
goal k + 2 /= m.
Now we can start with the inner induction in which we analyze the different
cases why m can be in odd_numbers and prove the inner goal k + 2 = m.
For the inner induction proof (induction on m) the compiler generates the
goal predicate {m: k + 2 = m} which does not need any generalization.
The second case of the inner induction proof is the more interesting one. In
the second case we analyze that m is equal to o + 2 for some ther numbers
o. The goal in this case is o + 2 in {m: k + 2 /= m} which evaluates to
k + 2 /= o + 2. The induction hypothesis o in {m: k + 2 = m} which
evaluates to k + 2 /= o is useless in this case.
However we know that o in odd_numbers is valid and can specialized the
induction hypothesis of the outer induction proof to k /= o which is useful
because it implies k + 2 /= o + 2.
Having this we can complete the proof.
all(n,m:NATURAL)
require
n in even_numbers
m in odd_numbers
ensure
n /= m
inspect
n in even_numbers
case 0 in even_numbers
(inspect
m in odd_numbers
)
case all(k) k in even_numbers ==> k + 2 in even_numbers
(assert
all(m) m in odd_numbers ==> k /= m -- outer induction
-- hypothesis
m in odd_numbers -- shifted into the context
-- with a fresh variable 'm'
-- goal: k + 2 /= m
inspect
m in odd_numbers
case all(o) o in odd_numbers ==> o + 2 in odd_numbers
assert
k /= o -- from outer induction hypothesis
k + 2 /= o + 2 -- goal
)
end
Note that the cases 0 and 1 are trivial because 0 /= 1 is valid and for
all numbers x the inequalities 0 /= x + 2 and x + 2 /= 1 are valid which
can be verified by expanding the inequality function /= and by doing
computation of the equality function =.