# HG changeset patch # User Adam Chlipala # Date 1319662631 14400 # Node ID ab60b10890edd27377672dab9071a7c453426187 # Parent bb1a470c175768c4bd9fa644d7a425f2849aa170 Non-termination monad diff -r bb1a470c1757 -r ab60b10890ed src/GeneralRec.v --- a/src/GeneralRec.v Wed Oct 26 15:12:21 2011 -0400 +++ b/src/GeneralRec.v Wed Oct 26 16:57:11 2011 -0400 @@ -275,3 +275,305 @@ ]] Some more recent Coq features provide more convenient syntax for defining recursive functions. Interested readers can consult the Coq manual about the commands %\index{Function}%[Function] and %\index{Program Fixpoint}%[Program Fixpoint]. *) + + +(** * A Non-Termination Monad *) + +Section computation. + Variable A : Type. + + Definition computation := + {f : nat -> option A + | forall (n : nat) (v : A), + f n = Some v + -> forall (n' : nat), n' >= n + -> f n' = Some v}. + + Definition runTo (m : computation) (n : nat) (v : A) := + proj1_sig m n = Some v. + + Definition run (m : computation) (v : A) := + exists n, runTo m n v. +End computation. + +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 _ (refl_equal _)) 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 _ (refl_equal _)) 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. + +Require Import Max. + +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 Bottom. + Variable A : Type. + + Definition Bottom : computation A. + exists (fun _ : nat => @None A); abstract run. + Defined. + + Theorem run_Bottom : forall v, ~run Bottom v. + run. + Qed. +End Bottom. + +Section Return. + Variable A : Type. + Variable v : A. + + Definition Return : computation A. + intros; exists (fun _ : nat => Some v); abstract run. + Defined. + + Theorem run_Return : run Return v. + run. + Qed. + + Theorem run_Return_inv : forall x, run Return x -> x = v. + run. + Qed. +End Return. + +Hint Resolve run_Return. + +Section Bind. + Variables A B : Type. + Variable m1 : computation A. + Variable m2 : A -> computation B. + + Definition Bind : computation B. + exists (fun n => + let (f1, Hf1) := m1 in + match f1 n with + | None => None + | Some v => + let (f2, Hf2) := m2 v in + f2 n + end); abstract run. + Defined. + + Require Import Max. + + Theorem run_Bind : forall (v1 : A) (v2 : B), + run m1 v1 + -> run (m2 v1) v2 + -> run Bind v2. + run; match goal with + | [ x : nat, y : nat |- _ ] => exists (max x y) + end; run. + Qed. + + Theorem run_Bind_inv : forall (v2 : B), + run Bind v2 + -> exists v1 : A, + run m1 v1 + /\ run (m2 v1) v2. + run. + Qed. +End Bind. + +Hint Resolve run_Bind. + +Notation "x <- m1 ; m2" := + (Bind m1 (fun x => m2)) (right associativity, at level 70). + +Definition meq A (m1 m2 : computation A) := forall n, proj1_sig m1 n = proj1_sig m2 n. + +Theorem left_identity : forall A B (a : A) (f : A -> computation B), + meq (Bind (Return a) f) (f a). + run. +Qed. + +Theorem right_identity : forall A (m : computation A), + meq (Bind m (@Return _)) m. + run. +Qed. + +Theorem associativity : forall A B C (m : computation A) (f : A -> computation B) (g : B -> computation C), + meq (Bind (Bind m f) g) (Bind m (fun x => Bind (f x) g)). + run. +Qed. + +Section monotone_runTo. + Variable A : Type. + Variable c : computation A. + Variable v : A. + + Theorem monotone_runTo : forall (n1 : nat), + runTo c n1 v + -> forall n2, n2 >= n1 + -> runTo c n2 v. + run. + Qed. +End monotone_runTo. + +Hint Resolve monotone_runTo. + +Section lattice. + Variable A : Type. + + Definition leq (x y : option A) := + forall v, x = Some v -> y = Some v. +End lattice. + +Hint Unfold leq. + +Section Fix. + Variables A B : Type. + Variable f : (A -> computation B) -> (A -> computation B). + + Hypothesis f_continuous : forall n v v1 x, + runTo (f v1 x) n v + -> forall (v2 : A -> computation B), + (forall x, leq (proj1_sig (v1 x) n) (proj1_sig (v2 x) n)) + -> runTo (f v2 x) n v. + + Fixpoint Fix' (n : nat) (x : A) : computation B := + match n with + | O => Bottom _ + | S n' => f (Fix' n') x + end. + + Hint Extern 1 (_ >= _) => omega. + 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. + unfold runTo in *; induction n; crush; + match goal with + | [ H : _ >= _ |- _ ] => inversion H; crush; eauto + end. + 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. + intro x; exists (fun n => proj1_sig (Fix' n x) n); abstract run. + Defined. + + Definition extensional (f : (A -> computation B) -> (A -> computation B)) := + forall g1 g2 n, + (forall x, proj1_sig (g1 x) n = proj1_sig (g2 x) n) + -> forall x, proj1_sig (f g1 x) n = proj1_sig (f g2 x) n. + + Hypothesis f_extensional : extensional f. + + Theorem run_Fix : forall x v, + run (f Fix x) v + -> run (Fix x) v. + run; match goal with + | [ n : nat |- _ ] => exists (S n); eauto + end. + Qed. +End Fix. + +Hint Resolve run_Fix. + +Lemma leq_Some : forall A (x y : A), leq (Some x) (Some y) + -> x = y. + intros ? ? ? H; generalize (H _ (refl_equal _)); crush. +Qed. + +Lemma leq_None : forall A (x y : A), leq (Some x) None + -> False. + intros ? ? ? H; generalize (H _ (refl_equal _)); crush. +Qed. + +Definition mergeSort' : forall A, (A -> A -> bool) -> list A -> computation (list A). + refine (fun A le => Fix + (fun (mergeSort : list A -> computation (list A)) + (ls : list A) => + if le_lt_dec 2 (length ls) + then let lss := partition ls in + ls1 <- mergeSort (fst lss); + ls2 <- mergeSort (snd lss); + Return (merge le ls1 ls2) + else Return ls) _); abstract (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). +Defined. + +Print mergeSort'. + +Lemma test_mergeSort' : run (mergeSort' leb (1 :: 2 :: 36 :: 8 :: 19 :: nil)) + (1 :: 2 :: 8 :: 19 :: 36 :: nil). + exists 4; reflexivity. +Qed. + +Definition looper : bool -> computation unit. + refine (Fix (fun looper (b : bool) => + if b then Return tt else looper b) _); + abstract (unfold leq in *; run; + repeat match goal with + | [ x : unit |- _ ] => destruct x + | [ x : bool |- _ ] => destruct x + end; auto). +Defined. + +Lemma test_looper : run (looper true) tt. + exists 1; reflexivity. +Qed.