zify Nat.double and Nat.div2

[andres-erbsen]

I just coached a new Coq user to work around this incompleteness; it didn't leave a good impression.

• Added changelog.
• Opened overlay pull requests
  • cross-crypto
    • FCF
  • tlc
  • flocq
  • neural-net-interp

[andres-erbsen]

The added change in stdlib is only needed until #18730 is merged, to retain zify's ability to see that Nat.div2 returns non-negative values.

[andres-erbsen]

@coqbot run full ci

[coqbot-app]

🔴 CI failures at commit 2f227a4 without any failure in the test-suite

✔️ Corresponding jobs for the base commit 139b6ce succeeded

❔ Ask me to try to extract minimal test cases that can be added to the test-suite

🏃 @coqbot ci minimize will minimize the following targets: ci-flocq, ci-neural_net_interp, ci-perennial

• You can also pass me a specific list of targets to minimize as arguments.

⚠️ ⌛ You may want to wait until the pipeline for the base commit (139b6ce) finishes.

[andres-erbsen]

@silene would you be willing to port Flocq over this change? Below is a draft patch that gets Flocq to build with this PR, but it probably isn't backwards compatible in a couple of proofs due to increased power of lia. I believe all of these should be fixable, but not understanding the proofs I could only do an ugly hack job myself.

commit f98c1989c49b72d40e78c85dcab51654d6df849d
Author: Andres Erbsen <andres-github@andres.systems>
Date:   Sat Mar 2 01:25:33 2024 +0000

    port over coq/coq#18729 (wont work on baseline)

diff --git a/src/Calc/Div.v b/src/Calc/Div.v
index 718ccae..c335309 100644
--- a/src/Calc/Div.v
+++ b/src/Calc/Div.v
@@ -73,6 +73,7 @@ Theorem Fdiv_core_correct :
   let '(m, l) := Fdiv_core m1 e1 m2 e2 e in
   inbetween_float beta m e (F2R (Float beta m1 e1) / F2R (Float beta m2 e2)) l.
 Proof.
+clear fexp.
 intros m1 e1 m2 e2 e Hm1 Hm2.
 unfold Fdiv_core.
 match goal with |- context [if ?b then ?b1 else ?b2] => set (m12 := if b then b1 else b2) end.
diff --git a/src/Calc/Sqrt.v b/src/Calc/Sqrt.v
index 0e2b822..02ca0c6 100644
--- a/src/Calc/Sqrt.v
+++ b/src/Calc/Sqrt.v
@@ -77,6 +77,7 @@ Theorem Fsqrt_core_correct :
   let '(m, l) := Fsqrt_core m1 e1 e in
   inbetween_float beta m e (sqrt (F2R (Float beta m1 e1))) l.
 Proof.
+clear fexp.
 intros m1 e1 e Hm1 He.
 unfold Fsqrt_core.
 set (m' := Zmult _ _).
diff --git a/src/Pff/Pff.v b/src/Pff/Pff.v
index e058003..5046292 100644
--- a/src/Pff/Pff.v
+++ b/src/Pff/Pff.v
@@ -17514,33 +17514,11 @@ Hypothesis D5: (Closest b radix (t3-x2y2)%R  t4).
 
 Lemma SLe: (2 <= s).
 unfold s; auto with zarith.
-assert (2<= t-Nat.div2 t)%Z; auto with zarith.
-apply Zmult_le_reg_r with 2%Z; try lia.
-replace ((t-Nat.div2 t)*2)%Z with (2*t-2*Nat.div2 t)%Z by ring.
-replace (2*Nat.div2 t)%Z with (Z_of_nat (Nat.double (Nat.div2 t))).
-case (Nat.Even_or_Odd t); intros I.
-rewrite <- Even_double by easy. lia.
-apply Z.le_trans with (2*t+1-(S ( Nat.double (Nat.div2 t))))%Z; try lia.
-rewrite <- Odd_double by easy. lia.
-unfold Nat.double; rewrite inj_plus; ring.
 Qed.
 
 
 Lemma SGe: (s <= t-2).
-unfold s.
-cut (2<= Nat.div2 t)%Z. lia.
-apply Zmult_le_reg_r with 2%Z; try lia.
-replace (Nat.div2 t*2)%Z with (Z_of_nat (Nat.double (Nat.div2 t))).
-case (Nat.Even_or_Odd t); intros I.
-rewrite <- Even_double by easy. lia.
-apply Z.le_trans with (-1+(S ( Nat.double (Nat.div2 t))))%Z. 2: lia.
-rewrite <- Odd_double; auto with zarith.
-case (Zle_lt_or_eq 4 t); auto with zarith.
-intros I2; absurd (Nat.Odd t); auto.
-intros I3; apply Nat.Even_Odd_False with t; auto.
-replace t with (4) by auto with zarith.
-now exists 2.
-unfold Nat.double; rewrite inj_plus; ring.
+unfold s. nia.
 Qed.
 
 Lemma s2Ge: (t <= s + s)%Z.
@@ -17558,18 +17536,7 @@ Qed.
 
 
 Lemma s2Le: (s + s <= t + 1)%Z.
-unfold s.
-rewrite inj_minus1; auto with zarith.
-2: generalize (Nat.lt_div2 t); auto with zarith.
-assert (t<= 2*(Nat.div2 t)+1)%Z; auto with zarith.
-case (Nat.Even_or_Odd t); intros I.
-apply Z.le_trans with  ((Nat.double (Nat.div2 t)+1))%Z.
-2:unfold Nat.double; rewrite inj_plus; auto with zarith.
-rewrite <- Even_double; auto with zarith.
-apply Z.le_trans with ((S ( Nat.double (Nat.div2 t))))%Z; auto with zarith.
-2: rewrite inj_S; unfold Z.succ; auto with zarith.
-2: unfold Nat.double; rewrite inj_plus; auto with zarith.
-rewrite <- Odd_double; auto with zarith.
+unfold s. nia.
 Qed.
 
 
@@ -17722,8 +17689,8 @@ apply Zmult_lt_compat_l; auto with zarith.
 intros I; rewrite <- I.
 rewrite Zmult_0_l; apply Z.mul_pos_pos; apply Zpower_nat_less; lia.
 rewrite pGivesBound; rewrite <- Zpower_nat_is_exp; auto with zarith.
-apply Zpower_nat_monotone_le; auto with zarith.
-generalize s2Le; auto with zarith.
+apply Zpower_nat_monotone_le; auto with zarith;
+try solve [generalize s2Le; auto with zarith].
 apply sym_eq; unfold vNum in |- *.
 apply
  trans_eq
@@ -17902,19 +17869,19 @@ fold FtoRradix in H'; rewrite Z3 in H'; rewrite <- Ny in H'; auto with real.
 apply trans_eq with (0+ty)%R; auto with real.
 unfold s; apply SLe; auto.
 unfold s; apply SGe; auto.
-right; auto.
-elim Veltkamp with radix b s t y p' q' hy; auto with zarith arith.
-2: apply SLe; auto.
-2: apply SGe; auto.
-2: elim Cy; auto.
+right; auto. {
+elim Veltkamp with radix b s t y p' q' hy; auto with zarith arith;
+try solve [ apply SLe; auto];
+try solve [ apply SGe; auto];
+try solve [ elim Cy; auto].
 intros T1 T; elim T; intros hy' T'; elim T'; intros G1 T''; elim T''; intros ; clear T1 T T' T''.
 unfold FtoRradix; rewrite <- G1.
  apply ClosestZero with (Bound (P_of_succ_nat (pred (Z.abs_nat (Zpower_nat radix (t - s)))))
                                (dExp b)) (t-s) (FtoR radix y)%R; auto with zarith.
-apply p'GivesBound; solve [auto with zarith].
+apply p'GivesBound; solve [auto with zarith]. }
 cut (s <= t-2) ;[idtac | apply SGe; auto].
-unfold s; auto with zarith.
-unfold FtoRradix; apply ClosestZero with b t (x*y)%R; auto with zarith.
+unfold s; auto with zarith; intros.
+unfold FtoRradix. apply ClosestZero with b t (x*y)%R; auto with zarith.
 rewrite <- Ny; ring.
 elim bimplybplusNorm with radix b s t y; auto.
 2: unfold s; apply SLe; auto.
@@ -18165,7 +18132,7 @@ unfold FtoRradix; rewrite <- G1.
  apply ClosestZero with (Bound (P_of_succ_nat (pred (Z.abs_nat (Zpower_nat radix (t - s)))))
             (dExp b)) (t-s) (FtoR radix x)%R; auto with zarith.
 apply p'GivesBound; auto with zarith.
-cut  (s <= t - 2); [unfold s; auto with zarith| apply SGe; auto].
+cut  (s <= t - 2); [unfold s; auto with zarith; intros| apply SGe; auto].
 unfold FtoRradix; apply ClosestZero with b t (x*y)%R; auto with zarith.
 rewrite <- Ny; ring.
 elim bimplybplusNorm with radix b s t x; auto.
@@ -18858,7 +18825,7 @@ unfold FtoRradix; rewrite <- G1.
 apply ClosestZero with (Bound (P_of_succ_nat (pred (Z.abs_nat (Zpower_nat radix (t - s)))))
             (dExp b)) (t-s) (FtoR radix x)%R; auto with zarith.
 apply p'GivesBound; auto with zarith.
-cut (s <= t-2); [unfold s; auto with zarith | apply SGe; auto].
+cut (s <= t-2); [unfold s; auto with zarith; intros | apply SGe; auto].
 unfold FtoRradix; apply ClosestZero with b t (x*y)%R; auto with zarith.
 rewrite <- Ny; ring.
 case (Req_dec 0%R y); intros Nx.
@@ -18909,7 +18876,7 @@ unfold FtoRradix; rewrite <- G1.
 apply ClosestZero with (Bound (P_of_succ_nat (pred (Z.abs_nat (Zpower_nat radix (t - s)))))
             (dExp b)) (t-s) (FtoR radix y)%R; auto with zarith.
 apply p'GivesBound; auto with zarith.
-cut (s <= t-2); [unfold s; auto with zarith | apply SGe; auto].
+cut (s <= t-2); [unfold s; auto with zarith; intros | apply SGe; auto].
 unfold FtoRradix; apply ClosestZero with b t (x*y)%R; auto with zarith.
 rewrite <- Nx; ring.
 apply Dekker2_aux; auto.
diff --git a/src/Pff/Pff2Flocq.v b/src/Pff/Pff2Flocq.v
index 6691ff2..5ce37cb 100644
--- a/src/Pff/Pff2Flocq.v
+++ b/src/Pff/Pff2Flocq.v
@@ -903,11 +903,11 @@ assert (TT: (Z.div2 prec = Nat.div2 (Z.abs_nat prec))%Z).
 rewrite Nat.div2_div, Z.div2_div, Nat2Z.inj_div; simpl.
 rewrite inj_abs; lia.
 rewrite <- TT.
-rewrite inj_abs; try lia.
-rewrite Z.max_r; try lia.
-assert (Z.div2 prec <= prec)%Z; try lia.
-rewrite Z.div2_div; apply Zlt_le_weak.
-apply Z_div_lt; lia.
+rewrite inj_abs; try lia;
+try rewrite Z.max_r; try lia;
+assert (Z.div2 prec <= prec)%Z; try lia;
+try rewrite Z.div2_div; try apply Zlt_le_weak;
+try apply Z_div_lt; lia.
 (* *)
 assert (D:(((- dExp (make_bound beta prec emin) <= Pff.Fexp fx + Pff.Fexp fy)%Z ->
         (FtoR beta fx * FtoR beta fy = FtoR beta fr + FtoR beta ft4)) /\
diff --git a/src/Prop/Relative.v b/src/Prop/Relative.v
index 1925e7b..77cdd22 100644
--- a/src/Prop/Relative.v
+++ b/src/Prop/Relative.v
@@ -504,6 +504,7 @@ Proof. apply Rmult_le_pos; [lra|apply bpow_ge_0]. Qed.
 
 Lemma u_ro_lt_1 : (u_ro < 1)%R.
 Proof.
+clear choice.
 unfold u_ro; apply (Rmult_lt_reg_l 2); [lra|].
 rewrite <-Rmult_assoc, Rinv_r, Rmult_1_l, Rmult_1_r; [|lra].
 apply (Rle_lt_trans _ (bpow 0));

[andres-erbsen]

@coqbot run full ci

[andres-erbsen]

@coqbot run full ci

[coqbot-app]

🔴 CI failure at commit 8c8c7bb without any failure in the test-suite

✔️ Corresponding job for the base commit d2c3b06 succeeded

❔ Ask me to try to extract a minimal test case that can be added to the test-suite

🏃 @coqbot ci minimize will minimize the following target: ci-flocq

• You can also pass me a specific list of targets to minimize as arguments.

[andres-erbsen]

@coq/micromega-maintainers I think this PR is ready.

Mtac2 failure is unrelated (in an mlg file). Here is an updated backwards-compatible patch for flocq (@silene please apply):

diff --git a/src/Pff/Pff.v b/src/Pff/Pff.v
index e058003..0d9c9a7 100644
--- a/src/Pff/Pff.v
+++ b/src/Pff/Pff.v
@@ -17551,7 +17551,7 @@ apply Z.le_trans with  (Nat.double (Nat.div2 t)).
 unfold Nat.double; rewrite inj_plus; auto with zarith.
 rewrite <- Even_double; auto with zarith.
 apply Z.le_trans with (-1+(S ( Nat.double (Nat.div2 t))))%Z.
-rewrite inj_S; unfold Z.succ; auto with zarith.
+rewrite inj_S; unfold Z.succ; auto with zarith;
 unfold Nat.double; rewrite inj_plus; auto with zarith.
 rewrite <- Odd_double by easy. lia.
 Qed.
@@ -17566,9 +17566,9 @@ case (Nat.Even_or_Odd t); intros I.
 apply Z.le_trans with  ((Nat.double (Nat.div2 t)+1))%Z.
 2:unfold Nat.double; rewrite inj_plus; auto with zarith.
 rewrite <- Even_double; auto with zarith.
-apply Z.le_trans with ((S ( Nat.double (Nat.div2 t))))%Z; auto with zarith.
-2: rewrite inj_S; unfold Z.succ; auto with zarith.
-2: unfold Nat.double; rewrite inj_plus; auto with zarith.
+apply Z.le_trans with ((S ( Nat.double (Nat.div2 t))))%Z; auto with zarith;
+try solve [rewrite inj_S; unfold Z.succ; auto with zarith;
+  unfold Nat.double; rewrite inj_plus; auto with zarith].
 rewrite <- Odd_double; auto with zarith.
 Qed.
 

[fajb]

I can merge when the flocq patch is applied. @silene don't hesitate to ping @fajb

[silene]

Done.

[fajb]

Thanks @silene

@coqbot: merge now

[coqbot-app]

@fajb: You cannot merge this PR because:

• There is no kind: label.

[fajb]

@coqbot: merge now

[fajb]

Thanks @andres-erbsen