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

Set Implicit Arguments.
Unset Strict Implicit.

Inductive partial (A:Type) : Type :=
  Def : A -> partial A
| Undef : partial A.

Implicit Arguments Undef [A].

Lemma partial_injective : forall (A:Type)(a a':A),
  Def a = Def 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:partial A) =>
  match x with
    Def x' =>
      match y with
        Def y' => x' = y'
      | Undef => False
      end
  | Undef => True
  end.
*)

Definition rel_flat_ord : relation (partial A) :=
  fun (x y:partial A) => (x = y) \/ (x = Undef).

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

Lemma rel_flat_ord_trans : transitive (partial 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 = Undef) by (apply trans_eq with y; trivial).
auto.
Qed.

Lemma rel_flat_ord_antisym : antisymmetric (partial A) rel_flat_ord.
unfold antisymmetric, rel_flat_ord.
intuition.
apply trans_eq with (@Undef 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 <> Undef -> x <= Def a -> x = Def a.
intros.
firstorder.
contradiction.
Qed.

Lemma Def_not_Undef : forall (a:A), Def a <> Undef.
red.
intros a HDef.
inversion HDef.
Qed.

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

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

Lemma flat_ord_case : forall x:flat_ord, (exists a, x = Def a) \/ x = Undef.
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 := @Undef 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 = Undef).
(* forall n, c n = Undef *)
intro Hc.
exists (@Undef A).
split; intros.
rewrite Hc.
apply rel_flat_ord_refl.
unfold rel_flat_ord.
apply or_intror; apply refl_equal.
(* ~ (forall n, c n = Undef) *)
intro Hc.
elim (not_all_ex_not nat_ord (fun n => c n = Undef) Hc).
intros n HcnUndef.
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 <= Def a) by (apply (chain_weak_determinacy Hmn Hcm); assumption).
rewrite (rel_flat_ord_determinacy HcnUndef 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 Undef.
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_Undef : forall (c:chain flat_cpo),
  (forall n, c n <= Undef) -> lub_flat_cpo c = Undef.
intros c Hcn.
assert (Hlubc:lub_flat_cpo c <= Undef).
apply lub_flat_cpo_least; exact Hcn.
exact (rel_flat_ord_Undef_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 = Undef).
intros H; exists 0; symmetry; rewrite H; apply lub_flat_cpo_least_Undef.
intros n; rewrite H; apply (rel_flat_ord_refl (A:=A) Undef).
intros H; destruct (not_all_ex_not _ (fun x => c x = Undef) 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 = Def _ |- ?b = Undef -> _ =>
  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 Def_of_chain_is_lub : forall (A:Type)(c:chain (&ord A)) n v,
  c n = Def v -> lub c = Def v.
intros A c n v Hc.
apply rel_flat_ord_maximal with (x:=(lub c)) (a:=v).
apply (@ord_trans_law (&ord A) (Def v) (c n)).
symmetry in Hc; apply (eq_rel_ord Hc).
exact (lub_upper_bound_law c n).
Qed.

Lemma iter_Def_eq_fixp :
  forall A B (f:(A-O->&cpo B)-C->(A-O->&cpo B)) x n v,
    iter f n x = Def v -> fixp f x = Def v.
intros A B f x n v Hiter.
simpl.
assert (Hlub: lub (iter (f_cont f) <_o> x) = Def v).
apply (@Def_of_chain_is_lub B (iter (f_cont f) <_o> x) n).
apply Hiter.
apply Hlub.
Qed.

Lemma iter_Def_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 = Def v -> fixp f x y = Def v.
intros A B C f x y n v Hiter.
simpl.
assert (Hlub: lub ((iter (f_cont f) <_o> x) <_o> y) = Def v).
apply (@Def_of_chain_is_lub C ((iter (f_cont f) <_o> x) <_o> y) n).
apply Hiter.
apply Hlub.
Qed.