From Undecidability.Shared.Libs.PSL Require Import Prelim.
From Undecidability.Shared.Libs.PSL Require Import EqDec.


Lemma complete_induction (p : Prop) (x : ) :
( x, ( y, y<x p y) p x) p x.

Proof. intros A. apply A. induction x ; intros y B.
exfalso ; .
apply A. intros z C. apply IHx. . Qed.


Lemma size_induction X (f : X ) (p : X Prop) :
  ( x, ( y, f y < f x p y) p x)
   x, p x.

Proof.
  intros IH x. apply IH.
  assert (G: n y, f y < n p y).
  { intros n. induction n.
    - intros y B. exfalso. .
    - intros y B. apply IH. intros z C. apply IHn. . }
  apply G.
Qed.


Lemma size_induction_dep L (X : L Type) (f : l, X l ) (p : l, X l Type) :
  ( l x, ( l' y, f l' y < f l x p l' y) p l x)
   l x, p l x.
Proof.
  intros IH l x. apply IH. intros l'.
  assert (G: n l' y, f l' y < n p l' y).
  { intros n. induction n; intros l'' y.
    - intros B. exfalso. .
    - intros B. apply IH. intros ll z C. eapply IHn. . }
  apply G.
Qed.


Instance nat_le_dec (x y : ) : dec (x y) :=
  le_dec x y.

Lemma size_recursion (X : Type) (sigma : X ) (p : X Type) :
  ( x, ( y, y < x p y) p x)
   x, p x.
Proof.
  intros D x. apply D. revert x.
  enough ( n y, y < n p y) by eauto.
  intros n. induction n; intros y E.
  - exfalso; .
  - apply D. intros x F. apply IHn. .
Qed.


Arguments size_recursion {X} {p} _ _.

Section Iteration.
  Variables (X: Type) (f: X X).

  Fixpoint it (n : ) (x : X) : X :=
    match n with
      | 0 x
      | S n' f (it n' x)
    end.

  Lemma it_ind (p : X Prop) x n :
    p x ( z, p z p (f z)) p (it n x).
  Proof.
    intros A B. induction n; cbn; auto.
  Qed.


  Definition FP (x : X) : Prop := f x = x.

  Lemma it_fp (sigma : X ) x :
    ( n, FP (it n x) (it n x) > (it (S n) x))
    FP (it ( x) x).
  Proof.
    intros A.
    assert (B: n, FP (it n x) x n + (it n x)).
    { intros n; induction n; cbn.
      - auto.
      - destruct IHn as [B|B].
        + left. now rewrite B.
        + destruct (A n) as [C|C].
          * left. now rewrite C.
          * right. cbn in C. . }
    destruct (A ( x)), (B ( x)); auto; exfalso; .
  Qed.

End Iteration.