Hello,
One thing that I think may be tripping you is that in your first definition of equal, you introduce explicit equality constraints between elements of t. Thinking explicitly about the distinction between t, whose elements and opaque, and the type of its observations, option t, that you use to build a bisimilarity on t, can be useful.
If it can help, here are two approches, one by hand, and one with library support. Hopefully the comments help, but don’t hesitate if things remain opaque.
Set Primitive Projections.
CoInductive t : Set := mk { pred : option t }.
(* It's sometimes useful to explicitly distinguish your datatype t,
of which values are completely opaque, from the datatype of their
observation, that offers to the outerworld an observation, in this
case whether they can take a transition to a new [t], or are a distinguished
stuck inhabitant.
*)
Definition t' := option t.
Module byHand.
(* So that we can think of first defining what it means to agree
on a layer of observation.
*)
Definition eqF (R : t -> t -> Prop) : t' -> t' -> Prop :=
fun x y =>
match x,y with
| None, None => True
| Some x, Some y => R x y
| _, _ => False
end.
(* And then tie the knot... Except that the positivity condition
annoys us, so we inline both notions.
*)
Fail CoInductive equal : t -> t -> Prop :=
| SEqual n m : eqF equal (pred n) (pred m) -> equal n m.
CoInductive equal : t -> t -> Prop :=
| ENone n m : pred n = None -> pred m = None -> equal n m
| ESome n m n' m':
pred n = Some n' ->
pred m = Some m' ->
equal n' m' ->
equal n m.
(* Importantly, as stupid as your unfolding law seems
it relies on establishing a bisimulation between both
objects. Here we are going to see that they expose the
same head behavior (either stuck, or can step), and
happen to jump to the exact same state afterwards.
Coq's guard condition is just lenient enough that
we can simply exploit the reflexivity of the relation
in this second case.
Reflexivity is however a proper cofix, and we need to
be careful to not upset the guard behind the scene.
*)
Lemma equal_refl : forall x, equal x x.
Proof.
cofix cih.
intros x.
destruct (pred x) as [x' | ] eqn:eq.
- exact (ESome x x x' x' eq eq (cih x')).
- exact (ENone x x eq eq).
Qed.
(* Once we have that, we just observe one layer, and we are done *)
Lemma unfold_t : forall x, equal {| pred := pred x |} x.
Proof.
intros x.
destruct (pred x) eqn:eq.
- eapply ESome.
reflexivity.
exact eq.
apply equal_refl.
- eapply ENone.
reflexivity.
exact eq.
Qed.
End byHand.
(* My sentiment is that you really should use libraries for that though. They free you from the guard condition, guide you to understand what you are doing, and provide stronger reasoning principles.
Essentially one of:
- paco, based on parameterized coinduction
- coinduction < 1.5, based on the companion in the style of coinduction all the way up
- coinduction >= 1.5, based on the companion built by tower induction.
Here, with the latest (`opam install coq-coinduction`)
*)
From Coinduction Require Import all.
Module withLib.
(* This time we have to define the monotone functor making one observation *)
Definition eqF : mon (t -> t -> Prop).
refine {|
body R t u :=
match pred t, pred u with
| None, None => True
| Some x, Some y => R x y
| _, _ => False
end
|}.
intros ?? LE a b ?.
destruct (pred a), (pred b); auto.
now apply LE.
Defined.
(* We use the library [gfp] construction *)
Notation equal := (gfp eqF).
Infix "≡" := (elem _) (at level 10).
(* If we try to prove the unfolding, we see more explicitly the short coming in the care we want to conclude by reflexivity *)
Lemma eval_equal :
forall x, equal {| pred := pred x |} x.
Proof.
coinduction r cih.
intros x; cbn.
destruct (pred x); auto.
Abort.
(* The base solution is to observe that we went with an incorrect coinduction candidate, we hence restart by extending it with the diagonal *)
Lemma eval_equal :
forall x, equal {| pred := pred x |} x.
Proof.
cut (
(forall x, equal {| pred := pred x |} x) /\
(forall x, equal x x)
).
- intuition.
- coinduction r [cih cih'].
split.
+ intros x; cbn.
destruct (pred x); auto.
+ intros x; cbn.
destruct (pred x); auto.
Qed.
(* But more efficiently, we want to justify that "up-to reflexivity" is a valid coinduction principle *)
#[local] Instance equal_upto_refl (c : Chain eqF) : Reflexive (elem c).
Proof.
apply Reflexive_chain. intros R HR x.
cbn.
now destruct (pred x).
Qed.
(* Allowing for a clean proof *)
Lemma eval_equal' :
forall x, equal {| pred := pred x |} x.
Proof.
coinduction r cih.
intros x; cbn.
destruct (pred x); auto.
Qed.
(* More examples by Damien Pous: https://github.com/damien-pous/coinduction-examples *)
End withLib.