diff options
| author | thery | 2007-07-24 16:10:42 +0000 |
|---|---|---|
| committer | thery | 2007-07-24 16:10:42 +0000 |
| commit | 85b6a5450f8cdcbdc38c2adf559dbcc57ed39d93 (patch) | |
| tree | 422b18f77199b419775547b59704698fe867dbdc | |
| parent | a0256a0012011ef685797c0bd4a92f6dd320f626 (diff) | |
proof of compare added
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10045 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | theories/Ints/num/NMake.v | 1113 | ||||
| -rw-r--r-- | theories/Ints/num/Nbasic.v | 169 | ||||
| -rw-r--r-- | theories/Ints/num/Zn2Z.v | 32 | ||||
| -rw-r--r-- | theories/Ints/num/genN.ml | 919 |
4 files changed, 1600 insertions, 633 deletions
diff --git a/theories/Ints/num/NMake.v b/theories/Ints/num/NMake.v index 6c8ae2f72f..bc44bcd929 100644 --- a/theories/Ints/num/NMake.v +++ b/theories/Ints/num/NMake.v @@ -29,6 +29,7 @@ Module Make (W0:W0Type). Definition w10 := zn2z w9. Definition w11 := zn2z w10. Definition w12 := zn2z w11. + Definition w13 := zn2z w12. Definition w0_op := W0.w_op. Definition w1_op := mk_zn2z_op w0_op. @@ -46,19 +47,20 @@ Module Make (W0:W0Type). Definition w13_op := mk_zn2z_op_karatsuba w12_op. Definition w14_op := mk_zn2z_op_karatsuba w13_op. Definition w15_op := mk_zn2z_op_karatsuba w14_op. + Definition w16_op := mk_zn2z_op_karatsuba w15_op. Section Make_op. Variable mk : forall w', znz_op w' -> znz_op (zn2z w'). - Fixpoint make_op_aux (n:nat) : znz_op (word w12 (S n)):= - match n return znz_op (word w12 (S n)) with - | O => w13_op + Fixpoint make_op_aux (n:nat) : znz_op (word w13 (S n)):= + match n return znz_op (word w13 (S n)) with + | O => w14_op | S n1 => - match n1 return znz_op (word w12 (S (S n1))) with - | O => w14_op + match n1 return znz_op (word w13 (S (S n1))) with + | O => w15_op | S n2 => - match n2 return znz_op (word w12 (S (S (S n2)))) with - | O => w15_op + match n2 return znz_op (word w13 (S (S (S n2)))) with + | O => w16_op | S n3 => mk _ (mk _ (mk _ (make_op_aux n3))) end end @@ -82,7 +84,8 @@ Module Make (W0:W0Type). | N10 : w10 -> t_ | N11 : w11 -> t_ | N12 : w12 -> t_ - | Nn : forall n, word w12 (S n) -> t_. + | N13 : w13 -> t_ + | Nn : forall n, word w13 (S n) -> t_. Definition t := t_. @@ -101,6 +104,7 @@ Module Make (W0:W0Type). Definition one10 := w10_op.(znz_1). Definition one11 := w11_op.(znz_1). Definition one12 := w12_op.(znz_1). + Definition one13 := w13_op.(znz_1). Definition zero := N0 w_0. Definition one := N0 one0. @@ -118,6 +122,7 @@ Module Make (W0:W0Type). Definition w10_succ_c := w10_op.(znz_succ_c). Definition w11_succ_c := w11_op.(znz_succ_c). Definition w12_succ_c := w12_op.(znz_succ_c). + Definition w13_succ_c := w13_op.(znz_succ_c). Definition w0_succ := w0_op.(znz_succ). Definition w1_succ := w1_op.(znz_succ). @@ -132,6 +137,7 @@ Module Make (W0:W0Type). Definition w10_succ := w10_op.(znz_succ). Definition w11_succ := w11_op.(znz_succ). Definition w12_succ := w12_op.(znz_succ). + Definition w13_succ := w13_op.(znz_succ). Definition succ x := match x with @@ -198,7 +204,12 @@ Module Make (W0:W0Type). | N12 wx => match w12_succ_c wx with | C0 r => N12 r - | C1 r => Nn 0 (WW one12 r) + | C1 r => N13 (WW one12 r) + end + | N13 wx => + match w13_succ_c wx with + | C0 r => N13 r + | C1 r => Nn 0 (WW one13 r) end | Nn n wx => let op := make_op n in @@ -232,6 +243,8 @@ Module Make (W0:W0Type). Eval lazy beta zeta iota delta [extend]in extend 11. Definition extend12 := Eval lazy beta zeta iota delta [extend]in extend 12. + Definition extend13 := + Eval lazy beta zeta iota delta [extend]in extend 13. Definition w0_eq0 := w0_op.(znz_eq0). Definition w1_eq0 := w1_op.(znz_eq0). @@ -246,6 +259,7 @@ Module Make (W0:W0Type). Definition w10_eq0 := w10_op.(znz_eq0). Definition w11_eq0 := w11_op.(znz_eq0). Definition w12_eq0 := w12_op.(znz_eq0). + Definition w13_eq0 := w13_op.(znz_eq0). Definition w0_0W := w0_op.(znz_0W). Definition w1_0W := w1_op.(znz_0W). @@ -260,6 +274,7 @@ Module Make (W0:W0Type). Definition w10_0W := w10_op.(znz_0W). Definition w11_0W := w11_op.(znz_0W). Definition w12_0W := w12_op.(znz_0W). + Definition w13_0W := w13_op.(znz_0W). Definition w0_WW := w0_op.(znz_WW). @@ -276,6 +291,7 @@ Module Make (W0:W0Type). Definition w10_add_c := w10_op.(znz_add_c). Definition w11_add_c := w11_op.(znz_add_c). Definition w12_add_c := w12_op.(znz_add_c). + Definition w13_add_c := w13_op.(znz_add_c). Definition w0_add x y := match w0_add_c x y with @@ -340,9 +356,14 @@ Module Make (W0:W0Type). Definition w12_add x y := match w12_add_c x y with | C0 r => N12 r - | C1 r => Nn 0 (WW one12 r) + | C1 r => N13 (WW one12 r) + end. + Definition w13_add x y := + match w13_add_c x y with + | C0 r => N13 r + | C1 r => Nn 0 (WW one13 r) end. - Definition addn n (x y : word w12 (S n)) := + Definition addn n (x y : word w13 (S n)) := let op := make_op n in match op.(znz_add_c) x y with | C0 r => Nn n r @@ -375,9 +396,11 @@ Module Make (W0:W0Type). if w0_eq0 wx then y else w11_add (extend10 w0 (WW w_0 wx)) wy | N0 wx, N12 wy => if w0_eq0 wx then y else w12_add (extend11 w0 (WW w_0 wx)) wy + | N0 wx, N13 wy => + if w0_eq0 wx then y else w13_add (extend12 w0 (WW w_0 wx)) wy | N0 wx, Nn n wy => if w0_eq0 wx then y - else addn n (extend n w12 (extend12 w0 (WW w_0 wx))) wy + else addn n (extend n w13 (extend13 w0 (WW w_0 wx))) wy | N1 wx, N0 wy => if w0_eq0 wy then x else w1_add wx (WW w_0 wy) | N1 wx, N1 wy => w1_add wx wy @@ -392,7 +415,8 @@ Module Make (W0:W0Type). | N1 wx, N10 wy => w10_add (extend9 w0 wx) wy | N1 wx, N11 wy => w11_add (extend10 w0 wx) wy | N1 wx, N12 wy => w12_add (extend11 w0 wx) wy - | N1 wx, Nn n wy => addn n (extend n w12 (extend12 w0 wx)) wy + | N1 wx, N13 wy => w13_add (extend12 w0 wx) wy + | N1 wx, Nn n wy => addn n (extend n w13 (extend13 w0 wx)) wy | N2 wx, N0 wy => if w0_eq0 wy then x else w2_add wx (extend1 w0 (WW w_0 wy)) | N2 wx, N1 wy => w2_add wx (extend1 w0 wy) @@ -407,7 +431,8 @@ Module Make (W0:W0Type). | N2 wx, N10 wy => w10_add (extend8 w1 wx) wy | N2 wx, N11 wy => w11_add (extend9 w1 wx) wy | N2 wx, N12 wy => w12_add (extend10 w1 wx) wy - | N2 wx, Nn n wy => addn n (extend n w12 (extend11 w1 wx)) wy + | N2 wx, N13 wy => w13_add (extend11 w1 wx) wy + | N2 wx, Nn n wy => addn n (extend n w13 (extend12 w1 wx)) wy | N3 wx, N0 wy => if w0_eq0 wy then x else w3_add wx (extend2 w0 (WW w_0 wy)) | N3 wx, N1 wy => w3_add wx (extend2 w0 wy) @@ -422,7 +447,8 @@ Module Make (W0:W0Type). | N3 wx, N10 wy => w10_add (extend7 w2 wx) wy | N3 wx, N11 wy => w11_add (extend8 w2 wx) wy | N3 wx, N12 wy => w12_add (extend9 w2 wx) wy - | N3 wx, Nn n wy => addn n (extend n w12 (extend10 w2 wx)) wy + | N3 wx, N13 wy => w13_add (extend10 w2 wx) wy + | N3 wx, Nn n wy => addn n (extend n w13 (extend11 w2 wx)) wy | N4 wx, N0 wy => if w0_eq0 wy then x else w4_add wx (extend3 w0 (WW w_0 wy)) | N4 wx, N1 wy => w4_add wx (extend3 w0 wy) @@ -437,7 +463,8 @@ Module Make (W0:W0Type). | N4 wx, N10 wy => w10_add (extend6 w3 wx) wy | N4 wx, N11 wy => w11_add (extend7 w3 wx) wy | N4 wx, N12 wy => w12_add (extend8 w3 wx) wy - | N4 wx, Nn n wy => addn n (extend n w12 (extend9 w3 wx)) wy + | N4 wx, N13 wy => w13_add (extend9 w3 wx) wy + | N4 wx, Nn n wy => addn n (extend n w13 (extend10 w3 wx)) wy | N5 wx, N0 wy => if w0_eq0 wy then x else w5_add wx (extend4 w0 (WW w_0 wy)) | N5 wx, N1 wy => w5_add wx (extend4 w0 wy) @@ -452,7 +479,8 @@ Module Make (W0:W0Type). | N5 wx, N10 wy => w10_add (extend5 w4 wx) wy | N5 wx, N11 wy => w11_add (extend6 w4 wx) wy | N5 wx, N12 wy => w12_add (extend7 w4 wx) wy - | N5 wx, Nn n wy => addn n (extend n w12 (extend8 w4 wx)) wy + | N5 wx, N13 wy => w13_add (extend8 w4 wx) wy + | N5 wx, Nn n wy => addn n (extend n w13 (extend9 w4 wx)) wy | N6 wx, N0 wy => if w0_eq0 wy then x else w6_add wx (extend5 w0 (WW w_0 wy)) | N6 wx, N1 wy => w6_add wx (extend5 w0 wy) @@ -467,7 +495,8 @@ Module Make (W0:W0Type). | N6 wx, N10 wy => w10_add (extend4 w5 wx) wy | N6 wx, N11 wy => w11_add (extend5 w5 wx) wy | N6 wx, N12 wy => w12_add (extend6 w5 wx) wy - | N6 wx, Nn n wy => addn n (extend n w12 (extend7 w5 wx)) wy + | N6 wx, N13 wy => w13_add (extend7 w5 wx) wy + | N6 wx, Nn n wy => addn n (extend n w13 (extend8 w5 wx)) wy | N7 wx, N0 wy => if w0_eq0 wy then x else w7_add wx (extend6 w0 (WW w_0 wy)) | N7 wx, N1 wy => w7_add wx (extend6 w0 wy) @@ -482,7 +511,8 @@ Module Make (W0:W0Type). | N7 wx, N10 wy => w10_add (extend3 w6 wx) wy | N7 wx, N11 wy => w11_add (extend4 w6 wx) wy | N7 wx, N12 wy => w12_add (extend5 w6 wx) wy - | N7 wx, Nn n wy => addn n (extend n w12 (extend6 w6 wx)) wy + | N7 wx, N13 wy => w13_add (extend6 w6 wx) wy + | N7 wx, Nn n wy => addn n (extend n w13 (extend7 w6 wx)) wy | N8 wx, N0 wy => if w0_eq0 wy then x else w8_add wx (extend7 w0 (WW w_0 wy)) | N8 wx, N1 wy => w8_add wx (extend7 w0 wy) @@ -497,7 +527,8 @@ Module Make (W0:W0Type). | N8 wx, N10 wy => w10_add (extend2 w7 wx) wy | N8 wx, N11 wy => w11_add (extend3 w7 wx) wy | N8 wx, N12 wy => w12_add (extend4 w7 wx) wy - | N8 wx, Nn n wy => addn n (extend n w12 (extend5 w7 wx)) wy + | N8 wx, N13 wy => w13_add (extend5 w7 wx) wy + | N8 wx, Nn n wy => addn n (extend n w13 (extend6 w7 wx)) wy | N9 wx, N0 wy => if w0_eq0 wy then x else w9_add wx (extend8 w0 (WW w_0 wy)) | N9 wx, N1 wy => w9_add wx (extend8 w0 wy) @@ -512,7 +543,8 @@ Module Make (W0:W0Type). | N9 wx, N10 wy => w10_add (extend1 w8 wx) wy | N9 wx, N11 wy => w11_add (extend2 w8 wx) wy | N9 wx, N12 wy => w12_add (extend3 w8 wx) wy - | N9 wx, Nn n wy => addn n (extend n w12 (extend4 w8 wx)) wy + | N9 wx, N13 wy => w13_add (extend4 w8 wx) wy + | N9 wx, Nn n wy => addn n (extend n w13 (extend5 w8 wx)) wy | N10 wx, N0 wy => if w0_eq0 wy then x else w10_add wx (extend9 w0 (WW w_0 wy)) | N10 wx, N1 wy => w10_add wx (extend9 w0 wy) @@ -527,7 +559,8 @@ Module Make (W0:W0Type). | N10 wx, N10 wy => w10_add wx wy | N10 wx, N11 wy => w11_add (extend1 w9 wx) wy | N10 wx, N12 wy => w12_add (extend2 w9 wx) wy - | N10 wx, Nn n wy => addn n (extend n w12 (extend3 w9 wx)) wy + | N10 wx, N13 wy => w13_add (extend3 w9 wx) wy + | N10 wx, Nn n wy => addn n (extend n w13 (extend4 w9 wx)) wy | N11 wx, N0 wy => if w0_eq0 wy then x else w11_add wx (extend10 w0 (WW w_0 wy)) | N11 wx, N1 wy => w11_add wx (extend10 w0 wy) @@ -542,7 +575,8 @@ Module Make (W0:W0Type). | N11 wx, N10 wy => w11_add wx (extend1 w9 wy) | N11 wx, N11 wy => w11_add wx wy | N11 wx, N12 wy => w12_add (extend1 w10 wx) wy - | N11 wx, Nn n wy => addn n (extend n w12 (extend2 w10 wx)) wy + | N11 wx, N13 wy => w13_add (extend2 w10 wx) wy + | N11 wx, Nn n wy => addn n (extend n w13 (extend3 w10 wx)) wy | N12 wx, N0 wy => if w0_eq0 wy then x else w12_add wx (extend11 w0 (WW w_0 wy)) | N12 wx, N1 wy => w12_add wx (extend11 w0 wy) @@ -557,22 +591,40 @@ Module Make (W0:W0Type). | N12 wx, N10 wy => w12_add wx (extend2 w9 wy) | N12 wx, N11 wy => w12_add wx (extend1 w10 wy) | N12 wx, N12 wy => w12_add wx wy - | N12 wx, Nn n wy => addn n (extend n w12 (extend1 w11 wx)) wy + | N12 wx, N13 wy => w13_add (extend1 w11 wx) wy + | N12 wx, Nn n wy => addn n (extend n w13 (extend2 w11 wx)) wy + | N13 wx, N0 wy => + if w0_eq0 wy then x else w13_add wx (extend12 w0 (WW w_0 wy)) + | N13 wx, N1 wy => w13_add wx (extend12 w0 wy) + | N13 wx, N2 wy => w13_add wx (extend11 w1 wy) + | N13 wx, N3 wy => w13_add wx (extend10 w2 wy) + | N13 wx, N4 wy => w13_add wx (extend9 w3 wy) + | N13 wx, N5 wy => w13_add wx (extend8 w4 wy) + | N13 wx, N6 wy => w13_add wx (extend7 w5 wy) + | N13 wx, N7 wy => w13_add wx (extend6 w6 wy) + | N13 wx, N8 wy => w13_add wx (extend5 w7 wy) + | N13 wx, N9 wy => w13_add wx (extend4 w8 wy) + | N13 wx, N10 wy => w13_add wx (extend3 w9 wy) + | N13 wx, N11 wy => w13_add wx (extend2 w10 wy) + | N13 wx, N12 wy => w13_add wx (extend1 w11 wy) + | N13 wx, N13 wy => w13_add wx wy + | N13 wx, Nn n wy => addn n (extend n w13 (extend1 w12 wx)) wy | Nn n wx, N0 wy => if w0_eq0 wy then x - else addn n wx (extend n w12 (extend12 w0 (WW w_0 wy))) - | Nn n wx, N1 wy => addn n wx (extend n w12 (extend12 w0 wy)) - | Nn n wx, N2 wy => addn n wx (extend n w12 (extend11 w1 wy)) - | Nn n wx, N3 wy => addn n wx (extend n w12 (extend10 w2 wy)) - | Nn n wx, N4 wy => addn n wx (extend n w12 (extend9 w3 wy)) - | Nn n wx, N5 wy => addn n wx (extend n w12 (extend8 w4 wy)) - | Nn n wx, N6 wy => addn n wx (extend n w12 (extend7 w5 wy)) - | Nn n wx, N7 wy => addn n wx (extend n w12 (extend6 w6 wy)) - | Nn n wx, N8 wy => addn n wx (extend n w12 (extend5 w7 wy)) - | Nn n wx, N9 wy => addn n wx (extend n w12 (extend4 w8 wy)) - | Nn n wx, N10 wy => addn n wx (extend n w12 (extend3 w9 wy)) - | Nn n wx, N11 wy => addn n wx (extend n w12 (extend2 w10 wy)) - | Nn n wx, N12 wy => addn n wx (extend n w12 (extend1 w11 wy)) + else addn n wx (extend n w13 (extend13 w0 (WW w_0 wy))) + | Nn n wx, N1 wy => addn n wx (extend n w13 (extend13 w0 wy)) + | Nn n wx, N2 wy => addn n wx (extend n w13 (extend12 w1 wy)) + | Nn n wx, N3 wy => addn n wx (extend n w13 (extend11 w2 wy)) + | Nn n wx, N4 wy => addn n wx (extend n w13 (extend10 w3 wy)) + | Nn n wx, N5 wy => addn n wx (extend n w13 (extend9 w4 wy)) + | Nn n wx, N6 wy => addn n wx (extend n w13 (extend8 w5 wy)) + | Nn n wx, N7 wy => addn n wx (extend n w13 (extend7 w6 wy)) + | Nn n wx, N8 wy => addn n wx (extend n w13 (extend6 w7 wy)) + | Nn n wx, N9 wy => addn n wx (extend n w13 (extend5 w8 wy)) + | Nn n wx, N10 wy => addn n wx (extend n w13 (extend4 w9 wy)) + | Nn n wx, N11 wy => addn n wx (extend n w13 (extend3 w10 wy)) + | Nn n wx, N12 wy => addn n wx (extend n w13 (extend2 w11 wy)) + | Nn n wx, N13 wy => addn n wx (extend n w13 (extend1 w12 wy)) | Nn n wx, Nn m wy => let mn := Max.max n m in let d := diff n m in @@ -620,10 +672,13 @@ Module Make (W0:W0Type). reduce_n1 _ _ zero w11_eq0 reduce_11 N12. Definition reduce_13 := Eval lazy beta iota delta[reduce_n1] in - reduce_n1 _ _ zero w12_eq0 reduce_12 (Nn 0). + reduce_n1 _ _ zero w12_eq0 reduce_12 N13. + Definition reduce_14 := + Eval lazy beta iota delta[reduce_n1] in + reduce_n1 _ _ zero w13_eq0 reduce_13 (Nn 0). Definition reduce_n n := Eval lazy beta iota delta[reduce_n] in - reduce_n _ _ zero reduce_13 Nn n. + reduce_n _ _ zero reduce_14 Nn n. Definition w0_pred_c := w0_op.(znz_pred_c). Definition w1_pred_c := w1_op.(znz_pred_c). @@ -638,6 +693,7 @@ Module Make (W0:W0Type). Definition w10_pred_c := w10_op.(znz_pred_c). Definition w11_pred_c := w11_op.(znz_pred_c). Definition w12_pred_c := w12_op.(znz_pred_c). + Definition w13_pred_c := w13_op.(znz_pred_c). Definition pred x := match x with @@ -706,6 +762,11 @@ Module Make (W0:W0Type). | C0 r => reduce_12 r | C1 r => zero end + | N13 wx => + match w13_pred_c wx with + | C0 r => reduce_13 r + | C1 r => zero + end | Nn n wx => let op := make_op n in match op.(znz_pred_c) wx with @@ -728,6 +789,7 @@ Module Make (W0:W0Type). Definition w10_sub_c := w10_op.(znz_sub_c). Definition w11_sub_c := w11_op.(znz_sub_c). Definition w12_sub_c := w12_op.(znz_sub_c). + Definition w13_sub_c := w13_op.(znz_sub_c). Definition w0_sub x y := match w0_sub_c x y with @@ -794,8 +856,13 @@ Module Make (W0:W0Type). | C0 r => reduce_12 r | C1 r => zero end. + Definition w13_sub x y := + match w13_sub_c x y with + | C0 r => reduce_13 r + | C1 r => zero + end. - Definition subn n (x y : word w12 (S n)) := + Definition subn n (x y : word w13 (S n)) := let op := make_op n in match op.(znz_sub_c) x y with | C0 r => Nn n r @@ -828,9 +895,11 @@ Module Make (W0:W0Type). if w0_eq0 wx then zero else w11_sub (extend10 w0 (WW w_0 wx)) wy | N0 wx, N12 wy => if w0_eq0 wx then zero else w12_sub (extend11 w0 (WW w_0 wx)) wy + | N0 wx, N13 wy => + if w0_eq0 wx then zero else w13_sub (extend12 w0 (WW w_0 wx)) wy | N0 wx, Nn n wy => if w0_eq0 wx then zero - else subn n (extend n w12 (extend12 w0 (WW w_0 wx))) wy + else subn n (extend n w13 (extend13 w0 (WW w_0 wx))) wy | N1 wx, N0 wy => if w0_eq0 wy then x else w1_sub wx (WW w_0 wy) @@ -846,7 +915,8 @@ Module Make (W0:W0Type). | N1 wx, N10 wy => w10_sub (extend9 w0 wx) wy | N1 wx, N11 wy => w11_sub (extend10 w0 wx) wy | N1 wx, N12 wy => w12_sub (extend11 w0 wx) wy - | N1 wx, Nn n wy => subn n (extend n w12 (extend12 w0 wx)) wy + | N1 wx, N13 wy => w13_sub (extend12 w0 wx) wy + | N1 wx, Nn n wy => subn n (extend n w13 (extend13 w0 wx)) wy | N2 wx, N0 wy => if w0_eq0 wy then x else w2_sub wx (extend1 w0 (WW w_0 wy)) @@ -862,7 +932,8 @@ Module Make (W0:W0Type). | N2 wx, N10 wy => w10_sub (extend8 w1 wx) wy | N2 wx, N11 wy => w11_sub (extend9 w1 wx) wy | N2 wx, N12 wy => w12_sub (extend10 w1 wx) wy - | N2 wx, Nn n wy => subn n (extend n w12 (extend11 w1 wx)) wy + | N2 wx, N13 wy => w13_sub (extend11 w1 wx) wy + | N2 wx, Nn n wy => subn n (extend n w13 (extend12 w1 wx)) wy | N3 wx, N0 wy => if w0_eq0 wy then x else w3_sub wx (extend2 w0 (WW w_0 wy)) @@ -878,7 +949,8 @@ Module Make (W0:W0Type). | N3 wx, N10 wy => w10_sub (extend7 w2 wx) wy | N3 wx, N11 wy => w11_sub (extend8 w2 wx) wy | N3 wx, N12 wy => w12_sub (extend9 w2 wx) wy - | N3 wx, Nn n wy => subn n (extend n w12 (extend10 w2 wx)) wy + | N3 wx, N13 wy => w13_sub (extend10 w2 wx) wy + | N3 wx, Nn n wy => subn n (extend n w13 (extend11 w2 wx)) wy | N4 wx, N0 wy => if w0_eq0 wy then x else w4_sub wx (extend3 w0 (WW w_0 wy)) @@ -894,7 +966,8 @@ Module Make (W0:W0Type). | N4 wx, N10 wy => w10_sub (extend6 w3 wx) wy | N4 wx, N11 wy => w11_sub (extend7 w3 wx) wy | N4 wx, N12 wy => w12_sub (extend8 w3 wx) wy - | N4 wx, Nn n wy => subn n (extend n w12 (extend9 w3 wx)) wy + | N4 wx, N13 wy => w13_sub (extend9 w3 wx) wy + | N4 wx, Nn n wy => subn n (extend n w13 (extend10 w3 wx)) wy | N5 wx, N0 wy => if w0_eq0 wy then x else w5_sub wx (extend4 w0 (WW w_0 wy)) @@ -910,7 +983,8 @@ Module Make (W0:W0Type). | N5 wx, N10 wy => w10_sub (extend5 w4 wx) wy | N5 wx, N11 wy => w11_sub (extend6 w4 wx) wy | N5 wx, N12 wy => w12_sub (extend7 w4 wx) wy - | N5 wx, Nn n wy => subn n (extend n w12 (extend8 w4 wx)) wy + | N5 wx, N13 wy => w13_sub (extend8 w4 wx) wy + | N5 wx, Nn n wy => subn n (extend n w13 (extend9 w4 wx)) wy | N6 wx, N0 wy => if w0_eq0 wy then x else w6_sub wx (extend5 w0 (WW w_0 wy)) @@ -926,7 +1000,8 @@ Module Make (W0:W0Type). | N6 wx, N10 wy => w10_sub (extend4 w5 wx) wy | N6 wx, N11 wy => w11_sub (extend5 w5 wx) wy | N6 wx, N12 wy => w12_sub (extend6 w5 wx) wy - | N6 wx, Nn n wy => subn n (extend n w12 (extend7 w5 wx)) wy + | N6 wx, N13 wy => w13_sub (extend7 w5 wx) wy + | N6 wx, Nn n wy => subn n (extend n w13 (extend8 w5 wx)) wy | N7 wx, N0 wy => if w0_eq0 wy then x else w7_sub wx (extend6 w0 (WW w_0 wy)) @@ -942,7 +1017,8 @@ Module Make (W0:W0Type). | N7 wx, N10 wy => w10_sub (extend3 w6 wx) wy | N7 wx, N11 wy => w11_sub (extend4 w6 wx) wy | N7 wx, N12 wy => w12_sub (extend5 w6 wx) wy - | N7 wx, Nn n wy => subn n (extend n w12 (extend6 w6 wx)) wy + | N7 wx, N13 wy => w13_sub (extend6 w6 wx) wy + | N7 wx, Nn n wy => subn n (extend n w13 (extend7 w6 wx)) wy | N8 wx, N0 wy => if w0_eq0 wy then x else w8_sub wx (extend7 w0 (WW w_0 wy)) @@ -958,7 +1034,8 @@ Module Make (W0:W0Type). | N8 wx, N10 wy => w10_sub (extend2 w7 wx) wy | N8 wx, N11 wy => w11_sub (extend3 w7 wx) wy | N8 wx, N12 wy => w12_sub (extend4 w7 wx) wy - | N8 wx, Nn n wy => subn n (extend n w12 (extend5 w7 wx)) wy + | N8 wx, N13 wy => w13_sub (extend5 w7 wx) wy + | N8 wx, Nn n wy => subn n (extend n w13 (extend6 w7 wx)) wy | N9 wx, N0 wy => if w0_eq0 wy then x else w9_sub wx (extend8 w0 (WW w_0 wy)) @@ -974,7 +1051,8 @@ Module Make (W0:W0Type). | N9 wx, N10 wy => w10_sub (extend1 w8 wx) wy | N9 wx, N11 wy => w11_sub (extend2 w8 wx) wy | N9 wx, N12 wy => w12_sub (extend3 w8 wx) wy - | N9 wx, Nn n wy => subn n (extend n w12 (extend4 w8 wx)) wy + | N9 wx, N13 wy => w13_sub (extend4 w8 wx) wy + | N9 wx, Nn n wy => subn n (extend n w13 (extend5 w8 wx)) wy | N10 wx, N0 wy => if w0_eq0 wy then x else w10_sub wx (extend9 w0 (WW w_0 wy)) @@ -990,7 +1068,8 @@ Module Make (W0:W0Type). | N10 wx, N10 wy => w10_sub wx wy | N10 wx, N11 wy => w11_sub (extend1 w9 wx) wy | N10 wx, N12 wy => w12_sub (extend2 w9 wx) wy - | N10 wx, Nn n wy => subn n (extend n w12 (extend3 w9 wx)) wy + | N10 wx, N13 wy => w13_sub (extend3 w9 wx) wy + | N10 wx, Nn n wy => subn n (extend n w13 (extend4 w9 wx)) wy | N11 wx, N0 wy => if w0_eq0 wy then x else w11_sub wx (extend10 w0 (WW w_0 wy)) @@ -1006,7 +1085,8 @@ Module Make (W0:W0Type). | N11 wx, N10 wy => w11_sub wx (extend1 w9 wy) | N11 wx, N11 wy => w11_sub wx wy | N11 wx, N12 wy => w12_sub (extend1 w10 wx) wy - | N11 wx, Nn n wy => subn n (extend n w12 (extend2 w10 wx)) wy + | N11 wx, N13 wy => w13_sub (extend2 w10 wx) wy + | N11 wx, Nn n wy => subn n (extend n w13 (extend3 w10 wx)) wy | N12 wx, N0 wy => if w0_eq0 wy then x else w12_sub wx (extend11 w0 (WW w_0 wy)) @@ -1022,22 +1102,41 @@ Module Make (W0:W0Type). | N12 wx, N10 wy => w12_sub wx (extend2 w9 wy) | N12 wx, N11 wy => w12_sub wx (extend1 w10 wy) | N12 wx, N12 wy => w12_sub wx wy - | N12 wx, Nn n wy => subn n (extend n w12 (extend1 w11 wx)) wy + | N12 wx, N13 wy => w13_sub (extend1 w11 wx) wy + | N12 wx, Nn n wy => subn n (extend n w13 (extend2 w11 wx)) wy + | N13 wx, N0 wy => + if w0_eq0 wy then x + else w13_sub wx (extend12 w0 (WW w_0 wy)) + | N13 wx, N1 wy => w13_sub wx (extend12 w0 wy) + | N13 wx, N2 wy => w13_sub wx (extend11 w1 wy) + | N13 wx, N3 wy => w13_sub wx (extend10 w2 wy) + | N13 wx, N4 wy => w13_sub wx (extend9 w3 wy) + | N13 wx, N5 wy => w13_sub wx (extend8 w4 wy) + | N13 wx, N6 wy => w13_sub wx (extend7 w5 wy) + | N13 wx, N7 wy => w13_sub wx (extend6 w6 wy) + | N13 wx, N8 wy => w13_sub wx (extend5 w7 wy) + | N13 wx, N9 wy => w13_sub wx (extend4 w8 wy) + | N13 wx, N10 wy => w13_sub wx (extend3 w9 wy) + | N13 wx, N11 wy => w13_sub wx (extend2 w10 wy) + | N13 wx, N12 wy => w13_sub wx (extend1 w11 wy) + | N13 wx, N13 wy => w13_sub wx wy + | N13 wx, Nn n wy => subn n (extend n w13 (extend1 w12 wx)) wy | Nn n wx, N0 wy => if w0_eq0 wy then x - else subn n wx (extend n w12 (extend12 w0 (WW w_0 wy))) - | Nn n wx, N1 wy => subn n wx (extend n w12 (extend12 w0 wy)) - | Nn n wx, N2 wy => subn n wx (extend n w12 (extend11 w1 wy)) - | Nn n wx, N3 wy => subn n wx (extend n w12 (extend10 w2 wy)) - | Nn n wx, N4 wy => subn n wx (extend n w12 (extend9 w3 wy)) - | Nn n wx, N5 wy => subn n wx (extend n w12 (extend8 w4 wy)) - | Nn n wx, N6 wy => subn n wx (extend n w12 (extend7 w5 wy)) - | Nn n wx, N7 wy => subn n wx (extend n w12 (extend6 w6 wy)) - | Nn n wx, N8 wy => subn n wx (extend n w12 (extend5 w7 wy)) - | Nn n wx, N9 wy => subn n wx (extend n w12 (extend4 w8 wy)) - | Nn n wx, N10 wy => subn n wx (extend n w12 (extend3 w9 wy)) - | Nn n wx, N11 wy => subn n wx (extend n w12 (extend2 w10 wy)) - | Nn n wx, N12 wy => subn n wx (extend n w12 (extend1 w11 wy)) + else subn n wx (extend n w13 (extend13 w0 (WW w_0 wy))) + | Nn n wx, N1 wy => subn n wx (extend n w13 (extend13 w0 wy)) + | Nn n wx, N2 wy => subn n wx (extend n w13 (extend12 w1 wy)) + | Nn n wx, N3 wy => subn n wx (extend n w13 (extend11 w2 wy)) + | Nn n wx, N4 wy => subn n wx (extend n w13 (extend10 w3 wy)) + | Nn n wx, N5 wy => subn n wx (extend n w13 (extend9 w4 wy)) + | Nn n wx, N6 wy => subn n wx (extend n w13 (extend8 w5 wy)) + | Nn n wx, N7 wy => subn n wx (extend n w13 (extend7 w6 wy)) + | Nn n wx, N8 wy => subn n wx (extend n w13 (extend6 w7 wy)) + | Nn n wx, N9 wy => subn n wx (extend n w13 (extend5 w8 wy)) + | Nn n wx, N10 wy => subn n wx (extend n w13 (extend4 w9 wy)) + | Nn n wx, N11 wy => subn n wx (extend n w13 (extend3 w10 wy)) + | Nn n wx, N12 wy => subn n wx (extend n w13 (extend2 w11 wy)) + | Nn n wx, N13 wy => subn n wx (extend n w13 (extend1 w12 wy)) | Nn n wx, Nn m wy => let mn := Max.max n m in let d := diff n m in @@ -1085,6 +1184,9 @@ Module Make (W0:W0Type). Definition compare_12 := w12_op.(znz_compare). Definition comparen_12 := compare_mn_1 w12 w12 W0 compare_12 (compare_12 W0) compare_12. + Definition compare_13 := w13_op.(znz_compare). + Definition comparen_13 := + compare_mn_1 w13 w13 W0 compare_13 (compare_13 W0) compare_13. Definition compare x y := match x, y with @@ -1101,8 +1203,9 @@ Module Make (W0:W0Type). | N0 wx, N10 wy => opp_compare (comparen_0 10 wy wx) | N0 wx, N11 wy => opp_compare (comparen_0 11 wy wx) | N0 wx, N12 wy => opp_compare (comparen_0 12 wy wx) + | N0 wx, N13 wy => opp_compare (comparen_0 13 wy wx) | N0 wx, Nn n wy => - opp_compare (compare_mn_1 w12 w0 w_0 compare_0 (compare_12 W0) (comparen_0 12) (S n) wy wx) + opp_compare (compare_mn_1 w13 w0 w_0 compare_0 (compare_13 W0) (comparen_0 13) (S n) wy wx) | N1 wx, N0 wy => comparen_0 1 wx wy | N1 wx, N1 wy => compare_1 wx wy | N1 wx, N2 wy => opp_compare (comparen_1 1 wy wx) @@ -1116,8 +1219,9 @@ Module Make (W0:W0Type). | N1 wx, N10 wy => opp_compare (comparen_1 9 wy wx) | N1 wx, N11 wy => opp_compare (comparen_1 10 wy wx) | N1 wx, N12 wy => opp_compare (comparen_1 11 wy wx) + | N1 wx, N13 wy => opp_compare (comparen_1 12 wy wx) | N1 wx, Nn n wy => - opp_compare (compare_mn_1 w12 w1 W0 compare_1 (compare_12 W0) (comparen_1 11) (S n) wy wx) + opp_compare (compare_mn_1 w13 w1 W0 compare_1 (compare_13 W0) (comparen_1 12) (S n) wy wx) | N2 wx, N0 wy => comparen_0 2 wx wy | N2 wx, N1 wy => comparen_1 1 wx wy | N2 wx, N2 wy => compare_2 wx wy @@ -1131,8 +1235,9 @@ Module Make (W0:W0Type). | N2 wx, N10 wy => opp_compare (comparen_2 8 wy wx) | N2 wx, N11 wy => opp_compare (comparen_2 9 wy wx) | N2 wx, N12 wy => opp_compare (comparen_2 10 wy wx) + | N2 wx, N13 wy => opp_compare (comparen_2 11 wy wx) | N2 wx, Nn n wy => - opp_compare (compare_mn_1 w12 w2 W0 compare_2 (compare_12 W0) (comparen_2 10) (S n) wy wx) + opp_compare (compare_mn_1 w13 w2 W0 compare_2 (compare_13 W0) (comparen_2 11) (S n) wy wx) | N3 wx, N0 wy => comparen_0 3 wx wy | N3 wx, N1 wy => comparen_1 2 wx wy | N3 wx, N2 wy => comparen_2 1 wx wy @@ -1146,8 +1251,9 @@ Module Make (W0:W0Type). | N3 wx, N10 wy => opp_compare (comparen_3 7 wy wx) | N3 wx, N11 wy => opp_compare (comparen_3 8 wy wx) | N3 wx, N12 wy => opp_compare (comparen_3 9 wy wx) + | N3 wx, N13 wy => opp_compare (comparen_3 10 wy wx) | N3 wx, Nn n wy => - opp_compare (compare_mn_1 w12 w3 W0 compare_3 (compare_12 W0) (comparen_3 9) (S n) wy wx) + opp_compare (compare_mn_1 w13 w3 W0 compare_3 (compare_13 W0) (comparen_3 10) (S n) wy wx) | N4 wx, N0 wy => comparen_0 4 wx wy | N4 wx, N1 wy => comparen_1 3 wx wy | N4 wx, N2 wy => comparen_2 2 wx wy @@ -1161,8 +1267,9 @@ Module Make (W0:W0Type). | N4 wx, N10 wy => opp_compare (comparen_4 6 wy wx) | N4 wx, N11 wy => opp_compare (comparen_4 7 wy wx) | N4 wx, N12 wy => opp_compare (comparen_4 8 wy wx) + | N4 wx, N13 wy => opp_compare (comparen_4 9 wy wx) | N4 wx, Nn n wy => - opp_compare (compare_mn_1 w12 w4 W0 compare_4 (compare_12 W0) (comparen_4 8) (S n) wy wx) + opp_compare (compare_mn_1 w13 w4 W0 compare_4 (compare_13 W0) (comparen_4 9) (S n) wy wx) | N5 wx, N0 wy => comparen_0 5 wx wy | N5 wx, N1 wy => comparen_1 4 wx wy | N5 wx, N2 wy => comparen_2 3 wx wy @@ -1176,8 +1283,9 @@ Module Make (W0:W0Type). | N5 wx, N10 wy => opp_compare (comparen_5 5 wy wx) | N5 wx, N11 wy => opp_compare (comparen_5 6 wy wx) | N5 wx, N12 wy => opp_compare (comparen_5 7 wy wx) + | N5 wx, N13 wy => opp_compare (comparen_5 8 wy wx) | N5 wx, Nn n wy => - opp_compare (compare_mn_1 w12 w5 W0 compare_5 (compare_12 W0) (comparen_5 7) (S n) wy wx) + opp_compare (compare_mn_1 w13 w5 W0 compare_5 (compare_13 W0) (comparen_5 8) (S n) wy wx) | N6 wx, N0 wy => comparen_0 6 wx wy | N6 wx, N1 wy => comparen_1 5 wx wy | N6 wx, N2 wy => comparen_2 4 wx wy @@ -1191,8 +1299,9 @@ Module Make (W0:W0Type). | N6 wx, N10 wy => opp_compare (comparen_6 4 wy wx) | N6 wx, N11 wy => opp_compare (comparen_6 5 wy wx) | N6 wx, N12 wy => opp_compare (comparen_6 6 wy wx) + | N6 wx, N13 wy => opp_compare (comparen_6 7 wy wx) | N6 wx, Nn n wy => - opp_compare (compare_mn_1 w12 w6 W0 compare_6 (compare_12 W0) (comparen_6 6) (S n) wy wx) + opp_compare (compare_mn_1 w13 w6 W0 compare_6 (compare_13 W0) (comparen_6 7) (S n) wy wx) | N7 wx, N0 wy => comparen_0 7 wx wy | N7 wx, N1 wy => comparen_1 6 wx wy | N7 wx, N2 wy => comparen_2 5 wx wy @@ -1206,8 +1315,9 @@ Module Make (W0:W0Type). | N7 wx, N10 wy => opp_compare (comparen_7 3 wy wx) | N7 wx, N11 wy => opp_compare (comparen_7 4 wy wx) | N7 wx, N12 wy => opp_compare (comparen_7 5 wy wx) + | N7 wx, N13 wy => opp_compare (comparen_7 6 wy wx) | N7 wx, Nn n wy => - opp_compare (compare_mn_1 w12 w7 W0 compare_7 (compare_12 W0) (comparen_7 5) (S n) wy wx) + opp_compare (compare_mn_1 w13 w7 W0 compare_7 (compare_13 W0) (comparen_7 6) (S n) wy wx) | N8 wx, N0 wy => comparen_0 8 wx wy | N8 wx, N1 wy => comparen_1 7 wx wy | N8 wx, N2 wy => comparen_2 6 wx wy @@ -1221,8 +1331,9 @@ Module Make (W0:W0Type). | N8 wx, N10 wy => opp_compare (comparen_8 2 wy wx) | N8 wx, N11 wy => opp_compare (comparen_8 3 wy wx) | N8 wx, N12 wy => opp_compare (comparen_8 4 wy wx) + | N8 wx, N13 wy => opp_compare (comparen_8 5 wy wx) | N8 wx, Nn n wy => - opp_compare (compare_mn_1 w12 w8 W0 compare_8 (compare_12 W0) (comparen_8 4) (S n) wy wx) + opp_compare (compare_mn_1 w13 w8 W0 compare_8 (compare_13 W0) (comparen_8 5) (S n) wy wx) | N9 wx, N0 wy => comparen_0 9 wx wy | N9 wx, N1 wy => comparen_1 8 wx wy | N9 wx, N2 wy => comparen_2 7 wx wy @@ -1236,8 +1347,9 @@ Module Make (W0:W0Type). | N9 wx, N10 wy => opp_compare (comparen_9 1 wy wx) | N9 wx, N11 wy => opp_compare (comparen_9 2 wy wx) | N9 wx, N12 wy => opp_compare (comparen_9 3 wy wx) + | N9 wx, N13 wy => opp_compare (comparen_9 4 wy wx) | N9 wx, Nn n wy => - opp_compare (compare_mn_1 w12 w9 W0 compare_9 (compare_12 W0) (comparen_9 3) (S n) wy wx) + opp_compare (compare_mn_1 w13 w9 W0 compare_9 (compare_13 W0) (comparen_9 4) (S n) wy wx) | N10 wx, N0 wy => comparen_0 10 wx wy | N10 wx, N1 wy => comparen_1 9 wx wy | N10 wx, N2 wy => comparen_2 8 wx wy @@ -1251,8 +1363,9 @@ Module Make (W0:W0Type). | N10 wx, N10 wy => compare_10 wx wy | N10 wx, N11 wy => opp_compare (comparen_10 1 wy wx) | N10 wx, N12 wy => opp_compare (comparen_10 2 wy wx) + | N10 wx, N13 wy => opp_compare (comparen_10 3 wy wx) | N10 wx, Nn n wy => - opp_compare (compare_mn_1 w12 w10 W0 compare_10 (compare_12 W0) (comparen_10 2) (S n) wy wx) + opp_compare (compare_mn_1 w13 w10 W0 compare_10 (compare_13 W0) (comparen_10 3) (S n) wy wx) | N11 wx, N0 wy => comparen_0 11 wx wy | N11 wx, N1 wy => comparen_1 10 wx wy | N11 wx, N2 wy => comparen_2 9 wx wy @@ -1266,8 +1379,9 @@ Module Make (W0:W0Type). | N11 wx, N10 wy => comparen_10 1 wx wy | N11 wx, N11 wy => compare_11 wx wy | N11 wx, N12 wy => opp_compare (comparen_11 1 wy wx) + | N11 wx, N13 wy => opp_compare (comparen_11 2 wy wx) | N11 wx, Nn n wy => - opp_compare (compare_mn_1 w12 w11 W0 compare_11 (compare_12 W0) (comparen_11 1) (S n) wy wx) + opp_compare (compare_mn_1 w13 w11 W0 compare_11 (compare_13 W0) (comparen_11 2) (S n) wy wx) | N12 wx, N0 wy => comparen_0 12 wx wy | N12 wx, N1 wy => comparen_1 11 wx wy | N12 wx, N2 wy => comparen_2 10 wx wy @@ -1281,34 +1395,53 @@ Module Make (W0:W0Type). | N12 wx, N10 wy => comparen_10 2 wx wy | N12 wx, N11 wy => comparen_11 1 wx wy | N12 wx, N12 wy => compare_12 wx wy + | N12 wx, N13 wy => opp_compare (comparen_12 1 wy wx) | N12 wx, Nn n wy => - opp_compare (compare_mn_1 w12 w12 W0 compare_12 (compare_12 W0) (comparen_12 0) (S n) wy wx) + opp_compare (compare_mn_1 w13 w12 W0 compare_12 (compare_13 W0) (comparen_12 1) (S n) wy wx) + | N13 wx, N0 wy => comparen_0 13 wx wy + | N13 wx, N1 wy => comparen_1 12 wx wy + | N13 wx, N2 wy => comparen_2 11 wx wy + | N13 wx, N3 wy => comparen_3 10 wx wy + | N13 wx, N4 wy => comparen_4 9 wx wy + | N13 wx, N5 wy => comparen_5 8 wx wy + | N13 wx, N6 wy => comparen_6 7 wx wy + | N13 wx, N7 wy => comparen_7 6 wx wy + | N13 wx, N8 wy => comparen_8 5 wx wy + | N13 wx, N9 wy => comparen_9 4 wx wy + | N13 wx, N10 wy => comparen_10 3 wx wy + | N13 wx, N11 wy => comparen_11 2 wx wy + | N13 wx, N12 wy => comparen_12 1 wx wy + | N13 wx, N13 wy => compare_13 wx wy + | N13 wx, Nn n wy => + opp_compare (compare_mn_1 w13 w13 W0 compare_13 (compare_13 W0) (comparen_13 0) (S n) wy wx) | Nn n wx, N0 wy => - compare_mn_1 w12 w0 w_0 compare_0 (compare_12 W0) (comparen_0 12) (S n) wx wy + compare_mn_1 w13 w0 w_0 compare_0 (compare_13 W0) (comparen_0 13) (S n) wx wy | Nn n wx, N1 wy => - compare_mn_1 w12 w1 W0 compare_1 (compare_12 W0) (comparen_1 11) (S n) wx wy + compare_mn_1 w13 w1 W0 compare_1 (compare_13 W0) (comparen_1 12) (S n) wx wy | Nn n wx, N2 wy => - compare_mn_1 w12 w2 W0 compare_2 (compare_12 W0) (comparen_2 10) (S n) wx wy + compare_mn_1 w13 w2 W0 compare_2 (compare_13 W0) (comparen_2 11) (S n) wx wy | Nn n wx, N3 wy => - compare_mn_1 w12 w3 W0 compare_3 (compare_12 W0) (comparen_3 9) (S n) wx wy + compare_mn_1 w13 w3 W0 compare_3 (compare_13 W0) (comparen_3 10) (S n) wx wy | Nn n wx, N4 wy => - compare_mn_1 w12 w4 W0 compare_4 (compare_12 W0) (comparen_4 8) (S n) wx wy + compare_mn_1 w13 w4 W0 compare_4 (compare_13 W0) (comparen_4 9) (S n) wx wy | Nn n wx, N5 wy => - compare_mn_1 w12 w5 W0 compare_5 (compare_12 W0) (comparen_5 7) (S n) wx wy + compare_mn_1 w13 w5 W0 compare_5 (compare_13 W0) (comparen_5 8) (S n) wx wy | Nn n wx, N6 wy => - compare_mn_1 w12 w6 W0 compare_6 (compare_12 W0) (comparen_6 6) (S n) wx wy + compare_mn_1 w13 w6 W0 compare_6 (compare_13 W0) (comparen_6 7) (S n) wx wy | Nn n wx, N7 wy => - compare_mn_1 w12 w7 W0 compare_7 (compare_12 W0) (comparen_7 5) (S n) wx wy + compare_mn_1 w13 w7 W0 compare_7 (compare_13 W0) (comparen_7 6) (S n) wx wy | Nn n wx, N8 wy => - compare_mn_1 w12 w8 W0 compare_8 (compare_12 W0) (comparen_8 4) (S n) wx wy + compare_mn_1 w13 w8 W0 compare_8 (compare_13 W0) (comparen_8 5) (S n) wx wy | Nn n wx, N9 wy => - compare_mn_1 w12 w9 W0 compare_9 (compare_12 W0) (comparen_9 3) (S n) wx wy + compare_mn_1 w13 w9 W0 compare_9 (compare_13 W0) (comparen_9 4) (S n) wx wy | Nn n wx, N10 wy => - compare_mn_1 w12 w10 W0 compare_10 (compare_12 W0) (comparen_10 2) (S n) wx wy + compare_mn_1 w13 w10 W0 compare_10 (compare_13 W0) (comparen_10 3) (S n) wx wy | Nn n wx, N11 wy => - compare_mn_1 w12 w11 W0 compare_11 (compare_12 W0) (comparen_11 1) (S n) wx wy + compare_mn_1 w13 w11 W0 compare_11 (compare_13 W0) (comparen_11 2) (S n) wx wy | Nn n wx, N12 wy => - compare_mn_1 w12 w12 W0 compare_12 (compare_12 W0) (comparen_12 0) (S n) wx wy + compare_mn_1 w13 w12 W0 compare_12 (compare_13 W0) (comparen_12 1) (S n) wx wy + | Nn n wx, N13 wy => + compare_mn_1 w13 w13 W0 compare_13 (compare_13 W0) (comparen_13 0) (S n) wx wy | Nn n wx, Nn m wy => let mn := Max.max n m in let d := diff n m in @@ -1337,6 +1470,7 @@ Module Make (W0:W0Type). Definition w10_mul_c := w10_op.(znz_mul_c). Definition w11_mul_c := w11_op.(znz_mul_c). Definition w12_mul_c := w12_op.(znz_mul_c). + Definition w13_mul_c := w13_op.(znz_mul_c). Definition w0_mul_add := Eval lazy beta delta [w_mul_add] in @@ -1377,6 +1511,9 @@ Module Make (W0:W0Type). Definition w12_mul_add := Eval lazy beta delta [w_mul_add] in @w_mul_add w12 W0 w12_succ w12_add_c w12_mul_c. + Definition w13_mul_add := + Eval lazy beta delta [w_mul_add] in + @w_mul_add w13 W0 w13_succ w13_add_c w13_mul_c. Definition w0_mul_add_n1 := @gen_mul_add_n1 w0 w_0 w0_op.(znz_WW) w0_0W w0_mul_add. @@ -1404,6 +1541,8 @@ Module Make (W0:W0Type). @gen_mul_add_n1 w11 W0 w11_op.(znz_WW) w11_0W w11_mul_add. Definition w12_mul_add_n1 := @gen_mul_add_n1 w12 W0 w12_op.(znz_WW) w12_0W w12_mul_add. + Definition w13_mul_add_n1 := + @gen_mul_add_n1 w13 W0 w13_op.(znz_WW) w13_0W w13_mul_add. Definition mul x y := match x, y with @@ -1480,13 +1619,19 @@ Module Make (W0:W0Type). else let (w,r) := w0_mul_add_n1 12 wy wx w_0 in if w0_eq0 w then N12 r - else Nn 0 (WW (extend11 w0 (WW w_0 w)) r) + else N13 (WW (extend11 w0 (WW w_0 w)) r) + | N0 wx, N13 wy => + if w0_eq0 wx then zero + else + let (w,r) := w0_mul_add_n1 13 wy wx w_0 in + if w0_eq0 w then N13 r + else Nn 0 (WW (extend12 w0 (WW w_0 w)) r) | N0 wx, Nn n wy => if w0_eq0 wx then zero else - let (w,r) := w12_mul_add_n1 (S n) wy (extend11 w0 (WW w_0 wx)) W0 in - if w12_eq0 w then Nn n r - else Nn (S n) (WW (extend n w12 (WW W0 w)) r) + let (w,r) := w13_mul_add_n1 (S n) wy (extend12 w0 (WW w_0 wx)) W0 in + if w13_eq0 w then Nn n r + else Nn (S n) (WW (extend n w13 (WW W0 w)) r) | N1 wx, N0 wy => if w0_eq0 wy then zero else @@ -1538,11 +1683,15 @@ Module Make (W0:W0Type). | N1 wx, N12 wy => let (w,r) := w1_mul_add_n1 11 wy wx W0 in if w1_eq0 w then N12 r - else Nn 0 (WW (extend11 w0 w) r) + else N13 (WW (extend11 w0 w) r) + | N1 wx, N13 wy => + let (w,r) := w1_mul_add_n1 12 wy wx W0 in + if w1_eq0 w then N13 r + else Nn 0 (WW (extend12 w0 w) r) | N1 wx, Nn n wy => - let (w,r) := w12_mul_add_n1 (S n) wy (extend11 w0 wx) W0 in - if w12_eq0 w then Nn n r - else Nn (S n) (WW (extend n w12 (WW W0 w)) r) + let (w,r) := w13_mul_add_n1 (S n) wy (extend12 w0 wx) W0 in + if w13_eq0 w then Nn n r + else Nn (S n) (WW (extend n w13 (WW W0 w)) r) | N2 wx, N0 wy => if w0_eq0 wy then zero else @@ -1594,11 +1743,15 @@ Module Make (W0:W0Type). | N2 wx, N12 wy => let (w,r) := w2_mul_add_n1 10 wy wx W0 in if w2_eq0 w then N12 r - else Nn 0 (WW (extend10 w1 w) r) + else N13 (WW (extend10 w1 w) r) + | N2 wx, N13 wy => + let (w,r) := w2_mul_add_n1 11 wy wx W0 in + if w2_eq0 w then N13 r + else Nn 0 (WW (extend11 w1 w) r) | N2 wx, Nn n wy => - let (w,r) := w12_mul_add_n1 (S n) wy (extend10 w1 wx) W0 in - if w12_eq0 w then Nn n r - else Nn (S n) (WW (extend n w12 (WW W0 w)) r) + let (w,r) := w13_mul_add_n1 (S n) wy (extend11 w1 wx) W0 in + if w13_eq0 w then Nn n r + else Nn (S n) (WW (extend n w13 (WW W0 w)) r) | N3 wx, N0 wy => if w0_eq0 wy then zero else @@ -1650,11 +1803,15 @@ Module Make (W0:W0Type). | N3 wx, N12 wy => let (w,r) := w3_mul_add_n1 9 wy wx W0 in if w3_eq0 w then N12 r - else Nn 0 (WW (extend9 w2 w) r) + else N13 (WW (extend9 w2 w) r) + | N3 wx, N13 wy => + let (w,r) := w3_mul_add_n1 10 wy wx W0 in + if w3_eq0 w then N13 r + else Nn 0 (WW (extend10 w2 w) r) | N3 wx, Nn n wy => - let (w,r) := w12_mul_add_n1 (S n) wy (extend9 w2 wx) W0 in - if w12_eq0 w then Nn n r - else Nn (S n) (WW (extend n w12 (WW W0 w)) r) + let (w,r) := w13_mul_add_n1 (S n) wy (extend10 w2 wx) W0 in + if w13_eq0 w then Nn n r + else Nn (S n) (WW (extend n w13 (WW W0 w)) r) | N4 wx, N0 wy => if w0_eq0 wy then zero else @@ -1706,11 +1863,15 @@ Module Make (W0:W0Type). | N4 wx, N12 wy => let (w,r) := w4_mul_add_n1 8 wy wx W0 in if w4_eq0 w then N12 r - else Nn 0 (WW (extend8 w3 w) r) + else N13 (WW (extend8 w3 w) r) + | N4 wx, N13 wy => + let (w,r) := w4_mul_add_n1 9 wy wx W0 in + if w4_eq0 w then N13 r + else Nn 0 (WW (extend9 w3 w) r) | N4 wx, Nn n wy => - let (w,r) := w12_mul_add_n1 (S n) wy (extend8 w3 wx) W0 in - if w12_eq0 w then Nn n r - else Nn (S n) (WW (extend n w12 (WW W0 w)) r) + let (w,r) := w13_mul_add_n1 (S n) wy (extend9 w3 wx) W0 in + if w13_eq0 w then Nn n r + else Nn (S n) (WW (extend n w13 (WW W0 w)) r) | N5 wx, N0 wy => if w0_eq0 wy then zero else @@ -1762,11 +1923,15 @@ Module Make (W0:W0Type). | N5 wx, N12 wy => let (w,r) := w5_mul_add_n1 7 wy wx W0 in if w5_eq0 w then N12 r - else Nn 0 (WW (extend7 w4 w) r) + else N13 (WW (extend7 w4 w) r) + | N5 wx, N13 wy => + let (w,r) := w5_mul_add_n1 8 wy wx W0 in + if w5_eq0 w then N13 r + else Nn 0 (WW (extend8 w4 w) r) | N5 wx, Nn n wy => - let (w,r) := w12_mul_add_n1 (S n) wy (extend7 w4 wx) W0 in - if w12_eq0 w then Nn n r - else Nn (S n) (WW (extend n w12 (WW W0 w)) r) + let (w,r) := w13_mul_add_n1 (S n) wy (extend8 w4 wx) W0 in + if w13_eq0 w then Nn n r + else Nn (S n) (WW (extend n w13 (WW W0 w)) r) | N6 wx, N0 wy => if w0_eq0 wy then zero else @@ -1818,11 +1983,15 @@ Module Make (W0:W0Type). | N6 wx, N12 wy => let (w,r) := w6_mul_add_n1 6 wy wx W0 in if w6_eq0 w then N12 r - else Nn 0 (WW (extend6 w5 w) r) + else N13 (WW (extend6 w5 w) r) + | N6 wx, N13 wy => + let (w,r) := w6_mul_add_n1 7 wy wx W0 in + if w6_eq0 w then N13 r + else Nn 0 (WW (extend7 w5 w) r) | N6 wx, Nn n wy => - let (w,r) := w12_mul_add_n1 (S n) wy (extend6 w5 wx) W0 in - if w12_eq0 w then Nn n r - else Nn (S n) (WW (extend n w12 (WW W0 w)) r) + let (w,r) := w13_mul_add_n1 (S n) wy (extend7 w5 wx) W0 in + if w13_eq0 w then Nn n r + else Nn (S n) (WW (extend n w13 (WW W0 w)) r) | N7 wx, N0 wy => if w0_eq0 wy then zero else @@ -1874,11 +2043,15 @@ Module Make (W0:W0Type). | N7 wx, N12 wy => let (w,r) := w7_mul_add_n1 5 wy wx W0 in if w7_eq0 w then N12 r - else Nn 0 (WW (extend5 w6 w) r) + else N13 (WW (extend5 w6 w) r) + | N7 wx, N13 wy => + let (w,r) := w7_mul_add_n1 6 wy wx W0 in + if w7_eq0 w then N13 r + else Nn 0 (WW (extend6 w6 w) r) | N7 wx, Nn n wy => - let (w,r) := w12_mul_add_n1 (S n) wy (extend5 w6 wx) W0 in - if w12_eq0 w then Nn n r - else Nn (S n) (WW (extend n w12 (WW W0 w)) r) + let (w,r) := w13_mul_add_n1 (S n) wy (extend6 w6 wx) W0 in + if w13_eq0 w then Nn n r + else Nn (S n) (WW (extend n w13 (WW W0 w)) r) | N8 wx, N0 wy => if w0_eq0 wy then zero else @@ -1930,11 +2103,15 @@ Module Make (W0:W0Type). | N8 wx, N12 wy => let (w,r) := w8_mul_add_n1 4 wy wx W0 in if w8_eq0 w then N12 r - else Nn 0 (WW (extend4 w7 w) r) + else N13 (WW (extend4 w7 w) r) + | N8 wx, N13 wy => + let (w,r) := w8_mul_add_n1 5 wy wx W0 in + if w8_eq0 w then N13 r + else Nn 0 (WW (extend5 w7 w) r) | N8 wx, Nn n wy => - let (w,r) := w12_mul_add_n1 (S n) wy (extend4 w7 wx) W0 in - if w12_eq0 w then Nn n r - else Nn (S n) (WW (extend n w12 (WW W0 w)) r) + let (w,r) := w13_mul_add_n1 (S n) wy (extend5 w7 wx) W0 in + if w13_eq0 w then Nn n r + else Nn (S n) (WW (extend n w13 (WW W0 w)) r) | N9 wx, N0 wy => if w0_eq0 wy then zero else @@ -1986,11 +2163,15 @@ Module Make (W0:W0Type). | N9 wx, N12 wy => let (w,r) := w9_mul_add_n1 3 wy wx W0 in if w9_eq0 w then N12 r - else Nn 0 (WW (extend3 w8 w) r) + else N13 (WW (extend3 w8 w) r) + | N9 wx, N13 wy => + let (w,r) := w9_mul_add_n1 4 wy wx W0 in + if w9_eq0 w then N13 r + else Nn 0 (WW (extend4 w8 w) r) | N9 wx, Nn n wy => - let (w,r) := w12_mul_add_n1 (S n) wy (extend3 w8 wx) W0 in - if w12_eq0 w then Nn n r - else Nn (S n) (WW (extend n w12 (WW W0 w)) r) + let (w,r) := w13_mul_add_n1 (S n) wy (extend4 w8 wx) W0 in + if w13_eq0 w then Nn n r + else Nn (S n) (WW (extend n w13 (WW W0 w)) r) | N10 wx, N0 wy => if w0_eq0 wy then zero else @@ -2042,11 +2223,15 @@ Module Make (W0:W0Type). | N10 wx, N12 wy => let (w,r) := w10_mul_add_n1 2 wy wx W0 in if w10_eq0 w then N12 r - else Nn 0 (WW (extend2 w9 w) r) + else N13 (WW (extend2 w9 w) r) + | N10 wx, N13 wy => + let (w,r) := w10_mul_add_n1 3 wy wx W0 in + if w10_eq0 w then N13 r + else Nn 0 (WW (extend3 w9 w) r) | N10 wx, Nn n wy => - let (w,r) := w12_mul_add_n1 (S n) wy (extend2 w9 wx) W0 in - if w12_eq0 w then Nn n r - else Nn (S n) (WW (extend n w12 (WW W0 w)) r) + let (w,r) := w13_mul_add_n1 (S n) wy (extend3 w9 wx) W0 in + if w13_eq0 w then Nn n r + else Nn (S n) (WW (extend n w13 (WW W0 w)) r) | N11 wx, N0 wy => if w0_eq0 wy then zero else @@ -2098,121 +2283,193 @@ Module Make (W0:W0Type). | N11 wx, N12 wy => let (w,r) := w11_mul_add_n1 1 wy wx W0 in if w11_eq0 w then N12 r - else Nn 0 (WW (extend1 w10 w) r) + else N13 (WW (extend1 w10 w) r) + | N11 wx, N13 wy => + let (w,r) := w11_mul_add_n1 2 wy wx W0 in + if w11_eq0 w then N13 r + else Nn 0 (WW (extend2 w10 w) r) | N11 wx, Nn n wy => - let (w,r) := w12_mul_add_n1 (S n) wy (extend1 w10 wx) W0 in - if w12_eq0 w then Nn n r - else Nn (S n) (WW (extend n w12 (WW W0 w)) r) + let (w,r) := w13_mul_add_n1 (S n) wy (extend2 w10 wx) W0 in + if w13_eq0 w then Nn n r + else Nn (S n) (WW (extend n w13 (WW W0 w)) r) | N12 wx, N0 wy => if w0_eq0 wy then zero else let (w,r) := w0_mul_add_n1 12 wx wy w_0 in if w0_eq0 w then N12 r - else Nn 0 (WW (extend11 w0 (WW w_0 w)) r) + else N13 (WW (extend11 w0 (WW w_0 w)) r) | N12 wx, N1 wy => let (w,r) := w1_mul_add_n1 11 wx wy W0 in if w1_eq0 w then N12 r - else Nn 0 (WW (extend11 w0 w) r) + else N13 (WW (extend11 w0 w) r) | N12 wx, N2 wy => let (w,r) := w2_mul_add_n1 10 wx wy W0 in if w2_eq0 w then N12 r - else Nn 0 (WW (extend10 w1 w) r) + else N13 (WW (extend10 w1 w) r) | N12 wx, N3 wy => let (w,r) := w3_mul_add_n1 9 wx wy W0 in if w3_eq0 w then N12 r - else Nn 0 (WW (extend9 w2 w) r) + else N13 (WW (extend9 w2 w) r) | N12 wx, N4 wy => let (w,r) := w4_mul_add_n1 8 wx wy W0 in if w4_eq0 w then N12 r - else Nn 0 (WW (extend8 w3 w) r) + else N13 (WW (extend8 w3 w) r) | N12 wx, N5 wy => let (w,r) := w5_mul_add_n1 7 wx wy W0 in if w5_eq0 w then N12 r - else Nn 0 (WW (extend7 w4 w) r) + else N13 (WW (extend7 w4 w) r) | N12 wx, N6 wy => let (w,r) := w6_mul_add_n1 6 wx wy W0 in if w6_eq0 w then N12 r - else Nn 0 (WW (extend6 w5 w) r) + else N13 (WW (extend6 w5 w) r) | N12 wx, N7 wy => let (w,r) := w7_mul_add_n1 5 wx wy W0 in if w7_eq0 w then N12 r - else Nn 0 (WW (extend5 w6 w) r) + else N13 (WW (extend5 w6 w) r) | N12 wx, N8 wy => let (w,r) := w8_mul_add_n1 4 wx wy W0 in if w8_eq0 w then N12 r - else Nn 0 (WW (extend4 w7 w) r) + else N13 (WW (extend4 w7 w) r) | N12 wx, N9 wy => let (w,r) := w9_mul_add_n1 3 wx wy W0 in if w9_eq0 w then N12 r - else Nn 0 (WW (extend3 w8 w) r) + else N13 (WW (extend3 w8 w) r) | N12 wx, N10 wy => let (w,r) := w10_mul_add_n1 2 wx wy W0 in if w10_eq0 w then N12 r - else Nn 0 (WW (extend2 w9 w) r) + else N13 (WW (extend2 w9 w) r) | N12 wx, N11 wy => let (w,r) := w11_mul_add_n1 1 wx wy W0 in if w11_eq0 w then N12 r - else Nn 0 (WW (extend1 w10 w) r) + else N13 (WW (extend1 w10 w) r) | N12 wx, N12 wy => - Nn 0 (w12_mul_c wx wy) + N13 (w12_mul_c wx wy) + | N12 wx, N13 wy => + let (w,r) := w12_mul_add_n1 1 wy wx W0 in + if w12_eq0 w then N13 r + else Nn 0 (WW (extend1 w11 w) r) | N12 wx, Nn n wy => - let (w,r) := w12_mul_add_n1 (S n) wy wx W0 in - if w12_eq0 w then Nn n r - else Nn (S n) (WW (extend n w12 (WW W0 w)) r) + let (w,r) := w13_mul_add_n1 (S n) wy (extend1 w11 wx) W0 in + if w13_eq0 w then Nn n r + else Nn (S n) (WW (extend n w13 (WW W0 w)) r) + | N13 wx, N0 wy => + if w0_eq0 wy then zero + else + let (w,r) := w0_mul_add_n1 13 wx wy w_0 in + if w0_eq0 w then N13 r + else Nn 0 (WW (extend12 w0 (WW w_0 w)) r) + | N13 wx, N1 wy => + let (w,r) := w1_mul_add_n1 12 wx wy W0 in + if w1_eq0 w then N13 r + else Nn 0 (WW (extend12 w0 w) r) + | N13 wx, N2 wy => + let (w,r) := w2_mul_add_n1 11 wx wy W0 in + if w2_eq0 w then N13 r + else Nn 0 (WW (extend11 w1 w) r) + | N13 wx, N3 wy => + let (w,r) := w3_mul_add_n1 10 wx wy W0 in + if w3_eq0 w then N13 r + else Nn 0 (WW (extend10 w2 w) r) + | N13 wx, N4 wy => + let (w,r) := w4_mul_add_n1 9 wx wy W0 in + if w4_eq0 w then N13 r + else Nn 0 (WW (extend9 w3 w) r) + | N13 wx, N5 wy => + let (w,r) := w5_mul_add_n1 8 wx wy W0 in + if w5_eq0 w then N13 r + else Nn 0 (WW (extend8 w4 w) r) + | N13 wx, N6 wy => + let (w,r) := w6_mul_add_n1 7 wx wy W0 in + if w6_eq0 w then N13 r + else Nn 0 (WW (extend7 w5 w) r) + | N13 wx, N7 wy => + let (w,r) := w7_mul_add_n1 6 wx wy W0 in + if w7_eq0 w then N13 r + else Nn 0 (WW (extend6 w6 w) r) + | N13 wx, N8 wy => + let (w,r) := w8_mul_add_n1 5 wx wy W0 in + if w8_eq0 w then N13 r + else Nn 0 (WW (extend5 w7 w) r) + | N13 wx, N9 wy => + let (w,r) := w9_mul_add_n1 4 wx wy W0 in + if w9_eq0 w then N13 r + else Nn 0 (WW (extend4 w8 w) r) + | N13 wx, N10 wy => + let (w,r) := w10_mul_add_n1 3 wx wy W0 in + if w10_eq0 w then N13 r + else Nn 0 (WW (extend3 w9 w) r) + | N13 wx, N11 wy => + let (w,r) := w11_mul_add_n1 2 wx wy W0 in + if w11_eq0 w then N13 r + else Nn 0 (WW (extend2 w10 w) r) + | N13 wx, N12 wy => + let (w,r) := w12_mul_add_n1 1 wx wy W0 in + if w12_eq0 w then N13 r + else Nn 0 (WW (extend1 w11 w) r) + | N13 wx, N13 wy => + Nn 0 (w13_mul_c wx wy) + | N13 wx, Nn n wy => + let (w,r) := w13_mul_add_n1 (S n) wy wx W0 in + if w13_eq0 w then Nn n r + else Nn (S n) (WW (extend n w13 (WW W0 w)) r) | Nn n wx, N0 wy => if w0_eq0 wy then zero else - let (w,r) := w12_mul_add_n1 (S n) wx (extend11 w0 (WW w_0 wy)) W0 in - if w12_eq0 w then Nn n r - else Nn (S n) (WW (extend n w12 (WW W0 w)) r) + let (w,r) := w13_mul_add_n1 (S n) wx (extend12 w0 (WW w_0 wy)) W0 in + if w13_eq0 w then Nn n r + else Nn (S n) (WW (extend n w13 (WW W0 w)) r) | Nn n wx, N1 wy => - let (w,r) := w12_mul_add_n1 (S n) wx (extend11 w0 wy) W0 in - if w12_eq0 w then Nn n r - else Nn (S n) (WW (extend n w12 (WW W0 w)) r) + let (w,r) := w13_mul_add_n1 (S n) wx (extend12 w0 wy) W0 in + if w13_eq0 w then Nn n r + else Nn (S n) (WW (extend n w13 (WW W0 w)) r) | Nn n wx, N2 wy => - let (w,r) := w12_mul_add_n1 (S n) wx (extend10 w1 wy) W0 in - if w12_eq0 w then Nn n r - else Nn (S n) (WW (extend n w12 (WW W0 w)) r) + let (w,r) := w13_mul_add_n1 (S n) wx (extend11 w1 wy) W0 in + if w13_eq0 w then Nn n r + else Nn (S n) (WW (extend n w13 (WW W0 w)) r) | Nn n wx, N3 wy => - let (w,r) := w12_mul_add_n1 (S n) wx (extend9 w2 wy) W0 in - if w12_eq0 w then Nn n r - else Nn (S n) (WW (extend n w12 (WW W0 w)) r) + let (w,r) := w13_mul_add_n1 (S n) wx (extend10 w2 wy) W0 in + if w13_eq0 w then Nn n r + else Nn (S n) (WW (extend n w13 (WW W0 w)) r) | Nn n wx, N4 wy => - let (w,r) := w12_mul_add_n1 (S n) wx (extend8 w3 wy) W0 in - if w12_eq0 w then Nn n r - else Nn (S n) (WW (extend n w12 (WW W0 w)) r) + let (w,r) := w13_mul_add_n1 (S n) wx (extend9 w3 wy) W0 in + if w13_eq0 w then Nn n r + else Nn (S n) (WW (extend n w13 (WW W0 w)) r) | Nn n wx, N5 wy => - let (w,r) := w12_mul_add_n1 (S n) wx (extend7 w4 wy) W0 in - if w12_eq0 w then Nn n r - else Nn (S n) (WW (extend n w12 (WW W0 w)) r) + let (w,r) := w13_mul_add_n1 (S n) wx (extend8 w4 wy) W0 in + if w13_eq0 w then Nn n r + else Nn (S n) (WW (extend n w13 (WW W0 w)) r) | Nn n wx, N6 wy => - let (w,r) := w12_mul_add_n1 (S n) wx (extend6 w5 wy) W0 in - if w12_eq0 w then Nn n r - else Nn (S n) (WW (extend n w12 (WW W0 w)) r) + let (w,r) := w13_mul_add_n1 (S n) wx (extend7 w5 wy) W0 in + if w13_eq0 w then Nn n r + else Nn (S n) (WW (extend n w13 (WW W0 w)) r) | Nn n wx, N7 wy => - let (w,r) := w12_mul_add_n1 (S n) wx (extend5 w6 wy) W0 in - if w12_eq0 w then Nn n r - else Nn (S n) (WW (extend n w12 (WW W0 w)) r) + let (w,r) := w13_mul_add_n1 (S n) wx (extend6 w6 wy) W0 in + if w13_eq0 w then Nn n r + else Nn (S n) (WW (extend n w13 (WW W0 w)) r) | Nn n wx, N8 wy => - let (w,r) := w12_mul_add_n1 (S n) wx (extend4 w7 wy) W0 in - if w12_eq0 w then Nn n r - else Nn (S n) (WW (extend n w12 (WW W0 w)) r) + let (w,r) := w13_mul_add_n1 (S n) wx (extend5 w7 wy) W0 in + if w13_eq0 w then Nn n r + else Nn (S n) (WW (extend n w13 (WW W0 w)) r) | Nn n wx, N9 wy => - let (w,r) := w12_mul_add_n1 (S n) wx (extend3 w8 wy) W0 in - if w12_eq0 w then Nn n r - else Nn (S n) (WW (extend n w12 (WW W0 w)) r) + let (w,r) := w13_mul_add_n1 (S n) wx (extend4 w8 wy) W0 in + if w13_eq0 w then Nn n r + else Nn (S n) (WW (extend n w13 (WW W0 w)) r) | Nn n wx, N10 wy => - let (w,r) := w12_mul_add_n1 (S n) wx (extend2 w9 wy) W0 in - if w12_eq0 w then Nn n r - else Nn (S n) (WW (extend n w12 (WW W0 w)) r) + let (w,r) := w13_mul_add_n1 (S n) wx (extend3 w9 wy) W0 in + if w13_eq0 w then Nn n r + else Nn (S n) (WW (extend n w13 (WW W0 w)) r) | Nn n wx, N11 wy => - let (w,r) := w12_mul_add_n1 (S n) wx (extend1 w10 wy) W0 in - if w12_eq0 w then Nn n r - else Nn (S n) (WW (extend n w12 (WW W0 w)) r) + let (w,r) := w13_mul_add_n1 (S n) wx (extend2 w10 wy) W0 in + if w13_eq0 w then Nn n r + else Nn (S n) (WW (extend n w13 (WW W0 w)) r) | Nn n wx, N12 wy => - let (w,r) := w12_mul_add_n1 (S n) wx wy W0 in - if w12_eq0 w then Nn n r - else Nn (S n) (WW (extend n w12 (WW W0 w)) r) + let (w,r) := w13_mul_add_n1 (S n) wx (extend1 w11 wy) W0 in + if w13_eq0 w then Nn n r + else Nn (S n) (WW (extend n w13 (WW W0 w)) r) + | Nn n wx, N13 wy => + let (w,r) := w13_mul_add_n1 (S n) wx wy W0 in + if w13_eq0 w then Nn n r + else Nn (S n) (WW (extend n w13 (WW W0 w)) r) | Nn n wx, Nn m wy => let mn := Max.max n m in let d := diff n m in @@ -2235,6 +2492,7 @@ Module Make (W0:W0Type). Definition w10_square_c := w10_op.(znz_square_c). Definition w11_square_c := w11_op.(znz_square_c). Definition w12_square_c := w12_op.(znz_square_c). + Definition w13_square_c := w13_op.(znz_square_c). Definition square x := match x with @@ -2250,7 +2508,8 @@ Module Make (W0:W0Type). | N9 wx => N10 (w9_square_c wx) | N10 wx => N11 (w10_square_c wx) | N11 wx => N12 (w11_square_c wx) - | N12 wx => Nn 0 (w12_square_c wx) + | N12 wx => N13 (w12_square_c wx) + | N13 wx => Nn 0 (w13_square_c wx) | Nn n wx => let op := make_op n in Nn (S n) (op.(znz_square_c) wx) @@ -2276,6 +2535,7 @@ Module Make (W0:W0Type). Definition w10_sqrt := w10_op.(znz_sqrt). Definition w11_sqrt := w11_op.(znz_sqrt). Definition w12_sqrt := w12_op.(znz_sqrt). + Definition w13_sqrt := w13_op.(znz_sqrt). Definition sqrt x := match x with @@ -2292,6 +2552,7 @@ Module Make (W0:W0Type). | N10 wx => reduce_10 (w10_sqrt wx) | N11 wx => reduce_11 (w11_sqrt wx) | N12 wx => reduce_12 (w12_sqrt wx) + | N13 wx => reduce_13 (w13_sqrt wx) | Nn n wx => let op := make_op n in reduce_n n (op.(znz_sqrt) wx) @@ -2310,6 +2571,7 @@ Module Make (W0:W0Type). Definition w10_div_gt := w10_op.(znz_div_gt). Definition w11_div_gt := w11_op.(znz_div_gt). Definition w12_div_gt := w12_op.(znz_div_gt). + Definition w13_div_gt := w13_op.(znz_div_gt). Definition w0_divn1 := gen_divn1 w0_op.(znz_zdigits) w0_op.(znz_0) @@ -2376,6 +2638,11 @@ Module Make (W0:W0Type). w12_op.(znz_WW) w12_op.(znz_head0) w12_op.(znz_add_mul_div) w12_op.(znz_div21) w12_op.(znz_compare) w12_op.(znz_sub). + Definition w13_divn1 := + gen_divn1 w13_op.(znz_zdigits) w13_op.(znz_0) + w13_op.(znz_WW) w13_op.(znz_head0) + w13_op.(znz_add_mul_div) w13_op.(znz_div21) + w13_op.(znz_compare) w13_op.(znz_sub). Definition div_gt x y := match x, y with @@ -2428,8 +2695,12 @@ Module Make (W0:W0Type). let wx':= GenBase.extend w0_0W 11 wx in let (q, r):= w12_div_gt wx' wy in (reduce_12 q, reduce_12 r) + | N0 wx, N13 wy => + let wx':= GenBase.extend w0_0W 12 wx in + let (q, r):= w13_div_gt wx' wy in + (reduce_13 q, reduce_13 r) | N0 wx, Nn n wy => - let wx':= extend n w12 (GenBase.extend w0_0W 12 wx) in + let wx':= extend n w13 (GenBase.extend w0_0W 13 wx) in let (q, r):= (make_op n).(znz_div_gt) wx' wy in (reduce_n n q, reduce_n n r) | N1 wx, N0 wy => let (q, r):= w0_divn1 1 wx wy in (reduce_1 q, reduce_0 r) @@ -2478,8 +2749,12 @@ Module Make (W0:W0Type). let wx':= GenBase.extend w1_0W 10 wx in let (q, r):= w12_div_gt wx' wy in (reduce_12 q, reduce_12 r) + | N1 wx, N13 wy => + let wx':= GenBase.extend w1_0W 11 wx in + let (q, r):= w13_div_gt wx' wy in + (reduce_13 q, reduce_13 r) | N1 wx, Nn n wy => - let wx':= extend n w12 (GenBase.extend w1_0W 11 wx) in + let wx':= extend n w13 (GenBase.extend w1_0W 12 wx) in let (q, r):= (make_op n).(znz_div_gt) wx' wy in (reduce_n n q, reduce_n n r) | N2 wx, N0 wy => let (q, r):= w0_divn1 2 wx wy in (reduce_2 q, reduce_0 r) @@ -2525,8 +2800,12 @@ Module Make (W0:W0Type). let wx':= GenBase.extend w2_0W 9 wx in let (q, r):= w12_div_gt wx' wy in (reduce_12 q, reduce_12 r) + | N2 wx, N13 wy => + let wx':= GenBase.extend w2_0W 10 wx in + let (q, r):= w13_div_gt wx' wy in + (reduce_13 q, reduce_13 r) | N2 wx, Nn n wy => - let wx':= extend n w12 (GenBase.extend w2_0W 10 wx) in + let wx':= extend n w13 (GenBase.extend w2_0W 11 wx) in let (q, r):= (make_op n).(znz_div_gt) wx' wy in (reduce_n n q, reduce_n n r) | N3 wx, N0 wy => let (q, r):= w0_divn1 3 wx wy in (reduce_3 q, reduce_0 r) @@ -2569,8 +2848,12 @@ Module Make (W0:W0Type). let wx':= GenBase.extend w3_0W 8 wx in let (q, r):= w12_div_gt wx' wy in (reduce_12 q, reduce_12 r) + | N3 wx, N13 wy => + let wx':= GenBase.extend w3_0W 9 wx in + let (q, r):= w13_div_gt wx' wy in + (reduce_13 q, reduce_13 r) | N3 wx, Nn n wy => - let wx':= extend n w12 (GenBase.extend w3_0W 9 wx) in + let wx':= extend n w13 (GenBase.extend w3_0W 10 wx) in let (q, r):= (make_op n).(znz_div_gt) wx' wy in (reduce_n n q, reduce_n n r) | N4 wx, N0 wy => let (q, r):= w0_divn1 4 wx wy in (reduce_4 q, reduce_0 r) @@ -2610,8 +2893,12 @@ Module Make (W0:W0Type). let wx':= GenBase.extend w4_0W 7 wx in let (q, r):= w12_div_gt wx' wy in (reduce_12 q, reduce_12 r) + | N4 wx, N13 wy => + let wx':= GenBase.extend w4_0W 8 wx in + let (q, r):= w13_div_gt wx' wy in + (reduce_13 q, reduce_13 r) | N4 wx, Nn n wy => - let wx':= extend n w12 (GenBase.extend w4_0W 8 wx) in + let wx':= extend n w13 (GenBase.extend w4_0W 9 wx) in let (q, r):= (make_op n).(znz_div_gt) wx' wy in (reduce_n n q, reduce_n n r) | N5 wx, N0 wy => let (q, r):= w0_divn1 5 wx wy in (reduce_5 q, reduce_0 r) @@ -2648,8 +2935,12 @@ Module Make (W0:W0Type). let wx':= GenBase.extend w5_0W 6 wx in let (q, r):= w12_div_gt wx' wy in (reduce_12 q, reduce_12 r) + | N5 wx, N13 wy => + let wx':= GenBase.extend w5_0W 7 wx in + let (q, r):= w13_div_gt wx' wy in + (reduce_13 q, reduce_13 r) | N5 wx, Nn n wy => - let wx':= extend n w12 (GenBase.extend w5_0W 7 wx) in + let wx':= extend n w13 (GenBase.extend w5_0W 8 wx) in let (q, r):= (make_op n).(znz_div_gt) wx' wy in (reduce_n n q, reduce_n n r) | N6 wx, N0 wy => let (q, r):= w0_divn1 6 wx wy in (reduce_6 q, reduce_0 r) @@ -2683,8 +2974,12 @@ Module Make (W0:W0Type). let wx':= GenBase.extend w6_0W 5 wx in let (q, r):= w12_div_gt wx' wy in (reduce_12 q, reduce_12 r) + | N6 wx, N13 wy => + let wx':= GenBase.extend w6_0W 6 wx in + let (q, r):= w13_div_gt wx' wy in + (reduce_13 q, reduce_13 r) | N6 wx, Nn n wy => - let wx':= extend n w12 (GenBase.extend w6_0W 6 wx) in + let wx':= extend n w13 (GenBase.extend w6_0W 7 wx) in let (q, r):= (make_op n).(znz_div_gt) wx' wy in (reduce_n n q, reduce_n n r) | N7 wx, N0 wy => let (q, r):= w0_divn1 7 wx wy in (reduce_7 q, reduce_0 r) @@ -2715,8 +3010,12 @@ Module Make (W0:W0Type). let wx':= GenBase.extend w7_0W 4 wx in let (q, r):= w12_div_gt wx' wy in (reduce_12 q, reduce_12 r) + | N7 wx, N13 wy => + let wx':= GenBase.extend w7_0W 5 wx in + let (q, r):= w13_div_gt wx' wy in + (reduce_13 q, reduce_13 r) | N7 wx, Nn n wy => - let wx':= extend n w12 (GenBase.extend w7_0W 5 wx) in + let wx':= extend n w13 (GenBase.extend w7_0W 6 wx) in let (q, r):= (make_op n).(znz_div_gt) wx' wy in (reduce_n n q, reduce_n n r) | N8 wx, N0 wy => let (q, r):= w0_divn1 8 wx wy in (reduce_8 q, reduce_0 r) @@ -2744,8 +3043,12 @@ Module Make (W0:W0Type). let wx':= GenBase.extend w8_0W 3 wx in let (q, r):= w12_div_gt wx' wy in (reduce_12 q, reduce_12 r) + | N8 wx, N13 wy => + let wx':= GenBase.extend w8_0W 4 wx in + let (q, r):= w13_div_gt wx' wy in + (reduce_13 q, reduce_13 r) | N8 wx, Nn n wy => - let wx':= extend n w12 (GenBase.extend w8_0W 4 wx) in + let wx':= extend n w13 (GenBase.extend w8_0W 5 wx) in let (q, r):= (make_op n).(znz_div_gt) wx' wy in (reduce_n n q, reduce_n n r) | N9 wx, N0 wy => let (q, r):= w0_divn1 9 wx wy in (reduce_9 q, reduce_0 r) @@ -2770,8 +3073,12 @@ Module Make (W0:W0Type). let wx':= GenBase.extend w9_0W 2 wx in let (q, r):= w12_div_gt wx' wy in (reduce_12 q, reduce_12 r) + | N9 wx, N13 wy => + let wx':= GenBase.extend w9_0W 3 wx in + let (q, r):= w13_div_gt wx' wy in + (reduce_13 q, reduce_13 r) | N9 wx, Nn n wy => - let wx':= extend n w12 (GenBase.extend w9_0W 3 wx) in + let wx':= extend n w13 (GenBase.extend w9_0W 4 wx) in let (q, r):= (make_op n).(znz_div_gt) wx' wy in (reduce_n n q, reduce_n n r) | N10 wx, N0 wy => let (q, r):= w0_divn1 10 wx wy in (reduce_10 q, reduce_0 r) @@ -2793,8 +3100,12 @@ Module Make (W0:W0Type). let wx':= GenBase.extend w10_0W 1 wx in let (q, r):= w12_div_gt wx' wy in (reduce_12 q, reduce_12 r) + | N10 wx, N13 wy => + let wx':= GenBase.extend w10_0W 2 wx in + let (q, r):= w13_div_gt wx' wy in + (reduce_13 q, reduce_13 r) | N10 wx, Nn n wy => - let wx':= extend n w12 (GenBase.extend w10_0W 2 wx) in + let wx':= extend n w13 (GenBase.extend w10_0W 3 wx) in let (q, r):= (make_op n).(znz_div_gt) wx' wy in (reduce_n n q, reduce_n n r) | N11 wx, N0 wy => let (q, r):= w0_divn1 11 wx wy in (reduce_11 q, reduce_0 r) @@ -2813,8 +3124,12 @@ Module Make (W0:W0Type). let wx':= GenBase.extend w11_0W 0 wx in let (q, r):= w12_div_gt wx' wy in (reduce_12 q, reduce_12 r) + | N11 wx, N13 wy => + let wx':= GenBase.extend w11_0W 1 wx in + let (q, r):= w13_div_gt wx' wy in + (reduce_13 q, reduce_13 r) | N11 wx, Nn n wy => - let wx':= extend n w12 (GenBase.extend w11_0W 1 wx) in + let wx':= extend n w13 (GenBase.extend w11_0W 2 wx) in let (q, r):= (make_op n).(znz_div_gt) wx' wy in (reduce_n n q, reduce_n n r) | N12 wx, N0 wy => let (q, r):= w0_divn1 12 wx wy in (reduce_12 q, reduce_0 r) @@ -2830,62 +3145,88 @@ Module Make (W0:W0Type). | N12 wx, N10 wy => let (q, r):= w10_divn1 2 wx wy in (reduce_12 q, reduce_10 r) | N12 wx, N11 wy => let (q, r):= w11_divn1 1 wx wy in (reduce_12 q, reduce_11 r) | N12 wx, N12 wy => let (q, r):= w12_div_gt wx wy in (reduce_12 q, reduce_12 r) + | N12 wx, N13 wy => + let wx':= GenBase.extend w12_0W 0 wx in + let (q, r):= w13_div_gt wx' wy in + (reduce_13 q, reduce_13 r) | N12 wx, Nn n wy => - let wx':= extend n w12 (GenBase.extend w12_0W 0 wx) in + let wx':= extend n w13 (GenBase.extend w12_0W 1 wx) in + let (q, r):= (make_op n).(znz_div_gt) wx' wy in + (reduce_n n q, reduce_n n r) + | N13 wx, N0 wy => let (q, r):= w0_divn1 13 wx wy in (reduce_13 q, reduce_0 r) + | N13 wx, N1 wy => let (q, r):= w1_divn1 12 wx wy in (reduce_13 q, reduce_1 r) + | N13 wx, N2 wy => let (q, r):= w2_divn1 11 wx wy in (reduce_13 q, reduce_2 r) + | N13 wx, N3 wy => let (q, r):= w3_divn1 10 wx wy in (reduce_13 q, reduce_3 r) + | N13 wx, N4 wy => let (q, r):= w4_divn1 9 wx wy in (reduce_13 q, reduce_4 r) + | N13 wx, N5 wy => let (q, r):= w5_divn1 8 wx wy in (reduce_13 q, reduce_5 r) + | N13 wx, N6 wy => let (q, r):= w6_divn1 7 wx wy in (reduce_13 q, reduce_6 r) + | N13 wx, N7 wy => let (q, r):= w7_divn1 6 wx wy in (reduce_13 q, reduce_7 r) + | N13 wx, N8 wy => let (q, r):= w8_divn1 5 wx wy in (reduce_13 q, reduce_8 r) + | N13 wx, N9 wy => let (q, r):= w9_divn1 4 wx wy in (reduce_13 q, reduce_9 r) + | N13 wx, N10 wy => let (q, r):= w10_divn1 3 wx wy in (reduce_13 q, reduce_10 r) + | N13 wx, N11 wy => let (q, r):= w11_divn1 2 wx wy in (reduce_13 q, reduce_11 r) + | N13 wx, N12 wy => let (q, r):= w12_divn1 1 wx wy in (reduce_13 q, reduce_12 r) + | N13 wx, N13 wy => let (q, r):= w13_div_gt wx wy in (reduce_13 q, reduce_13 r) + | N13 wx, Nn n wy => + let wx':= extend n w13 (GenBase.extend w13_0W 0 wx) in let (q, r):= (make_op n).(znz_div_gt) wx' wy in (reduce_n n q, reduce_n n r) | Nn n wx, N0 wy => - let wy':= GenBase.extend w0_0W 11 wy in - let (q, r):= w12_divn1 (S n) wx wy' in - (reduce_n n q, reduce_12 r) + let wy':= GenBase.extend w0_0W 12 wy in + let (q, r):= w13_divn1 (S n) wx wy' in + (reduce_n n q, reduce_13 r) | Nn n wx, N1 wy => - let wy':= GenBase.extend w1_0W 10 wy in - let (q, r):= w12_divn1 (S n) wx wy' in - (reduce_n n q, reduce_12 r) + let wy':= GenBase.extend w1_0W 11 wy in + let (q, r):= w13_divn1 (S n) wx wy' in + (reduce_n n q, reduce_13 r) | Nn n wx, N2 wy => - let wy':= GenBase.extend w2_0W 9 wy in - let (q, r):= w12_divn1 (S n) wx wy' in - (reduce_n n q, reduce_12 r) + let wy':= GenBase.extend w2_0W 10 wy in + let (q, r):= w13_divn1 (S n) wx wy' in + (reduce_n n q, reduce_13 r) | Nn n wx, N3 wy => - let wy':= GenBase.extend w3_0W 8 wy in - let (q, r):= w12_divn1 (S n) wx wy' in - (reduce_n n q, reduce_12 r) + let wy':= GenBase.extend w3_0W 9 wy in + let (q, r):= w13_divn1 (S n) wx wy' in + (reduce_n n q, reduce_13 r) | Nn n wx, N4 wy => - let wy':= GenBase.extend w4_0W 7 wy in - let (q, r):= w12_divn1 (S n) wx wy' in - (reduce_n n q, reduce_12 r) + let wy':= GenBase.extend w4_0W 8 wy in + let (q, r):= w13_divn1 (S n) wx wy' in + (reduce_n n q, reduce_13 r) | Nn n wx, N5 wy => - let wy':= GenBase.extend w5_0W 6 wy in - let (q, r):= w12_divn1 (S n) wx wy' in - (reduce_n n q, reduce_12 r) + let wy':= GenBase.extend w5_0W 7 wy in + let (q, r):= w13_divn1 (S n) wx wy' in + (reduce_n n q, reduce_13 r) | Nn n wx, N6 wy => - let wy':= GenBase.extend w6_0W 5 wy in - let (q, r):= w12_divn1 (S n) wx wy' in - (reduce_n n q, reduce_12 r) + let wy':= GenBase.extend w6_0W 6 wy in + let (q, r):= w13_divn1 (S n) wx wy' in + (reduce_n n q, reduce_13 r) | Nn n wx, N7 wy => - let wy':= GenBase.extend w7_0W 4 wy in - let (q, r):= w12_divn1 (S n) wx wy' in - (reduce_n n q, reduce_12 r) + let wy':= GenBase.extend w7_0W 5 wy in + let (q, r):= w13_divn1 (S n) wx wy' in + (reduce_n n q, reduce_13 r) | Nn n wx, N8 wy => - let wy':= GenBase.extend w8_0W 3 wy in - let (q, r):= w12_divn1 (S n) wx wy' in - (reduce_n n q, reduce_12 r) + let wy':= GenBase.extend w8_0W 4 wy in + let (q, r):= w13_divn1 (S n) wx wy' in + (reduce_n n q, reduce_13 r) | Nn n wx, N9 wy => - let wy':= GenBase.extend w9_0W 2 wy in - let (q, r):= w12_divn1 (S n) wx wy' in - (reduce_n n q, reduce_12 r) + let wy':= GenBase.extend w9_0W 3 wy in + let (q, r):= w13_divn1 (S n) wx wy' in + (reduce_n n q, reduce_13 r) | Nn n wx, N10 wy => - let wy':= GenBase.extend w10_0W 1 wy in - let (q, r):= w12_divn1 (S n) wx wy' in - (reduce_n n q, reduce_12 r) + let wy':= GenBase.extend w10_0W 2 wy in + let (q, r):= w13_divn1 (S n) wx wy' in + (reduce_n n q, reduce_13 r) | Nn n wx, N11 wy => - let wy':= GenBase.extend w11_0W 0 wy in - let (q, r):= w12_divn1 (S n) wx wy' in - (reduce_n n q, reduce_12 r) + let wy':= GenBase.extend w11_0W 1 wy in + let (q, r):= w13_divn1 (S n) wx wy' in + (reduce_n n q, reduce_13 r) | Nn n wx, N12 wy => + let wy':= GenBase.extend w12_0W 0 wy in + let (q, r):= w13_divn1 (S n) wx wy' in + (reduce_n n q, reduce_13 r) + | Nn n wx, N13 wy => let wy':= wy in - let (q, r):= w12_divn1 (S n) wx wy' in - (reduce_n n q, reduce_12 r) + let (q, r):= w13_divn1 (S n) wx wy' in + (reduce_n n q, reduce_13 r) | Nn n wx, Nn m wy => let mn := Max.max n m in let d := diff n m in @@ -2918,6 +3259,7 @@ Module Make (W0:W0Type). Definition w10_mod_gt := w10_op.(znz_mod_gt). Definition w11_mod_gt := w11_op.(znz_mod_gt). Definition w12_mod_gt := w12_op.(znz_mod_gt). + Definition w13_mod_gt := w13_op.(znz_mod_gt). Definition w0_modn1 := gen_modn1 w0_op.(znz_zdigits) w0_op.(znz_0) @@ -2971,6 +3313,10 @@ Module Make (W0:W0Type). gen_modn1 w12_op.(znz_zdigits) w12_op.(znz_0) w12_op.(znz_head0) w12_op.(znz_add_mul_div) w12_op.(znz_div21) w12_op.(znz_compare) w12_op.(znz_sub). + Definition w13_modn1 := + gen_modn1 w13_op.(znz_zdigits) w13_op.(znz_0) + w13_op.(znz_head0) w13_op.(znz_add_mul_div) w13_op.(znz_div21) + w13_op.(znz_compare) w13_op.(znz_sub). Definition mod_gt x y := match x, y with @@ -3011,8 +3357,11 @@ Module Make (W0:W0Type). | N0 wx, N12 wy => let wx':= GenBase.extend w0_0W 11 wx in reduce_12 (w12_mod_gt wx' wy) + | N0 wx, N13 wy => + let wx':= GenBase.extend w0_0W 12 wx in + reduce_13 (w13_mod_gt wx' wy) | N0 wx, Nn n wy => - let wx':= extend n w12 (GenBase.extend w0_0W 12 wx) in + let wx':= extend n w13 (GenBase.extend w0_0W 13 wx) in reduce_n n ((make_op n).(znz_mod_gt) wx' wy) | N1 wx, N0 wy => reduce_0 (w0_modn1 1 wx wy) | N1 wx, N1 wy => reduce_1 (w1_mod_gt wx wy) @@ -3049,8 +3398,11 @@ Module Make (W0:W0Type). | N1 wx, N12 wy => let wx':= GenBase.extend w1_0W 10 wx in reduce_12 (w12_mod_gt wx' wy) + | N1 wx, N13 wy => + let wx':= GenBase.extend w1_0W 11 wx in + reduce_13 (w13_mod_gt wx' wy) | N1 wx, Nn n wy => - let wx':= extend n w12 (GenBase.extend w1_0W 11 wx) in + let wx':= extend n w13 (GenBase.extend w1_0W 12 wx) in reduce_n n ((make_op n).(znz_mod_gt) wx' wy) | N2 wx, N0 wy => reduce_0 (w0_modn1 2 wx wy) | N2 wx, N1 wy => reduce_1 (w1_modn1 1 wx wy) @@ -3085,8 +3437,11 @@ Module Make (W0:W0Type). | N2 wx, N12 wy => let wx':= GenBase.extend w2_0W 9 wx in reduce_12 (w12_mod_gt wx' wy) + | N2 wx, N13 wy => + let wx':= GenBase.extend w2_0W 10 wx in + reduce_13 (w13_mod_gt wx' wy) | N2 wx, Nn n wy => - let wx':= extend n w12 (GenBase.extend w2_0W 10 wx) in + let wx':= extend n w13 (GenBase.extend w2_0W 11 wx) in reduce_n n ((make_op n).(znz_mod_gt) wx' wy) | N3 wx, N0 wy => reduce_0 (w0_modn1 3 wx wy) | N3 wx, N1 wy => reduce_1 (w1_modn1 2 wx wy) @@ -3119,8 +3474,11 @@ Module Make (W0:W0Type). | N3 wx, N12 wy => let wx':= GenBase.extend w3_0W 8 wx in reduce_12 (w12_mod_gt wx' wy) + | N3 wx, N13 wy => + let wx':= GenBase.extend w3_0W 9 wx in + reduce_13 (w13_mod_gt wx' wy) | N3 wx, Nn n wy => - let wx':= extend n w12 (GenBase.extend w3_0W 9 wx) in + let wx':= extend n w13 (GenBase.extend w3_0W 10 wx) in reduce_n n ((make_op n).(znz_mod_gt) wx' wy) | N4 wx, N0 wy => reduce_0 (w0_modn1 4 wx wy) | N4 wx, N1 wy => reduce_1 (w1_modn1 3 wx wy) @@ -3151,8 +3509,11 @@ Module Make (W0:W0Type). | N4 wx, N12 wy => let wx':= GenBase.extend w4_0W 7 wx in reduce_12 (w12_mod_gt wx' wy) + | N4 wx, N13 wy => + let wx':= GenBase.extend w4_0W 8 wx in + reduce_13 (w13_mod_gt wx' wy) | N4 wx, Nn n wy => - let wx':= extend n w12 (GenBase.extend w4_0W 8 wx) in + let wx':= extend n w13 (GenBase.extend w4_0W 9 wx) in reduce_n n ((make_op n).(znz_mod_gt) wx' wy) | N5 wx, N0 wy => reduce_0 (w0_modn1 5 wx wy) | N5 wx, N1 wy => reduce_1 (w1_modn1 4 wx wy) @@ -3181,8 +3542,11 @@ Module Make (W0:W0Type). | N5 wx, N12 wy => let wx':= GenBase.extend w5_0W 6 wx in reduce_12 (w12_mod_gt wx' wy) + | N5 wx, N13 wy => + let wx':= GenBase.extend w5_0W 7 wx in + reduce_13 (w13_mod_gt wx' wy) | N5 wx, Nn n wy => - let wx':= extend n w12 (GenBase.extend w5_0W 7 wx) in + let wx':= extend n w13 (GenBase.extend w5_0W 8 wx) in reduce_n n ((make_op n).(znz_mod_gt) wx' wy) | N6 wx, N0 wy => reduce_0 (w0_modn1 6 wx wy) | N6 wx, N1 wy => reduce_1 (w1_modn1 5 wx wy) @@ -3209,8 +3573,11 @@ Module Make (W0:W0Type). | N6 wx, N12 wy => let wx':= GenBase.extend w6_0W 5 wx in reduce_12 (w12_mod_gt wx' wy) + | N6 wx, N13 wy => + let wx':= GenBase.extend w6_0W 6 wx in + reduce_13 (w13_mod_gt wx' wy) | N6 wx, Nn n wy => - let wx':= extend n w12 (GenBase.extend w6_0W 6 wx) in + let wx':= extend n w13 (GenBase.extend w6_0W 7 wx) in reduce_n n ((make_op n).(znz_mod_gt) wx' wy) | N7 wx, N0 wy => reduce_0 (w0_modn1 7 wx wy) | N7 wx, N1 wy => reduce_1 (w1_modn1 6 wx wy) @@ -3235,8 +3602,11 @@ Module Make (W0:W0Type). | N7 wx, N12 wy => let wx':= GenBase.extend w7_0W 4 wx in reduce_12 (w12_mod_gt wx' wy) + | N7 wx, N13 wy => + let wx':= GenBase.extend w7_0W 5 wx in + reduce_13 (w13_mod_gt wx' wy) | N7 wx, Nn n wy => - let wx':= extend n w12 (GenBase.extend w7_0W 5 wx) in + let wx':= extend n w13 (GenBase.extend w7_0W 6 wx) in reduce_n n ((make_op n).(znz_mod_gt) wx' wy) | N8 wx, N0 wy => reduce_0 (w0_modn1 8 wx wy) | N8 wx, N1 wy => reduce_1 (w1_modn1 7 wx wy) @@ -3259,8 +3629,11 @@ Module Make (W0:W0Type). | N8 wx, N12 wy => let wx':= GenBase.extend w8_0W 3 wx in reduce_12 (w12_mod_gt wx' wy) + | N8 wx, N13 wy => + let wx':= GenBase.extend w8_0W 4 wx in + reduce_13 (w13_mod_gt wx' wy) | N8 wx, Nn n wy => - let wx':= extend n w12 (GenBase.extend w8_0W 4 wx) in + let wx':= extend n w13 (GenBase.extend w8_0W 5 wx) in reduce_n n ((make_op n).(znz_mod_gt) wx' wy) | N9 wx, N0 wy => reduce_0 (w0_modn1 9 wx wy) | N9 wx, N1 wy => reduce_1 (w1_modn1 8 wx wy) @@ -3281,8 +3654,11 @@ Module Make (W0:W0Type). | N9 wx, N12 wy => let wx':= GenBase.extend w9_0W 2 wx in reduce_12 (w12_mod_gt wx' wy) + | N9 wx, N13 wy => + let wx':= GenBase.extend w9_0W 3 wx in + reduce_13 (w13_mod_gt wx' wy) | N9 wx, Nn n wy => - let wx':= extend n w12 (GenBase.extend w9_0W 3 wx) in + let wx':= extend n w13 (GenBase.extend w9_0W 4 wx) in reduce_n n ((make_op n).(znz_mod_gt) wx' wy) | N10 wx, N0 wy => reduce_0 (w0_modn1 10 wx wy) | N10 wx, N1 wy => reduce_1 (w1_modn1 9 wx wy) @@ -3301,8 +3677,11 @@ Module Make (W0:W0Type). | N10 wx, N12 wy => let wx':= GenBase.extend w10_0W 1 wx in reduce_12 (w12_mod_gt wx' wy) + | N10 wx, N13 wy => + let wx':= GenBase.extend w10_0W 2 wx in + reduce_13 (w13_mod_gt wx' wy) | N10 wx, Nn n wy => - let wx':= extend n w12 (GenBase.extend w10_0W 2 wx) in + let wx':= extend n w13 (GenBase.extend w10_0W 3 wx) in reduce_n n ((make_op n).(znz_mod_gt) wx' wy) | N11 wx, N0 wy => reduce_0 (w0_modn1 11 wx wy) | N11 wx, N1 wy => reduce_1 (w1_modn1 10 wx wy) @@ -3319,8 +3698,11 @@ Module Make (W0:W0Type). | N11 wx, N12 wy => let wx':= GenBase.extend w11_0W 0 wx in reduce_12 (w12_mod_gt wx' wy) + | N11 wx, N13 wy => + let wx':= GenBase.extend w11_0W 1 wx in + reduce_13 (w13_mod_gt wx' wy) | N11 wx, Nn n wy => - let wx':= extend n w12 (GenBase.extend w11_0W 1 wx) in + let wx':= extend n w13 (GenBase.extend w11_0W 2 wx) in reduce_n n ((make_op n).(znz_mod_gt) wx' wy) | N12 wx, N0 wy => reduce_0 (w0_modn1 12 wx wy) | N12 wx, N1 wy => reduce_1 (w1_modn1 11 wx wy) @@ -3335,48 +3717,71 @@ Module Make (W0:W0Type). | N12 wx, N10 wy => reduce_10 (w10_modn1 2 wx wy) | N12 wx, N11 wy => reduce_11 (w11_modn1 1 wx wy) | N12 wx, N12 wy => reduce_12 (w12_mod_gt wx wy) + | N12 wx, N13 wy => + let wx':= GenBase.extend w12_0W 0 wx in + reduce_13 (w13_mod_gt wx' wy) | N12 wx, Nn n wy => - let wx':= extend n w12 (GenBase.extend w12_0W 0 wx) in + let wx':= extend n w13 (GenBase.extend w12_0W 1 wx) in + reduce_n n ((make_op n).(znz_mod_gt) wx' wy) + | N13 wx, N0 wy => reduce_0 (w0_modn1 13 wx wy) + | N13 wx, N1 wy => reduce_1 (w1_modn1 12 wx wy) + | N13 wx, N2 wy => reduce_2 (w2_modn1 11 wx wy) + | N13 wx, N3 wy => reduce_3 (w3_modn1 10 wx wy) + | N13 wx, N4 wy => reduce_4 (w4_modn1 9 wx wy) + | N13 wx, N5 wy => reduce_5 (w5_modn1 8 wx wy) + | N13 wx, N6 wy => reduce_6 (w6_modn1 7 wx wy) + | N13 wx, N7 wy => reduce_7 (w7_modn1 6 wx wy) + | N13 wx, N8 wy => reduce_8 (w8_modn1 5 wx wy) + | N13 wx, N9 wy => reduce_9 (w9_modn1 4 wx wy) + | N13 wx, N10 wy => reduce_10 (w10_modn1 3 wx wy) + | N13 wx, N11 wy => reduce_11 (w11_modn1 2 wx wy) + | N13 wx, N12 wy => reduce_12 (w12_modn1 1 wx wy) + | N13 wx, N13 wy => reduce_13 (w13_mod_gt wx wy) + | N13 wx, Nn n wy => + let wx':= extend n w13 (GenBase.extend w13_0W 0 wx) in reduce_n n ((make_op n).(znz_mod_gt) wx' wy) | Nn n wx, N0 wy => - let wy':= GenBase.extend w0_0W 11 wy in - reduce_12 (w12_modn1 (S n) wx wy') + let wy':= GenBase.extend w0_0W 12 wy in + reduce_13 (w13_modn1 (S n) wx wy') | Nn n wx, N1 wy => - let wy':= GenBase.extend w1_0W 10 wy in - reduce_12 (w12_modn1 (S n) wx wy') + let wy':= GenBase.extend w1_0W 11 wy in + reduce_13 (w13_modn1 (S n) wx wy') | Nn n wx, N2 wy => - let wy':= GenBase.extend w2_0W 9 wy in - reduce_12 (w12_modn1 (S n) wx wy') + let wy':= GenBase.extend w2_0W 10 wy in + reduce_13 (w13_modn1 (S n) wx wy') | Nn n wx, N3 wy => - let wy':= GenBase.extend w3_0W 8 wy in - reduce_12 (w12_modn1 (S n) wx wy') + let wy':= GenBase.extend w3_0W 9 wy in + reduce_13 (w13_modn1 (S n) wx wy') | Nn n wx, N4 wy => - let wy':= GenBase.extend w4_0W 7 wy in - reduce_12 (w12_modn1 (S n) wx wy') + let wy':= GenBase.extend w4_0W 8 wy in + reduce_13 (w13_modn1 (S n) wx wy') | Nn n wx, N5 wy => - let wy':= GenBase.extend w5_0W 6 wy in - reduce_12 (w12_modn1 (S n) wx wy') + let wy':= GenBase.extend w5_0W 7 wy in + reduce_13 (w13_modn1 (S n) wx wy') | Nn n wx, N6 wy => - let wy':= GenBase.extend w6_0W 5 wy in - reduce_12 (w12_modn1 (S n) wx wy') + let wy':= GenBase.extend w6_0W 6 wy in + reduce_13 (w13_modn1 (S n) wx wy') | Nn n wx, N7 wy => - let wy':= GenBase.extend w7_0W 4 wy in - reduce_12 (w12_modn1 (S n) wx wy') + let wy':= GenBase.extend w7_0W 5 wy in + reduce_13 (w13_modn1 (S n) wx wy') | Nn n wx, N8 wy => - let wy':= GenBase.extend w8_0W 3 wy in - reduce_12 (w12_modn1 (S n) wx wy') + let wy':= GenBase.extend w8_0W 4 wy in + reduce_13 (w13_modn1 (S n) wx wy') | Nn n wx, N9 wy => - let wy':= GenBase.extend w9_0W 2 wy in - reduce_12 (w12_modn1 (S n) wx wy') + let wy':= GenBase.extend w9_0W 3 wy in + reduce_13 (w13_modn1 (S n) wx wy') | Nn n wx, N10 wy => - let wy':= GenBase.extend w10_0W 1 wy in - reduce_12 (w12_modn1 (S n) wx wy') + let wy':= GenBase.extend w10_0W 2 wy in + reduce_13 (w13_modn1 (S n) wx wy') | Nn n wx, N11 wy => - let wy':= GenBase.extend w11_0W 0 wy in - reduce_12 (w12_modn1 (S n) wx wy') + let wy':= GenBase.extend w11_0W 1 wy in + reduce_13 (w13_modn1 (S n) wx wy') | Nn n wx, N12 wy => + let wy':= GenBase.extend w12_0W 0 wy in + reduce_13 (w13_modn1 (S n) wx wy') + | Nn n wx, N13 wy => let wy':= wy in - reduce_12 (w12_modn1 (S n) wx wy') + reduce_13 (w13_modn1 (S n) wx wy') | Nn n wx, Nn m wy => let mn := Max.max n m in let d := diff n m in @@ -3408,6 +3813,7 @@ Module Make (W0:W0Type). | N10 _ => w10_op.(znz_digits) | N11 _ => w11_op.(znz_digits) | N12 _ => w12_op.(znz_digits) + | N13 _ => w13_op.(znz_digits) | Nn n _ => (make_op n).(znz_digits) end. @@ -3461,8 +3867,9 @@ Definition pheight p := Peano.pred (nat_of_P (get_height w0_op.(znz_digits) (ple | (S (S (S (S (S (S (S (S (S (S O)))))))))) => reduce_10 (snd (w10_op.(znz_of_pos) x)) | (S (S (S (S (S (S (S (S (S (S (S O))))))))))) => reduce_11 (snd (w11_op.(znz_of_pos) x)) | (S (S (S (S (S (S (S (S (S (S (S (S O)))))))))))) => reduce_12 (snd (w12_op.(znz_of_pos) x)) + | (S (S (S (S (S (S (S (S (S (S (S (S (S O))))))))))))) => reduce_13 (snd (w13_op.(znz_of_pos) x)) | _ => - let n := minus h 13 in + let n := minus h 14 in reduce_n n (snd ((make_op n).(znz_of_pos) x)) end. @@ -3487,6 +3894,7 @@ Definition pheight p := Peano.pred (nat_of_P (get_height w0_op.(znz_digits) (ple | N10 wx => w10_op.(znz_to_Z) wx | N11 wx => w11_op.(znz_to_Z) wx | N12 wx => w12_op.(znz_to_Z) wx + | N13 wx => w13_op.(znz_to_Z) wx | Nn n wx => (make_op n).(znz_to_Z) wx end. @@ -3504,6 +3912,7 @@ Definition pheight p := Peano.pred (nat_of_P (get_height w0_op.(znz_digits) (ple | N10 w=> reduce_10 (w10_op.(znz_head0) w) | N11 w=> reduce_11 (w11_op.(znz_head0) w) | N12 w=> reduce_12 (w12_op.(znz_head0) w) + | N13 w=> reduce_13 (w13_op.(znz_head0) w) | Nn n w=> reduce_n n ((make_op n).(znz_head0) w) end. @@ -3521,6 +3930,7 @@ Definition pheight p := Peano.pred (nat_of_P (get_height w0_op.(znz_digits) (ple | N10 w=> reduce_10 (w10_op.(znz_tail0) w) | N11 w=> reduce_11 (w11_op.(znz_tail0) w) | N12 w=> reduce_12 (w12_op.(znz_tail0) w) + | N13 w=> reduce_13 (w13_op.(znz_tail0) w) | Nn n w=> reduce_n n ((make_op n).(znz_tail0) w) end. @@ -3539,11 +3949,12 @@ Definition pheight p := Peano.pred (nat_of_P (get_height w0_op.(znz_digits) (ple | N10 _ => reduce_10 w10_op.(znz_zdigits) | N11 _ => reduce_11 w11_op.(znz_zdigits) | N12 _ => reduce_12 w12_op.(znz_zdigits) + | N13 _ => reduce_13 w13_op.(znz_zdigits) | Nn n _ => reduce_n n (make_op n).(znz_zdigits) end. - Definition level f0 f1 f2 f3 f4 f5 f6 f7 f8 f9 f10 f11 f12 fn x y: t_ := match x, y with + Definition level f0 f1 f2 f3 f4 f5 f6 f7 f8 f9 f10 f11 f12 f13 fn x y: t_ := match x, y with | N0 wx, N0 wy => f0 wx wy | N0 wx, N1 wy => f1 (WW w_0 wx) wy | N0 wx, N2 wy => f2 (extend1 w0 (WW w_0 wx)) wy @@ -3557,8 +3968,9 @@ Definition pheight p := Peano.pred (nat_of_P (get_height w0_op.(znz_digits) (ple | N0 wx, N10 wy => f10 (extend9 w0 (WW w_0 wx)) wy | N0 wx, N11 wy => f11 (extend10 w0 (WW w_0 wx)) wy | N0 wx, N12 wy => f12 (extend11 w0 (WW w_0 wx)) wy + | N0 wx, N13 wy => f13 (extend12 w0 (WW w_0 wx)) wy | N0 wx, Nn n wy => - fn n (extend n w12 (extend12 w0 (WW w_0 wx))) wy + fn n (extend n w13 (extend13 w0 (WW w_0 wx))) wy | N1 wx, N0 wy => f1 wx (WW w_0 wy) | N1 wx, N1 wy => f1 wx wy @@ -3573,7 +3985,8 @@ Definition pheight p := Peano.pred (nat_of_P (get_height w0_op.(znz_digits) (ple | N1 wx, N10 wy => f10 (extend9 w0 wx) wy | N1 wx, N11 wy => f11 (extend10 w0 wx) wy | N1 wx, N12 wy => f12 (extend11 w0 wx) wy - | N1 wx, Nn n wy => fn n (extend n w12 (extend12 w0 wx)) wy + | N1 wx, N13 wy => f13 (extend12 w0 wx) wy + | N1 wx, Nn n wy => fn n (extend n w13 (extend13 w0 wx)) wy | N2 wx, N0 wy => f2 wx (extend1 w0 (WW w_0 wy)) | N2 wx, N1 wy => f2 wx (extend1 w0 wy) @@ -3588,7 +4001,8 @@ Definition pheight p := Peano.pred (nat_of_P (get_height w0_op.(znz_digits) (ple | N2 wx, N10 wy => f10 (extend8 w1 wx) wy | N2 wx, N11 wy => f11 (extend9 w1 wx) wy | N2 wx, N12 wy => f12 (extend10 w1 wx) wy - | N2 wx, Nn n wy => fn n (extend n w12 (extend11 w1 wx)) wy + | N2 wx, N13 wy => f13 (extend11 w1 wx) wy + | N2 wx, Nn n wy => fn n (extend n w13 (extend12 w1 wx)) wy | N3 wx, N0 wy => f3 wx (extend2 w0 (WW w_0 wy)) | N3 wx, N1 wy => f3 wx (extend2 w0 wy) @@ -3603,7 +4017,8 @@ Definition pheight p := Peano.pred (nat_of_P (get_height w0_op.(znz_digits) (ple | N3 wx, N10 wy => f10 (extend7 w2 wx) wy | N3 wx, N11 wy => f11 (extend8 w2 wx) wy | N3 wx, N12 wy => f12 (extend9 w2 wx) wy - | N3 wx, Nn n wy => fn n (extend n w12 (extend10 w2 wx)) wy + | N3 wx, N13 wy => f13 (extend10 w2 wx) wy + | N3 wx, Nn n wy => fn n (extend n w13 (extend11 w2 wx)) wy | N4 wx, N0 wy => f4 wx (extend3 w0 (WW w_0 wy)) | N4 wx, N1 wy => f4 wx (extend3 w0 wy) @@ -3618,7 +4033,8 @@ Definition pheight p := Peano.pred (nat_of_P (get_height w0_op.(znz_digits) (ple | N4 wx, N10 wy => f10 (extend6 w3 wx) wy | N4 wx, N11 wy => f11 (extend7 w3 wx) wy | N4 wx, N12 wy => f12 (extend8 w3 wx) wy - | N4 wx, Nn n wy => fn n (extend n w12 (extend9 w3 wx)) wy + | N4 wx, N13 wy => f13 (extend9 w3 wx) wy + | N4 wx, Nn n wy => fn n (extend n w13 (extend10 w3 wx)) wy | N5 wx, N0 wy => f5 wx (extend4 w0 (WW w_0 wy)) | N5 wx, N1 wy => f5 wx (extend4 w0 wy) @@ -3633,7 +4049,8 @@ Definition pheight p := Peano.pred (nat_of_P (get_height w0_op.(znz_digits) (ple | N5 wx, N10 wy => f10 (extend5 w4 wx) wy | N5 wx, N11 wy => f11 (extend6 w4 wx) wy | N5 wx, N12 wy => f12 (extend7 w4 wx) wy - | N5 wx, Nn n wy => fn n (extend n w12 (extend8 w4 wx)) wy + | N5 wx, N13 wy => f13 (extend8 w4 wx) wy + | N5 wx, Nn n wy => fn n (extend n w13 (extend9 w4 wx)) wy | N6 wx, N0 wy => f6 wx (extend5 w0 (WW w_0 wy)) | N6 wx, N1 wy => f6 wx (extend5 w0 wy) @@ -3648,7 +4065,8 @@ Definition pheight p := Peano.pred (nat_of_P (get_height w0_op.(znz_digits) (ple | N6 wx, N10 wy => f10 (extend4 w5 wx) wy | N6 wx, N11 wy => f11 (extend5 w5 wx) wy | N6 wx, N12 wy => f12 (extend6 w5 wx) wy - | N6 wx, Nn n wy => fn n (extend n w12 (extend7 w5 wx)) wy + | N6 wx, N13 wy => f13 (extend7 w5 wx) wy + | N6 wx, Nn n wy => fn n (extend n w13 (extend8 w5 wx)) wy | N7 wx, N0 wy => f7 wx (extend6 w0 (WW w_0 wy)) | N7 wx, N1 wy => f7 wx (extend6 w0 wy) @@ -3663,7 +4081,8 @@ Definition pheight p := Peano.pred (nat_of_P (get_height w0_op.(znz_digits) (ple | N7 wx, N10 wy => f10 (extend3 w6 wx) wy | N7 wx, N11 wy => f11 (extend4 w6 wx) wy | N7 wx, N12 wy => f12 (extend5 w6 wx) wy - | N7 wx, Nn n wy => fn n (extend n w12 (extend6 w6 wx)) wy + | N7 wx, N13 wy => f13 (extend6 w6 wx) wy + | N7 wx, Nn n wy => fn n (extend n w13 (extend7 w6 wx)) wy | N8 wx, N0 wy => f8 wx (extend7 w0 (WW w_0 wy)) | N8 wx, N1 wy => f8 wx (extend7 w0 wy) @@ -3678,7 +4097,8 @@ Definition pheight p := Peano.pred (nat_of_P (get_height w0_op.(znz_digits) (ple | N8 wx, N10 wy => f10 (extend2 w7 wx) wy | N8 wx, N11 wy => f11 (extend3 w7 wx) wy | N8 wx, N12 wy => f12 (extend4 w7 wx) wy - | N8 wx, Nn n wy => fn n (extend n w12 (extend5 w7 wx)) wy + | N8 wx, N13 wy => f13 (extend5 w7 wx) wy + | N8 wx, Nn n wy => fn n (extend n w13 (extend6 w7 wx)) wy | N9 wx, N0 wy => f9 wx (extend8 w0 (WW w_0 wy)) | N9 wx, N1 wy => f9 wx (extend8 w0 wy) @@ -3693,7 +4113,8 @@ Definition pheight p := Peano.pred (nat_of_P (get_height w0_op.(znz_digits) (ple | N9 wx, N10 wy => f10 (extend1 w8 wx) wy | N9 wx, N11 wy => f11 (extend2 w8 wx) wy | N9 wx, N12 wy => f12 (extend3 w8 wx) wy - | N9 wx, Nn n wy => fn n (extend n w12 (extend4 w8 wx)) wy + | N9 wx, N13 wy => f13 (extend4 w8 wx) wy + | N9 wx, Nn n wy => fn n (extend n w13 (extend5 w8 wx)) wy | N10 wx, N0 wy => f10 wx (extend9 w0 (WW w_0 wy)) | N10 wx, N1 wy => f10 wx (extend9 w0 wy) @@ -3708,7 +4129,8 @@ Definition pheight p := Peano.pred (nat_of_P (get_height w0_op.(znz_digits) (ple | N10 wx, N10 wy => f10 wx wy | N10 wx, N11 wy => f11 (extend1 w9 wx) wy | N10 wx, N12 wy => f12 (extend2 w9 wx) wy - | N10 wx, Nn n wy => fn n (extend n w12 (extend3 w9 wx)) wy + | N10 wx, N13 wy => f13 (extend3 w9 wx) wy + | N10 wx, Nn n wy => fn n (extend n w13 (extend4 w9 wx)) wy | N11 wx, N0 wy => f11 wx (extend10 w0 (WW w_0 wy)) | N11 wx, N1 wy => f11 wx (extend10 w0 wy) @@ -3723,7 +4145,8 @@ Definition pheight p := Peano.pred (nat_of_P (get_height w0_op.(znz_digits) (ple | N11 wx, N10 wy => f11 wx (extend1 w9 wy) | N11 wx, N11 wy => f11 wx wy | N11 wx, N12 wy => f12 (extend1 w10 wx) wy - | N11 wx, Nn n wy => fn n (extend n w12 (extend2 w10 wx)) wy + | N11 wx, N13 wy => f13 (extend2 w10 wx) wy + | N11 wx, Nn n wy => fn n (extend n w13 (extend3 w10 wx)) wy | N12 wx, N0 wy => f12 wx (extend11 w0 (WW w_0 wy)) | N12 wx, N1 wy => f12 wx (extend11 w0 wy) @@ -3738,21 +4161,39 @@ Definition pheight p := Peano.pred (nat_of_P (get_height w0_op.(znz_digits) (ple | N12 wx, N10 wy => f12 wx (extend2 w9 wy) | N12 wx, N11 wy => f12 wx (extend1 w10 wy) | N12 wx, N12 wy => f12 wx wy - | N12 wx, Nn n wy => fn n (extend n w12 (extend1 w11 wx)) wy + | N12 wx, N13 wy => f13 (extend1 w11 wx) wy + | N12 wx, Nn n wy => fn n (extend n w13 (extend2 w11 wx)) wy + | N13 wx, N0 wy => + f13 wx (extend12 w0 (WW w_0 wy)) + | N13 wx, N1 wy => f13 wx (extend12 w0 wy) + | N13 wx, N2 wy => f13 wx (extend11 w1 wy) + | N13 wx, N3 wy => f13 wx (extend10 w2 wy) + | N13 wx, N4 wy => f13 wx (extend9 w3 wy) + | N13 wx, N5 wy => f13 wx (extend8 w4 wy) + | N13 wx, N6 wy => f13 wx (extend7 w5 wy) + | N13 wx, N7 wy => f13 wx (extend6 w6 wy) + | N13 wx, N8 wy => f13 wx (extend5 w7 wy) + | N13 wx, N9 wy => f13 wx (extend4 w8 wy) + | N13 wx, N10 wy => f13 wx (extend3 w9 wy) + | N13 wx, N11 wy => f13 wx (extend2 w10 wy) + | N13 wx, N12 wy => f13 wx (extend1 w11 wy) + | N13 wx, N13 wy => f13 wx wy + | N13 wx, Nn n wy => fn n (extend n w13 (extend1 w12 wx)) wy | Nn n wx, N0 wy => - fn n wx (extend n w12 (extend12 w0 (WW w_0 wy))) - | Nn n wx, N1 wy => fn n wx (extend n w12 (extend12 w0 wy)) - | Nn n wx, N2 wy => fn n wx (extend n w12 (extend11 w1 wy)) - | Nn n wx, N3 wy => fn n wx (extend n w12 (extend10 w2 wy)) - | Nn n wx, N4 wy => fn n wx (extend n w12 (extend9 w3 wy)) - | Nn n wx, N5 wy => fn n wx (extend n w12 (extend8 w4 wy)) - | Nn n wx, N6 wy => fn n wx (extend n w12 (extend7 w5 wy)) - | Nn n wx, N7 wy => fn n wx (extend n w12 (extend6 w6 wy)) - | Nn n wx, N8 wy => fn n wx (extend n w12 (extend5 w7 wy)) - | Nn n wx, N9 wy => fn n wx (extend n w12 (extend4 w8 wy)) - | Nn n wx, N10 wy => fn n wx (extend n w12 (extend3 w9 wy)) - | Nn n wx, N11 wy => fn n wx (extend n w12 (extend2 w10 wy)) - | Nn n wx, N12 wy => fn n wx (extend n w12 (extend1 w11 wy)) + fn n wx (extend n w13 (extend13 w0 (WW w_0 wy))) + | Nn n wx, N1 wy => fn n wx (extend n w13 (extend13 w0 wy)) + | Nn n wx, N2 wy => fn n wx (extend n w13 (extend12 w1 wy)) + | Nn n wx, N3 wy => fn n wx (extend n w13 (extend11 w2 wy)) + | Nn n wx, N4 wy => fn n wx (extend n w13 (extend10 w3 wy)) + | Nn n wx, N5 wy => fn n wx (extend n w13 (extend9 w4 wy)) + | Nn n wx, N6 wy => fn n wx (extend n w13 (extend8 w5 wy)) + | Nn n wx, N7 wy => fn n wx (extend n w13 (extend7 w6 wy)) + | Nn n wx, N8 wy => fn n wx (extend n w13 (extend6 w7 wy)) + | Nn n wx, N9 wy => fn n wx (extend n w13 (extend5 w8 wy)) + | Nn n wx, N10 wy => fn n wx (extend n w13 (extend4 w9 wy)) + | Nn n wx, N11 wy => fn n wx (extend n w13 (extend3 w10 wy)) + | Nn n wx, N12 wy => fn n wx (extend n w13 (extend2 w11 wy)) + | Nn n wx, N13 wy => fn n wx (extend n w13 (extend1 w12 wy)) | Nn n wx, Nn m wy => let mn := Max.max n m in let d := diff n m in @@ -3774,6 +4215,7 @@ Definition pheight p := Peano.pred (nat_of_P (get_height w0_op.(znz_digits) (ple Definition shiftr10 n x := w10_op.(znz_add_mul_div) (w10_op.(znz_sub) w10_op.(znz_zdigits) n) w10_op.(znz_0) x. Definition shiftr11 n x := w11_op.(znz_add_mul_div) (w11_op.(znz_sub) w11_op.(znz_zdigits) n) w11_op.(znz_0) x. Definition shiftr12 n x := w12_op.(znz_add_mul_div) (w12_op.(znz_sub) w12_op.(znz_zdigits) n) w12_op.(znz_0) x. + Definition shiftr13 n x := w13_op.(znz_add_mul_div) (w13_op.(znz_sub) w13_op.(znz_zdigits) n) w13_op.(znz_0) x. Definition shiftrn n p x := (make_op n).(znz_add_mul_div) ((make_op n).(znz_sub) (make_op n).(znz_zdigits) p) (make_op n).(znz_0) x. Definition shiftr := @@ -3791,6 +4233,7 @@ Definition pheight p := Peano.pred (nat_of_P (get_height w0_op.(znz_digits) (ple (fun n x => reduce_10 (shiftr10 n x)) (fun n x => reduce_11 (shiftr11 n x)) (fun n x => reduce_12 (shiftr12 n x)) + (fun n x => reduce_13 (shiftr13 n x)) (fun n p x => reduce_n n (shiftrn n p x)). Definition safe_shiftr n x := @@ -3812,6 +4255,7 @@ Definition pheight p := Peano.pred (nat_of_P (get_height w0_op.(znz_digits) (ple Definition shiftl10 n x := w10_op.(znz_add_mul_div) n x w10_op.(znz_0). Definition shiftl11 n x := w11_op.(znz_add_mul_div) n x w11_op.(znz_0). Definition shiftl12 n x := w12_op.(znz_add_mul_div) n x w12_op.(znz_0). + Definition shiftl13 n x := w13_op.(znz_add_mul_div) n x w13_op.(znz_0). Definition shiftln n p x := (make_op n).(znz_add_mul_div) p x (make_op n).(znz_0). Definition shiftl := Eval lazy beta delta [level] in @@ -3828,6 +4272,7 @@ Definition pheight p := Peano.pred (nat_of_P (get_height w0_op.(znz_digits) (ple (fun n x => reduce_10 (shiftl10 n x)) (fun n x => reduce_11 (shiftl11 n x)) (fun n x => reduce_12 (shiftl12 n x)) + (fun n x => reduce_13 (shiftl13 n x)) (fun n p x => reduce_n n (shiftln n p x)). @@ -3844,18 +4289,19 @@ Definition pheight p := Peano.pred (nat_of_P (get_height w0_op.(znz_digits) (ple | N9 w=> N10 (extend1 _ w) | N10 w=> N11 (extend1 _ w) | N11 w=> N12 (extend1 _ w) - | N12 w=> Nn 0 (extend1 _ w) + | N12 w=> N13 (extend1 _ w) + | N13 w=> Nn 0 (extend1 _ w) | Nn n w=> Nn (S n) (extend1 _ w) end. - Definition safe_shiftl_aux_body cont n x := - match compare n (head0 x) with - Gt => cont n (double_size x) - | _ => shiftl n x - end. + Definition safe_shiftl_aux_body cont n x := + match compare n (head0 x) with + Gt => cont n (double_size x) + | _ => shiftl n x + end. Fixpoint safe_shiftl_aux p cont n x {struct p} := - safe_shiftl_aux_body + safe_shiftl_aux_body (fun n x => match p with | xH => cont n x | xO p => safe_shiftl_aux p (safe_shiftl_aux p cont) n x @@ -3880,8 +4326,35 @@ Definition pheight p := Peano.pred (nat_of_P (get_height w0_op.(znz_digits) (ple | N10 wx => w10_op.(znz_is_even) wx | N11 wx => w11_op.(znz_is_even) wx | N12 wx => w12_op.(znz_is_even) wx + | N13 wx => w13_op.(znz_is_even) wx | Nn n wx => (make_op n).(znz_is_even) wx end. +(* Proof section *) + + Open Scope Z_scope. + Notation "[ x ]" := (to_Z x). + + Theorem succ_spec: forall n, [succ n] = [n] + 1. + Admitted. + + Theorem spec_add: forall x y, [add x y] = [x] + [y]. + Admitted. + + Theorem spec_sub: forall x y, [y] <= [x] -> [sub x y] = [x] - [y]. + Admitted. + + Theorem spec_sub0: forall x y, [x] < [y] -> [sub x y] = 0. + Admitted. + + Theorem spec_compare: forall x y, + match compare x y with + Eq => [x] = [y] + | Lt => [x] < [y] + | Gt => [x] > [y] + end. + Proof. + Admitted. + End Make. diff --git a/theories/Ints/num/Nbasic.v b/theories/Ints/num/Nbasic.v index 846aabe8ca..c96425cb5d 100644 --- a/theories/Ints/num/Nbasic.v +++ b/theories/Ints/num/Nbasic.v @@ -3,6 +3,7 @@ Require Import ZAux. Require Import ZDivModAux. Require Import Basic_type. Require Import Max. +Require Import GenBase. (* To compute the necessary height *) @@ -275,6 +276,57 @@ Section CompareRec. end end. + Variable wm_base: positive. + Variable wm_to_Z: wm -> Z. + Variable w_to_Z: w -> Z. + Variable w_to_Z_0: w_to_Z w_0 = 0. + Variable spec_compare0_m: forall x, + match compare0_m x with + Eq => w_to_Z w_0 = wm_to_Z x + | Lt => w_to_Z w_0 < wm_to_Z x + | Gt => w_to_Z w_0 > wm_to_Z x + end. + Variable wm_to_Z_pos: forall x, 0 <= wm_to_Z x < base wm_base. + + Let gen_to_Z := gen_to_Z wm_base wm_to_Z. + Let gen_wB := gen_wB wm_base. + + Lemma base_xO: forall n, base (xO n) = (base n)^2. + Proof. + intros n1; unfold base. + rewrite (Zpos_xO n1); rewrite Zmult_comm; rewrite ZAux.Zpower_mult; auto with zarith. + Qed. + + Let gen_to_Z_pos: forall n x, 0 <= gen_to_Z n x < gen_wB n := + (spec_gen_to_Z wm_base wm_to_Z wm_to_Z_pos). + + + Lemma spec_compare0_mn: forall n x, + match compare0_mn n x with + Eq => 0 = gen_to_Z n x + | Lt => 0 < gen_to_Z n x + | Gt => 0 > gen_to_Z n x + end. + Proof. + intros n; elim n; clear n; auto. + intros x; generalize (spec_compare0_m x); rewrite w_to_Z_0; auto. + intros n Hrec x; case x; unfold compare0_mn; fold compare0_mn; auto. + intros xh xl. + generalize (Hrec xh); case compare0_mn; auto. + generalize (Hrec xl); case compare0_mn; auto. + simpl gen_to_Z; intros H1 H2; rewrite H1; rewrite <- H2; auto. + simpl gen_to_Z; intros H1 H2; rewrite <- H2; auto. + case (gen_to_Z_pos n xl); auto with zarith. + intros H1; simpl gen_to_Z. + set (u := GenBase.gen_wB wm_base n). + case (gen_to_Z_pos n xl); intros H2 H3. + assert (0 < u); auto with zarith. + unfold u, GenBase.gen_wB, base; auto with zarith. + change 0 with (0 + 0); apply Zplus_lt_le_compat; auto with zarith. + apply Zmult_lt_0_compat; auto with zarith. + case (gen_to_Z_pos n xh); auto with zarith. + Qed. + Fixpoint compare_mn_1 (n:nat) : word wm n -> w -> comparison := match n return word wm n -> w -> comparison with | O => compare_m @@ -289,7 +341,124 @@ Section CompareRec. end end. + Variable spec_compare: forall x y, + match compare x y with + Eq => w_to_Z x = w_to_Z y + | Lt => w_to_Z x < w_to_Z y + | Gt => w_to_Z x > w_to_Z y + end. + Variable spec_compare_m: forall x y, + match compare_m x y with + Eq => wm_to_Z x = w_to_Z y + | Lt => wm_to_Z x < w_to_Z y + | Gt => wm_to_Z x > w_to_Z y + end. + Variable wm_base_lt: forall x, + 0 <= w_to_Z x < base (wm_base). + + Let gen_wB_lt: forall n x, + 0 <= w_to_Z x < (gen_wB n). + Proof. + intros n x; elim n; simpl; auto; clear n. + intros n (H0, H); split; auto. + apply Zlt_le_trans with (1:= H). + unfold gen_wB, GenBase.gen_wB; simpl. + rewrite base_xO. + set (u := base (gen_digits wm_base n)). + assert (0 < u). + unfold u, base; auto with zarith. + replace (u^2) with (u * u); simpl; auto with zarith. + apply Zle_trans with (1 * u); auto with zarith. + unfold Zpower_pos; simpl; ring. + Qed. + + + Lemma spec_compare_mn_1: forall n x y, + match compare_mn_1 n x y with + Eq => gen_to_Z n x = w_to_Z y + | Lt => gen_to_Z n x < w_to_Z y + | Gt => gen_to_Z n x > w_to_Z y + end. + Proof. + intros n; elim n; simpl; auto; clear n. + intros n Hrec x; case x; clear x; auto. + intros y; generalize (spec_compare w_0 y); rewrite w_to_Z_0; case compare; auto. + intros xh xl y; simpl; generalize (spec_compare0_mn n xh); case compare0_mn; intros H1b. + rewrite <- H1b; rewrite Zmult_0_l; rewrite Zplus_0_l; auto. + apply Hrec. + apply Zlt_gt. + case (gen_wB_lt n y); intros _ H0. + apply Zlt_le_trans with (1:= H0). + fold gen_wB. + case (gen_to_Z_pos n xl); intros H1 H2. + apply Zle_trans with (gen_to_Z n xh * gen_wB n); auto with zarith. + apply Zle_trans with (1 * gen_wB n); auto with zarith. + case (gen_to_Z_pos n xh); auto with zarith. + Qed. + End CompareRec. +Section AddS. + + Variable w wm: Set. + Variable incr : wm -> carry wm. + Variable addr : w -> wm -> carry wm. + Variable injr : w -> zn2z wm. + Variable w_0 u: w. + Fixpoint injs (n:nat): word w (S n) := + match n return (word w (S n)) with + O => WW w_0 u + | S n1 => (WW W0 (injs n1)) + end. + + Definition adds x y := + match y with + W0 => C0 (injr x) + | WW hy ly => match addr x ly with + C0 z => C0 (WW hy z) + | C1 z => match incr hy with + C0 z1 => C0 (WW z1 z) + | C1 z1 => C1 (WW z1 z) + end + end + end. + +End AddS. + + + Lemma spec_opp: forall u x y, + match u with + | Eq => y = x + | Lt => y < x + | Gt => y > x + end -> + match opp_compare u with + | Eq => x = y + | Lt => x < y + | Gt => x > y + end. + Proof. + intros u x y; case u; simpl; auto with zarith. + Qed. + + Fixpoint length_pos x := + match x with xH => O | xO x1 => S (length_pos x1) | xI x1 => S (length_pos x1) end. + + Theorem length_pos_lt: forall x y, + (length_pos x < length_pos y)%nat -> Zpos x < Zpos y. + Proof. + intros x; elim x; clear x; [intros x1 Hrec | intros x1 Hrec | idtac]; + intros y; case y; clear y; intros y1 H || intros H; simpl length_pos; + try (rewrite (Zpos_xI x1) || rewrite (Zpos_xO x1)); + try (rewrite (Zpos_xI y1) || rewrite (Zpos_xO y1)); + try (inversion H; fail); + try (assert (Zpos x1 < Zpos y1); [apply Hrec; apply lt_S_n | idtac]; auto with zarith); + assert (0 < Zpos y1); auto with zarith; red; auto. + Qed. + + Theorem cancel_app: forall A B (f g: A -> B) x, f = g -> f x = g x. + Proof. + intros A B f g x H; rewrite H; auto. + Qed. diff --git a/theories/Ints/num/Zn2Z.v b/theories/Ints/num/Zn2Z.v index 45bfc1ac2c..2925b202dd 100644 --- a/theories/Ints/num/Zn2Z.v +++ b/theories/Ints/num/Zn2Z.v @@ -861,7 +861,37 @@ refine rewrite (spec_zdigits op_spec). rewrite <- Zpos_xO; exact spec_ww_digits. Qed. +End Zn2Z. + +Section MulAdd. + Variable w: Set. + Variable op: znz_op w. + Variable sop: znz_spec op. + + Definition mul_add:= w_mul_add (znz_0 op) (znz_succ op) (znz_add_c op) (znz_mul_c op). + + Notation "[| x |]" := (znz_to_Z op x) (at level 0, x at level 99). + + Notation "[|| x ||]" := + (zn2z_to_Z (base (znz_digits op)) (znz_to_Z op) x) (at level 0, x at level 99). + + + Lemma spec_mul_add: forall x y z, + let (zh, zl) := mul_add x y z in + [||WW zh zl||] = [|x|] * [|y|] + [|z|]. + Proof. + intros x y z. + refine (spec_w_mul_add _ _ _ _ _ _ _ _ _ _ _ _ x y z); auto. + exact (spec_0 sop). + exact (spec_to_Z sop). + exact (spec_succ sop). + exact (spec_add_c sop). + exact (spec_mul_c sop). + Qed. + +End MulAdd. + + -End Zn2Z. diff --git a/theories/Ints/num/genN.ml b/theories/Ints/num/genN.ml index 5295bcc1c9..b2bbf0a199 100644 --- a/theories/Ints/num/genN.ml +++ b/theories/Ints/num/genN.ml @@ -1,11 +1,21 @@ open Format -let size = 12 +let size = 13 let sizeaux = 1 let t = "t" let c = "N" let gen_proof = false +let gen_proof1 = false +let gen_proof2 = false +let gen_proof3 = false +let gen_proof4 = false +let gen_proof5 = false +let gen_proof6 = false +let gen_proof7 = false +let gen_proof8 = false +let gen_proof9 = false + (******* Start Printing ********) let basename = "N" @@ -941,14 +951,14 @@ let print_Make () = (* Safe shiftl *) - fprintf fmt " Definition safe_shiftl_aux_body cont n x :=\n"; - fprintf fmt " match compare n (head0 x) with\n"; - fprintf fmt " Gt => cont n (double_size x)\n"; - fprintf fmt " | _ => shiftl n x\n"; - fprintf fmt " end.\n"; + fprintf fmt " Definition safe_shiftl_aux_body cont n x :=\n"; + fprintf fmt " match compare n (head0 x) with\n"; + fprintf fmt " Gt => cont n (double_size x)\n"; + fprintf fmt " | _ => shiftl n x\n"; + fprintf fmt " end.\n"; fprintf fmt "\n"; fprintf fmt " Fixpoint safe_shiftl_aux p cont n x {struct p} :=\n"; - fprintf fmt " safe_shiftl_aux_body \n"; + fprintf fmt " safe_shiftl_aux_body \n"; fprintf fmt " (fun n x => match p with\n"; fprintf fmt " | xH => cont n x\n"; fprintf fmt " | xO p => safe_shiftl_aux p (safe_shiftl_aux p cont) n x\n"; @@ -969,11 +979,12 @@ let print_Make () = fprintf fmt " end.\n"; fprintf fmt "\n"; - if gen_proof then - begin + fprintf fmt "(* Proof section *)\n"; fprintf fmt "\n"; + if gen_proof1 then + begin fprintf fmt " Let w0_spec: znz_spec w0_op := W0.w_spec.\n"; for i = 1 to 3 do fprintf fmt " Let w%i_spec: znz_spec w%i_op := mk_znz2_spec w%i_spec.\n" i i (i-1) @@ -1008,11 +1019,14 @@ let print_Make () = fprintf fmt " exact (mk_znz2_karatsuba_spec Hrec).\n"; fprintf fmt " Qed.\n"; fprintf fmt " \n"; + end; fprintf fmt " Open Scope Z_scope.\n"; fprintf fmt " Notation \"[ x ]\" := (to_Z x).\n"; fprintf fmt " \n"; + if gen_proof2 then + begin for i = 1 to size + 1 do fprintf fmt " Let znz_to_Z_%i: forall x y,\n" i; fprintf fmt " znz_to_Z w%i_op (WW x y) = \n" i; @@ -1030,8 +1044,11 @@ let print_Make () = fprintf fmt " intros n x y; rewrite make_op_S; auto.\n"; fprintf fmt " Qed. \n"; fprintf fmt "\n"; + end; fprintf fmt " Theorem succ_spec: forall n, [succ n] = [n] + 1.\n"; + if gen_proof3 then + begin fprintf fmt " Proof.\n"; fprintf fmt " intros n; case n; unfold succ, to_Z.\n"; for i = 0 to size do @@ -1050,410 +1067,688 @@ let print_Make () = fprintf fmt " apply f_equal2 with (f := Zplus); auto;\n"; fprintf fmt " apply f_equal2 with (f := Zmult); auto;\n"; fprintf fmt " exact (spec_1 (wn_spec k))).\n"; - fprintf fmt " Qed.\n "; + fprintf fmt " Qed.\n "; + end else + fprintf fmt " Admitted.\n"; fprintf fmt "\n"; + if gen_proof4 then + begin for i = 0 to size do - fprintf fmt " Let spec_w%i_add: forall x y, [w%i_add x y] = [%s%i x] + [%s%i y].\n" i i c i c i; - fprintf fmt " Proof.\n"; - fprintf fmt " intros n m; unfold to_Z, w%i_add, w%i_add_c.\n" i i; - fprintf fmt " generalize (spec_add_c w%i_spec n m); case znz_add_c; auto.\n" i; - fprintf fmt " intros ww H; rewrite <- H.\n"; - fprintf fmt " rewrite znz_to_Z_%i; unfold interp_carry;\n" (i + 1); - fprintf fmt " apply f_equal2 with (f := Zplus); auto;\n"; - fprintf fmt " apply f_equal2 with (f := Zmult); auto;\n"; - fprintf fmt " exact (spec_1 w%i_spec).\n" i; - fprintf fmt " Qed.\n"; - fprintf fmt " Hint Rewrite spec_w%i_add: addr.\n" i; + fprintf fmt " Let spec_w%i_add: forall x y, [w%i_add x y] = [%s%i x] + [%s%i y].\n" i i c i c i; + fprintf fmt " Proof.\n"; + fprintf fmt " intros n m; unfold to_Z, w%i_add, w%i_add_c.\n" i i; + fprintf fmt " generalize (spec_add_c w%i_spec n m); case znz_add_c; auto.\n" i; + fprintf fmt " intros ww H; rewrite <- H.\n"; + fprintf fmt " rewrite znz_to_Z_%i; unfold interp_carry;\n" (i + 1); + fprintf fmt " apply f_equal2 with (f := Zplus); auto;\n"; + fprintf fmt " apply f_equal2 with (f := Zmult); auto;\n"; + fprintf fmt " exact (spec_1 w%i_spec).\n" i; + fprintf fmt " Qed.\n"; + fprintf fmt " Hint Rewrite spec_w%i_add: addr.\n" i; fprintf fmt "\n"; done; - fprintf fmt " Let spec_wn_add: forall n x y, [addn n x y] = [%sn n x] + [%sn n y].\n" c c; - fprintf fmt " Proof.\n"; - fprintf fmt " intros k n m; unfold to_Z, addn.\n"; - fprintf fmt " generalize (spec_add_c (wn_spec k) n m); case znz_add_c; auto.\n"; - fprintf fmt " intros ww H; rewrite <- H.\n"; - fprintf fmt " rewrite (znz_to_Z_n k); unfold interp_carry;\n"; - fprintf fmt " apply f_equal2 with (f := Zplus); auto;\n"; - fprintf fmt " apply f_equal2 with (f := Zmult); auto;\n"; - fprintf fmt " exact (spec_1 (wn_spec k)).\n"; - fprintf fmt " Qed.\n"; - fprintf fmt " Hint Rewrite spec_wn_add: addr.\n"; + fprintf fmt " Let spec_wn_add: forall n x y, [addn n x y] = [%sn n x] + [%sn n y].\n" c c; + fprintf fmt " Proof.\n"; + fprintf fmt " intros k n m; unfold to_Z, addn.\n"; + fprintf fmt " generalize (spec_add_c (wn_spec k) n m); case znz_add_c; auto.\n"; + fprintf fmt " intros ww H; rewrite <- H.\n"; + fprintf fmt " rewrite (znz_to_Z_n k); unfold interp_carry;\n"; + fprintf fmt " apply f_equal2 with (f := Zplus); auto;\n"; + fprintf fmt " apply f_equal2 with (f := Zmult); auto;\n"; + fprintf fmt " exact (spec_1 (wn_spec k)).\n"; + fprintf fmt " Qed.\n"; + fprintf fmt " Hint Rewrite spec_wn_add: addr.\n"; fprintf fmt "\n"; for i = 0 to size do - fprintf fmt " Let spec_w%i_eq0: forall x, if w%i_eq0 x then [%s%i x] = 0 else True.\n" i i c i; - fprintf fmt " Proof.\n"; - fprintf fmt " intros x; unfold w%i_eq0.\n" i; - fprintf fmt " generalize (spec_eq0 w%i_spec x); case znz_eq0; auto.\n" i; - fprintf fmt " Qed.\n"; + fprintf fmt " Let spec_w%i_eq0: forall x, if w%i_eq0 x then [%s%i x] = 0 else True.\n" i i c i; + fprintf fmt " Proof.\n"; + fprintf fmt " intros x; unfold w%i_eq0.\n" i; + fprintf fmt " generalize (spec_eq0 w%i_spec x); case znz_eq0; auto.\n" i; + fprintf fmt " Qed.\n"; fprintf fmt "\n"; done; - fprintf fmt " Let spec_extendn_0: forall n wx, [%sn n (extend n _ wx)] = [%sn 0 wx].\n" c c; - fprintf fmt " intros n; elim n; auto.\n"; - fprintf fmt " intros n1 Hrec wx; simpl extend; rewrite <- Hrec; auto.\n"; - fprintf fmt " unfold to_Z.\n"; - fprintf fmt " case n1; auto; intros n2; repeat rewrite make_op_S; auto.\n"; - fprintf fmt " Qed.\n"; - fprintf fmt " Hint Rewrite spec_extendn_0: extr.\n"; + fprintf fmt " Let spec_extendn_0: forall n wx, [%sn n (extend n _ wx)] = [%sn 0 wx].\n" c c; + fprintf fmt " intros n; elim n; auto.\n"; + fprintf fmt " intros n1 Hrec wx; simpl extend; rewrite <- Hrec; auto.\n"; + fprintf fmt " unfold to_Z.\n"; + fprintf fmt " case n1; auto; intros n2; repeat rewrite make_op_S; auto.\n"; + fprintf fmt " Qed.\n"; + fprintf fmt " Hint Rewrite spec_extendn_0: extr.\n"; fprintf fmt "\n"; - fprintf fmt " Let spec_extendn0_0: forall n wx, [%sn (S n) (WW W0 wx)] = [%sn n wx].\n" c c; - fprintf fmt " Proof.\n"; - fprintf fmt " intros n x; unfold to_Z.\n"; - fprintf fmt " rewrite znz_to_Z_n.\n"; - fprintf fmt " rewrite <- (Zplus_0_l (znz_to_Z (make_op n) x)).\n"; - fprintf fmt " apply (f_equal2 Zplus); auto.\n"; - fprintf fmt " case n; auto.\n"; - fprintf fmt " intros n1; rewrite make_op_S; auto.\n"; - fprintf fmt " Qed.\n"; - fprintf fmt " Hint Rewrite spec_extendn_0: extr.\n"; + fprintf fmt " Let spec_extendn0_0: forall n wx, [%sn (S n) (WW W0 wx)] = [%sn n wx].\n" c c; + fprintf fmt " Proof.\n"; + fprintf fmt " intros n x; unfold to_Z.\n"; + fprintf fmt " rewrite znz_to_Z_n.\n"; + fprintf fmt " rewrite <- (Zplus_0_l (znz_to_Z (make_op n) x)).\n"; + fprintf fmt " apply (f_equal2 Zplus); auto.\n"; + fprintf fmt " case n; auto.\n"; + fprintf fmt " intros n1; rewrite make_op_S; auto.\n"; + fprintf fmt " Qed.\n"; + fprintf fmt " Hint Rewrite spec_extendn_0: extr.\n"; fprintf fmt "\n"; - fprintf fmt " Let spec_extend_tr: forall m n (w: word _ (S n)),\n"; - fprintf fmt " [%sn (m + n) (extend_tr w m)] = [%sn n w].\n" c c; - fprintf fmt " Proof.\n"; - fprintf fmt " induction m; auto.\n"; - fprintf fmt " intros n x; simpl extend_tr.\n"; - fprintf fmt " simpl plus; rewrite spec_extendn0_0; auto.\n"; - fprintf fmt " Qed.\n"; - fprintf fmt " Hint Rewrite spec_extend_tr: extr.\n"; + fprintf fmt " Let spec_extend_tr: forall m n (w: word _ (S n)),\n"; + fprintf fmt " [%sn (m + n) (extend_tr w m)] = [%sn n w].\n" c c; + fprintf fmt " Proof.\n"; + fprintf fmt " induction m; auto.\n"; + fprintf fmt " intros n x; simpl extend_tr.\n"; + fprintf fmt " simpl plus; rewrite spec_extendn0_0; auto.\n"; + fprintf fmt " Qed.\n"; + fprintf fmt " Hint Rewrite spec_extend_tr: extr.\n"; fprintf fmt "\n"; - fprintf fmt " Let spec_cast_l: forall n m x1,\n"; - fprintf fmt " [%sn (Max.max n m)\n" c; - fprintf fmt " (castm (diff_r n m) (extend_tr x1 (snd (diff n m))))] =\n"; - fprintf fmt " [%sn n x1].\n" c; - fprintf fmt " Proof.\n"; - fprintf fmt " intros n m x1; case (diff_r n m); simpl castm.\n"; - fprintf fmt " rewrite spec_extend_tr; auto.\n"; - fprintf fmt " Qed.\n"; - fprintf fmt " Hint Rewrite spec_cast_l: extr.\n"; + fprintf fmt " Let spec_cast_l: forall n m x1,\n"; + fprintf fmt " [%sn (Max.max n m)\n" c; + fprintf fmt " (castm (diff_r n m) (extend_tr x1 (snd (diff n m))))] =\n"; + fprintf fmt " [%sn n x1].\n" c; + fprintf fmt " Proof.\n"; + fprintf fmt " intros n m x1; case (diff_r n m); simpl castm.\n"; + fprintf fmt " rewrite spec_extend_tr; auto.\n"; + fprintf fmt " Qed.\n"; + fprintf fmt " Hint Rewrite spec_cast_l: extr.\n"; fprintf fmt "\n"; - fprintf fmt " Let spec_cast_r: forall n m x1,\n"; - fprintf fmt " [%sn (Max.max n m)\n" c; - fprintf fmt " (castm (diff_l n m) (extend_tr x1 (fst (diff n m))))] =\n"; - fprintf fmt " [%sn m x1].\n" c; - fprintf fmt " Proof.\n"; - fprintf fmt " intros n m x1; case (diff_l n m); simpl castm.\n"; - fprintf fmt " rewrite spec_extend_tr; auto.\n"; - fprintf fmt " Qed.\n"; - fprintf fmt " Hint Rewrite spec_cast_r: extr.\n"; + fprintf fmt " Let spec_cast_r: forall n m x1,\n"; + fprintf fmt " [%sn (Max.max n m)\n" c; + fprintf fmt " (castm (diff_l n m) (extend_tr x1 (fst (diff n m))))] =\n"; + fprintf fmt " [%sn m x1].\n" c; + fprintf fmt " Proof.\n"; + fprintf fmt " intros n m x1; case (diff_l n m); simpl castm.\n"; + fprintf fmt " rewrite spec_extend_tr; auto.\n"; + fprintf fmt " Qed.\n"; + fprintf fmt " Hint Rewrite spec_cast_r: extr.\n"; fprintf fmt "\n"; - fprintf fmt " Let spec_extend0_0: forall wx, [%s1 (WW w_0 wx)] = [%s0 wx].\n" c c; - fprintf fmt " Proof.\n"; - fprintf fmt " intros x; unfold to_Z.\n"; - fprintf fmt " rewrite <- (Zplus_0_l (znz_to_Z w0_op x)).\n"; - fprintf fmt " rewrite znz_to_Z_1.\n"; - fprintf fmt " rewrite <- (Zmult_0_l (base (znz_digits w0_op))).\n"; - fprintf fmt " apply (f_equal2 Zplus); auto.\n"; - fprintf fmt " apply (f_equal2 Zmult); auto.\n"; - fprintf fmt " exact (spec_0 w0_spec); auto.\n"; - fprintf fmt " Qed.\n"; - fprintf fmt " Hint Rewrite spec_extend0_0: extr.\n"; - fprintf fmt " \n"; + fprintf fmt " Let spec_extend0_0: forall wx, [%s1 (WW w_0 wx)] = [%s0 wx].\n" c c; + fprintf fmt " Proof.\n"; + fprintf fmt " intros x; unfold to_Z.\n"; + fprintf fmt " rewrite <- (Zplus_0_l (znz_to_Z w0_op x)).\n"; + fprintf fmt " rewrite znz_to_Z_1.\n"; + fprintf fmt " rewrite <- (Zmult_0_l (base (znz_digits w0_op))).\n"; + fprintf fmt " apply (f_equal2 Zplus); auto.\n"; + fprintf fmt " apply (f_equal2 Zmult); auto.\n"; + fprintf fmt " exact (spec_0 w0_spec); auto.\n"; + fprintf fmt " Qed.\n"; + fprintf fmt " Hint Rewrite spec_extend0_0: extr.\n"; + fprintf fmt " \n"; for i = 1 to size do for j = 1 to size - i do - fprintf fmt " Let spec_extend%i_%i: forall wx, [%s%i (extend%i _ wx)] = [%s%i wx].\n" i j c (i + j) i c j; - fprintf fmt " Proof. + fprintf fmt " Let spec_extend%i_%i: forall wx, [%s%i (extend%i _ wx)] = [%s%i wx].\n" i j c (i + j) i c j; + fprintf fmt " Proof. intros x; unfold extend%i, to_Z.\n" i; - fprintf fmt " rewrite <- (Zplus_0_l (znz_to_Z w%i_op x)).\n" j; - fprintf fmt " rewrite znz_to_Z_%i; auto.\n" (i + j); - fprintf fmt " Qed.\n"; - fprintf fmt " Hint Rewrite spec_extend%i_%i: extr.\n" i j; + fprintf fmt " rewrite <- (Zplus_0_l (znz_to_Z w%i_op x)).\n" j; + fprintf fmt " rewrite znz_to_Z_%i; auto.\n" (i + j); + fprintf fmt " Qed.\n"; + fprintf fmt " Hint Rewrite spec_extend%i_%i: extr.\n" i j; fprintf fmt "\n"; done; - fprintf fmt " Let spec_extend%i_0: forall wx, [%sn 0 (extend%i _ wx)] = [N%i wx].\n" i c i (size + 1 - i); - fprintf fmt " Proof.\n"; - fprintf fmt " intros x; unfold extend%i, to_Z; auto.\n" (size + 1 - i); - fprintf fmt " Qed.\n"; - fprintf fmt " Hint Rewrite spec_extend%i_0: extr.\n" i; - fprintf fmt " \n"; + fprintf fmt " Let spec_extend%i_0: forall wx, [%sn 0 (extend%i _ wx)] = [N%i wx].\n" i c i (size + 1 - i); + fprintf fmt " Proof.\n"; + fprintf fmt " intros x; unfold extend%i, to_Z; auto.\n" (size + 1 - i); + fprintf fmt " Qed.\n"; + fprintf fmt " Hint Rewrite spec_extend%i_0: extr.\n" i; + fprintf fmt " \n"; done; + end; - - fprintf fmt " Theorem spec_add: forall x y, [add x y] = [x] + [y].\n"; - fprintf fmt " Proof.\n"; - fprintf fmt " intros x y; case x; unfold add.\n"; - fprintf fmt " intros x1; case y.\n"; - fprintf fmt " intros y1; rewrite spec_w0_add; auto.\n"; + fprintf fmt " Theorem spec_add: forall x y, [add x y] = [x] + [y].\n"; + if gen_proof5 then + begin + fprintf fmt " Proof.\n"; + fprintf fmt " intros x y; case x; unfold add.\n"; + fprintf fmt " intros x1; case y.\n"; + fprintf fmt " intros y1; rewrite spec_w0_add; auto.\n"; for i = 1 to size do - fprintf fmt " intros y1; generalize (spec_w0_eq0 x1); case w0_eq0; intros HH.\n"; - fprintf fmt " rewrite HH; auto.\n"; + fprintf fmt " intros y1; generalize (spec_w0_eq0 x1); case w0_eq0; intros HH.\n"; + fprintf fmt " rewrite HH; auto.\n"; if i = 1 then - fprintf fmt " rewrite spec_w1_add; rewrite spec_extend0_0; auto.\n" + fprintf fmt " rewrite spec_w1_add; rewrite spec_extend0_0; auto.\n" else - fprintf fmt " rewrite spec_w%i_add; rewrite spec_extend%i_1; rewrite spec_extend0_0; auto.\n" i (i -1); + fprintf fmt " rewrite spec_w%i_add; rewrite spec_extend%i_1; rewrite spec_extend0_0; auto.\n" i (i -1); done; - fprintf fmt " intros n y1; generalize (spec_w0_eq0 x1); case w0_eq0; intros HH.\n"; - fprintf fmt " rewrite HH; auto.\n"; - fprintf fmt " rewrite spec_wn_add.\n"; - fprintf fmt " rewrite spec_extendn_0; rewrite spec_extend%i_0; rewrite spec_extend0_0; auto.\n" size; + fprintf fmt " intros n y1; generalize (spec_w0_eq0 x1); case w0_eq0; intros HH.\n"; + fprintf fmt " rewrite HH; auto.\n"; + fprintf fmt " rewrite spec_wn_add.\n"; + fprintf fmt " rewrite spec_extendn_0; rewrite spec_extend%i_0; rewrite spec_extend0_0; auto.\n" size; for i = 1 to size do - fprintf fmt " intros x1; case y.\n"; - fprintf fmt " intros y1; generalize (spec_w0_eq0 y1); case w0_eq0; intros HH.\n"; - fprintf fmt " rewrite HH; rewrite Zplus_0_r; auto.\n"; + fprintf fmt " intros x1; case y.\n"; + fprintf fmt " intros y1; generalize (spec_w0_eq0 y1); case w0_eq0; intros HH.\n"; + fprintf fmt " rewrite HH; rewrite Zplus_0_r; auto.\n"; if i = 1 then - fprintf fmt " rewrite spec_w1_add; rewrite spec_extend0_0; auto.\n" + fprintf fmt " rewrite spec_w1_add; rewrite spec_extend0_0; auto.\n" else - fprintf fmt " rewrite spec_w%i_add; rewrite spec_extend%i_1; rewrite spec_extend0_0; auto.\n" i (i-1); + fprintf fmt " rewrite spec_w%i_add; rewrite spec_extend%i_1; rewrite spec_extend0_0; auto.\n" i (i-1); for j = 1 to size do if i <= j then - fprintf fmt " intros y1; rewrite spec_w%i_add; auto.\n" j + fprintf fmt " intros y1; rewrite spec_w%i_add; auto.\n" j else - fprintf fmt " intros y1; rewrite spec_w%i_add; auto.\n" i; + fprintf fmt " intros y1; rewrite spec_w%i_add; auto.\n" i; done; - fprintf fmt " intros n y1; rewrite spec_wn_add.\n"; - fprintf fmt " rewrite spec_extendn_0; rewrite spec_extend%i_0; auto.\n" (size + 1 - i); - done; - fprintf fmt " intros n x1; case y.\n"; - fprintf fmt " intros y1; generalize (spec_w0_eq0 y1); case w0_eq0; intros HH.\n"; - fprintf fmt " rewrite HH; rewrite Zplus_0_r; auto.\n"; - fprintf fmt " rewrite spec_wn_add; rewrite spec_extendn_0; \n"; - fprintf fmt " rewrite spec_extend%i_0; rewrite spec_extend0_0; auto.\n" size; + fprintf fmt " intros n y1; rewrite spec_wn_add.\n"; + fprintf fmt " rewrite spec_extendn_0; rewrite spec_extend%i_0; auto.\n" (size + 1 - i); + done; + fprintf fmt " intros n x1; case y.\n"; + fprintf fmt " intros y1; generalize (spec_w0_eq0 y1); case w0_eq0; intros HH.\n"; + fprintf fmt " rewrite HH; rewrite Zplus_0_r; auto.\n"; + fprintf fmt " rewrite spec_wn_add; rewrite spec_extendn_0; \n"; + fprintf fmt " rewrite spec_extend%i_0; rewrite spec_extend0_0; auto.\n" size; for i = 1 to size do - fprintf fmt " intros y1; rewrite spec_wn_add; rewrite spec_extendn_0; rewrite spec_extend%i_0; auto.\n" (size + 1 - i); + fprintf fmt " intros y1; rewrite spec_wn_add; rewrite spec_extendn_0; rewrite spec_extend%i_0; auto.\n" (size + 1 - i); done; - fprintf fmt " intros m y1; rewrite spec_wn_add; rewrite spec_cast_l; rewrite spec_cast_r; auto.\n"; - fprintf fmt " Qed.\n"; + fprintf fmt " intros m y1; rewrite spec_wn_add; rewrite spec_cast_l; rewrite spec_cast_r; auto.\n"; + fprintf fmt " Qed.\n"; + end else + fprintf fmt " Admitted.\n"; fprintf fmt "\n"; - fprintf fmt " Let spec_reduce_0: forall x, [reduce_0 x] = [%s0 x].\n" c; - fprintf fmt " Proof.\n"; - fprintf fmt " intros x; unfold to_Z, reduce_0.\n"; - fprintf fmt " auto.\n"; - fprintf fmt " Qed.\n"; - fprintf fmt " \n"; + if gen_proof6 then + begin + fprintf fmt " Let spec_reduce_0: forall x, [reduce_0 x] = [%s0 x].\n" c; + fprintf fmt " Proof.\n"; + fprintf fmt " intros x; unfold to_Z, reduce_0.\n"; + fprintf fmt " auto.\n"; + fprintf fmt " Qed.\n"; + fprintf fmt " \n"; for i = 1 to size + 1 do if (i == size + 1) then - fprintf fmt " Let spec_reduce_%i: forall x, [reduce_%i x] = [%sn 0 x].\n" i i c + fprintf fmt " Let spec_reduce_%i: forall x, [reduce_%i x] = [%sn 0 x].\n" i i c else - fprintf fmt " Let spec_reduce_%i: forall x, [reduce_%i x] = [%s%i x].\n" i i c i; - fprintf fmt " Proof.\n"; - fprintf fmt " intros x; case x; unfold reduce_%i.\n" i; - fprintf fmt " exact (spec_0 w0_spec).\n"; - fprintf fmt " intros x1 y1.\n"; - fprintf fmt " generalize (spec_w%i_eq0 x1); \n" (i - 1); - fprintf fmt " case w%i_eq0; intros H1; auto.\n" (i - 1); + fprintf fmt " Let spec_reduce_%i: forall x, [reduce_%i x] = [%s%i x].\n" i i c i; + fprintf fmt " Proof.\n"; + fprintf fmt " intros x; case x; unfold reduce_%i.\n" i; + fprintf fmt " exact (spec_0 w0_spec).\n"; + fprintf fmt " intros x1 y1.\n"; + fprintf fmt " generalize (spec_w%i_eq0 x1); \n" (i - 1); + fprintf fmt " case w%i_eq0; intros H1; auto.\n" (i - 1); if i <> 1 then - fprintf fmt " rewrite spec_reduce_%i.\n" (i - 1); - fprintf fmt " unfold to_Z; rewrite znz_to_Z_%i.\n" i; - fprintf fmt " unfold to_Z in H1; rewrite H1; auto.\n"; - fprintf fmt " Qed.\n"; - fprintf fmt " \n"; + fprintf fmt " rewrite spec_reduce_%i.\n" (i - 1); + fprintf fmt " unfold to_Z; rewrite znz_to_Z_%i.\n" i; + fprintf fmt " unfold to_Z in H1; rewrite H1; auto.\n"; + fprintf fmt " Qed.\n"; + fprintf fmt " \n"; done; - fprintf fmt " Let spec_reduce_n: forall n x, [reduce_n n x] = [%sn n x].\n" c; - fprintf fmt " Proof.\n"; - fprintf fmt " intros n; elim n; simpl reduce_n.\n"; - fprintf fmt " intros x; rewrite <- spec_reduce_%i; auto.\n" (size + 1); - fprintf fmt " intros n1 Hrec x; case x.\n"; - fprintf fmt " unfold to_Z; rewrite make_op_S; auto.\n"; - fprintf fmt " exact (spec_0 w0_spec).\n"; - fprintf fmt " intros x1 y1; case x1; auto.\n"; - fprintf fmt " rewrite Hrec.\n"; - fprintf fmt " rewrite spec_extendn0_0; auto.\n"; - fprintf fmt " Qed.\n"; - fprintf fmt " \n"; - - fprintf fmt " Let to_Z_pos: forall x, 0 <= [x].\n"; - fprintf fmt " Proof.\n"; - fprintf fmt " intros x; case x; unfold to_Z.\n"; - for i = 0 to size do - fprintf fmt " intros x1; case (spec_to_Z w%i_spec x1); auto.\n" i; - done; - fprintf fmt " intros n x1; case (spec_to_Z (wn_spec n) x1); auto.\n"; - fprintf fmt " Qed.\n"; - fprintf fmt " \n"; + fprintf fmt " Let spec_reduce_n: forall n x, [reduce_n n x] = [%sn n x].\n" c; + fprintf fmt " Proof.\n"; + fprintf fmt " intros n; elim n; simpl reduce_n.\n"; + fprintf fmt " intros x; rewrite <- spec_reduce_%i; auto.\n" (size + 1); + fprintf fmt " intros n1 Hrec x; case x.\n"; + fprintf fmt " unfold to_Z; rewrite make_op_S; auto.\n"; + fprintf fmt " exact (spec_0 w0_spec).\n"; + fprintf fmt " intros x1 y1; case x1; auto.\n"; + fprintf fmt " rewrite Hrec.\n"; + fprintf fmt " rewrite spec_extendn0_0; auto.\n"; + fprintf fmt " Qed.\n"; + fprintf fmt " \n"; - fprintf fmt " Let spec_pred: forall x, 0 < [x] -> [pred x] = [x] - 1.\n"; + fprintf fmt " Let to_Z_pos: forall x, 0 <= [x].\n"; fprintf fmt " Proof.\n"; - fprintf fmt " intros x; case x; unfold pred.\n"; + fprintf fmt " intros x; case x; unfold to_Z.\n"; for i = 0 to size do - fprintf fmt " intros x1 H1; unfold w%i_pred_c; \n" i; - fprintf fmt " generalize (spec_pred_c w%i_spec x1); case znz_pred_c; intros y1.\n" i; - fprintf fmt " rewrite spec_reduce_%i; auto.\n" i; - fprintf fmt " unfold interp_carry; unfold to_Z.\n"; - fprintf fmt " case (spec_to_Z w%i_spec x1); intros HH1 HH2.\n" i; - fprintf fmt " case (spec_to_Z w%i_spec y1); intros HH3 HH4 HH5.\n" i; - fprintf fmt " assert (znz_to_Z w%i_op x1 - 1 < 0); auto with zarith.\n" i; - fprintf fmt " unfold to_Z in H1; auto with zarith.\n"; - done; - fprintf fmt " intros n x1 H1; \n"; - fprintf fmt " generalize (spec_pred_c (wn_spec n) x1); case znz_pred_c; intros y1.\n"; - fprintf fmt " rewrite spec_reduce_n; auto.\n"; - fprintf fmt " unfold interp_carry; unfold to_Z.\n"; - fprintf fmt " case (spec_to_Z (wn_spec n) x1); intros HH1 HH2.\n"; - fprintf fmt " case (spec_to_Z (wn_spec n) y1); intros HH3 HH4 HH5.\n"; - fprintf fmt " assert (znz_to_Z (make_op n) x1 - 1 < 0); auto with zarith.\n"; - fprintf fmt " unfold to_Z in H1; auto with zarith.\n"; + fprintf fmt " intros x1; case (spec_to_Z w%i_spec x1); auto.\n" i; + done; + fprintf fmt " intros n x1; case (spec_to_Z (wn_spec n) x1); auto.\n"; fprintf fmt " Qed.\n"; fprintf fmt " \n"; - fprintf fmt " Let spec_pred0: forall x, [x] = 0 -> [pred x] = 0.\n"; - fprintf fmt " Proof.\n"; - fprintf fmt " intros x; case x; unfold pred.\n"; + fprintf fmt " Let spec_pred: forall x, 0 < [x] -> [pred x] = [x] - 1.\n"; + fprintf fmt " Proof.\n"; + fprintf fmt " intros x; case x; unfold pred.\n"; for i = 0 to size do - fprintf fmt " intros x1 H1; unfold w%i_pred_c; \n" i; - fprintf fmt " generalize (spec_pred_c w%i_spec x1); case znz_pred_c; intros y1.\n" i; - fprintf fmt " unfold interp_carry; unfold to_Z.\n"; - fprintf fmt " unfold to_Z in H1; auto with zarith.\n"; - fprintf fmt " case (spec_to_Z w%i_spec y1); intros HH3 HH4; auto with zarith.\n" i; - fprintf fmt " intros; exact (spec_0 w0_spec).\n"; - done; - fprintf fmt " intros n x1 H1; \n"; - fprintf fmt " generalize (spec_pred_c (wn_spec n) x1); case znz_pred_c; intros y1.\n"; - fprintf fmt " unfold interp_carry; unfold to_Z.\n"; - fprintf fmt " unfold to_Z in H1; auto with zarith.\n"; - fprintf fmt " case (spec_to_Z (wn_spec n) y1); intros HH3 HH4; auto with zarith.\n"; - fprintf fmt " intros; exact (spec_0 w0_spec).\n"; - fprintf fmt " Qed.\n"; - fprintf fmt " \n"; + fprintf fmt " intros x1 H1; unfold w%i_pred_c; \n" i; + fprintf fmt " generalize (spec_pred_c w%i_spec x1); case znz_pred_c; intros y1.\n" i; + fprintf fmt " rewrite spec_reduce_%i; auto.\n" i; + fprintf fmt " unfold interp_carry; unfold to_Z.\n"; + fprintf fmt " case (spec_to_Z w%i_spec x1); intros HH1 HH2.\n" i; + fprintf fmt " case (spec_to_Z w%i_spec y1); intros HH3 HH4 HH5.\n" i; + fprintf fmt " assert (znz_to_Z w%i_op x1 - 1 < 0); auto with zarith.\n" i; + fprintf fmt " unfold to_Z in H1; auto with zarith.\n"; + done; + fprintf fmt " intros n x1 H1; \n"; + fprintf fmt " generalize (spec_pred_c (wn_spec n) x1); case znz_pred_c; intros y1.\n"; + fprintf fmt " rewrite spec_reduce_n; auto.\n"; + fprintf fmt " unfold interp_carry; unfold to_Z.\n"; + fprintf fmt " case (spec_to_Z (wn_spec n) x1); intros HH1 HH2.\n"; + fprintf fmt " case (spec_to_Z (wn_spec n) y1); intros HH3 HH4 HH5.\n"; + fprintf fmt " assert (znz_to_Z (make_op n) x1 - 1 < 0); auto with zarith.\n"; + fprintf fmt " unfold to_Z in H1; auto with zarith.\n"; + fprintf fmt " Qed.\n"; + fprintf fmt " \n"; + + fprintf fmt " Let spec_pred0: forall x, [x] = 0 -> [pred x] = 0.\n"; + fprintf fmt " Proof.\n"; + fprintf fmt " intros x; case x; unfold pred.\n"; + for i = 0 to size do + fprintf fmt " intros x1 H1; unfold w%i_pred_c; \n" i; + fprintf fmt " generalize (spec_pred_c w%i_spec x1); case znz_pred_c; intros y1.\n" i; + fprintf fmt " unfold interp_carry; unfold to_Z.\n"; + fprintf fmt " unfold to_Z in H1; auto with zarith.\n"; + fprintf fmt " case (spec_to_Z w%i_spec y1); intros HH3 HH4; auto with zarith.\n" i; + fprintf fmt " intros; exact (spec_0 w0_spec).\n"; + done; + fprintf fmt " intros n x1 H1; \n"; + fprintf fmt " generalize (spec_pred_c (wn_spec n) x1); case znz_pred_c; intros y1.\n"; + fprintf fmt " unfold interp_carry; unfold to_Z.\n"; + fprintf fmt " unfold to_Z in H1; auto with zarith.\n"; + fprintf fmt " case (spec_to_Z (wn_spec n) y1); intros HH3 HH4; auto with zarith.\n"; + fprintf fmt " intros; exact (spec_0 w0_spec).\n"; + fprintf fmt " Qed.\n"; + fprintf fmt " \n"; for i = 0 to size do - fprintf fmt " Let spec_w%i_sub: forall x y, [%s%i y] <= [%s%i x] -> [w%i_sub x y] = [%s%i x] - [%s%i y].\n" i c i c i i c i c i; - fprintf fmt " Proof.\n"; - fprintf fmt " intros n m; unfold w%i_sub, w%i_sub_c.\n" i i; - fprintf fmt " generalize (spec_sub_c w%i_spec n m); case znz_sub_c; \n" i; + fprintf fmt " Let spec_w%i_sub: forall x y, [%s%i y] <= [%s%i x] -> [w%i_sub x y] = [%s%i x] - [%s%i y].\n" i c i c i i c i c i; + fprintf fmt " Proof.\n"; + fprintf fmt " intros n m; unfold w%i_sub, w%i_sub_c.\n" i i; + fprintf fmt " generalize (spec_sub_c w%i_spec n m); case znz_sub_c; \n" i; if i == 0 then - fprintf fmt " intros x; auto.\n" + fprintf fmt " intros x; auto.\n" else - fprintf fmt " intros x; try rewrite spec_reduce_%i; auto.\n" i; - fprintf fmt " unfold interp_carry; unfold zero, w_0, to_Z.\n"; - fprintf fmt " rewrite (spec_0 w0_spec).\n"; - fprintf fmt " case (spec_to_Z w%i_spec x); intros; auto with zarith.\n" i; - fprintf fmt " Qed.\n"; + fprintf fmt " intros x; try rewrite spec_reduce_%i; auto.\n" i; + fprintf fmt " unfold interp_carry; unfold zero, w_0, to_Z.\n"; + fprintf fmt " rewrite (spec_0 w0_spec).\n"; + fprintf fmt " case (spec_to_Z w%i_spec x); intros; auto with zarith.\n" i; + fprintf fmt " Qed.\n"; fprintf fmt "\n"; done; - fprintf fmt " Let spec_wn_sub: forall n x y, [%sn n y] <= [%sn n x] -> [subn n x y] = [%sn n x] - [%sn n y].\n" c c c c; - fprintf fmt " Proof.\n"; - fprintf fmt " intros k n m; unfold subn.\n"; - fprintf fmt " generalize (spec_sub_c (wn_spec k) n m); case znz_sub_c; \n"; - fprintf fmt " intros x; auto.\n"; - fprintf fmt " unfold interp_carry, to_Z.\n"; - fprintf fmt " case (spec_to_Z (wn_spec k) x); intros; auto with zarith.\n"; - fprintf fmt " Qed.\n"; + fprintf fmt " Let spec_wn_sub: forall n x y, [%sn n y] <= [%sn n x] -> [subn n x y] = [%sn n x] - [%sn n y].\n" c c c c; + fprintf fmt " Proof.\n"; + fprintf fmt " intros k n m; unfold subn.\n"; + fprintf fmt " generalize (spec_sub_c (wn_spec k) n m); case znz_sub_c; \n"; + fprintf fmt " intros x; auto.\n"; + fprintf fmt " unfold interp_carry, to_Z.\n"; + fprintf fmt " case (spec_to_Z (wn_spec k) x); intros; auto with zarith.\n"; + fprintf fmt " Qed.\n"; fprintf fmt "\n"; + end; - - fprintf fmt " Theorem spec_sub: forall x y, [y] <= [x] -> [sub x y] = [x] - [y].\n"; - fprintf fmt " Proof.\n"; - fprintf fmt " intros x y; case x; unfold sub.\n"; - fprintf fmt " intros x1; case y.\n"; - fprintf fmt " intros y1 H; rewrite spec_w0_sub; auto.\n"; + fprintf fmt " Theorem spec_sub: forall x y, [y] <= [x] -> [sub x y] = [x] - [y].\n"; + if gen_proof7 then + begin + fprintf fmt " Proof.\n"; + fprintf fmt " intros x y; case x; unfold sub.\n"; + fprintf fmt " intros x1; case y.\n"; + fprintf fmt " intros y1 H; rewrite spec_w0_sub; auto.\n"; for i = 1 to size do - fprintf fmt " intros y1 H; generalize (spec_w0_eq0 x1); case w0_eq0; intros HH.\n"; - fprintf fmt " generalize H; rewrite HH; unfold to_Z, zero, w_0.\n"; - fprintf fmt " rewrite (spec_0 w0_spec); case (spec_to_Z w%i_spec y1); auto with zarith.\n" i; + fprintf fmt " intros y1 H; generalize (spec_w0_eq0 x1); case w0_eq0; intros HH.\n"; + fprintf fmt " generalize H; rewrite HH; unfold to_Z, zero, w_0.\n"; + fprintf fmt " rewrite (spec_0 w0_spec); case (spec_to_Z w%i_spec y1); auto with zarith.\n" i; if i == 1 then - fprintf fmt " rewrite spec_w1_sub; rewrite spec_extend0_0; auto.\n" + fprintf fmt " rewrite spec_w1_sub; rewrite spec_extend0_0; auto.\n" else - fprintf fmt " rewrite spec_w%i_sub; rewrite spec_extend%i_1; rewrite spec_extend0_0; auto.\n" i (i - 1); + fprintf fmt " rewrite spec_w%i_sub; rewrite spec_extend%i_1; rewrite spec_extend0_0; auto.\n" i (i - 1); done; - fprintf fmt " intros n y1 H; generalize (spec_w0_eq0 x1); case w0_eq0; intros HH.\n"; - fprintf fmt " generalize H; rewrite HH; unfold to_Z, zero, w_0.\n"; - fprintf fmt " rewrite (spec_0 w0_spec); case (spec_to_Z (wn_spec n) y1); auto with zarith.\n"; - fprintf fmt " rewrite spec_wn_sub; rewrite spec_extendn_0; rewrite spec_extend%i_0; rewrite spec_extend0_0; auto.\n" size; + fprintf fmt " intros n y1 H; generalize (spec_w0_eq0 x1); case w0_eq0; intros HH.\n"; + fprintf fmt " generalize H; rewrite HH; unfold to_Z, zero, w_0.\n"; + fprintf fmt " rewrite (spec_0 w0_spec); case (spec_to_Z (wn_spec n) y1); auto with zarith.\n"; + fprintf fmt " rewrite spec_wn_sub; rewrite spec_extendn_0; rewrite spec_extend%i_0; rewrite spec_extend0_0; auto.\n" size; for i = 1 to size do - fprintf fmt " intros x1; case y.\n"; - fprintf fmt " intros y1 H; generalize (spec_w0_eq0 y1); case w0_eq0; intros HH.\n"; - fprintf fmt " rewrite HH; rewrite Zminus_0_r; auto.\n"; + fprintf fmt " intros x1; case y.\n"; + fprintf fmt " intros y1 H; generalize (spec_w0_eq0 y1); case w0_eq0; intros HH.\n"; + fprintf fmt " rewrite HH; rewrite Zminus_0_r; auto.\n"; if i = 1 then - fprintf fmt " rewrite spec_w1_sub; rewrite spec_extend0_0; auto.\n" + fprintf fmt " rewrite spec_w1_sub; rewrite spec_extend0_0; auto.\n" else - fprintf fmt " rewrite spec_w%i_sub; rewrite spec_extend%i_1; rewrite spec_extend0_0; auto.\n" i (i-1); + fprintf fmt " rewrite spec_w%i_sub; rewrite spec_extend%i_1; rewrite spec_extend0_0; auto.\n" i (i-1); for j = 1 to size do if i <= j then - fprintf fmt " intros y1 H; rewrite spec_w%i_sub; auto.\n" j + fprintf fmt " intros y1 H; rewrite spec_w%i_sub; auto.\n" j else - fprintf fmt " intros y1 H; rewrite spec_w%i_sub; auto.\n" i; + fprintf fmt " intros y1 H; rewrite spec_w%i_sub; auto.\n" i; done; - fprintf fmt " intros n y1 H; rewrite spec_wn_sub;\n"; - fprintf fmt " rewrite spec_extendn_0; rewrite spec_extend%i_0; auto.\n" (size + 1 - i); - done; - fprintf fmt " intros n x1; case y.\n"; - fprintf fmt " intros y1 H; generalize (spec_w0_eq0 y1); case w0_eq0; intros HH.\n"; - fprintf fmt " rewrite HH; rewrite Zminus_0_r; auto.\n"; - fprintf fmt " rewrite spec_wn_sub; rewrite spec_extendn_0; \n"; - fprintf fmt " rewrite spec_extend%i_0; rewrite spec_extend0_0; auto.\n" size; + fprintf fmt " intros n y1 H; rewrite spec_wn_sub;\n"; + fprintf fmt " rewrite spec_extendn_0; rewrite spec_extend%i_0; auto.\n" (size + 1 - i); + done; + fprintf fmt " intros n x1; case y.\n"; + fprintf fmt " intros y1 H; generalize (spec_w0_eq0 y1); case w0_eq0; intros HH.\n"; + fprintf fmt " rewrite HH; rewrite Zminus_0_r; auto.\n"; + fprintf fmt " rewrite spec_wn_sub; rewrite spec_extendn_0; \n"; + fprintf fmt " rewrite spec_extend%i_0; rewrite spec_extend0_0; auto.\n" size; for i = 1 to size do - fprintf fmt " intros y1 H; rewrite spec_wn_sub; rewrite spec_extendn_0; rewrite spec_extend%i_0; auto.\n" (size + 1 - i); + fprintf fmt " intros y1 H; rewrite spec_wn_sub; rewrite spec_extendn_0; rewrite spec_extend%i_0; auto.\n" (size + 1 - i); done; - fprintf fmt " intros m y1 H; rewrite spec_wn_sub; rewrite spec_cast_l; rewrite spec_cast_r; auto.\n"; - fprintf fmt " Qed.\n"; + fprintf fmt " intros m y1 H; rewrite spec_wn_sub; rewrite spec_cast_l; rewrite spec_cast_r; auto.\n"; + fprintf fmt " Qed.\n"; + end else + fprintf fmt " Admitted.\n"; fprintf fmt "\n"; + if gen_proof8 then + begin for i = 0 to size do - fprintf fmt " Let spec_w%i_sub0: forall x y, [%s%i x] < [%s%i y] -> [w%i_sub x y] = 0.\n" i c i c i i; - fprintf fmt " Proof.\n"; - fprintf fmt " intros n m; unfold w%i_sub, w%i_sub_c.\n" i i; - fprintf fmt " generalize (spec_sub_c w%i_spec n m); case znz_sub_c; \n" i; - fprintf fmt " intros x; unfold interp_carry.\n"; - fprintf fmt " unfold to_Z; case (spec_to_Z w%i_spec x); intros; auto with zarith.\n" i; - fprintf fmt " intros; unfold to_Z, zero, w_0; rewrite (spec_0 w0_spec); auto.\n"; - fprintf fmt " Qed.\n"; + fprintf fmt " Let spec_w%i_sub0: forall x y, [%s%i x] < [%s%i y] -> [w%i_sub x y] = 0.\n" i c i c i i; + fprintf fmt " Proof.\n"; + fprintf fmt " intros n m; unfold w%i_sub, w%i_sub_c.\n" i i; + fprintf fmt " generalize (spec_sub_c w%i_spec n m); case znz_sub_c; \n" i; + fprintf fmt " intros x; unfold interp_carry.\n"; + fprintf fmt " unfold to_Z; case (spec_to_Z w%i_spec x); intros; auto with zarith.\n" i; + fprintf fmt " intros; unfold to_Z, zero, w_0; rewrite (spec_0 w0_spec); auto.\n"; + fprintf fmt " Qed.\n"; fprintf fmt "\n"; done; - fprintf fmt " Let spec_wn_sub0: forall n x y, [%sn n x] < [%sn n y] -> [subn n x y] = 0.\n" c c; - fprintf fmt " Proof.\n"; - fprintf fmt " intros k n m; unfold subn.\n"; - fprintf fmt " generalize (spec_sub_c (wn_spec k) n m); case znz_sub_c; \n"; - fprintf fmt " intros x; unfold interp_carry.\n"; - fprintf fmt " unfold to_Z; case (spec_to_Z (wn_spec k) x); intros; auto with zarith.\n"; - fprintf fmt " intros; unfold to_Z, w_0; rewrite (spec_0 (w0_spec)); auto.\n"; - fprintf fmt " Qed.\n"; + fprintf fmt " Let spec_wn_sub0: forall n x y, [%sn n x] < [%sn n y] -> [subn n x y] = 0.\n" c c; + fprintf fmt " Proof.\n"; + fprintf fmt " intros k n m; unfold subn.\n"; + fprintf fmt " generalize (spec_sub_c (wn_spec k) n m); case znz_sub_c; \n"; + fprintf fmt " intros x; unfold interp_carry.\n"; + fprintf fmt " unfold to_Z; case (spec_to_Z (wn_spec k) x); intros; auto with zarith.\n"; + fprintf fmt " intros; unfold to_Z, w_0; rewrite (spec_0 (w0_spec)); auto.\n"; + fprintf fmt " Qed.\n"; fprintf fmt "\n"; + end; - - fprintf fmt " Theorem spec_sub0: forall x y, [x] < [y] -> [sub x y] = 0.\n"; - fprintf fmt " Proof.\n"; - fprintf fmt " intros x y; case x; unfold sub.\n"; - fprintf fmt " intros x1; case y.\n"; - fprintf fmt " intros y1 H; rewrite spec_w0_sub0; auto.\n"; + fprintf fmt " Theorem spec_sub0: forall x y, [x] < [y] -> [sub x y] = 0.\n"; + if gen_proof9 then + begin + fprintf fmt " Proof.\n"; + fprintf fmt " intros x y; case x; unfold sub.\n"; + fprintf fmt " intros x1; case y.\n"; + fprintf fmt " intros y1 H; rewrite spec_w0_sub0; auto.\n"; for i = 1 to size do - fprintf fmt " intros y1 H; generalize (spec_w0_eq0 x1); case w0_eq0; intros HH.\n"; - fprintf fmt " unfold to_Z, zero, w_0; rewrite (spec_0 w0_spec); auto.\n"; + fprintf fmt " intros y1 H; generalize (spec_w0_eq0 x1); case w0_eq0; intros HH.\n"; + fprintf fmt " unfold to_Z, zero, w_0; rewrite (spec_0 w0_spec); auto.\n"; if i == 1 then - fprintf fmt " apply spec_w1_sub0; rewrite spec_extend0_0; auto.\n" + fprintf fmt " apply spec_w1_sub0; rewrite spec_extend0_0; auto.\n" else - fprintf fmt " apply spec_w%i_sub0; rewrite spec_extend%i_1; rewrite spec_extend0_0; auto.\n" i (i - 1); + fprintf fmt " apply spec_w%i_sub0; rewrite spec_extend%i_1; rewrite spec_extend0_0; auto.\n" i (i - 1); done; - fprintf fmt " intros n y1 H; generalize (spec_w0_eq0 x1); case w0_eq0; intros HH.\n"; - fprintf fmt " unfold to_Z, zero, w_0; rewrite (spec_0 w0_spec); auto.\n"; - fprintf fmt " apply spec_wn_sub0; rewrite spec_extendn_0; rewrite spec_extend%i_0; rewrite spec_extend0_0; auto.\n" size; + fprintf fmt " intros n y1 H; generalize (spec_w0_eq0 x1); case w0_eq0; intros HH.\n"; + fprintf fmt " unfold to_Z, zero, w_0; rewrite (spec_0 w0_spec); auto.\n"; + fprintf fmt " apply spec_wn_sub0; rewrite spec_extendn_0; rewrite spec_extend%i_0; rewrite spec_extend0_0; auto.\n" size; for i = 1 to size do - fprintf fmt " intros x1; case y.\n"; - fprintf fmt " intros y1 H; generalize (spec_w0_eq0 y1); case w0_eq0; intros HH.\n"; - fprintf fmt " generalize H; rewrite HH; unfold to_Z; case (spec_to_Z w%i_spec x1); auto with zarith.\n" i; + fprintf fmt " intros x1; case y.\n"; + fprintf fmt " intros y1 H; generalize (spec_w0_eq0 y1); case w0_eq0; intros HH.\n"; + fprintf fmt " generalize H; rewrite HH; unfold to_Z; case (spec_to_Z w%i_spec x1); auto with zarith.\n" i; if i = 1 then - fprintf fmt " apply spec_w1_sub0; rewrite spec_extend0_0; auto.\n" + fprintf fmt " apply spec_w1_sub0; rewrite spec_extend0_0; auto.\n" else - fprintf fmt " apply spec_w%i_sub0; rewrite spec_extend%i_1; rewrite spec_extend0_0; auto.\n" i (i-1); + fprintf fmt " apply spec_w%i_sub0; rewrite spec_extend%i_1; rewrite spec_extend0_0; auto.\n" i (i-1); for j = 1 to size do if i <= j then - fprintf fmt " intros y1 H; apply spec_w%i_sub0; auto.\n" j + fprintf fmt " intros y1 H; apply spec_w%i_sub0; auto.\n" j else - fprintf fmt " intros y1 H; apply spec_w%i_sub0; auto.\n" i; + fprintf fmt " intros y1 H; apply spec_w%i_sub0; auto.\n" i; done; - fprintf fmt " intros n y1 H; apply spec_wn_sub0;\n"; - fprintf fmt " rewrite spec_extendn_0; rewrite spec_extend%i_0; auto.\n" (size + 1 - i); - done; - fprintf fmt " intros n x1; case y.\n"; - fprintf fmt " intros y1 H; generalize (spec_w0_eq0 y1); case w0_eq0; intros HH.\n"; - fprintf fmt " generalize H; rewrite HH; unfold to_Z; case (spec_to_Z (wn_spec n) x1); auto with zarith.\n"; - fprintf fmt " apply spec_wn_sub0; rewrite spec_extendn_0; \n"; - fprintf fmt " rewrite spec_extend%i_0; rewrite spec_extend0_0; auto.\n" size; + fprintf fmt " intros n y1 H; apply spec_wn_sub0;\n"; + fprintf fmt " rewrite spec_extendn_0; rewrite spec_extend%i_0; auto.\n" (size + 1 - i); + done; + fprintf fmt " intros n x1; case y.\n"; + fprintf fmt " intros y1 H; generalize (spec_w0_eq0 y1); case w0_eq0; intros HH.\n"; + fprintf fmt " generalize H; rewrite HH; unfold to_Z; case (spec_to_Z (wn_spec n) x1); auto with zarith.\n"; + fprintf fmt " apply spec_wn_sub0; rewrite spec_extendn_0; \n"; + fprintf fmt " rewrite spec_extend%i_0; rewrite spec_extend0_0; auto.\n" size; for i = 1 to size do - fprintf fmt " intros y1 H; apply spec_wn_sub0; rewrite spec_extendn_0; rewrite spec_extend%i_0; auto.\n" (size + 1 - i); + fprintf fmt " intros y1 H; apply spec_wn_sub0; rewrite spec_extendn_0; rewrite spec_extend%i_0; auto.\n" (size + 1 - i); done; - fprintf fmt " intros m y1 H; apply spec_wn_sub0; rewrite spec_cast_l; rewrite spec_cast_r; auto.\n"; - fprintf fmt " Qed.\n"; + fprintf fmt " intros m y1 H; apply spec_wn_sub0; rewrite spec_cast_l; rewrite spec_cast_r; auto.\n"; + fprintf fmt " Qed.\n" + end + else + fprintf fmt " Admitted.\n"; + fprintf fmt "\n"; + + + if gen_proof then + begin + fprintf fmt " Let gen_make: forall n y, GenBase.gen_to_Z (znz_digits w%i_op) (znz_to_Z w%i_op) (S n) y =\n" size size; + fprintf fmt " znz_to_Z (make_op n) y.\n"; + fprintf fmt " Proof.\n"; + fprintf fmt " intros n; elim n; auto.\n"; + fprintf fmt " intros n1 Hrec y; case y; auto.\n"; + fprintf fmt " rewrite make_op_S; auto.\n"; + fprintf fmt " intros yh yl; rewrite znz_to_Z_n.\n"; + fprintf fmt " replace (base (znz_digits (make_op n1))) with (GenBase.gen_wB (znz_digits w%i_op) (S n1)).\n" size; + fprintf fmt " rewrite <- Hrec; rewrite <- Hrec; auto.\n"; + fprintf fmt " elim n1; clear Hrec y yh yl n1; auto.\n"; + fprintf fmt " intros n1 Hrec; rewrite make_op_S.\n"; + fprintf fmt " change (%sznz_digits (word w%i (S (S n1))) (mk_zn2z_op_karatsuba (make_op n1))) with (xO (znz_digits (make_op n1))).\n" "@" size; + fprintf fmt " rewrite base_xO; rewrite <- Hrec.\n"; + fprintf fmt " unfold GenBase.gen_wB; rewrite <- base_xO; auto.\n"; + fprintf fmt " Qed.\n"; + + + + fprintf fmt " Fixpoint nmake_op (ww:Set) (ww_op: znz_op ww) (n: nat) : \n"; + fprintf fmt " znz_op (word ww n) :=\n"; + fprintf fmt " match n return znz_op (word ww n) with \n"; + fprintf fmt " O => ww_op\n"; + fprintf fmt " | S n1 => mk_zn2z_op (nmake_op ww ww_op n1) \n"; + fprintf fmt " end.\n"; + fprintf fmt "\n"; + fprintf fmt " Theorem digits_th1: forall w (x: znz_op w) (y: znz_op w),\n"; + fprintf fmt " znz_digits x = znz_digits y ->\n"; + fprintf fmt " znz_digits (mk_zn2z_op x) = znz_digits (mk_zn2z_op y).\n"; + fprintf fmt " intros ww x y H.\n"; + fprintf fmt " simpl; unfold zn2z_to_Z; rewrite H; auto.\n"; + fprintf fmt " Qed.\n"; + fprintf fmt "\n"; + fprintf fmt "\n"; + fprintf fmt " Theorem digits_th2: forall w (x: znz_op w) (y: znz_op w),\n"; + fprintf fmt " znz_digits x = znz_digits y ->\n"; + fprintf fmt " znz_digits (mk_zn2z_op_karatsuba x) = znz_digits (mk_zn2z_op y).\n"; + fprintf fmt " intros ww x y H.\n"; + fprintf fmt " simpl; unfold zn2z_to_Z; rewrite H; auto.\n"; + fprintf fmt " Qed.\n"; + fprintf fmt "\n"; + fprintf fmt " Theorem make_th1: forall w (x: znz_op w) (y: znz_op w),\n"; + fprintf fmt " znz_digits x = znz_digits y ->\n"; + fprintf fmt " znz_to_Z x = znz_to_Z y ->\n"; + fprintf fmt " znz_to_Z (mk_zn2z_op x) = znz_to_Z (mk_zn2z_op y).\n"; + fprintf fmt " intros ww x y H H1.\n"; + fprintf fmt " simpl; unfold zn2z_to_Z; rewrite H; \n"; + fprintf fmt " rewrite H1; auto.\n"; + fprintf fmt " Qed.\n"; + fprintf fmt "\n"; + fprintf fmt " Theorem make_th2: forall w (x: znz_op w) (y: znz_op w),\n"; + fprintf fmt " znz_digits x = znz_digits y ->\n"; + fprintf fmt " znz_to_Z x = znz_to_Z y -> \n"; + fprintf fmt " znz_to_Z (mk_zn2z_op_karatsuba x) = znz_to_Z (mk_zn2z_op y).\n"; + fprintf fmt " intros ww x y H H1.\n"; + fprintf fmt " simpl; unfold zn2z_to_Z; rewrite H; \n"; + fprintf fmt " rewrite H1; auto.\n"; + fprintf fmt " Qed.\n"; + fprintf fmt "\n"; + fprintf fmt " Let nmake_op0 := nmake_op _ w0_op.\n"; + fprintf fmt "\n"; + fprintf fmt " Theorem make_th3: forall ww (w_op: znz_op ww) x, \n"; + fprintf fmt " nmake_op _ w_op (S x) = mk_zn2z_op (nmake_op _ w_op x).\n"; + fprintf fmt " auto.\n"; + fprintf fmt " Qed.\n"; fprintf fmt "\n"; + fprintf fmt " Theorem make_th4: forall x,\n"; + fprintf fmt " nmake_op0 (S x) = mk_zn2z_op (nmake_op0 x).\n"; + fprintf fmt " auto.\n"; + fprintf fmt " Qed.\n"; + fprintf fmt "\n"; + fprintf fmt " Theorem digits_0: znz_digits w0_op = znz_digits (nmake_op0 0).\n"; + fprintf fmt " auto.\n"; + fprintf fmt " Qed.\n"; + fprintf fmt "\n"; + fprintf fmt " Theorem nmake_0: znz_to_Z w0_op = znz_to_Z (nmake_op0 0).\n"; + fprintf fmt " auto.\n"; + fprintf fmt " Qed.\n"; + + for i = 1 to size do + fprintf fmt " Theorem digits_%i: znz_digits w%i_op = znz_digits (nmake_op0 %i).\n" i i i; + fprintf fmt " rewrite make_th4; unfold w%i_op.\n" i; + fprintf fmt " exact_no_check (digits_th1 _ _ _ digits_%i).\n" (i - 1); + fprintf fmt " Qed.\n"; + fprintf fmt "\n"; + fprintf fmt " Theorem nmake_%i: znz_to_Z w%i_op = znz_to_Z (nmake_op0 %i).\n" i i i; + fprintf fmt " rewrite make_th4; unfold w%i_op.\n" i; + fprintf fmt " exact_no_check (make_th1 _ _ _ digits_%i nmake_%i).\n" (i - 1) (i -1); + fprintf fmt " Qed.\n"; + done; + + + fprintf fmt " Theorem digits_gend:forall n ww (w_op: znz_op ww), \n"; + fprintf fmt " znz_digits (nmake_op _ w_op n) = \n"; + fprintf fmt " GenBase.gen_digits (znz_digits w_op) n.\n"; + fprintf fmt " Proof."; + fprintf fmt " intros n; elim n; auto; clear n.\n"; + fprintf fmt " intros n Hrec ww ww_op; simpl GenBase.gen_digits.\n"; + fprintf fmt " rewrite <- Hrec; auto.\n"; + fprintf fmt " Qed.\n"; + fprintf fmt "\n"; + fprintf fmt " Theorem nmake_gen: forall n ww (w_op: znz_op ww), \n"; + fprintf fmt " znz_to_Z (nmake_op _ w_op n) =\n"; + fprintf fmt " %sGenBase.gen_to_Z _ (znz_digits w_op) (znz_to_Z w_op) n.\n" "@"; + fprintf fmt " Proof."; + fprintf fmt " intros n; elim n; auto; clear n.\n"; + fprintf fmt " intros n Hrec ww ww_op; simpl GenBase.gen_to_Z; unfold zn2z_to_Z.\n"; + fprintf fmt " rewrite <- Hrec; auto.\n"; + fprintf fmt " unfold GenBase.gen_wB; rewrite <- digits_gend; auto.\n"; + fprintf fmt " Qed.\n"; + fprintf fmt "\n"; + + + + fprintf fmt " Theorem digits_clean: forall ww (w_op1 w_op2: znz_op ww) n, \n"; + fprintf fmt " znz_digits w_op1 = znz_digits w_op2 ->\n"; + fprintf fmt " znz_digits (nmake_op _ w_op1 n) = znz_digits (nmake_op _ w_op2 n).\n"; + fprintf fmt " Proof.\n"; + fprintf fmt " intros ww w_op1 w_op2 n; elim n; auto; clear n.\n"; + fprintf fmt " intros n Hrec H1.\n"; + fprintf fmt " simpl; unfold zn2z_to_Z; rewrite Hrec; auto.\n"; + fprintf fmt " Qed.\n"; + fprintf fmt " \n"; + fprintf fmt " Theorem nmake_clean: forall ww (w_op1 w_op2: znz_op ww) n, \n"; + fprintf fmt " znz_digits w_op1 = znz_digits w_op2 ->\n"; + fprintf fmt " znz_to_Z w_op1 = znz_to_Z w_op2 ->\n"; + fprintf fmt " znz_to_Z (nmake_op _ w_op1 n) =\n"; + fprintf fmt " znz_to_Z (nmake_op _ w_op2 n).\n"; + fprintf fmt " Proof.\n"; + fprintf fmt " intros ww w_op1 w_op2 n; elim n; auto; clear n.\n"; + fprintf fmt " intros n Hrec H1 H2.\n"; + fprintf fmt " generalize (digits_clean _ _ _ n H1).\n"; + fprintf fmt " simpl; unfold zn2z_to_Z; intros H3.\n"; + fprintf fmt " rewrite Hrec; auto; rewrite H3; auto.\n"; + fprintf fmt " Qed.\n"; + fprintf fmt " \n"; end; + (* Comparison *) + fprintf fmt " Theorem spec_compare: forall x y,\n"; + fprintf fmt " match compare x y with \n"; + fprintf fmt " Eq => [x] = [y]\n"; + fprintf fmt " | Lt => [x] < [y]\n"; + fprintf fmt " | Gt => [x] > [y]\n"; + fprintf fmt " end.\n"; + fprintf fmt " Proof.\n"; + if gen_proof then + begin + for i= 0 to size do + fprintf fmt " assert(F1_%i:= (spec_0 w%i_spec)).\n" i i; + fprintf fmt " assert(F2_%i:= (spec_compare w%i_spec (znz_0 w%i_op))).\n" i i i; + fprintf fmt " assert(F3_%i:= (spec_to_Z w%i_spec)).\n" i i; + fprintf fmt " assert(F4_%i:= (spec_compare w%i_spec)).\n" i i; + done; + fprintf fmt " intros x; case x; clear x; unfold compare, to_Z.\n"; + for i = 0 to size do + fprintf fmt " intros x y; case y; clear y; auto.\n"; + for j = 0 to i - 1 do + fprintf fmt " intros y; unfold comparen_%i, w_0, compare_%i.\n" j j; + fprintf fmt " replace (znz_to_Z w%i_op x) with (%sGenBase.gen_to_Z w%i (znz_digits w%i_op) (znz_to_Z w%i_op) %i x).\n" i "@" j j j (i -j); + fprintf fmt " apply spec_compare_mn_1; auto.\n"; + fprintf fmt " rewrite <- nmake_gen; rewrite nmake_%i. \n" i; + if (i == 0) || (j == 0) then + fprintf fmt " unfold nmake_op0; auto.\n" + else + begin + fprintf fmt " replace (nmake_op0 %i) with (nmake_op _ (nmake_op0 %i) %i).\n" i j (i-j); + fprintf fmt " apply cancel_app.\n"; + fprintf fmt " exact (nmake_clean _ _ _ %i digits_%i nmake_%i).\n" (i - j) j j; + fprintf fmt " unfold nmake_op0, nmake_op; auto.\n"; + end; + + done; + fprintf fmt " exact (spec_compare w%i_spec x).\n" i; + for j = i + 1 to size do + fprintf fmt " intros y; apply spec_opp; unfold comparen_%i, w_0, compare_%i.\n" i i; + fprintf fmt " replace (znz_to_Z w%i_op y) with (%sGenBase.gen_to_Z w%i (znz_digits w%i_op) (znz_to_Z w%i_op) %i y). \n" j "@" i i i (j - i); + fprintf fmt " apply spec_compare_mn_1; auto.\n"; + fprintf fmt " rewrite <- nmake_gen; rewrite nmake_%i.\n" j; + if (i == 0) then + fprintf fmt " unfold nmake_op0; auto.\n" + else + begin + fprintf fmt " replace (nmake_op0 %i) with (nmake_op _ (nmake_op0 %i) %i).\n" j i (j - i); + fprintf fmt " apply cancel_app.\n"; + fprintf fmt " exact (nmake_clean _ _ _ %i digits_%i nmake_%i).\n" (j - i) i i; + fprintf fmt " unfold nmake_op0, nmake_op; auto.\n"; + end; + done; + fprintf fmt " intros n y; apply spec_opp; unfold comparen_%i, w%i, w_0, compare_0.\n" i i; + fprintf fmt " rewrite <- gen_make.\n"; + fprintf fmt " apply spec_compare_mn_1; auto.\n"; + if i <> size then + begin + fprintf fmt " try rewrite (spec_0 w%i_spec); auto.\n" i; + fprintf fmt " intros x1 y1.\n"; + fprintf fmt " replace (znz_to_Z w%i_op x1) with (%sGenBase.gen_to_Z w%i (znz_digits w%i_op) (znz_to_Z w%i_op) %i x1).\n" size "@" i i i (size - i); + fprintf fmt " apply spec_compare_mn_1; auto.\n"; + fprintf fmt " rewrite <- nmake_gen; rewrite nmake_%i.\n" size; + if (i == 0) then + fprintf fmt " unfold nmake_op0; auto.\n" + else + begin + fprintf fmt " replace (nmake_op0 %i) with (nmake_op _ (nmake_op0 %i) %i).\n" size i (size - i); + fprintf fmt " apply cancel_app.\n"; + fprintf fmt " exact (nmake_clean _ _ _ %i digits_%i nmake_%i).\n" (size - i) i i; + fprintf fmt " unfold nmake_op0, nmake_op; auto.\n"; + end; + fprintf fmt " intros x1; case (F3_%i x1); split; auto.\n" i; + fprintf fmt " apply Zlt_trans with (1 := H0); unfold base; apply ZPowerAux.Zpower_lt_monotone.\n"; + fprintf fmt " auto with zarith.\n"; + fprintf fmt " split; [red; intro HH; discriminate HH | idtac].\n"; + fprintf fmt " apply length_pos_lt.\n"; + fprintf fmt " change (length_pos (znz_digits w%i_op)) with\n" size; + fprintf fmt " (S(%i + (length_pos (znz_digits w%i_op))))%snat.\n" (size - i - 1) i "%"; + fprintf fmt " apply le_lt_n_Sm; apply le_plus_r.\n"; + end; + done; + fprintf fmt " intros n x y; case y; clear y.\n"; + for i = 0 to size do + fprintf fmt " intros y; rewrite <- gen_make; unfold comparen_%i; apply spec_compare_mn_1; auto.\n" i; + if i <> size then + begin + fprintf fmt " unfold w_0; try rewrite (spec_0 w%i_spec); auto.\n" i; + fprintf fmt " intros x1 y1.\n"; + fprintf fmt " replace (znz_to_Z w%i_op x1) with (%sGenBase.gen_to_Z w%i (znz_digits w%i_op) (znz_to_Z w%i_op) %i x1).\n" size "@" i i i (size - i); + fprintf fmt " apply spec_compare_mn_1; auto.\n"; + fprintf fmt " rewrite <- nmake_gen; rewrite nmake_%i.\n" size; + if (i == 0) then + fprintf fmt " unfold nmake_op0; auto.\n" + else + begin + fprintf fmt " replace (nmake_op0 %i) with (nmake_op _ (nmake_op0 %i) %i).\n" size i (size - i); + fprintf fmt " apply cancel_app.\n"; + fprintf fmt " exact (nmake_clean _ _ _ %i digits_%i nmake_%i).\n" (size - i) i i; + fprintf fmt " unfold nmake_op0, nmake_op; auto.\n"; + end; + fprintf fmt " intros x1; case (F3_%i x1); split; auto.\n" i; + fprintf fmt " apply Zlt_trans with (1 := H0); unfold base; apply ZPowerAux.Zpower_lt_monotone.\n"; + fprintf fmt " auto with zarith.\n"; + fprintf fmt " split; [red; intro HH; discriminate HH | idtac].\n"; + fprintf fmt " apply length_pos_lt.\n"; + fprintf fmt " change (length_pos (znz_digits w%i_op)) with\n" size; + fprintf fmt " (S(%i + (length_pos (znz_digits w%i_op))))%snat.\n" (size - i - 1) i "%"; + fprintf fmt " apply le_lt_n_Sm; apply le_plus_r.\n"; + end + done; + fprintf fmt " intros m y.\n"; + fprintf fmt " generalize (spec_cast_l n m x); simpl to_Z; simpl word; intros HH; rewrite <- HH; clear HH.\n"; + fprintf fmt " generalize (spec_cast_r n m y); simpl to_Z; simpl word; intros HH; rewrite <- HH; clear HH.\n"; + fprintf fmt " apply (spec_compare (wn_spec (Max.max n m))).\n"; + fprintf fmt " Qed.\n"; + end else + fprintf fmt " Admitted.\n"; + fprintf fmt "\n"; + fprintf fmt "End Make.\n"; fprintf fmt "\n"; pp_print_flush fmt () |