Closed RandomActsOfGrammar closed 4 years ago
An assertion with an equality to the left of an implication results in the two sides being equal for the remainder of the proof.
Consider the following theorem:
Theorem error : forall (x y a b : o), a = b. intros. assert (a = b -> x = y). skip. search.
The state after the assert is
assert
Subgoal 1: Variables: x y b ============================ b = b -> x = y Subgoal is: b = b
Note that the second subgoal has been changed from a = b to b = b.
a = b
b = b
We get the same behavior if we put the implication under a disjunction. In the following theorem
Theorem error2 : forall (x y a b : o), a = b. intros. assert (x = y \/ (a = b -> x = y)). skip. search.
the state after the assert is
Subgoal 1: Variables: x y b ============================ x = y \/ (b = b -> x = y) Subgoal is: b = b
However, if we instead put it under a conjunction, the two sides do not become equal. In proving
Theorem fine : forall (x y a b : o), a = b. intros. assert (x = y /\ (a = b -> x = y)). skip. skip.
the proof state after the assert is
Subgoal 1: Variables: x y a b ============================ x = y /\ (a = b -> x = y) Subgoal is: a = b
as we expect it to be.
I ran all these examples using Abella 2.0.6.
I believe this is what #113 describes, which is fixed in the master branch. Sadly the fix is not yet released.
I think you're right. I didn't find that one when I was looking for an existing issue.
An assertion with an equality to the left of an implication results in the two sides being equal for the remainder of the proof.
Consider the following theorem:
The state after the
assert
isNote that the second subgoal has been changed from
a = b
tob = b
.We get the same behavior if we put the implication under a disjunction. In the following theorem
the state after the
assert
isHowever, if we instead put it under a conjunction, the two sides do not become equal. In proving
the proof state after the
assert
isas we expect it to be.
I ran all these examples using Abella 2.0.6.