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_mod_one_equals_zero(
592 &mut self,
593 left: &Obj,
594 right: &Obj,
595 line_file: LineFile,
596 ) -> Result<Option<StmtResult>, RuntimeError> {
597 let mod_obj = if Self::obj_is_builtin_literal_zero(left) {
598 match right {
599 Obj::Mod(m) => m,
600 _ => return Ok(None),
601 }
602 } else if Self::obj_is_builtin_literal_zero(right) {
603 match left {
604 Obj::Mod(m) => m,
605 _ => return Ok(None),
606 }
607 } else {
608 return Ok(None);
609 };
610 if !Self::obj_is_builtin_literal_one(mod_obj.right.as_ref()) {
611 return Ok(None);
612 }
613 Ok(Some(factual_equal_success_by_builtin_reason(
614 left,
615 right,
616 line_file,
617 "equality: x % 1 = 0",
618 )))
619 }
620
621 fn try_verify_pow_one_identity(
624 &mut self,
625 left: &Obj,
626 right: &Obj,
627 line_file: LineFile,
628 verify_state: &VerifyState,
629 ) -> Result<Option<StmtResult>, RuntimeError> {
630 let (pow, other) = match (left, right) {
631 (Obj::Pow(p), other) => (p, other),
632 (other, Obj::Pow(p)) => (p, other),
633 _ => return Ok(None),
634 };
635 if !Self::obj_is_builtin_literal_one(pow.exponent.as_ref()) {
636 return Ok(None);
637 }
638 if !self
639 .verify_objs_are_equal(pow.base.as_ref(), other, line_file.clone(), verify_state)?
640 .is_true()
641 {
642 return Ok(None);
643 }
644 Ok(Some(factual_equal_success_by_builtin_reason(
645 left,
646 right,
647 line_file,
648 "equality: a^1 = a",
649 )))
650 }
651
652 fn power_factor_matches_base_and_exponent(
653 &mut self,
654 factor: &Obj,
655 base: &Obj,
656 exponent: &Obj,
657 line_file: LineFile,
658 verify_state: &VerifyState,
659 ) -> Result<bool, RuntimeError> {
660 let Obj::Pow(pow) = factor else {
661 if !Self::obj_is_builtin_literal_one(exponent) {
662 return Ok(false);
663 }
664 return Ok(self
665 .verify_objs_are_equal(base, factor, line_file.clone(), verify_state)?
666 .is_true());
667 };
668 if !self
669 .verify_objs_are_equal(base, pow.base.as_ref(), line_file.clone(), verify_state)?
670 .is_true()
671 {
672 return Ok(false);
673 }
674 Ok(self
675 .verify_objs_are_equal(
676 exponent,
677 pow.exponent.as_ref(),
678 line_file.clone(),
679 verify_state,
680 )?
681 .is_true())
682 }
683
684 fn obj_is_verified_in_n_pos(
685 &mut self,
686 obj: &Obj,
687 line_file: LineFile,
688 verify_state: &VerifyState,
689 ) -> Result<bool, RuntimeError> {
690 let in_n_pos: AtomicFact =
691 InFact::new(obj.clone(), StandardSet::NPos.into(), line_file).into();
692 Ok(self
693 .verify_non_equational_known_then_builtin_rules_only(&in_n_pos, verify_state)?
694 .is_true())
695 }
696
697 fn power_addition_exponent_rule_holds_one_direction(
698 &mut self,
699 combined_power: &Pow,
700 product: &Mul,
701 line_file: LineFile,
702 verify_state: &VerifyState,
703 ) -> Result<bool, RuntimeError> {
704 let Obj::Add(add_exponent) = combined_power.exponent.as_ref() else {
705 return Ok(false);
706 };
707
708 let candidates = [
711 (
712 product.left.as_ref(),
713 product.right.as_ref(),
714 add_exponent.left.as_ref(),
715 add_exponent.right.as_ref(),
716 ),
717 (
718 product.right.as_ref(),
719 product.left.as_ref(),
720 add_exponent.left.as_ref(),
721 add_exponent.right.as_ref(),
722 ),
723 ];
724
725 for (left_factor, right_factor, left_exp, right_exp) in candidates {
726 if !self.power_factor_matches_base_and_exponent(
727 left_factor,
728 combined_power.base.as_ref(),
729 left_exp,
730 line_file.clone(),
731 verify_state,
732 )? {
733 continue;
734 }
735 if !self.power_factor_matches_base_and_exponent(
736 right_factor,
737 combined_power.base.as_ref(),
738 right_exp,
739 line_file.clone(),
740 verify_state,
741 )? {
742 continue;
743 }
744 if !self.obj_is_verified_in_n_pos(left_exp, line_file.clone(), verify_state)? {
745 return Ok(false);
746 }
747 if !self.obj_is_verified_in_n_pos(right_exp, line_file.clone(), verify_state)? {
748 return Ok(false);
749 }
750 return Ok(true);
751 }
752
753 Ok(false)
754 }
755
756 fn try_verify_power_addition_exponent_rule(
757 &mut self,
758 left: &Obj,
759 right: &Obj,
760 line_file: LineFile,
761 verify_state: &VerifyState,
762 ) -> Result<Option<StmtResult>, RuntimeError> {
763 let holds = match (left, right) {
764 (Obj::Pow(pow), Obj::Mul(product)) => self
765 .power_addition_exponent_rule_holds_one_direction(
766 pow,
767 product,
768 line_file.clone(),
769 verify_state,
770 )?,
771 (Obj::Mul(product), Obj::Pow(pow)) => self
772 .power_addition_exponent_rule_holds_one_direction(
773 pow,
774 product,
775 line_file.clone(),
776 verify_state,
777 )?,
778 _ => false,
779 };
780 if holds {
781 return Ok(Some(factual_equal_success_by_builtin_reason(
782 left,
783 right,
784 line_file,
785 "equality: a^(m+n) = a^m * a^n for m,n in N_pos",
786 )));
787 }
788 Ok(None)
789 }
790
791 fn verify_context_arg_equality(
792 &mut self,
793 left: &Obj,
794 right: &Obj,
795 line_file: LineFile,
796 verify_state: &VerifyState,
797 ) -> Result<bool, RuntimeError> {
798 Ok(self
799 .verify_objs_are_equal(left, right, line_file, verify_state)?
800 .is_true())
801 }
802
803 fn try_verify_same_algebra_context_by_equal_args(
806 &mut self,
807 left: &Obj,
808 right: &Obj,
809 line_file: LineFile,
810 verify_state: &VerifyState,
811 ) -> Result<Option<StmtResult>, RuntimeError> {
812 let args_equal = match (left, right) {
813 (Obj::Add(l), Obj::Add(r)) => {
814 self.verify_context_arg_equality(
815 l.left.as_ref(),
816 r.left.as_ref(),
817 line_file.clone(),
818 verify_state,
819 )? && self.verify_context_arg_equality(
820 l.right.as_ref(),
821 r.right.as_ref(),
822 line_file.clone(),
823 verify_state,
824 )?
825 }
826 (Obj::Sub(l), Obj::Sub(r)) => {
827 self.verify_context_arg_equality(
828 l.left.as_ref(),
829 r.left.as_ref(),
830 line_file.clone(),
831 verify_state,
832 )? && self.verify_context_arg_equality(
833 l.right.as_ref(),
834 r.right.as_ref(),
835 line_file.clone(),
836 verify_state,
837 )?
838 }
839 (Obj::Mul(l), Obj::Mul(r)) => {
840 self.verify_context_arg_equality(
841 l.left.as_ref(),
842 r.left.as_ref(),
843 line_file.clone(),
844 verify_state,
845 )? && self.verify_context_arg_equality(
846 l.right.as_ref(),
847 r.right.as_ref(),
848 line_file.clone(),
849 verify_state,
850 )?
851 }
852 (Obj::Div(l), Obj::Div(r)) => {
853 self.verify_context_arg_equality(
854 l.left.as_ref(),
855 r.left.as_ref(),
856 line_file.clone(),
857 verify_state,
858 )? && self.verify_context_arg_equality(
859 l.right.as_ref(),
860 r.right.as_ref(),
861 line_file.clone(),
862 verify_state,
863 )?
864 }
865 (Obj::Mod(l), Obj::Mod(r)) => {
866 self.verify_context_arg_equality(
867 l.left.as_ref(),
868 r.left.as_ref(),
869 line_file.clone(),
870 verify_state,
871 )? && self.verify_context_arg_equality(
872 l.right.as_ref(),
873 r.right.as_ref(),
874 line_file.clone(),
875 verify_state,
876 )?
877 }
878 (Obj::Pow(l), Obj::Pow(r)) => {
879 self.verify_context_arg_equality(
880 l.base.as_ref(),
881 r.base.as_ref(),
882 line_file.clone(),
883 verify_state,
884 )? && self.verify_context_arg_equality(
885 l.exponent.as_ref(),
886 r.exponent.as_ref(),
887 line_file.clone(),
888 verify_state,
889 )?
890 }
891 _ => return Ok(None),
892 };
893 if !args_equal {
894 return Ok(None);
895 }
896 Ok(Some(factual_equal_success_by_builtin_reason(
897 left,
898 right,
899 line_file,
900 "equality: same algebraic context with equal arguments",
901 )))
902 }
903
904 fn try_verify_log_identity_equalities(
906 &mut self,
907 left: &Obj,
908 right: &Obj,
909 line_file: LineFile,
910 verify_state: &VerifyState,
911 ) -> Result<Option<StmtResult>, RuntimeError> {
912 let (log, other) = match (left, right) {
913 (Obj::Log(l), o) => (l, o),
914 (o, Obj::Log(l)) => (l, o),
915 _ => return Ok(None),
916 };
917
918 if let Obj::Pow(p) = log.arg.as_ref() {
919 let base_ok = self.verify_objs_are_equal(
920 p.base.as_ref(),
921 log.base.as_ref(),
922 line_file.clone(),
923 verify_state,
924 )?;
925 if base_ok.is_true() {
926 let exp_ok = self.verify_objs_are_equal(
927 p.exponent.as_ref(),
928 other,
929 line_file.clone(),
930 verify_state,
931 )?;
932 if exp_ok.is_true() {
933 return Ok(Some(factual_equal_success_by_builtin_reason(
934 left,
935 right,
936 line_file,
937 "equality: log(a, a^b) = b",
938 )));
939 }
940 }
941 }
942
943 Ok(None)
944 }
945
946 fn try_verify_log_base_power_rule(
948 &mut self,
949 left: &Obj,
950 right: &Obj,
951 line_file: LineFile,
952 verify_state: &VerifyState,
953 ) -> Result<Option<StmtResult>, RuntimeError> {
954 let (log, other) = match (left, right) {
955 (Obj::Log(l), o) => (l, o),
956 (o, Obj::Log(l)) => (l, o),
957 _ => return Ok(None),
958 };
959 let Obj::Pow(p) = log.base.as_ref() else {
960 return Ok(None);
961 };
962 let inner_log: Obj = Log::new((*p.base).clone(), (*log.arg).clone()).into();
963 let expected: Obj = Div::new(inner_log, (*p.exponent).clone()).into();
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^b, c) = log(a, c) / b",
972 )));
973 }
974 Ok(None)
975 }
976
977 fn try_verify_log_arg_power_rule(
979 &mut self,
980 left: &Obj,
981 right: &Obj,
982 line_file: LineFile,
983 verify_state: &VerifyState,
984 ) -> Result<Option<StmtResult>, RuntimeError> {
985 let (log, other) = match (left, right) {
986 (Obj::Log(l), o) => (l, o),
987 (o, Obj::Log(l)) => (l, o),
988 _ => return Ok(None),
989 };
990 let Obj::Pow(p) = log.arg.as_ref() else {
991 return Ok(None);
992 };
993 let inner_log: Obj = Log::new((*log.base).clone(), (*p.base).clone()).into();
994 let expected1: Obj = Mul::new((*p.exponent).clone(), inner_log.clone()).into();
995 let expected2: Obj = Mul::new(inner_log, (*p.exponent).clone()).into();
996 for expected in [expected1, expected2] {
997 let inner =
998 self.verify_objs_are_equal(other, &expected, line_file.clone(), verify_state)?;
999 if inner.is_true() {
1000 return Ok(Some(factual_equal_success_by_builtin_reason(
1001 left,
1002 right,
1003 line_file,
1004 "equality: log(a, x^b) = b * log(a, x)",
1005 )));
1006 }
1007 }
1008 Ok(None)
1009 }
1010
1011 fn try_verify_log_product_rule(
1013 &mut self,
1014 left: &Obj,
1015 right: &Obj,
1016 line_file: LineFile,
1017 verify_state: &VerifyState,
1018 ) -> Result<Option<StmtResult>, RuntimeError> {
1019 let (log, other) = match (left, right) {
1020 (Obj::Log(l), o) => (l, o),
1021 (o, Obj::Log(l)) => (l, o),
1022 _ => return Ok(None),
1023 };
1024 let Obj::Mul(m) = log.arg.as_ref() else {
1025 return Ok(None);
1026 };
1027 let l1: Obj = Log::new((*log.base).clone(), (*m.left).clone()).into();
1028 let l2: Obj = Log::new((*log.base).clone(), (*m.right).clone()).into();
1029 let expected1: Obj = Add::new(l1.clone(), l2.clone()).into();
1030 let expected2: Obj = Add::new(l2, l1).into();
1031 for expected in [expected1, expected2] {
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 }
1043 Ok(None)
1044 }
1045
1046 fn try_verify_log_quotient_rule(
1048 &mut self,
1049 left: &Obj,
1050 right: &Obj,
1051 line_file: LineFile,
1052 verify_state: &VerifyState,
1053 ) -> Result<Option<StmtResult>, RuntimeError> {
1054 let (log, other) = match (left, right) {
1055 (Obj::Log(l), o) => (l, o),
1056 (o, Obj::Log(l)) => (l, o),
1057 _ => return Ok(None),
1058 };
1059 let Obj::Div(d) = log.arg.as_ref() else {
1060 return Ok(None);
1061 };
1062 let l1: Obj = Log::new((*log.base).clone(), (*d.left).clone()).into();
1063 let l2: Obj = Log::new((*log.base).clone(), (*d.right).clone()).into();
1064 let expected = Sub::new(l1, l2).into();
1065 let inner =
1066 self.verify_objs_are_equal(other, &expected, line_file.clone(), verify_state)?;
1067 if inner.is_true() {
1068 return Ok(Some(factual_equal_success_by_builtin_reason(
1069 left,
1070 right,
1071 line_file,
1072 "equality: log(a, x/y) = log(a, x) - log(a, y)",
1073 )));
1074 }
1075 Ok(None)
1076 }
1077
1078 fn try_verify_log_algebra_identities(
1080 &mut self,
1081 left: &Obj,
1082 right: &Obj,
1083 line_file: LineFile,
1084 verify_state: &VerifyState,
1085 ) -> Result<Option<StmtResult>, RuntimeError> {
1086 if let Some(done) =
1087 self.try_verify_log_base_power_rule(left, right, line_file.clone(), verify_state)?
1088 {
1089 return Ok(Some(done));
1090 }
1091 if let Some(done) =
1092 self.try_verify_log_arg_power_rule(left, right, line_file.clone(), verify_state)?
1093 {
1094 return Ok(Some(done));
1095 }
1096 if let Some(done) =
1097 self.try_verify_log_product_rule(left, right, line_file.clone(), verify_state)?
1098 {
1099 return Ok(Some(done));
1100 }
1101 if let Some(done) =
1102 self.try_verify_log_quotient_rule(left, right, line_file.clone(), verify_state)?
1103 {
1104 return Ok(Some(done));
1105 }
1106 Ok(None)
1107 }
1108
1109 fn try_verify_anonymous_fn_application_equals_other_side(
1112 &mut self,
1113 statement_left: &Obj,
1114 statement_right: &Obj,
1115 application_side: &Obj,
1116 other_side: &Obj,
1117 line_file: LineFile,
1118 verify_state: &VerifyState,
1119 ) -> Result<Option<StmtResult>, RuntimeError> {
1120 let Obj::FnObj(fn_obj) = application_side else {
1121 return Ok(None);
1122 };
1123 let FnObjHead::AnonymousFnLiteral(af) = fn_obj.head.as_ref() else {
1124 return Ok(None);
1125 };
1126 if fn_obj.body.is_empty() {
1127 return Ok(None);
1128 }
1129 let param_defs = &af.body.params_def_with_set;
1130 let n_params = ParamGroupWithSet::number_of_params(param_defs);
1131 if n_params == 0 {
1132 return Ok(None);
1133 }
1134 let mut args: Vec<Obj> = Vec::new();
1135 for g in fn_obj.body.iter() {
1136 for b in g.iter() {
1137 args.push((**b).clone());
1138 }
1139 }
1140 if args.len() != n_params {
1141 return Ok(None);
1142 }
1143 let param_to_arg_map =
1144 ParamGroupWithSet::param_defs_and_args_to_param_to_arg_map(param_defs, &args);
1145 let reduced =
1146 self.inst_obj(af.equal_to.as_ref(), ¶m_to_arg_map, ParamObjType::FnSet)?;
1147 let inner =
1148 self.verify_objs_are_equal(&reduced, other_side, line_file.clone(), verify_state)?;
1149 if inner.is_true() {
1150 return Ok(Some(factual_equal_success_by_builtin_reason(
1151 statement_left,
1152 statement_right,
1153 line_file,
1154 "equality: anonymous function application — substitute args into the body, equals the other side",
1155 )));
1156 }
1157 Ok(None)
1158 }
1159
1160 fn try_verify_log_equals_by_pow_inverse(
1162 &mut self,
1163 left: &Obj,
1164 right: &Obj,
1165 line_file: LineFile,
1166 verify_state: &VerifyState,
1167 ) -> Result<Option<StmtResult>, RuntimeError> {
1168 let (log, other) = match (left, right) {
1169 (Obj::Log(l), o) => (l, o),
1170 (o, Obj::Log(l)) => (l, o),
1171 _ => return Ok(None),
1172 };
1173 let pow_obj: Obj = Pow::new((*log.base).clone(), other.clone()).into();
1174 let inner = self.verify_objs_are_equal(
1175 &pow_obj,
1176 log.arg.as_ref(),
1177 line_file.clone(),
1178 verify_state,
1179 )?;
1180 if inner.is_true() {
1181 return Ok(Some(factual_equal_success_by_builtin_reason(
1182 left,
1183 right,
1184 line_file,
1185 "equality: log(a, b) = c from a^c = b",
1186 )));
1187 }
1188 Ok(None)
1189 }
1190
1191 fn try_verify_sum_additivity(
1194 &mut self,
1195 left: &Obj,
1196 right: &Obj,
1197 line_file: LineFile,
1198 verify_state: &VerifyState,
1199 ) -> Result<Option<StmtResult>, RuntimeError> {
1200 if !verify_state.is_round_0() {
1201 return Ok(None);
1202 }
1203
1204 let (sum_m, sum_a, sum_b) = match (left, right) {
1205 (Obj::Sum(m), Obj::Add(a)) => match (a.left.as_ref(), a.right.as_ref()) {
1206 (Obj::Sum(a1), Obj::Sum(a2)) => (m, a1, a2),
1207 _ => return Ok(None),
1208 },
1209 (Obj::Add(a), Obj::Sum(m)) => match (a.left.as_ref(), a.right.as_ref()) {
1210 (Obj::Sum(a1), Obj::Sum(a2)) => (m, a1, a2),
1211 _ => return Ok(None),
1212 },
1213 _ => return Ok(None),
1214 };
1215
1216 let mut require_eq = |a: &Obj, b: &Obj| -> Result<bool, RuntimeError> {
1217 Ok(self
1218 .verify_objs_are_equal(a, b, line_file.clone(), verify_state)?
1219 .is_true())
1220 };
1221 if !require_eq(sum_m.start.as_ref(), sum_a.start.as_ref())? {
1222 return Ok(None);
1223 }
1224 if !require_eq(sum_m.start.as_ref(), sum_b.start.as_ref())? {
1225 return Ok(None);
1226 }
1227 if !require_eq(sum_m.end.as_ref(), sum_a.end.as_ref())? {
1228 return Ok(None);
1229 }
1230 if !require_eq(sum_m.end.as_ref(), sum_b.end.as_ref())? {
1231 return Ok(None);
1232 }
1233
1234 let x_name = self.generate_random_unused_name();
1235 let x_obj = obj_for_bound_param_in_scope(x_name.clone(), ParamObjType::Forall);
1236
1237 let Some(l_inst) =
1238 self.instantiate_unary_anonymous_summand_at(sum_m.func.as_ref(), &x_obj)?
1239 else {
1240 return Ok(None);
1241 };
1242 let Some(a_inst) =
1243 self.instantiate_unary_anonymous_summand_at(sum_a.func.as_ref(), &x_obj)?
1244 else {
1245 return Ok(None);
1246 };
1247 let Some(b_inst) =
1248 self.instantiate_unary_anonymous_summand_at(sum_b.func.as_ref(), &x_obj)?
1249 else {
1250 return Ok(None);
1251 };
1252
1253 let then_fact: ExistOrAndChainAtomicFact =
1254 EqualFact::new(l_inst, Add::new(a_inst, b_inst).into(), line_file.clone()).into();
1255
1256 let dom_lo: Fact =
1257 LessEqualFact::new((*sum_m.start).clone(), x_obj.clone(), line_file.clone()).into();
1258 let dom_hi: Fact =
1259 LessEqualFact::new(x_obj.clone(), (*sum_m.end).clone(), line_file.clone()).into();
1260
1261 let forall_fact: Fact = ForallFact::new(
1262 ParamDefWithType::new(vec![ParamGroupWithParamType::new(
1263 vec![x_name],
1264 ParamType::Obj(StandardSet::Z.into()),
1265 )]),
1266 vec![dom_lo, dom_hi],
1267 vec![then_fact],
1268 line_file.clone(),
1269 )?
1270 .into();
1271
1272 let r = self.verify_fact(&forall_fact, verify_state)?;
1273 if r.is_true() {
1274 return Ok(Some(factual_equal_success_by_builtin_reason(
1275 left,
1276 right,
1277 line_file,
1278 "equality: sum additivity from pointwise equality on the integer index range",
1279 )));
1280 }
1281 Ok(None)
1282 }
1283
1284 fn instantiate_unary_anonymous_summand_at(
1285 &mut self,
1286 func: &Obj,
1287 x: &Obj,
1288 ) -> Result<Option<Obj>, RuntimeError> {
1289 let af: &AnonymousFn = match func {
1290 Obj::AnonymousFn(af) => af,
1291 Obj::FnObj(fo) => {
1292 if !fo.body.is_empty() {
1293 return Ok(None);
1294 }
1295 match fo.head.as_ref() {
1296 FnObjHead::AnonymousFnLiteral(a) => a.as_ref(),
1297 _ => return Ok(None),
1298 }
1299 }
1300 _ => return Ok(None),
1301 };
1302 if ParamGroupWithSet::number_of_params(&af.body.params_def_with_set) != 1 {
1303 return Ok(None);
1304 }
1305 let param_defs = &af.body.params_def_with_set;
1306 let args = vec![x.clone()];
1307 let param_to_arg_map =
1308 ParamGroupWithSet::param_defs_and_args_to_param_to_arg_map(param_defs, &args);
1309 Ok(Some(self.inst_obj(
1310 af.equal_to.as_ref(),
1311 ¶m_to_arg_map,
1312 ParamObjType::FnSet,
1313 )?))
1314 }
1315
1316 fn try_verify_sum_merge_adjacent_ranges(
1318 &mut self,
1319 left: &Obj,
1320 right: &Obj,
1321 line_file: LineFile,
1322 verify_state: &VerifyState,
1323 ) -> Result<Option<StmtResult>, RuntimeError> {
1324 if !verify_state.is_round_0() {
1325 return Ok(None);
1326 }
1327 let (add, s3) = match (left, right) {
1328 (Obj::Add(a), Obj::Sum(s)) => (a, s),
1329 (Obj::Sum(s), Obj::Add(a)) => (a, s),
1330 _ => return Ok(None),
1331 };
1332 let (s1, s2) = match (add.left.as_ref(), add.right.as_ref()) {
1333 (Obj::Sum(x), Obj::Sum(y)) => (x, y),
1334 _ => return Ok(None),
1335 };
1336 for (a, b) in [(s1, s2), (s2, s1)] {
1337 if let Some(done) = self.try_verify_sum_merge_ordered_pair(
1338 a,
1339 b,
1340 s3,
1341 left,
1342 right,
1343 line_file.clone(),
1344 verify_state,
1345 )? {
1346 return Ok(Some(done));
1347 }
1348 }
1349 Ok(None)
1350 }
1351
1352 fn try_verify_sum_merge_ordered_pair(
1353 &mut self,
1354 s1: &Sum,
1355 s2: &Sum,
1356 s3: &Sum,
1357 stmt_left: &Obj,
1358 stmt_right: &Obj,
1359 line_file: LineFile,
1360 verify_state: &VerifyState,
1361 ) -> Result<Option<StmtResult>, RuntimeError> {
1362 let one: Obj = Number::new("1".to_string()).into();
1363 let gap = Add::new((*s1.end).clone(), one).into();
1364 if !self
1365 .verify_objs_are_equal(&gap, s2.start.as_ref(), line_file.clone(), verify_state)?
1366 .is_true()
1367 {
1368 return Ok(None);
1369 }
1370 if !self
1371 .verify_objs_are_equal(
1372 s1.start.as_ref(),
1373 s3.start.as_ref(),
1374 line_file.clone(),
1375 verify_state,
1376 )?
1377 .is_true()
1378 {
1379 return Ok(None);
1380 }
1381 if !self
1382 .verify_objs_are_equal(
1383 s2.end.as_ref(),
1384 s3.end.as_ref(),
1385 line_file.clone(),
1386 verify_state,
1387 )?
1388 .is_true()
1389 {
1390 return Ok(None);
1391 }
1392 if !self
1393 .verify_objs_are_equal(
1394 s1.func.as_ref(),
1395 s2.func.as_ref(),
1396 line_file.clone(),
1397 verify_state,
1398 )?
1399 .is_true()
1400 {
1401 return Ok(None);
1402 }
1403 if !self
1404 .verify_objs_are_equal(
1405 s1.func.as_ref(),
1406 s3.func.as_ref(),
1407 line_file.clone(),
1408 verify_state,
1409 )?
1410 .is_true()
1411 {
1412 return Ok(None);
1413 }
1414 Ok(Some(factual_equal_success_by_builtin_reason(
1415 stmt_left,
1416 stmt_right,
1417 line_file,
1418 "equality: merge adjacent sum ranges with the same summand",
1419 )))
1420 }
1421
1422 fn try_verify_sum_split_last_term(
1424 &mut self,
1425 left: &Obj,
1426 right: &Obj,
1427 line_file: LineFile,
1428 verify_state: &VerifyState,
1429 ) -> Result<Option<StmtResult>, RuntimeError> {
1430 if !verify_state.is_round_0() {
1431 return Ok(None);
1432 }
1433 let one: Obj = Number::new("1".to_string()).into();
1434 for (full_obj, add_obj) in [(left, right), (right, left)] {
1435 let Obj::Sum(s_full) = full_obj else {
1436 continue;
1437 };
1438 let Obj::Add(a) = add_obj else {
1439 continue;
1440 };
1441 for (sum_part, tail) in [
1442 (a.left.as_ref(), a.right.as_ref()),
1443 (a.right.as_ref(), a.left.as_ref()),
1444 ] {
1445 let Obj::Sum(s_pre) = sum_part else {
1446 continue;
1447 };
1448 if !self
1449 .verify_objs_are_equal(
1450 s_full.start.as_ref(),
1451 s_pre.start.as_ref(),
1452 line_file.clone(),
1453 verify_state,
1454 )?
1455 .is_true()
1456 {
1457 continue;
1458 }
1459 let end_pre_plus_one: Obj = Add::new((*s_pre.end).clone(), one.clone()).into();
1460 if !self
1461 .verify_objs_are_equal(
1462 s_full.end.as_ref(),
1463 &end_pre_plus_one,
1464 line_file.clone(),
1465 verify_state,
1466 )?
1467 .is_true()
1468 {
1469 continue;
1470 }
1471 if !self
1472 .verify_objs_are_equal(
1473 s_full.func.as_ref(),
1474 s_pre.func.as_ref(),
1475 line_file.clone(),
1476 verify_state,
1477 )?
1478 .is_true()
1479 {
1480 continue;
1481 }
1482 let Some(expected_tail) = self.instantiate_unary_anonymous_summand_at(
1483 s_full.func.as_ref(),
1484 s_full.end.as_ref(),
1485 )?
1486 else {
1487 continue;
1488 };
1489 if !self
1490 .verify_objs_are_equal(&expected_tail, tail, line_file.clone(), verify_state)?
1491 .is_true()
1492 {
1493 continue;
1494 }
1495 return Ok(Some(factual_equal_success_by_builtin_reason(
1496 left,
1497 right,
1498 line_file,
1499 "equality: sum through e equals sum through e-1 plus last summand f(e)",
1500 )));
1501 }
1502 }
1503 Ok(None)
1504 }
1505
1506 fn try_verify_product_split_last_term(
1508 &mut self,
1509 left: &Obj,
1510 right: &Obj,
1511 line_file: LineFile,
1512 verify_state: &VerifyState,
1513 ) -> Result<Option<StmtResult>, RuntimeError> {
1514 if !verify_state.is_round_0() {
1515 return Ok(None);
1516 }
1517 let one: Obj = Number::new("1".to_string()).into();
1518 for (full_obj, mul_obj) in [(left, right), (right, left)] {
1519 let Obj::Product(p_full) = full_obj else {
1520 continue;
1521 };
1522 let Obj::Mul(m) = mul_obj else {
1523 continue;
1524 };
1525 for (prod_part, tail) in [
1526 (m.left.as_ref(), m.right.as_ref()),
1527 (m.right.as_ref(), m.left.as_ref()),
1528 ] {
1529 let Obj::Product(p_pre) = prod_part else {
1530 continue;
1531 };
1532 if !self
1533 .verify_objs_are_equal(
1534 p_full.start.as_ref(),
1535 p_pre.start.as_ref(),
1536 line_file.clone(),
1537 verify_state,
1538 )?
1539 .is_true()
1540 {
1541 continue;
1542 }
1543 let end_pre_plus_one: Obj = Add::new((*p_pre.end).clone(), one.clone()).into();
1544 if !self
1545 .verify_objs_are_equal(
1546 p_full.end.as_ref(),
1547 &end_pre_plus_one,
1548 line_file.clone(),
1549 verify_state,
1550 )?
1551 .is_true()
1552 {
1553 continue;
1554 }
1555 if !self
1556 .verify_objs_are_equal(
1557 p_full.func.as_ref(),
1558 p_pre.func.as_ref(),
1559 line_file.clone(),
1560 verify_state,
1561 )?
1562 .is_true()
1563 {
1564 continue;
1565 }
1566 let Some(expected_tail) = self.instantiate_unary_anonymous_summand_at(
1567 p_full.func.as_ref(),
1568 p_full.end.as_ref(),
1569 )?
1570 else {
1571 continue;
1572 };
1573 if !self
1574 .verify_objs_are_equal(&expected_tail, tail, line_file.clone(), verify_state)?
1575 .is_true()
1576 {
1577 continue;
1578 }
1579 return Ok(Some(factual_equal_success_by_builtin_reason(
1580 left,
1581 right,
1582 line_file,
1583 "equality: product through e equals product through e-1 times last factor f(e)",
1584 )));
1585 }
1586 }
1587 Ok(None)
1588 }
1589
1590 fn flatten_left_assoc_add_chain(obj: &Obj) -> Vec<&Obj> {
1591 match obj {
1592 Obj::Add(a) => {
1593 let mut v = Self::flatten_left_assoc_add_chain(a.left.as_ref());
1594 v.push(a.right.as_ref());
1595 v
1596 }
1597 _ => vec![obj],
1598 }
1599 }
1600
1601 fn flatten_left_assoc_mul_chain(obj: &Obj) -> Vec<&Obj> {
1602 match obj {
1603 Obj::Mul(m) => {
1604 let mut v = Self::flatten_left_assoc_mul_chain(m.left.as_ref());
1605 v.push(m.right.as_ref());
1606 v
1607 }
1608 _ => vec![obj],
1609 }
1610 }
1611
1612 fn try_verify_sum_partition_adjacent_ranges(
1614 &mut self,
1615 left: &Obj,
1616 right: &Obj,
1617 line_file: LineFile,
1618 verify_state: &VerifyState,
1619 ) -> Result<Option<StmtResult>, RuntimeError> {
1620 if !verify_state.is_round_0() {
1621 return Ok(None);
1622 }
1623 let one: Obj = Number::new("1".to_string()).into();
1624 for (full_side, add_side) in [(left, right), (right, left)] {
1625 let Obj::Sum(s_full) = full_side else {
1626 continue;
1627 };
1628 let Obj::Add(_) = add_side else {
1629 continue;
1630 };
1631 let parts = Self::flatten_left_assoc_add_chain(add_side);
1632 if parts.len() < 2 {
1633 continue;
1634 }
1635 let mut sums: Vec<&Sum> = Vec::with_capacity(parts.len());
1636 let mut all_sum = true;
1637 for p in &parts {
1638 if let Obj::Sum(s) = p {
1639 sums.push(s);
1640 } else {
1641 all_sum = false;
1642 break;
1643 }
1644 }
1645 if !all_sum {
1646 continue;
1647 }
1648 if !self
1649 .verify_objs_are_equal(
1650 s_full.start.as_ref(),
1651 sums[0].start.as_ref(),
1652 line_file.clone(),
1653 verify_state,
1654 )?
1655 .is_true()
1656 {
1657 continue;
1658 }
1659 if !self
1660 .verify_objs_are_equal(
1661 s_full.end.as_ref(),
1662 sums[sums.len() - 1].end.as_ref(),
1663 line_file.clone(),
1664 verify_state,
1665 )?
1666 .is_true()
1667 {
1668 continue;
1669 }
1670 let mut gaps_ok = true;
1671 for i in 0..sums.len().saturating_sub(1) {
1672 let gap = Add::new((*sums[i].end).clone(), one.clone()).into();
1673 if !self
1674 .verify_objs_are_equal(
1675 &gap,
1676 sums[i + 1].start.as_ref(),
1677 line_file.clone(),
1678 verify_state,
1679 )?
1680 .is_true()
1681 {
1682 gaps_ok = false;
1683 break;
1684 }
1685 }
1686 if !gaps_ok {
1687 continue;
1688 }
1689 let mut func_ok = true;
1690 for s in &sums {
1691 if !self
1692 .verify_objs_are_equal(
1693 s_full.func.as_ref(),
1694 s.func.as_ref(),
1695 line_file.clone(),
1696 verify_state,
1697 )?
1698 .is_true()
1699 {
1700 func_ok = false;
1701 break;
1702 }
1703 }
1704 if !func_ok {
1705 continue;
1706 }
1707 return Ok(Some(factual_equal_success_by_builtin_reason(
1708 left,
1709 right,
1710 line_file,
1711 "equality: sum partitions closed range into adjacent sub-sums with the same summand",
1712 )));
1713 }
1714 Ok(None)
1715 }
1716
1717 fn try_verify_product_partition_adjacent_ranges(
1719 &mut self,
1720 left: &Obj,
1721 right: &Obj,
1722 line_file: LineFile,
1723 verify_state: &VerifyState,
1724 ) -> Result<Option<StmtResult>, RuntimeError> {
1725 if !verify_state.is_round_0() {
1726 return Ok(None);
1727 }
1728 let one: Obj = Number::new("1".to_string()).into();
1729 for (full_side, mul_side) in [(left, right), (right, left)] {
1730 let Obj::Product(p_full) = full_side else {
1731 continue;
1732 };
1733 let Obj::Mul(_) = mul_side else {
1734 continue;
1735 };
1736 let parts = Self::flatten_left_assoc_mul_chain(mul_side);
1737 if parts.len() < 2 {
1738 continue;
1739 }
1740 let mut products: Vec<&Product> = Vec::with_capacity(parts.len());
1741 let mut all_prod = true;
1742 for p in &parts {
1743 if let Obj::Product(pr) = p {
1744 products.push(pr);
1745 } else {
1746 all_prod = false;
1747 break;
1748 }
1749 }
1750 if !all_prod {
1751 continue;
1752 }
1753 if !self
1754 .verify_objs_are_equal(
1755 p_full.start.as_ref(),
1756 products[0].start.as_ref(),
1757 line_file.clone(),
1758 verify_state,
1759 )?
1760 .is_true()
1761 {
1762 continue;
1763 }
1764 if !self
1765 .verify_objs_are_equal(
1766 p_full.end.as_ref(),
1767 products[products.len() - 1].end.as_ref(),
1768 line_file.clone(),
1769 verify_state,
1770 )?
1771 .is_true()
1772 {
1773 continue;
1774 }
1775 let mut gaps_ok = true;
1776 for i in 0..products.len().saturating_sub(1) {
1777 let gap = Add::new((*products[i].end).clone(), one.clone()).into();
1778 if !self
1779 .verify_objs_are_equal(
1780 &gap,
1781 products[i + 1].start.as_ref(),
1782 line_file.clone(),
1783 verify_state,
1784 )?
1785 .is_true()
1786 {
1787 gaps_ok = false;
1788 break;
1789 }
1790 }
1791 if !gaps_ok {
1792 continue;
1793 }
1794 let mut func_ok = true;
1795 for p in &products {
1796 if !self
1797 .verify_objs_are_equal(
1798 p_full.func.as_ref(),
1799 p.func.as_ref(),
1800 line_file.clone(),
1801 verify_state,
1802 )?
1803 .is_true()
1804 {
1805 func_ok = false;
1806 break;
1807 }
1808 }
1809 if !func_ok {
1810 continue;
1811 }
1812 return Ok(Some(factual_equal_success_by_builtin_reason(
1813 left,
1814 right,
1815 line_file,
1816 "equality: product partitions closed range into adjacent sub-products with the same factor",
1817 )));
1818 }
1819 Ok(None)
1820 }
1821
1822 fn try_verify_sum_reindex_shift(
1825 &mut self,
1826 left: &Obj,
1827 right: &Obj,
1828 line_file: LineFile,
1829 verify_state: &VerifyState,
1830 ) -> Result<Option<StmtResult>, RuntimeError> {
1831 if !verify_state.is_round_0() {
1832 return Ok(None);
1833 }
1834 for (l_obj, r_obj) in [(left, right), (right, left)] {
1835 let (Obj::Sum(l_sum), Obj::Sum(r_sum)) = (l_obj, r_obj) else {
1836 continue;
1837 };
1838 let k: Obj = Sub::new((*r_sum.start).clone(), (*l_sum.start).clone()).into();
1839 let k_end = Sub::new((*r_sum.end).clone(), (*l_sum.end).clone()).into();
1840 if !self
1841 .verify_objs_are_equal(&k, &k_end, line_file.clone(), verify_state)?
1842 .is_true()
1843 {
1844 continue;
1845 }
1846 let y_name = self.generate_random_unused_name();
1847 let y_obj = obj_for_bound_param_in_scope(y_name.clone(), ParamObjType::Forall);
1848 let index_for_left = Sub::new(y_obj.clone(), k.clone()).into();
1849 let Some(at_l) =
1850 self.instantiate_unary_anonymous_summand_at(l_sum.func.as_ref(), &index_for_left)?
1851 else {
1852 continue;
1853 };
1854 let Some(at_r) =
1855 self.instantiate_unary_anonymous_summand_at(r_sum.func.as_ref(), &y_obj)?
1856 else {
1857 continue;
1858 };
1859 let then_fact: ExistOrAndChainAtomicFact =
1860 EqualFact::new(at_l, at_r, line_file.clone()).into();
1861 let dom_lo: Fact =
1862 LessEqualFact::new((*r_sum.start).clone(), y_obj.clone(), line_file.clone()).into();
1863 let dom_hi: Fact =
1864 LessEqualFact::new(y_obj.clone(), (*r_sum.end).clone(), line_file.clone()).into();
1865 let forall_fact: Fact = ForallFact::new(
1866 ParamDefWithType::new(vec![ParamGroupWithParamType::new(
1867 vec![y_name],
1868 ParamType::Obj(StandardSet::Z.into()),
1869 )]),
1870 vec![dom_lo, dom_hi],
1871 vec![then_fact],
1872 line_file.clone(),
1873 )?
1874 .into();
1875 let r = self.verify_fact(&forall_fact, verify_state)?;
1876 if r.is_true() {
1877 return Ok(Some(factual_equal_success_by_builtin_reason(
1878 left,
1879 right,
1880 line_file,
1881 "equality: sum reindexing (integer shift) from pointwise equality on the range",
1882 )));
1883 }
1884 }
1885 Ok(None)
1886 }
1887
1888 fn try_verify_sum_constant_summand(
1890 &mut self,
1891 left: &Obj,
1892 right: &Obj,
1893 line_file: LineFile,
1894 verify_state: &VerifyState,
1895 ) -> Result<Option<StmtResult>, RuntimeError> {
1896 if !verify_state.is_round_0() {
1897 return Ok(None);
1898 }
1899 for (sum_side, other) in [(left, right), (right, left)] {
1900 let Obj::Sum(s) = sum_side else {
1901 continue;
1902 };
1903 let af = match s.func.as_ref() {
1904 Obj::AnonymousFn(af) => af,
1905 Obj::FnObj(fo) if fo.body.is_empty() => match fo.head.as_ref() {
1906 FnObjHead::AnonymousFnLiteral(a) => a.as_ref(),
1907 _ => continue,
1908 },
1909 _ => continue,
1910 };
1911 if ParamGroupWithSet::number_of_params(&af.body.params_def_with_set) != 1 {
1912 continue;
1913 }
1914 let names = ParamGroupWithSet::collect_param_names(&af.body.params_def_with_set);
1915 let pname = match names.first() {
1916 Some(n) => n.as_str(),
1917 None => continue,
1918 };
1919 if obj_expr_mentions_bare_id(af.equal_to.as_ref(), pname) {
1920 continue;
1921 }
1922 let c = (*af.equal_to).clone();
1923 let one: Obj = Number::new("1".to_string()).into();
1924 let count: Obj =
1925 Add::new(Sub::new((*s.end).clone(), (*s.start).clone()).into(), one).into();
1926 let m1: Obj = Mul::new(count.clone(), c.clone()).into();
1927 let m2: Obj = Mul::new(c, count).into();
1928 if self
1929 .verify_objs_are_equal(other, &m1, line_file.clone(), verify_state)?
1930 .is_true()
1931 || self
1932 .verify_objs_are_equal(other, &m2, line_file.clone(), verify_state)?
1933 .is_true()
1934 {
1935 return Ok(Some(factual_equal_success_by_builtin_reason(
1936 left,
1937 right,
1938 line_file,
1939 "equality: sum of a constant summand over a closed integer range",
1940 )));
1941 }
1942 }
1943 Ok(None)
1944 }
1945
1946 fn try_verify_mod_nested_same_modulus_absorption(
1951 &mut self,
1952 left: &Obj,
1953 right: &Obj,
1954 line_file: LineFile,
1955 verify_state: &VerifyState,
1956 ) -> Result<Option<StmtResult>, RuntimeError> {
1957 for (side_nested, side_simple) in [(left, right), (right, left)] {
1958 let Obj::Mod(outer) = side_nested else {
1959 continue;
1960 };
1961 let Obj::Mod(inner) = outer.left.as_ref() else {
1962 continue;
1963 };
1964 let Obj::Mod(simple) = side_simple else {
1965 continue;
1966 };
1967 if !self
1968 .verify_objs_are_equal(
1969 outer.right.as_ref(),
1970 inner.right.as_ref(),
1971 line_file.clone(),
1972 verify_state,
1973 )?
1974 .is_true()
1975 {
1976 continue;
1977 }
1978 if !self
1979 .verify_objs_are_equal(
1980 outer.right.as_ref(),
1981 simple.right.as_ref(),
1982 line_file.clone(),
1983 verify_state,
1984 )?
1985 .is_true()
1986 {
1987 continue;
1988 }
1989 if !self
1990 .verify_objs_are_equal(
1991 inner.left.as_ref(),
1992 simple.left.as_ref(),
1993 line_file.clone(),
1994 verify_state,
1995 )?
1996 .is_true()
1997 {
1998 continue;
1999 }
2000 return Ok(Some(factual_equal_success_by_builtin_reason(
2001 left,
2002 right,
2003 line_file,
2004 "equality: nested mod with same modulus absorbs inner mod",
2005 )));
2006 }
2007 Ok(None)
2008 }
2009
2010 fn try_verify_mod_peel_nested_same_modulus(
2013 &mut self,
2014 left: &Obj,
2015 right: &Obj,
2016 line_file: LineFile,
2017 verify_state: &VerifyState,
2018 ) -> Result<Option<StmtResult>, RuntimeError> {
2019 let (Obj::Mod(lm), Obj::Mod(rm)) = (left, right) else {
2020 return Ok(None);
2021 };
2022 if !self
2023 .verify_objs_are_equal(
2024 lm.right.as_ref(),
2025 rm.right.as_ref(),
2026 line_file.clone(),
2027 verify_state,
2028 )?
2029 .is_true()
2030 {
2031 return Ok(None);
2032 }
2033 let modulus = lm.right.as_ref();
2034
2035 if let Obj::Mod(r_inner) = rm.left.as_ref() {
2036 if self
2037 .verify_objs_are_equal(
2038 r_inner.right.as_ref(),
2039 modulus,
2040 line_file.clone(),
2041 verify_state,
2042 )?
2043 .is_true()
2044 {
2045 let lhs: Obj = Mod::new((*lm.left).clone(), (*lm.right).clone()).into();
2046 let rhs: Obj = Mod::new((*r_inner.left).clone(), (*lm.right).clone()).into();
2047 if self
2048 .verify_objs_are_equal(&lhs, &rhs, line_file.clone(), verify_state)?
2049 .is_true()
2050 {
2051 return Ok(Some(factual_equal_success_by_builtin_reason(
2052 left,
2053 right,
2054 line_file,
2055 "equality: mod — peel outer nested % m to reuse residue equality (full verify_objs_are_equal)",
2056 )));
2057 }
2058 }
2059 }
2060
2061 if let Obj::Mod(l_inner) = lm.left.as_ref() {
2062 if self
2063 .verify_objs_are_equal(
2064 l_inner.right.as_ref(),
2065 modulus,
2066 line_file.clone(),
2067 verify_state,
2068 )?
2069 .is_true()
2070 {
2071 let lhs: Obj = Mod::new((*l_inner.left).clone(), (*lm.right).clone()).into();
2072 let rhs: Obj = Mod::new((*rm.left).clone(), (*lm.right).clone()).into();
2073 if self
2074 .verify_objs_are_equal(&lhs, &rhs, line_file.clone(), verify_state)?
2075 .is_true()
2076 {
2077 return Ok(Some(factual_equal_success_by_builtin_reason(
2078 left,
2079 right,
2080 line_file,
2081 "equality: mod — peel outer nested % m to reuse residue equality (full verify_objs_are_equal)",
2082 )));
2083 }
2084 }
2085 }
2086
2087 Ok(None)
2088 }
2089
2090 fn try_verify_mod_congruence_from_inner_binary(
2095 &mut self,
2096 left: &Obj,
2097 right: &Obj,
2098 line_file: LineFile,
2099 verify_state: &VerifyState,
2100 ) -> Result<Option<StmtResult>, RuntimeError> {
2101 let (Obj::Mod(lm), Obj::Mod(rm)) = (left, right) else {
2102 return Ok(None);
2103 };
2104 if !self
2105 .verify_objs_are_equal(
2106 lm.right.as_ref(),
2107 rm.right.as_ref(),
2108 line_file.clone(),
2109 verify_state,
2110 )?
2111 .is_true()
2112 {
2113 return Ok(None);
2114 }
2115 let mut pair_ok = |a: &Obj, b: &Obj| -> Result<bool, RuntimeError> {
2116 let l: Obj = Mod::new(a.clone(), (*lm.right).clone()).into();
2117 let r: Obj = Mod::new(b.clone(), (*rm.right).clone()).into();
2118 Ok(self
2119 .verify_objs_are_equal(&l, &r, line_file.clone(), verify_state)?
2120 .is_true())
2121 };
2122 let ok = match (lm.left.as_ref(), rm.left.as_ref()) {
2123 (Obj::Add(la), Obj::Add(ra)) => {
2124 pair_ok(la.left.as_ref(), ra.left.as_ref())?
2125 && pair_ok(la.right.as_ref(), ra.right.as_ref())?
2126 }
2127 (Obj::Sub(ls), Obj::Sub(rs)) => {
2128 pair_ok(ls.left.as_ref(), rs.left.as_ref())?
2129 && pair_ok(ls.right.as_ref(), rs.right.as_ref())?
2130 }
2131 (Obj::Mul(lx), Obj::Mul(rx)) => {
2132 pair_ok(lx.left.as_ref(), rx.left.as_ref())?
2133 && pair_ok(lx.right.as_ref(), rx.right.as_ref())?
2134 }
2135 _ => return Ok(None),
2136 };
2137 if !ok {
2138 return Ok(None);
2139 }
2140 Ok(Some(factual_equal_success_by_builtin_reason(
2141 left,
2142 right,
2143 line_file,
2144 "equality: integer congruence — same modulus, residues for matching + / - / *",
2145 )))
2146 }
2147
2148 pub fn verify_equality_by_builtin_rules(
2149 &mut self,
2150 left: &Obj,
2151 right: &Obj,
2152 line_file: LineFile,
2153 verify_state: &VerifyState,
2154 ) -> Result<StmtResult, RuntimeError> {
2155 if verify_equality_by_they_are_the_same(left, right) {
2156 return Ok(factual_equal_success_by_builtin_reason(
2157 left,
2158 right,
2159 line_file,
2160 "they are the same",
2161 )
2162 .into());
2163 }
2164
2165 if let Some(done) = self.try_verify_objs_equal_by_expanding_family(
2166 left,
2167 right,
2168 line_file.clone(),
2169 verify_state,
2170 )? {
2171 return Ok(done);
2172 }
2173
2174 if let Some(done) =
2175 self.try_verify_abs_equalities(left, right, line_file.clone(), verify_state)?
2176 {
2177 return Ok(done);
2178 }
2179
2180 if let Some(done) = self.try_verify_zero_equals_subtraction_implies_equal_operands(
2181 left,
2182 right,
2183 line_file.clone(),
2184 verify_state,
2185 )? {
2186 return Ok(done);
2187 }
2188
2189 if let Some(done) = self.try_verify_zero_equals_pow_from_base_zero(
2190 left,
2191 right,
2192 line_file.clone(),
2193 verify_state,
2194 )? {
2195 return Ok(done);
2196 }
2197
2198 if let Some(done) =
2199 self.try_verify_pow_one_identity(left, right, line_file.clone(), verify_state)?
2200 {
2201 return Ok(done);
2202 }
2203
2204 if let Some(done) = self.try_verify_power_addition_exponent_rule(
2205 left,
2206 right,
2207 line_file.clone(),
2208 verify_state,
2209 )? {
2210 return Ok(done);
2211 }
2212
2213 if let Some(done) = self.try_verify_same_algebra_context_by_equal_args(
2214 left,
2215 right,
2216 line_file.clone(),
2217 verify_state,
2218 )? {
2219 return Ok(done);
2220 }
2221
2222 if let Some(done) =
2223 self.try_verify_log_identity_equalities(left, right, line_file.clone(), verify_state)?
2224 {
2225 return Ok(done);
2226 }
2227
2228 if let Some(done) =
2229 self.try_verify_log_algebra_identities(left, right, line_file.clone(), verify_state)?
2230 {
2231 return Ok(done);
2232 }
2233
2234 if let Some(done) =
2235 self.try_verify_log_equals_by_pow_inverse(left, right, line_file.clone(), verify_state)?
2236 {
2237 return Ok(done);
2238 }
2239
2240 if let Some(done) =
2241 self.try_verify_sum_additivity(left, right, line_file.clone(), verify_state)?
2242 {
2243 return Ok(done);
2244 }
2245
2246 if let Some(done) =
2247 self.try_verify_sum_merge_adjacent_ranges(left, right, line_file.clone(), verify_state)?
2248 {
2249 return Ok(done);
2250 }
2251
2252 if let Some(done) =
2253 self.try_verify_sum_split_last_term(left, right, line_file.clone(), verify_state)?
2254 {
2255 return Ok(done);
2256 }
2257
2258 if let Some(done) =
2259 self.try_verify_product_split_last_term(left, right, line_file.clone(), verify_state)?
2260 {
2261 return Ok(done);
2262 }
2263
2264 if let Some(done) = self.try_verify_sum_partition_adjacent_ranges(
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_product_partition_adjacent_ranges(
2274 left,
2275 right,
2276 line_file.clone(),
2277 verify_state,
2278 )? {
2279 return Ok(done);
2280 }
2281
2282 if let Some(done) =
2283 self.try_verify_sum_reindex_shift(left, right, line_file.clone(), verify_state)?
2284 {
2285 return Ok(done);
2286 }
2287
2288 if let Some(done) =
2289 self.try_verify_sum_constant_summand(left, right, line_file.clone(), verify_state)?
2290 {
2291 return Ok(done);
2292 }
2293
2294 if let Some(done) = self.try_verify_mod_nested_same_modulus_absorption(
2295 left,
2296 right,
2297 line_file.clone(),
2298 verify_state,
2299 )? {
2300 return Ok(done);
2301 }
2302
2303 if let Some(done) = self.try_verify_zero_mod_equals_zero(left, right, line_file.clone())? {
2304 return Ok(done);
2305 }
2306
2307 if let Some(done) = self.try_verify_mod_one_equals_zero(left, right, line_file.clone())? {
2308 return Ok(done);
2309 }
2310
2311 if let Some(done) = self.try_verify_mod_peel_nested_same_modulus(
2312 left,
2313 right,
2314 line_file.clone(),
2315 verify_state,
2316 )? {
2317 return Ok(done);
2318 }
2319
2320 if let Some(done) = self.try_verify_mod_congruence_from_inner_binary(
2321 left,
2322 right,
2323 line_file.clone(),
2324 verify_state,
2325 )? {
2326 return Ok(done);
2327 }
2328
2329 let (result, calculated_left, calculated_right) = self
2330 .verify_equality_by_they_are_the_same_and_calculation(
2331 left,
2332 right,
2333 line_file.clone(),
2334 verify_state,
2335 )?;
2336 if result.is_true() {
2337 return Ok(result);
2338 }
2339
2340 if objs_equal_by_rational_expression_evaluation(&left, &right) {
2341 return Ok(
2342 (FactualStmtSuccess::new_with_verified_by_builtin_rules_recording_stmt(
2343 EqualFact::new(left.clone(), right.clone(), line_file).into(),
2344 "calculation and rational expression simplification".to_string(),
2345 Vec::new(),
2346 ))
2347 .into(),
2348 );
2349 }
2350
2351 if objs_equal_by_rational_expression_evaluation(&calculated_left, &calculated_right) {
2352 return Ok(
2353 (FactualStmtSuccess::new_with_verified_by_builtin_rules_recording_stmt(
2354 EqualFact::new(left.clone(), right.clone(), line_file).into(),
2355 "calculation and rational expression simplification".to_string(),
2356 Vec::new(),
2357 ))
2358 .into(),
2359 );
2360 }
2361
2362 if let Some(done) = self.try_verify_anonymous_fn_application_equals_other_side(
2363 left,
2364 right,
2365 left,
2366 right,
2367 line_file.clone(),
2368 verify_state,
2369 )? {
2370 return Ok(done);
2371 }
2372 if let Some(done) = self.try_verify_anonymous_fn_application_equals_other_side(
2373 left,
2374 right,
2375 right,
2376 left,
2377 line_file.clone(),
2378 verify_state,
2379 )? {
2380 return Ok(done);
2381 }
2382
2383 if let (Obj::FnSet(left_fn_set), Obj::FnSet(right_fn_set)) = (left, right) {
2384 return self.verify_fn_set_with_params_equality_by_builtin_rules(
2385 left_fn_set,
2386 right_fn_set,
2387 line_file,
2388 verify_state,
2389 );
2390 }
2391
2392 if let (Obj::AnonymousFn(l), Obj::AnonymousFn(r)) = (left, right) {
2393 if l.to_string() == r.to_string() {
2394 return Ok(
2395 (FactualStmtSuccess::new_with_verified_by_builtin_rules_recording_stmt(
2396 EqualFact::new(left.clone(), right.clone(), line_file).into(),
2397 "anonymous fn: identical surface syntax (params, dom, ret, body)"
2398 .to_string(),
2399 Vec::new(),
2400 ))
2401 .into(),
2402 );
2403 }
2404 }
2405
2406 Ok((StmtUnknown::new()).into())
2407 }
2408}
2409
2410impl Runtime {
2411 fn try_verify_equality_pair_by_the_same_then_calculation_then_fn_obj_same_head_known_args(
2412 &mut self,
2413 left: &Obj,
2414 right: &Obj,
2415 line_file: LineFile,
2416 verify_state: &VerifyState,
2417 ) -> Result<Option<StmtResult>, RuntimeError> {
2418 let (result, _, _) = self.verify_equality_by_they_are_the_same_and_calculation(
2419 left,
2420 right,
2421 line_file.clone(),
2422 verify_state,
2423 )?;
2424 if result.is_true() {
2425 return Ok(Some(result));
2426 }
2427 if let Some(shape_result) =
2428 self.try_verify_equal_by_same_shape_and_known_equality_args(left, right, line_file)
2429 {
2430 if shape_result.is_true() {
2431 return Ok(Some(shape_result));
2432 }
2433 }
2434 Ok(None)
2435 }
2436
2437 pub fn try_verify_equality_with_known_equalities_by_builtin_rules_only(
2438 &mut self,
2439 left: &Obj,
2440 right: &Obj,
2441 line_file: LineFile,
2442 verify_state: &VerifyState,
2443 known_objs_equal_to_left: Option<&Rc<Vec<Obj>>>,
2444 known_objs_equal_to_right: Option<&Rc<Vec<Obj>>>,
2445 ) -> Result<Option<StmtResult>, RuntimeError> {
2446 match (known_objs_equal_to_left, known_objs_equal_to_right) {
2447 (None, None) => Ok(None),
2448 (Some(known_objs_equal_to_left), None) => {
2449 for obj in known_objs_equal_to_left.iter() {
2450 if let Some(result) = self
2451 .try_verify_equality_pair_by_the_same_then_calculation_then_fn_obj_same_head_known_args(
2452 obj,
2453 right,
2454 line_file.clone(),
2455 verify_state,
2456 )?
2457 {
2458 return Ok(Some(result));
2459 }
2460 }
2461 Ok(None)
2462 }
2463 (None, Some(known_objs_equal_to_right)) => {
2464 for obj in known_objs_equal_to_right.iter() {
2465 if let Some(result) = self
2466 .try_verify_equality_pair_by_the_same_then_calculation_then_fn_obj_same_head_known_args(
2467 left,
2468 obj,
2469 line_file.clone(),
2470 verify_state,
2471 )?
2472 {
2473 return Ok(Some(result));
2474 }
2475 }
2476 Ok(None)
2477 }
2478 (Some(known_objs_equal_to_left), Some(known_objs_equal_to_right)) => {
2479 for obj1 in known_objs_equal_to_left.iter() {
2480 for obj2 in known_objs_equal_to_right.iter() {
2481 if let Some(result) = self
2482 .try_verify_equality_pair_by_the_same_then_calculation_then_fn_obj_same_head_known_args(
2483 obj1,
2484 obj2,
2485 line_file.clone(),
2486 verify_state,
2487 )?
2488 {
2489 return Ok(Some(result));
2490 }
2491 }
2492 }
2493 Ok(None)
2494 }
2495 }
2496 }
2497
2498 pub fn objs_have_same_known_equality_rc_in_some_env(&self, left: &Obj, right: &Obj) -> bool {
2499 let left_key: ObjString = left.to_string();
2500 let right_key: ObjString = right.to_string();
2501 for env in self.iter_environments_from_top() {
2502 let left_entry = env.known_equality.get(&left_key);
2503 let right_entry = env.known_equality.get(&right_key);
2504 if let (Some((_, left_rc)), Some((_, right_rc))) = (left_entry, right_entry) {
2505 if Rc::ptr_eq(left_rc, right_rc) {
2506 return true;
2507 }
2508 }
2509 }
2510 false
2511 }
2512
2513 fn arg_pairs_share_known_equality_class(&self, pairs: &[(&Obj, &Obj)]) -> bool {
2514 pairs
2515 .iter()
2516 .all(|(a, b)| self.objs_have_same_known_equality_rc_in_some_env(a, b))
2517 }
2518
2519 fn boxed_obj_vecs_share_known_equality_class(
2520 &self,
2521 left: &[Box<Obj>],
2522 right: &[Box<Obj>],
2523 ) -> bool {
2524 if left.len() != right.len() {
2525 return false;
2526 }
2527 left.iter()
2528 .zip(right.iter())
2529 .all(|(a, b)| self.objs_have_same_known_equality_rc_in_some_env(a, b))
2530 }
2531
2532 pub fn try_verify_equal_by_same_shape_and_known_equality_args(
2533 &self,
2534 left: &Obj,
2535 right: &Obj,
2536 line_file: LineFile,
2537 ) -> Option<StmtResult> {
2538 let reason = "same shape and paired args share known equality class";
2539 match (left, right) {
2540 (Obj::FnObj(left_fn), Obj::FnObj(right_fn)) => {
2541 let left_head_obj = left_fn.head.as_ref().clone().into();
2542 let right_head_obj = right_fn.head.as_ref().clone().into();
2543 if !verify_equality_by_they_are_the_same(&left_head_obj, &right_head_obj) {
2544 return Some((StmtUnknown::new()).into());
2545 }
2546 if left_fn.body.len() != right_fn.body.len() {
2547 return Some((StmtUnknown::new()).into());
2548 }
2549 for (left_group, right_group) in left_fn.body.iter().zip(right_fn.body.iter()) {
2550 if !self.boxed_obj_vecs_share_known_equality_class(left_group, right_group) {
2551 return Some((StmtUnknown::new()).into());
2552 }
2553 }
2554 Some(factual_equal_success_by_builtin_reason(
2555 left, right, line_file, reason,
2556 ))
2557 }
2558 (Obj::Add(l), Obj::Add(r)) => {
2559 if self.arg_pairs_share_known_equality_class(&[
2560 (&l.left, &r.left),
2561 (&l.right, &r.right),
2562 ]) {
2563 Some(factual_equal_success_by_builtin_reason(
2564 left, right, line_file, reason,
2565 ))
2566 } else {
2567 Some((StmtUnknown::new()).into())
2568 }
2569 }
2570 (Obj::MatrixAdd(l), Obj::MatrixAdd(r)) => {
2571 if self.arg_pairs_share_known_equality_class(&[
2572 (&l.left, &r.left),
2573 (&l.right, &r.right),
2574 ]) {
2575 Some(factual_equal_success_by_builtin_reason(
2576 left, right, line_file, reason,
2577 ))
2578 } else {
2579 Some((StmtUnknown::new()).into())
2580 }
2581 }
2582 (Obj::MatrixSub(l), Obj::MatrixSub(r)) => {
2583 if self.arg_pairs_share_known_equality_class(&[
2584 (&l.left, &r.left),
2585 (&l.right, &r.right),
2586 ]) {
2587 Some(factual_equal_success_by_builtin_reason(
2588 left, right, line_file, reason,
2589 ))
2590 } else {
2591 Some((StmtUnknown::new()).into())
2592 }
2593 }
2594 (Obj::MatrixMul(l), Obj::MatrixMul(r)) => {
2595 if self.arg_pairs_share_known_equality_class(&[
2596 (&l.left, &r.left),
2597 (&l.right, &r.right),
2598 ]) {
2599 Some(factual_equal_success_by_builtin_reason(
2600 left, right, line_file, reason,
2601 ))
2602 } else {
2603 Some((StmtUnknown::new()).into())
2604 }
2605 }
2606 (Obj::MatrixScalarMul(l), Obj::MatrixScalarMul(r)) => {
2607 if self.arg_pairs_share_known_equality_class(&[
2608 (&l.scalar, &r.scalar),
2609 (&l.matrix, &r.matrix),
2610 ]) {
2611 Some(factual_equal_success_by_builtin_reason(
2612 left, right, line_file, reason,
2613 ))
2614 } else {
2615 Some((StmtUnknown::new()).into())
2616 }
2617 }
2618 (Obj::MatrixPow(l), Obj::MatrixPow(r)) => {
2619 if self.arg_pairs_share_known_equality_class(&[
2620 (&l.base, &r.base),
2621 (&l.exponent, &r.exponent),
2622 ]) {
2623 Some(factual_equal_success_by_builtin_reason(
2624 left, right, line_file, reason,
2625 ))
2626 } else {
2627 Some((StmtUnknown::new()).into())
2628 }
2629 }
2630 (Obj::Sub(l), Obj::Sub(r)) => {
2631 if self.arg_pairs_share_known_equality_class(&[
2632 (&l.left, &r.left),
2633 (&l.right, &r.right),
2634 ]) {
2635 Some(factual_equal_success_by_builtin_reason(
2636 left, right, line_file, reason,
2637 ))
2638 } else {
2639 Some((StmtUnknown::new()).into())
2640 }
2641 }
2642 (Obj::Mul(l), Obj::Mul(r)) => {
2643 if self.arg_pairs_share_known_equality_class(&[
2644 (&l.left, &r.left),
2645 (&l.right, &r.right),
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::Div(l), Obj::Div(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::Mod(l), Obj::Mod(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::Pow(l), Obj::Pow(r)) => {
2679 if self.arg_pairs_share_known_equality_class(&[
2680 (&l.base, &r.base),
2681 (&l.exponent, &r.exponent),
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::Log(l), Obj::Log(r)) => {
2691 if self
2692 .arg_pairs_share_known_equality_class(&[(&l.base, &r.base), (&l.arg, &r.arg)])
2693 {
2694 Some(factual_equal_success_by_builtin_reason(
2695 left, right, line_file, reason,
2696 ))
2697 } else {
2698 Some((StmtUnknown::new()).into())
2699 }
2700 }
2701 (Obj::Max(l), Obj::Max(r)) => {
2702 if self.arg_pairs_share_known_equality_class(&[
2703 (&l.left, &r.left),
2704 (&l.right, &r.right),
2705 ]) {
2706 Some(factual_equal_success_by_builtin_reason(
2707 left, right, line_file, reason,
2708 ))
2709 } else {
2710 Some((StmtUnknown::new()).into())
2711 }
2712 }
2713 (Obj::Min(l), Obj::Min(r)) => {
2714 if self.arg_pairs_share_known_equality_class(&[
2715 (&l.left, &r.left),
2716 (&l.right, &r.right),
2717 ]) {
2718 Some(factual_equal_success_by_builtin_reason(
2719 left, right, line_file, reason,
2720 ))
2721 } else {
2722 Some((StmtUnknown::new()).into())
2723 }
2724 }
2725 (Obj::Union(l), Obj::Union(r)) => {
2726 if self.arg_pairs_share_known_equality_class(&[
2727 (&l.left, &r.left),
2728 (&l.right, &r.right),
2729 ]) {
2730 Some(factual_equal_success_by_builtin_reason(
2731 left, right, line_file, reason,
2732 ))
2733 } else {
2734 Some((StmtUnknown::new()).into())
2735 }
2736 }
2737 (Obj::Intersect(l), Obj::Intersect(r)) => {
2738 if self.arg_pairs_share_known_equality_class(&[
2739 (&l.left, &r.left),
2740 (&l.right, &r.right),
2741 ]) {
2742 Some(factual_equal_success_by_builtin_reason(
2743 left, right, line_file, reason,
2744 ))
2745 } else {
2746 Some((StmtUnknown::new()).into())
2747 }
2748 }
2749 (Obj::SetMinus(l), Obj::SetMinus(r)) => {
2750 if self.arg_pairs_share_known_equality_class(&[
2751 (&l.left, &r.left),
2752 (&l.right, &r.right),
2753 ]) {
2754 Some(factual_equal_success_by_builtin_reason(
2755 left, right, line_file, reason,
2756 ))
2757 } else {
2758 Some((StmtUnknown::new()).into())
2759 }
2760 }
2761 (Obj::SetDiff(l), Obj::SetDiff(r)) => {
2762 if self.arg_pairs_share_known_equality_class(&[
2763 (&l.left, &r.left),
2764 (&l.right, &r.right),
2765 ]) {
2766 Some(factual_equal_success_by_builtin_reason(
2767 left, right, line_file, reason,
2768 ))
2769 } else {
2770 Some((StmtUnknown::new()).into())
2771 }
2772 }
2773 (Obj::Cup(l), Obj::Cup(r)) => {
2774 if self.objs_have_same_known_equality_rc_in_some_env(&l.left, &r.left) {
2775 Some(factual_equal_success_by_builtin_reason(
2776 left, right, line_file, reason,
2777 ))
2778 } else {
2779 Some((StmtUnknown::new()).into())
2780 }
2781 }
2782 (Obj::Cap(l), Obj::Cap(r)) => {
2783 if self.objs_have_same_known_equality_rc_in_some_env(&l.left, &r.left) {
2784 Some(factual_equal_success_by_builtin_reason(
2785 left, right, line_file, reason,
2786 ))
2787 } else {
2788 Some((StmtUnknown::new()).into())
2789 }
2790 }
2791 (Obj::PowerSet(l), Obj::PowerSet(r)) => {
2792 if self.objs_have_same_known_equality_rc_in_some_env(&l.set, &r.set) {
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::Choose(l), Obj::Choose(r)) => {
2801 if self.objs_have_same_known_equality_rc_in_some_env(&l.set, &r.set) {
2802 Some(factual_equal_success_by_builtin_reason(
2803 left, right, line_file, reason,
2804 ))
2805 } else {
2806 Some((StmtUnknown::new()).into())
2807 }
2808 }
2809 (Obj::CartDim(l), Obj::CartDim(r)) => {
2810 if self.objs_have_same_known_equality_rc_in_some_env(&l.set, &r.set) {
2811 Some(factual_equal_success_by_builtin_reason(
2812 left, right, line_file, reason,
2813 ))
2814 } else {
2815 Some((StmtUnknown::new()).into())
2816 }
2817 }
2818 (Obj::TupleDim(l), Obj::TupleDim(r)) => {
2819 if self.objs_have_same_known_equality_rc_in_some_env(&l.arg, &r.arg) {
2820 Some(factual_equal_success_by_builtin_reason(
2821 left, right, line_file, reason,
2822 ))
2823 } else {
2824 Some((StmtUnknown::new()).into())
2825 }
2826 }
2827 (Obj::Count(l), Obj::Count(r)) => {
2828 if self.objs_have_same_known_equality_rc_in_some_env(&l.set, &r.set) {
2829 Some(factual_equal_success_by_builtin_reason(
2830 left, right, line_file, reason,
2831 ))
2832 } else {
2833 Some((StmtUnknown::new()).into())
2834 }
2835 }
2836 (Obj::Range(l), Obj::Range(r)) => {
2837 if self
2838 .arg_pairs_share_known_equality_class(&[(&l.start, &r.start), (&l.end, &r.end)])
2839 {
2840 Some(factual_equal_success_by_builtin_reason(
2841 left, right, line_file, reason,
2842 ))
2843 } else {
2844 Some((StmtUnknown::new()).into())
2845 }
2846 }
2847 (Obj::Sum(l), Obj::Sum(r)) => {
2848 if self.arg_pairs_share_known_equality_class(&[
2849 (&l.start, &r.start),
2850 (&l.end, &r.end),
2851 (&l.func, &r.func),
2852 ]) {
2853 Some(factual_equal_success_by_builtin_reason(
2854 left, right, line_file, reason,
2855 ))
2856 } else {
2857 Some((StmtUnknown::new()).into())
2858 }
2859 }
2860 (Obj::Product(l), Obj::Product(r)) => {
2861 if self.arg_pairs_share_known_equality_class(&[
2862 (&l.start, &r.start),
2863 (&l.end, &r.end),
2864 (&l.func, &r.func),
2865 ]) {
2866 Some(factual_equal_success_by_builtin_reason(
2867 left, right, line_file, reason,
2868 ))
2869 } else {
2870 Some((StmtUnknown::new()).into())
2871 }
2872 }
2873 (Obj::ClosedRange(l), Obj::ClosedRange(r)) => {
2874 if self
2875 .arg_pairs_share_known_equality_class(&[(&l.start, &r.start), (&l.end, &r.end)])
2876 {
2877 Some(factual_equal_success_by_builtin_reason(
2878 left, right, line_file, reason,
2879 ))
2880 } else {
2881 Some((StmtUnknown::new()).into())
2882 }
2883 }
2884 (Obj::FiniteSeqSet(l), Obj::FiniteSeqSet(r)) => {
2885 if self.arg_pairs_share_known_equality_class(&[(&l.set, &r.set), (&l.n, &r.n)]) {
2886 Some(factual_equal_success_by_builtin_reason(
2887 left, right, line_file, reason,
2888 ))
2889 } else {
2890 Some((StmtUnknown::new()).into())
2891 }
2892 }
2893 (Obj::SeqSet(l), Obj::SeqSet(r)) => {
2894 if self.arg_pairs_share_known_equality_class(&[(&l.set, &r.set)]) {
2895 Some(factual_equal_success_by_builtin_reason(
2896 left, right, line_file, reason,
2897 ))
2898 } else {
2899 Some((StmtUnknown::new()).into())
2900 }
2901 }
2902 (Obj::MatrixSet(l), Obj::MatrixSet(r)) => {
2903 if self.arg_pairs_share_known_equality_class(&[
2904 (&l.set, &r.set),
2905 (&l.row_len, &r.row_len),
2906 (&l.col_len, &r.col_len),
2907 ]) {
2908 Some(factual_equal_success_by_builtin_reason(
2909 left, right, line_file, reason,
2910 ))
2911 } else {
2912 Some((StmtUnknown::new()).into())
2913 }
2914 }
2915 (Obj::Proj(l), Obj::Proj(r)) => {
2916 if self.arg_pairs_share_known_equality_class(&[(&l.set, &r.set), (&l.dim, &r.dim)])
2917 {
2918 Some(factual_equal_success_by_builtin_reason(
2919 left, right, line_file, reason,
2920 ))
2921 } else {
2922 Some((StmtUnknown::new()).into())
2923 }
2924 }
2925 (Obj::ObjAtIndex(l), Obj::ObjAtIndex(r)) => {
2926 if self
2927 .arg_pairs_share_known_equality_class(&[(&l.obj, &r.obj), (&l.index, &r.index)])
2928 {
2929 Some(factual_equal_success_by_builtin_reason(
2930 left, right, line_file, reason,
2931 ))
2932 } else {
2933 Some((StmtUnknown::new()).into())
2934 }
2935 }
2936 (Obj::Tuple(l), Obj::Tuple(r)) => {
2937 if self.boxed_obj_vecs_share_known_equality_class(&l.args, &r.args) {
2938 Some(factual_equal_success_by_builtin_reason(
2939 left, right, line_file, reason,
2940 ))
2941 } else {
2942 Some((StmtUnknown::new()).into())
2943 }
2944 }
2945 (Obj::ListSet(l), Obj::ListSet(r)) => {
2946 if self.boxed_obj_vecs_share_known_equality_class(&l.list, &r.list) {
2947 Some(factual_equal_success_by_builtin_reason(
2948 left, right, line_file, reason,
2949 ))
2950 } else {
2951 Some((StmtUnknown::new()).into())
2952 }
2953 }
2954 (Obj::Cart(l), Obj::Cart(r)) => {
2955 if self.boxed_obj_vecs_share_known_equality_class(&l.args, &r.args) {
2956 Some(factual_equal_success_by_builtin_reason(
2957 left, right, line_file, reason,
2958 ))
2959 } else {
2960 Some((StmtUnknown::new()).into())
2961 }
2962 }
2963 _ => None,
2964 }
2965 }
2966
2967 pub fn verify_equality_by_they_are_the_same_and_calculation(
2968 &mut self,
2969 left: &Obj,
2970 right: &Obj,
2971 line_file: LineFile,
2972 _verify_state: &VerifyState,
2973 ) -> Result<(StmtResult, Obj, Obj), RuntimeError> {
2974 if verify_equality_by_they_are_the_same(left, right) {
2975 return Ok((
2976 factual_equal_success_by_builtin_reason(
2977 left,
2978 right,
2979 line_file,
2980 "they are the same",
2981 ),
2982 left.clone(),
2983 right.clone(),
2984 ));
2985 }
2986
2987 let left_resolved = self.resolve_obj(left);
2988 let right_resolved = self.resolve_obj(right);
2989
2990 if left_resolved.two_objs_can_be_calculated_and_equal_by_calculation(&right_resolved) {
2991 return Ok((
2992 factual_equal_success_by_builtin_reason(left, right, line_file, "calculation"),
2993 left_resolved,
2994 right_resolved,
2995 ));
2996 }
2997
2998 Ok((
2999 StmtResult::StmtUnknown(StmtUnknown::new()),
3000 left_resolved,
3001 right_resolved,
3002 ))
3003 }
3004}