Require Import List Arith Nat Lia Relations.

From Undecidability.Shared.Libs.DLW.Utils
  Require Import utils_tac utils_list finite php.

From Undecidability.TRAKHTENBROT
  Require Import notations.

Set Implicit Arguments.


Section gfp.


  Variable (M : Type).

  Implicit Type (R T : M M Prop).

  Notation "R ⊆ T" := ( x y, R x y T x y).

  Notation "R 'o' T" := ( x z y, R x y T y z) (at level 58).

  Let incl_trans R S T : R S S T R T.
  Proof. firstorder. Qed.

  Let comp_mono R R' T T' : R R' T T' R o T R' o T'.
  Proof. firstorder. Qed.

  Variable (F : (M M Prop) M M Prop).

  Hypothesis ( : R T, R T F R F T).
  Let sym R := x y R y x.

  Let i := iter F ( _ _ True).

  Let iS n : i (S n) = F (i n).
  Proof. apply iter_S. Qed.

  Let : i 0 = _ _ True.
  Proof. auto. Qed.

  Let i_S n : i (S n) i n.
  Proof.
    unfold i.
    induction n as [ | n IHn ].
    + simpl; auto.
    + intros ? ?.
      rewrite iter_S with (n := n), iter_S.
      apply , IHn.
  Qed.


  Let i_decr n m : n m i m i n.
  Proof. induction 1; auto. Qed.

  Definition gfp x y := n, i n x y.

  Notation I := (@eq M).

  Hypothesis : I F I.
  Let i_refl n : I i n.
  Proof.
    induction n as [ | n IHn ].
    + rewrite ; auto.
    + rewrite iS.
      apply incl_trans with (1 := ), , IHn.
  Qed.


  Let gfp_refl : I gfp.
  Proof. intros ? ? [] ?; apply i_refl; auto. Qed.

  Hypothesis : R, sym (F R) F (sym R).
  Let i_sym n : sym (i n) i n.
  Proof.
    induction n as [ | n IHn ].
    + intros ? ?; rewrite ; simpl; auto.
    + rewrite iS; apply incl_trans with (2 := _ IHn), .
  Qed.


  Let gfp_sym : sym gfp gfp.
  Proof. intros ? ? H ?; apply i_sym, H. Qed.

  Hypothesis : R, F R o F R F (R o R).
  Let i_trans n : i n o i n i n.
  Proof.
    induction n as [ | n IHn ].
    + rewrite ; auto.
    + rewrite iS; apply incl_trans with (1 := @ _), , IHn.
  Qed.


  Let gfp_trans : gfp o gfp gfp.
  Proof.
    intros ? ? H ?; apply i_trans.
    revert H; apply comp_mono; auto.
  Qed.


  Fact gfp_equiv : equiv _ gfp.
  Proof.
    msplit 2.
    + intro; apply gfp_refl; auto.
    + intros ? y ? ? ?; apply gfp_trans; exists y; auto.
    + intros ? ?; apply gfp_sym.
  Qed.


  Fact gfp_greatest R : R F R R gfp.
  Proof.
    intros HR x y H n; revert x y H.
    induction n as [ | n IHn ].
    + now auto.
    + apply incl_trans with (1 := HR).
      rewrite iS; apply ; auto.
  Qed.


  Let gfp_fix1 : F gfp gfp.
  Proof.
    intros ? ? H ?.
    apply i_S; rewrite iS.
    revert H; apply ; auto.
  Qed.



  Definition gfp_continuous := (s : M M Prop),
                        ( n m, n m s m s n)
                      ( x y n, F (s n) x y) F ( x y n, s n x y).

  Variable : gfp_continuous.

  Let gfp_fix0 : gfp F gfp.
  Proof.
    intros ? ? H.
    apply ; auto.
    intro; rewrite iS; apply H.
  Qed.


  Fact gfp_fix x y : F gfp x y gfp x y.
  Proof. split; auto. Qed.


  Let dec R := x y, { R x y } + { R x y }.

  Variable : R, dec R dec (F R).
  Let i_dec n : dec (i n).
  Proof.
    induction n as [ | n IHn ].
    + rewrite ; left; auto.
    + rewrite iS; apply ; auto.
  Qed.




  Let i_dup n m : n < m i n i m k, n k x y, gfp x y i k x y.
  Proof.
    intros .
    generalize (i_decr ) (i_S n); rewrite iS; intros .
    generalize (incl_trans _ _ _ ); intros .
    assert ( p, i n i (p+n)) as .
    { induction p as [ | p IHp ]; auto.
      simpl plus; rewrite iS.
      apply incl_trans with (1 := ), ; auto. }
    intros k Hk x y; split; auto.
    intros H a.
    destruct (le_lt_dec a k).
    + revert H; apply i_decr; auto.
    + replace a with (a-n+n) by .
      apply .
      revert H; apply i_decr; auto.
  Qed.



  Let gfp_reached b : ( n m, n < m b i n i m) ( x y, gfp x y i b x y).
  Proof.
    intros (n & m & & ).
    apply i_dup with (2 := ); auto; try .
  Qed.


  Variable : finite_t M.

  Theorem gfp_finite_t : { n | x y, gfp x y i n x y }.
  Proof.
    destruct finite_t_weak_dec_rels with (1 := )
      as (mR & HmR).
    exists (S (length mR)).
    set (l := map i (list_an 0 (S (length mR)))).
    apply (@gfp_reached (S (length mR))).
    destruct php_upto
      with (R := R T x y, R x y T x y)
           (l := l) (m := mR)
      as (a & R & b & T & c & & ).
    + intros R S H ? ?; rewrite H; tauto.
    + intros R S T ? ?; rewrite , ; tauto.
    + intros R HR.
      unfold l in HR; apply in_map_iff in HR.
      destruct HR as (n & & _).
      destruct (HmR (i n)) as (T & & ).
      * intros x y; destruct (i_dec n x y); tauto.
      * exists T; auto.
    + unfold l; rewrite map_length, list_an_length; auto.
    + unfold l in ; apply map_duplicate_inv in .
      destruct as (a' & n & b' & m & c' & & & & & & ).
      exists n, m; rewrite , ; split; try (intros ? ?; apply ).
      apply list_an_duplicate_inv in ; .
  Qed.



  Theorem gfp_decidable : dec gfp.
  Proof.
    destruct gfp_finite_t as (n & Hn).
    intros x y; destruct (i_dec n x y); [ left | right ];
      rewrite Hn; tauto.
  Qed.


End gfp.