From 0ed668481dbaaae8e4c9fa4aa31f225c246b158e Mon Sep 17 00:00:00 2001
From: Adam Chlipala <adam@chlipala.net>
Date: Sat, 8 Feb 2020 14:56:10 -0500
Subject: [PATCH] Some N-related library content contributed by Sam Gruetter

---
 FrapWithoutSets.v | 69 +++++++++++++++++++++++++++++++++++++++++++----
 1 file changed, 64 insertions(+), 5 deletions(-)

diff --git a/FrapWithoutSets.v b/FrapWithoutSets.v
index 1ffda1f..31568e8 100644
--- a/FrapWithoutSets.v
+++ b/FrapWithoutSets.v
@@ -1,4 +1,4 @@
-Require Import Eqdep String Arith Lia Program Sets Relations Map Var Invariant Bool ModelCheck.
+Require Import Eqdep String NArith Arith Lia Program Sets Relations Map Var Invariant Bool ModelCheck.
 Export Ascii String Arith Sets Relations Map Var Invariant Bool ModelCheck.
 Require Import List.
 Export List ListNotations.
@@ -98,7 +98,25 @@ Ltac instantiate_obviouses :=
          | [ H : _ |- _ ] => instantiate_obvious H
          end.
 
-Ltac induct e := (inductN e || dependent induction e); instantiate_obviouses.
+(** * Interlude: special notations and induction principle for [N] *)
+
+(* Note: recurse is an identifier, but we will always use the name "recurse" by convention *)
+Declare Scope N_recursion_scope.
+Notation "recurse 'by' 'cases' | 0 => A | n + 1 => B 'end'" :=
+  (N.recursion A (fun n recurse => B))
+  (at level 11, A at level 200, n at level 0, B at level 200,
+   format "'[hv' recurse  'by'  'cases' '//' '|'  0  =>  A '//' '|'  n  +  1  =>  B '//' 'end' ']'")
+: N_recursion_scope.
+
+Open Scope N_recursion_scope.
+
+Lemma indN: forall (P: N -> Prop),
+    P 0%N ->                                 (* base case to prove *)
+    (forall n: N, P n -> P (n + 1)%N) ->     (* inductive case to prove *)
+    forall n, P n.                           (* conclusion to enjoy *)
+Proof. setoid_rewrite N.add_1_r. exact N.peano_ind. Qed.
+
+Ltac induct e := (induction e using indN || inductN e || dependent induction e); instantiate_obviouses.
 
 Ltac invert' H := inversion H; clear H; subst.
 
@@ -335,9 +353,9 @@ Inductive ordering (n m : nat) :=
 | Eq (_ : n = m)
 | Gt (_ : n > m).
 
-Local Hint Constructors ordering.
-Local Hint Extern 1 (_ < _) => lia.
-Local Hint Extern 1 (_ > _) => lia.
+Local Hint Constructors ordering : core.
+Local Hint Extern 1 (_ < _) => lia : core.
+Local Hint Extern 1 (_ > _) => lia : core.
 
 Theorem totally_ordered : forall n m, ordering n m.
 Proof.
@@ -409,3 +427,44 @@ Ltac dep_cases E :=
       try match goal with
             | [ H : _ = E |- _ ] => try rewrite <- H in *; clear H
           end.
+
+(** * More with [N] *)
+
+Lemma recursion_step: forall {A: Type} (a: A) (f: N -> A -> A) (n: N),
+    N.recursion a f (n + 1) = f n (N.recursion a f n).
+Proof.
+  intros until f. setoid_rewrite N.add_1_r.
+  eapply N.recursion_succ; cbv; intuition congruence.
+Qed.
+
+Ltac head f :=
+  match f with
+  | ?g _ => head g
+  | _ => constr:(f)
+  end.
+
+(* If a function f is defined as
+
+  recurse by cases
+  | 0 => base
+  | k + 1 => step recurse k
+  end.
+
+  and we have an occurrence of (f (k + 1)) in our goal, we can use
+  "unfold_recurse f k" to replace (f (k + 1)) by (step (f k) k),
+  ie it allows us to unfold one recursive step. *)
+Ltac unfold_recurse f k :=
+  let h := head f in
+  let rhs := eval unfold h in f in
+  lazymatch rhs with
+  | N.recursion ?base ?step =>
+    let g := eval cbv beta in (step k (f k)) in
+    rewrite (recursion_step base step k : f (k + 1) = g) in *
+  | _ => let expected := open_constr:(N.recursion _ _) in
+         fail "The provided term" f "expands to" rhs "which is not of the expected form" expected
+  end.
+
+(* This will make "simplify" a bit less nice in some cases (but these are easily worked around using
+   linear_arithmetic). *)
+Arguments N.mul: simpl never.
+Arguments N.add: simpl never.