summaryrefslogtreecommitdiff
path: root/test-suite/complexity/ring2.v
blob: 6945edc8842fa713d88b3bb990250e0cb06f3cbb (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
(* This example checks the efficiency of the abstract machine used by ring *)
(* Expected time < 1.00s *)

Require Import BinInt Zbool.

Definition Zplus 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) Zplus Zmult Zminus Zopp (@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 "+" := Zplus : 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.