Failure of weakening?

[lambdacalculator]

Sorry for dropping into the middle of a proof, but a single proof state should be enough to illustrate my problem (in Abella 2.0.5):

Variables: G R G' T T' E1 E0 E2 E' E'1
IH : forall G R G' E T T', rep_ctx G R G' -> {G |- of E T}* ->
       {R |- rept T T'} ->
       (exists E', {R |- rep E T E'} /\ {G' |- fof E' T'})
H1 : rep_ctx G R G'
H3 : {R |- rept T T'}
H4 : {G |- of E2 nat}*
H5 : {G |- of E0 T}*
H6 : {G, of n1 T |- of (E1 n1) T}*
H7 : {R |- rep E2 nat E'}
H8 : {G' |- fof E' (all (t\arr t (arr (arr t t) t)))}
H9 : {R |- rep E0 T E'1}
H10 : {G' |- fof E'1 T'}
H11 : {G |- typ T}
H12 : rep_ctx (of n1 T :: G) (rep n1 T n1 :: R) (fof n1 T' :: G')
============================
 exists E', {R |- rep (iter E2 E0 E1) T E'} /\ {G' |- fof E' T'}

After apply IH to H12 H6 H3, I get

Error: Unification failure (constant clash between :: and R)

But if I explicitly weaken H3 with A1:assert {R, rep n1 T n1 |- rept T T'}. apply IH to H12 H6 A1. both tactics succeed. I thought weakening was for free in situations like this.

[chaudhuri]

Sorry for the delay in getting to this.

The problem here is that when you give an explicit argument to apply, it expects exactly what fits, not something upto weakening. This is different from underscore arguments to apply or search (implicit or explicit), which tries weakening to match.

Further investigation is needed to see if there is a way to relax this without breaking a lot of proofs.

[lambdacalculator]

Thanks for the comment. I seem to remember getting weakening in situations other than with underscore arguments, but I guess I was mistaken. My sense is that allowing weakening, even with explicit arguments, would not break any proofs, since it wouldn't disallow any currently-working tactics but only enable some tactics that wouldn't have worked before. Also, since the "infrastructure" needed to handle weakening is already present with underscore arguments, explicit arguments would just need inherit a little of that infrastructure. Said another way, I imagine every explicit argument as a special case of an underscore where there is a strong hint as to the shape of the proposition to be guessed. (This is just speculation, though, as I shamefully haven't looked at the code yet, although FWIW I hope to do so this summer.)

[chaudhuri]

I'm generally in agreement that weakening (monotonicity) should be tried by default no matter how the argument was selected (explicit or guessed).