Doubly Reversed Flag Proof
We are given a flag that may be up or down, like on an old fashioned mail box, with methods to put the flag up, put it down, and reverse it. There is just one attribute (namely up?) showing whether the flag is up or down. This is illustrated by the Java applet below (due to Grant Malcolm); see also the following OBJ3 specification.
    


th FLAG is sort Flag .
  ops (up_)(dn_)(rev_) : Flag -> Flag .
  op up?_ : Flag -> Bool .
  var F : Flag .
  eq up? up F = true . 
  eq up? dn F = false .
  eq up? rev F = not up? F .
endth

We want to show that if we reverse the flag twice, then the flag returns to its original state, i.e., we want to show that for all flags F, 
    rev rev F = F .
Unfortunately, this equation is not satisfied by all models (i.e., implementations) of FLAG. For example, consider the model whose states are natural numbers, and whose operations are as defined in the following: 

  obj NFLAG is pr EVENAT *(sort Nat to Flag) .
    ops (up_)(dn_)(rev_) : Flag -> Flag .
    op up?_ : Flag -> Bool .
    var F : Flag .
    eq up F = 2 * F . 
    eq dn F = 2 * F + 1 .
    eq rev F = F + 1 .
    eq up? F = even(F) .
  endo
where EVENAT denotes the natural numbers with an even operation; see the applet below (due to Akira Mori). Here, the equation is not satisfied because 
     rev rev F = F + 2 .
For another example, consider the model whose states are "histories" that is, sequences of all methods (i.e., messages) received so far. Then the state after a double reversal of F is the sequence rev rev F, which does not equal the sequence F; see the applet below (due to Akira Mori). Such an implementation (or one a little simpler) would be needed if some other attributes were required, such as the number of methods received, or the last method received.

    

Actually, there is only one implementation (up to isomorphism) where the equation is actually true of all reachable states. There are infinitely many other implementations where the equation is literally false, but always "appears to be true". This means that the equation is observationally or behaviorally satisfied by M, which we write as 
   M  (F : Flag) rev rev F = F
even though 
   M  (F : Flag) rev rev F = F
(ordinary satisfaction) does not hold. Thus, we have to use a technique that allows us to prove behavioral satisfaction, not just ordinary satisfaction. This is why we use coinduction. This situation is actually very common: software engineers often write clever code that doesn't really satisfy its specification, but does always "appear to".

This flag example is about the simplest non-trivial example for coinduction we could think of, but if you are not already familiar with hidden algebra and coinduction, you will have some work to do before you can follow our proof. In that case, you should do some background reading; you might also start with proofs using more familiar techniques, such as induction.

To the first tatami (i.e., proof page) of the formal coinductive proof.
To the Hand Made Tatami demos homepage.
To the Links Project homepage.
To the UCSD Meaning and Computation Group homepage.
13 October 1996