Better way to preserve the lhs for @auto_prover_..'s

Implemented Issue #291 to specifically preserve the lhs (rather
than the lhs expression in a blanket way) for @auto_prover_..'s
(see Issue #308).

packages/proveit/_core_/expression/expr.py

@@ -1636,6 +1636,10 @@ def _update_marked_expr(self, markers_and_marked_expr,
             return None
         try:
             markers, marked_expr = markers_and_marked_expr
+            if marked_expr in markers:
+                # This entire sub-expression is marked, so we
+                # all simplifications are fair game here.
+                return None
             marked_expr = sub_expr_fn(marked_expr)
             assert isinstance(marked_expr, Expression)
             return (markers, marked_expr)

packages/proveit/decorators.py

@@ -34,6 +34,7 @@ def decorated_prover(*args, **kwargs):
             raise ValueError(
                     "Adding 'replacements' and setting 'preserve_all' "
                     "to True are incompatible settings.")
+        preserve_lhs = kwargs.pop('preserve_lhs', False)
         preserve_expr = kwargs.pop('preserve_expr', None)
         if len(args) > 0:
             _self = args[0]
@@ -169,8 +170,24 @@ def checked_truth(proven_truth):
                 # Effect the replacements and/or auto-simplification by
                 # regenerating the proof object under the active defaults.
                 orig_proven_truth = proven_truth
+                if preserve_lhs:
+                    from proveit import safe_dummy_var
+                    from proveit.relation import Relation
+                    _expr = proven_truth.expr
+                    if not isinstance(_expr, Relation):
+                        raise TypeError(
+                            "@relation_proven, %s, expected to prove a"
+                            "Relation expression but got %s"%(func, _expr))
+                    simplify_only_where_marked = True
+                    dummy_var = safe_dummy_var(_expr)
+                    markers_and_marked_expr = (
+                        (dummy_var,), type(_expr)(_expr.lhs, dummy_var))
+                else:
+                    simplify_only_where_marked = False
+                    marker_and_Marked_expr = None
                 new_proven_truth = (
-                    proven_truth.proof().regenerate_proof_object()
+                    proven_truth.proof().regenerate_proof_object(
+                        simplify_only_where_marked, markers_and_marked_expr)
                     .proven_truth)
                 proven_truth = (new_proven_truth.inner_expr()
                                 .with_mimicked_style(proven_truth.expr))
@@ -246,16 +263,19 @@ def decorated_relation_prover(*args, **kwargs):
                             "have an 'expr' attribute."%func)
         alter_lhs = kwargs.pop('alter_lhs', False)
         if not alter_lhs:
-            # preserve the left side.
-            if 'preserve_expr' in kwargs:
-                if 'preserved_exprs' in kwargs:
-                    kwargs['preserved_exprs'] = (
+            if automatic:
+                kwargs['preserve_lhs'] = True
+            else:
+                # preserve the left side.
+                if 'preserve_expr' in kwargs:
+                    if 'preserved_exprs' in kwargs:
+                        kwargs['preserved_exprs'] = (
                             kwargs['preserved_exprs'].union([expr]))
+                    else:
+                        kwargs['preserved_exprs'] = (
+                            defaults.preserved_exprs.union([expr]))
                 else:
-                    kwargs['preserved_exprs'] = (
-                           defaults.preserved_exprs.union([expr]))
-            else:
-                kwargs['preserve_expr'] = expr
+                    kwargs['preserve_expr'] = expr
 
         # Use the regular @prover wrapper.
         proven_truth = decorated_prover(*args, **kwargs)