(* recursion.v *) (* Przykłady zaczerpnięte z Coq'Art *) (* Rekursja ograniczona *) Require Import Arith. Fixpoint bdiv_aux (b m n : nat) {struct b} : nat*nat := match b with | O => (0, 0) | S b' => match le_gt_dec n m with | left H => match bdiv_aux b' (m-n) n with | pair q r => (S q, r) end | right H => (0, m) end end. Theorem bdiv_aux_correct1 : forall b m n : nat, m <= b -> 0 < n -> m = fst (bdiv_aux b m n) * n + snd (bdiv_aux b m n). Admitted. Theorem bdiv_aux_correct2 : forall b m n, m <= b -> 0 < n -> snd (bdiv_aux b m n) < n. Admitted. Definition bdiv : forall m n : nat, 0 < n -> {q : nat & {r : nat | m = q * n + r /\ r < n}}. refine (fun (m n : nat) (h : 0 < n) => let p := bdiv_aux m m n in existS (fun q:nat => {r : nat | m = q*n+r /\ r < n}) (fst p) (exist _ (snd p) _)). unfold p; split. apply bdiv_aux_correct1; auto. apply bdiv_aux_correct2; auto. Defined. Recursive Extraction bdiv. (* Time Eval lazy beta iota zeta delta in (bdiv_aux 20000 20000 31). Time Eval lazy beta iota zeta delta in match bdiv 20000 31 (lt_O_Sn 30) with existS q (exist r _) => (q, r) end. *) (* Dobrze ufundowana rekursja *) Require Import Lt. Print Acc. Check Acc_inv. Theorem lt_Acc : forall n : nat, Acc lt n. Proof. induction n. constructor. intros p H. inversion H. constructor; intros y H. Print lt. Check le_lt_or_eq. case (le_lt_or_eq _ _ H). inversion IHn. intro H1. apply H0. SearchPattern (_ < _). apply lt_S_n; auto. intro H1; injection H1; intro H2. rewrite H2; apply IHn. Qed. Print well_founded. Eval red in (well_founded lt). Check well_founded_induction. Check well_founded_ind. Theorem lt_wf : well_founded lt. Proof lt_Acc. Definition div_type (m : nat) := forall n : nat, 0 < n -> {q : nat & {r : nat | m = q*n+r /\ r < n}}. Definition div_type' (m n q : nat) := {r : nat | m = q*n+r /\ r < n}. Definition div_type'' (m n q r : nat) := m = q*n+r /\ r < n. Print well_founded_induction_type. Check Acc_rec. Definition div_F : forall x : nat, (forall y : nat, y div_type y) -> div_type x. unfold div_type at 2. refine (fun m div_rec n Hlt => match le_gt_dec n m with | left H_n_le_m => match div_rec (m-n) _ n _ with | existS q (exist r H_spec) => existS (div_type' m n) (S q) (exist (div_type'' m n (S q)) r _) end | right H_n_gt_m => existS (div_type' m n) 0 (exist (div_type'' m n 0) m _) end); unfold div_type''; auto with arith. destruct H_spec; split; auto. rewrite (le_plus_minus n m H_n_le_m); rewrite H; ring. Qed. Definition div : forall m n : nat, 0 < n -> {q : nat & {r : nat | m = q*n+r /\ r < n}} := well_founded_induction lt_wf div_type div_F. Extraction Inline div_F. Recursive Extraction div. (* Rekursja na podstawie iteracji *) Definition div_it_F (f : nat -> nat -> nat * nat) (m n : nat) := match le_gt_dec n m with | left _ => let (q, r) := f (m-n) n in (S q, r) | right _ => (0, m) end. Fixpoint iter (X : Set) (n : nat) (F : X -> X) (g : X) {struct n} : X := match n with | O => g | S p => F (iter X p F g) end. Implicit Arguments iter [X]. Ltac caseEq f := generalize (refl_equal f); pattern f at -1; case f. Definition div_it_terminates : forall n m : nat, 0 < m -> {v : nat*nat | exists p : nat, (forall k : nat, p < k -> forall g : nat -> nat -> nat*nat, iter k div_it_F g n m = v)}. intros n; elim n using (well_founded_induction lt_wf). intros n' Hrec m Hlt. caseEq (le_gt_dec m n'); intros H Heq_test. case Hrec with (y := n'-m)(2 := Hlt); auto with arith. intros [q r]; intros Hex; exists (S q, r). elim Hex; intros p Heq. exists (S p). intros k. case k. intros; elim (lt_n_O (S p)); auto. intros k' Hplt g; simpl; unfold div_it_F at 1. rewrite Heq; auto with arith. rewrite Heq_test; auto. exists (0, n'); exists 0; intros k; case k. intros; elim (lt_irrefl 0); auto. intros k' Hltp g; simpl; unfold div_it_F at 1. rewrite Heq_test; auto. Defined. Definition div_it (n m : nat) (H : 0 < m) : nat*nat := let (v, _) := div_it_terminates n m H in v. Recursive Extraction div_it. Definition max (m n:nat) : nat := match le_gt_dec m n with left _ => n | right _ => m end. Theorem max1_correct : forall n m:nat, n <= max n m. intros n m; unfold max; case (le_gt_dec n m); auto with arith. Qed. Theorem max2_correct : forall n m:nat, m <= max n m. intros n m; unfold max; case (le_gt_dec n m); auto with arith. Qed. Hint Resolve max1_correct max2_correct : arith. Theorem div_it_fix_eqn : forall (n m:nat)(h:(0 < m)), div_it n m h = match le_gt_dec m n with | left H => let (q,r) := div_it (n-m) m h in (S q, r) | right H => (0, n) end. Proof. intros n m h. unfold div_it; case (div_it_terminates n m h). intros v Hex1; case (div_it_terminates (n-m) m h). intros v' Hex2. elim Hex2; elim Hex1; intros p Heq1 p' Heq2. rewrite <- Heq1 with (k := S (S (max p p')))(g := fun x y:nat => v). rewrite <- Heq2 with (k := S (max p p'))(g := fun x y:nat => v). reflexivity. eauto with arith. eauto with arith. Qed. Theorem div_it_correct1 : forall (m n:nat)(h:0 < n), m = fst (div_it m n h) * n + snd (div_it m n h). Proof. intros m; elim m using (well_founded_ind lt_wf). intros m' Hrec n h; rewrite div_it_fix_eqn. case (le_gt_dec n m'); intros H; trivial. pattern m' at 1; rewrite (le_plus_minus n m'); auto. pattern (m'-n) at 1. rewrite Hrec with (m'-n) n h; auto with arith. case (div_it (m'-n) n h); simpl; auto with arith. Qed. Lemma let_pair : forall t : nat*nat, snd (let (a, b) := t in (S a, b)) = snd t. Proof. intros. induction t. simpl. auto. Qed. Theorem div_it_correct2 : forall (m n : nat)(h : 0 < n), snd (div_it m n h) < n. Proof. intro m; elim m using (well_founded_ind lt_wf). intros m' Hrec n h. rewrite div_it_fix_eqn. case (le_gt_dec n m'); intro H; trivial. assert (snd (div_it (m'-n) n h) < n). apply Hrec; apply lt_minus; auto. rewrite let_pair with (div_it (m'-n) n h); auto. Qed. (* Recursja na dowolnym predykacie *) Fixpoint div2 (n:nat) : nat := match n with S (S p) => S (div2 p) | _ => 0 end. Inductive log_domain : nat->Prop := | log_domain_1 : log_domain 1 | log_domain_2 : forall p:nat, log_domain (S (div2 p))-> log_domain (S (S p)). Check log_domain_ind. Theorem log_domain_non_O : forall x:nat, log_domain x -> x <> 0. Proof. intros x H; case H; intros; discriminate. Qed. Theorem log_domain_inv : forall x p:nat, log_domain x -> x = S (S p)-> log_domain (S (div2 p)). Proof. intros x p H; case H; try (intros H'; discriminate H'). intros p' H1 H2. injection H2; intros H3. Show Proof. rewrite <- H3. Show Proof. assumption. Defined. Eval compute in log_domain_inv 3 1 (log_domain_2 1 log_domain_1) (refl_equal 3). Fixpoint log (x : nat) (h : log_domain x) {struct h} : nat := match x as y return x = y -> nat with | O => fun h' => False_rec nat (log_domain_non_O x h h') | S O => fun h' => O | S (S p) => fun h' => S (log (S (div2 p)) (log_domain_inv x p h h')) end (refl_equal x). Print log_domain_inv. Scheme log_domain_ind2 := Induction for log_domain Sort Prop. Check log_domain_ind. Check log_domain_ind2. Fixpoint two_power (n:nat) : nat := match n with | O => 1 | S p => 2 * two_power p end. Hypothesis mult2_div2_le : forall x:nat, 2 * div2 x <= x. Theorem pow_log_le : forall (x:nat)(h:log_domain x), two_power (log x h) <= x. Proof. intros x h; elim h using log_domain_ind2. simpl; auto with arith. intros p l Hl. lazy beta iota zeta delta [two_power log_domain_inv log]; fold log two_power. Check le_trans. apply le_trans with (2 * S (div2 p)); auto with arith. exact (mult2_div2_le (S (S p))). Qed. Recursive Extraction log. (* EOF *)