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.