Library Fixpoints

Require Export Encoding.

First Fixed Point Theorem


Theorem FirstFixedPoint (s : term) : closed s -> exists t, closed t /\ s t == t.

Proof.

  intros cls_s.

  pose (A := lam (s (#0 #0))).

  pose (t := A A).

  exists t.
split; value.
  symmetry.
cbv. crush.
Qed.


Second Fixed Point Theorem


Theorem SecondFixedPoint (s : term) : closed s -> exists t, closed t /\ s (tenc t) == t.

Proof.

  intros cls_s.

  pose (A := lam(s (App #0 (Q #0)))).

  pose (t := A (tenc A)).

  exists t.
split; value.
  symmetry.
unfold t, A.
  transitivity (s (App (tenc A) (Q (tenc A)))).
crush.
  rewrite Q_correct, App_correct.
reflexivity.
Qed.


Goal exists t, closed t /\ t == (tenc t).

Proof.

  destruct (SecondFixedPoint) with ( s := I) as [t [cls_t A]].
value.
  exists t.

  split; value.
symmetry in A. eapply (eqTrans A). crush.
Qed.