diff options
Diffstat (limited to 'mathcomp/ssrtest/rewpatterns.v')
| -rw-r--r-- | mathcomp/ssrtest/rewpatterns.v | 14 |
1 files changed, 7 insertions, 7 deletions
diff --git a/mathcomp/ssrtest/rewpatterns.v b/mathcomp/ssrtest/rewpatterns.v index 95c3c00..22ca265 100644 --- a/mathcomp/ssrtest/rewpatterns.v +++ b/mathcomp/ssrtest/rewpatterns.v @@ -10,7 +10,7 @@ by move=> x y f; rewrite [_.+1](addnC x.+1). Qed. Lemma test2 : forall x y f, x + y + f (y + x) + f (y + x) = x + y + f (y + x) + f (x + y). -by move=> x y f; rewrite {2}[in f _]addnC. +by move=> x y f; rewrite {2}[in f _]addnC. Qed. Lemma test2' : forall x y f, true && f (x * (y + x)) = true && f(x * (x + y)). @@ -27,7 +27,7 @@ by move=> x y f; rewrite [in f _](addnC x). (* put y when bound var will be OK * Qed. Lemma test3 : forall x y f, x + f (x + y) (f (y + x) x) = x + f (x + y) (f (x + y) x). -by move=> x y f; rewrite [in X in (f _ X)](addnC y). +by move=> x y f; rewrite [in X in (f _ X)](addnC y). Qed. Lemma test3' : forall x y f, x = y -> x + f (x + x) x + f (x + x) x = @@ -37,7 +37,7 @@ Qed. Lemma test3'' : forall x y f, x = y -> x + f (x + y) x + f (x + y) x = x + f (x + y) x + f (y + y) x. -by move=> x y f E; rewrite {2}[in X in (f X _)]E. +by move=> x y f E; rewrite {2}[in X in (f X _)]E. Qed. Lemma test4 : forall x y f, x = y -> x + f (fun _ : nat => x + x) x + f (fun _ => x + x) x = @@ -52,22 +52,22 @@ Qed. Lemma test5 : forall x y f, x = y -> x + f (y + x) x + f (y + x) x = x + f (x + y) x + f (y + x) x. -by move=> x y f E; rewrite {1}[X in (f X _)]addnC. +by move=> x y f E; rewrite {1}[X in (f X _)]addnC. Qed. Lemma test3''' : forall x y f, x = y -> x + f (x + y) x + f (x + y) (x + y) = x + f (x + y) x + f (y + y) (x + y). -by move=> x y f E; rewrite {1}[in X in (f X X)]E. +by move=> x y f E; rewrite {1}[in X in (f X X)]E. Qed. Lemma test3'''' : forall x y f, x = y -> x + f (x + y) x + f (x + y) (x + y) = x + f (x + y) x + f (y + y) (y + y). -by move=> x y f E; rewrite [in X in (f X X)]E. +by move=> x y f E; rewrite [in X in (f X X)]E. Qed. Lemma test3x : forall x y f, y+y = x+y -> x + f (x + y) x + f (x + y) (x + y) = x + f (x + y) x + f (y + y) (y + y). -by move=> x y f E; rewrite -[X in (f X X)]E. +by move=> x y f E; rewrite -[X in (f X X)]E. Qed. Lemma test6 : forall x y (f : nat -> nat), f (x + y).+1 = f (y.+1 + x). |