blob: 04fa59075b9dd5ca524fbc306cd7402bfc36f3e4 (
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
|
(* This example checks the efficiency of the abstract machine used by ring *)
(* Expected time < 1.00s *)
Require Import BinInt Zbool.
Definition Zadd x y :=
match x with
| 0%Z => y
| Zpos x' =>
match y with
| 0%Z => x
| Zpos y' => Zpos (x' + y')
| Zneg y' =>
match (x' ?= y')%positive with
| Eq => 0%Z
| Lt => Zneg (y' - x')
| Gt => Zpos (x' - y')
end
end
| Zneg x' =>
match y with
| 0%Z => x
| Zpos y' =>
match (x' ?= y')%positive with
| Eq => 0%Z
| Lt => Zpos (y' - x')
| Gt => Zneg (x' - y')
end
| Zneg y' => Zneg (x' + y')
end
end.
Require Import Ring.
Lemma Zth : ring_theory Z0 (Zpos xH) Zadd Z.mul Z.sub Z.opp (@eq Z).
Admitted.
Ltac Zcst t :=
match isZcst t with
true => t
| _ => constr:(NotConstant)
end.
Add Ring Zr : Zth
(decidable Zeq_bool_eq, constants [Zcst]).
Open Scope Z_scope.
Infix "+" := Zadd : Z_scope.
Goal forall a, a+a+a+a+a+a+a+a+a+a+a+a+a = a*13.
Timeout 5 Time intro; ring.
|
