A companion theorem for division specified by a fixpoint equation

The following script contains the assumptions that describe a division function. For instance, these facts can be obtained when the function is defined using a recursion by iteration technique.

Parameter div_it : forall n m:nat, 0 < m -> nat*nat.

Axiom 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)

These assumptions can be used to prove a companion theorem:

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).
 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.

Prove the second companion theorem, with the following statement:

forall (m n:nat)(h:0 < n), snd (div_it m n h) < n


Follow this link

Going home
Yves Bertot
Last modified: Tue May 20 15:26:16 MEST 2003