Make `NatCancel` no backtracking and puts its internals in a module.

theories/nat_cancel.v

@@ -25,62 +25,78 @@ Results in:
 
 The instances are setup up so that canceling is performed in two stages.
 
-- In the first stage, using the class [NatCancel], it traverses [m] w.r.t. [S]
+- In the first stage, using the class [NatCancelL], it traverses [m] w.r.t. [S]
   and [+].
 - In the second stage, for each leaf (i.e. a constant or arbitrary term)
-  obtained by the traversal in stage 1, it uses the class [NatCancelLeaf] to
+  obtained by the traversal in stage 1, it uses the class [NatCancelR] to
   cancel the leaf in [n].
 
 Be warned: Since the canceler is implemented using type classes it should only
 be used it either of the inputs is relatively small. For bigger inputs, an
 approach based on reflection would be better, but for small inputs, the overhead
 of reification will probably not be worth it. *)
+
 Class NatCancel (m n m' n' : nat) := nat_cancel : m' + n = m + n'.
 Hint Mode NatCancel ! ! - - : typeclass_instances.
-Class NatCancelLeaf (m n m' n' : nat) := nat_cancel_leaf : NatCancel m n m' n'.
-Hint Mode NatCancelLeaf ! ! - - : typeclass_instances.
-
-Global Existing Instance nat_cancel_leaf | 100.
-
-Class MakeNatS (n1 n2 m : nat) := make_nat_S : m = n1 + n2.
-Global Instance make_nat_S_0_l n : MakeNatS 0 n n.
-Proof. done. Qed.
-Global Instance make_nat_S_1 n : MakeNatS 1 n (S n).
-Proof. done. Qed.
-
-Class MakeNatPlus (n1 n2 m : nat) := make_nat_plus : m = n1 + n2.
-Global Instance make_nat_plus_0_l n : MakeNatPlus 0 n n.
-Proof. done. Qed.
-Global Instance make_nat_plus_0_r n : MakeNatPlus n 0 n.
-Proof. unfold MakeNatPlus. by rewrite Nat.add_0_r. Qed.
-Global Instance make_nat_plus_default n1 n2 : MakeNatPlus n1 n2 (n1 + n2) | 100.
-Proof. done. Qed.
-
-Global Instance nat_cancel_leaf_here m : NatCancelLeaf m m 0 0 | 0.
-Proof. by unfold NatCancelLeaf, NatCancel. Qed.
-Global Instance nat_cancel_leaf_else m n : NatCancelLeaf m n m n | 100.
-Proof. by unfold NatCancelLeaf, NatCancel. Qed.
-Global Instance nat_cancel_leaf_plus m m' m'' n1 n2 n1' n2' n1'n2' :
-  NatCancelLeaf m n1 m' n1' → NatCancelLeaf m' n2 m'' n2' →
-  MakeNatPlus n1' n2' n1'n2' → NatCancelLeaf m (n1 + n2) m'' n1'n2' | 2.
-Proof. unfold NatCancelLeaf, NatCancel, MakeNatPlus. omega. Qed.
-Global Instance nat_cancel_leaf_S_here m n m' n' :
-  NatCancelLeaf m n m' n' → NatCancelLeaf (S m) (S n) m' n' | 3.
-Proof. unfold NatCancelLeaf, NatCancel. omega. Qed.
-Global Instance nat_cancel_leaf_S_else m n m' n' :
-  NatCancelLeaf m n m' n' → NatCancelLeaf m (S n) m' (S n') | 4.
-Proof. unfold NatCancelLeaf, NatCancel. omega. Qed.
-
-(** The instance [nat_cancel_S_both] is redundant, but may reduce proof search
-quite a bit, e.g. when canceling constants in constants. *)
-Global Instance nat_cancel_S_both m n m' n' :
-  NatCancel m n m' n' → NatCancel (S m) (S n) m' n' | 1.
-Proof. unfold NatCancel. omega. Qed.
-Global Instance nat_cancel_plus m1 m2 m1' m2' m1'm2' n n' n'' :
-  NatCancel m1 n m1' n' → NatCancel m2 n' m2' n'' →
-  MakeNatPlus m1' m2' m1'm2' → NatCancel (m1 + m2) n m1'm2' n'' | 2.
-Proof. unfold NatCancel, MakeNatPlus. omega. Qed.
-Global Instance nat_cancel_S m m' m'' Sm' n n' n'' :
-  NatCancel m n m' n' → NatCancelLeaf 1 n' m'' n'' →
-  MakeNatS m'' m' Sm' → NatCancel (S m) n Sm' n'' | 3.
-Proof. unfold NatCancelLeaf, NatCancel, MakeNatS. omega. Qed.
+
+Module nat_cancel.
+  Class NatCancelL (m n m' n' : nat) := nat_cancel_l : m' + n = m + n'.
+  Hint Mode NatCancelL ! ! - - : typeclass_instances.
+  Class NatCancelR (m n m' n' : nat) := nat_cancel_r : NatCancelL m n m' n'.
+  Hint Mode NatCancelR ! ! - - : typeclass_instances.
+  Existing Instance nat_cancel_r | 100.
+
+  (** The implementation of the canceler is highly non-deterministic, but since
+  it will always succeed, no backtracking will ever be performed. In order to
+  avoid issues like:
+
+    https://gitlab.mpi-sws.org/FP/iris-coq/issues/153
+
+  we wrap the entire canceler in the [NoBackTrack] class. *)
+  Instance nat_cancel_start m n m' n' :
+    NoBackTrack (NatCancelL m n m' n') → NatCancel m n m' n'.
+  Proof. by intros [?]. Qed.
+
+  Class MakeNatS (n1 n2 m : nat) := make_nat_S : m = n1 + n2.
+  Instance make_nat_S_0_l n : MakeNatS 0 n n.
+  Proof. done. Qed.
+  Instance make_nat_S_1 n : MakeNatS 1 n (S n).
+  Proof. done. Qed.
+
+  Class MakeNatPlus (n1 n2 m : nat) := make_nat_plus : m = n1 + n2.
+  Instance make_nat_plus_0_l n : MakeNatPlus 0 n n.
+  Proof. done. Qed.
+  Instance make_nat_plus_0_r n : MakeNatPlus n 0 n.
+  Proof. unfold MakeNatPlus. by rewrite Nat.add_0_r. Qed.
+  Instance make_nat_plus_default n1 n2 : MakeNatPlus n1 n2 (n1 + n2) | 100.
+  Proof. done. Qed.
+
+  Instance nat_cancel_leaf_here m : NatCancelR m m 0 0 | 0.
+  Proof. by unfold NatCancelR, NatCancelL. Qed.
+  Instance nat_cancel_leaf_else m n : NatCancelR m n m n | 100.
+  Proof. by unfold NatCancelR. Qed.
+  Instance nat_cancel_leaf_plus m m' m'' n1 n2 n1' n2' n1'n2' :
+    NatCancelR m n1 m' n1' → NatCancelR m' n2 m'' n2' →
+    MakeNatPlus n1' n2' n1'n2' → NatCancelR m (n1 + n2) m'' n1'n2' | 2.
+  Proof. unfold NatCancelR, NatCancelL, MakeNatPlus. omega. Qed.
+  Instance nat_cancel_leaf_S_here m n m' n' :
+    NatCancelR m n m' n' → NatCancelR (S m) (S n) m' n' | 3.
+  Proof. unfold NatCancelR, NatCancelL. omega. Qed.
+  Instance nat_cancel_leaf_S_else m n m' n' :
+    NatCancelR m n m' n' → NatCancelR m (S n) m' (S n') | 4.
+  Proof. unfold NatCancelR, NatCancelL. omega. Qed.
+
+  (** The instance [nat_cancel_S_both] is redundant, but may reduce proof search
+  quite a bit, e.g. when canceling constants in constants. *)
+  Instance nat_cancel_S_both m n m' n' :
+    NatCancelL m n m' n' → NatCancelL (S m) (S n) m' n' | 1.
+  Proof. unfold NatCancelL. omega. Qed.
+  Instance nat_cancel_plus m1 m2 m1' m2' m1'm2' n n' n'' :
+    NatCancelL m1 n m1' n' → NatCancelL m2 n' m2' n'' →
+    MakeNatPlus m1' m2' m1'm2' → NatCancelL (m1 + m2) n m1'm2' n'' | 2.
+  Proof. unfold NatCancelL, MakeNatPlus. omega. Qed.
+  Instance nat_cancel_S m m' m'' Sm' n n' n'' :
+    NatCancelL m n m' n' → NatCancelR 1 n' m'' n'' →
+    MakeNatS m'' m' Sm' → NatCancelL (S m) n Sm' n'' | 3.
+  Proof. unfold NatCancelR, NatCancelL, MakeNatS. omega. Qed.
+End nat_cancel.