Require Export CompletePreorder FixedPoint.
Require Import Relations Le Compare_dec Classical ClassicalDescription.

Set Implicit Arguments.
Unset Strict Implicit.

Inductive pointed (A:Type) : Type :=
  in_pointed : A -> pointed A
| bottom : pointed A.

Implicit Arguments bottom [A].

Lemma pointed_injective : forall (A:Type)(a a':A),
  in_pointed a = in_pointed a' -> a = a'.
intros A a a' H.
injection H.
trivial.
Qed.

(* the flat ordering determined by a type *)
Section flat_ord.

Variable A:Type.

(*
Definition rel_flat_ord := fun (x y:pointed A) =>
  match x with
    in_pointed x' =>
      match y with
        in_pointed y' => x' = y'
      | bottom => False
      end
  | bottom => True
  end.
*)

Definition rel_flat_ord : relation (pointed A) :=
  fun (x y:pointed A) => (x = y) \/ (x = bottom).

Lemma rel_flat_ord_refl : reflexive (pointed A) rel_flat_ord.
unfold reflexive, rel_flat_ord.
auto.
Qed.

Lemma rel_flat_ord_trans : transitive (pointed A) rel_flat_ord.
unfold transitive, rel_flat_ord.
intuition.
assert (Hx:x = z) by (apply trans_eq with y; trivial).
auto.
assert (Hx:x = bottom) by (apply trans_eq with y; trivial).
auto.
Qed.

Lemma rel_flat_ord_antisym : antisymmetric (pointed A) rel_flat_ord.
unfold antisymmetric, rel_flat_ord.
intuition.
apply trans_eq with (@bottom A); [assumption | apply sym_eq; assumption].
Qed.

Canonical Structure flat_ord :=
  Build_ord rel_flat_ord_refl rel_flat_ord_trans.

Lemma rel_flat_ord_determinacy : forall (x:flat_ord)(a:A),
  x <> bottom -> x <= in_pointed a -> x = in_pointed a.
intros.
firstorder.
contradiction.
Qed.

Lemma in_pointed_not_bottom : forall (a:A), in_pointed a <> bottom.
red.
intros a Hin_pointed.
inversion Hin_pointed.
Qed.

Lemma rel_flat_ord_maximal : forall (x:flat_ord)(a:A),
  in_pointed a <= x -> x = in_pointed a.
intros x a.
simpl.
unfold rel_flat_ord.
intro Hx_or.
inversion Hx_or as [Hx | Hin_pointed].
auto.
destruct (in_pointed_not_bottom Hin_pointed).
Qed.

Lemma rel_flat_ord_bottom_minimal : forall (x:flat_ord), x <= bottom -> x = bottom.
intros x Hx.
inversion Hx as [Heq | Heq]; exact Heq.
Qed.

Lemma flat_ord_case : forall x:flat_ord, (exists a, x = in_pointed a) \/ x = bottom.
intro.
case x.
intro a.
apply or_introl.
exists a.
reflexivity.
apply or_intror.
reflexivity.
Qed.

End flat_ord.

Notation "&ord A" := (flat_ord A)
  (at level 35, right associativity) : ord_scope.

(*
Theorem classical_definite_description :
  forall (A : Type) (P : A->Prop), inhabited A ->
  {x : A | (exists! x : A, P x) -> P x}.
*)

Theorem computational_dependent_description :
  forall (A:Type)(B:A->Type)(R:forall a:A, B a -> Prop)(i:forall a, (B a)),
    (forall a:A, exists x:B a, R a x /\ (forall y:B a, R a y -> x = y)) ->
      {f:forall a:A, B a & (forall a:A, R a (f a))}.
intros A B R i Hsig.
assert (Hx:forall a, {x:B a | (exists! x:B a, R a x) -> R a x}).
intro a; apply (@classical_definite_description (B a) (R a) (i a)).
exists (fun a => let (v, _) := Hx a in v).
intros a; destruct (Hx a) as [v Hv].
apply Hv.
destruct (Hsig a) as [p Hp].
exists p; exact Hp.
Qed.

Lemma simpl_premise_computational_dependent_description :
  forall (A:Type)(B:A->Type)(R:forall a:A, B a -> Prop)(a:A),
    (exists x:B a, R a x) /\
      (forall (x y:B a), R a x -> R a y -> x = y) ->
        exists x:B a, R a x /\ (forall y:B a, R a y -> x = y).
firstorder.
Qed.

Definition ex_sigT :
  forall (A:Type)(P:A->Prop), A -> (exists a:A, P a /\ forall a':A, P a' -> a = a') ->
    {a:A & P a}
    (* sigT (fun a:A => P a) *) .
intros A P witness Hex.
(*
exists (epsilon (inhabits witness) P).
apply epsilon_spec.
destruct Hex as [v [Hp Hu]]; exists v; exact Hp.
Defined.
*)
assert (HsigT: {f : unit -> A &  forall u : unit, P (f u)}).
apply (@computational_dependent_description
  unit (fun _:unit => A) (fun (_:unit)(a:A) => P a)); trivial.
destruct HsigT as [f Hf].
exists (f tt).
exact (Hf tt).
Defined.

Definition is_lub (O:ord)(R:relation O)(x:O)(c:chain O) :=
  (forall n, R (c n) x) /\
    (forall y, (forall n, R (c n) y) -> R x y).

Definition complete (O:ord)(rel:relation O) :=
  forall c:chain O, exists x:O, is_lub rel x c.

Lemma lub_flat_ord_unique :
  forall (A:Type)(x:&ord A)(c:chain (&ord A)),
    is_lub (@rel_flat_ord A) x c ->
      forall (y:&ord A), is_lub (@rel_flat_ord A) y c -> x = y.
unfold is_lub.
intros O x c Hx y Hy.
destruct Hx as [Hx_ub Hx_min].
destruct Hy as [Hy_ub Hy_min].
assert (Hxy:x <= y) by apply (Hx_min y Hy_ub).
assert (Hyx:y <= x) by apply (Hy_min x Hx_ub).
induction x; apply (rel_flat_ord_antisym Hxy Hyx).
Qed.

(* the flat pointed omega-cpo determined by a type *)
Section flat_cpo.

Variable A:Type.

Definition bot_flat_cpo := @bottom A.

Lemma bot_flat_cpo_least : forall (x:&ord A), bot_flat_cpo <= x.
simpl.
unfold rel_flat_ord.
intro x.
apply or_intror.
unfold bot_flat_cpo.
apply refl_equal.
Qed.

(* the proof of completeness of the flat (pre)ordering on A is made using the
   classical law of excludded middle *)
Lemma rel_flat_ord_complete : complete (@rel_flat_ord A).
unfold complete.
intro c.
elim classic with (forall n, c n = bottom).
(* forall n, c n = bottom *)
intro Hc.
exists (@bottom A).
split; intros.
rewrite Hc.
apply rel_flat_ord_refl.
unfold rel_flat_ord.
apply or_intror; apply refl_equal.
(* ~ (forall n, c n = bottom) *)
intro Hc.
elim (not_all_ex_not nat_ord (fun n => c n = bottom) Hc).
intros n Hcnbottom.
exists (c n).
split.
intro m.
case (le_gt_dec m n).
(** **)
intro Hmn.
destruct Hmn.
apply rel_flat_ord_refl.
apply rel_flat_ord_trans with (c m0).
apply (monofun_law c); assumption.
apply (monofun_law c); apply le_n_Sn.
(** **)
intro Hmn.
(* the use of case_eq thanks to Nicolas Julien *)
case_eq (c m).
intros a Hcm.
assert (Hcn:c n <= in_pointed a) by (apply (chain_weak_determinacy Hmn Hcm); assumption).
rewrite (rel_flat_ord_determinacy Hcnbottom Hcn).
apply rel_flat_ord_refl.
(* *)
unfold rel_flat_ord; auto.
(* *)
intros y Hy.
exact (Hy n).
Qed.

Lemma lub_flat_cpo_ex : forall c:chain (&ord A), exists x:&ord A,
  (is_lub (@rel_flat_ord A) x c /\
    (forall y:&ord A, is_lub (@rel_flat_ord A) y c -> x = y)).
intro.
apply simpl_premise_computational_dependent_description with
  (A:=chain (&ord A))
  (B:=fun x:chain (&ord A) => &ord A)
  (R:=fun x y => is_lub (@rel_flat_ord A) y x).
split.
apply (rel_flat_ord_complete c).
intros.
apply (lub_flat_ord_unique (x:=x) (c:=c)); assumption.
Qed.

Definition lub_flat_cpo_sigT : forall c:chain (&ord A),
  {a:&ord A  &  is_lub (@rel_flat_ord A) a c}.
intro.
apply ex_sigT.
exact bottom.
exact (lub_flat_cpo_ex c).
Defined.

Definition lub_flat_cpo (c:chain (&ord A)) : &ord A :=
  projT1 (lub_flat_cpo_sigT c).

Definition lub_flat_cpo_spec (c:chain (&ord A))
      : is_lub (@rel_flat_ord A) (lub_flat_cpo c) c :=
  projT2 (lub_flat_cpo_sigT c).

Lemma lub_flat_cpo_upper_bound : forall (c:chain (&ord A))(n:nat_ord),
  c n <= lub_flat_cpo c.
intros.
destruct (lub_flat_cpo_spec c) as [Hspec1 _].
exact (Hspec1 n).
Qed.

Lemma lub_flat_cpo_least : forall (c:chain (&ord A))(x:&ord A),
  (forall n, c n <= x) -> lub_flat_cpo c <= x.
intros c x Hx.
destruct (lub_flat_cpo_spec c) as [_ Hspec2].
exact (Hspec2 x Hx).
Qed.

Canonical Structure flat_cpo :=
  Build_cpo bot_flat_cpo_least lub_flat_cpo_upper_bound lub_flat_cpo_least.

Lemma lub_flat_cpo_least_bottom : forall (c:chain flat_cpo),
  (forall n, c n <= bottom) -> lub_flat_cpo c = bottom.
intros c Hcn.
assert (Hlubc:lub_flat_cpo c <= bottom).
apply lub_flat_cpo_least; exact Hcn.
exact (rel_flat_ord_bottom_minimal Hlubc).
Qed.

Lemma lub_flat_cpo_witness :
  forall (c:chain flat_cpo),  exists n, c n = lub c.
intros c; elim classic with (forall n, c n = bottom).
intros H; exists 0; symmetry; rewrite H; apply lub_flat_cpo_least_bottom.
intros n; rewrite H; apply (rel_flat_ord_refl (A:=A) bottom).
intros H; destruct (not_all_ex_not _ (fun x => c x = bottom) H) as [n Hn].
case_eq (c n); [intros a H' | intros H'; rewrite H' in Hn; case Hn; auto ].
exists n.
assert (H'' := lub_flat_cpo_upper_bound c n).
case H''; auto; match goal with  H' : ?a = in_pointed _ |- ?b = bottom -> _ =>
  change b with a; rewrite H'; intros; discriminate end.
Qed.

End flat_cpo.

(* now we are able to consider the cpo structure on functions to flat_cpo type:
Parameters (A B:Type)(phi:A -O-> (flat_cpo B)). *)

Notation "&cpo A" := (flat_cpo A)
  (at level 35, right associativity) : ord_scope.

Lemma fixp_flat_witness :
  forall A B (f : (A-O->&cpo B)-C->(A-O->&cpo B)) x,
   exists n, fixp f x = iter f n x.
intros A B f x.
destruct (lub_flat_cpo_witness (iter f <_o> x)) as [n Hn]; exists n.
match goal with Hn : ?a = _ |- _ = ?b => change b with a end; rewrite Hn.
clear Hn n.
case f.
intro f'; case f'.
reflexivity.
Qed.

Lemma fixp_flat_witness_2 :
  forall A B C (f : (A-O->B-O->&cpo C)-C->(A-O->B-O->&cpo C)) x y,
   exists n, fixp f x y = iter f n x y.
intros A B C f x y.
destruct (lub_flat_cpo_witness ((iter f <_o> x) <_o> y)) as [n Hn]; exists n.
match goal with Hn : ?a = _ |- _ = ?b => change b with a end; rewrite Hn.
clear Hn n.
case f.
intro f'; case f'.
reflexivity.
Qed.

Lemma in_pointed_of_chain_is_lub : forall (A:Type)(c:chain (&ord A)) n v,
  c n = in_pointed v -> lub c = in_pointed v.
intros A c n v Hc.
assert (Hcle: in_pointed v <= c n) by (symmetry in Hc; apply (eq_rel_ord Hc)).
apply rel_flat_ord_maximal with (x:=(lub c)) (a:=v).
apply order_trans_law with (1:=Hcle).
apply (lub_upper_bound_law c n).
Qed.

Lemma iter_in_pointed_eq_fixp :
  forall A B (f:(A-O->&cpo B)-C->(A-O->&cpo B)) x n v,
    iter f n x = in_pointed v -> fixp f x = in_pointed v.
intros A B f x n v Hiter.
simpl.
assert (Hlub: lub (iter (f_cont f) <_o> x) = in_pointed v).
apply in_pointed_of_chain_is_lub with (c:=iter (f_cont f) <_o> x) (n:=n).
apply Hiter.
apply Hlub.
Qed.

Lemma iter_in_pointed_eq_fixp_2 :
  forall A B C (f:(A-O->B-O->&cpo C)-C->(A-O->B-O->&cpo C)) x y n v,
    iter f n x y = in_pointed v -> fixp f x y = in_pointed v.
intros A B C f x y n v Hiter.
simpl.
assert (Hlub: lub ((iter (f_cont f) <_o> x) <_o> y) = in_pointed v).
apply in_pointed_of_chain_is_lub with (c:=(iter (f_cont f) <_o> x) <_o> y) (n:=n).
apply Hiter.
apply Hlub.
Qed.