In Coq, coinduction takes the form of proving A -> A subject to the guardedness constraint to make sure there is progress. This formulation is error prone in that it looks like you have reached the destination at the beginning and in that it is not easy to see guardedness based on the current state in the proof. Are there alternate formulations that are closer to how induction is normally specified, where you have to reach a conclusion that is different from the premise?
An example:
CoInductive stream A : Type :=
| SCons : A -> stream A -> stream A
.
Arguments SCons [A] _ _.
CoInductive sEq A : stream A -> stream A -> Prop :=
| StreamEq x s0 s1 : sEq A s0 s1 -> sEq A (SCons x s0) (SCons x s1)
.
Arguments sEq [A].
Arguments StreamEq [A].
Theorem sEq_refl {A} (s : stream A) : sEq s s.
revert s; cofix f; intros.
destruct s.
apply StreamEq.
apply f.
Qed.
After cofix, you get this bizarre state:
A : Type
f : forall s : stream A, sEq s s
s : stream A
============================
sEq s s
Even worse, it won't detect the error if you try to apply f until you close it with Qed.
So, basically, are there formulations of coinduction that would catch this error early on, instead of waiting for the whole proof to finish and checking the guardedness?
Use the paco library. It provides a greatest fixpoint operator to define coinductive predicates, and that goes with sound reasoning principles, so that the goal doesn't look like A -> A. The library comes with a tutorial (rendered here).
From Paco Require Import paco.
Set Implicit Arguments.
CoInductive stream A : Type := SCons
{ head : A;
tail : stream A
}.
Arguments SCons [A] _ _.
Definition seq_ {A} (r : stream A -> stream A -> Prop) (s1 s2 : stream A) : Prop
:= head s1 = head s2 /\ r (tail s1) (tail s2).
Definition seq {A} : stream A -> stream A -> Prop := paco2 (seq_ (A := A)) bot2.
Theorem seq_refl {A} (s : stream A) : seq s s.
Proof.
revert s; pcofix self; intros.
pfold.
split.
- reflexivity.
- right. apply self.
Qed.