Add Z.peano_rect_strong

This version provides hypotheses about the non{negativity,positivity} of the Z.

1 files changed, 43 insertions, 13 deletions

diff --git a/src/Util/ZUtil/Peano.v b/src/Util/ZUtil/Peano.v
index 262d757ce..d0ba81ef4 100644
--- a/src/Util/ZUtil/Peano.v
+++ b/src/Util/ZUtil/Peano.v
@@ -2,6 +2,8 @@
 Require Import Coq.micromega.Lia.
 Require Import Coq.ZArith.BinInt.
 Require Import Crypto.Util.Tactics.BreakMatch.
+Require Import Crypto.Util.HProp.
+Require Import Crypto.Util.Decidable.
 
 Local Open Scope Z_scope.
 Module Z.
@@ -32,6 +34,44 @@ Module Z.
     rewrite Pos.add_1_r; reflexivity.
   Qed.
 
+  Section rect_strong.
+    Context (P : Z -> Type)
+            (P0 : P 0)
+            (Psucc : forall z, z = 0 \/ 0 < z -> P z -> P (Z.succ' z))
+            (Ppred : forall z, z = 0 \/ z < 0 -> P z -> P (Z.pred' z)).
+
+    Definition peano_rect_strong z : P z
+      := match z return P z with
+         | 0 => P0
+         | Z.pos x => Pos.peano_rect (fun p => P (Z.pos p)) (Psucc _ (or_introl eq_refl) P0) (fun p => Psucc (Z.pos p) (or_intror (Pos2Z.is_pos _))) x
+         | Z.neg x => Pos.peano_rect (fun p => P (Z.neg p)) (Ppred _ (or_introl eq_refl) P0) (fun p => Ppred (Z.neg p) (or_intror (Pos2Z.neg_is_neg _))) x
+         end.
+
+    Local Ltac peano_rect_t :=
+      repeat first [ progress unfold peano_rect_strong
+                   | progress simpl
+                   | reflexivity
+                   | exfalso; lia
+                   | rewrite Pos.peano_rect_succ
+                   | progress f_equal; []
+                   | match goal with
+                     | [ |- ?x = ?y :> (_ < _) ]
+                       => apply allpath_hprop
+                     end ].
+    Lemma peano_rect_strong_base
+      : peano_rect_strong 0 = P0.
+    Proof. reflexivity. Qed.
+    Lemma peano_rect_strong_succ z (pf : z = 0 \/ 0 < z)
+      : peano_rect_strong (Z.succ' z) = Psucc z pf (peano_rect_strong z).
+    Proof.
+      destruct pf; [ subst | destruct z]; peano_rect_t.
+    Qed.
+    Lemma peano_rect_strong_pred z (pf : z = 0 \/ z < 0)
+      : peano_rect_strong (Z.pred' z) = Ppred z pf (peano_rect_strong z).
+    Proof.
+      destruct pf; [ subst | destruct z]; peano_rect_t.
+    Qed.
+  End rect_strong.
   Section rect.
     Context (P : Z -> Type)
             (P0 : P 0)
@@ -39,11 +79,7 @@ Module Z.
             (Ppred : forall z, P z -> P (Z.pred' z)).
 
     Definition peano_rect z : P z
-      := match z return P z with
-         | 0 => P0
-         | Z.pos x => Pos.peano_rect (fun p => P (Z.pos p)) (Psucc _ P0) (fun p => Psucc (Z.pos p)) x
-         | Z.neg x => Pos.peano_rect (fun p => P (Z.neg p)) (Ppred _ P0) (fun p => Ppred (Z.neg p)) x
-         end.
+      := peano_rect_strong P P0 (fun z pf => Psucc z) (fun z pf => Ppred z) z.
 
     Lemma peano_rect_base
       : peano_rect 0 = P0.
@@ -51,18 +87,12 @@ Module Z.
     Lemma peano_rect_succ z
       : 0 <= z -> peano_rect (Z.succ' z) = Psucc z (peano_rect z).
     Proof.
-      unfold peano_rect; destruct z; simpl; try reflexivity;
-        rewrite ?Pos.peano_rect_succ;
-        try reflexivity.
-      intro; exfalso; lia.
+      unfold peano_rect; intro; erewrite peano_rect_strong_succ by lia; reflexivity.
     Qed.
     Lemma peano_rect_pred z
       : z <= 0 -> peano_rect (Z.pred' z) = Ppred z (peano_rect z).
     Proof.
-      unfold peano_rect; destruct z; simpl; try reflexivity;
-        rewrite ?Pos.peano_rect_succ;
-        try reflexivity.
-      intro; exfalso; lia.
+      unfold peano_rect; intro; erewrite peano_rect_strong_pred by lia; reflexivity.
     Qed.
   End rect.
 End Z.