Remove duplicate lemma.

examples/in_progress/mp.mlw

@@ -190,17 +190,10 @@ module N
   = assert   { value_sub x x1 x2 = value_sub x x1 (x2-1)
                + power radix (x2-x1-1) * l2i (Map.get x (x2-1)) }
 
-  let rec lemma value_sub_upper_bound_tight (x:map int limb) (x1 x2:int)
-    requires { x1 <= x2 }
-    variant  { x2 - x1 }
-    ensures  { value_sub x x1 x2 < power radix (x2-x1)  }
-  = if x1 = x2 then () else
-    value_sub_upper_bound_tight x x1 (x2-1)
-
-  let lemma value_sub_upper_bound_tighter (x:map int limb) (x1 x2:int)
+  let lemma value_sub_upper_bound_tight (x:map int limb) (x1 x2:int)
     requires { x1 < x2 }
     ensures  { value_sub x x1 x2 < power radix (x2-x1-1) *  (l2i (Map.get x (x2-1)) + 1) }
-  = value_sub_upper_bound_tight x x1 (x2-1)
+  = value_sub_upper_bound x x1 (x2-1)
 
   exception Break31 int31
 

examples/in_progress/mp/mp_N_WP_parameter_mul_1.v

@@ -164,11 +164,7 @@ Axiom value_sub_lower_bound_tight : forall (x:(map.Map.map Z uint32)) (x1:Z)
   (x2 - 1%Z)%Z)))%Z <= (value_sub x x1 x2))%Z.
 
 Axiom value_sub_upper_bound_tight : forall (x:(map.Map.map Z uint32)) (x1:Z)
-  (x2:Z), (x1 <= x2)%Z -> ((value_sub x x1
-  x2) < (int.Power.power (4294967295%Z + 1%Z)%Z (x2 - x1)%Z))%Z.
-
-Axiom value_sub_upper_bound_tighter : forall (x:(map.Map.map Z uint32))
-  (x1:Z) (x2:Z), (x1 < x2)%Z -> ((value_sub x x1
+  (x2:Z), (x1 < x2)%Z -> ((value_sub x x1
   x2) < ((int.Power.power (4294967295%Z + 1%Z)%Z
   ((x2 - x1)%Z - 1%Z)%Z) * ((to_int1 (map.Map.get x
   (x2 - 1%Z)%Z)) + 1%Z)%Z)%Z)%Z.
@@ -222,8 +218,8 @@ revert h28.
 rewrite h6, 2!Zminus_0_r, Power.Power_0, Zmult_1_l.
 rewrite h14, h18, 2!Zplus_0_l.
 intros H1.
-assert (H2 := value_sub_upper_bound_tight x1 0 (to_int x) h1).
-assert (H3 := value_sub_upper_bound_tight y1 0 (to_int y) h2).
+assert (H2 := value_sub_upper_bound x1 0 (to_int x) h1).
+assert (H3 := value_sub_upper_bound y1 0 (to_int y) h2).
 rewrite Zminus_0_r in H2, H3.
 refine (_ (Zmult_lt_compat _ _ _ _ (conj _ H2) (conj _ H3))).
 apply Z.le_ngt.