diff options
Diffstat (limited to 'plugins/ring/LegacyArithRing.v')
-rw-r--r-- | plugins/ring/LegacyArithRing.v | 90 |
1 files changed, 90 insertions, 0 deletions
diff --git a/plugins/ring/LegacyArithRing.v b/plugins/ring/LegacyArithRing.v new file mode 100644 index 00000000..231b5fbb --- /dev/null +++ b/plugins/ring/LegacyArithRing.v @@ -0,0 +1,90 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(* $Id$ *) + +(* Instantiation of the Ring tactic for the naturals of Arith $*) + +Require Import Bool. +Require Export LegacyRing. +Require Export Arith. +Require Import Eqdep_dec. + +Open Local Scope nat_scope. + +Unboxed Fixpoint nateq (n m:nat) {struct m} : bool := + match n, m with + | O, O => true + | S n', S m' => nateq n' m' + | _, _ => false + end. + +Lemma nateq_prop : forall n m:nat, Is_true (nateq n m) -> n = m. +Proof. + simple induction n; simple induction m; intros; try contradiction. + trivial. + unfold Is_true in H1. + rewrite (H n1 H1). + trivial. +Qed. + +Hint Resolve nateq_prop: arithring. + +Definition NatTheory : Semi_Ring_Theory plus mult 1 0 nateq. + split; intros; auto with arith arithring. +(* apply (fun n m p:nat => plus_reg_l m p n) with (n := n). + trivial.*) +Defined. + + +Add Legacy Semi Ring nat plus mult 1 0 nateq NatTheory [ 0 S ]. + +Goal forall n:nat, S n = 1 + n. +intro; reflexivity. +Save S_to_plus_one. + +(* Replace all occurrences of (S exp) by (plus (S O) exp), except when + exp is already O and only for those occurrences than can be reached by going + down plus and mult operations *) +Ltac rewrite_S_to_plus_term t := + match constr:t with + | 1 => constr:1 + | (S ?X1) => + let t1 := rewrite_S_to_plus_term X1 in + constr:(1 + t1) + | (?X1 + ?X2) => + let t1 := rewrite_S_to_plus_term X1 + with t2 := rewrite_S_to_plus_term X2 in + constr:(t1 + t2) + | (?X1 * ?X2) => + let t1 := rewrite_S_to_plus_term X1 + with t2 := rewrite_S_to_plus_term X2 in + constr:(t1 * t2) + | _ => constr:t + end. + +(* Apply S_to_plus on both sides of an equality *) +Ltac rewrite_S_to_plus := + match goal with + | |- (?X1 = ?X2) => + try + let t1 := + (**) (**) + rewrite_S_to_plus_term X1 + with t2 := rewrite_S_to_plus_term X2 in + change (t1 = t2) in |- * + | |- (?X1 = ?X2) => + try + let t1 := + (**) (**) + rewrite_S_to_plus_term X1 + with t2 := rewrite_S_to_plus_term X2 in + change (t1 = t2) in |- * + end. + +Ltac ring_nat := rewrite_S_to_plus; ring. |