Knaster_Tarski.v

(* 
  
  Dominique code from the Coq mailing list 
  
 *)

Section KNASTER_TARSKI.

Variable A: Type.

Variable eq: A -> A -> Prop.
Variable eq_dec: forall (x y: A), {eq x y} + {~eq x y}.

Variable le: A -> A -> Prop.
Hypothesis le_trans: forall x y z, le x y -> le y z -> le x z.
Hypothesis eq_le: forall x y, eq x y -> le y x.

Definition gt (x y: A) := le y x /\ ~eq y x.

Variable bot: A.
Hypothesis bot_smallest: forall x, le bot x.

Section FIXPOINT.

Variable F: A -> A.
Hypothesis F_mon: forall x y, le x y -> le (F x) (F y).

Lemma iterate_le:
  forall (x: A) (PRE: le x (F x)), le (F x) (F (F x)).
Proof. intros; apply F_mon, PRE. Qed.

Let P x := le x (F x) -> A.

Local Definition G (x : A) (loop : forall y, gt y x -> P y) 
  (hx : le x (F x)) : A.
  refine
    (let x' := F x in 
    match eq_dec x x' with
    | left e   => x
    | right ne => loop x' _ _ 
    end).
  exact (conj hx ne).
  eapply F_mon.
  exact hx.
Defined.

Definition iterate' := Fix_F P G.

Check G.

Lemma iterate'_eq x (a : Acc gt x) PRE : eq (iterate' x a PRE) (F (iterate' x a PRE)).
Proof.
  Check Acc_inv_dep.
  induction a as [x] using Acc_inv_dep. 
  cbn; unfold G.
  destruct (eq_dec x (F x)); eauto.
Qed.

Hypothesis gt_wf: well_founded gt.

Definition fixpoint' := iterate' bot (gt_wf bot) (bot_smallest (F bot)).

Theorem fixpoint'_eq : eq fixpoint' (F fixpoint').
Proof. apply iterate'_eq. Qed.

End FIXPOINT.

End KNASTER_TARSKI.

Check fixpoint'_eq.

Require Import Extraction.

Extraction Inline G.
Recursive Extraction fixpoint'.