(* G54DTP Dependently Typed Programming. General Recursion, Bove/Capretta method Venanzio Capretta, March 2011. *) (* We want to represent the following function in Coq. But the argument doesn't decrease in the recursive calls. myfun : nat -> nat myfun 0 = 0 myfun 1 = 1 myfun n = myfun (n/2) + 1 if n is even myfun n = myfun (n+1) if n is odd *) Require Import Arith. Require Import Even. Require Import Div2. (* First we define an inductive constructive predicate that characterizes the arguments for which we know how to compute the result of the function. *) Inductive Dom_myfun: nat -> Set := dmf_zero: Dom_myfun 0 | dmf_one: Dom_myfun 1 | dmf_even: forall n, n>1 -> even n -> Dom_myfun (div2 n) -> Dom_myfun n | dmf_odd: forall n, n>1 -> odd n -> Dom_myfun (S n) -> Dom_myfun n. (* dmf_zero and dmf_one say that we know how to copute the function on 0 and 1. dmf_even says that for an even number larger than one we can compute the result if we already know how to compute it for (div2 n), that is n divided by two. dmf_odd says that for an odd number larger than one we can compute the result if we already know ho to compute it for n+1. *) (* The function ca be defined by recursion on a proof h of the domain predicate. *) Fixpoint myfun_aux (n:nat)(h:Dom_myfun n): nat := match h with dmf_zero => O | dmf_one => S O | dmf_even n p he h' => S (myfun_aux (div2 n) h') | dmf_odd n q ho h' => myfun_aux (S n) h' end. (* (RecArg n) is a set containing the hypotheses that we need to prove to conclude that (Dom_myfun n) holds. For 0 and 1 is just unit because we don't need any hypotheses. *) Definition RecArg (n:nat): Set := if (le_lt_dec n 1) then unit else if (even_odd_dec n) then Dom_myfun (div2 n) else Dom_myfun (S n). (* A "Definition" is just like a Lemma or a Theorem but it is used to prove something in Set instead of in Prop. *) Definition rec_arg_dom: forall n, RecArg n -> Dom_myfun n. intros n; unfold RecArg. case (le_lt_dec n 1). intro hle1; case (le_lt_eq_dec n 1 hle1). intro nlt1. rewrite <- (le_n_O_eq n). intros; apply dmf_zero. apply le_S_n. exact nlt1. intros h1 _; rewrite h1; apply dmf_one. intro p; case (even_odd_dec n). apply dmf_even. exact p. apply dmf_odd. exact p. Defined. (* Closing with "Defined" instead of "Qed" tells Coq not to forget the proof because it will be needed for computations. *) (* We have a uniform proof for the domain predicate: change 101 with any other number and the proof still works. *) Definition hdmf: Dom_myfun 101. repeat (apply rec_arg_dom; compute). exact tt. Defined. Eval compute in (myfun_aux 101 hdmf). (* This is a little property of div2 that we are going to need later. *) Lemma div2_pos: forall n, n>1 -> div2 n > 0. Proof. intro n; case n; simpl. intro h; elim (lt_n_O 1 h). intro n'; case n'; simpl. intro h; apply lt_S_n; exact h. intros; apply le_n_S. apply le_O_n. Qed. (* The domain predicate is satisfied by every number. *) Definition dom_myfun_all: forall n, Dom_myfun n. intro n0. apply (lt_wf_rec n0 Dom_myfun). clear n0; intros n IH; apply (rec_arg_dom n). red. case (le_lt_dec n 1). intros; exact tt. intro h1; case (even_odd_dec n). intro he; apply IH. apply lt_div2. apply lt_S_n. apply le_S. exact h1. intro ho; apply dmf_even. apply lt_S. exact h1. apply even_S; exact ho. apply IH. rewrite <- odd_div2. rewrite (odd_double n ho) at 2. apply lt_n_S. apply plus_lt_compat_r with (n:=0). apply div2_pos. exact h1. exact ho. Defined. (* Now we can define the function without the extra argument. *) Definition myfun (n:nat): nat := myfun_aux n (dom_myfun_all n). Eval compute in (myfun 101).