Enhance trivial proof tactic

[brianhuffman]

Currently the trivial proof tactic can only discharge proof states with goals of the form EqTrue True (possibly surrounded by some number of Pi quantifiers). It would be good to generalize this a bit. In particular, we should enable it to solve any goal of the form Eq t x x by reflexivity. Note that EqTrue True is definitionally equal to Eq Bit True True, so it is also an instance of reflexivity.

Even better would be to have an extensible set of theorems that could be resolved with proof goals to solve them, of which reflexivity could be one.

[robdockins]

Agreed, I think it would be very nice generalization to enhance trivial to solve instances of reflexivity. It would be even better, I think, to have it solve reflexivity up to conversion (i.e., try to unify the two sides). This would reduce the need for finding exactly which simplification rules will make them look identical.

However, I'm a little more skeptical about adding extensible theorems. That sounds to me like it would be better as a separate tactic.

[brianhuffman]

Yeah, maybe the extensibility is a bit overkill for trivial. (The idea was inspired by the . tactic in Isabelle/Isar proofs, which is similarly extensible.) I like the reflexivity-up-to-conversion idea.

[robdockins]

Does scConvertible do the job we want?

[brianhuffman]

Not quite. We really want to check whether a term unifies with the pattern Eq ?t ?x ?x modulo convertibility, but scConvertible requires two complete terms, not a term and a pattern.

Unless we want to implement a generic matching- or unification-modulo-convertibility operation, we might need to do something a bit ad-hoc. Probably what we need is to evaluate the goal to whnf (with scWhnf), then check that it's of the form Eq ?t ?x ?y, and finally call scConvertible on the terms that matched ?x and ?y.

[robdockins]

Your second paragraph there was basically what I had in mind, modulo questions about handling free variables from going under Pi binders.

[robdockins]

I guess we could just try to actually build the corresponding proof term and type-check it? That might be easier.

[robdockins]

Some local testing indicates that building a candidate proof term from Refl and checking that it is convertible with the goal will work. I think this should be pretty easy to implement.

[robdockins]

Fixed via #1568