use crate::prelude::*;
use crate::verify::verify_number_in_standard_set::is_integer_after_simplification;
impl Runtime {
pub fn _verify_not_equal_fact_with_builtin_rules(
&mut self,
not_equal_fact: &NotEqualFact,
verify_state: &VerifyState,
) -> Result<StmtResult, RuntimeError> {
let left_obj = ¬_equal_fact.left;
let right_obj = ¬_equal_fact.right;
match (
self.resolve_obj_to_number_for_not_equal_builtin_rule(left_obj),
self.resolve_obj_to_number_for_not_equal_builtin_rule(right_obj),
) {
(Some(left_number), Some(right_number)) => {
if left_number.normalized_value != right_number.normalized_value {
return Ok(
(FactualStmtSuccess::new_with_verified_by_builtin_rules_recording_stmt(
not_equal_fact.clone().into(),
"not_equal_numeric_resolved_or_equal_class_calculation".to_string(),
Vec::new(),
))
.into(),
);
}
}
_ => {}
}
if let (Obj::ListSet(left_ls), Obj::ListSet(right_ls)) = (left_obj, right_obj) {
if left_ls.list.len() != right_ls.list.len() {
return Ok(
(FactualStmtSuccess::new_with_verified_by_builtin_rules_recording_stmt(
not_equal_fact.clone().into(),
"list_set_different_length".to_string(),
Vec::new(),
))
.into(),
);
}
}
if let Some(verified_result) =
self.try_verify_not_equal_empty_set_from_nonempty(not_equal_fact)?
{
return Ok(verified_result);
}
if let Some(verified_result) =
self.try_verify_not_equal_from_known_strict_order(not_equal_fact)?
{
return Ok(verified_result);
}
if let Some(verified_result) =
self.try_verify_not_equal_zero_from_n_and_one_le(not_equal_fact, verify_state)?
{
return Ok(verified_result);
}
if let Some(verified_result) =
self.try_verify_not_equal_pow_from_base_nonzero(not_equal_fact, verify_state)?
{
return Ok(verified_result);
}
if let Some(verified_result) = self
.try_verify_square_sum_not_equal_zero_from_nonzero_component(
not_equal_fact,
verify_state,
)?
{
return Ok(verified_result);
}
match self
.try_verify_not_equal_fact_when_zero_and_binary_arithmetic_reduces_by_operand_facts(
not_equal_fact,
verify_state,
)? {
Some(verified_result) => return Ok(verified_result),
None => {}
}
Ok((StmtUnknown::new()).into())
}
}
impl Runtime {
fn try_parse_number_literal_obj_string_for_not_equal_builtin_rule(
&self,
obj_string: &str,
) -> Option<Number> {
let trimmed = obj_string.trim();
if trimmed.is_empty() {
return None;
}
let parsed = Number::new(trimmed.to_string());
if parsed.to_string() == trimmed {
return Some(parsed);
}
None
}
fn resolve_obj_to_number_for_not_equal_builtin_rule(&self, obj: &Obj) -> Option<Number> {
if let Some(number) = self.resolve_obj_to_number_resolved(obj) {
return Some(number);
}
let obj_key = obj.to_string();
if let Some(number) = self.get_object_equal_to_normalized_decimal_number(&obj_key) {
return Some(number);
}
let all_equal_obj_strings = self.get_all_objs_equal_to_given(&obj_key);
for equal_obj_string in all_equal_obj_strings {
if let Some(number) =
self.get_object_equal_to_normalized_decimal_number(&equal_obj_string)
{
return Some(number);
}
if let Some(number) = self
.try_parse_number_literal_obj_string_for_not_equal_builtin_rule(&equal_obj_string)
{
return Some(number);
}
}
None
}
fn try_verify_not_equal_empty_set_from_nonempty(
&mut self,
not_equal_fact: &NotEqualFact,
) -> Result<Option<StmtResult>, RuntimeError> {
let line_file = not_equal_fact.line_file.clone();
let set = match (¬_equal_fact.left, ¬_equal_fact.right) {
(Obj::ListSet(list), set) if list.list.is_empty() => set.clone(),
(set, Obj::ListSet(list)) if list.list.is_empty() => set.clone(),
_ => return Ok(None),
};
let nonempty: AtomicFact = IsNonemptySetFact::new(set, line_file).into();
let sub = self.verify_non_equational_known_then_builtin_rules_only(
&nonempty,
&VerifyState::new(0, true),
)?;
if !sub.is_true() {
return Ok(None);
}
Ok(Some(
FactualStmtSuccess::new_with_verified_by_builtin_rules_label_and_steps(
not_equal_fact.clone().into(),
InferResult::new(),
"not_equal_empty_set_from_nonempty".to_string(),
vec![sub],
)
.into(),
))
}
fn try_verify_not_equal_from_known_strict_order(
&mut self,
not_equal_fact: &NotEqualFact,
) -> Result<Option<StmtResult>, RuntimeError> {
let line_file = not_equal_fact.line_file.clone();
let x = not_equal_fact.left.clone();
let y = not_equal_fact.right.clone();
let candidates: [AtomicFact; 4] = [
LessFact::new(x.clone(), y.clone(), line_file.clone()).into(),
GreaterFact::new(x.clone(), y.clone(), line_file.clone()).into(),
LessFact::new(y.clone(), x.clone(), line_file.clone()).into(),
GreaterFact::new(y.clone(), x.clone(), line_file.clone()).into(),
];
for order_atomic in candidates {
let sub =
self.verify_non_equational_atomic_fact_with_known_atomic_facts(&order_atomic)?;
if sub.is_true() {
return Ok(Some(
FactualStmtSuccess::new_with_verified_by_builtin_rules_label_and_steps(
not_equal_fact.clone().into(),
InferResult::new(),
"not_equal_from_known_strict_order".to_string(),
vec![sub],
)
.into(),
));
}
}
Ok(None)
}
fn try_verify_not_equal_zero_from_n_and_one_le(
&mut self,
not_equal_fact: &NotEqualFact,
verify_state: &VerifyState,
) -> Result<Option<StmtResult>, RuntimeError> {
let line_file = not_equal_fact.line_file.clone();
let one_obj: Obj = Number::new("1".to_string()).into();
let x = match (¬_equal_fact.left, ¬_equal_fact.right) {
(l, r) if self.obj_represents_zero_for_not_equal_builtin_rules(r) => l.clone(),
(l, r) if self.obj_represents_zero_for_not_equal_builtin_rules(l) => r.clone(),
_ => return Ok(None),
};
let in_n: AtomicFact =
InFact::new(x.clone(), StandardSet::N.into(), line_file.clone()).into();
if !self
.verify_non_equational_known_then_builtin_rules_only(&in_n, verify_state)?
.is_true()
{
return Ok(None);
}
let ge: AtomicFact =
GreaterEqualFact::new(x.clone(), one_obj.clone(), line_file.clone()).into();
if self
.verify_non_equational_atomic_fact_with_known_atomic_facts(&ge)?
.is_true()
{
return Ok(Some(
FactualStmtSuccess::new_with_verified_by_builtin_rules_recording_stmt(
not_equal_fact.clone().into(),
"n != 0 from n $in N and 1 <= n".to_string(),
Vec::new(),
)
.into(),
));
}
let one_le: AtomicFact = LessEqualFact::new(one_obj, x, line_file.clone()).into();
if self
.verify_non_equational_atomic_fact_with_known_atomic_facts(&one_le)?
.is_true()
{
return Ok(Some(
FactualStmtSuccess::new_with_verified_by_builtin_rules_recording_stmt(
not_equal_fact.clone().into(),
"n != 0 from n $in N and 1 <= n".to_string(),
Vec::new(),
)
.into(),
));
}
Ok(None)
}
fn try_verify_not_equal_pow_from_base_nonzero(
&mut self,
not_equal_fact: &NotEqualFact,
verify_state: &VerifyState,
) -> Result<Option<StmtResult>, RuntimeError> {
let line_file = not_equal_fact.line_file.clone();
let zero_obj: Obj = Number::new("0".to_string()).into();
let pow = match (¬_equal_fact.left, ¬_equal_fact.right) {
(Obj::Pow(p), r) if self.obj_represents_zero_for_not_equal_builtin_rules(r) => p,
(l, Obj::Pow(p)) if self.obj_represents_zero_for_not_equal_builtin_rules(l) => p,
_ => return Ok(None),
};
let Obj::Number(exp_num) = pow.exponent.as_ref() else {
return Ok(None);
};
if !is_integer_after_simplification(exp_num) {
return Ok(None);
}
let base = pow.base.as_ref().clone();
let base_neq_zero: AtomicFact = NotEqualFact::new(base, zero_obj, line_file.clone()).into();
let mut result =
self.verify_non_equational_atomic_fact_with_known_atomic_facts(&base_neq_zero)?;
if !result.is_true() {
result = self.verify_non_equational_atomic_fact(&base_neq_zero, verify_state, true)?;
}
if result.is_true() {
return Ok(Some(
FactualStmtSuccess::new_with_verified_by_builtin_rules_label_and_steps(
not_equal_fact.clone().into(),
InferResult::new(),
"not_equal_pow_from_base_nonzero".to_string(),
vec![result],
)
.into(),
));
}
Ok(None)
}
fn try_verify_square_sum_not_equal_zero_from_nonzero_component(
&mut self,
not_equal_fact: &NotEqualFact,
verify_state: &VerifyState,
) -> Result<Option<StmtResult>, RuntimeError> {
let line_file = not_equal_fact.line_file.clone();
let expression_obj =
if self.obj_represents_zero_for_not_equal_builtin_rules(¬_equal_fact.right) {
¬_equal_fact.left
} else if self.obj_represents_zero_for_not_equal_builtin_rules(¬_equal_fact.left) {
¬_equal_fact.right
} else {
return Ok(None);
};
let Some((left_base, right_base)) =
self.square_sum_bases_for_not_equal_zero(expression_obj)
else {
return Ok(None);
};
let zero_obj: Obj = Number::new("0".to_string()).into();
let left_nonzero: AtomicFact =
NotEqualFact::new(left_base.clone(), zero_obj.clone(), line_file.clone()).into();
let right_nonzero: AtomicFact =
NotEqualFact::new(right_base.clone(), zero_obj, line_file.clone()).into();
let known_or = OrFact::new(
vec![
AndChainAtomicFact::AtomicFact(left_nonzero.clone()),
AndChainAtomicFact::AtomicFact(right_nonzero.clone()),
],
line_file.clone(),
);
let mut steps = Vec::new();
let known_or_result = self.verify_or_fact(&known_or, verify_state)?;
if known_or_result.is_true() {
steps.push(known_or_result);
return Ok(Some(
FactualStmtSuccess::new_with_verified_by_builtin_rules_label_and_steps(
not_equal_fact.clone().into(),
InferResult::new(),
"square_sum_not_equal_zero_from_nonzero_component_or".to_string(),
steps,
)
.into(),
));
}
let left_result =
self.verify_non_equational_atomic_fact(&left_nonzero, verify_state, true)?;
if left_result.is_true() {
steps.push(left_result);
return Ok(Some(
FactualStmtSuccess::new_with_verified_by_builtin_rules_label_and_steps(
not_equal_fact.clone().into(),
InferResult::new(),
"square_sum_not_equal_zero_from_left_nonzero".to_string(),
steps,
)
.into(),
));
}
let right_result =
self.verify_non_equational_atomic_fact(&right_nonzero, verify_state, true)?;
if right_result.is_true() {
steps.push(right_result);
return Ok(Some(
FactualStmtSuccess::new_with_verified_by_builtin_rules_label_and_steps(
not_equal_fact.clone().into(),
InferResult::new(),
"square_sum_not_equal_zero_from_right_nonzero".to_string(),
steps,
)
.into(),
));
}
Ok(None)
}
fn square_sum_bases_for_not_equal_zero(&self, obj: &Obj) -> Option<(Obj, Obj)> {
let Obj::Add(add) = obj else {
return None;
};
let left_base = self.square_base_for_not_equal_zero(add.left.as_ref())?;
let right_base = self.square_base_for_not_equal_zero(add.right.as_ref())?;
Some((left_base, right_base))
}
fn square_base_for_not_equal_zero(&self, obj: &Obj) -> Option<Obj> {
match obj {
Obj::Pow(pow) => {
let Obj::Number(exp_number) = pow.exponent.as_ref() else {
return None;
};
if exp_number.to_string() == "2" {
Some(pow.base.as_ref().clone())
} else {
None
}
}
Obj::Mul(mul) if mul.left.as_ref().to_string() == mul.right.as_ref().to_string() => {
Some(mul.left.as_ref().clone())
}
_ => None,
}
}
fn obj_represents_zero_for_not_equal_builtin_rules(self: &Self, obj: &Obj) -> bool {
match self.resolve_obj_to_number(obj) {
Some(number) => number.normalized_value == "0",
None => false,
}
}
fn operand_is_not_equal_to_zero_by_known_non_equational_facts(
&mut self,
operand: &Obj,
line_file: LineFile,
) -> Result<bool, RuntimeError> {
let zero_obj: Obj = Number::new("0".to_string()).into();
let operand_not_equal_zero_fact =
NotEqualFact::new(operand.clone(), zero_obj, line_file).into();
let verify_result = self.verify_non_equational_atomic_fact_with_known_atomic_facts(
&operand_not_equal_zero_fact,
)?;
Ok(verify_result.is_true())
}
fn both_operands_nonzero_by_known_non_equational_facts(
&mut self,
left_operand: &Obj,
right_operand: &Obj,
line_file: LineFile,
) -> Result<bool, RuntimeError> {
let left_nonzero = self.operand_is_not_equal_to_zero_by_known_non_equational_facts(
left_operand,
line_file.clone(),
)?;
if !left_nonzero {
return Ok(false);
}
self.operand_is_not_equal_to_zero_by_known_non_equational_facts(right_operand, line_file)
}
fn both_operands_strictly_positive_by_non_equational_verify(
&mut self,
left_operand: &Obj,
right_operand: &Obj,
line_file: LineFile,
verify_state: &VerifyState,
) -> Result<bool, RuntimeError> {
let zero_obj: Obj = Number::new("0".to_string()).into();
let zero_less_than_left =
LessFact::new(zero_obj.clone(), left_operand.clone(), line_file.clone()).into();
if !self.non_equational_atomic_fact_holds_by_full_verify_pipeline(
&zero_less_than_left,
verify_state,
)? {
return Ok(false);
}
let zero_less_than_right = LessFact::new(zero_obj, right_operand.clone(), line_file).into();
self.non_equational_atomic_fact_holds_by_full_verify_pipeline(
&zero_less_than_right,
verify_state,
)
}
fn both_operands_strictly_negative_by_non_equational_verify(
&mut self,
left_operand: &Obj,
right_operand: &Obj,
line_file: LineFile,
verify_state: &VerifyState,
) -> Result<bool, RuntimeError> {
let zero_obj: Obj = Number::new("0".to_string()).into();
let left_less_than_zero =
LessFact::new(left_operand.clone(), zero_obj.clone(), line_file.clone()).into();
if !self.non_equational_atomic_fact_holds_by_full_verify_pipeline(
&left_less_than_zero,
verify_state,
)? {
return Ok(false);
}
let right_less_than_zero = LessFact::new(right_operand.clone(), zero_obj, line_file).into();
self.non_equational_atomic_fact_holds_by_full_verify_pipeline(
&right_less_than_zero,
verify_state,
)
}
pub fn mul_product_negative_when_factors_have_strict_opposite_sign_by_non_equational_verify(
&mut self,
left_factor: &Obj,
right_factor: &Obj,
line_file: LineFile,
verify_state: &VerifyState,
) -> Result<bool, RuntimeError> {
let zero_obj: Obj = Number::new("0".to_string()).into();
let left_less_than_zero =
LessFact::new(left_factor.clone(), zero_obj.clone(), line_file.clone()).into();
let zero_less_than_right =
LessFact::new(zero_obj.clone(), right_factor.clone(), line_file.clone()).into();
if self.non_equational_atomic_fact_holds_by_full_verify_pipeline(
&left_less_than_zero,
verify_state,
)? && self.non_equational_atomic_fact_holds_by_full_verify_pipeline(
&zero_less_than_right,
verify_state,
)? {
return Ok(true);
}
let zero_less_than_left =
LessFact::new(zero_obj.clone(), left_factor.clone(), line_file.clone()).into();
let right_less_than_zero = LessFact::new(right_factor.clone(), zero_obj, line_file).into();
Ok(
self.non_equational_atomic_fact_holds_by_full_verify_pipeline(
&zero_less_than_left,
verify_state,
)? && self.non_equational_atomic_fact_holds_by_full_verify_pipeline(
&right_less_than_zero,
verify_state,
)?,
)
}
fn sub_difference_nonzero_when_operands_have_strict_opposite_sign_by_non_equational_verify(
&mut self,
minuend: &Obj,
subtrahend: &Obj,
line_file: LineFile,
verify_state: &VerifyState,
) -> Result<bool, RuntimeError> {
let zero_obj: Obj = Number::new("0".to_string()).into();
let zero_less_than_minuend =
LessFact::new(zero_obj.clone(), minuend.clone(), line_file.clone()).into();
let subtrahend_less_than_zero =
LessFact::new(subtrahend.clone(), zero_obj.clone(), line_file.clone()).into();
if self.non_equational_atomic_fact_holds_by_full_verify_pipeline(
&zero_less_than_minuend,
verify_state,
)? && self.non_equational_atomic_fact_holds_by_full_verify_pipeline(
&subtrahend_less_than_zero,
verify_state,
)? {
return Ok(true);
}
let minuend_less_than_zero =
LessFact::new(minuend.clone(), zero_obj.clone(), line_file.clone()).into();
let zero_less_than_subtrahend =
LessFact::new(zero_obj, subtrahend.clone(), line_file).into();
Ok(
self.non_equational_atomic_fact_holds_by_full_verify_pipeline(
&minuend_less_than_zero,
verify_state,
)? && self.non_equational_atomic_fact_holds_by_full_verify_pipeline(
&zero_less_than_subtrahend,
verify_state,
)?,
)
}
fn try_verify_not_equal_fact_when_zero_and_binary_arithmetic_reduces_by_operand_facts(
&mut self,
not_equal_fact: &NotEqualFact,
verify_state: &VerifyState,
) -> Result<Option<StmtResult>, RuntimeError> {
let line_file = not_equal_fact.line_file.clone();
let expression_obj =
if self.obj_represents_zero_for_not_equal_builtin_rules(¬_equal_fact.right) {
¬_equal_fact.left
} else if self.obj_represents_zero_for_not_equal_builtin_rules(¬_equal_fact.left) {
¬_equal_fact.right
} else {
return Ok(None);
};
let builtin_rule_label = match expression_obj {
Obj::Add(add) => {
if self.both_operands_strictly_positive_by_non_equational_verify(
&add.left,
&add.right,
line_file.clone(),
verify_state,
)? {
Some("add_not_equal_zero_both_operands_strictly_positive")
} else if self.both_operands_strictly_negative_by_non_equational_verify(
&add.left,
&add.right,
line_file.clone(),
verify_state,
)? {
Some("add_not_equal_zero_both_operands_strictly_negative")
} else {
None
}
}
Obj::Mul(mul) => {
if self.both_operands_nonzero_by_known_non_equational_facts(
&mul.left,
&mul.right,
line_file.clone(),
)? {
Some("mul_not_equal_zero_both_factors_nonzero_by_known_facts")
} else if self.both_operands_strictly_positive_by_non_equational_verify(
&mul.left,
&mul.right,
line_file.clone(),
verify_state,
)? {
Some("mul_not_equal_zero_both_factors_strictly_positive")
} else if self.both_operands_strictly_negative_by_non_equational_verify(
&mul.left,
&mul.right,
line_file.clone(),
verify_state,
)? {
Some("mul_not_equal_zero_both_factors_strictly_negative")
} else {
None
}
}
Obj::Sub(sub) => {
if self.sub_difference_nonzero_when_operands_have_strict_opposite_sign_by_non_equational_verify(
&sub.left,
&sub.right,
line_file,
verify_state,
)? {
Some("sub_not_equal_zero_operands_strict_opposite_sign")
} else {
None
}
}
other => {
let zero_obj: Obj = Number::new("0".to_string()).into();
let zero_lt_a = LessFact::new(
zero_obj.clone(),
other.clone(),
line_file.clone(),
).into();
let final_round_verify_state = verify_state.make_final_round_state();
if self.non_equational_atomic_fact_holds_by_full_verify_pipeline(
&zero_lt_a,
&final_round_verify_state,
)? {
Some("not_equal_zero_operand_strictly_positive")
} else {
let a_lt_0 = LessFact::new(
other.clone(),
zero_obj,
line_file.clone(),
).into();
if self.non_equational_atomic_fact_holds_by_full_verify_pipeline(
&a_lt_0,
&final_round_verify_state,
)? {
Some("not_equal_zero_operand_strictly_negative")
} else {
None
}
}
}
};
match builtin_rule_label {
Some(rule_label) => Ok(Some(
(FactualStmtSuccess::new_with_verified_by_builtin_rules_recording_stmt(
not_equal_fact.clone().into(),
rule_label.to_string(),
Vec::new(),
))
.into(),
)),
None => Ok(None),
}
}
}