Library cawu.coinduction

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).
   intros Hf Hg.
   rewrite <-compA, Hg.
   rewrite compA, Hf.
   now rewrite compA.

 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).
   intros H x. simpl. apply sup_spec. intros i Hi.
   rewrite (H _ Hi x). apply b. eapply eleq_xsup; eauto.


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.
   transitivity (t (b bot)).
   now apply t.
   apply compat_t.
and actually the greatest one
 Proposition leq_gfp y: y b y y gfp.
   intro H.
   assert (: const y t) by now apply leq_xsup_id, compat_const.
   apply ( bot).

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

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 == .
   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.

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).

Lemma 6.2
 Lemma B_spec f g: f B g f o b b o g.
   split; intro H. rewrite H. intro. apply sup_spec. intros h Hh. apply Hh.
   now apply leq_xsup_id.
 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.
  apply antisym.
   apply leq_gfp. rewrite B_spec. apply compat_t.
   apply leq_t. rewrite <-B_spec. apply gfp_pfp.

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.
   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.

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.

Theorem 10.2
 Theorem accumulate y x: y b (t (cup x y)) y t x.
   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.

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.
   rewrite o_mcap, 2compA, invol.
   rewrite mcap_o, <-2compA, invol.
   now rewrite capC.

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).
   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).

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).
   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.

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.
   rewrite mcap_o. apply cap_spec. split.
    now rewrite <-id_t.
    apply b_t.

Proposition 9.1
 Proposition t_t´: t == .
   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.

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

 Lemma B´S_BS: S, S=T S= o S == B o S.
   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.

Proposition 9.2
 Proposition T´_T: == T.
   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.

 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.

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

Theorem 10.1
 Theorem G_bt: == b o t.
   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.

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

End s.
End paco.