1use crate::prelude::*;
2use crate::verify::verify_builtin_rules::{
3 compare_normalized_number_str_to_zero, normalized_decimal_string_is_even_integer,
4 NumberCompareResult,
5};
6use crate::verify::verify_number_in_standard_set::is_integer_after_simplification;
7use std::rc::Rc;
8
9#[inline]
11pub fn objs_equal_by_display_string(a: &Obj, b: &Obj) -> bool {
12 a.to_string() == b.to_string()
13}
14
15pub fn verify_equality_by_they_are_the_same(left: &Obj, right: &Obj) -> bool {
16 objs_equal_by_display_string(left, right)
17}
18
19#[inline]
20fn obj_expr_mentions_bare_id_on_two(l: &Obj, r: &Obj, id: &str) -> bool {
21 obj_expr_mentions_bare_id(l, id) || obj_expr_mentions_bare_id(r, id)
22}
23
24fn obj_expr_mentions_bare_id(obj: &Obj, id: &str) -> bool {
27 match obj {
28 Obj::Atom(AtomObj::Identifier(i)) => i.name == id,
29 Obj::Number(_) | Obj::StandardSet(_) => false,
30 Obj::Add(b) => obj_expr_mentions_bare_id_on_two(b.left.as_ref(), b.right.as_ref(), id),
31 Obj::Sub(b) => obj_expr_mentions_bare_id_on_two(b.left.as_ref(), b.right.as_ref(), id),
32 Obj::Mul(b) => obj_expr_mentions_bare_id_on_two(b.left.as_ref(), b.right.as_ref(), id),
33 Obj::Div(b) => obj_expr_mentions_bare_id_on_two(b.left.as_ref(), b.right.as_ref(), id),
34 Obj::Mod(b) => obj_expr_mentions_bare_id_on_two(b.left.as_ref(), b.right.as_ref(), id),
35 Obj::Max(b) => obj_expr_mentions_bare_id_on_two(b.left.as_ref(), b.right.as_ref(), id),
36 Obj::Min(b) => obj_expr_mentions_bare_id_on_two(b.left.as_ref(), b.right.as_ref(), id),
37 Obj::Union(b) => obj_expr_mentions_bare_id_on_two(b.left.as_ref(), b.right.as_ref(), id),
38 Obj::Intersect(b) => {
39 obj_expr_mentions_bare_id_on_two(b.left.as_ref(), b.right.as_ref(), id)
40 }
41 Obj::SetMinus(b) => obj_expr_mentions_bare_id_on_two(b.left.as_ref(), b.right.as_ref(), id),
42 Obj::SetDiff(b) => obj_expr_mentions_bare_id_on_two(b.left.as_ref(), b.right.as_ref(), id),
43 Obj::MatrixAdd(b) => {
44 obj_expr_mentions_bare_id_on_two(b.left.as_ref(), b.right.as_ref(), id)
45 }
46 Obj::MatrixSub(b) => {
47 obj_expr_mentions_bare_id_on_two(b.left.as_ref(), b.right.as_ref(), id)
48 }
49 Obj::MatrixMul(b) => {
50 obj_expr_mentions_bare_id_on_two(b.left.as_ref(), b.right.as_ref(), id)
51 }
52 Obj::Pow(p) => {
53 obj_expr_mentions_bare_id(p.base.as_ref(), id)
54 || obj_expr_mentions_bare_id(p.exponent.as_ref(), id)
55 }
56 Obj::MatrixScalarMul(m) => {
57 obj_expr_mentions_bare_id(m.scalar.as_ref(), id)
58 || obj_expr_mentions_bare_id(m.matrix.as_ref(), id)
59 }
60 Obj::MatrixPow(m) => {
61 obj_expr_mentions_bare_id(m.base.as_ref(), id)
62 || obj_expr_mentions_bare_id(m.exponent.as_ref(), id)
63 }
64 Obj::Abs(u) => obj_expr_mentions_bare_id(u.arg.as_ref(), id),
65 Obj::PowerSet(u) => obj_expr_mentions_bare_id(u.set.as_ref(), id),
66 Obj::Cup(u) => obj_expr_mentions_bare_id(u.left.as_ref(), id),
67 Obj::Cap(u) => obj_expr_mentions_bare_id(u.left.as_ref(), id),
68 Obj::Log(l) => {
69 obj_expr_mentions_bare_id(l.base.as_ref(), id)
70 || obj_expr_mentions_bare_id(l.arg.as_ref(), id)
71 }
72 Obj::ListSet(list) => list
73 .list
74 .iter()
75 .any(|o| obj_expr_mentions_bare_id(o.as_ref(), id)),
76 Obj::Tuple(t) => t
77 .args
78 .iter()
79 .any(|o| obj_expr_mentions_bare_id(o.as_ref(), id)),
80 Obj::Cart(c) => c
81 .args
82 .iter()
83 .any(|o| obj_expr_mentions_bare_id(o.as_ref(), id)),
84 Obj::Count(c) => obj_expr_mentions_bare_id(c.set.as_ref(), id),
85 Obj::TupleDim(t) => obj_expr_mentions_bare_id(t.arg.as_ref(), id),
86 Obj::CartDim(c) => obj_expr_mentions_bare_id(c.set.as_ref(), id),
87 Obj::Proj(p) => {
88 obj_expr_mentions_bare_id(p.set.as_ref(), id)
89 || obj_expr_mentions_bare_id(p.dim.as_ref(), id)
90 }
91 Obj::ObjAtIndex(oi) => {
92 obj_expr_mentions_bare_id(oi.obj.as_ref(), id)
93 || obj_expr_mentions_bare_id(oi.index.as_ref(), id)
94 }
95 Obj::Range(r) => obj_expr_mentions_bare_id_on_two(r.start.as_ref(), r.end.as_ref(), id),
96 Obj::ClosedRange(r) => {
97 obj_expr_mentions_bare_id_on_two(r.start.as_ref(), r.end.as_ref(), id)
98 }
99 Obj::Sum(s) => {
100 obj_expr_mentions_bare_id(s.start.as_ref(), id)
101 || obj_expr_mentions_bare_id(s.end.as_ref(), id)
102 || obj_expr_mentions_bare_id(s.func.as_ref(), id)
103 }
104 Obj::Product(p) => {
105 obj_expr_mentions_bare_id(p.start.as_ref(), id)
106 || obj_expr_mentions_bare_id(p.end.as_ref(), id)
107 || obj_expr_mentions_bare_id(p.func.as_ref(), id)
108 }
109 Obj::FiniteSeqListObj(f) => f
110 .objs
111 .iter()
112 .any(|o| obj_expr_mentions_bare_id(o.as_ref(), id)),
113 Obj::MatrixListObj(m) => m.rows.iter().any(|row| {
114 row.iter()
115 .any(|o| obj_expr_mentions_bare_id(o.as_ref(), id))
116 }),
117 Obj::Choose(ch) => obj_expr_mentions_bare_id(ch.set.as_ref(), id),
118 Obj::FamilyObj(fo) => fo.params.iter().any(|p| obj_expr_mentions_bare_id(p, id)),
119 Obj::FiniteSeqSet(fs) => {
120 obj_expr_mentions_bare_id(fs.set.as_ref(), id)
121 || obj_expr_mentions_bare_id(fs.n.as_ref(), id)
122 }
123 Obj::SeqSet(ss) => obj_expr_mentions_bare_id(ss.set.as_ref(), id),
124 Obj::MatrixSet(ms) => {
125 obj_expr_mentions_bare_id(ms.set.as_ref(), id)
126 || obj_expr_mentions_bare_id(ms.row_len.as_ref(), id)
127 || obj_expr_mentions_bare_id(ms.col_len.as_ref(), id)
128 }
129 Obj::Atom(AtomObj::IdentifierWithMod(_)) => false,
130 Obj::AnonymousFn(anon) => {
131 for g in &anon.body.params_def_with_set {
132 if obj_expr_mentions_bare_id(&g.set, id) {
133 return true;
134 }
135 }
136 obj_expr_mentions_bare_id(anon.body.ret_set.as_ref(), id)
137 || obj_expr_mentions_bare_id(anon.equal_to.as_ref(), id)
138 }
139 Obj::FnObj(_) | Obj::FnSet(_) | Obj::SetBuilder(_) => true,
140 Obj::Atom(AtomObj::Forall(p)) => p.name == id,
141 Obj::Atom(AtomObj::Def(p)) => p.name == id,
142 Obj::Atom(AtomObj::Exist(p)) => p.name == id,
143 Obj::Atom(AtomObj::SetBuilder(p)) => p.name == id,
144 Obj::Atom(AtomObj::FnSet(p)) => p.name == id,
145 Obj::Atom(AtomObj::Induc(p)) => p.name == id,
146 Obj::Atom(AtomObj::DefAlgo(p)) => p.name == id,
147 }
148}
149
150fn factual_equal_success_by_builtin_reason(
151 left: &Obj,
152 right: &Obj,
153 line_file: LineFile,
154 reason: &str,
155) -> StmtResult {
156 StmtResult::FactualStmtSuccess(
157 FactualStmtSuccess::new_with_verified_by_builtin_rules_recording_stmt(
158 EqualFact::new(left.clone(), right.clone(), line_file).into(),
159 reason.to_string(),
160 Vec::new(),
161 ),
162 )
163}
164
165impl Runtime {
166 fn literal_zero_obj_for_abs_builtin() -> Obj {
167 Obj::Number(Number::new("0".to_string()))
168 }
169
170 fn obj_is_literal_neg_one_for_abs_builtin(obj: &Obj) -> bool {
171 match obj {
172 Obj::Number(n) => n.normalized_value == "-1",
173 _ => false,
174 }
175 }
176
177 fn obj_is_negation_of_for_abs_builtin(obj: &Obj, expected_arg: &Obj) -> bool {
178 match obj {
179 Obj::Mul(m) => {
180 (Self::obj_is_literal_neg_one_for_abs_builtin(m.left.as_ref())
181 && objs_equal_by_display_string(m.right.as_ref(), expected_arg))
182 || (Self::obj_is_literal_neg_one_for_abs_builtin(m.right.as_ref())
183 && objs_equal_by_display_string(m.left.as_ref(), expected_arg))
184 }
185 _ => false,
186 }
187 }
188
189 fn obj_is_abs_product_for_abs_builtin(obj: &Obj, x: &Obj, y: &Obj) -> bool {
190 let Obj::Mul(m) = obj else {
191 return false;
192 };
193 match (m.left.as_ref(), m.right.as_ref()) {
194 (Obj::Abs(left_abs), Obj::Abs(right_abs)) => {
195 objs_equal_by_display_string(left_abs.arg.as_ref(), x)
196 && objs_equal_by_display_string(right_abs.arg.as_ref(), y)
197 }
198 _ => false,
199 }
200 }
201
202 fn try_verify_abs_nonnegative_identity(
203 &mut self,
204 left: &Obj,
205 right: &Obj,
206 line_file: LineFile,
207 verify_state: &VerifyState,
208 ) -> Result<Option<StmtResult>, RuntimeError> {
209 let (arg, other) = match (left, right) {
210 (Obj::Abs(abs), other) => (abs.arg.as_ref(), other),
211 (other, Obj::Abs(abs)) => (abs.arg.as_ref(), other),
212 _ => return Ok(None),
213 };
214 if !objs_equal_by_display_string(arg, other) {
215 return Ok(None);
216 }
217 let nonnegative: AtomicFact = LessEqualFact::new(
218 Self::literal_zero_obj_for_abs_builtin(),
219 arg.clone(),
220 line_file.clone(),
221 )
222 .into();
223 let nonnegative_result =
224 self.verify_non_equational_known_then_builtin_rules_only(&nonnegative, verify_state)?;
225 if !nonnegative_result.is_true() {
226 return Ok(None);
227 }
228 Ok(Some(
229 FactualStmtSuccess::new_with_verified_by_builtin_rules_recording_stmt(
230 EqualFact::new(left.clone(), right.clone(), line_file).into(),
231 "abs: abs(x) = x from 0 <= x".to_string(),
232 vec![nonnegative_result],
233 )
234 .into(),
235 ))
236 }
237
238 fn try_verify_abs_nonpositive_negation(
239 &mut self,
240 left: &Obj,
241 right: &Obj,
242 line_file: LineFile,
243 verify_state: &VerifyState,
244 ) -> Result<Option<StmtResult>, RuntimeError> {
245 let (arg, other) = match (left, right) {
246 (Obj::Abs(abs), other) => (abs.arg.as_ref(), other),
247 (other, Obj::Abs(abs)) => (abs.arg.as_ref(), other),
248 _ => return Ok(None),
249 };
250 if !Self::obj_is_negation_of_for_abs_builtin(other, arg) {
251 return Ok(None);
252 }
253 let nonpositive: AtomicFact = LessEqualFact::new(
254 arg.clone(),
255 Self::literal_zero_obj_for_abs_builtin(),
256 line_file.clone(),
257 )
258 .into();
259 let nonpositive_result =
260 self.verify_non_equational_known_then_builtin_rules_only(&nonpositive, verify_state)?;
261 if !nonpositive_result.is_true() {
262 return Ok(None);
263 }
264 Ok(Some(
265 FactualStmtSuccess::new_with_verified_by_builtin_rules_recording_stmt(
266 EqualFact::new(left.clone(), right.clone(), line_file).into(),
267 "abs: abs(x) = -x from x <= 0".to_string(),
268 vec![nonpositive_result],
269 )
270 .into(),
271 ))
272 }
273
274 fn try_verify_abs_product(
275 &mut self,
276 left: &Obj,
277 right: &Obj,
278 line_file: LineFile,
279 ) -> Result<Option<StmtResult>, RuntimeError> {
280 let matches_abs_product = |abs_side: &Obj, product_side: &Obj| -> bool {
281 let Obj::Abs(abs) = abs_side else {
282 return false;
283 };
284 let Obj::Mul(inner_mul) = abs.arg.as_ref() else {
285 return false;
286 };
287 Self::obj_is_abs_product_for_abs_builtin(
288 product_side,
289 inner_mul.left.as_ref(),
290 inner_mul.right.as_ref(),
291 )
292 };
293
294 if !matches_abs_product(left, right) && !matches_abs_product(right, left) {
295 return Ok(None);
296 }
297 Ok(Some(factual_equal_success_by_builtin_reason(
298 left,
299 right,
300 line_file,
301 "abs: abs(x * y) = abs(x) * abs(y)",
302 )))
303 }
304
305 fn try_verify_abs_even_power(
308 &mut self,
309 left: &Obj,
310 right: &Obj,
311 line_file: LineFile,
312 ) -> Result<Option<StmtResult>, RuntimeError> {
313 let (Obj::Pow(left_pow), Obj::Pow(right_pow)) = (left, right) else {
314 return Ok(None);
315 };
316 if !objs_equal_by_display_string(left_pow.exponent.as_ref(), right_pow.exponent.as_ref()) {
317 return Ok(None);
318 }
319 let Obj::Number(exp_num) = left_pow.exponent.as_ref() else {
320 return Ok(None);
321 };
322 if !normalized_decimal_string_is_even_integer(&exp_num.normalized_value) {
323 return Ok(None);
324 }
325
326 let bases_match = match (left_pow.base.as_ref(), right_pow.base.as_ref()) {
327 (Obj::Abs(abs), other) => objs_equal_by_display_string(abs.arg.as_ref(), other),
328 (other, Obj::Abs(abs)) => objs_equal_by_display_string(other, abs.arg.as_ref()),
329 _ => false,
330 };
331 if !bases_match {
332 return Ok(None);
333 }
334
335 Ok(Some(factual_equal_success_by_builtin_reason(
336 left,
337 right,
338 line_file,
339 "abs: x^n = abs(x)^n for even integer n",
340 )))
341 }
342
343 fn try_verify_zero_from_abs_zero(
344 &mut self,
345 left: &Obj,
346 right: &Obj,
347 line_file: LineFile,
348 ) -> Result<Option<StmtResult>, RuntimeError> {
349 let zero = Self::literal_zero_obj_for_abs_builtin();
350 let arg = if objs_equal_by_display_string(left, &zero) {
351 right
352 } else if objs_equal_by_display_string(right, &zero) {
353 left
354 } else {
355 return Ok(None);
356 };
357 let abs_arg: Obj = Abs::new(arg.clone()).into();
358 if !self.objs_have_same_known_equality_rc_in_some_env(&abs_arg, &zero) {
359 return Ok(None);
360 }
361 Ok(Some(factual_equal_success_by_builtin_reason(
362 left,
363 right,
364 line_file,
365 "abs: x = 0 from abs(x) = 0",
366 )))
367 }
368
369 fn try_verify_abs_equalities(
370 &mut self,
371 left: &Obj,
372 right: &Obj,
373 line_file: LineFile,
374 verify_state: &VerifyState,
375 ) -> Result<Option<StmtResult>, RuntimeError> {
376 if let Some(done) =
377 self.try_verify_abs_nonnegative_identity(left, right, line_file.clone(), verify_state)?
378 {
379 return Ok(Some(done));
380 }
381 if let Some(done) =
382 self.try_verify_abs_nonpositive_negation(left, right, line_file.clone(), verify_state)?
383 {
384 return Ok(Some(done));
385 }
386 if let Some(done) = self.try_verify_abs_product(left, right, line_file.clone())? {
387 return Ok(Some(done));
388 }
389 if let Some(done) = self.try_verify_abs_even_power(left, right, line_file.clone())? {
390 return Ok(Some(done));
391 }
392 if let Some(done) = self.try_verify_zero_from_abs_zero(left, right, line_file)? {
393 return Ok(Some(done));
394 }
395 Ok(None)
396 }
397
398 fn try_verify_objs_equal_by_expanding_family(
400 &mut self,
401 left: &Obj,
402 right: &Obj,
403 line_file: LineFile,
404 verify_state: &VerifyState,
405 ) -> Result<Option<StmtResult>, RuntimeError> {
406 if let (Obj::FamilyObj(fl), Obj::FamilyObj(fr)) = (left, right) {
407 if let (Ok(el), Ok(er)) = (
408 self.instantiate_family_member_set(fl),
409 self.instantiate_family_member_set(fr),
410 ) {
411 let r = self.verify_objs_are_equal(&el, &er, line_file.clone(), verify_state)?;
412 if r.is_true() {
413 return Ok(Some(factual_equal_success_by_builtin_reason(
414 left,
415 right,
416 line_file,
417 "equality: expand family definition (substitute parameters into equal_to)",
418 )));
419 }
420 }
421 }
422 if let Obj::FamilyObj(f) = left {
423 if let Ok(expanded) = self.instantiate_family_member_set(f) {
424 let r =
425 self.verify_objs_are_equal(&expanded, right, line_file.clone(), verify_state)?;
426 if r.is_true() {
427 return Ok(Some(factual_equal_success_by_builtin_reason(
428 left,
429 right,
430 line_file,
431 "equality: expand family definition (substitute parameters into equal_to)",
432 )));
433 }
434 }
435 }
436 if let Obj::FamilyObj(f) = right {
437 if let Ok(expanded) = self.instantiate_family_member_set(f) {
438 let r =
439 self.verify_objs_are_equal(left, &expanded, line_file.clone(), verify_state)?;
440 if r.is_true() {
441 return Ok(Some(factual_equal_success_by_builtin_reason(
442 left,
443 right,
444 line_file,
445 "equality: expand family definition (substitute parameters into equal_to)",
446 )));
447 }
448 }
449 }
450 Ok(None)
451 }
452
453 fn obj_is_builtin_literal_zero(obj: &Obj) -> bool {
454 match obj {
455 Obj::Number(n) => matches!(
456 compare_normalized_number_str_to_zero(&n.normalized_value),
457 NumberCompareResult::Equal
458 ),
459 _ => false,
460 }
461 }
462
463 fn obj_is_builtin_literal_one(obj: &Obj) -> bool {
464 match obj {
465 Obj::Number(n) => n.normalized_value == "1",
466 _ => false,
467 }
468 }
469
470 fn try_verify_zero_equals_subtraction_implies_equal_operands(
472 &mut self,
473 left: &Obj,
474 right: &Obj,
475 line_file: LineFile,
476 verify_state: &VerifyState,
477 ) -> Result<Option<StmtResult>, RuntimeError> {
478 let (x, y) = if Self::obj_is_builtin_literal_zero(left) {
479 match right {
480 Obj::Sub(s) => (s.left.as_ref(), s.right.as_ref()),
481 _ => return Ok(None),
482 }
483 } else if Self::obj_is_builtin_literal_zero(right) {
484 match left {
485 Obj::Sub(s) => (s.left.as_ref(), s.right.as_ref()),
486 _ => return Ok(None),
487 }
488 } else {
489 return Ok(None);
490 };
491
492 let inner = self.verify_objs_are_equal(x, y, line_file.clone(), verify_state)?;
493 if inner.is_true() {
494 return Ok(Some(factual_equal_success_by_builtin_reason(
495 left,
496 right,
497 line_file,
498 "equality: 0 = x - y with x = y (known or builtin)",
499 )));
500 }
501 Ok(None)
502 }
503
504 fn try_verify_zero_equals_pow_from_base_zero(
506 &mut self,
507 left: &Obj,
508 right: &Obj,
509 line_file: LineFile,
510 verify_state: &VerifyState,
511 ) -> Result<Option<StmtResult>, RuntimeError> {
512 let pow = if Self::obj_is_builtin_literal_zero(left) {
513 match right {
514 Obj::Pow(p) => p,
515 _ => return Ok(None),
516 }
517 } else if Self::obj_is_builtin_literal_zero(right) {
518 match left {
519 Obj::Pow(p) => p,
520 _ => return Ok(None),
521 }
522 } else {
523 return Ok(None);
524 };
525 let Obj::Number(exp_num) = pow.exponent.as_ref() else {
526 return Ok(None);
527 };
528 if !is_integer_after_simplification(exp_num) {
529 return Ok(None);
530 }
531 if !matches!(
532 compare_normalized_number_str_to_zero(&exp_num.normalized_value),
533 NumberCompareResult::Greater
534 ) {
535 return Ok(None);
536 }
537
538 let base = pow.base.as_ref();
539 let zero_side = if Self::obj_is_builtin_literal_zero(left) {
540 left
541 } else {
542 right
543 };
544 let inner = self.verify_objs_are_equal(base, zero_side, line_file.clone(), verify_state)?;
545 if inner.is_true() {
546 return Ok(Some(factual_equal_success_by_builtin_reason(
547 left,
548 right,
549 line_file,
550 "equality: 0 = a^n from a = 0, n positive integer literal",
551 )));
552 }
553 Ok(None)
554 }
555
556 fn try_verify_zero_mod_equals_zero(
559 &mut self,
560 left: &Obj,
561 right: &Obj,
562 line_file: LineFile,
563 ) -> Result<Option<StmtResult>, RuntimeError> {
564 let mod_obj = if Self::obj_is_builtin_literal_zero(left) {
565 match right {
566 Obj::Mod(m) => m,
567 _ => return Ok(None),
568 }
569 } else if Self::obj_is_builtin_literal_zero(right) {
570 match left {
571 Obj::Mod(m) => m,
572 _ => return Ok(None),
573 }
574 } else {
575 return Ok(None);
576 };
577 if !Self::obj_is_builtin_literal_zero(mod_obj.left.as_ref()) {
578 return Ok(None);
579 }
580 Ok(Some(factual_equal_success_by_builtin_reason(
581 left,
582 right,
583 line_file,
584 "equality: 0 % m = 0",
585 )))
586 }
587
588 fn try_verify_pow_one_identity(
591 &mut self,
592 left: &Obj,
593 right: &Obj,
594 line_file: LineFile,
595 verify_state: &VerifyState,
596 ) -> Result<Option<StmtResult>, RuntimeError> {
597 let (pow, other) = match (left, right) {
598 (Obj::Pow(p), other) => (p, other),
599 (other, Obj::Pow(p)) => (p, other),
600 _ => return Ok(None),
601 };
602 if !Self::obj_is_builtin_literal_one(pow.exponent.as_ref()) {
603 return Ok(None);
604 }
605 if !self
606 .verify_objs_are_equal(pow.base.as_ref(), other, line_file.clone(), verify_state)?
607 .is_true()
608 {
609 return Ok(None);
610 }
611 Ok(Some(factual_equal_success_by_builtin_reason(
612 left,
613 right,
614 line_file,
615 "equality: a^1 = a",
616 )))
617 }
618
619 fn power_factor_matches_base_and_exponent(
620 &mut self,
621 factor: &Obj,
622 base: &Obj,
623 exponent: &Obj,
624 line_file: LineFile,
625 verify_state: &VerifyState,
626 ) -> Result<bool, RuntimeError> {
627 let Obj::Pow(pow) = factor else {
628 if !Self::obj_is_builtin_literal_one(exponent) {
629 return Ok(false);
630 }
631 return Ok(self
632 .verify_objs_are_equal(base, factor, line_file.clone(), verify_state)?
633 .is_true());
634 };
635 if !self
636 .verify_objs_are_equal(base, pow.base.as_ref(), line_file.clone(), verify_state)?
637 .is_true()
638 {
639 return Ok(false);
640 }
641 Ok(self
642 .verify_objs_are_equal(
643 exponent,
644 pow.exponent.as_ref(),
645 line_file.clone(),
646 verify_state,
647 )?
648 .is_true())
649 }
650
651 fn obj_is_verified_in_n_pos(
652 &mut self,
653 obj: &Obj,
654 line_file: LineFile,
655 verify_state: &VerifyState,
656 ) -> Result<bool, RuntimeError> {
657 let in_n_pos: AtomicFact =
658 InFact::new(obj.clone(), StandardSet::NPos.into(), line_file).into();
659 Ok(self
660 .verify_non_equational_known_then_builtin_rules_only(&in_n_pos, verify_state)?
661 .is_true())
662 }
663
664 fn power_addition_exponent_rule_holds_one_direction(
665 &mut self,
666 combined_power: &Pow,
667 product: &Mul,
668 line_file: LineFile,
669 verify_state: &VerifyState,
670 ) -> Result<bool, RuntimeError> {
671 let Obj::Add(add_exponent) = combined_power.exponent.as_ref() else {
672 return Ok(false);
673 };
674
675 let candidates = [
678 (
679 product.left.as_ref(),
680 product.right.as_ref(),
681 add_exponent.left.as_ref(),
682 add_exponent.right.as_ref(),
683 ),
684 (
685 product.right.as_ref(),
686 product.left.as_ref(),
687 add_exponent.left.as_ref(),
688 add_exponent.right.as_ref(),
689 ),
690 ];
691
692 for (left_factor, right_factor, left_exp, right_exp) in candidates {
693 if !self.power_factor_matches_base_and_exponent(
694 left_factor,
695 combined_power.base.as_ref(),
696 left_exp,
697 line_file.clone(),
698 verify_state,
699 )? {
700 continue;
701 }
702 if !self.power_factor_matches_base_and_exponent(
703 right_factor,
704 combined_power.base.as_ref(),
705 right_exp,
706 line_file.clone(),
707 verify_state,
708 )? {
709 continue;
710 }
711 if !self.obj_is_verified_in_n_pos(left_exp, line_file.clone(), verify_state)? {
712 return Ok(false);
713 }
714 if !self.obj_is_verified_in_n_pos(right_exp, line_file.clone(), verify_state)? {
715 return Ok(false);
716 }
717 return Ok(true);
718 }
719
720 Ok(false)
721 }
722
723 fn try_verify_power_addition_exponent_rule(
724 &mut self,
725 left: &Obj,
726 right: &Obj,
727 line_file: LineFile,
728 verify_state: &VerifyState,
729 ) -> Result<Option<StmtResult>, RuntimeError> {
730 let holds = match (left, right) {
731 (Obj::Pow(pow), Obj::Mul(product)) => self
732 .power_addition_exponent_rule_holds_one_direction(
733 pow,
734 product,
735 line_file.clone(),
736 verify_state,
737 )?,
738 (Obj::Mul(product), Obj::Pow(pow)) => self
739 .power_addition_exponent_rule_holds_one_direction(
740 pow,
741 product,
742 line_file.clone(),
743 verify_state,
744 )?,
745 _ => false,
746 };
747 if holds {
748 return Ok(Some(factual_equal_success_by_builtin_reason(
749 left,
750 right,
751 line_file,
752 "equality: a^(m+n) = a^m * a^n for m,n in N_pos",
753 )));
754 }
755 Ok(None)
756 }
757
758 fn verify_context_arg_equality(
759 &mut self,
760 left: &Obj,
761 right: &Obj,
762 line_file: LineFile,
763 verify_state: &VerifyState,
764 ) -> Result<bool, RuntimeError> {
765 Ok(self
766 .verify_objs_are_equal(left, right, line_file, verify_state)?
767 .is_true())
768 }
769
770 fn try_verify_same_algebra_context_by_equal_args(
773 &mut self,
774 left: &Obj,
775 right: &Obj,
776 line_file: LineFile,
777 verify_state: &VerifyState,
778 ) -> Result<Option<StmtResult>, RuntimeError> {
779 let args_equal = match (left, right) {
780 (Obj::Add(l), Obj::Add(r)) => {
781 self.verify_context_arg_equality(
782 l.left.as_ref(),
783 r.left.as_ref(),
784 line_file.clone(),
785 verify_state,
786 )? && self.verify_context_arg_equality(
787 l.right.as_ref(),
788 r.right.as_ref(),
789 line_file.clone(),
790 verify_state,
791 )?
792 }
793 (Obj::Sub(l), Obj::Sub(r)) => {
794 self.verify_context_arg_equality(
795 l.left.as_ref(),
796 r.left.as_ref(),
797 line_file.clone(),
798 verify_state,
799 )? && self.verify_context_arg_equality(
800 l.right.as_ref(),
801 r.right.as_ref(),
802 line_file.clone(),
803 verify_state,
804 )?
805 }
806 (Obj::Mul(l), Obj::Mul(r)) => {
807 self.verify_context_arg_equality(
808 l.left.as_ref(),
809 r.left.as_ref(),
810 line_file.clone(),
811 verify_state,
812 )? && self.verify_context_arg_equality(
813 l.right.as_ref(),
814 r.right.as_ref(),
815 line_file.clone(),
816 verify_state,
817 )?
818 }
819 (Obj::Div(l), Obj::Div(r)) => {
820 self.verify_context_arg_equality(
821 l.left.as_ref(),
822 r.left.as_ref(),
823 line_file.clone(),
824 verify_state,
825 )? && self.verify_context_arg_equality(
826 l.right.as_ref(),
827 r.right.as_ref(),
828 line_file.clone(),
829 verify_state,
830 )?
831 }
832 (Obj::Mod(l), Obj::Mod(r)) => {
833 self.verify_context_arg_equality(
834 l.left.as_ref(),
835 r.left.as_ref(),
836 line_file.clone(),
837 verify_state,
838 )? && self.verify_context_arg_equality(
839 l.right.as_ref(),
840 r.right.as_ref(),
841 line_file.clone(),
842 verify_state,
843 )?
844 }
845 (Obj::Pow(l), Obj::Pow(r)) => {
846 self.verify_context_arg_equality(
847 l.base.as_ref(),
848 r.base.as_ref(),
849 line_file.clone(),
850 verify_state,
851 )? && self.verify_context_arg_equality(
852 l.exponent.as_ref(),
853 r.exponent.as_ref(),
854 line_file.clone(),
855 verify_state,
856 )?
857 }
858 _ => return Ok(None),
859 };
860 if !args_equal {
861 return Ok(None);
862 }
863 Ok(Some(factual_equal_success_by_builtin_reason(
864 left,
865 right,
866 line_file,
867 "equality: same algebraic context with equal arguments",
868 )))
869 }
870
871 fn try_verify_log_identity_equalities(
873 &mut self,
874 left: &Obj,
875 right: &Obj,
876 line_file: LineFile,
877 verify_state: &VerifyState,
878 ) -> Result<Option<StmtResult>, RuntimeError> {
879 let (log, other) = match (left, right) {
880 (Obj::Log(l), o) => (l, o),
881 (o, Obj::Log(l)) => (l, o),
882 _ => return Ok(None),
883 };
884
885 if let Obj::Pow(p) = log.arg.as_ref() {
886 let base_ok = self.verify_objs_are_equal(
887 p.base.as_ref(),
888 log.base.as_ref(),
889 line_file.clone(),
890 verify_state,
891 )?;
892 if base_ok.is_true() {
893 let exp_ok = self.verify_objs_are_equal(
894 p.exponent.as_ref(),
895 other,
896 line_file.clone(),
897 verify_state,
898 )?;
899 if exp_ok.is_true() {
900 return Ok(Some(factual_equal_success_by_builtin_reason(
901 left,
902 right,
903 line_file,
904 "equality: log(a, a^b) = b",
905 )));
906 }
907 }
908 }
909
910 Ok(None)
911 }
912
913 fn try_verify_log_base_power_rule(
915 &mut self,
916 left: &Obj,
917 right: &Obj,
918 line_file: LineFile,
919 verify_state: &VerifyState,
920 ) -> Result<Option<StmtResult>, RuntimeError> {
921 let (log, other) = match (left, right) {
922 (Obj::Log(l), o) => (l, o),
923 (o, Obj::Log(l)) => (l, o),
924 _ => return Ok(None),
925 };
926 let Obj::Pow(p) = log.base.as_ref() else {
927 return Ok(None);
928 };
929 let inner_log: Obj = Log::new((*p.base).clone(), (*log.arg).clone()).into();
930 let expected: Obj = Div::new(inner_log, (*p.exponent).clone()).into();
931 let inner =
932 self.verify_objs_are_equal(other, &expected, line_file.clone(), verify_state)?;
933 if inner.is_true() {
934 return Ok(Some(factual_equal_success_by_builtin_reason(
935 left,
936 right,
937 line_file,
938 "equality: log(a^b, c) = log(a, c) / b",
939 )));
940 }
941 Ok(None)
942 }
943
944 fn try_verify_log_arg_power_rule(
946 &mut self,
947 left: &Obj,
948 right: &Obj,
949 line_file: LineFile,
950 verify_state: &VerifyState,
951 ) -> Result<Option<StmtResult>, RuntimeError> {
952 let (log, other) = match (left, right) {
953 (Obj::Log(l), o) => (l, o),
954 (o, Obj::Log(l)) => (l, o),
955 _ => return Ok(None),
956 };
957 let Obj::Pow(p) = log.arg.as_ref() else {
958 return Ok(None);
959 };
960 let inner_log: Obj = Log::new((*log.base).clone(), (*p.base).clone()).into();
961 let expected1: Obj = Mul::new((*p.exponent).clone(), inner_log.clone()).into();
962 let expected2: Obj = Mul::new(inner_log, (*p.exponent).clone()).into();
963 for expected in [expected1, expected2] {
964 let inner =
965 self.verify_objs_are_equal(other, &expected, line_file.clone(), verify_state)?;
966 if inner.is_true() {
967 return Ok(Some(factual_equal_success_by_builtin_reason(
968 left,
969 right,
970 line_file,
971 "equality: log(a, x^b) = b * log(a, x)",
972 )));
973 }
974 }
975 Ok(None)
976 }
977
978 fn try_verify_log_product_rule(
980 &mut self,
981 left: &Obj,
982 right: &Obj,
983 line_file: LineFile,
984 verify_state: &VerifyState,
985 ) -> Result<Option<StmtResult>, RuntimeError> {
986 let (log, other) = match (left, right) {
987 (Obj::Log(l), o) => (l, o),
988 (o, Obj::Log(l)) => (l, o),
989 _ => return Ok(None),
990 };
991 let Obj::Mul(m) = log.arg.as_ref() else {
992 return Ok(None);
993 };
994 let l1: Obj = Log::new((*log.base).clone(), (*m.left).clone()).into();
995 let l2: Obj = Log::new((*log.base).clone(), (*m.right).clone()).into();
996 let expected1: Obj = Add::new(l1.clone(), l2.clone()).into();
997 let expected2: Obj = Add::new(l2, l1).into();
998 for expected in [expected1, expected2] {
999 let inner =
1000 self.verify_objs_are_equal(other, &expected, line_file.clone(), verify_state)?;
1001 if inner.is_true() {
1002 return Ok(Some(factual_equal_success_by_builtin_reason(
1003 left,
1004 right,
1005 line_file,
1006 "equality: log(a, x*y) = log(a, x) + log(a, y)",
1007 )));
1008 }
1009 }
1010 Ok(None)
1011 }
1012
1013 fn try_verify_log_quotient_rule(
1015 &mut self,
1016 left: &Obj,
1017 right: &Obj,
1018 line_file: LineFile,
1019 verify_state: &VerifyState,
1020 ) -> Result<Option<StmtResult>, RuntimeError> {
1021 let (log, other) = match (left, right) {
1022 (Obj::Log(l), o) => (l, o),
1023 (o, Obj::Log(l)) => (l, o),
1024 _ => return Ok(None),
1025 };
1026 let Obj::Div(d) = log.arg.as_ref() else {
1027 return Ok(None);
1028 };
1029 let l1: Obj = Log::new((*log.base).clone(), (*d.left).clone()).into();
1030 let l2: Obj = Log::new((*log.base).clone(), (*d.right).clone()).into();
1031 let expected = Sub::new(l1, l2).into();
1032 let inner =
1033 self.verify_objs_are_equal(other, &expected, line_file.clone(), verify_state)?;
1034 if inner.is_true() {
1035 return Ok(Some(factual_equal_success_by_builtin_reason(
1036 left,
1037 right,
1038 line_file,
1039 "equality: log(a, x/y) = log(a, x) - log(a, y)",
1040 )));
1041 }
1042 Ok(None)
1043 }
1044
1045 fn try_verify_log_algebra_identities(
1047 &mut self,
1048 left: &Obj,
1049 right: &Obj,
1050 line_file: LineFile,
1051 verify_state: &VerifyState,
1052 ) -> Result<Option<StmtResult>, RuntimeError> {
1053 if let Some(done) =
1054 self.try_verify_log_base_power_rule(left, right, line_file.clone(), verify_state)?
1055 {
1056 return Ok(Some(done));
1057 }
1058 if let Some(done) =
1059 self.try_verify_log_arg_power_rule(left, right, line_file.clone(), verify_state)?
1060 {
1061 return Ok(Some(done));
1062 }
1063 if let Some(done) =
1064 self.try_verify_log_product_rule(left, right, line_file.clone(), verify_state)?
1065 {
1066 return Ok(Some(done));
1067 }
1068 if let Some(done) =
1069 self.try_verify_log_quotient_rule(left, right, line_file.clone(), verify_state)?
1070 {
1071 return Ok(Some(done));
1072 }
1073 Ok(None)
1074 }
1075
1076 fn try_verify_anonymous_fn_application_equals_other_side(
1079 &mut self,
1080 statement_left: &Obj,
1081 statement_right: &Obj,
1082 application_side: &Obj,
1083 other_side: &Obj,
1084 line_file: LineFile,
1085 verify_state: &VerifyState,
1086 ) -> Result<Option<StmtResult>, RuntimeError> {
1087 let Obj::FnObj(fn_obj) = application_side else {
1088 return Ok(None);
1089 };
1090 let FnObjHead::AnonymousFnLiteral(af) = fn_obj.head.as_ref() else {
1091 return Ok(None);
1092 };
1093 if fn_obj.body.is_empty() {
1094 return Ok(None);
1095 }
1096 let param_defs = &af.body.params_def_with_set;
1097 let n_params = ParamGroupWithSet::number_of_params(param_defs);
1098 if n_params == 0 {
1099 return Ok(None);
1100 }
1101 let mut args: Vec<Obj> = Vec::new();
1102 for g in fn_obj.body.iter() {
1103 for b in g.iter() {
1104 args.push((**b).clone());
1105 }
1106 }
1107 if args.len() != n_params {
1108 return Ok(None);
1109 }
1110 let param_to_arg_map =
1111 ParamGroupWithSet::param_defs_and_args_to_param_to_arg_map(param_defs, &args);
1112 let reduced =
1113 self.inst_obj(af.equal_to.as_ref(), ¶m_to_arg_map, ParamObjType::FnSet)?;
1114 let inner =
1115 self.verify_objs_are_equal(&reduced, other_side, line_file.clone(), verify_state)?;
1116 if inner.is_true() {
1117 return Ok(Some(factual_equal_success_by_builtin_reason(
1118 statement_left,
1119 statement_right,
1120 line_file,
1121 "equality: anonymous function application — substitute args into the body, equals the other side",
1122 )));
1123 }
1124 Ok(None)
1125 }
1126
1127 fn try_verify_log_equals_by_pow_inverse(
1129 &mut self,
1130 left: &Obj,
1131 right: &Obj,
1132 line_file: LineFile,
1133 verify_state: &VerifyState,
1134 ) -> Result<Option<StmtResult>, RuntimeError> {
1135 let (log, other) = match (left, right) {
1136 (Obj::Log(l), o) => (l, o),
1137 (o, Obj::Log(l)) => (l, o),
1138 _ => return Ok(None),
1139 };
1140 let pow_obj: Obj = Pow::new((*log.base).clone(), other.clone()).into();
1141 let inner = self.verify_objs_are_equal(
1142 &pow_obj,
1143 log.arg.as_ref(),
1144 line_file.clone(),
1145 verify_state,
1146 )?;
1147 if inner.is_true() {
1148 return Ok(Some(factual_equal_success_by_builtin_reason(
1149 left,
1150 right,
1151 line_file,
1152 "equality: log(a, b) = c from a^c = b",
1153 )));
1154 }
1155 Ok(None)
1156 }
1157
1158 fn try_verify_sum_additivity(
1161 &mut self,
1162 left: &Obj,
1163 right: &Obj,
1164 line_file: LineFile,
1165 verify_state: &VerifyState,
1166 ) -> Result<Option<StmtResult>, RuntimeError> {
1167 if !verify_state.is_round_0() {
1168 return Ok(None);
1169 }
1170
1171 let (sum_m, sum_a, sum_b) = match (left, right) {
1172 (Obj::Sum(m), Obj::Add(a)) => match (a.left.as_ref(), a.right.as_ref()) {
1173 (Obj::Sum(a1), Obj::Sum(a2)) => (m, a1, a2),
1174 _ => return Ok(None),
1175 },
1176 (Obj::Add(a), Obj::Sum(m)) => match (a.left.as_ref(), a.right.as_ref()) {
1177 (Obj::Sum(a1), Obj::Sum(a2)) => (m, a1, a2),
1178 _ => return Ok(None),
1179 },
1180 _ => return Ok(None),
1181 };
1182
1183 let mut require_eq = |a: &Obj, b: &Obj| -> Result<bool, RuntimeError> {
1184 Ok(self
1185 .verify_objs_are_equal(a, b, line_file.clone(), verify_state)?
1186 .is_true())
1187 };
1188 if !require_eq(sum_m.start.as_ref(), sum_a.start.as_ref())? {
1189 return Ok(None);
1190 }
1191 if !require_eq(sum_m.start.as_ref(), sum_b.start.as_ref())? {
1192 return Ok(None);
1193 }
1194 if !require_eq(sum_m.end.as_ref(), sum_a.end.as_ref())? {
1195 return Ok(None);
1196 }
1197 if !require_eq(sum_m.end.as_ref(), sum_b.end.as_ref())? {
1198 return Ok(None);
1199 }
1200
1201 let x_name = self.generate_random_unused_name();
1202 let x_obj = obj_for_bound_param_in_scope(x_name.clone(), ParamObjType::Forall);
1203
1204 let Some(l_inst) =
1205 self.instantiate_unary_anonymous_summand_at(sum_m.func.as_ref(), &x_obj)?
1206 else {
1207 return Ok(None);
1208 };
1209 let Some(a_inst) =
1210 self.instantiate_unary_anonymous_summand_at(sum_a.func.as_ref(), &x_obj)?
1211 else {
1212 return Ok(None);
1213 };
1214 let Some(b_inst) =
1215 self.instantiate_unary_anonymous_summand_at(sum_b.func.as_ref(), &x_obj)?
1216 else {
1217 return Ok(None);
1218 };
1219
1220 let then_fact: ExistOrAndChainAtomicFact =
1221 EqualFact::new(l_inst, Add::new(a_inst, b_inst).into(), line_file.clone()).into();
1222
1223 let dom_lo: Fact =
1224 LessEqualFact::new((*sum_m.start).clone(), x_obj.clone(), line_file.clone()).into();
1225 let dom_hi: Fact =
1226 LessEqualFact::new(x_obj.clone(), (*sum_m.end).clone(), line_file.clone()).into();
1227
1228 let forall_fact: Fact = ForallFact::new(
1229 ParamDefWithType::new(vec![ParamGroupWithParamType::new(
1230 vec![x_name],
1231 ParamType::Obj(StandardSet::Z.into()),
1232 )]),
1233 vec![dom_lo, dom_hi],
1234 vec![then_fact],
1235 line_file.clone(),
1236 )?
1237 .into();
1238
1239 let r = self.verify_fact(&forall_fact, verify_state)?;
1240 if r.is_true() {
1241 return Ok(Some(factual_equal_success_by_builtin_reason(
1242 left,
1243 right,
1244 line_file,
1245 "equality: sum additivity from pointwise equality on the integer index range",
1246 )));
1247 }
1248 Ok(None)
1249 }
1250
1251 fn instantiate_unary_anonymous_summand_at(
1252 &mut self,
1253 func: &Obj,
1254 x: &Obj,
1255 ) -> Result<Option<Obj>, RuntimeError> {
1256 let af: &AnonymousFn = match func {
1257 Obj::AnonymousFn(af) => af,
1258 Obj::FnObj(fo) => {
1259 if !fo.body.is_empty() {
1260 return Ok(None);
1261 }
1262 match fo.head.as_ref() {
1263 FnObjHead::AnonymousFnLiteral(a) => a.as_ref(),
1264 _ => return Ok(None),
1265 }
1266 }
1267 _ => return Ok(None),
1268 };
1269 if ParamGroupWithSet::number_of_params(&af.body.params_def_with_set) != 1 {
1270 return Ok(None);
1271 }
1272 let param_defs = &af.body.params_def_with_set;
1273 let args = vec![x.clone()];
1274 let param_to_arg_map =
1275 ParamGroupWithSet::param_defs_and_args_to_param_to_arg_map(param_defs, &args);
1276 Ok(Some(self.inst_obj(
1277 af.equal_to.as_ref(),
1278 ¶m_to_arg_map,
1279 ParamObjType::FnSet,
1280 )?))
1281 }
1282
1283 fn try_verify_sum_merge_adjacent_ranges(
1285 &mut self,
1286 left: &Obj,
1287 right: &Obj,
1288 line_file: LineFile,
1289 verify_state: &VerifyState,
1290 ) -> Result<Option<StmtResult>, RuntimeError> {
1291 if !verify_state.is_round_0() {
1292 return Ok(None);
1293 }
1294 let (add, s3) = match (left, right) {
1295 (Obj::Add(a), Obj::Sum(s)) => (a, s),
1296 (Obj::Sum(s), Obj::Add(a)) => (a, s),
1297 _ => return Ok(None),
1298 };
1299 let (s1, s2) = match (add.left.as_ref(), add.right.as_ref()) {
1300 (Obj::Sum(x), Obj::Sum(y)) => (x, y),
1301 _ => return Ok(None),
1302 };
1303 for (a, b) in [(s1, s2), (s2, s1)] {
1304 if let Some(done) = self.try_verify_sum_merge_ordered_pair(
1305 a,
1306 b,
1307 s3,
1308 left,
1309 right,
1310 line_file.clone(),
1311 verify_state,
1312 )? {
1313 return Ok(Some(done));
1314 }
1315 }
1316 Ok(None)
1317 }
1318
1319 fn try_verify_sum_merge_ordered_pair(
1320 &mut self,
1321 s1: &Sum,
1322 s2: &Sum,
1323 s3: &Sum,
1324 stmt_left: &Obj,
1325 stmt_right: &Obj,
1326 line_file: LineFile,
1327 verify_state: &VerifyState,
1328 ) -> Result<Option<StmtResult>, RuntimeError> {
1329 let one: Obj = Number::new("1".to_string()).into();
1330 let gap = Add::new((*s1.end).clone(), one).into();
1331 if !self
1332 .verify_objs_are_equal(&gap, s2.start.as_ref(), line_file.clone(), verify_state)?
1333 .is_true()
1334 {
1335 return Ok(None);
1336 }
1337 if !self
1338 .verify_objs_are_equal(
1339 s1.start.as_ref(),
1340 s3.start.as_ref(),
1341 line_file.clone(),
1342 verify_state,
1343 )?
1344 .is_true()
1345 {
1346 return Ok(None);
1347 }
1348 if !self
1349 .verify_objs_are_equal(
1350 s2.end.as_ref(),
1351 s3.end.as_ref(),
1352 line_file.clone(),
1353 verify_state,
1354 )?
1355 .is_true()
1356 {
1357 return Ok(None);
1358 }
1359 if !self
1360 .verify_objs_are_equal(
1361 s1.func.as_ref(),
1362 s2.func.as_ref(),
1363 line_file.clone(),
1364 verify_state,
1365 )?
1366 .is_true()
1367 {
1368 return Ok(None);
1369 }
1370 if !self
1371 .verify_objs_are_equal(
1372 s1.func.as_ref(),
1373 s3.func.as_ref(),
1374 line_file.clone(),
1375 verify_state,
1376 )?
1377 .is_true()
1378 {
1379 return Ok(None);
1380 }
1381 Ok(Some(factual_equal_success_by_builtin_reason(
1382 stmt_left,
1383 stmt_right,
1384 line_file,
1385 "equality: merge adjacent sum ranges with the same summand",
1386 )))
1387 }
1388
1389 fn try_verify_sum_split_last_term(
1391 &mut self,
1392 left: &Obj,
1393 right: &Obj,
1394 line_file: LineFile,
1395 verify_state: &VerifyState,
1396 ) -> Result<Option<StmtResult>, RuntimeError> {
1397 if !verify_state.is_round_0() {
1398 return Ok(None);
1399 }
1400 let one: Obj = Number::new("1".to_string()).into();
1401 for (full_obj, add_obj) in [(left, right), (right, left)] {
1402 let Obj::Sum(s_full) = full_obj else {
1403 continue;
1404 };
1405 let Obj::Add(a) = add_obj else {
1406 continue;
1407 };
1408 for (sum_part, tail) in [
1409 (a.left.as_ref(), a.right.as_ref()),
1410 (a.right.as_ref(), a.left.as_ref()),
1411 ] {
1412 let Obj::Sum(s_pre) = sum_part else {
1413 continue;
1414 };
1415 if !self
1416 .verify_objs_are_equal(
1417 s_full.start.as_ref(),
1418 s_pre.start.as_ref(),
1419 line_file.clone(),
1420 verify_state,
1421 )?
1422 .is_true()
1423 {
1424 continue;
1425 }
1426 let end_pre_plus_one: Obj = Add::new((*s_pre.end).clone(), one.clone()).into();
1427 if !self
1428 .verify_objs_are_equal(
1429 s_full.end.as_ref(),
1430 &end_pre_plus_one,
1431 line_file.clone(),
1432 verify_state,
1433 )?
1434 .is_true()
1435 {
1436 continue;
1437 }
1438 if !self
1439 .verify_objs_are_equal(
1440 s_full.func.as_ref(),
1441 s_pre.func.as_ref(),
1442 line_file.clone(),
1443 verify_state,
1444 )?
1445 .is_true()
1446 {
1447 continue;
1448 }
1449 let Some(expected_tail) = self.instantiate_unary_anonymous_summand_at(
1450 s_full.func.as_ref(),
1451 s_full.end.as_ref(),
1452 )?
1453 else {
1454 continue;
1455 };
1456 if !self
1457 .verify_objs_are_equal(&expected_tail, tail, line_file.clone(), verify_state)?
1458 .is_true()
1459 {
1460 continue;
1461 }
1462 return Ok(Some(factual_equal_success_by_builtin_reason(
1463 left,
1464 right,
1465 line_file,
1466 "equality: sum through e equals sum through e-1 plus last summand f(e)",
1467 )));
1468 }
1469 }
1470 Ok(None)
1471 }
1472
1473 fn try_verify_product_split_last_term(
1475 &mut self,
1476 left: &Obj,
1477 right: &Obj,
1478 line_file: LineFile,
1479 verify_state: &VerifyState,
1480 ) -> Result<Option<StmtResult>, RuntimeError> {
1481 if !verify_state.is_round_0() {
1482 return Ok(None);
1483 }
1484 let one: Obj = Number::new("1".to_string()).into();
1485 for (full_obj, mul_obj) in [(left, right), (right, left)] {
1486 let Obj::Product(p_full) = full_obj else {
1487 continue;
1488 };
1489 let Obj::Mul(m) = mul_obj else {
1490 continue;
1491 };
1492 for (prod_part, tail) in [
1493 (m.left.as_ref(), m.right.as_ref()),
1494 (m.right.as_ref(), m.left.as_ref()),
1495 ] {
1496 let Obj::Product(p_pre) = prod_part else {
1497 continue;
1498 };
1499 if !self
1500 .verify_objs_are_equal(
1501 p_full.start.as_ref(),
1502 p_pre.start.as_ref(),
1503 line_file.clone(),
1504 verify_state,
1505 )?
1506 .is_true()
1507 {
1508 continue;
1509 }
1510 let end_pre_plus_one: Obj = Add::new((*p_pre.end).clone(), one.clone()).into();
1511 if !self
1512 .verify_objs_are_equal(
1513 p_full.end.as_ref(),
1514 &end_pre_plus_one,
1515 line_file.clone(),
1516 verify_state,
1517 )?
1518 .is_true()
1519 {
1520 continue;
1521 }
1522 if !self
1523 .verify_objs_are_equal(
1524 p_full.func.as_ref(),
1525 p_pre.func.as_ref(),
1526 line_file.clone(),
1527 verify_state,
1528 )?
1529 .is_true()
1530 {
1531 continue;
1532 }
1533 let Some(expected_tail) = self.instantiate_unary_anonymous_summand_at(
1534 p_full.func.as_ref(),
1535 p_full.end.as_ref(),
1536 )?
1537 else {
1538 continue;
1539 };
1540 if !self
1541 .verify_objs_are_equal(&expected_tail, tail, line_file.clone(), verify_state)?
1542 .is_true()
1543 {
1544 continue;
1545 }
1546 return Ok(Some(factual_equal_success_by_builtin_reason(
1547 left,
1548 right,
1549 line_file,
1550 "equality: product through e equals product through e-1 times last factor f(e)",
1551 )));
1552 }
1553 }
1554 Ok(None)
1555 }
1556
1557 fn flatten_left_assoc_add_chain(obj: &Obj) -> Vec<&Obj> {
1558 match obj {
1559 Obj::Add(a) => {
1560 let mut v = Self::flatten_left_assoc_add_chain(a.left.as_ref());
1561 v.push(a.right.as_ref());
1562 v
1563 }
1564 _ => vec![obj],
1565 }
1566 }
1567
1568 fn flatten_left_assoc_mul_chain(obj: &Obj) -> Vec<&Obj> {
1569 match obj {
1570 Obj::Mul(m) => {
1571 let mut v = Self::flatten_left_assoc_mul_chain(m.left.as_ref());
1572 v.push(m.right.as_ref());
1573 v
1574 }
1575 _ => vec![obj],
1576 }
1577 }
1578
1579 fn try_verify_sum_partition_adjacent_ranges(
1581 &mut self,
1582 left: &Obj,
1583 right: &Obj,
1584 line_file: LineFile,
1585 verify_state: &VerifyState,
1586 ) -> Result<Option<StmtResult>, RuntimeError> {
1587 if !verify_state.is_round_0() {
1588 return Ok(None);
1589 }
1590 let one: Obj = Number::new("1".to_string()).into();
1591 for (full_side, add_side) in [(left, right), (right, left)] {
1592 let Obj::Sum(s_full) = full_side else {
1593 continue;
1594 };
1595 let Obj::Add(_) = add_side else {
1596 continue;
1597 };
1598 let parts = Self::flatten_left_assoc_add_chain(add_side);
1599 if parts.len() < 2 {
1600 continue;
1601 }
1602 let mut sums: Vec<&Sum> = Vec::with_capacity(parts.len());
1603 let mut all_sum = true;
1604 for p in &parts {
1605 if let Obj::Sum(s) = p {
1606 sums.push(s);
1607 } else {
1608 all_sum = false;
1609 break;
1610 }
1611 }
1612 if !all_sum {
1613 continue;
1614 }
1615 if !self
1616 .verify_objs_are_equal(
1617 s_full.start.as_ref(),
1618 sums[0].start.as_ref(),
1619 line_file.clone(),
1620 verify_state,
1621 )?
1622 .is_true()
1623 {
1624 continue;
1625 }
1626 if !self
1627 .verify_objs_are_equal(
1628 s_full.end.as_ref(),
1629 sums[sums.len() - 1].end.as_ref(),
1630 line_file.clone(),
1631 verify_state,
1632 )?
1633 .is_true()
1634 {
1635 continue;
1636 }
1637 let mut gaps_ok = true;
1638 for i in 0..sums.len().saturating_sub(1) {
1639 let gap = Add::new((*sums[i].end).clone(), one.clone()).into();
1640 if !self
1641 .verify_objs_are_equal(
1642 &gap,
1643 sums[i + 1].start.as_ref(),
1644 line_file.clone(),
1645 verify_state,
1646 )?
1647 .is_true()
1648 {
1649 gaps_ok = false;
1650 break;
1651 }
1652 }
1653 if !gaps_ok {
1654 continue;
1655 }
1656 let mut func_ok = true;
1657 for s in &sums {
1658 if !self
1659 .verify_objs_are_equal(
1660 s_full.func.as_ref(),
1661 s.func.as_ref(),
1662 line_file.clone(),
1663 verify_state,
1664 )?
1665 .is_true()
1666 {
1667 func_ok = false;
1668 break;
1669 }
1670 }
1671 if !func_ok {
1672 continue;
1673 }
1674 return Ok(Some(factual_equal_success_by_builtin_reason(
1675 left,
1676 right,
1677 line_file,
1678 "equality: sum partitions closed range into adjacent sub-sums with the same summand",
1679 )));
1680 }
1681 Ok(None)
1682 }
1683
1684 fn try_verify_product_partition_adjacent_ranges(
1686 &mut self,
1687 left: &Obj,
1688 right: &Obj,
1689 line_file: LineFile,
1690 verify_state: &VerifyState,
1691 ) -> Result<Option<StmtResult>, RuntimeError> {
1692 if !verify_state.is_round_0() {
1693 return Ok(None);
1694 }
1695 let one: Obj = Number::new("1".to_string()).into();
1696 for (full_side, mul_side) in [(left, right), (right, left)] {
1697 let Obj::Product(p_full) = full_side else {
1698 continue;
1699 };
1700 let Obj::Mul(_) = mul_side else {
1701 continue;
1702 };
1703 let parts = Self::flatten_left_assoc_mul_chain(mul_side);
1704 if parts.len() < 2 {
1705 continue;
1706 }
1707 let mut products: Vec<&Product> = Vec::with_capacity(parts.len());
1708 let mut all_prod = true;
1709 for p in &parts {
1710 if let Obj::Product(pr) = p {
1711 products.push(pr);
1712 } else {
1713 all_prod = false;
1714 break;
1715 }
1716 }
1717 if !all_prod {
1718 continue;
1719 }
1720 if !self
1721 .verify_objs_are_equal(
1722 p_full.start.as_ref(),
1723 products[0].start.as_ref(),
1724 line_file.clone(),
1725 verify_state,
1726 )?
1727 .is_true()
1728 {
1729 continue;
1730 }
1731 if !self
1732 .verify_objs_are_equal(
1733 p_full.end.as_ref(),
1734 products[products.len() - 1].end.as_ref(),
1735 line_file.clone(),
1736 verify_state,
1737 )?
1738 .is_true()
1739 {
1740 continue;
1741 }
1742 let mut gaps_ok = true;
1743 for i in 0..products.len().saturating_sub(1) {
1744 let gap = Add::new((*products[i].end).clone(), one.clone()).into();
1745 if !self
1746 .verify_objs_are_equal(
1747 &gap,
1748 products[i + 1].start.as_ref(),
1749 line_file.clone(),
1750 verify_state,
1751 )?
1752 .is_true()
1753 {
1754 gaps_ok = false;
1755 break;
1756 }
1757 }
1758 if !gaps_ok {
1759 continue;
1760 }
1761 let mut func_ok = true;
1762 for p in &products {
1763 if !self
1764 .verify_objs_are_equal(
1765 p_full.func.as_ref(),
1766 p.func.as_ref(),
1767 line_file.clone(),
1768 verify_state,
1769 )?
1770 .is_true()
1771 {
1772 func_ok = false;
1773 break;
1774 }
1775 }
1776 if !func_ok {
1777 continue;
1778 }
1779 return Ok(Some(factual_equal_success_by_builtin_reason(
1780 left,
1781 right,
1782 line_file,
1783 "equality: product partitions closed range into adjacent sub-products with the same factor",
1784 )));
1785 }
1786 Ok(None)
1787 }
1788
1789 fn try_verify_sum_reindex_shift(
1792 &mut self,
1793 left: &Obj,
1794 right: &Obj,
1795 line_file: LineFile,
1796 verify_state: &VerifyState,
1797 ) -> Result<Option<StmtResult>, RuntimeError> {
1798 if !verify_state.is_round_0() {
1799 return Ok(None);
1800 }
1801 for (l_obj, r_obj) in [(left, right), (right, left)] {
1802 let (Obj::Sum(l_sum), Obj::Sum(r_sum)) = (l_obj, r_obj) else {
1803 continue;
1804 };
1805 let k: Obj = Sub::new((*r_sum.start).clone(), (*l_sum.start).clone()).into();
1806 let k_end = Sub::new((*r_sum.end).clone(), (*l_sum.end).clone()).into();
1807 if !self
1808 .verify_objs_are_equal(&k, &k_end, line_file.clone(), verify_state)?
1809 .is_true()
1810 {
1811 continue;
1812 }
1813 let y_name = self.generate_random_unused_name();
1814 let y_obj = obj_for_bound_param_in_scope(y_name.clone(), ParamObjType::Forall);
1815 let index_for_left = Sub::new(y_obj.clone(), k.clone()).into();
1816 let Some(at_l) =
1817 self.instantiate_unary_anonymous_summand_at(l_sum.func.as_ref(), &index_for_left)?
1818 else {
1819 continue;
1820 };
1821 let Some(at_r) =
1822 self.instantiate_unary_anonymous_summand_at(r_sum.func.as_ref(), &y_obj)?
1823 else {
1824 continue;
1825 };
1826 let then_fact: ExistOrAndChainAtomicFact =
1827 EqualFact::new(at_l, at_r, line_file.clone()).into();
1828 let dom_lo: Fact =
1829 LessEqualFact::new((*r_sum.start).clone(), y_obj.clone(), line_file.clone()).into();
1830 let dom_hi: Fact =
1831 LessEqualFact::new(y_obj.clone(), (*r_sum.end).clone(), line_file.clone()).into();
1832 let forall_fact: Fact = ForallFact::new(
1833 ParamDefWithType::new(vec![ParamGroupWithParamType::new(
1834 vec![y_name],
1835 ParamType::Obj(StandardSet::Z.into()),
1836 )]),
1837 vec![dom_lo, dom_hi],
1838 vec![then_fact],
1839 line_file.clone(),
1840 )?
1841 .into();
1842 let r = self.verify_fact(&forall_fact, verify_state)?;
1843 if r.is_true() {
1844 return Ok(Some(factual_equal_success_by_builtin_reason(
1845 left,
1846 right,
1847 line_file,
1848 "equality: sum reindexing (integer shift) from pointwise equality on the range",
1849 )));
1850 }
1851 }
1852 Ok(None)
1853 }
1854
1855 fn try_verify_sum_constant_summand(
1857 &mut self,
1858 left: &Obj,
1859 right: &Obj,
1860 line_file: LineFile,
1861 verify_state: &VerifyState,
1862 ) -> Result<Option<StmtResult>, RuntimeError> {
1863 if !verify_state.is_round_0() {
1864 return Ok(None);
1865 }
1866 for (sum_side, other) in [(left, right), (right, left)] {
1867 let Obj::Sum(s) = sum_side else {
1868 continue;
1869 };
1870 let af = match s.func.as_ref() {
1871 Obj::AnonymousFn(af) => af,
1872 Obj::FnObj(fo) if fo.body.is_empty() => match fo.head.as_ref() {
1873 FnObjHead::AnonymousFnLiteral(a) => a.as_ref(),
1874 _ => continue,
1875 },
1876 _ => continue,
1877 };
1878 if ParamGroupWithSet::number_of_params(&af.body.params_def_with_set) != 1 {
1879 continue;
1880 }
1881 let names = ParamGroupWithSet::collect_param_names(&af.body.params_def_with_set);
1882 let pname = match names.first() {
1883 Some(n) => n.as_str(),
1884 None => continue,
1885 };
1886 if obj_expr_mentions_bare_id(af.equal_to.as_ref(), pname) {
1887 continue;
1888 }
1889 let c = (*af.equal_to).clone();
1890 let one: Obj = Number::new("1".to_string()).into();
1891 let count: Obj =
1892 Add::new(Sub::new((*s.end).clone(), (*s.start).clone()).into(), one).into();
1893 let m1: Obj = Mul::new(count.clone(), c.clone()).into();
1894 let m2: Obj = Mul::new(c, count).into();
1895 if self
1896 .verify_objs_are_equal(other, &m1, line_file.clone(), verify_state)?
1897 .is_true()
1898 || self
1899 .verify_objs_are_equal(other, &m2, line_file.clone(), verify_state)?
1900 .is_true()
1901 {
1902 return Ok(Some(factual_equal_success_by_builtin_reason(
1903 left,
1904 right,
1905 line_file,
1906 "equality: sum of a constant summand over a closed integer range",
1907 )));
1908 }
1909 }
1910 Ok(None)
1911 }
1912
1913 fn try_verify_mod_nested_same_modulus_absorption(
1918 &mut self,
1919 left: &Obj,
1920 right: &Obj,
1921 line_file: LineFile,
1922 verify_state: &VerifyState,
1923 ) -> Result<Option<StmtResult>, RuntimeError> {
1924 for (side_nested, side_simple) in [(left, right), (right, left)] {
1925 let Obj::Mod(outer) = side_nested else {
1926 continue;
1927 };
1928 let Obj::Mod(inner) = outer.left.as_ref() else {
1929 continue;
1930 };
1931 let Obj::Mod(simple) = side_simple else {
1932 continue;
1933 };
1934 if !self
1935 .verify_objs_are_equal(
1936 outer.right.as_ref(),
1937 inner.right.as_ref(),
1938 line_file.clone(),
1939 verify_state,
1940 )?
1941 .is_true()
1942 {
1943 continue;
1944 }
1945 if !self
1946 .verify_objs_are_equal(
1947 outer.right.as_ref(),
1948 simple.right.as_ref(),
1949 line_file.clone(),
1950 verify_state,
1951 )?
1952 .is_true()
1953 {
1954 continue;
1955 }
1956 if !self
1957 .verify_objs_are_equal(
1958 inner.left.as_ref(),
1959 simple.left.as_ref(),
1960 line_file.clone(),
1961 verify_state,
1962 )?
1963 .is_true()
1964 {
1965 continue;
1966 }
1967 return Ok(Some(factual_equal_success_by_builtin_reason(
1968 left,
1969 right,
1970 line_file,
1971 "equality: nested mod with same modulus absorbs inner mod",
1972 )));
1973 }
1974 Ok(None)
1975 }
1976
1977 fn try_verify_mod_peel_nested_same_modulus(
1980 &mut self,
1981 left: &Obj,
1982 right: &Obj,
1983 line_file: LineFile,
1984 verify_state: &VerifyState,
1985 ) -> Result<Option<StmtResult>, RuntimeError> {
1986 let (Obj::Mod(lm), Obj::Mod(rm)) = (left, right) else {
1987 return Ok(None);
1988 };
1989 if !self
1990 .verify_objs_are_equal(
1991 lm.right.as_ref(),
1992 rm.right.as_ref(),
1993 line_file.clone(),
1994 verify_state,
1995 )?
1996 .is_true()
1997 {
1998 return Ok(None);
1999 }
2000 let modulus = lm.right.as_ref();
2001
2002 if let Obj::Mod(r_inner) = rm.left.as_ref() {
2003 if self
2004 .verify_objs_are_equal(
2005 r_inner.right.as_ref(),
2006 modulus,
2007 line_file.clone(),
2008 verify_state,
2009 )?
2010 .is_true()
2011 {
2012 let lhs: Obj = Mod::new((*lm.left).clone(), (*lm.right).clone()).into();
2013 let rhs: Obj = Mod::new((*r_inner.left).clone(), (*lm.right).clone()).into();
2014 if self
2015 .verify_objs_are_equal(&lhs, &rhs, line_file.clone(), verify_state)?
2016 .is_true()
2017 {
2018 return Ok(Some(factual_equal_success_by_builtin_reason(
2019 left,
2020 right,
2021 line_file,
2022 "equality: mod — peel outer nested % m to reuse residue equality (full verify_objs_are_equal)",
2023 )));
2024 }
2025 }
2026 }
2027
2028 if let Obj::Mod(l_inner) = lm.left.as_ref() {
2029 if self
2030 .verify_objs_are_equal(
2031 l_inner.right.as_ref(),
2032 modulus,
2033 line_file.clone(),
2034 verify_state,
2035 )?
2036 .is_true()
2037 {
2038 let lhs: Obj = Mod::new((*l_inner.left).clone(), (*lm.right).clone()).into();
2039 let rhs: Obj = Mod::new((*rm.left).clone(), (*lm.right).clone()).into();
2040 if self
2041 .verify_objs_are_equal(&lhs, &rhs, line_file.clone(), verify_state)?
2042 .is_true()
2043 {
2044 return Ok(Some(factual_equal_success_by_builtin_reason(
2045 left,
2046 right,
2047 line_file,
2048 "equality: mod — peel outer nested % m to reuse residue equality (full verify_objs_are_equal)",
2049 )));
2050 }
2051 }
2052 }
2053
2054 Ok(None)
2055 }
2056
2057 fn try_verify_mod_congruence_from_inner_binary(
2062 &mut self,
2063 left: &Obj,
2064 right: &Obj,
2065 line_file: LineFile,
2066 verify_state: &VerifyState,
2067 ) -> Result<Option<StmtResult>, RuntimeError> {
2068 let (Obj::Mod(lm), Obj::Mod(rm)) = (left, right) else {
2069 return Ok(None);
2070 };
2071 if !self
2072 .verify_objs_are_equal(
2073 lm.right.as_ref(),
2074 rm.right.as_ref(),
2075 line_file.clone(),
2076 verify_state,
2077 )?
2078 .is_true()
2079 {
2080 return Ok(None);
2081 }
2082 let mut pair_ok = |a: &Obj, b: &Obj| -> Result<bool, RuntimeError> {
2083 let l: Obj = Mod::new(a.clone(), (*lm.right).clone()).into();
2084 let r: Obj = Mod::new(b.clone(), (*rm.right).clone()).into();
2085 Ok(self
2086 .verify_objs_are_equal(&l, &r, line_file.clone(), verify_state)?
2087 .is_true())
2088 };
2089 let ok = match (lm.left.as_ref(), rm.left.as_ref()) {
2090 (Obj::Add(la), Obj::Add(ra)) => {
2091 pair_ok(la.left.as_ref(), ra.left.as_ref())?
2092 && pair_ok(la.right.as_ref(), ra.right.as_ref())?
2093 }
2094 (Obj::Sub(ls), Obj::Sub(rs)) => {
2095 pair_ok(ls.left.as_ref(), rs.left.as_ref())?
2096 && pair_ok(ls.right.as_ref(), rs.right.as_ref())?
2097 }
2098 (Obj::Mul(lx), Obj::Mul(rx)) => {
2099 pair_ok(lx.left.as_ref(), rx.left.as_ref())?
2100 && pair_ok(lx.right.as_ref(), rx.right.as_ref())?
2101 }
2102 _ => return Ok(None),
2103 };
2104 if !ok {
2105 return Ok(None);
2106 }
2107 Ok(Some(factual_equal_success_by_builtin_reason(
2108 left,
2109 right,
2110 line_file,
2111 "equality: integer congruence — same modulus, residues for matching + / - / *",
2112 )))
2113 }
2114
2115 pub fn verify_equality_by_builtin_rules(
2116 &mut self,
2117 left: &Obj,
2118 right: &Obj,
2119 line_file: LineFile,
2120 verify_state: &VerifyState,
2121 ) -> Result<StmtResult, RuntimeError> {
2122 if let Some(done) = self.try_verify_objs_equal_by_expanding_family(
2123 left,
2124 right,
2125 line_file.clone(),
2126 verify_state,
2127 )? {
2128 return Ok(done);
2129 }
2130
2131 if let Some(done) =
2132 self.try_verify_abs_equalities(left, right, line_file.clone(), verify_state)?
2133 {
2134 return Ok(done);
2135 }
2136
2137 if let Some(done) = self.try_verify_zero_equals_subtraction_implies_equal_operands(
2138 left,
2139 right,
2140 line_file.clone(),
2141 verify_state,
2142 )? {
2143 return Ok(done);
2144 }
2145
2146 if let Some(done) = self.try_verify_zero_equals_pow_from_base_zero(
2147 left,
2148 right,
2149 line_file.clone(),
2150 verify_state,
2151 )? {
2152 return Ok(done);
2153 }
2154
2155 if let Some(done) =
2156 self.try_verify_pow_one_identity(left, right, line_file.clone(), verify_state)?
2157 {
2158 return Ok(done);
2159 }
2160
2161 if let Some(done) = self.try_verify_power_addition_exponent_rule(
2162 left,
2163 right,
2164 line_file.clone(),
2165 verify_state,
2166 )? {
2167 return Ok(done);
2168 }
2169
2170 if let Some(done) = self.try_verify_same_algebra_context_by_equal_args(
2171 left,
2172 right,
2173 line_file.clone(),
2174 verify_state,
2175 )? {
2176 return Ok(done);
2177 }
2178
2179 if let Some(done) =
2180 self.try_verify_log_identity_equalities(left, right, line_file.clone(), verify_state)?
2181 {
2182 return Ok(done);
2183 }
2184
2185 if let Some(done) =
2186 self.try_verify_log_algebra_identities(left, right, line_file.clone(), verify_state)?
2187 {
2188 return Ok(done);
2189 }
2190
2191 if let Some(done) =
2192 self.try_verify_log_equals_by_pow_inverse(left, right, line_file.clone(), verify_state)?
2193 {
2194 return Ok(done);
2195 }
2196
2197 if let Some(done) =
2198 self.try_verify_sum_additivity(left, right, line_file.clone(), verify_state)?
2199 {
2200 return Ok(done);
2201 }
2202
2203 if let Some(done) =
2204 self.try_verify_sum_merge_adjacent_ranges(left, right, line_file.clone(), verify_state)?
2205 {
2206 return Ok(done);
2207 }
2208
2209 if let Some(done) =
2210 self.try_verify_sum_split_last_term(left, right, line_file.clone(), verify_state)?
2211 {
2212 return Ok(done);
2213 }
2214
2215 if let Some(done) =
2216 self.try_verify_product_split_last_term(left, right, line_file.clone(), verify_state)?
2217 {
2218 return Ok(done);
2219 }
2220
2221 if let Some(done) = self.try_verify_sum_partition_adjacent_ranges(
2222 left,
2223 right,
2224 line_file.clone(),
2225 verify_state,
2226 )? {
2227 return Ok(done);
2228 }
2229
2230 if let Some(done) = self.try_verify_product_partition_adjacent_ranges(
2231 left,
2232 right,
2233 line_file.clone(),
2234 verify_state,
2235 )? {
2236 return Ok(done);
2237 }
2238
2239 if let Some(done) =
2240 self.try_verify_sum_reindex_shift(left, right, line_file.clone(), verify_state)?
2241 {
2242 return Ok(done);
2243 }
2244
2245 if let Some(done) =
2246 self.try_verify_sum_constant_summand(left, right, line_file.clone(), verify_state)?
2247 {
2248 return Ok(done);
2249 }
2250
2251 if let Some(done) = self.try_verify_mod_nested_same_modulus_absorption(
2252 left,
2253 right,
2254 line_file.clone(),
2255 verify_state,
2256 )? {
2257 return Ok(done);
2258 }
2259
2260 if let Some(done) = self.try_verify_zero_mod_equals_zero(left, right, line_file.clone())? {
2261 return Ok(done);
2262 }
2263
2264 if let Some(done) = self.try_verify_mod_peel_nested_same_modulus(
2265 left,
2266 right,
2267 line_file.clone(),
2268 verify_state,
2269 )? {
2270 return Ok(done);
2271 }
2272
2273 if let Some(done) = self.try_verify_mod_congruence_from_inner_binary(
2274 left,
2275 right,
2276 line_file.clone(),
2277 verify_state,
2278 )? {
2279 return Ok(done);
2280 }
2281
2282 let (result, calculated_left, calculated_right) = self
2283 .verify_equality_by_they_are_the_same_and_calculation(
2284 left,
2285 right,
2286 line_file.clone(),
2287 verify_state,
2288 )?;
2289 if result.is_true() {
2290 return Ok(result);
2291 }
2292
2293 if objs_equal_by_rational_expression_evaluation(&left, &right) {
2294 return Ok(
2295 (FactualStmtSuccess::new_with_verified_by_builtin_rules_recording_stmt(
2296 EqualFact::new(left.clone(), right.clone(), line_file).into(),
2297 "calculation and rational expression simplification".to_string(),
2298 Vec::new(),
2299 ))
2300 .into(),
2301 );
2302 }
2303
2304 if objs_equal_by_rational_expression_evaluation(&calculated_left, &calculated_right) {
2305 return Ok(
2306 (FactualStmtSuccess::new_with_verified_by_builtin_rules_recording_stmt(
2307 EqualFact::new(left.clone(), right.clone(), line_file).into(),
2308 "calculation and rational expression simplification".to_string(),
2309 Vec::new(),
2310 ))
2311 .into(),
2312 );
2313 }
2314
2315 if let Some(done) = self.try_verify_anonymous_fn_application_equals_other_side(
2316 left,
2317 right,
2318 left,
2319 right,
2320 line_file.clone(),
2321 verify_state,
2322 )? {
2323 return Ok(done);
2324 }
2325 if let Some(done) = self.try_verify_anonymous_fn_application_equals_other_side(
2326 left,
2327 right,
2328 right,
2329 left,
2330 line_file.clone(),
2331 verify_state,
2332 )? {
2333 return Ok(done);
2334 }
2335
2336 if let (Obj::FnSet(left_fn_set), Obj::FnSet(right_fn_set)) = (left, right) {
2337 return self.verify_fn_set_with_params_equality_by_builtin_rules(
2338 left_fn_set,
2339 right_fn_set,
2340 line_file,
2341 verify_state,
2342 );
2343 }
2344
2345 if let (Obj::AnonymousFn(l), Obj::AnonymousFn(r)) = (left, right) {
2346 if l.to_string() == r.to_string() {
2347 return Ok(
2348 (FactualStmtSuccess::new_with_verified_by_builtin_rules_recording_stmt(
2349 EqualFact::new(left.clone(), right.clone(), line_file).into(),
2350 "anonymous fn: identical surface syntax (params, dom, ret, body)"
2351 .to_string(),
2352 Vec::new(),
2353 ))
2354 .into(),
2355 );
2356 }
2357 }
2358
2359 Ok((StmtUnknown::new()).into())
2360 }
2361}
2362
2363impl Runtime {
2364 fn try_verify_equality_pair_by_the_same_then_calculation_then_fn_obj_same_head_known_args(
2365 &mut self,
2366 left: &Obj,
2367 right: &Obj,
2368 line_file: LineFile,
2369 verify_state: &VerifyState,
2370 ) -> Result<Option<StmtResult>, RuntimeError> {
2371 let (result, _, _) = self.verify_equality_by_they_are_the_same_and_calculation(
2372 left,
2373 right,
2374 line_file.clone(),
2375 verify_state,
2376 )?;
2377 if result.is_true() {
2378 return Ok(Some(result));
2379 }
2380 if let Some(shape_result) =
2381 self.try_verify_equal_by_same_shape_and_known_equality_args(left, right, line_file)
2382 {
2383 if shape_result.is_true() {
2384 return Ok(Some(shape_result));
2385 }
2386 }
2387 Ok(None)
2388 }
2389
2390 pub fn try_verify_equality_with_known_equalities_by_builtin_rules_only(
2391 &mut self,
2392 left: &Obj,
2393 right: &Obj,
2394 line_file: LineFile,
2395 verify_state: &VerifyState,
2396 known_objs_equal_to_left: Option<&Rc<Vec<Obj>>>,
2397 known_objs_equal_to_right: Option<&Rc<Vec<Obj>>>,
2398 ) -> Result<Option<StmtResult>, RuntimeError> {
2399 match (known_objs_equal_to_left, known_objs_equal_to_right) {
2400 (None, None) => Ok(None),
2401 (Some(known_objs_equal_to_left), None) => {
2402 for obj in known_objs_equal_to_left.iter() {
2403 if let Some(result) = self
2404 .try_verify_equality_pair_by_the_same_then_calculation_then_fn_obj_same_head_known_args(
2405 obj,
2406 right,
2407 line_file.clone(),
2408 verify_state,
2409 )?
2410 {
2411 return Ok(Some(result));
2412 }
2413 }
2414 Ok(None)
2415 }
2416 (None, Some(known_objs_equal_to_right)) => {
2417 for obj in known_objs_equal_to_right.iter() {
2418 if let Some(result) = self
2419 .try_verify_equality_pair_by_the_same_then_calculation_then_fn_obj_same_head_known_args(
2420 left,
2421 obj,
2422 line_file.clone(),
2423 verify_state,
2424 )?
2425 {
2426 return Ok(Some(result));
2427 }
2428 }
2429 Ok(None)
2430 }
2431 (Some(known_objs_equal_to_left), Some(known_objs_equal_to_right)) => {
2432 for obj1 in known_objs_equal_to_left.iter() {
2433 for obj2 in known_objs_equal_to_right.iter() {
2434 if let Some(result) = self
2435 .try_verify_equality_pair_by_the_same_then_calculation_then_fn_obj_same_head_known_args(
2436 obj1,
2437 obj2,
2438 line_file.clone(),
2439 verify_state,
2440 )?
2441 {
2442 return Ok(Some(result));
2443 }
2444 }
2445 }
2446 Ok(None)
2447 }
2448 }
2449 }
2450
2451 pub fn objs_have_same_known_equality_rc_in_some_env(&self, left: &Obj, right: &Obj) -> bool {
2452 let left_key: ObjString = left.to_string();
2453 let right_key: ObjString = right.to_string();
2454 for env in self.iter_environments_from_top() {
2455 let left_entry = env.known_equality.get(&left_key);
2456 let right_entry = env.known_equality.get(&right_key);
2457 if let (Some((_, left_rc)), Some((_, right_rc))) = (left_entry, right_entry) {
2458 if Rc::ptr_eq(left_rc, right_rc) {
2459 return true;
2460 }
2461 }
2462 }
2463 false
2464 }
2465
2466 fn arg_pairs_share_known_equality_class(&self, pairs: &[(&Obj, &Obj)]) -> bool {
2467 pairs
2468 .iter()
2469 .all(|(a, b)| self.objs_have_same_known_equality_rc_in_some_env(a, b))
2470 }
2471
2472 fn boxed_obj_vecs_share_known_equality_class(
2473 &self,
2474 left: &[Box<Obj>],
2475 right: &[Box<Obj>],
2476 ) -> bool {
2477 if left.len() != right.len() {
2478 return false;
2479 }
2480 left.iter()
2481 .zip(right.iter())
2482 .all(|(a, b)| self.objs_have_same_known_equality_rc_in_some_env(a, b))
2483 }
2484
2485 pub fn try_verify_equal_by_same_shape_and_known_equality_args(
2486 &self,
2487 left: &Obj,
2488 right: &Obj,
2489 line_file: LineFile,
2490 ) -> Option<StmtResult> {
2491 let reason = "same shape and paired args share known equality class";
2492 match (left, right) {
2493 (Obj::FnObj(left_fn), Obj::FnObj(right_fn)) => {
2494 let left_head_obj = left_fn.head.as_ref().clone().into();
2495 let right_head_obj = right_fn.head.as_ref().clone().into();
2496 if !verify_equality_by_they_are_the_same(&left_head_obj, &right_head_obj) {
2497 return Some((StmtUnknown::new()).into());
2498 }
2499 if left_fn.body.len() != right_fn.body.len() {
2500 return Some((StmtUnknown::new()).into());
2501 }
2502 for (left_group, right_group) in left_fn.body.iter().zip(right_fn.body.iter()) {
2503 if !self.boxed_obj_vecs_share_known_equality_class(left_group, right_group) {
2504 return Some((StmtUnknown::new()).into());
2505 }
2506 }
2507 Some(factual_equal_success_by_builtin_reason(
2508 left, right, line_file, reason,
2509 ))
2510 }
2511 (Obj::Add(l), Obj::Add(r)) => {
2512 if self.arg_pairs_share_known_equality_class(&[
2513 (&l.left, &r.left),
2514 (&l.right, &r.right),
2515 ]) {
2516 Some(factual_equal_success_by_builtin_reason(
2517 left, right, line_file, reason,
2518 ))
2519 } else {
2520 Some((StmtUnknown::new()).into())
2521 }
2522 }
2523 (Obj::MatrixAdd(l), Obj::MatrixAdd(r)) => {
2524 if self.arg_pairs_share_known_equality_class(&[
2525 (&l.left, &r.left),
2526 (&l.right, &r.right),
2527 ]) {
2528 Some(factual_equal_success_by_builtin_reason(
2529 left, right, line_file, reason,
2530 ))
2531 } else {
2532 Some((StmtUnknown::new()).into())
2533 }
2534 }
2535 (Obj::MatrixSub(l), Obj::MatrixSub(r)) => {
2536 if self.arg_pairs_share_known_equality_class(&[
2537 (&l.left, &r.left),
2538 (&l.right, &r.right),
2539 ]) {
2540 Some(factual_equal_success_by_builtin_reason(
2541 left, right, line_file, reason,
2542 ))
2543 } else {
2544 Some((StmtUnknown::new()).into())
2545 }
2546 }
2547 (Obj::MatrixMul(l), Obj::MatrixMul(r)) => {
2548 if self.arg_pairs_share_known_equality_class(&[
2549 (&l.left, &r.left),
2550 (&l.right, &r.right),
2551 ]) {
2552 Some(factual_equal_success_by_builtin_reason(
2553 left, right, line_file, reason,
2554 ))
2555 } else {
2556 Some((StmtUnknown::new()).into())
2557 }
2558 }
2559 (Obj::MatrixScalarMul(l), Obj::MatrixScalarMul(r)) => {
2560 if self.arg_pairs_share_known_equality_class(&[
2561 (&l.scalar, &r.scalar),
2562 (&l.matrix, &r.matrix),
2563 ]) {
2564 Some(factual_equal_success_by_builtin_reason(
2565 left, right, line_file, reason,
2566 ))
2567 } else {
2568 Some((StmtUnknown::new()).into())
2569 }
2570 }
2571 (Obj::MatrixPow(l), Obj::MatrixPow(r)) => {
2572 if self.arg_pairs_share_known_equality_class(&[
2573 (&l.base, &r.base),
2574 (&l.exponent, &r.exponent),
2575 ]) {
2576 Some(factual_equal_success_by_builtin_reason(
2577 left, right, line_file, reason,
2578 ))
2579 } else {
2580 Some((StmtUnknown::new()).into())
2581 }
2582 }
2583 (Obj::Sub(l), Obj::Sub(r)) => {
2584 if self.arg_pairs_share_known_equality_class(&[
2585 (&l.left, &r.left),
2586 (&l.right, &r.right),
2587 ]) {
2588 Some(factual_equal_success_by_builtin_reason(
2589 left, right, line_file, reason,
2590 ))
2591 } else {
2592 Some((StmtUnknown::new()).into())
2593 }
2594 }
2595 (Obj::Mul(l), Obj::Mul(r)) => {
2596 if self.arg_pairs_share_known_equality_class(&[
2597 (&l.left, &r.left),
2598 (&l.right, &r.right),
2599 ]) {
2600 Some(factual_equal_success_by_builtin_reason(
2601 left, right, line_file, reason,
2602 ))
2603 } else {
2604 Some((StmtUnknown::new()).into())
2605 }
2606 }
2607 (Obj::Div(l), Obj::Div(r)) => {
2608 if self.arg_pairs_share_known_equality_class(&[
2609 (&l.left, &r.left),
2610 (&l.right, &r.right),
2611 ]) {
2612 Some(factual_equal_success_by_builtin_reason(
2613 left, right, line_file, reason,
2614 ))
2615 } else {
2616 Some((StmtUnknown::new()).into())
2617 }
2618 }
2619 (Obj::Mod(l), Obj::Mod(r)) => {
2620 if self.arg_pairs_share_known_equality_class(&[
2621 (&l.left, &r.left),
2622 (&l.right, &r.right),
2623 ]) {
2624 Some(factual_equal_success_by_builtin_reason(
2625 left, right, line_file, reason,
2626 ))
2627 } else {
2628 Some((StmtUnknown::new()).into())
2629 }
2630 }
2631 (Obj::Pow(l), Obj::Pow(r)) => {
2632 if self.arg_pairs_share_known_equality_class(&[
2633 (&l.base, &r.base),
2634 (&l.exponent, &r.exponent),
2635 ]) {
2636 Some(factual_equal_success_by_builtin_reason(
2637 left, right, line_file, reason,
2638 ))
2639 } else {
2640 Some((StmtUnknown::new()).into())
2641 }
2642 }
2643 (Obj::Log(l), Obj::Log(r)) => {
2644 if self
2645 .arg_pairs_share_known_equality_class(&[(&l.base, &r.base), (&l.arg, &r.arg)])
2646 {
2647 Some(factual_equal_success_by_builtin_reason(
2648 left, right, line_file, reason,
2649 ))
2650 } else {
2651 Some((StmtUnknown::new()).into())
2652 }
2653 }
2654 (Obj::Max(l), Obj::Max(r)) => {
2655 if self.arg_pairs_share_known_equality_class(&[
2656 (&l.left, &r.left),
2657 (&l.right, &r.right),
2658 ]) {
2659 Some(factual_equal_success_by_builtin_reason(
2660 left, right, line_file, reason,
2661 ))
2662 } else {
2663 Some((StmtUnknown::new()).into())
2664 }
2665 }
2666 (Obj::Min(l), Obj::Min(r)) => {
2667 if self.arg_pairs_share_known_equality_class(&[
2668 (&l.left, &r.left),
2669 (&l.right, &r.right),
2670 ]) {
2671 Some(factual_equal_success_by_builtin_reason(
2672 left, right, line_file, reason,
2673 ))
2674 } else {
2675 Some((StmtUnknown::new()).into())
2676 }
2677 }
2678 (Obj::Union(l), Obj::Union(r)) => {
2679 if self.arg_pairs_share_known_equality_class(&[
2680 (&l.left, &r.left),
2681 (&l.right, &r.right),
2682 ]) {
2683 Some(factual_equal_success_by_builtin_reason(
2684 left, right, line_file, reason,
2685 ))
2686 } else {
2687 Some((StmtUnknown::new()).into())
2688 }
2689 }
2690 (Obj::Intersect(l), Obj::Intersect(r)) => {
2691 if self.arg_pairs_share_known_equality_class(&[
2692 (&l.left, &r.left),
2693 (&l.right, &r.right),
2694 ]) {
2695 Some(factual_equal_success_by_builtin_reason(
2696 left, right, line_file, reason,
2697 ))
2698 } else {
2699 Some((StmtUnknown::new()).into())
2700 }
2701 }
2702 (Obj::SetMinus(l), Obj::SetMinus(r)) => {
2703 if self.arg_pairs_share_known_equality_class(&[
2704 (&l.left, &r.left),
2705 (&l.right, &r.right),
2706 ]) {
2707 Some(factual_equal_success_by_builtin_reason(
2708 left, right, line_file, reason,
2709 ))
2710 } else {
2711 Some((StmtUnknown::new()).into())
2712 }
2713 }
2714 (Obj::SetDiff(l), Obj::SetDiff(r)) => {
2715 if self.arg_pairs_share_known_equality_class(&[
2716 (&l.left, &r.left),
2717 (&l.right, &r.right),
2718 ]) {
2719 Some(factual_equal_success_by_builtin_reason(
2720 left, right, line_file, reason,
2721 ))
2722 } else {
2723 Some((StmtUnknown::new()).into())
2724 }
2725 }
2726 (Obj::Cup(l), Obj::Cup(r)) => {
2727 if self.objs_have_same_known_equality_rc_in_some_env(&l.left, &r.left) {
2728 Some(factual_equal_success_by_builtin_reason(
2729 left, right, line_file, reason,
2730 ))
2731 } else {
2732 Some((StmtUnknown::new()).into())
2733 }
2734 }
2735 (Obj::Cap(l), Obj::Cap(r)) => {
2736 if self.objs_have_same_known_equality_rc_in_some_env(&l.left, &r.left) {
2737 Some(factual_equal_success_by_builtin_reason(
2738 left, right, line_file, reason,
2739 ))
2740 } else {
2741 Some((StmtUnknown::new()).into())
2742 }
2743 }
2744 (Obj::PowerSet(l), Obj::PowerSet(r)) => {
2745 if self.objs_have_same_known_equality_rc_in_some_env(&l.set, &r.set) {
2746 Some(factual_equal_success_by_builtin_reason(
2747 left, right, line_file, reason,
2748 ))
2749 } else {
2750 Some((StmtUnknown::new()).into())
2751 }
2752 }
2753 (Obj::Choose(l), Obj::Choose(r)) => {
2754 if self.objs_have_same_known_equality_rc_in_some_env(&l.set, &r.set) {
2755 Some(factual_equal_success_by_builtin_reason(
2756 left, right, line_file, reason,
2757 ))
2758 } else {
2759 Some((StmtUnknown::new()).into())
2760 }
2761 }
2762 (Obj::CartDim(l), Obj::CartDim(r)) => {
2763 if self.objs_have_same_known_equality_rc_in_some_env(&l.set, &r.set) {
2764 Some(factual_equal_success_by_builtin_reason(
2765 left, right, line_file, reason,
2766 ))
2767 } else {
2768 Some((StmtUnknown::new()).into())
2769 }
2770 }
2771 (Obj::TupleDim(l), Obj::TupleDim(r)) => {
2772 if self.objs_have_same_known_equality_rc_in_some_env(&l.arg, &r.arg) {
2773 Some(factual_equal_success_by_builtin_reason(
2774 left, right, line_file, reason,
2775 ))
2776 } else {
2777 Some((StmtUnknown::new()).into())
2778 }
2779 }
2780 (Obj::Count(l), Obj::Count(r)) => {
2781 if self.objs_have_same_known_equality_rc_in_some_env(&l.set, &r.set) {
2782 Some(factual_equal_success_by_builtin_reason(
2783 left, right, line_file, reason,
2784 ))
2785 } else {
2786 Some((StmtUnknown::new()).into())
2787 }
2788 }
2789 (Obj::Range(l), Obj::Range(r)) => {
2790 if self
2791 .arg_pairs_share_known_equality_class(&[(&l.start, &r.start), (&l.end, &r.end)])
2792 {
2793 Some(factual_equal_success_by_builtin_reason(
2794 left, right, line_file, reason,
2795 ))
2796 } else {
2797 Some((StmtUnknown::new()).into())
2798 }
2799 }
2800 (Obj::Sum(l), Obj::Sum(r)) => {
2801 if self.arg_pairs_share_known_equality_class(&[
2802 (&l.start, &r.start),
2803 (&l.end, &r.end),
2804 (&l.func, &r.func),
2805 ]) {
2806 Some(factual_equal_success_by_builtin_reason(
2807 left, right, line_file, reason,
2808 ))
2809 } else {
2810 Some((StmtUnknown::new()).into())
2811 }
2812 }
2813 (Obj::Product(l), Obj::Product(r)) => {
2814 if self.arg_pairs_share_known_equality_class(&[
2815 (&l.start, &r.start),
2816 (&l.end, &r.end),
2817 (&l.func, &r.func),
2818 ]) {
2819 Some(factual_equal_success_by_builtin_reason(
2820 left, right, line_file, reason,
2821 ))
2822 } else {
2823 Some((StmtUnknown::new()).into())
2824 }
2825 }
2826 (Obj::ClosedRange(l), Obj::ClosedRange(r)) => {
2827 if self
2828 .arg_pairs_share_known_equality_class(&[(&l.start, &r.start), (&l.end, &r.end)])
2829 {
2830 Some(factual_equal_success_by_builtin_reason(
2831 left, right, line_file, reason,
2832 ))
2833 } else {
2834 Some((StmtUnknown::new()).into())
2835 }
2836 }
2837 (Obj::FiniteSeqSet(l), Obj::FiniteSeqSet(r)) => {
2838 if self.arg_pairs_share_known_equality_class(&[(&l.set, &r.set), (&l.n, &r.n)]) {
2839 Some(factual_equal_success_by_builtin_reason(
2840 left, right, line_file, reason,
2841 ))
2842 } else {
2843 Some((StmtUnknown::new()).into())
2844 }
2845 }
2846 (Obj::SeqSet(l), Obj::SeqSet(r)) => {
2847 if self.arg_pairs_share_known_equality_class(&[(&l.set, &r.set)]) {
2848 Some(factual_equal_success_by_builtin_reason(
2849 left, right, line_file, reason,
2850 ))
2851 } else {
2852 Some((StmtUnknown::new()).into())
2853 }
2854 }
2855 (Obj::MatrixSet(l), Obj::MatrixSet(r)) => {
2856 if self.arg_pairs_share_known_equality_class(&[
2857 (&l.set, &r.set),
2858 (&l.row_len, &r.row_len),
2859 (&l.col_len, &r.col_len),
2860 ]) {
2861 Some(factual_equal_success_by_builtin_reason(
2862 left, right, line_file, reason,
2863 ))
2864 } else {
2865 Some((StmtUnknown::new()).into())
2866 }
2867 }
2868 (Obj::Proj(l), Obj::Proj(r)) => {
2869 if self.arg_pairs_share_known_equality_class(&[(&l.set, &r.set), (&l.dim, &r.dim)])
2870 {
2871 Some(factual_equal_success_by_builtin_reason(
2872 left, right, line_file, reason,
2873 ))
2874 } else {
2875 Some((StmtUnknown::new()).into())
2876 }
2877 }
2878 (Obj::ObjAtIndex(l), Obj::ObjAtIndex(r)) => {
2879 if self
2880 .arg_pairs_share_known_equality_class(&[(&l.obj, &r.obj), (&l.index, &r.index)])
2881 {
2882 Some(factual_equal_success_by_builtin_reason(
2883 left, right, line_file, reason,
2884 ))
2885 } else {
2886 Some((StmtUnknown::new()).into())
2887 }
2888 }
2889 (Obj::Tuple(l), Obj::Tuple(r)) => {
2890 if self.boxed_obj_vecs_share_known_equality_class(&l.args, &r.args) {
2891 Some(factual_equal_success_by_builtin_reason(
2892 left, right, line_file, reason,
2893 ))
2894 } else {
2895 Some((StmtUnknown::new()).into())
2896 }
2897 }
2898 (Obj::ListSet(l), Obj::ListSet(r)) => {
2899 if self.boxed_obj_vecs_share_known_equality_class(&l.list, &r.list) {
2900 Some(factual_equal_success_by_builtin_reason(
2901 left, right, line_file, reason,
2902 ))
2903 } else {
2904 Some((StmtUnknown::new()).into())
2905 }
2906 }
2907 (Obj::Cart(l), Obj::Cart(r)) => {
2908 if self.boxed_obj_vecs_share_known_equality_class(&l.args, &r.args) {
2909 Some(factual_equal_success_by_builtin_reason(
2910 left, right, line_file, reason,
2911 ))
2912 } else {
2913 Some((StmtUnknown::new()).into())
2914 }
2915 }
2916 _ => None,
2917 }
2918 }
2919
2920 pub fn verify_equality_by_they_are_the_same_and_calculation(
2921 &mut self,
2922 left: &Obj,
2923 right: &Obj,
2924 line_file: LineFile,
2925 _verify_state: &VerifyState,
2926 ) -> Result<(StmtResult, Obj, Obj), RuntimeError> {
2927 if verify_equality_by_they_are_the_same(left, right) {
2928 return Ok((
2929 factual_equal_success_by_builtin_reason(
2930 left,
2931 right,
2932 line_file,
2933 "they are the same",
2934 ),
2935 left.clone(),
2936 right.clone(),
2937 ));
2938 }
2939
2940 let left_resolved = self.resolve_obj(left);
2941 let right_resolved = self.resolve_obj(right);
2942
2943 if left_resolved.two_objs_can_be_calculated_and_equal_by_calculation(&right_resolved) {
2944 return Ok((
2945 factual_equal_success_by_builtin_reason(left, right, line_file, "calculation"),
2946 left_resolved,
2947 right_resolved,
2948 ));
2949 }
2950
2951 Ok((
2952 StmtResult::StmtUnknown(StmtUnknown::new()),
2953 left_resolved,
2954 right_resolved,
2955 ))
2956 }
2957}