Playing with Partiality in Coq

Library partial

It's well known (or at least it should be), that though coq is a total functional programming langauge, that doesn't stop us from expressing our computations in it. The partiality monad (see e.g. Operational Semantics Using the Partiality Monad) is a pretty natural and enjoyable way to do this.

This work is heavily inspired by the cpdt chapter on streams in its technique: especially the useful trick of manually writing the coinduction predicate. There is actually a brief mention of this monad in cpdt, with a demonstration of its inconveniences. You can see there for that, but for now lets keep the parade sunny --- we won't have any problems in this development.

The actual examples here come from Aaron Stump's blog; I wrote them up in agda earlier using the standard library (http://hpaste.org/78532), but today I actually develop the partiality monad from scratch for them.

Why coq now? Partly for learning, but also it seems to me that proper coinduction (see later, Park's principle) is often a very pretty way to present proofs. However it generates many small and tedious goals which proper automation can dispose of (but would be hell to write manually).

Require Import Setoid.
Require Import Arith Utf8 CpdtTactics List.
Set Implicit Arguments.

A partial value can be thought of as a computation which takes time to run. The actual return value is of the form (now x). For every "unit" of time it took to compute, there is a "later" constructor wrapped around (now x). I write "unit" in quotes because there is actually no requirement that the units of time have any relationship to real-world time.

To analyze partial values, I invent current and future. Once a computation returns, its future is constant --- always the final value.

CoInductive Partial (A : Type) : Type :=
| now : A → Partial A
| later : Partial A → Partial A.

Hint Constructors Partial.

Definition current {A : Type} (x : Partial A) :=
  match x with
    | now x' => Some x'
    | later x' => None
  end.

Definition future {A : Type} (x : Partial A) :=
  match x with
    | now x' => now x'
    | later x' => x'
  end.

Fixpoint future_at {A : Type} n (x : Partial A) :=
  match n with
    | 0 => x
    | S m => future (future_at m x)
  end.

CoFixpoint never (A : Type): Partial A := later (never A).

Coq is extremely cautious when it comes to expanding out coinductive computations, since it doesn't want to loop forever. If we have a coinductive value x, and we rewrite it to the form matchAndDoNothing x, coq will be willing compute the first entry in x for the pattern match. In general, it will expand out only so much of the stream that is actually "used" (as far as I know, this is equivalent to being pattern matched on --- there are no other elimination forms).

Definition matchAndDoNothing {A : Type} (P : Partial A) :=
  match P with
      | now x => now x
      | later y => later y
  end.
Lemma xisx (A : Type) (x : Partial A): x = matchAndDoNothing x.
destruct x; auto.
Qed.

A tactic for tearing apart existentials and conjunctions, since intuition won't do it for us.

Ltac destruct_conj :=
  repeat (
  match goal with
      | [H : (_ ∧ _) |- _] => destruct H
      | [H : prod _ _ |- _] => destruct H
      | [H : ∃ _, _ |- _] => destruct H
  end).

The crush tactic is normally hopeless when it comes to proving existentials, because it won't try to guess which value x to use for exists x, P(x). Sometimes we can hack around this by throwing around a bunch of unknown "existential values" (instantiating x with a ?) and hoping that the ? gets filled. This tactic is often stupid compared to eauto, but it happens to work well enough today.

Ltac ecrush :=
  try (match goal with
      | [ |- ∃ _, _ ] =>
        try solve [eexists; ecrush]
      | [ |- _ ∨ _ ] =>
        try (solve [eleft; ecrush]
                   || solve [eright; ecrush])
      | _ => solve [crush]
  end).

A special tactic for dealing with coinduction proofs where we need to extract info from an existential coinductive variable. A bit of a hack to call destruct_conj, in order to clean up the internals as quickly as possible. In general I'm not being very careful with my tactics, and they have unintended side-effects --- but for just this development it doesn't really matter.

Ltac destruct_exists :=
  try (match goal with
      | [H : ∃ _, _ |- _] =>
        let x := fresh "x"
        with Hx := fresh "Hx"
        in destruct H as (x, Hx);
           destruct_conj;
           destruct x
  end).

A tactic which wraps around aforementioned neverisnever hack to force computation in coinductive types.

Ltac simpl_co x :=
  rewrite (xisx x); simpl;
  try (match goal with
    | [|- context[match ?P with
                   | now x => now x
                   | later y => later y
                 end]]
=> (fold (matchAndDoNothing P); rewrite <- xisx)
  end).

Now that all the useful tactics are declared, back to the actual content. It's not called the partiality monad for nothing.

CoFixpoint bind {A B : Type} (x : Partial A) (f : A → Partial B): Partial B :=
  match x with
    | now x => f x
    | later x => later (bind x f)
  end.

Notation "x >>= f" := (bind x f) (at level 42).

Lemma bind_unit : ∀ A B (a : A) (f : A → Partial B), (now a) >>= f = f a.
intros; simpl_co (now a >>= f); trivial.
Qed.

Hint Rewrite bind_unit.

Equality of partial values (formally, strong bisimulation). Unfortunately, without extensionality = is pretty undesirable for coinductive values; you have to define values the same way for them to be intensionally equal.

CoInductive PEq (A : Type) : Partial A → Partial A → Prop :=
  | wnow : ∀ (x y : A), PEq (now x) (now x)
  | wlater : ∀ x y, PEq x y → PEq (later x) (later y).

Hint Constructors PEq.

Simplify the arguments to Bisimilarity. This is easy to write in terms of simpl_co. For some silly reason I decided I would try to make it more hygienic in its side-effects, which in the end didn't help anybody (and it's still not really hygienic).

Ltac simpl_under_PEq :=
  match goal with
    | [|- PEq ?A ?B] =>
      rewrite (xisx A); simpl;
      rewrite (xisx B); simpl;
      try (match goal with
               | [|- PEq (match ?P with
                                     | now x => now x
                                     | later y => later y
                                   end) _]
                 => fold (matchAndDoNothing P); rewrite <- xisx
                 end);
      try (match goal with
             | [|- PEq _ (match ?Q with
                                  | now x => now x
                                  | later y => later y
                                end)]
               => fold (matchAndDoNothing Q); rewrite <- xisx
                 end)
  end.

Strong bisimulation is an equivalence relation.

Lemma PEq_refl : ∀ {A : Type} (a : Partial A), PEq a a.
cofix. intros.
destruct a; constructor; auto.
Qed.

Hint Resolve PEq_refl.

Lemma PEq_trans: ∀ A (a b c : Partial A), PEq a b → PEq b c → PEq a c.
cofix.
intros.
inversion H; inversion H0; crush.
constructor.
eauto.
Qed.


Lemma PEq_symm : ∀ A (a b : Partial A), PEq a b → PEq b a.
cofix. intros.
inversion H; constructor; eauto.
Qed.

Hint Resolve PEq_symm.

Add Parametric Relation A : (Partial A) (PEq (A:=A))
  reflexivity proved by PEq_refl
  symmetry proved by (PEq_symm (A := A))
  transitivity proved by (PEq_trans (A := A))
    as PEq_rel.

This is the exciting part. Up to now we've been writing proofs with cofix, which is okay but not great: it's very easy to write a good-looking proof and have it get rejected due to guardedness (coq needs to see that the proof "produces" something eventually; see e.g. cpdt if you need background). Automation tools have a big problem with this, since circular proofs are very short and thus easy to compute. Instead of using that ugly jaunt, we will use a proper coinduction predicate.

I think of coinduction in terms of invariants. In order to prove equality, we choose a "bisimulation" R --- basically, an invariant stronger than equality. This invariant is preserved when we step forward in time --- that is to say, when we apply future to both of our arguments (see h2). R (see h1) implies that our immediate observation (current) of the computations is identical; because it is always preserved, there is never a way to tell the streams apart. If we have the base case, that R holds at time zero (for our initial arguments; unnamed and final hypothesis) then we can use this information to construct a value of type PEq.

That was a relatively complete explanation, but here's something simpler. Just looking at h1 and h2, we see that current (future_at n p1) = current (future_at n p2) for all n. We want to choose a predicate R which explains why this crucial equation is true, by proving h1 and h2. Looking at our examples later, this intuition should hopefully crystallize.

The coinduction principle is sometimes referred to as Park's principle.

Section PEq_coind.
  Variable A : Type.
  Variable R : Partial A → Partial A → Prop.
  Hypothesis h1 : ∀ p1 p2, R p1 p2 → current p1 = current p2.
  Hypothesis h2 : ∀ p1 p2, R p1 p2 → R (future p1) (future p2).

  Lemma Simple_Bisim1 : ∀ a b, R (now a) b → PEq (now a) b.
    intros. apply h1 in H. destruct b; crush.
  Qed.

  Lemma Simple_Bisim2 : ∀ a b, R (later a) (now b)
                               → PEq (later a) (now b).
    intros; apply h1 in H; crush.
  Qed.

  Theorem PEq_coind : ∀ p1 p2, R p1 p2 → PEq p1 p2.
  cofix. destruct p1.
  - apply Simple_Bisim1.
  - destruct p2.
    + apply Simple_Bisim2.
    + intros. constructor.
      assert (Heq := h2 H); apply PEq_coind; trivial.
  Qed.
End PEq_coind.

Lemma neverIsNever A : PEq (never A) (never A).
apply (PEq_coind (λ p1 p2, p1 = never A /\ p2 = never A)); crush.
Qed.

I will demonstrate a very simple coinductive proof using plus first.

Definition plus (a b : Partial nat) :=
  a >>= λ a', b >>= λ b',
  now (a' + b').

Hint Rewrite plus_0_r.

Lemma plusNowIsAdd : ∀ x y, plus (now x) (now y) = now (x + y).
  unfold plus; crush.
Qed.

Hint Rewrite plusNowIsAdd.
Hint Resolve now.

Coinduction generates a large number of subgoals (the hypotheses from before). If we choose our predicate right, they are often relatively trivial --- then coind_forceful can dispose of them completely.

Ltac coind_forceful P :=
  apply (PEq_coind P);
  intuition; destruct_exists; ecrush.

Demonstration! Remember that the coinductive predicate is all that really matters. y here is future_at n x where n represents the current time. p1 and p2 are similarly future_at n x and future_at n (plus x (now 0)).

Here is my "intuitive" explanation: y represents the current state of the computation x. Both of our computations wait for y to terminate, so they are equal up to that point. Once y does terminate, the proof is also trivial.

Theorem zeroAdd : ∀ (x : Partial nat), PEq x (plus x (now 0)).
intros. coind_forceful (λ p1 p2, ∃ y, p1 = y ∧ p2 = plus y (now 0)).
Qed.

We can prove very useful and seemingly scary theorems by just choosing the right coinductive predicates. In this case, we step-by-step observe the evolution of a --- once it actually returns a value x then we are left with b x >>= c on both sides and it is obvious they are equal from then on.

Lemma bind_assoc : ∀ A B C (a : Partial A)
                     (b : A → Partial B)
                     (c : B → Partial C),
                     PEq ((a >>= b) >>= c) (a >>= (λ x, b x >>= c)).
intros.
coind_forceful (λ p1 p2,
                (∃ y, p1 = (y >>= b) >>= c ∧ p2 = y >>= (λ x, b x >>= c))
                  ∨
                (p1 = p2)).
Qed.
Hint Resolve bind_assoc.

Lemma PEq_current : ∀ A (p1 p2 : Partial A), PEq p1 p2
                                             → current p1 = current p2.
intros.
destruct p1; destruct p2; inversion H; crush.
Qed.

Lemma PEq_future : ∀ A (p1 p2 : Partial A), PEq p1 p2
                                            → PEq (future p1) (future p2).
intros.
destruct p1; destruct p2; inversion H; crush.
Qed.

Hint Resolve PEq_current PEq_future.

The proof here is much like those before --- how pretty!

Lemma bind_cong : ∀ (α β : Type) (f g : α → Partial β),
                    (∀ (x : α), PEq (f x) (g x)) →
                    ∀ (x : Partial α), PEq (x >>= f) (x >>= g).
intros.
coind_forceful (λ p1 p2,
                PEq p1 p2 ∨ (∃ y, p1 = (y >>= f) ∧ p2 = (y >>= g))).
Qed.

Hint Resolve bind_cong.

A "real" demonstration. In fact there is no coinduction in this development, since we already wrote cong and assoc (which crush will call upon). This is quite a satisfying end, however.

Section RevMap.
  Hypothesis α β : Type.
  Hypothesis f : α → Partial β.
  Fixpoint revmap (l : list α) (l' : list β): Partial (list β) :=
    match l with
      | nil => now l'
      | x :: l => f x >>= λ f_x, revmap l (f_x :: l')
    end.

  Theorem revmapsplits :
    ∀ (l1 l2 : list α) (l' : list β),
      PEq (revmap (l1 ++ l2) l') (revmap l1 l' >>= revmap l2).
    induction l1 as [|x]; crush.
    destruct (f x) as [|p]; crush.

    simpl_under_PEq; constructor.
    transitivity (p >>= (λ f_x : β, revmap l1 (f_x :: l') >>= revmap l2)); auto.
  Qed.
End RevMap.