diff options
| author | letouzey | 2011-01-03 18:51:13 +0000 |
|---|---|---|
| committer | letouzey | 2011-01-03 18:51:13 +0000 |
| commit | 8e2d90a6a9f4480026afd433fc997d9958f76a38 (patch) | |
| tree | 6a92d154766a3a8934b91705acf79cc994a42061 /theories/Numbers/Integer/NatPairs | |
| parent | 05662999c9ab0183c0f97fc18579379142ac7b38 (diff) | |
Numbers: some improvements in proofs
- a ltac solve_proper which generalizes solve_predicate_wd and co
- using le_elim is nicer that (apply le_lteq; destruct ...)
- "apply ->" can now be "apply" most of the time.
Benefit: NumPrelude is now almost empty
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13762 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories/Numbers/Integer/NatPairs')
| -rw-r--r-- | theories/Numbers/Integer/NatPairs/ZNatPairs.v | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/theories/Numbers/Integer/NatPairs/ZNatPairs.v b/theories/Numbers/Integer/NatPairs/ZNatPairs.v index ab555ca321..2b568dddcf 100644 --- a/theories/Numbers/Integer/NatPairs/ZNatPairs.v +++ b/theories/Numbers/Integer/NatPairs/ZNatPairs.v @@ -13,7 +13,7 @@ Require Export Ring. Notation "s #1" := (fst s) (at level 9, format "s '#1'") : pair_scope. Notation "s #2" := (snd s) (at level 9, format "s '#2'") : pair_scope. -Open Local Scope pair_scope. +Local Open Scope pair_scope. Module ZPairsAxiomsMod (Import N : NAxiomsMiniSig) <: ZAxiomsMiniSig. Module Import NProp. @@ -173,8 +173,8 @@ rewrite (A_wd (n, m) (0, p)) by (rewrite add_0_l; now rewrite add_comm). apply H2. rewrite (A_wd (n, m) (p, 0)) by now rewrite add_0_r. apply H1. induct p. assumption. intros p IH. -apply -> (A_wd (0, p) (1, N.succ p)) in IH; [| now rewrite add_0_l, add_1_l]. -rewrite one_succ in IH. now apply <- AS. +apply (A_wd (0, p) (1, N.succ p)) in IH; [| now rewrite add_0_l, add_1_l]. +rewrite one_succ in IH. now apply AS. induct p. assumption. intros p IH. replace 0 with (snd (p, 0)); [| reflexivity]. replace (N.succ p) with (N.succ (fst (p, 0))); [| reflexivity]. now apply -> AS. |