(* G54DTP Dependently Typed Programming. The minimization function. Venanzio Capretta, March 2011. *) (* Minimization function: min : (nat -> nat) -> nat min f = if (f 0 = 0) then 0 else min (\n -> f (S n)) + 1 This function cannot be programmed directly. *) (* Inductive definition of the domain. *) Inductive Dom_min: (nat->nat) -> Set := dminO: forall f:nat->nat, (f O)=O -> Dom_min f | dminS: forall f:nat->nat, (f O)<>O -> Dom_min (fun x => f (S x)) -> Dom_min f. (* The formalization of min has an extra argument: a proof of Dom_min and it is defined by recursion on it. *) Fixpoint min (f:nat->nat)(h:Dom_min f): nat := match h with dminO f p => O | dminS f q h' => S (min (fun x => f (S x)) h') end. (* A family of functions that we are going to use as examples. *) Definition down (k:nat): nat -> nat:= fun x => k-x. Eval compute in (down 5 4). Eval compute in (down 10 2). Eval compute in (down 3 5). Definition ddown5: Dom_min (down 5). repeat (apply dminS; [simpl; discriminate | simpl]). apply dminO. trivial. Defined. Eval compute in (min (down 5) ddown5). (* A general proof that works for all parameters. *) Definition ddown: forall n, Dom_min (down n). intro n; elim n. apply dminO; trivial. intros n' H; apply dminS. simpl. auto. simpl. exact H. Defined. Eval compute in (min (down 10) (ddown 10)). (* Another example. *) Definition myfun: nat -> nat := fun x => 2*x + 7 - x*x*x. Eval compute in (myfun 0). Eval compute in (myfun 2). Eval compute in (myfun 3). (* The proof is exactly the same as for (down 5). *) Definition dmyfun: Dom_min myfun. repeat (apply dminS; [simpl; discriminate | simpl]). apply dminO. trivial. Defined. Eval compute in (min myfun dmyfun). (* The minimization function for streams instead of functions: find the first position where a stream of naturals is zero. *) Require Import Streams. Check hd. Check tl. Inductive Dom_smin: Stream nat -> Set := dmin_head: forall (s:Stream nat), hd s = 0 -> Dom_smin s | dmin_tail: forall (s:Stream nat), hd s <> 0 -> Dom_smin (tl s) -> Dom_smin s. Fixpoint smin (s:Stream nat)(h:Dom_smin s): nat := match h with dmin_head s p => O | dmin_tail s q h' => S (smin (tl s) h') end. Set Implicit Arguments. (* Constant streams *) CoFixpoint consts (A:Set)(a:A): Stream A := Cons a (consts a). (* Decreasing streams starting from a given parameter. *) Fixpoint decs (n:nat): Stream nat := match n with O => consts O | S n' => Cons n (decs n') end. Eval simpl in (decs 10). (* Recall the operator that unfolds a stream many times. *) Fixpoint sunf (A:Set)(s:Stream A)(n:nat): Stream A := match n with O => s | S n' => match s with Cons a s' => Cons a (sunf s' n') end end. Eval simpl in (sunf (decs 10) 20). Lemma dmin_decs10: Dom_smin (decs 10). repeat (apply dmin_tail; [discriminate | simpl]). apply dmin_head. simpl. trivial. Defined. Eval simpl in (smin (decs 10) dmin_decs10).