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.