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.