(* G54DTP Dependently Typed Programming. Divisibility relation, quotient and remainder. Venanzio Capretta, March 2011. *) (* Inductive definition of the "less than" relation. *) Inductive LessThan: nat -> nat -> Prop := lt_O: forall m:nat, LessThan O m | lt_S: forall n m: nat, LessThan n m -> LessThan (S n) (S m). Lemma lt_4_7: LessThan 4 7. Proof. repeat (apply lt_S). apply lt_O. Qed. Require Import Arith. (* Order relations are already defined in the library in a slightly different way. *) Print le. (* n<=m is notation for (le n m). *) Print lt. (* n Divides y z -> Divides x z. Proof. intros x y z Hxy Hyz. elim Hxy. intros h Hy. elim Hyz. intros k Hz. red. exists (k*h). rewrite Hz. rewrite Hy. rewrite mult_assoc. (* "mult_assoc is defined in the library. *) trivial. Qed. (* We want to define quotient and remainder. The following definition doesn't work: Fixpoint div (n m:nat): nat := if (le_lt_dec m n) then S (div (n-m) m) else 0. It is rejected because it is not structurally recursive. *) (* First we define an inductive relation that characterises the pairs of arguments on which "div" works. "Dom_div n m" means that we can divide n by m. *) Inductive Dom_div: nat -> nat -> Set := ddiv_lt: forall n m, n Dom_div n m | ddiv_le: forall n m, m<=n -> Dom_div (n-m) m -> Dom_div n m. (* ddiv_lt says that if n O | ddiv_le n m q h => S (div_aux (n-m) m h) end. (* If m is at least 1, then we can always do the division. *) Theorem dom_div_all : forall n m, 1<=m -> Dom_div n m. intro n'. Check lt_wf_rec. apply (lt_wf_rec n' (fun n=>forall m : nat, 1 <= m -> Dom_div n m)). intros n IH m Hm. case (le_lt_dec m n). intro Hle; apply ddiv_le. exact Hle. apply IH. apply lt_minus. exact Hle. exact Hm. exact Hm. intro Hlt; apply ddiv_lt. exact Hlt. Defined. (* The previous theorem always provides a proof of divisibility, so we can use that in place of the extra argument. (and we return 0 if m is 0. *) Definition div (n m:nat): nat := match (le_lt_dec 1 m) with left h => div_aux n m (dom_div_all n m h) | right _ => 0 end. Eval compute in (div 107 15). (* In a similar way we can define the remainder of the division. *) Fixpoint rem_aux (n m:nat)(h:Dom_div n m): nat := match h with ddiv_lt n m p => n | ddiv_le n m q h => rem_aux (n-m) m h end. Definition rem (n m:nat): nat := match (le_lt_dec 1 m) with left h => rem_aux n m (dom_div_all n m h) | right _ => n end. Eval compute in (rem 107 15). (* And now some properties of quotient and remainder. *) Lemma div_rem_aux: forall n m h, n = (div_aux n m h)*m + (rem_aux n m h). Proof. induction h; simpl. trivial. transitivity (m+(n-m)). symmetry; apply le_plus_minus_r. assumption. rewrite IHh at 1. apply plus_assoc. Qed. Theorem div_rem: forall n m, n = (div n m)*m + (rem n m). Proof. intros n m; unfold div; unfold rem. case (le_lt_dec 1 m). intro H1m; apply div_rem_aux. trivial. Qed. Theorem rem0_divides: forall n m, rem n m = 0 -> Divides m n. Proof. intros n m H. exists (div n m). rewrite (div_rem n m) at 1. rewrite H. rewrite plus_0_r. trivial. Qed. Lemma mult_lt: forall k m, k*m < m -> k=0. Proof. induction k; simpl. trivial. intros m Hm. absurd (m rem_aux n m h = 0. Proof. intros n' m' h'; elim h'; simpl. intros n m Hnm k Hk. rewrite Hk in Hnm. rewrite Hk. rewrite (mult_lt k m Hnm). trivial. intros n m Hle h IH k Hk. apply IH with (k:=k-1). rewrite Hk. rewrite mult_minus. trivial. Qed. Lemma rem_aux_mult_O: forall m k h, rem_aux (k*m) m h = 0. Proof. intros m k h; apply rem_aux_eqmult_0 with (k:=k). trivial. Qed. Lemma divides_remO: forall n m, Divides m n -> rem n m = 0. Proof. intros n m. unfold rem; case (le_lt_dec 1 m). intros p h; elim h; simpl. apply rem_aux_eqmult_0. intros Hm h; elim h. intros k Hk. cut (m=0). intro H0; rewrite Hk; rewrite H0. apply mult_0_r. red in Hm. symmetry. apply le_n_O_eq. apply le_S_n. exact Hm. Qed.