(*
 * Copyright (c) 2009-2010, Andrew Appel, Robert Dockins and Aquinas Hobor.
 *
 *)

Require Import VST.msl.base.
Require Import VST.msl.ageable.
Require Import VST.msl.predicates_hered.
Require Import VST.msl.subtypes.

Require Import Coq.Wellfounded.Wellfounded.
Require Import Coq.funind.Recdef.

Delimit Scope pred with pred.
Local Open Scope pred.

Set Implicit Arguments.

Definition contractive {A} `{ageable A} (f: pred A -> pred A) : Prop :=
  forall P Q,  |> (P <=> Q)  |-- f P <=> f Q.

Definition nonexpansive {A} `{ageable A} (f: pred A -> pred A) : Prop :=
  forall P Q,  (P <=> Q)  |-- f P <=> f Q.

Definition HOcontractive {A} `{ageable A} (X: Type) (f: (X -> pred A) -> (X -> pred A)) : Prop :=
  forall P Q,  (ALL x:X, |> (P x <=> Q x)) |-- (ALL x:X, f P x <=> f Q x).

Definition HOnonexpansive {A} `{ageable A} (X: Type) (f: (X -> pred A) -> (X -> pred A)) : Prop :=
  forall P Q, (ALL x:X, P x <=> Q x)  |-- (ALL x:X, f P x <=> f Q x).

Module Type HO_REC.

  Parameter HORec : forall {A} `{ageable A} X (f: (X -> pred A) -> (X -> pred A)), X -> pred A.
  Axiom HORec_fold_unfold : forall {A} `{ageable A} X f (H:HOcontractive (X:=X) f),
    HORec f = f (HORec f).

  Parameter Rec : forall {A} `{ageable A} (f: pred A -> pred A), pred A.
  Axiom Rec_fold_unfold : forall {A} `{ageable A} f (H:contractive f),
    Rec f = f (Rec f).

End HO_REC.

Module HoRec : HO_REC.

Section HORec.
  Variable A:Type.
  Variable ag: ageable A.
  Variable X:Type.
  Variable f: (X-> pred A) -> (X -> pred A).

  Fixpoint HORec' (n:nat) : X -> pred A :=
    match n with
    | S n' => f (HORec' n')
    | O    => f (fun _ => FF)
    end.

  Hypothesis Hcont : HOcontractive f.

  Lemma HORec'_unage:   forall j n x a,
        (n >= level a) ->  (HORec' n x a <-> HORec' (j+n) x a).
  Proof.
(* Goal: forall (j n : nat) (x : X) (a : A) (_ : ge n (@level A ag a)), iff (@app_pred A ag (HORec' n x) a) (@app_pred A ag (HORec' (Init.Nat.add j n) x) a) *)
  induction j; intros. simpl; intuition.
(* Goal: iff (@app_pred A ag (HORec' n x) a) (@app_pred A ag (HORec' (Init.Nat.add (S j) n) x) a) *)
  specialize (IHj _ x a H).
(* Goal: iff (@app_pred A ag (HORec' n x) a) (@app_pred A ag (HORec' (Init.Nat.add (S j) n) x) a) *)
   rewrite IHj. clear IHj.
(* Goal: iff (@app_pred A ag (HORec' (Init.Nat.add j n) x) a) (@app_pred A ag (HORec' (Init.Nat.add (S j) n) x) a) *)
  change (S j + n) with (S (j + n)).
(* Goal: iff (@app_pred A ag (HORec' (Init.Nat.add j n) x) a) (@app_pred A ag (HORec' (S (Init.Nat.add j n)) x) a) *)
   assert (j + n >= level a) by omega.
(* Goal: iff (@app_pred A ag (HORec' (Init.Nat.add j n) x) a) (@app_pred A ag (HORec' (S (Init.Nat.add j n)) x) a) *)
   clear H; rename H0 into H.
(* Goal: iff (@app_pred A ag (HORec' (Init.Nat.add j n) x) a) (@app_pred A ag (HORec' (S (Init.Nat.add j n)) x) a) *)
    remember (j+n) as i; clear Heqi.

   assert ((ALL  x : X , (HORec' i x <=> HORec' (S i) x)) (level a)).
(* Goal: @app_pred nat ag_nat (@allp nat ag_nat X (fun x : X => @fash A ag (@andp A ag (@imp A ag (HORec' i x) (HORec' (S i) x)) (@imp A ag (HORec' (S i) x) (HORec' i x))))) (@level A ag a) *)
(* Goal: iff (@app_pred A ag (HORec' i x) a) (@app_pred A ag (HORec' (S i) x) a) *)
   clear - H Hcont.
(* Goal: @app_pred nat ag_nat (@allp nat ag_nat X (fun x : X => @fash A ag (@andp A ag (@imp A ag (HORec' i x) (HORec' (S i) x)) (@imp A ag (HORec' (S i) x) (HORec' i x))))) (@level A ag a) *)
(* Goal: iff (@app_pred A ag (HORec' i x) a) (@app_pred A ag (HORec' (S i) x) a) *)
   remember (level a) as n; clear Heqn.
(* Goal: @app_pred nat ag_nat (@allp nat ag_nat X (fun x : X => @fash A ag (@andp A ag (@imp A ag (HORec' i x) (HORec' (S i) x)) (@imp A ag (HORec' (S i) x) (HORec' i x))))) n *)
(* Goal: iff (@app_pred A ag (HORec' i x) a) (@app_pred A ag (HORec' (S i) x) a) *)
   revert n H; induction i; intros.
(* Goal: @app_pred nat ag_nat (@allp nat ag_nat X (fun x : X => @fash A ag (@andp A ag (@imp A ag (HORec' O x) (HORec' (S O) x)) (@imp A ag (HORec' (S O) x) (HORec' O x))))) n *)
(* Goal: @app_pred nat ag_nat (@allp nat ag_nat X (fun x : X => @fash A ag (@andp A ag (@imp A ag (HORec' (S i) x) (HORec' (S (S i)) x)) (@imp A ag (HORec' (S (S i)) x) (HORec' (S i) x))))) n *)
(* Goal: iff (@app_pred A ag (HORec' i x) a) (@app_pred A ag (HORec' (S i) x) a) *)
   replace n with 0 by omega. clear H.
(* Goal: @app_pred nat ag_nat (@allp nat ag_nat X (fun x : X => @fash A ag (@andp A ag (@imp A ag (HORec' (S i) x) (HORec' (S (S i)) x)) (@imp A ag (HORec' (S (S i)) x) (HORec' (S i) x))))) n *)
(* Goal: iff (@app_pred A ag (HORec' i x) a) (@app_pred A ag (HORec' (S i) x) a) *)
   intro x.
(* Goal: @app_pred nat ag_nat (@fash A ag (@andp A ag (@imp A ag (HORec' O x) (HORec' (S O) x)) (@imp A ag (HORec' (S O) x) (HORec' O x)))) O *)
(* Goal: @app_pred nat ag_nat (@allp nat ag_nat X (fun x : X => @fash A ag (@andp A ag (@imp A ag (HORec' (S i) x) (HORec' (S (S i)) x)) (@imp A ag (HORec' (S (S i)) x) (HORec' (S i) x))))) n *)
(* Goal: iff (@app_pred A ag (HORec' i x) a) (@app_pred A ag (HORec' (S i) x) a) *)
   specialize (Hcont (fun _ => FF) (HORec' 0)).
(* Goal: @app_pred nat ag_nat (@fash A ag (@andp A ag (@imp A ag (HORec' O x) (HORec' (S O) x)) (@imp A ag (HORec' (S O) x) (HORec' O x)))) O *)
(* Goal: @app_pred nat ag_nat (@allp nat ag_nat X (fun x : X => @fash A ag (@andp A ag (@imp A ag (HORec' (S i) x) (HORec' (S (S i)) x)) (@imp A ag (HORec' (S (S i)) x) (HORec' (S i) x))))) n *)
(* Goal: iff (@app_pred A ag (HORec' i x) a) (@app_pred A ag (HORec' (S i) x) a) *)
   specialize (Hcont O).
(* Goal: @app_pred A ag (f (fun _ : X => @FF A ag) x) x' *)
   spec Hcont. repeat (hnf; intros). simpl in *.
(* Goal: and (forall (a' : A) (_ : @necR A ag y a') (_ : False), @app_pred A ag (f (fun _ : X => @FF A ag) b) a') (forall (a' : A) (_ : @necR A ag y a') (_ : @app_pred A ag (f (fun _ : X => @FF A ag) b) a'), False) *)
(* Goal: @app_pred nat ag_nat (@fash A ag (@andp A ag (@imp A ag (HORec' O x) (HORec' (S O) x)) (@imp A ag (HORec' (S O) x) (HORec' O x)))) O *)
(* Goal: @app_pred nat ag_nat (@allp nat ag_nat X (fun x : X => @fash A ag (@andp A ag (@imp A ag (HORec' (S i) x) (HORec' (S (S i)) x)) (@imp A ag (HORec' (S (S i)) x) (HORec' (S i) x))))) n *)
(* Goal: iff (@app_pred A ag (HORec' i x) a) (@app_pred A ag (HORec' (S i) x) a) *)
   rewrite laterR_nat in H; elimtype False; omega.
(* Goal: @app_pred A ag (f (fun _ : X => @FF A ag) x) x' *)
   specialize ( Hcont x).
(* Goal: @app_pred nat ag_nat (@fash A ag (@andp A ag (@imp A ag (HORec' O x) (HORec' (S O) x)) (@imp A ag (HORec' (S O) x) (HORec' O x)))) O *)
(* Goal: @app_pred nat ag_nat (@allp nat ag_nat X (fun x : X => @fash A ag (@andp A ag (@imp A ag (HORec' (S i) x) (HORec' (S (S i)) x)) (@imp A ag (HORec' (S (S i)) x) (HORec' (S i) x))))) n *)
(* Goal: iff (@app_pred A ag (HORec' i x) a) (@app_pred A ag (HORec' (S i) x) a) *)
    simpl in *. auto.
(* Goal: @app_pred nat ag_nat (@allp nat ag_nat X (fun x : X => @fash A ag (@andp A ag (@imp A ag (HORec' (S i) x) (HORec' (S (S i)) x)) (@imp A ag (HORec' (S (S i)) x) (HORec' (S i) x))))) n *)
(* Goal: iff (@app_pred A ag (HORec' i x) a) (@app_pred A ag (HORec' (S i) x) a) *)
   intro x.
(* Goal: @app_pred nat ag_nat (@fash A ag (@andp A ag (@imp A ag (HORec' (S i) x) (HORec' (S (S i)) x)) (@imp A ag (HORec' (S (S i)) x) (HORec' (S i) x)))) n *)
(* Goal: iff (@app_pred A ag (HORec' i x) a) (@app_pred A ag (HORec' (S i) x) a) *)
   apply (Hcont (HORec' i) (HORec' (S i))).
(* Goal: @app_pred nat ag_nat (@allp nat ag_nat X (fun x : X => @box nat ag_nat (@laterM nat ag_nat) (@fash A ag (@andp A ag (@imp A ag (HORec' i x) (HORec' (S i) x)) (@imp A ag (HORec' (S i) x) (HORec' i x)))))) n *)
(* Goal: iff (@app_pred A ag (HORec' i x) a) (@app_pred A ag (HORec' (S i) x) a) *)
   intro s. intros ? ?. apply IHi.  simpl  in H0.  rewrite laterR_nat in H0; omega.
(* Goal: iff (@app_pred A ag (HORec' i x) a) (@app_pred A ag (HORec' (S i) x) a) *)
   clear - H0.
(* Goal: @eq (@pred A H) (f (@HORec A H unit (fun (x : forall _ : unit, @pred A H) (_ : unit) => f (x tt)) tt)) (f (@HORec A H unit (fun (x : forall _ : unit, @pred A H) (_ : unit) => f (x tt)) tt)) *)
(* Goal: @HOcontractive A H unit (fun (x : forall _ : unit, @pred A H) (_ : unit) => f (x tt)) *)
   destruct (H0 x a); auto.
(* Goal: @eq (@pred A H) (f (@HORec A H unit (fun (x : forall _ : unit, @pred A H) (_ : unit) => f (x tt)) tt)) (f (@HORec A H unit (fun (x : forall _ : unit, @pred A H) (_ : unit) => f (x tt)) tt)) *)
(* Goal: @HOcontractive A H unit (fun (x : forall _ : unit, @pred A H) (_ : unit) => f (x tt)) *)
   split; auto.
  Qed.

End HORec.

Definition HORec {A} `{ag: ageable A}  {X: Type} (f:  (X-> pred A) -> (X -> pred A)) (x: X) : pred A :=
     mkPred (fun a : A => app_pred (@HORec' A ag X f (level a) x) a).

Lemma HORec_fold_unfold {A} `{ageable A} : forall X f (H:HOcontractive (X:=X) f),
            HORec f = f (HORec f).
Proof.
(* Goal: forall (A : Type) (H : ageable A) (f : forall _ : @pred A H, @pred A H) (_ : @contractive A H f), @eq (@pred A H) (@Rec A H f) (f (@Rec A H f)) *)
  intros. rename H into ag. rename H0 into Hcont.
(* Goal: @eq (forall _ : X, @pred A ag) (@HORec A ag X f) (f (@HORec A ag X f)) *)
   unfold HORec.
(* Goal: @eq (forall _ : X, @pred A ag) (fun x : X => @mkPred A ag (fun a : A => @app_pred A ag (@HORec' A ag X f (@level A ag a) x) a)) (f (fun x : X => @mkPred A ag (fun a : A => @app_pred A ag (@HORec' A ag X f (@level A ag a) x) a))) *)
    extensionality x.
(* Goal: @eq (@pred A ag) (@mkPred A ag (fun a : A => @app_pred A ag (@HORec' A ag X f (@level A ag a) x) a)) (f (fun x : X => @mkPred A ag (fun a : A => @app_pred A ag (@HORec' A ag X f (@level A ag a) x) a)) x) *)
    cut (forall a, HORec f x a <-> f (HORec f) x a).
(* Goal: forall _ : forall a : A, iff (@app_pred A ag (@HORec A ag X f x) a) (@app_pred A ag (f (@HORec A ag X f) x) a), @eq (@pred A ag) (@mkPred A ag (fun a : A => @app_pred A ag (@HORec' A ag X f (@level A ag a) x) a)) (f (fun x : X => @mkPred A ag (fun a : A => @app_pred A ag (@HORec' A ag X f (@level A ag a) x) a)) x) *)
(* Goal: forall a : A, iff (@app_pred A ag (@HORec A ag X f x) a) (@app_pred A ag (f (@HORec A ag X f) x) a) *)
    intros; apply pred_ext; hnf; firstorder.

(* Goal: forall a : A, iff (@app_pred A ag (@HORec A ag X f x) a) (@app_pred A ag (f (@HORec A ag X f) x) a) *)
    intro a; simpl.
(* Goal: forall (A : Type) (H : ageable A) (f : forall _ : @pred A H, @pred A H) (_ : @contractive A H f), @eq (@pred A H) (@Rec A H f) (f (@Rec A H f)) *)
    case_eq (age1 a); intros.
(* Goal: iff (forall (x' : A) (_ : @necR A ag a x'), @app_pred A ag (@HORec' A ag X f (@level A ag x') x) x') (@app_pred A ag (f (@HORec A ag X f) x) a) *)
(* Goal: iff (forall (x' : A) (_ : @necR A ag a x'), @app_pred A ag (@HORec' A ag X f (@level A ag x') x) x') (@app_pred A ag (f (@HORec A ag X f) x) a) *)
    apply age_level in H.
(* Goal: iff (forall (x' : A) (_ : @necR A ag a x'), @app_pred A ag (@HORec' A ag X f (@level A ag x') x) x') (@app_pred A ag (f (@HORec A ag X f) x) a) *)
(* Goal: iff (forall (x' : A) (_ : @necR A ag a x'), @app_pred A ag (@HORec' A ag X f (@level A ag x') x) x') (@app_pred A ag (f (@HORec A ag X f) x) a) *)
    remember (level a0) as n; clear a0 Heqn.
    destruct
      (@Hcont (HORec' f n) (HORec f) (level a)) with x a; [ | omega | ].
(* Goal: @app_pred A ag (@HORec' A ag X f (@level A ag a) x) a *)
(* Goal: @app_pred A ag (@HORec' A ag X f (@level A ag x') x) x' *)
(* Goal: iff (forall (x' : A) (_ : @necR A ag a x'), @app_pred A ag (@HORec' A ag X f (@level A ag x') x) x') (@app_pred A ag (f (@HORec A ag X f) x) a) *)
   rewrite H. clear a H.
(* Goal: @app_pred nat ag_nat (@allp nat ag_nat X (fun x : X => @box nat ag_nat (@laterM nat ag_nat) (@fash A ag (@andp A ag (@imp A ag (@HORec' A ag X f n x) (@HORec A ag X f x)) (@imp A ag (@HORec A ag X f x) (@HORec' A ag X f n x)))))) (S n) *)
(* Goal: iff (forall (x' : A) (_ : @necR A ag a x'), @app_pred A ag (@HORec' A ag X f (@level A ag x') x) x') (@app_pred A ag (f (@HORec A ag X f) x) a) *)
(* Goal: iff (forall (x' : A) (_ : @necR A ag a x'), @app_pred A ag (@HORec' A ag X f (@level A ag x') x) x') (@app_pred A ag (f (@HORec A ag X f) x) a) *)
    repeat (hnf; intros).
(* Goal: and (@app_pred A ag (@imp A ag (@HORec' A ag X f n b) (@HORec A ag X f b)) y) (@app_pred A ag (@imp A ag (@HORec A ag X f b) (@HORec' A ag X f n b)) y) *)
(* Goal: iff (forall (x' : A) (_ : @necR A ag a x'), @app_pred A ag (@HORec' A ag X f (@level A ag x') x) x') (@app_pred A ag (f (@HORec A ag X f) x) a) *)
(* Goal: iff (forall (x' : A) (_ : @necR A ag a x'), @app_pred A ag (@HORec' A ag X f (@level A ag x') x) x') (@app_pred A ag (f (@HORec A ag X f) x) a) *)
    simpl in H. apply laterR_level in H. simpl in H. unfold natLevel in H.
(* Goal: and (@app_pred A ag (@imp A ag (@HORec' A ag X f n b) (@HORec A ag X f b)) y) (@app_pred A ag (@imp A ag (@HORec A ag X f b) (@HORec' A ag X f n b)) y) *)
(* Goal: iff (forall (x' : A) (_ : @necR A ag a x'), @app_pred A ag (@HORec' A ag X f (@level A ag x') x) x') (@app_pred A ag (f (@HORec A ag X f) x) a) *)
(* Goal: iff (forall (x' : A) (_ : @necR A ag a x'), @app_pred A ag (@HORec' A ag X f (@level A ag x') x) x') (@app_pred A ag (f (@HORec A ag X f) x) a) *)
    assert (n >= level y) by omega.
(* Goal: and (@app_pred A ag (@imp A ag (@HORec' A ag X f n b) (@HORec A ag X f b)) y) (@app_pred A ag (@imp A ag (@HORec A ag X f b) (@HORec' A ag X f n b)) y) *)
(* Goal: iff (forall (x' : A) (_ : @necR A ag a x'), @app_pred A ag (@HORec' A ag X f (@level A ag x') x) x') (@app_pred A ag (f (@HORec A ag X f) x) a) *)
(* Goal: iff (forall (x' : A) (_ : @necR A ag a x'), @app_pred A ag (@HORec' A ag X f (@level A ag x') x) x') (@app_pred A ag (f (@HORec A ag X f) x) a) *)
    clear - Hcont H1.
(* Goal: forall (A : Type) (H : ageable A) (f : forall _ : @pred A H, @pred A H) (_ : @contractive A H f), @eq (@pred A H) (@Rec A H f) (f (@Rec A H f)) *)
    split; hnf; simpl; intros.
(* Goal: @app_pred A ag (@HORec' A ag X f (@level A ag x') b) x' *)
(* Goal: @app_pred A ag (@HORec' A ag X f n b) a' *)
(* Goal: iff (forall (x' : A) (_ : @necR A ag a x'), @app_pred A ag (@HORec' A ag X f (@level A ag x') x) x') (@app_pred A ag (f (@HORec A ag X f) x) a) *)
(* Goal: iff (forall (x' : A) (_ : @necR A ag a x'), @app_pred A ag (@HORec' A ag X f (@level A ag x') x) x') (@app_pred A ag (f (@HORec A ag X f) x) a) *)
    generalize (necR_level _ _ H2); intro.
(* Goal: @app_pred A ag (@HORec' A ag X f n b) a' *)
(* Goal: iff (forall (x' : A) (_ : @necR A ag a x'), @app_pred A ag (@HORec' A ag X f (@level A ag x') x) x') (@app_pred A ag (f (@HORec A ag X f) x) a) *)
(* Goal: iff (forall (x' : A) (_ : @necR A ag a x'), @app_pred A ag (@HORec' A ag X f (@level A ag x') x) x') (@app_pred A ag (f (@HORec A ag X f) x) a) *)
    generalize (necR_level _ _ H); intro.
    apply (@HORec'_unage _ _ X f  Hcont (n - level x') (level x') b x' (le_refl _)).
(* Goal: @app_pred A ag (@HORec' A ag X f (Init.Nat.add (Init.Nat.sub n (@level A ag x')) (@level A ag x')) b) x' *)
(* Goal: @app_pred A ag (@HORec' A ag X f n b) a' *)
(* Goal: iff (forall (x' : A) (_ : @necR A ag a x'), @app_pred A ag (@HORec' A ag X f (@level A ag x') x) x') (@app_pred A ag (f (@HORec A ag X f) x) a) *)
(* Goal: iff (forall (x' : A) (_ : @necR A ag a x'), @app_pred A ag (@HORec' A ag X f (@level A ag x') x) x') (@app_pred A ag (f (@HORec A ag X f) x) a) *)
    replace (n - level x' + level x') with n by omega.
(* Goal: @eq (@pred A H) (f (@HORec A H unit (fun (x : forall _ : unit, @pred A H) (_ : unit) => f (x tt)) tt)) (f (@HORec A H unit (fun (x : forall _ : unit, @pred A H) (_ : unit) => f (x tt)) tt)) *)
(* Goal: @HOcontractive A H unit (fun (x : forall _ : unit, @pred A H) (_ : unit) => f (x tt)) *)
    apply pred_nec_hereditary with a'; auto.
(* Goal: @app_pred A ag (@HORec' A ag X f n b) a' *)
(* Goal: iff (forall (x' : A) (_ : @necR A ag a x'), @app_pred A ag (@HORec' A ag X f (@level A ag x') x) x') (@app_pred A ag (f (@HORec A ag X f) x) a) *)
(* Goal: iff (forall (x' : A) (_ : @necR A ag a x'), @app_pred A ag (@HORec' A ag X f (@level A ag x') x) x') (@app_pred A ag (f (@HORec A ag X f) x) a) *)
    specialize (H0 _ (necR_refl _)).
(* Goal: @app_pred A ag (@HORec' A ag X f n b) a' *)
(* Goal: iff (forall (x' : A) (_ : @necR A ag a x'), @app_pred A ag (@HORec' A ag X f (@level A ag x') x) x') (@app_pred A ag (f (@HORec A ag X f) x) a) *)
(* Goal: iff (forall (x' : A) (_ : @necR A ag a x'), @app_pred A ag (@HORec' A ag X f (@level A ag x') x) x') (@app_pred A ag (f (@HORec A ag X f) x) a) *)
    apply (@HORec'_unage _ _ X f Hcont (n - level a') (level a') b a' (le_refl _)) in H0.
(* Goal: @app_pred A ag (@HORec' A ag X f n b) a' *)
(* Goal: iff (forall (x' : A) (_ : @necR A ag a x'), @app_pred A ag (@HORec' A ag X f (@level A ag x') x) x') (@app_pred A ag (f (@HORec A ag X f) x) a) *)
(* Goal: iff (forall (x' : A) (_ : @necR A ag a x'), @app_pred A ag (@HORec' A ag X f (@level A ag x') x) x') (@app_pred A ag (f (@HORec A ag X f) x) a) *)
    generalize (necR_level _ _ H); intro.
(* Goal: @app_pred A ag (@HORec' A ag X f n b) a' *)
(* Goal: iff (forall (x' : A) (_ : @necR A ag a x'), @app_pred A ag (@HORec' A ag X f (@level A ag x') x) x') (@app_pred A ag (f (@HORec A ag X f) x) a) *)
(* Goal: iff (forall (x' : A) (_ : @necR A ag a x'), @app_pred A ag (@HORec' A ag X f (@level A ag x') x) x') (@app_pred A ag (f (@HORec A ag X f) x) a) *)
    replace (n - level a' + level a') with n in H0 by omega.
(* Goal: @eq (@pred A H) (f (@HORec A H unit (fun (x : forall _ : unit, @pred A H) (_ : unit) => f (x tt)) tt)) (f (@HORec A H unit (fun (x : forall _ : unit, @pred A H) (_ : unit) => f (x tt)) tt)) *)
(* Goal: @HOcontractive A H unit (fun (x : forall _ : unit, @pred A H) (_ : unit) => f (x tt)) *)
    auto.
(* Goal: forall (A : Type) (H : ageable A) (f : forall _ : @pred A H, @pred A H) (_ : @contractive A H f), @eq (@pred A H) (@Rec A H f) (f (@Rec A H f)) *)
    split; intros.
(* Goal: @app_pred A ag (f (@HORec A ag X f) x) a *)
(* Goal: @app_pred A ag (@HORec' A ag X f (@level A ag x') x) x' *)
(* Goal: iff (forall (x' : A) (_ : @necR A ag a x'), @app_pred A ag (@HORec' A ag X f (@level A ag x') x) x') (@app_pred A ag (f (@HORec A ag X f) x) a) *)
    specialize (H2 _ (necR_refl _)).
(* Goal: @app_pred A ag (f (@HORec A ag X f) x) a *)
(* Goal: @app_pred A ag (@HORec' A ag X f (@level A ag x') x) x' *)
(* Goal: iff (forall (x' : A) (_ : @necR A ag a x'), @app_pred A ag (@HORec' A ag X f (@level A ag x') x) x') (@app_pred A ag (f (@HORec A ag X f) x) a) *)
    rewrite H in H2. simpl in H2.
(* Goal: @eq (@pred A H) (f (@HORec A H unit (fun (x : forall _ : unit, @pred A H) (_ : unit) => f (x tt)) tt)) (f (@HORec A H unit (fun (x : forall _ : unit, @pred A H) (_ : unit) => f (x tt)) tt)) *)
(* Goal: @HOcontractive A H unit (fun (x : forall _ : unit, @pred A H) (_ : unit) => f (x tt)) *)
    apply H0 in H2; auto.
(* Goal: @eq (@pred A H) (f (@HORec A H unit (fun (x : forall _ : unit, @pred A H) (_ : unit) => f (x tt)) tt)) (f (@HORec A H unit (fun (x : forall _ : unit, @pred A H) (_ : unit) => f (x tt)) tt)) *)
(* Goal: @HOcontractive A H unit (fun (x : forall _ : unit, @pred A H) (_ : unit) => f (x tt)) *)
    apply H1 in H2; auto.
(* Goal: @app_pred A ag (@HORec' A ag X f (@level A ag x') x) x' *)
(* Goal: iff (forall (x' : A) (_ : @necR A ag a x'), @app_pred A ag (@HORec' A ag X f (@level A ag x') x) x') (@app_pred A ag (f (@HORec A ag X f) x) a) *)
    assert (app_pred (HORec' f (level a) x) a).
(* Goal: @app_pred A ag (@HORec' A ag X f (@level A ag a) x) a *)
(* Goal: @app_pred A ag (@HORec' A ag X f (@level A ag x') x) x' *)
(* Goal: iff (forall (x' : A) (_ : @necR A ag a x'), @app_pred A ag (@HORec' A ag X f (@level A ag x') x) x') (@app_pred A ag (f (@HORec A ag X f) x) a) *)
    rewrite H. apply H2.
(* Goal: @app_pred A ag (@HORec' A ag X f (@level A ag x') x) x' *)
(* Goal: iff (forall (x' : A) (_ : @necR A ag a x'), @app_pred A ag (@HORec' A ag X f (@level A ag x') x) x') (@app_pred A ag (f (@HORec A ag X f) x) a) *)
     clear - H3 H4 Hcont.
(* Goal: @app_pred A ag (@HORec' A ag X f (@level A ag x') x) x' *)
(* Goal: iff (forall (x' : A) (_ : @necR A ag a x'), @app_pred A ag (@HORec' A ag X f (@level A ag x') x) x') (@app_pred A ag (f (@HORec A ag X f) x) a) *)
    apply (@HORec'_unage _ _ X f Hcont (level a - level x') (level x') x x' (le_refl _)).
    replace (level a - level x' + level x') with (level a)
        by (apply necR_level in H3; omega).
(* Goal: @eq (@pred A H) (f (@HORec A H unit (fun (x : forall _ : unit, @pred A H) (_ : unit) => f (x tt)) tt)) (f (@HORec A H unit (fun (x : forall _ : unit, @pred A H) (_ : unit) => f (x tt)) tt)) *)
(* Goal: @HOcontractive A H unit (fun (x : forall _ : unit, @pred A H) (_ : unit) => f (x tt)) *)
    apply pred_nec_hereditary with a; auto.
 (* None  case *)
(* Goal: iff (forall (x' : A) (_ : @necR A ag a x'), @app_pred A ag (@HORec' A ag X f (@level A ag x') x) x') (@app_pred A ag (f (@HORec A ag X f) x) a) *)
    assert (level a = 0) by (apply age1_level0; auto).
(* Goal: forall (A : Type) (H : ageable A) (f : forall _ : @pred A H, @pred A H) (_ : @contractive A H f), @eq (@pred A H) (@Rec A H f) (f (@Rec A H f)) *)
    split; intros.
(* Goal: @app_pred A ag (f (@HORec A ag X f) x) a *)
(* Goal: @app_pred A ag (@HORec' A ag X f (@level A ag x') x) x' *)
    destruct (@Hcont (fun _ => FF) (HORec f) (level a)) with x a; try omega.
(* Goal: @app_pred nat ag_nat (@allp nat ag_nat X (fun x : X => @box nat ag_nat (@laterM nat ag_nat) (@fash A ag (@andp A ag (@imp A ag (@FF A ag) (@HORec A ag X f x)) (@imp A ag (@HORec A ag X f x) (@FF A ag)))))) (@level A ag a) *)
(* Goal: @app_pred A ag (f (@HORec A ag X f) x) a *)
(* Goal: @app_pred A ag (@HORec' A ag X f (@level A ag x') x) x' *)
     rewrite H0.
(* Goal: forall (A : Type) (H : ageable A) (f : forall _ : @pred A H, @pred A H) (_ : @contractive A H f), @eq (@pred A H) (@Rec A H f) (f (@Rec A H f)) *)
    repeat (hnf; intros); split; hnf; simpl; intros.
(* Goal: and (forall (a' : A) (_ : @necR A ag y a') (_ : forall (x' : A) (_ : @necR A ag a' x'), @app_pred A ag (@HORec' A ag X f (@level A ag x') b) x'), False) (forall (a' : A) (_ : @necR A ag y a') (_ : False) (x' : A) (_ : @necR A ag a' x'), @app_pred A ag (@HORec' A ag X f (@level A ag x') b) x') *)
(* Goal: @app_pred A ag (f (fun _ : X => @FF A ag) x) x' *)
    simpl in H2.  apply laterR_level in H2. elimtype False; omega.
(* Goal: and (forall (a' : A) (_ : @necR A ag y a') (_ : forall (x' : A) (_ : @necR A ag a' x'), @app_pred A ag (@HORec' A ag X f (@level A ag x') b) x'), False) (forall (a' : A) (_ : @necR A ag y a') (_ : False) (x' : A) (_ : @necR A ag a' x'), @app_pred A ag (@HORec' A ag X f (@level A ag x') b) x') *)
(* Goal: @app_pred A ag (f (fun _ : X => @FF A ag) x) x' *)
        simpl in H2.  apply laterR_level in H2. clear - H2. simpl in H2.  unfold natLevel in H2; omega.
(* Goal: @app_pred A ag (f (@HORec A ag X f) x) a *)
(* Goal: @app_pred A ag (@HORec' A ag X f (@level A ag x') x) x' *)
     specialize (H1 _ (necR_refl _)). rewrite H0 in H1. simpl in H1.
(* Goal: @eq (@pred A H) (f (@HORec A H unit (fun (x : forall _ : unit, @pred A H) (_ : unit) => f (x tt)) tt)) (f (@HORec A H unit (fun (x : forall _ : unit, @pred A H) (_ : unit) => f (x tt)) tt)) *)
(* Goal: @HOcontractive A H unit (fun (x : forall _ : unit, @pred A H) (_ : unit) => f (x tt)) *)
     apply H2; auto.
(* Goal: @app_pred A ag (@HORec' A ag X f (@level A ag x') x) x' *)
     apply clos_rt_rt1n in H2.
(* Goal: @app_pred A ag (@HORec' A ag X f (@level A ag x') x) x' *)
    inv H2; [ | unfold age in H3; congruence].
(* Goal: @app_pred A ag (@HORec' A ag X f (@level A ag x') x) x' *)
    rewrite H0; simpl.
(* Goal: @app_pred A ag (f (fun _ : X => @FF A ag) x) x' *)
    specialize (Hcont (HORec f) (fun _ => FF)).
(* Goal: @app_pred A ag (f (fun _ : X => @FF A ag) x) x' *)
    specialize (Hcont 0).
(* Goal: @app_pred A ag (f (fun _ : X => @FF A ag) x) x' *)
    spec Hcont.
(* Goal: forall (A : Type) (H : ageable A) (f : forall _ : @pred A H, @pred A H) (_ : @contractive A H f), @eq (@pred A H) (@Rec A H f) (f (@Rec A H f)) *)
    simpl. intros. apply laterR_level in H2. simpl in H2. unfold natLevel in H2. elimtype False; omega.
(* Goal: @app_pred A ag (f (fun _ : X => @FF A ag) x) x' *)
    specialize ( Hcont x).
(* Goal: @app_pred A ag (f (fun _ : X => @FF A ag) x) x' *)
    hnf in Hcont. specialize ( Hcont x'). spec Hcont. omega.
(* Goal: @eq (@pred A H) (f (@HORec A H unit (fun (x : forall _ : unit, @pred A H) (_ : unit) => f (x tt)) tt)) (f (@HORec A H unit (fun (x : forall _ : unit, @pred A H) (_ : unit) => f (x tt)) tt)) *)
(* Goal: @HOcontractive A H unit (fun (x : forall _ : unit, @pred A H) (_ : unit) => f (x tt)) *)
    apply Hcont; auto.
Qed.

Section recursive.
  Variable A:Type.
  Variable ag:ageable A.

  Variable f:pred A -> pred A.
  Variable Hc : contractive f.

  Lemma cont_HOcont : @HOcontractive A ag unit (fun x _ => f (x tt)).
  Proof.
(* Goal: @HOcontractive A ag unit (fun (x : forall _ : unit, @pred A ag) (_ : unit) => f (x tt)) *)
    repeat intro.
(* Goal: @app_pred A ag (@andp A ag (@imp A ag (f (P tt)) (f (Q tt))) (@imp A ag (f (Q tt)) (f (P tt)))) y *)
    specialize ( H tt).
(* Goal: @eq (@pred A H) (f (@HORec A H unit (fun (x : forall _ : unit, @pred A H) (_ : unit) => f (x tt)) tt)) (f (@HORec A H unit (fun (x : forall _ : unit, @pred A H) (_ : unit) => f (x tt)) tt)) *)
(* Goal: @HOcontractive A H unit (fun (x : forall _ : unit, @pred A H) (_ : unit) => f (x tt)) *)
    eapply Hc; eauto.
  Qed.
End recursive.


Definition Rec {A} `{ageable A} f : pred A
  := HORec (fun x _ => f (x tt)) tt.

Lemma Rec_fold_unfold : forall {A} `{ageable A} f (H:contractive f),
  Rec f = f (Rec f).
Proof.
(* Goal: forall (A : Type) (H : ageable A) (f : forall _ : @pred A H, @pred A H) (_ : @contractive A H f), @eq (@pred A H) (@Rec A H f) (f (@Rec A H f)) *)
  intros.
(* Goal: @eq (@pred A H) (@Rec A H f) (f (@Rec A H f)) *)
  unfold Rec.
(* Goal: @eq (@pred A H) (@HORec A H unit (fun (x : forall _ : unit, @pred A H) (_ : unit) => f (x tt)) tt) (f (@HORec A H unit (fun (x : forall _ : unit, @pred A H) (_ : unit) => f (x tt)) tt)) *)
  pattern (HORec (fun x _ => f (x tt))) at 1.
(* Goal: (fun p : forall _ : unit, @pred A H => @eq (@pred A H) (p tt) (f (@HORec A H unit (fun (x : forall _ : unit, @pred A H) (_ : unit) => f (x tt)) tt))) (@HORec A H unit (fun (x : forall _ : unit, @pred A H) (_ : unit) => f (x tt))) *)
  rewrite HORec_fold_unfold.
(* Goal: @eq (@pred A H) (f (@HORec A H unit (fun (x : forall _ : unit, @pred A H) (_ : unit) => f (x tt)) tt)) (f (@HORec A H unit (fun (x : forall _ : unit, @pred A H) (_ : unit) => f (x tt)) tt)) *)
(* Goal: @HOcontractive A H unit (fun (x : forall _ : unit, @pred A H) (_ : unit) => f (x tt)) *)
  auto.
(* Goal: @eq (@pred A H) (f (@HORec A H unit (fun (x : forall _ : unit, @pred A H) (_ : unit) => f (x tt)) tt)) (f (@HORec A H unit (fun (x : forall _ : unit, @pred A H) (_ : unit) => f (x tt)) tt)) *)
(* Goal: @HOcontractive A H unit (fun (x : forall _ : unit, @pred A H) (_ : unit) => f (x tt)) *)
  apply cont_HOcont; auto.
Qed.

End HoRec.

Export HoRec.
