From Undecidability.Shared.Libs.PSL Require Import Prelim.
From Undecidability.Shared.Libs.PSL Require Import EqDec.
Lemma complete_induction (p : nat -> Prop) (x : nat) :
(forall x, (forall y, y<x -> p y) -> p x) -> p x.
Proof. intros A. apply A. induction x ; intros y B.
exfalso ; lia.
apply A. intros z C. apply IHx. lia. Qed.
Lemma size_induction X (f : X -> nat) (p : X -> Prop) :
(forall x, (forall y, f y < f x -> p y) -> p x) ->
forall x, p x.
Proof.
intros IH x. apply IH.
assert (G: forall n y, f y < n -> p y).
{ intros n. induction n.
- intros y B. exfalso. lia.
- intros y B. apply IH. intros z C. apply IHn. lia. }
apply G.
Qed.
Lemma size_induction_dep L (X : L -> Type) (f : forall l, X l -> nat) (p : forall l, X l -> Type) :
(forall l x, (forall l' y, f l' y < f l x -> p l' y) -> p l x) ->
forall l x, p l x.
Proof.
intros IH l x. apply IH. intros l'.
assert (G: forall n l' y, f l' y < n -> p l' y).
{ intros n. induction n; intros l'' y.
- intros B. exfalso. lia.
- intros B. apply IH. intros ll z C. eapply IHn. lia. }
apply G.
Qed.
Instance nat_le_dec (x y : nat) : dec (x <= y) :=
le_dec x y.
Lemma size_recursion (X : Type) (sigma : X -> nat) (p : X -> Type) :
(forall x, (forall y, sigma y < sigma x -> p y) -> p x) ->
forall x, p x.
Proof.
intros D x. apply D. revert x.
enough (forall n y, sigma y < n -> p y) by eauto.
intros n. induction n; intros y E.
- exfalso; lia.
- apply D. intros x F. apply IHn. lia.
Qed.
Arguments size_recursion {X} sigma {p} _ _.
Section Iteration.
Variables (X: Type) (f: X -> X).
Fixpoint it (n : nat) (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 -> (forall 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 -> nat) x :
(forall n, FP (it n x) \/ sigma (it n x) > sigma (it (S n) x)) ->
FP (it (sigma x) x).
Proof.
intros A.
assert (B: forall n, FP (it n x) \/ sigma x >= n + sigma (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. lia. }
destruct (A (sigma x)), (B (sigma x)); auto; exfalso; lia.
Qed.
End Iteration.
From Undecidability.Shared.Libs.PSL Require Import EqDec.
Lemma complete_induction (p : nat -> Prop) (x : nat) :
(forall x, (forall y, y<x -> p y) -> p x) -> p x.
Proof. intros A. apply A. induction x ; intros y B.
exfalso ; lia.
apply A. intros z C. apply IHx. lia. Qed.
Lemma size_induction X (f : X -> nat) (p : X -> Prop) :
(forall x, (forall y, f y < f x -> p y) -> p x) ->
forall x, p x.
Proof.
intros IH x. apply IH.
assert (G: forall n y, f y < n -> p y).
{ intros n. induction n.
- intros y B. exfalso. lia.
- intros y B. apply IH. intros z C. apply IHn. lia. }
apply G.
Qed.
Lemma size_induction_dep L (X : L -> Type) (f : forall l, X l -> nat) (p : forall l, X l -> Type) :
(forall l x, (forall l' y, f l' y < f l x -> p l' y) -> p l x) ->
forall l x, p l x.
Proof.
intros IH l x. apply IH. intros l'.
assert (G: forall n l' y, f l' y < n -> p l' y).
{ intros n. induction n; intros l'' y.
- intros B. exfalso. lia.
- intros B. apply IH. intros ll z C. eapply IHn. lia. }
apply G.
Qed.
Instance nat_le_dec (x y : nat) : dec (x <= y) :=
le_dec x y.
Lemma size_recursion (X : Type) (sigma : X -> nat) (p : X -> Type) :
(forall x, (forall y, sigma y < sigma x -> p y) -> p x) ->
forall x, p x.
Proof.
intros D x. apply D. revert x.
enough (forall n y, sigma y < n -> p y) by eauto.
intros n. induction n; intros y E.
- exfalso; lia.
- apply D. intros x F. apply IHn. lia.
Qed.
Arguments size_recursion {X} sigma {p} _ _.
Section Iteration.
Variables (X: Type) (f: X -> X).
Fixpoint it (n : nat) (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 -> (forall 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 -> nat) x :
(forall n, FP (it n x) \/ sigma (it n x) > sigma (it (S n) x)) ->
FP (it (sigma x) x).
Proof.
intros A.
assert (B: forall n, FP (it n x) \/ sigma x >= n + sigma (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. lia. }
destruct (A (sigma x)), (B (sigma x)); auto; exfalso; lia.
Qed.
End Iteration.