Require Import CpdtTactics. Require Import Max List. (* Consider a domain [nat] with the standard ordering *) (* A computation is then a monotone function [nat -> option A], where [option A] is basically a lift of the discrete domain (A, =) *) Section computation. Variable A : Type. Definition computation := { f : nat -> option A | forall n v, f n = Some v -> forall n', n <= n' -> f n' = Some v }. Definition runTo (m : computation) (v : A) (n : nat) := proj1_sig m n = Some v. Definition run (m : computation) (v : A) := exists n, runTo m v n. Program Definition bot : computation := exist _ (fun n => None) _. Program Definition ret (x : A) : computation := exist _ (fun _ => Some x) _. End computation. Arguments bot {_}. Arguments ret {_} x. Arguments run {_} m. Arguments runTo {_} m v n. (* Magic tactics *) Hint Unfold runTo. Ltac run' := unfold run, runTo in *; try red; crush; repeat (match goal with | [ _ : proj1_sig ?E _ = _ |- _ ] => match goal with | [ x : _ |- _ ] => match x with | E => destruct E end end | [ |- context[match ?M with exist _ _ _ => _ end] ] => let Heq := fresh "Heq" in case_eq M; intros ? ? Heq; try rewrite Heq in *; try subst | [ _ : context[match ?M with exist _ _ _ => _ end] |- _ ] => let Heq := fresh "Heq" in case_eq M; intros ? ? Heq; try rewrite Heq in *; subst | [ H : forall n v, ?E n = Some v -> _, _ : context[match ?E ?N with Some _ => _ | None => _ end] |- _ ] => specialize (H N); destruct (E N); try rewrite (H _ (eq_refl _)) by auto; try discriminate | [ H : forall n v, ?E n = Some v -> _, H' : ?E _ = Some _ |- _ ] => rewrite (H _ _ H') by auto end; simpl in *); eauto 7. Ltac run := run'; repeat (match goal with | [ H : forall n v, ?E n = Some v -> _ |- context[match ?E ?N with Some _ => _ | None => _ end] ] => specialize (H N); destruct (E N); try rewrite (H _ (eq_refl _)) by auto; try discriminate end; run'). Lemma ex_irrelevant : forall P : Prop, P -> exists n : nat, P. exists 0; auto. Qed. Hint Resolve ex_irrelevant. Theorem max_spec_le : forall n m, n <= m /\ max n m = m \/ m <= n /\ max n m = n. induction n; destruct m; simpl; intuition; specialize (IHn m); intuition. Qed. Ltac max := intros n m; generalize (max_spec_le n m); crush. Lemma max_1 : forall n m, max n m >= n. max. Qed. Lemma max_2 : forall n m, max n m >= m. max. Qed. Hint Resolve max_1 max_2. Lemma ge_refl : forall n, n >= n. crush. Qed. Hint Resolve ge_refl. Hint Extern 1 => match goal with | [ H : _ = exist _ _ _ |- _ ] => rewrite H end. Section bind. Variable A B : Type. Program Definition bind (m : computation A) (f : A -> computation B) : computation B := fun n => let (f1, _) := m in match f1 n with | None => None | Some v => let (f2, _) := f v in f2 n end. Next Obligation. run. Qed. Theorem run_Bind (v1 : A) (v2 : B) m f : run m v1 -> run (f v1) v2 -> run (bind m f) v2. Proof. run. exists (max x0 x). remember (x1 (max x0 x)) as X1M. rewrite (e x0 v1 H (max x0 x)) in HeqX1M; [ | apply max_1]. run. eapply e0; try eassumption. apply max_2. Qed. End bind. Arguments bind {_} {_} m f. Notation "x <- m1 ; m2" := (bind m1 (fun x => m2)) (right associativity, at level 70). Notation "m '>>=' f" := (bind m f) (right associativity, at level 70). (* Weak bisimilarity *) Definition weq {A} (m1 m2 : computation A) := exists m, forall n, m <= n -> (proj1_sig m1 n = proj1_sig m2 n). Definition meq {A} (m1 m2 : computation A) := forall n, proj1_sig m1 n = proj1_sig m2 n. (* Monadic laws *) Theorem left_identity : forall A B (a : A) (f : A -> computation B), meq (ret a >>= f) (f a). Proof. run. Qed. Theorem right_identity : forall A (m : computation A), meq (m >>= ret) m. Proof. run. Qed. Theorem associativity : forall A B C (m : computation A) (f : A -> computation B) (g : B -> computation C), meq ((m >>= f) >>= g) (m >>= (fun x => f x >>= g)). Proof. run. Qed. Definition leq_option {A : Type} (x y : option A) : Prop := forall v, x = Some v -> y = Some v. Definition leq_arrow {A B : Type} (leq : B -> B -> Prop) (f g : A -> B) : Prop := forall x, leq (f x) (g x). Definition monotone {A B : Type} (leqA : A -> A -> Prop) (leqB : B -> B -> Prop) (f : A -> B) : Prop := forall a a', leqA a a' -> leqB (f a) (f a'). Definition leq_comp {A : Type} (m1 m2 : computation A) : Prop := leq_arrow leq_option (proj1_sig m1) (proj1_sig m2). Definition monotone' {A B : Type} (f : (A -> computation B) -> (A -> computation B)) := monotone (leq_arrow leq_comp) (leq_arrow leq_comp) f. Section Fix. Variable A B : Type. Variable f : (A -> computation B) -> (A -> computation B). Hypothesis f_cont : monotone (leq_arrow leq_comp) (leq_arrow leq_comp) f. Fixpoint Fix' (n : nat) (x : A) : computation B := match n with | 0 => bot | S m => f (Fix' m) x end. Hint Extern 1 (_ >= _) => omega. Hint Extern 1 (_ <= _) => omega. Hint Unfold leq_arrow leq_comp. Lemma Fix'_ok : forall steps n x v, proj1_sig (Fix' n x) steps = Some v -> forall n', n' >= n -> proj1_sig (Fix' n' x) steps = Some v. Proof. unfold monotone, leq_arrow, leq_comp in f_cont. intros steps n. generalize dependent steps. induction n; crush; match goal with | [ H : _ >= _ |- _ ] => inversion H; crush; eauto | [ H : _ <= _ |- _ ] => inversion H; crush; eauto end. assert ((forall x : A, leq_arrow leq_option (proj1_sig (Fix' n x)) (proj1_sig (Fix' m x)))) as HFix'. { intros. unfold leq_arrow, leq_option. crush. } destruct (f_cont (Fix' n) (Fix' m) HFix' x steps v H). crush. Qed. Hint Resolve Fix'_ok. Hint Extern 1 (proj1_sig _ _ = _) => simpl; match goal with | [ |- proj1_sig ?E _ = _ ] => eapply (proj2_sig E) end. Definition Fix : A -> computation B. Proof. intro x. exists (fun n => proj1_sig (Fix' n x) n). abstract run. Defined. End Fix. Definition relation A := A -> A -> Prop. Class Lat (A : Type) := MkLat { leq : relation A ; leq_refl : forall x, leq x x ; leq_trans : forall x y z, leq x y -> leq y z -> leq x z }. Hint Resolve leq_refl. Hint Resolve leq_trans. Program Instance option_lat {A : Type} `{Lat A} : Lat (option A) := { leq := fun x y => forall v1, x = Some v1 -> exists v2, y = Some v2 /\ leq v1 v2 }. Next Obligation. eexists; crush. Qed. Next Obligation. destruct (H0 v1) as [v' [Hv' Hleq1]]; auto. subst. destruct (H1 v') as [v'' [Hv'' Hleq2]]; auto; subst. eexists; eauto. Qed. Program Instance arrow_lat {A B : Type} `{Lat B} : Lat (A -> B) := { leq := fun f1 f2 => forall x, leq (f1 x) (f2 x) }. Next Obligation. eapply leq_trans; eauto. Qed. Program Instance nat_lat : Lat nat := { leq := fun n m => n = m }. Definition liftDiscr (A: Type) : Lat A. Proof. refine (MkLat _ (fun a b => a = b) _ _); crush. Defined. Check (@leq (nat -> option nat) (@arrow_lat _ _ (liftDiscr _))). (* Here we only consider A with the discrete structure *) Program Instance computation_lat {A : Type} : Lat (computation A) := { leq := fun m1 m2 => @leq (nat -> option A) (@arrow_lat _ _ (@option_lat _ (liftDiscr _))) (proj1_sig m1) (proj1_sig m2) }. Next Obligation. run. Qed. Next Obligation. run. eexists. crush. destruct (H _ _ H1) as [? [? ?]]. destruct (H0 _ _ H2) as [? [? ?]]. crush. Qed. Definition cont {A B : Type} `{Lat A, Lat B} (f : A -> B) := forall v1 v2, leq v1 v2 -> leq (f v1) (f v2). (* Section Fix. *) (* Variable A B : Type. *) (* Variable f : (A -> computation B) -> (A -> computation B). *) (* Hypothesis f_cont : cont f. *) (* Fixpoint Fix' (n : nat) (x : A) : computation B := *) (* match n with *) (* | 0 => bot *) (* | S m => f (Fix' m) x *) (* end. *) (* Hint Extern 1 (_ >= _) => omega. *) (* Hint Extern 1 (_ <= _) => omega. *) (* Hint Unfold cont. *) (* Hint Unfold leq. *) (* Lemma Fix'_ok : forall steps n x v, *) (* proj1_sig (Fix' n x) steps = Some v -> *) (* forall n', n' >= n -> *) (* proj1_sig (Fix' n' x) steps = Some v. *) (* Proof. *) (* unfold cont in f_cont. *) (* intros steps n. generalize dependent steps. *) (* induction n; crush; *) (* match goal with *) (* | [ H : _ >= _ |- _ ] => inversion H; crush; eauto *) (* | [ H : _ <= _ |- _ ] => inversion H; crush; eauto *) (* end. *) (* assert (forall (x : A) (x0 : nat) (v1 : B), *) (* proj1_sig (Fix' n x) x0 = Some v1 -> *) (* exists v2 : B, proj1_sig (Fix' m x) x0 = Some v2 /\ v1 = v2) as HFix'. *) (* { intros. eexists. crush. } *) (* destruct (f_cont (Fix' n) (Fix' m) HFix' x steps v H) *) (* as [v2 [Hf Hfleq]]. *) (* crush. *) (* Qed. *) (* Hint Resolve Fix'_ok. *) (* Hint Extern 1 (proj1_sig _ _ = _) => simpl; *) (* match goal with *) (* | [ |- proj1_sig ?E _ = _ ] => eapply (proj2_sig E) *) (* end. *) (* Definition Fix : A -> computation B. *) (* Proof. *) (* intro x. exists (fun n => proj1_sig (Fix' n x) n). *) (* abstract run. *) (* Defined. *) (* End Fix. *) Program Definition f1 (g : nat -> computation nat) : nat -> computation nat := fun n m => Some n. Print f1. (* Lemma f1_cont : cont f1. *) (* unfold cont. unfold leq. simpl. *) (* run. *) (* Qed. *) Lemma f1_mono : monotone' f1. Proof. cbv. run. Qed. Definition f1' := (Fix _ _ f1 f1_mono). Goal exists v , run (f1' 3) v /\ v = 3. eexists; split. exists 5. compute. all: auto. Qed. (* Lemma cont_discr {I O : Type} P Q : *) (* (forall (x : I) (steps : nat) (v : O), P x steps v -> exists (v' : O), Q x steps v' /\ v = v') <-> *) (* (forall (x : I) (steps : nat) (v : O), P x steps v -> Q x steps v). *) (* Proof. split. *) (* - intros. specialize (H x steps v). *) (* destruct (H X) as [? ?]. crush. *) (* - crush. eexists. crush. *) (* Qed. *) (* Ltac cont_discr := *) (* repeat match goal with *) (* | [ H : forall (x : _) (steps : nat) (v : _), proj1_sig (?f x) steps = Some v -> exists _, _ /\ v = _ |- _ ] => rewrite (cont_discr _ _) in H *) (* | [ |- exists v, _ /\ _ = _ ] => eexists *) (* end. *) Lemma leq_Some : forall A (x y : A), @leq _ (@option_lat _ (liftDiscr _)) (Some x) (Some y) -> x = y. intros ? ? ? H; generalize (H _ (eq_refl _)); crush. Qed. Lemma leq_None : forall A (x y : A), @leq _ (@option_lat _ (liftDiscr _)) (Some x) None -> False. intros ? ? ? H; generalize (H _ (eq_refl _)); crush. Qed. Ltac mergeSort' := run; repeat (match goal with | [ |- context[match ?E with O => _ | S _ => _ end] ] => destruct E end; run); repeat match goal with | [ H : forall x, leq (proj1_sig (?f x) _) (proj1_sig (?g x) _) |- _ ] => match goal with | [ H1 : f ?arg = _, H2 : g ?arg = _ |- _ ] => generalize (H arg); rewrite H1; rewrite H2; clear H1 H2; simpl; intro end end; run; repeat match goal with | [ H : _ |- _ ] => (apply leq_None in H; tauto) || (apply leq_Some in H; subst) end; auto. Fixpoint split {A: Type} (ls : list A) : list A * list A := match ls with | nil => (nil, nil) | h :: nil => (h :: nil, nil) | h1 :: h2 :: ls' => let (ls1, ls2) := split ls' in (h1 :: ls1, h2 :: ls2) end. Fixpoint insert {A : Type} (le : A -> A -> bool) (x : A) (ls : list A) : list A := match ls with | nil => x :: nil | h :: ls' => if le x h then x :: ls else h :: insert le x ls' end. Fixpoint merge {A : Type} le (ls1 ls2 : list A) : list A := match ls1 with | nil => ls2 | h :: ls' => insert le h (merge le ls' ls2) end. Program Definition mergeSort' : forall A, (A -> A -> bool) -> list A -> computation (list A) := fun A le => Fix _ _ (fun (mergeSort : list A -> computation (list A)) (ls : list A) => if le_lt_dec 2 (length ls) then let lss := split ls in ls1 <- mergeSort (fst lss); ls2 <- mergeSort (snd lss); ret (merge le ls1 ls2) else ret ls) _. Next Obligation. intros f1 f2 Hf1f2. unfold leq_arrow, leq_comp in Hf1f2. simpl in Hf1f2. unfold leq_arrow, leq_option in Hf1f2. simpl. intros x steps v Hf1. crush. (* cont_discr; crush. *) repeat (match goal with | [ |- context[match ?E with O => _ | S _ => _ end] ] => destruct E end; run). repeat (match goal with | [ H1 : f1 ?arg = _, H2 : f2 ?arg = _ |- _ ] => generalize (Hf1f2 arg); rewrite H1; rewrite H2; clear H1 H2; simpl; intro end; run); mergeSort'. Defined. Arguments mergeSort' {_}. Lemma test_mergeSort' : exists v , run (mergeSort' leb (1 :: 2 :: 36 :: 8 :: 19 :: nil)) v. eexists. exists 10. compute. auto. Qed. (* We can write programs that may fail to terminate *) Ltac looper := unfold leq in *; run; repeat match goal with | [ x : unit |- _ ] => destruct x | [ x : bool |- _ ] => destruct x end; auto. Program Definition looper : bool -> computation unit := Fix _ _ (fun looper (b : bool) => if b then ret tt else looper b) _. Next Obligation. run. (* cont_discr. *) looper; compute; auto. Defined.