blob: 93c6eaf53998cf9db9f3d384f7b17e953534268b (
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
82
83
|
(***********************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *)
(* \VV/ *************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(***********************************************************************)
(* $Id$ *)
Require Export Bool.
Require Export Ring_theory.
Require Export Quote.
Require Export Ring_normalize.
Require Export Ring_abstract.
Declare ML Module "ring".
Grammar tactic simple_tactic : ast :=
ring [ "Ring" constrarg_list($arg) ] -> [(Ring ($LIST $arg))].
Syntax tactic level 0:
ring [ << (Ring ($LIST $lc)) >> ] -> [ "Ring" [1 1] (LISTSPC ($LIST $lc)) ]
| ring_e [ << (Ring) >> ] -> ["Ring"].
Grammar vernac vernac : ast :=
addring [ "Add" "Ring"
constrarg($a) constrarg($aplus) constrarg($amult) constrarg($aone)
constrarg($azero) constrarg($aopp) constrarg($aeq) constrarg($t)
"[" ne_constrarg_list($l) "]" "." ]
-> [(AddRing $a $aplus $amult $aone $azero $aopp $aeq $t
($LIST $l))]
| addsemiring [ "Add" "Semi" "Ring"
constrarg($a) constrarg($aplus) constrarg($amult)
constrarg($aone) constrarg($azero) constrarg($aeq)
constrarg($t)
"[" ne_constrarg_list($l) "]" "." ]
-> [(AddSemiRing $a $aplus $amult $aone $azero $aeq $t
($LIST $l))]
| addabstractring [ "Add" "Abstract" "Ring"
constrarg($a) constrarg($aplus) constrarg($amult)
constrarg($aone) constrarg($azero) constrarg($aopp)
constrarg($aeq) constrarg($t) "." ]
-> [(AddAbstractRing $a $aplus $amult $aone $azero $aopp $aeq $t)]
| addabstractsemiring [ "Add" "Abstract" "Semi" "Ring"
constrarg($a) constrarg($aplus) constrarg($amult)
constrarg($aone) constrarg($azero) constrarg($aeq)
constrarg($t) "." ]
-> [(AddAbstractSemiRing $a $aplus $amult $aone $azero $aeq $t )]
| addsetoidring [ "Add" "Setoid" "Ring"
constrarg($a) constrarg($aequiv) constrarg($asetth) constrarg($aplus) constrarg($amult)
constrarg($aone) constrarg($azero) constrarg($aopp) constrarg($aeq) constrarg($pm)
constrarg($mm) constrarg($om) constrarg($t) "[" ne_constrarg_list($l) "]" "." ]
-> [(AddSetoidRing $a $aequiv $asetth $aplus $amult $aone $azero $aopp $aeq $pm $mm $om $t
($LIST $l))]
| addsetoidsemiring [ "Add" "Semi" "Setoid" "Ring"
constrarg($a) constrarg($aequiv) constrarg($asetth) constrarg($aplus)
constrarg($amult) constrarg($aone) constrarg($azero) constrarg($aeq)
constrarg($pm) constrarg($mm) constrarg($t) "[" ne_constrarg_list($l) "]" "." ]
-> [(AddSemiRing $a $aequiv $asetth $aplus $amult $aone $azero $aeq $pm $mm $t
($LIST $l))]
.
(* As an example, we provide an instantation for bool. *)
(* Other instatiations are given in ArithRing and ZArithRing in the
same directory *)
Definition BoolTheory : (Ring_Theory xorb andb true false [b:bool]b eqb).
Split; Simpl.
NewDestruct n; NewDestruct m; Reflexivity.
NewDestruct n; NewDestruct m; NewDestruct p; Reflexivity.
NewDestruct n; NewDestruct m; Reflexivity.
NewDestruct n; NewDestruct m; NewDestruct p; Reflexivity.
NewDestruct n; Reflexivity.
NewDestruct n; Reflexivity.
NewDestruct n; Reflexivity.
NewDestruct n; NewDestruct m; NewDestruct p; Reflexivity.
NewDestruct x; NewDestruct y; Reflexivity Orelse Simpl; Tauto.
Defined.
Add Ring bool xorb andb true false [b:bool]b eqb BoolTheory [ true false ].
|
