Book a Demo!
CoCalc Logo Icon
StoreFeaturesDocsShareSupportNewsAboutPoliciesSign UpSign In
sagemath
GitHub Repository: sagemath/sagelib
Path: blob/master/sage/structure/proof/proof.py
4045 views
1
from sage.structure.sage_object import SageObject
2
3
class _ProofPref(SageObject):
4
"""
5
An object that holds global proof preferences. For now these are merely True/False flags for various parts of Sage that use probabilistic algorithms.
6
A True flag means that the subsystem (such as linear algebra or number fields) should return results that are true unconditionally: the correctness should not depend on an algorithm with a nonzero probability of returning an incorrect answer or on the truth of any unproven conjectures.
7
A False flag means that the subsystem can use faster methods to return answers that have a very small probability of being wrong.
8
"""
9
def __init__(self, proof = True):
10
self._require_proof = {}
11
self._require_proof["arithmetic"] = proof
12
self._require_proof["elliptic_curve"] = proof
13
self._require_proof["linear_algebra"] = proof
14
self._require_proof["number_field"] = proof
15
self._require_proof["polynomial"] = proof
16
self._require_proof["other"] = proof
17
18
def arithmetic(self, t = None):
19
"""
20
Controls the default proof strategy for integer arithmetic algorithms (such as primality testing).
21
22
INPUT:
23
t -- boolean or None
24
25
OUTPUT:
26
If t == True, requires integer arithmetic operations to (by default) return results that are true unconditionally: the correctness will not depend on an algorithm with a nonzero probability of returning an incorrect answer or on the truth of any unproven conjectures.
27
If t == False, allows integer arithmetic operations to (by default) return results that may depend on unproven conjectures or on probabilistic algorithms. Such algorithms often have a substantial speed improvement over those requiring proof.
28
If t is None, returns the integer arithmetic proof status.
29
30
EXAMPLES:
31
sage: proof.arithmetic()
32
True
33
sage: proof.arithmetic(False)
34
sage: proof.arithmetic()
35
False
36
sage: proof.arithmetic(True)
37
sage: proof.arithmetic()
38
True
39
"""
40
if t is None:
41
return self._require_proof["arithmetic"]
42
self._require_proof["arithmetic"] = bool(t)
43
44
def elliptic_curve(self, t = None):
45
"""
46
Controls the default proof strategy for elliptic curve algorithms.
47
48
INPUT:
49
t -- boolean or None
50
51
OUTPUT:
52
If t == True, requires elliptic curve algorithms to (by default) return results that are true unconditionally: the correctness will not depend on an algorithm with a nonzero probability of returning an incorrect answer or on the truth of any unproven conjectures.
53
If t == False, allows elliptic curve algorithms to (by default) return results that may depend on unproven conjectures or on probabilistic algorithms. Such algorithms often have a substantial speed improvement over those requiring proof.
54
If t is None, returns the current elliptic curve proof status.
55
56
EXAMPLES:
57
sage: proof.elliptic_curve()
58
True
59
sage: proof.elliptic_curve(False)
60
sage: proof.elliptic_curve()
61
False
62
sage: proof.elliptic_curve(True)
63
sage: proof.elliptic_curve()
64
True
65
"""
66
if t is None:
67
return self._require_proof["elliptic_curve"]
68
self._require_proof["elliptic_curve"] = bool(t)
69
70
def linear_algebra(self, t = None):
71
"""
72
Controls the default proof strategy for linear algebra algorithms.
73
74
INPUT:
75
t -- boolean or None
76
77
OUTPUT:
78
If t == True, requires linear algebra algorithms to (by default) return results that are true unconditionally: the correctness will not depend on an algorithm with a nonzero probability of returning an incorrect answer or on the truth of any unproven conjectures.
79
If t == False, allows linear algebra algorithms to (by default) return results that may depend on unproven conjectures or on probabilistic algorithms. Such algorithms often have a substantial speed improvement over those requiring proof.
80
If t is None, returns the current linear algebra proof status.
81
82
EXAMPLES:
83
sage: proof.linear_algebra()
84
True
85
sage: proof.linear_algebra(False)
86
sage: proof.linear_algebra()
87
False
88
sage: proof.linear_algebra(True)
89
sage: proof.linear_algebra()
90
True
91
"""
92
if t is None:
93
return self._require_proof["linear_algebra"]
94
self._require_proof["linear_algebra"] = bool(t)
95
96
def number_field(self, t = None):
97
"""
98
Controls the default proof strategy for number field algorithms.
99
100
INPUT:
101
t -- boolean or None
102
103
OUTPUT:
104
If t == True, requires number field algorithms to (by default) return results that are true unconditionally: the correctness will not depend on an algorithm with a nonzero probability of returning an incorrect answer or on the truth of any unproven conjectures.
105
If t == False, allows number field algorithms to (by default) return results that may depend on unproven conjectures or on probabilistic algorithms. Such algorithms often have a substantial speed improvement over those requiring proof.
106
If t is None, returns the current number field proof status.
107
108
EXAMPLES:
109
sage: proof.number_field()
110
True
111
sage: proof.number_field(False)
112
sage: proof.number_field()
113
False
114
sage: proof.number_field(True)
115
sage: proof.number_field()
116
True
117
"""
118
if t is None:
119
return self._require_proof["number_field"]
120
self._require_proof["number_field"] = bool(t)
121
122
def polynomial(self, t = None):
123
"""
124
Controls the default proof strategy for polynomial algorithms.
125
126
INPUT:
127
t -- boolean or None
128
129
OUTPUT:
130
If t == True, requires polynomial algorithms to (by default) return results that are true unconditionally: the correctness will not depend on an algorithm with a nonzero probability of returning an incorrect answer or on the truth of any unproven conjectures.
131
If t == False, allows polynomial algorithms to (by default) return results that may depend on unproven conjectures or on probabilistic algorithms. Such algorithms often have a substantial speed improvement over those requiring proof.
132
If t is None, returns the current polynomial proof status.
133
134
EXAMPLES:
135
sage: proof.polynomial()
136
True
137
sage: proof.polynomial(False)
138
sage: proof.polynomial()
139
False
140
sage: proof.polynomial(True)
141
sage: proof.polynomial()
142
True
143
"""
144
if t is None:
145
return self._require_proof["polynomial"]
146
self._require_proof["polynomial"] = bool(t)
147
148
149
_proof_prefs = _ProofPref(True) #Creates the global object that stores proof preferences.
150
151
def get_flag(t = None, subsystem = None):
152
"""
153
Used for easily determining the correct proof flag to use.
154
155
EXAMPLES:
156
sage: from sage.structure.proof.proof import get_flag
157
sage: get_flag(False)
158
False
159
sage: get_flag(True)
160
True
161
sage: get_flag()
162
True
163
sage: proof.all(False)
164
sage: get_flag()
165
False
166
"""
167
if t is None:
168
if subsystem in ["arithmetic", "elliptic_curve", "linear_algebra", "number_field","polynomial"]:
169
return _proof_prefs._require_proof[subsystem]
170
else:
171
return _proof_prefs._require_proof["other"]
172
return t
173
174
class WithProof:
175
"""
176
Use WithProof to temparily set the value of one of the proof
177
systems for a block of code, with a guarantee that it will be set
178
back to how it was before after the block is done, even if there is an error.
179
180
EXAMPLES::
181
182
sage: proof.arithmetic(True)
183
sage: with proof.WithProof('arithmetic',False): # this would hang "forever" if attempted with proof=True
184
... print (10^1000 + 453).is_prime()
185
... print 1/0
186
...
187
Traceback (most recent call last):
188
...
189
ZeroDivisionError: Rational division by zero
190
sage: proof.arithmetic()
191
True
192
"""
193
def __init__(self, subsystem, t):
194
"""
195
TESTS::
196
197
sage: proof.arithmetic(True)
198
sage: P = proof.WithProof('arithmetic',False); P
199
<sage.structure.proof.proof.WithProof instance at ...>
200
sage: P._subsystem
201
'arithmetic'
202
sage: P._t
203
False
204
sage: P._t_orig
205
True
206
"""
207
self._subsystem = str(subsystem)
208
self._t = bool(t)
209
self._t_orig = _proof_prefs._require_proof[subsystem]
210
211
def __enter__(self):
212
"""
213
TESTS::
214
215
sage: proof.arithmetic(True)
216
sage: P = proof.WithProof('arithmetic',False)
217
sage: P.__enter__()
218
sage: proof.arithmetic()
219
False
220
sage: proof.arithmetic(True)
221
"""
222
_proof_prefs._require_proof[self._subsystem] = self._t
223
224
def __exit__(self, *args):
225
"""
226
TESTS::
227
228
sage: proof.arithmetic(True)
229
sage: P = proof.WithProof('arithmetic',False)
230
sage: P.__enter__()
231
sage: proof.arithmetic()
232
False
233
sage: P.__exit__()
234
sage: proof.arithmetic()
235
True
236
"""
237
_proof_prefs._require_proof[self._subsystem] = self._t_orig
238
239
240