Handling equalities is way too painful

[silene]

Consider the following simplified testcase:

Kind t type.
Type abs t -> t.
Theorem foo : forall (T : t -> t) U V,
  T U = T V -> abs (T U) = abs (T V).
intros.

This goal should be trivial to prove by doing case H1. Unfortunately it does not work. Doing case H1 does not modify the goal, it just creates a new hypothesis H2: T U = T V, which is just H1 again. No progress was made at all!

So, let us try it another way. Let us first assert a simpler goal and then try to apply it:

assert forall A B, A = B -> abs A = abs B. (* automatically discharged *)
apply H2 to H1 with A = T U, B = T V.

Unfortunately, it still does not work. Doing apply just creates H3: T U = T V (no abs!). So, yet again, no progress was made.

The only way to succeed (that I found) was:

assert forall A B, A = B -> abs A = abs B. (* automatically discharged *)
backchain H2.

Not only is it ugly, but it does not scale. On more complicated goals, it is just impossible to use backchain (if only because the goal is not an equality). This leads to very contrived proofs for goals that would have been trivial to discharge if case worked correctly.

[ThatDaleMiller]

Equality as an assumption in Abella is treated via unification. Your example H2: T U = T V is an example of what is called a flex-flex pair since both of the two terms involve a variable (T) at their head. Actually, the unification in Abella is really pre-unification which means that, in general, Abella does attempt to solve flex-flex pairs at all: they are left untouched. This is why your first case statement makes no progress. There can be a great deal of non-determinism when attempting to unify T U = T V, and the degree of non-determinism is dependent on the signature of constants.

The only way I see to prove your theorem foo is to use the lemma forall A B, A = B -> abs A = abs B as you illustrated.

I would rather paraphrase your criticism not as a critique of equality in Abella but more as a critique about how it treats flexible terms in equations. Since flex-flex pairs have seldom appeared in most applications, we have not tried to propose a means to treat such pairs better.

Your theorem foo is not the kind of theorem that we have seen arise in the many applications we have of Abella. If you have an application where propositions such as foo need to be regularly solved, please let me know.

[silene]

If you have an application where propositions such as foo need to be regularly solved, please let me know.

Yes, we have a theorem where the issue appears all over the place. (We are not yet ready to disclose the full development, sorry.) The consequent of the theorem looks like T U = T' U. (In case you wonder, the theorem would be wrong if the consequent was T n1 = T' n1.). So, in all the subcases of the proof, we have to prove this kind of equality. Here is what the script looks like:

  assert forall A B, nabla x, A x = B x -> abs A = abs B.
  backchain H11.
  ...
  assert forall A B, nabla x, A x = B x -> abs A = abs B.
  backchain H11.
  ...
  assert forall A B C, A = B -> app A C = app B C.
  backchain H13.
  ...
  assert forall A B C, A = B -> app C A = app C B.
  backchain H14.
  ...
  assert forall (A B : trm -> trm) U, nabla x, A x = B x -> A U = B U.
  backchain H13 with A = X U*, B = X1 U*.
  ...
  assert forall (A B : trm -> trm) U, nabla x, A x = B x -> A U = B U.
  backchain H14 with A = X U*, B = X1 U*.
  ...
  assert forall (A B : trm ) (T : trm -> trm) , A = B -> T A = T B.
  backchain H14 with T = a\ X1 U* a.

There can be a great deal of non-determinism when attempting to unify T U = T V, and the degree of non-determinism is dependent on the signature of constants.

I see.

That said, in our case, it does not seem like we need something sophisticated. If search was turning a goal C x1 ... xn = C y1 ... yn (with C a rigid symbol) into n goals x1 = y1 ... xn = yn, and if it was eta-extending all the abstractions, this would make short work of the first 4 subcases. This should not introduce any kind of non-determinism, if I am not mistaken.

This leaves open the question on how to deal with the last 3 subcases. But, given that we had to use with clauses, I am willing to admit that these cases are much harder and will never be solved automatically.

[ThatDaleMiller]

One thing apparent from your example using assert and backchain is that it is possible to use backchain with a previous proved theorem and not just with an hypothesis (yes, the manual is confusing about this). For example,

Kind t type.
Type abs t -> t.

Theorem cong-abs : forall A B, A = B -> abs A = abs B.
  intros. case H1. search.

Theorem foo : forall (T : t -> t) U V,
  T U = T V -> abs (T U) = abs (T V).
intros. backchain cong-abs.

Thus, your sample can be simplified by proving several simple congruence-like theorems, such as

forall A B, A = B -> abs A = abs B.
forall (A B : trm -> trm), nabla x, A x = B x -> A = B.
forall A B C, A = B -> app A C = app B C.
forall (A B : trm -> trm) U, nabla x, A x = B x -> A U = B U.
forall (A B : trm ) (T : trm -> trm) , A = B -> T A = T B.

and then using backchain with the name of the respective theorem. The backchaining step must do some matching in order to find appropriate instantiations for universally quantified variables: such matching might be incomplete, so backchaining might not work all the time. Also note that, for the sake of using `backchain', the second lemma above is better written as

forall (A B : trm -> trm), (nabla x, A x = B x) -> A = B.

Although these are logically equal, backchaining will only need to generate instances for A and B and will not need to find an instance of the nominal x.

Regarding your suggestion of "turning a goal C x1 ... xn = C y1... yn (with C a rigid symbol) into n goals x1 = y1 ... xn = yn, this does seem interesting and probably easy to support. It could be called "simpl" after Huet's procedure of the same name.

[silene]

One thing apparent from your example using assert and backchain is that it is possible to use backchain with a previous proved theorem and not just with an hypothesis (yes, the manual is confusing about this).

That is how I did it initially. But once I noticed that assert automatically calls search which automatically discharges these lemmas, the proof process flowed better by just using assert. No need to dismiss the current proof, find a name, state the lemma (and possibly get it wrong because you no longer see the current goal), write a proof, restore the previous proof, and apply the lemma. Just asserting the intermediate goal feels much more efficient. Especially since most of the lemmas are used only once (and it is hard to predict when that will not be the case). Anyway, tastes and colors.

the second lemma above is better written as forall (A B : trm -> trm), (nabla x, A x = B x) -> A = B.

That is interesting. Abella tries very hard to discourage the user from ever parenthesizing nabla (e.g., Error: Can only induct on predicates and judgments). So, I did not even think about it.

That said, I do not see any difference. It seems Abella is just as happy with

  assert forall A B, (nabla x, A x = B x) -> abs A = abs B.
  backchain H11.

and

  assert forall A B, nabla x, A x = B x -> abs A = abs B.
  backchain H11.

Moreover, I am getting really confused by the fact that the following fails:

Theorem cong-abs:
  forall (A B : t -> t), nabla x, A x = B x -> abs A = abs B.
intros.
search. /* Error: Search failed */

while the following succeeds:

Theorem cong-abs:
  forall (A B : t -> t), nabla x, A x = B x -> abs A = abs B.
search. /* Proof completed. */

Parenthesizing nabla does not change a thing; calling intros first causes search to fail.

[ThatDaleMiller]

I guess I need to take back my claim about putting a scope on nabla to help backchaining. I tried to find my counterexample and haven't been able to reproduce it. I'm glad that the implementation is more robust than I thought it might be.

Looking forward to seeing your examples (when they are ready).

[chaudhuri]

Parenthesizing nabla does not change a thing; calling intros first causes search to fail.

The intros tactic does not do any left-asynchronous rules, whereas search does some obvious cases. Basically, intros preserves the hypothesis (A x = B x), while search automatically applies (the equivalent of) case on it.

The search tactic was extended in this way after a number of users complained that search was stupidly going down branches that can be obviously closed, making writing large proofs either slow or tedious.

As to why this discrepancy between the two tactics exists: making intros also do left-asynchronous rules breaks all our existing example proofs. As usual, backwards compatibility forces us to make non-optimal design choices.

[silene]

making intros also do left-asynchronous rules breaks all our existing example proofs

That makes sense, and it explains why intros cannot be changed. But why not make search a bit stronger, i.e., make it apply the equivalent of case to hypotheses before it starts? That way, whether intros is performed or not would not modify the behavior of search. Or would that break compatibility too?

[JimmyZJX]

I am also experiencing some of the problems discussed here. I wonder if a rewrite tactic makes sense and solves at least some problems.

For example,

Theorem foo : forall (T : t -> t) U V,
  T U = T V -> abs (T U) = abs (T V).
intros.
rewrite H1. % substitute (T U) to (T V) everywhere except H1, and leave other T/U/V unchanged

[ThatDaleMiller]

The following code is a workaround. Since Abella will not reason forward from an assumption of the form T U = T V, you can instead reason backward.

Kind t     type.
Type abs   t -> t.

Theorem bar : forall X Y, X = Y -> abs X = abs Y.
 intros. case H1. search.

Theorem foo : forall (T : t -> t) U V,  T U = T V -> abs (T U) = abs (T V).
  intros. backchain bar with X = (T U), Y = (T V).

Having said this, it seems odd to be proving foo when bar is a more general theorem with a trivial proof.

[JimmyZJX]

Thanks for the reply. I am aware of this type of wordaround and have used the technique several times before.

What I suggested was to add a new logic rule (or just a tactic) that explicitly rewrites the left-hand-side/right-hand-side term in hypotheses or goal, which might not solve all the problems discussed above, but at least some.