The Coq mailing list

[Brandon Moore <brandon_m_moore AT yahoo.com>]

Hello.

I am trying to define a syntax of proof trees for a system that allows some 
limited coinductive reasoning, where only certain hypotheses of certain proof 
rules should be considered "guarded" positions. I have a definition already 
that is explictly indexed with the sets of available and unguarded 
assumptions, but I'm hoping to using coinduction more directly.

A simplified example reasons about reachability in the transition system 
generated by substitution instances of some fixed set of rules. The basic 
shape of the proof system, ignoring coinduction, looks like this:

Inductive Proof : term -> term -> Prop :=
  | Prim : forall x y, rule x y -> Proof x y
  | Subst : forall v x y, Proof x y -> Proof (subst v x) (subst v y)
  | Trans : forall x y z, Proof x y -> Proof y z -> Proof x z.


The form of coinduction that's allowed permits infinite proof trees as long 
as every infinite path goes infinitely often to the right of an application 
of Trans. In the regualr version, you can remember any subgoal as a 
coinductive hypothesis, which doesn't become available until you are 
somewhere under the right side of a Trans (and remain available after that).


A partially-coinductive definition in Agda behaves exactly as I would like, 
but I haven't been able to define something equivalent in Coq.


data Proof  : Rel term where
  Prim : {x y : term} -> Axiom x y -> Proof x y
  Subst : (v : term){x y : term} -> Proof x y -> Proof (subst v x) (subst v y)
  Trans : (y : term){x z : term} -> Proof x y -> ∞ (Proof y z) -> Proof x z


I have a definition which allows some of this, but it only seems to allow the 
coinductive hypotheses to be used immediately in that position. To 
be faithful, other proof rules should preserve but not establish 
guardedness of a position.

For a self-contained example, here's a simple language of terms and a rule. 
Everything diverges with this rule, so we should be able to prove that 
anything reaches anything else.

Inductive term : Set :=
  Zero | Suc (t : term) | Var.
Fixpoint subst val t := match t with
  | Zero => Zero
  | Suc t' => Suc (subst val t')
  | Var => val
  end.

Inductive rule : term -> term -> Prop :=
  | step : rule Var (Suc Var).

Here's my mixed definition of proofs

Section mixed_proof.
  Variable CProof : term -> term -> Prop.
  Inductive IProof : term -> term -> Prop :=
  | Prim : forall x y, rule x y -> IProof x y
  | Subst : forall x y v, IProof x y -> IProof (subst v x) (subst v y)
  | Trans : forall x y z,
               IProof x y ->
               CProof y z ->
               IProof x z.
End mixed_proof.

CoInductive CProof : term -> term -> Prop :=
  | Wrap : forall x y, IProof CProof x y -> CProof x y.

Notation Proof := IProof CProof

Definition force x y : CProof x y -> Proof x y :=
  fun v => match v with
  | Wrap _ _ p => p
  end.

To remember some point where the goal is Proof, apply force, begin a cofix, 
and apply wrap again.

Fixpoint term_of_nat n := match n with
  | S n' => Suc (term_of_nat n')
  | O => Zero
  end.

Definition nat_diverges n : IProof CProof (term_of_nat n) Zero :=
  force _ _ (
    (cofix nat_div_c n : CProof (term_of_nat n) Zero :=
      Wrap _ _ (Trans _ _ (term_of_nat (S n)) _
        (Subst _ _ _ (term_of_nat n) (Prim _ _ _ step))
        (nat_div_c (S n))))
    n).

The problem is that the assumption has to be used at a position where CProof 
is expected.
It should be possible to prove Var => Zero

by transitivity on Var => Suc Var => Zero,
handling the left case by the primitive rule,
and the right case by substituting [Suc Var/Var]
and then appealing back to the original goal.

The problem is that going through IProof and applying Subst
isn't recognized as preserving guardedness:

Definition diverges : CProof Var Zero.
cofix.
refine
  (Wrap _ _
    (Trans _ _ (Suc Var) _
      (Prim _ _ _ step)
      _)).
refine (Wrap _ _ (Subst _ Var Zero (Suc Var) _)).
refine (force _ _ diverges).
Guarded.

On the other hand, making Subst a constructor in the coinductive type allows
broken proofs like infinite stacks of Subst Var - or in other words, 
incorrectly
consideres Subst to establish rather than just preserving guardedness.

This isn't covered in the tutorial on inductive types or in cdpt. I'm chasing 
references
on mendler-style coinduction and Agda's types, but haven't reached anything I 
see how
to use yet.


Brandon