# Library ip

Set Implicit Arguments.
Unset Strict Implicit.

Require Import Omega.

Ltac inv H := inversion H; subst; clear H.

Notation "p '<=1' q" := (forall x, p x -> q x) (at level 70).

Notation "p '=1' q" := (p <=1 q /\ q <=1 p) (at level 70).

Notation "R '<=2' S" := (forall x y, R x y -> S x y) (at level 70).

Notation "R '=2' S" := (R <=2 S /\ S <=2 R) (at level 70).

# Even numbers

Module Even.

Implicit Types p q : nat -> Prop.

Definition D1 q := q 0.

Definition D2 q := forall n, q n -> q (S (S n)).

Definition DI q := forall p, p 0 -> (forall n, q n -> p n -> p (S (S n))) -> q <=1 p.

Definition DL q := forall p, p 0 -> (forall n, p n -> p (S (S n))) -> q <=1 p.

Definition spec q := D1 q /\ D2 q /\ DI q.

Lemma spec_unique p q :
spec p -> spec q -> p =1 q.

Proof.

firstorder.

Qed.

Lemma DI_to_DL :
DI <=1 DL.

Proof.

firstorder.

Qed.

Lemma DL_to_DI q :
D1 q -> D2 q -> DL q -> DI q.

Proof.

intros A B C p D E.

cut (forall n, q n -> q n /\ p n).

{ firstorder. }
apply C; firstorder.

Qed.

Definition even n := forall p, D1 p -> D2 p -> p n.

Lemma B1 : D1 even.

Proof.

firstorder.

Qed.

Lemma B2 : D2 even.

Proof.

firstorder.

Qed.

Lemma BL : DL even.

Proof.

firstorder.

Qed.

Lemma BI : DI even.

Proof.

apply DL_to_DI.
exact B1. exact B2. exact BL.
Qed.

Lemma specI : spec even.

Proof.

repeat split.
exact B1. exact B2. exact BI.
Qed.

Lemma even_4 : even 4.

Proof.

apply B2, B2, B1.

Qed.

Lemma even_1 :
~ even 1.

Proof.

intros A.
remember 1 as n. revert n A Heqn.
refine (BI _ _).

- intros A.
omega.
- intros n A IH C.
omega.
Qed.

Lemma even_SS n :
even (S (S n)) -> even n.

Proof.

intros A.
remember (S (S n)) as k. revert k A n Heqk.
refine (BI _ _).

- intros n A.
exfalso. omega.
- intros k A IH n C.
inv C. exact A.
Qed.

Goal forall n, even n -> even (S n) -> False.

Proof.

refine (BI _ _).

- apply even_1.

- intros n A IH C.

apply IH, even_SS, C.

Qed.

End Even.

# Reflexive Transitive Closure

We specify R* as the least predicate that is reflexive and closed under left composition with R.

Module RTC.

Section Fix.

Variable X : Type.

Implicit Types R S p q : X -> X -> Prop.

Implicit Types x y z : X.

Definition reflexive R := forall x, R x x.

Definition lcomp R S := forall x y z, R x y -> S y z -> S x z.

Definition least R S := forall p, reflexive p -> lcomp R p -> S <=2 p.

Definition spec R S := reflexive S /\ lcomp R S /\ least R S.

Lemma spec_unique R S S' :
spec R S -> spec R S' -> S =2 S'.

Proof.

firstorder.

Qed.

We define R* as the intersection of all reflexive predicates closed under left composition with R.

Definition star R x y := forall p, reflexive p -> lcomp R p -> p x y.

Lemma star_spec R :
spec R (star R).

Proof.

firstorder.

Qed.

We establish the augmented induction principle for R*.

Definition ind R S := forall p, reflexive p ->
(forall x y z, R x y -> S y z -> p y z -> p x z) ->
S <=2 p.

Lemma spec_to_ind R S :
spec R S -> ind R S.

Proof.

intros [A [B L]] p C D.

pose (q x y := S x y /\ p x y).

cut (S <=2 q).

{ firstorder. }
apply L; firstorder.

Qed.

Lemma ind_to_least :
ind <=2 least.

Proof.

intros R S Ind p A B.
apply Ind; eauto.
Qed.

We establish a further induction principle for R* quantifying only over the first argument.

Definition ind1 R S := forall z (p : X -> Prop),
p z ->
(forall x y, R x y -> S y z -> p y -> p x) ->
forall x, S x z -> p x.

Lemma ind1_ind :
ind1 =2 ind.

Proof.

split; intros R S.

- intros Ind1 p A B x z.
revert x.
refine (Ind1 z _ _ _); eauto.

- intros Ind z p A B x C.

revert x z C A B.

refine (Ind _ _ _); cbv; eauto.

Qed.

End Fix.

End RTC.

Module KnasterTarski.

Section Fix.

Variable X : Type.

Variable F : (X -> Prop) -> (X -> Prop).

Implicit Types p q : X -> Prop.

Variable M : forall p q, p <=1 q -> F p <=1 F q.

Definition I x := forall p, F p <=1 p -> p x.

Lemma pure_induction p :
F p <=1 p -> I <=1 p.

Proof.

intros A x B.
apply B, A.
Qed.

Lemma prefixpoint :
F I <=1 I.

Proof.

intros x A p B.
apply B.
revert A.
apply M.
apply pure_induction, B.

Qed.

Lemma fixpoint :
F I =1 I.

Proof.

split.

- exact prefixpoint.

- apply pure_induction, M, prefixpoint.

Qed.

Lemma I_ub p :
p <=1 I -> F p <=1 I.

Proof.

intros A x B.
apply fixpoint. revert B. apply M, A.
Qed.

Notation "p '/\1' q" := (fun x => p x /\ q x) (at level 50).

Lemma I_conj p :
F (I /\1 p) <=1 I.

Proof.

apply I_ub.
tauto.
Qed.

Lemma augmented_induction p :
F (I /\1 p) <=1 p <-> I <=1 p.

Proof.

split.

- intros A.

cut (I <=1 I /\1 p).

{ intros B x C.
apply B, C. }
apply pure_induction.

eauto using I_conj.

- eauto using I_conj.

Qed.

End Fix.

End KnasterTarski.

Module Termination.

Section Fix.

Variable X : Type.

Implicit Types R : X -> X -> Prop.

Implicit Types p : X -> Prop.

Definition D1 R q := forall x, (R x <=1 q) -> q x.

Definition DL R q := forall p, D1 R p -> q <=1 p.

Definition DI R q := forall p, (forall x, R x <=1 q -> R x <=1 p -> p x) -> q <=1 p.

Definition ter R x := forall p, D1 R p -> p x.

Lemma B1 R :
D1 R (ter R).

Proof.

intros x A p B.
apply B. intros y C. apply A; assumption.
Qed.

Lemma BL R :
DL R (ter R).

Proof.

firstorder.

Qed.

Lemma BI R :
DI R (ter R).

Proof.

intros p A x B.

pose (q x := ter R x /\ p x).

cut (ter R <=1 q).

{ firstorder. }
apply BL.
intros y C. split.
- apply B1.
intros z D. apply C, D.
- apply A; firstorder.

Qed.

Lemma ter_destruct R x :
ter R x -> R x <=1 ter R.

Proof.

revert x.
refine (BI _). auto.
Qed.

End Fix.

End Termination.