# Coinduction All the Way Up

A new abstract theory of coinduction, encompassing
• enhancements of the coinductive proof method
• second order coinduction reasonning about enhancements
• parametrised coinduction, as proposed by Hur et al.
• powerful symmetry arguments
• compatibility and respectfulness
See the corresponding paper on HAL.

Require Export lattice.
Set Implicit Arguments.

# Knaster-Tarski and compatibility

Section s1.
Context {X} {L: CompleteLattice X}.

Variable b: mon X.

## compatible functions

Notation compat f := (f o b b o f) (only parsing).

compositionality properties of compatibility
Lemma compat_id: compat id.
Proof. reflexivity. Qed.

Lemma compat_comp f g: compat f compat g compat (f o g).
Proof.
intros Hf Hg.
rewrite <-compA, Hg.
rewrite compA, Hf.
now rewrite compA.
Qed.

Lemma compat_b: compat b.
Proof. reflexivity. Qed.

Lemma compat_const y: y b y compat (const y).
Proof. now intros ??. Qed.

Lemma compat_sup I (P: I Prop) (f: I mon X):
( i, P i compat (f i)) compat (sup P f).
Proof.
intros H x. simpl. apply sup_spec. intros i Hi.
rewrite (H _ Hi x). apply b. eapply eleq_xsup; eauto.
Qed.

## companion

the companion is the largest compatible function
Definition t := sup (fun fcompat f) id.

Lemma compat_t: compat t.
Proof. now apply compat_sup. Qed.

## Knaster Tarski

we will show that t bot is the greatest fixpoint of b (Theorem 3.3), whence the following definition
Definition gfp := t bot.

gfp is a post-fixpoint
Proposition gfp_pfp: gfp b gfp.
Proof.
transitivity (t (b bot)).
now apply t.
apply compat_t.
Qed.
and actually the greatest one
Proposition leq_gfp y: y b y y gfp.
Proof.
intro H.
assert (: const y t) by now apply leq_xsup_id, compat_const.
apply ( bot).
Qed.

thus a fixpoint, as in Knaster-Tarski's proof
Theorem gfp_fp: gfp == b gfp.
Proof.
apply antisym. apply gfp_pfp.
apply leq_gfp. apply b, gfp_pfp.
Qed.

more properties about t (Lemma 3.2)
Lemma leq_t f: compat f f t.
Proof. intro; now apply leq_xsup_id. Qed.

Lemma id_t: id t.
Proof. apply leq_t, compat_id. Qed.

Lemma b_t: b t.
Proof. apply leq_t, compat_b. Qed.

Lemma tt_t: t o t t.
Proof. apply leq_t, compat_comp; apply compat_t. Qed.

Lemma ft_t f: f t f o t t.
Proof. intro H. rewrite H. apply tt_t. Qed.

Lemma t_idem: t o t == t.
Proof. apply antisym. apply tt_t. now rewrite <-id_t at 2. Qed.

to sum up: gfp = t bot = t gfp t x Corollary 3.4
Corollary t_gfp: t gfp == gfp.
Proof. apply t_idem. Qed.

Corollary gfp_t x: gfp t x.
Proof. now apply t. Qed.

Lemma leq_f_ft f: f f o t.
Proof. now rewrite <-id_t. Qed.
Lemma leq_f_tf f: f t o f.
Proof. now rewrite <-id_t. Qed.

End s1.
Notation compat b f := (f o b b o f) (only parsing).
Global Opaque t.

Section s2.
Context {X} {L: CompleteLattice X}.

gfp is monotone, as a function from mon X to X (be careful: t is not monotone from mon X to mon X)
Instance gfp_leq: Proper (leq ==> leq) gfp.
Proof. intros b Hb. apply leq_gfp. rewrite gfp_fp at 1. apply Hb. Qed.
Instance gfp_weq: Proper (weq ==> weq) gfp := op_leq_weq_1.

Variable b: mon X.

t is intended to be used as an up-to technique, to play with = b o t rather than just b. The following proposition (Equation 11) shows that we would not get anything new by iterating this idea.
Notation := (b o t b).
Notation := (t ).
Notation t := (t b).
Proposition stagnate_t: t == .
Proof.
apply antisym´. apply leq_t. now rewrite compA, compat_t.
intro E. apply leq_t.
rewrite (leq_f_ft b b) at 3.
rewrite compat_t.
rewrite <-compA. rewrite E at 1.
now rewrite tt_t.
Qed.

as a corollary, is a valid enhancement of b (Theorem 3.6)
Corollary enhanced_gfp: gfp b == gfp .
Proof. apply stagnate_t. Qed.

and we get a unique enhanced coinduction principle
Corollary coinduction x: x b (t x) x gfp b.
Proof. intro. rewrite enhanced_gfp. now apply leq_gfp. Qed.

End s2.

# Compatibility up-to: second order reasoning

Section s3.
Context {X} {L: CompleteLattice X}.
Variable b: mon X.

a function whose post-fixpoints are the compatible functions (Definition 6.1)
Program Definition B: mon (mon X) :=
{| body g := sup (fun f f o b b o g) id |}.
Next Obligation.
intros g Hg x. apply sup_leq. 2: reflexivity.
intros f Hf z. now rewrite <-(Hg z).
Qed.

Lemma 6.2
Lemma B_spec f g: f B g f o b b o g.
Proof.
split; intro H. rewrite H. intro. apply sup_spec. intros h Hh. apply Hh.
now apply leq_xsup_id.
Qed.
Lemma Bfb f: B f o b b o f.
Proof. now apply B_spec. Qed.

the companion of b is the greatest fixpoint of B
Theorem companion_gfp: t b == gfp B.
Proof.
apply antisym.
apply leq_gfp. rewrite B_spec. apply compat_t.
apply leq_t. rewrite <-B_spec. apply gfp_pfp.
Qed.

T is the companion of B
Notation T := (t B).
Notation t := (t b).

corresponding second-order coinduction principle
Corollary Coinduction f: f o b b o (T f) f t.
Proof. rewrite <-B_spec, companion_gfp. apply coinduction. Qed.

## properties of the second order companion (Proposition 6.4)

the squaring function is compatible for B (Lemma 6.3)
Program Definition csquare: mon (mon X) := {| body f := f o f |}.
Next Obligation. intros ? ? ?. now apply comp_leq. Qed.
Lemma compat_csquare: compat B csquare.
Proof.
intro f. apply B_spec. change (B f o B f o b b o f o f).
rewrite <-compA, Bfb.
now rewrite compA, Bfb.
Qed.

so is the constant-to-identity function
Lemma compat_constid: const id o B B o const id.
Proof. intro f. now apply B_spec. Qed.

thus T f is always an idempotent function
Proposition TT_T f: T f o T f T f.
Proof. apply (ft_t (leq_t compat_csquare)). Qed.
Proposition id_T f: id T f.
Proof. apply (ft_t (leq_t compat_constid)). Qed.
Corollary T_idem f: T f o T f == T f.
Proof. apply antisym. apply TT_T. now rewrite <-id_T at 2. Qed.

T f always contains f, t, b, and gfp b
Lemma f_Tf f: f T f.
Proof. apply id_t. Qed.
Lemma t_T f: t T f.
Proof. rewrite companion_gfp. apply gfp_t. Qed.
Lemma b_T f: b T f.
Proof. rewrite b_t. apply t_T. Qed.
Lemma gfp_T f x: gfp b T f x.
Proof. rewrite (gfp_t b x). apply t_T. Qed.

helpers, to extract components out of T
Lemma fT_T f g: f T g f o T g T g.
Proof. intro H. rewrite H. apply TT_T. Qed.
Lemma fTf_Tf f: f o T f T f.
Proof. apply fT_T, f_Tf. Qed.
Lemma ftT_T f g: f t f o T g T g.
Proof. intro H. apply fT_T. rewrite H. apply t_T. Qed.
Lemma Tf_T f g: f T g T g o f T g.
Proof. intro H. rewrite H. apply TT_T. Qed.
Lemma Cancel f g x y: f T g x T g y f x T g y.
Proof. intros Hf Hx. rewrite Hx. now apply fT_T. Qed.

# Parametric coinduction: the accumulation rule

Program Definition xaccumulate y x: mon X :=
{| body z := sup (fun _:unit x z) (fun _:unit y) |}.
Next Obligation.
intros z Hz. apply sup_leq.
intros _ H. now rewrite H.
reflexivity.
Qed.

Theorem 10.2
Theorem accumulate y x: y b (t (cup x y)) y t x.
Proof.
intro H. set (f:=xaccumulate y x).
assert (E: y f x) by now apply eleq_xsup with tt.
cut (f t). intro F. now rewrite E.
apply Coinduction. intro z. apply sup_spec. intros _ Hxz.
rewrite H. apply b. apply Cancel. apply t_T.
apply cup_spec. split.
rewrite Hxz. apply b_T.
rewrite E, Hxz. apply Cancel. apply f_Tf. apply b_T.
Qed.

End s3.

# Symmetry arguments

Section symmetry.
we use a class to record the involution: this makes it possible to find the appropriate involution automativally in concrete examples
Context {X} {L: CompleteLattice X} {i: mon X}.
Class Involution := invol: i o i == id.
Context {I: Involution}.

Lemma invol´ x: i (i x) == x.
Proof. apply invol. Qed.

Lemma switch x y: i x y x i y.
Proof. split; (intro H; apply i in H; now rewrite invol´ in H). Qed.

Lemma Switch f g: i o f g f i o g.
Proof. split; (intros H x; apply switch, H). Qed.

Lemma compat_if_fi f: compat i f compat f i.
Proof. intro H; apply Switch. now rewrite compA, <-H, <-compA, invol. Qed.

b is assumed to be of the shape s i s i

Variable s: mon X.
Notation b := (cap s (i o s o i)).
Notation B := (B b).
Notation T := (t B).
Notation t := (t b).

i is compatible
Lemma compat_invol: compat b i.
Proof.
rewrite o_mcap, 2compA, invol.
rewrite mcap_o, <-2compA, invol.
now rewrite capC.
Qed.

thus below t
Lemma invol_t: i t.
Proof. apply leq_t, compat_invol. Qed.

reasoning by symmetry at the first level
Proposition by_symmetry x y: i x x x s (t y) x b (t y).
Proof.
assert(it: i o t == t). apply antisym´. apply ft_t, invol_t. apply Switch.
intros Hx Hxy. apply cap_spec. split. assumption.
apply switch. rewrite Hx, Hxy. now rewrite (it y).
Qed.

reasoning by symmetry at the second level
Proposition by_Symmetry f g: compat i f f o b s o (T g) f o b b o (T g).
Proof.
intros Hf Hfg. apply compat_if_fi in Hf.
rewrite mcap_o. apply cap_spec. split. assumption.
change (f o b i o (s o i o T g)). apply Switch.
rewrite compA, Hf.
rewrite <-compA, compat_invol.
rewrite compA, Hfg, <-2(compA s).
apply comp_leq. reflexivity.
assert (iT: i T g). rewrite invol_t at 1. apply t_T.
rewrite iT at 3. rewrite TT_T.
apply Switch. apply fT_T, iT.
Qed.

End symmetry.
Arguments Involution {X L} i.

# Proof system

Section proof_system.
Context {X} {L: CompleteLattice X}.

Variable b: mon X.
Notation B := (B b).
Notation T := (t B).
Notation t := (t b).

Lemma rule_init y: y t bot y gfp b.
Proof. now intro. Qed.

Lemma rule_done y x: y x y t x.
Proof. now rewrite <-id_t. Qed.

Lemma rule_upto f y x: f t y f (t x) y t x.
Proof. intros Hf Hy. now rewrite <- (ft_t Hf). Qed.

Lemma rule_coind y x: y b (t (cup x y)) y t x.
Proof. apply accumulate. Qed.

End proof_system.

# Coincidence of the greatest respectful and the greatest compatible

Module respectful.
Section s.
Context {X} {L: CompleteLattice X}.

Variable b: mon X.
Notation := (cap b id).
Notation := (t ).
Notation := (B ).
Notation := (t ).
Notation B := (B b).
Notation T := (t B).
Notation t := (t b).

Lemma b_b´t: b o t.
Proof.
rewrite mcap_o. apply cap_spec. split.
now rewrite <-id_t.
apply b_t.
Qed.

Proposition 9.1
Proposition t_t´: t == .
Proof.
apply antisym´.
apply leq_t. rewrite cap_l at 1.
rewrite compat_t. rewrite b_b´t at 1. now rewrite <-compA, tt_t.
intro E. apply leq_t. rewrite b_b´t at 2.
rewrite compA, compat_t.
rewrite E. rewrite <-compA, tt_t.
now rewrite cap_l at 1.
Qed.

Proposition bt_b´t: b o t == o t.
Proof.
apply antisym.
rewrite b_b´t at 1. now rewrite <-compA, tt_t.
now rewrite cap_l.
Qed.

Lemma B´S_BS: S, S=T S= o S == B o S.
Proof.
intros S HS g.
assert (tS: t o S g S g). destruct HS as [->| ->].
apply fT_T, t_T.
rewrite t_t´. apply fT_T, t_T.
assert (St: S g o t S g). destruct HS as [->| ->].
apply Tf_T, t_T.
rewrite t_t´. apply Tf_T, t_T.
apply from_below. intro f.
change (f (S g) f B (S g)). rewrite 2B_spec.
split; intro H.
rewrite b_b´t at 1. rewrite compA, H. rewrite <-compA, St.
now rewrite cap_l.
rewrite cap_l at 1. rewrite H. rewrite b_b´t at 1.
now rewrite <-tS at 2.
Qed.

Proposition 9.2
Proposition T´_T: == T.
Proof.
apply antisym; apply leq_t.
transitivity ( o B o ). now rewrite <-id_t at 3.
rewrite <-compA. rewrite <-B´S_BS by tauto.
rewrite compA, compat_t.
now rewrite <-compA, tt_t.
transitivity (T o o T). now rewrite <-id_t at 3.
rewrite <-compA. rewrite B´S_BS by tauto.
rewrite compA, compat_t.
now rewrite <-compA, tt_t.
Qed.

Proposition B´T´_BT: o == B o T.
Proof. rewrite T´_T. apply B´S_BS. tauto. Qed.

End s.
End respectful.

# Characterisation of Hur et al.' function G using the companion

Module paco.
Section s.

Context {X} {L: CompleteLattice X}.

Program Definition g (b: mon X) x: mon X := {| body y := b (cup x y) |}.
Next Obligation. intros y z H. now rewrite H. Qed.

Program Definition G b: mon X := {| body x := gfp (g b x) |}.
Next Obligation.
intros ? ? ?. apply gfp_leq.
intro. simpl. now rewrite H.
Qed.

Variable b: mon X.
Notation t := (t b).
Notation := (G (b o t)).

Theorem 10.1
Theorem G_bt: == b o t.
Proof.
apply antisym.
assert (E: t).
intro x. apply rule_coind. simpl. now rewrite gfp_fp at 1.
intro x. simpl. rewrite gfp_fp. simpl. apply b.
rewrite (E x). rewrite <-(tt_t b x) at 2. apply t. apply cup_spec. split.
apply id_t. reflexivity.
intro. simpl. apply leq_gfp. simpl. apply b, t, cup_l.
Qed.

Proposition G_upto: == t o .  Proof.
rewrite G_bt. apply antisym. intro. apply id_t.
now rewrite compA, compat_t, <-compA, tt_t.
Qed.

End s.
End paco.