Skip to content

Commit

Permalink
!120 prove inequalities
Browse files Browse the repository at this point in the history 
Merge pull request !120 from fyh/master
  • Loading branch information
@bzhan @gitee-org
bzhan authored and gitee-org committed Feb 24, 2023
2 parents 2a77b57 + 19455a4 commit f5edc03
Show file tree
Hide file tree
Showing 13 changed files with 594 additions and 55 deletions.
61 changes: 50 additions & 11 deletions integral/compstate.py
View file
Original file line number Diff line number Diff line change
Expand Up @@ -122,10 +122,13 @@ def export(self):
return res

def export_book(self):
p = self.parent
while (not isinstance(p, CompFile)):
p = p.parent
res = {
"type": "definition",
"expr": str(self.eq),
"path": self.parent.name
"path": p.name
}
if self.conds.data:
res["conds"] = [str(cond) for cond in self.conds.data]
Expand All @@ -149,10 +152,12 @@ def __init__(self, parent, ctx: Context, goal: Expr, conds: Optional[Conditions]
conds = Conditions()
self.conds = conds
self.proof = None

self.ctx = Context(ctx)
self.ctx.extend_condition(self.conds)
self.wellformed, self.bad_parts = check_wellformed(goal, self.ctx.get_conds())
self.sub_goals:List['Goal'] = list()
for p in self.bad_parts:
self.sub_goals.append(Goal(self, self.ctx, p, conds))

def __str__(self):
if self.is_finished():
Expand All @@ -168,7 +173,11 @@ def __eq__(self, other):
self.proof == other.proof

def is_finished(self):
return self.proof is not None and self.proof.is_finished()
if self.sub_goals == list():
return self.proof is not None and self.proof.is_finished()
else:
self.wellformed = all(g.is_finished() for g in self.sub_goals)
return self.proof is not None and self.proof.is_finished() and self.wellformed

def clear(self):
self.proof = None
Expand All @@ -180,6 +189,8 @@ def export(self):
"latex_goal": latex.convert_expr(self.goal),
"finished": self.is_finished(),
}
if self.sub_goals != list():
res['sub_goals'] = [g.export() for g in self.sub_goals]
if self.proof:
res['proof'] = self.proof.export()
if self.conds.data:
Expand All @@ -190,10 +201,13 @@ def export(self):
return res

def export_book(self):
p = self.parent
while(not isinstance(p, CompFile)):
p = p.parent
res = {
"type": "problem",
"expr": str(self.goal),
"path": self.parent.name
"path": p.name
}
if self.conds.data:
res["conds"] = [str(cond) for cond in self.conds.data]
Expand Down Expand Up @@ -348,15 +362,15 @@ class CalculationProof(StateItem):
"""
def __init__(self, parent, goal: Expr):
if not goal.is_equals():
raise AssertionError("CalculationProof: goal is not an equality.")
# if not goal.is_equals():
# raise AssertionError("CalculationProof: goal is not an equality.")

self.parent = parent
self.goal = goal
self.ctx = parent.ctx

self.lhs_calc = Calculation(self, self.ctx, self.goal.lhs)
self.rhs_calc = Calculation(self, self.ctx, self.goal.rhs)
self.predicate = goal.op
self.lhs_calc = Calculation(self, self.ctx, self.goal.args[0])
self.rhs_calc = Calculation(self, self.ctx, self.goal.args[1])

def __str__(self):
if self.is_finished():
Expand All @@ -372,7 +386,19 @@ def __str__(self):
return res

def is_finished(self):
return self.lhs_calc.last_expr == self.rhs_calc.last_expr
if self.predicate == '=':
return self.lhs_calc.last_expr == self.rhs_calc.last_expr
elif self.predicate == '>':
return self.ctx.get_conds().is_greater(self.lhs_calc.last_expr,self.rhs_calc.last_expr)
elif self.predicate == '<':
return self.ctx.get_conds().is_less(self.lhs_calc.last_expr, self.rhs_calc.last_expr)
elif self.predicate == '<=':
return self.ctx.get_conds().is_not_greater(self.lhs_calc.last_expr, self.rhs_calc.last_expr)
elif self.predicate == '>=':
return self.ctx.get_conds().is_not_less(self.lhs_calc.last_expr, self.rhs_calc.last_expr)
elif self.predicate == '!=':
return self.ctx.get_conds().is_not_equal(self.lhs_calc.last_expr, self.rhs_calc.last_expr)
raise NotImplementedError

def export(self):
return {
Expand Down Expand Up @@ -657,14 +683,17 @@ def add_calculation(self, calc: Union[str, Expr]) -> Calculation:
raise NotImplementedError
return self.content[-1]

def add_goal(self, goal: Union[str, Expr], *, conds: List[Union[str, Expr]] = None) -> Goal:
def add_goal(self, goal: Union[str, Expr, Goal], *, conds: List[Union[str, Expr]] = None) -> Goal:
"""Add a goal.
goal: statement of the goal.
conds: list of conditions for the goal. This is ignored if input goal
is already of type Goal.
"""
if isinstance(goal, Goal):
self.content.append(goal)
return self.content[-1]
if conds is not None:
for i in range(len(conds)):
if isinstance(conds[i], str):
Expand Down Expand Up @@ -823,6 +852,16 @@ def parse_item(parent, item) -> StateItem:
res = Goal(parent, ctx, goal, conds=conds)
if 'proof' in item:
res.proof = parse_item(res, item['proof'])
if 'wellformed' in item:
res.wellformed = item['wellformed']
if not res.wellformed and 'bad_parts' in item:
res.bad_parts = set()
for bad_e in item['bad_parts']:
res.bad_parts.add(parser.parse_expr(bad_e))
if 'sub_goals' in item:
res.sub_goals = list()
for g in item['sub_goals']:
res.sub_goals.append(parse_item(res, g))
return res
elif item['type'] == 'CalculationProof':
goal = parser.parse_expr(item['goal'])
Expand Down
35 changes: 34 additions & 1 deletion integral/conditions.py
View file
Original file line number Diff line number Diff line change
Expand Up @@ -66,18 +66,25 @@ def check_condition(self, cond: Expr) -> bool:
def is_positive(self, e: Expr) -> bool:
"""Return whether conditions imply e is positive."""
if e.is_op():
if e.op in ['+', '*', '/']:
if e.op in ['*', '/']:
if all(self.is_positive(arg) for arg in e.args):
return True
elif e.op == '+':
if all(self.is_not_negative(arg) for arg in e.args) and any(self.is_positive(arg) for arg in e.args):
return True
elif e.op == '^':
if e.args[1].is_evaluable():
tmp = expr.eval_expr(e.args[1])
if self.is_nonzero(e.args[0]) and tmp == int(tmp) and tmp % 2 == 0:
return True
elif self.is_positive(e.args[0]):
return True
elif e.is_fun():
if e.func_name == 'abs':
if self.is_nonzero(e.args[0]):
return True
elif e.func_name == 'cosh':
return True
interval = self.get_bounds_for_expr(e)
if interval is None:
return False
Expand All @@ -86,6 +93,17 @@ def is_positive(self, e: Expr) -> bool:

def is_not_negative(self, e: Expr) -> bool:
"""Return whether conditions imply e is not negative."""
if self.is_positive(e):
return True
if e.is_op():
if e.op in ['+', '*']:
if all(self.is_not_negative(arg) for arg in e.args):
return True
elif e.op == '^':
if e.args[1].is_evaluable():
tmp = expr.eval_expr(e.args[1])
if tmp == int(tmp) and tmp > 0 and tmp % 2 == 0:
return True
interval = self.get_bounds_for_expr(e)
if interval is None:
return False
Expand Down Expand Up @@ -141,3 +159,18 @@ def is_nonzero(self, e: Expr) -> bool:
if self.is_negative(e):
return True
return False

def is_greater(self, e1: Expr, e2: Expr) -> bool:
return self.is_positive(e1 - e2)

def is_less(self, e1: Expr, e2:Expr) -> bool:
return self.is_negative(e1 - e2)

def is_not_less(self, e1:Expr, e2:Expr):
return self.is_not_negative(e1 - e2)

def is_not_greater(self, e1:Expr, e2:Expr):
return self.is_not_positive(e1 - e2)

def is_not_equal(self, e1: Expr, e2: Expr):
return self.is_nonzero(e1 - e2)
9 changes: 5 additions & 4 deletions integral/context.py
View file
Original file line number Diff line number Diff line change
Expand Up @@ -249,10 +249,11 @@ def add_lemma(self, eq: Union[Expr, str]):
if isinstance(eq, str):
eq = parser.parse_expr(eq)
if not eq.is_equals():
raise TypeError

# Note: no conversion to symbols for lemmas within a file.
self.lemmas.append(Identity(eq.lhs, eq.rhs))
# raise TypeError
pass
else:
# Note: no conversion to symbols for lemmas within a file.
self.lemmas.append(Identity(eq.lhs, eq.rhs))

def add_induct_hyp(self, eq: Expr):
if not eq.is_equals():
Expand Down
102 changes: 97 additions & 5 deletions integral/examples/chapter2_practice01.json
View file
Original file line number Diff line number Diff line change
Expand Up @@ -179,9 +179,6 @@
"type": "Goal"
},
{
"bad_parts": [
"4 * x - x ^ 2 > 0"
],
"conds": [
{
"cond": "x > 0",
Expand Down Expand Up @@ -338,8 +335,103 @@
},
"type": "CalculationProof"
},
"type": "Goal",
"wellformed": false
"sub_goals": [
{
"conds": [
{
"cond": "x > 0",
"latex_cond": "x > 0"
},
{
"cond": "x < 4",
"latex_cond": "x < 4"
}
],
"finished": true,
"goal": "4 * x - x ^ 2 > 0",
"latex_goal": "4 x - x ^ {2} > 0",
"proof": {
"finished": true,
"goal": "4 * x - x ^ 2 > 0",
"latex_goal": "4 x - x ^ {2} > 0",
"lhs_calc": {
"latex_start": "4 x - x ^ {2}",
"start": "4 * x - x ^ 2",
"steps": [
{
"latex_res": "x (4 - x)",
"res": "x * (4 - x)",
"rule": {
"latex_str": "rewriting \\(4 x - x ^ {2}\\) to \\(x (4 - x)\\)",
"name": "Equation",
"new_expr": "x * (4 - x)",
"old_expr": "4 * x - x ^ 2",
"str": "rewriting 4 * x - x ^ 2 to x * (4 - x)"
},
"type": "CalculationStep"
}
],
"type": "Calculation"
},
"rhs_calc": {
"latex_start": "0",
"start": "0",
"steps": [],
"type": "Calculation"
},
"type": "CalculationProof"
},
"type": "Goal"
}
],
"type": "Goal"
},
{
"conds": [
{
"cond": "x > 0",
"latex_cond": "x > 0"
},
{
"cond": "x < 4",
"latex_cond": "x < 4"
}
],
"finished": true,
"goal": "4 * x - x ^ 2 > 0",
"latex_goal": "4 x - x ^ {2} > 0",
"proof": {
"finished": true,
"goal": "4 * x - x ^ 2 > 0",
"latex_goal": "4 x - x ^ {2} > 0",
"lhs_calc": {
"latex_start": "4 x - x ^ {2}",
"start": "4 * x - x ^ 2",
"steps": [
{
"latex_res": "x (4 - x)",
"res": "x * (4 - x)",
"rule": {
"latex_str": "rewriting \\(4 x - x ^ {2}\\) to \\(x (4 - x)\\)",
"name": "Equation",
"new_expr": "x * (4 - x)",
"old_expr": "4 * x - x ^ 2",
"str": "rewriting 4 * x - x ^ 2 to x * (4 - x)"
},
"type": "CalculationStep"
}
],
"type": "Calculation"
},
"rhs_calc": {
"latex_start": "0",
"start": "0",
"steps": [],
"type": "Calculation"
},
"type": "CalculationProof"
},
"type": "Goal"
}
],
"name": "chapter2_practice01"
Expand Down
Loading

0 comments on commit f5edc03

Please sign in to comment.