blob: c2abc4d12511c7fccb74d2e119dc49659e6a557b (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
|
(************************************************************************)
(* 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: ArithRing.v,v 1.1.2.1 2004/07/16 19:30:18 herbelin Exp $ *)
(* Instantiation of the Ring tactic for the naturals of Arith $*)
Require Export Ring.
Require Export Arith.
Require Eqdep_dec.
V7only [Import nat_scope.].
Open Local Scope nat_scope.
Fixpoint nateq [n,m:nat] : bool :=
Cases n m of
| O O => true
| (S n') (S m') => (nateq n' m')
| _ _ => false
end.
Lemma nateq_prop : (n,m:nat)(Is_true (nateq n m))->n==m.
Proof.
Induction n; Induction m; Intros; Try Contradiction.
Trivial.
Unfold Is_true in H1.
Rewrite (H n1 H1).
Trivial.
Save.
Hints Resolve nateq_prop eq2eqT : arithring.
Definition NatTheory : (Semi_Ring_Theory plus mult (1) (0) nateq).
Split; Intros; Auto with arith arithring.
Apply eq2eqT; Apply simpl_plus_l with n:=n.
Apply eqT2eq; Trivial.
Defined.
Add Semi Ring nat plus mult (1) (0) nateq NatTheory [O S].
Goal (n:nat)(S n)=(plus (S O) 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 *)
Recursive Meta Definition S_to_plus t :=
Match t With
| [(S O)] -> '(S O)
| [(S ?1)] -> Let t1 = (S_to_plus ?1) In
'(plus (S O) t1)
| [(plus ?1 ?2)] -> Let t1 = (S_to_plus ?1)
And t2 = (S_to_plus ?2) In
'(plus t1 t2)
| [(mult ?1 ?2)] -> Let t1 = (S_to_plus ?1)
And t2 = (S_to_plus ?2) In
'(mult t1 t2)
| [?] -> 't.
(* Apply S_to_plus on both sides of an equality *)
Tactic Definition S_to_plus_eq :=
Match Context With
| [ |- ?1 = ?2 ] ->
(**) Try (**)
Let t1 = (S_to_plus ?1)
And t2 = (S_to_plus ?2) In
Change t1=t2
| [ |- ?1 == ?2 ] ->
(**) Try (**)
Let t1 = (S_to_plus ?1)
And t2 = (S_to_plus ?2) In
Change (t1==t2).
Tactic Definition NatRing := S_to_plus_eq;Ring.
|
