aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/Arith
diff options
context:
space:
mode:
authorGravatar Emilio Jesus Gallego Arias <e+git@x80.org>2018-04-09 01:33:31 +0200
committerGravatar Emilio Jesus Gallego Arias <e+git@x80.org>2018-04-13 12:13:48 +0200
commit2243c25c79ab19876ad74452c9cecc7dcc88c67c (patch)
treef32573eb7d7c4dbdb4493e186bed87c80e61a747 /theories/Arith
parentb68e0b4f9ba37d1c2fa5921e1d934b4b38bfdfe7 (diff)
[ltac] Deprecate nameless fix/cofix.
LTAC's `fix` and `cofix` do require access to the proof object inside the tactic monad when used without a name. This is a bit inconvenient as we aim to make the handling of the proof object purely functional. Alternatives have been discussed in #7196, and it seems that deprecating the nameless forms may have the best cost/benefit ratio, so opening this PR for discussion. See also #6171.
Diffstat (limited to 'theories/Arith')
-rw-r--r--theories/Arith/Div2.v4
-rw-r--r--theories/Arith/Even.v4
-rw-r--r--theories/Arith/PeanoNat.v10
3 files changed, 9 insertions, 9 deletions
diff --git a/theories/Arith/Div2.v b/theories/Arith/Div2.v
index 42956c475..a5e457831 100644
--- a/theories/Arith/Div2.v
+++ b/theories/Arith/Div2.v
@@ -30,7 +30,7 @@ Lemma ind_0_1_SS :
P 0 -> P 1 -> (forall n, P n -> P (S (S n))) -> forall n, P n.
Proof.
intros P H0 H1 H2.
- fix 1.
+ fix ind_0_1_SS 1.
destruct n as [|[|n]].
- exact H0.
- exact H1.
@@ -105,7 +105,7 @@ Hint Resolve double_S: arith.
Lemma even_odd_double n :
(even n <-> n = double (div2 n)) /\ (odd n <-> n = S (double (div2 n))).
Proof.
- revert n. fix 1. destruct n as [|[|n]].
+ revert n. fix even_odd_double 1. destruct n as [|[|n]].
- (* n = 0 *)
split; split; auto with arith. inversion 1.
- (* n = 1 *)
diff --git a/theories/Arith/Even.v b/theories/Arith/Even.v
index baf119732..a1d0e9fcc 100644
--- a/theories/Arith/Even.v
+++ b/theories/Arith/Even.v
@@ -38,7 +38,7 @@ Hint Constructors odd: arith.
Lemma even_equiv : forall n, even n <-> Nat.Even n.
Proof.
- fix 1.
+ fix even_equiv 1.
destruct n as [|[|n]]; simpl.
- split; [now exists 0 | constructor].
- split.
@@ -52,7 +52,7 @@ Qed.
Lemma odd_equiv : forall n, odd n <-> Nat.Odd n.
Proof.
- fix 1.
+ fix odd_equiv 1.
destruct n as [|[|n]]; simpl.
- split.
+ inversion_clear 1.
diff --git a/theories/Arith/PeanoNat.v b/theories/Arith/PeanoNat.v
index 4e4938a99..bc58995fd 100644
--- a/theories/Arith/PeanoNat.v
+++ b/theories/Arith/PeanoNat.v
@@ -315,7 +315,7 @@ Import Private_Parity.
Lemma even_spec : forall n, even n = true <-> Even n.
Proof.
- fix 1.
+ fix even_spec 1.
destruct n as [|[|n]]; simpl.
- split; [ now exists 0 | trivial ].
- split; [ discriminate | intro H; elim (Even_1 H) ].
@@ -325,7 +325,7 @@ Qed.
Lemma odd_spec : forall n, odd n = true <-> Odd n.
Proof.
unfold odd.
- fix 1.
+ fix odd_spec 1.
destruct n as [|[|n]]; simpl.
- split; [ discriminate | intro H; elim (Odd_0 H) ].
- split; [ now exists 0 | trivial ].
@@ -473,7 +473,7 @@ Notation "( x | y )" := (divide x y) (at level 0) : nat_scope.
Lemma gcd_divide : forall a b, (gcd a b | a) /\ (gcd a b | b).
Proof.
- fix 1.
+ fix gcd_divide 1.
intros [|a] b; simpl.
split.
now exists 0.
@@ -502,7 +502,7 @@ Qed.
Lemma gcd_greatest : forall a b c, (c|a) -> (c|b) -> (c|gcd a b).
Proof.
- fix 1.
+ fix gcd_greatest 1.
intros [|a] b; simpl; auto.
fold (b mod (S a)).
intros c H H'. apply gcd_greatest; auto.
@@ -536,7 +536,7 @@ Qed.
Lemma le_div2 n : div2 (S n) <= n.
Proof.
revert n.
- fix 1.
+ fix le_div2 1.
destruct n; simpl; trivial. apply lt_succ_r.
destruct n; [simpl|]; trivial. now constructor.
Qed.