nat_cancel.v 4.35 KB
 Robbert Krebbers committed Feb 08, 2018 1 2 ``````From stdpp Require Import numbers. `````` Robbert Krebbers committed Feb 08, 2018 3 ``````(** The class [NatCancel m n m' n'] is a simple canceler for natural numbers `````` Robbert Krebbers committed Feb 08, 2018 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 ``````implemented using type classes. Input: [m], [n]; output: [m'], [n']. It turns an equality [n = m] into an equality [n' = m'] by canceling out terms that appear on both sides of the equality. We provide instances to handle the following connectives over natural numbers: n := 0 | t | n + m | S m Here, [t] represents arbitrary terms that do not fit the grammar. The instances the class perform a depth-first traversal (from left to right) through [n] and try to cancel each leaf in [m]. This implies that the shape of the original expressions [n] and [m] are preserved as much as possible. For example, canceling: S (S m2) + (k1 + (S k2 + k3)) + n1 = 2 + S ((n1 + S n2) + S (S m1 + m2)) Results in: k1 + (k2 + k3) = S (n2 + S (S m1)) The instances are setup up so that canceling is performed in two stages. `````` Robbert Krebbers committed Feb 09, 2018 28 ``````- In the first stage, using the class [NatCancelL], it traverses [m] w.r.t. [S] `````` Robbert Krebbers committed Feb 08, 2018 29 30 `````` and [+]. - In the second stage, for each leaf (i.e. a constant or arbitrary term) `````` Robbert Krebbers committed Feb 09, 2018 31 `````` obtained by the traversal in stage 1, it uses the class [NatCancelR] to `````` Robbert Krebbers committed Feb 08, 2018 32 33 34 35 36 37 `````` 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. *) `````` Robbert Krebbers committed Feb 09, 2018 38 `````` `````` Robbert Krebbers committed Feb 08, 2018 39 40 ``````Class NatCancel (m n m' n' : nat) := nat_cancel : m' + n = m + n'. Hint Mode NatCancel ! ! - - : typeclass_instances. `````` Robbert Krebbers committed Feb 09, 2018 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 `````` 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' : `````` Robbert Krebbers committed Apr 26, 2019 57 `````` TCNoBackTrack (NatCancelL m n m' n') → NatCancel m n m' n'. `````` Robbert Krebbers committed Feb 09, 2018 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 `````` 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. `````` Ralf Jung committed Jun 20, 2018 81 `````` Proof. unfold NatCancelR, NatCancelL, MakeNatPlus. lia. Qed. `````` Robbert Krebbers committed Feb 09, 2018 82 83 `````` Instance nat_cancel_leaf_S_here m n m' n' : NatCancelR m n m' n' → NatCancelR (S m) (S n) m' n' | 3. `````` Ralf Jung committed Jun 20, 2018 84 `````` Proof. unfold NatCancelR, NatCancelL. lia. Qed. `````` Robbert Krebbers committed Feb 09, 2018 85 86 `````` Instance nat_cancel_leaf_S_else m n m' n' : NatCancelR m n m' n' → NatCancelR m (S n) m' (S n') | 4. `````` Ralf Jung committed Jun 20, 2018 87 `````` Proof. unfold NatCancelR, NatCancelL. lia. Qed. `````` Robbert Krebbers committed Feb 09, 2018 88 89 90 91 92 `````` (** 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. `````` Ralf Jung committed Jun 20, 2018 93 `````` Proof. unfold NatCancelL. lia. Qed. `````` Robbert Krebbers committed Feb 09, 2018 94 95 96 `````` 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. `````` Ralf Jung committed Jun 20, 2018 97 `````` Proof. unfold NatCancelL, MakeNatPlus. lia. Qed. `````` Robbert Krebbers committed Feb 09, 2018 98 99 100 `````` 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. `````` Ralf Jung committed Jun 20, 2018 101 `````` Proof. unfold NatCancelR, NatCancelL, MakeNatS. lia. Qed. `````` Robbert Krebbers committed Feb 09, 2018 102 ``End nat_cancel.``