Streams & Unique Fixed Points

Nats.dfy

codatatype Stream = Cons(head: nat, tail: Stream)

function Upwards(n: nat): Stream {
   Cons(n, Upwards (n + 1))
}

function Nats() : Stream {
    Upwards(0)
}

function Repeat(n: nat) : Stream {
    Cons(n, Repeat(n))
}

function Add(s: Stream, t: Stream) : Stream {
    Cons(s.head + t.head, Add(s.tail, t.tail))
}

function Mul(s: Stream, t: Stream): Stream {
    Cons(s.head * t.head, Mul(s.tail, t.tail))
}

function Alternate(s: Stream, t: Stream): Stream {
    Cons(s.head, Alternate(t, s.tail))
}

greatest lemma UpwardsUniqueFixedPoint(t: nat, s: Stream) 
   requires s == Cons(t, Add(Repeat(1), s))
   ensures s == Upwards(t)
{}

lemma NatsUniqueFixedPoint(s: Stream)
   requires s == Cons(0, Add(Repeat(1), s))
   ensures s == Nats()
{
    UpwardsUniqueFixedPoint(0, s);
}

greatest lemma UpwardsLemma(t: nat)
  ensures Upwards(t) == Cons(t, Add(Repeat(1), Upwards(t)))
{
   UpwardsLemma(t + 1);   
}

greatest lemma AddLemma(s: Stream, t: Stream)
  ensures Add(s, t) == Add(t, s)
{}

greatest lemma MulRepeatAddLemma(m: nat, n: nat, s: Stream)
  ensures Mul(Repeat(m), Add(Repeat(n), s)) == Add(Repeat(m * n), Mul(Repeat(m), s))
{}

greatest lemma AddSplitLemma(m: nat, n: nat, s: Stream)
  ensures Add(s, Repeat(m + n)) == Add(Add(s, Repeat(m)), Repeat(n))
{}

greatest lemma AlternateLemma(s: Stream, t: Stream, m: nat)
  ensures Alternate(Add(s, Repeat(m)), Add(t, Repeat(m))) == Add(Alternate(s, t), Repeat(m))
{}

lemma UniqueFixedPointApplication()
   ensures Nats() == Alternate(Mul(Repeat(2), Nats()), Add(Mul(Repeat(2), Nats()), Repeat(1)))
{
   var s := Nats();
   var t := Repeat(2);
   var u := Repeat(1);
   calc {
      Alternate(Mul(t, s), Add(Mul(t, s), u));
      Cons(0, Alternate(Add(Mul(t, s), Repeat(1)), (Mul(t, s)).tail));
      Cons(0, Alternate(Add(Mul(t, s), Repeat(1)), (Mul(t, s.tail))));
      Cons(0, Alternate(Add(Mul(t, s), Repeat(1)), (Mul(t, Upwards(0).tail))));
      { UpwardsLemma(0); }
      Cons(0, Alternate(Add(Mul(t, s), Repeat(1)), (Mul(t, (Cons(0, Add(Repeat(1), s))).tail))));
      Cons(0, Alternate(Add(Mul(t, s), Repeat(1)), (Mul(t, Add(Repeat(1), s)))));
      { MulRepeatAddLemma(2, 1, s); }
      Cons(0, Alternate(Add(Mul(t, s), Repeat(1)), Add(t, Mul(Repeat(2), s))));
      { AddLemma(Mul(t, s), t); }
      Cons(0, Alternate(Add(Mul(t, s), Repeat(1)), Add(Mul(t, s), t)));
      { AddSplitLemma(1, 1, Mul(t, s)); }
      Cons(0, Alternate(Add(Mul(t, s), Repeat(1)), Add(Add(Mul(t, s), Repeat(1)), Repeat(1))));
      { AlternateLemma(Mul(t, s), Add(Mul(t, s), Repeat(1)), 1); }
      Cons(0, Add(Alternate(Mul(t, s), Add(Mul(t, s), Repeat(1))), Repeat(1)));
   }
   var m := Alternate(Mul(t, s), Add(Mul(t, s), Repeat(1)));
   assert m == Cons(0, Add(m, Repeat(1)));
   AddLemma(m, Repeat(1));
   assert m == Cons(0, Add(Repeat(1), m));
   NatsUniqueFixedPoint(m);
}

lemma {:induction false} UpwardsUniqueFixedPointAux(k: ORDINAL, t: nat, s: Stream) 
   decreases k
   requires s ==#[k] Cons(t, Add(Repeat(1), s))
   ensures s ==#[k] Upwards(t)
{
 
   calc ==#[k] {
      s;
      Cons(t, Add(Repeat(1), s));
      Cons(t, Add(Repeat(1), Cons(s.head, s.tail)));
      Cons(t, Add(Repeat(1), Cons(t, s.tail)));
      Cons(t, Cons(t+1, Add(Repeat(1), s.tail)));
   }

   if !k.IsLimit { 
      assert s.tail ==#[k-1] Cons(t + 1, Add(Repeat(1), s.tail));
      UpwardsUniqueFixedPointAux(k-1, t + 1, s.tail);
   }
   else {
      if k == 0 {}
      else { 
        assert k.IsLimit;
        assert k > 0;
        var l :| l < k;
        assert s.tail ==#[l] Cons(t + 1, Add(Repeat(1), s.tail));
        UpwardsUniqueFixedPointAux(l, t + 1, s.tail);
      }
   }
}

lemma UpwardsUniqueFixedPoint(t: nat, s: Stream) 
   requires s == Cons(t, Add(Repeat(1), s))
   ensures s == Upwards(t)
{
   forall k | true ensures s ==#[k] Upwards(t) {
        UpwardsUniqueFixedPointAux(k, t, s);
   }
}