diff options
Diffstat (limited to 'src/Util/ZUtil/Tactics/LinearSubstitute.v')
| -rw-r--r-- | src/Util/ZUtil/Tactics/LinearSubstitute.v | 8 |
1 files changed, 8 insertions, 0 deletions
diff --git a/src/Util/ZUtil/Tactics/LinearSubstitute.v b/src/Util/ZUtil/Tactics/LinearSubstitute.v index d03c9d196..960c06ce9 100644 --- a/src/Util/ZUtil/Tactics/LinearSubstitute.v +++ b/src/Util/ZUtil/Tactics/LinearSubstitute.v @@ -12,6 +12,8 @@ Module Z. Proof. omega. Qed. Lemma move_R_Xm x y z : y - x = z -> x = y - z. Proof. omega. Qed. + Lemma move_R_nX x y : -x = y -> x = -y. + Proof. omega. Qed. Lemma move_L_pX x y z : z = x + y -> z - y = x. Proof. omega. Qed. Lemma move_L_mX x y z : z = x - y -> z + y = x. @@ -20,6 +22,8 @@ Module Z. Proof. omega. Qed. Lemma move_L_Xm x y z : z = y - x -> y - z = x. Proof. omega. Qed. + Lemma move_L_nX x y : y = -x -> -y = x. + Proof. omega. Qed. (** [linear_substitute x] attempts to maipulate equations using only addition and subtraction to put [x] on the left, and then @@ -36,6 +40,8 @@ Module Z. | ?a - ?b => first [ contains for_var b; apply move_L_mX in H | contains for_var a; apply move_L_Xm in H ] + | -?a + => contains for_var a; apply move_L_nX in H | for_var => progress symmetry in H end @@ -46,6 +52,8 @@ Module Z. | ?a - ?b => first [ not contains for_var b; apply move_R_mX in H | not contains for_var a; apply move_R_Xm in H ] + | -?a + => contains for_var a; apply move_R_nX in H end ]. Ltac linear_solve_for_in for_var H := repeat linear_solve_for_in_step for_var H. Ltac linear_solve_for for_var := |