Recovering [gfp_weq] with the tower-based definition

[YaZko]

Hello,

The lemma [gfp_weq] that was proved over the gfp defined as t b bot (still present in the companion.v file) does not currently have an equivalent for gfp defined as inf (C b). We took a look at it with @nchappe and are a bit stuck.

It would be straightforward if the chain was closed under weq, but as we have discussed, that is not the case currently.

We hence tried to prove it specifically for gfp as follows:

• define two sets to be "in bijection" abusively by the ability to find corresponding equivalent elements,
• prove that two sets in bijections have equivalent infs
• prove that equivalent monotones bs have chains in bijection

We are however having troubles for the third bullet: the induction does not seem to hold when closing by inf, and we don't quite see where to go.

Would you have an insight in the issue by any chance?

P.S. : I think you mentioned that we could transport the result from the companion-gfp to the chain-gfp, but I don't think the two constructions are proved equivalent in the library at the moment, are they?

Best, Nicolas and Yannick

From Coinduction Require Import all.

Section Foo.
    Context (X : Type).
    Context (L: CompleteLattice X).

    Definition bij (U V : X -> Prop) : Prop :=
      (forall u, U u -> exists v, V v /\ u == v) /\
      (forall v, V v -> exists u, U u /\ u == v).

    Lemma foo (U V : X -> Prop):
      bij U V ->
      inf U == inf V.
    Proof.
      intros [F B].
      rewrite weq_spec; split.
      - apply inf_spec.
        intros v INV; apply B in INV as (u & INU & EQ).
        transitivity u.
        now apply leq_infx.
        now rewrite EQ.
      - apply inf_spec.
        intros u INU; apply F in INU as (v & INV & EQ).
        transitivity v.
        now apply leq_infx.
        now rewrite EQ.
    Qed.

    Lemma bar (b b': mon X) :
      b == b' ->
      bij (C b) (C b').
    Proof.
      intros EQb.
      split.
      - intros u INCu.
        induction INCu.
        + destruct IHINCu as (v & INCv & EQ).
          exists (b' v).
          split.
          now constructor.
          rewrite EQ; apply EQb.
        +  (* This doesn't seem to hold *)
          admit.
      - admit.
    Admitted.

    Instance gfp_weq : Proper (weq ==> weq) (gfp (X := X)).
    repeat intro.
    Transparent gfp.
    eapply foo.
    Opaque gfp.
    now apply bar.
    Qed.

[damien-pous]

Hi Yannick & Nicolas,

I've just pushed a commit to the 8.18 branch where I add this lemma, and a few other things. (I give an abstract proof which does not depend on the implementation of the gfp, only on the fact that it yields greatest postfixpoints).

I've also proved related lemmas about the chain, in case you would need them (C_leq and C_weq). And similarly that the companion respects [weq] (companion.t_weq).

Also, I've realised that the characterisation of the companion in terms of the chain in companion.v was done with a redefinition of the final chain (which was there before the file tower.v in fact...). Now it points to [tower.v] for the required defs, and you have the lemma companion.gfp_tower.

Is it enough?

[YaZko]

Hi Damien,

This looks perfect, thanks a lot! We had missed the trick of instantiating the existential with (inf (fun y => C g y /\ exists x, F x /\ x == y)) in C_weq, this makes a lot of sense of course.

Thanks again, Yannick