revert/intro with implementationDetail hypotheses

Stream: lean4

[Jannis Limperg]

I just realised that the revert/intro pattern promotes any implementationDetail hypothesis to default status. For example, consider the context

a b : A
_x : P a
h : a = b

where _x is an implementationDetail, so it's invisible and supposed to be ignored by everything. Running subst h will revert anything after a, including _x, and then reintroduce _x : P b. But at that point, we've forgotten that _x was an implementationDetail, so it becomes a regular hypothesis. This severely limits the utility of implementationDetail hypotheses: you can only use them reliably for closed terms.

What to do (if anything)? One option would be to have revert put an mdata wrapper around the type of _x, indicating that _x was previously an implementationDetail. intro would then consume this wrapper. As a bonus, this would probably reveal a number of latent mdata-related bugs since revert/intro is so common. :innocent:

[Jannis Limperg]

Actually, it might be better to encode the implementationDetail-ness in the name of the forall or let, rather than its type.

[Jannis Limperg]

I investigated this a bit more. Currently, revertAfter clears auxDecl hypotheses (but not implDetail hypotheses) by default if it would have to revert them. Plain revert (both the MetaM version and the tactic) fails by default under the same circumstances. This treatment of auxDecls should probably be extended to all implementationDetail hypotheses.

Going beyond that, it would be easy to add a new mode to revert which allows implementationDetail hypotheses to be reverted, marking them for special treatment by intro as described above. This would be suitable for tactics which internally use the revert/intro pattern.

However, for the revert tactic, there's no good choice:

• It can make implementationDetail hypotheses visible, breaking the abstraction.
• It can fail when encountering implementationDetail hypotheses, again breaking the abstraction.
• It can silently clear implementationDetail hypotheses, but that would make implementationDetail hypotheses unsuitable for attaching persistent metadata to goals.

[Mario Carneiro]

Last time we discussed this, I believe we decided to go for the third option, clearing implDetail hypotheses, because we don't want metadata from these hypotheses to leak into the proof term

[Mario Carneiro]

and actually reverting them is a big problem for things like auxDecl hypotheses because they aren't real hypotheses

[Mario Carneiro]

if you want persistent metadata on goals you should be using mdata in the type of the mvar

[Mario Carneiro]

that's what I'm doing for iris-lean

[Jannis Limperg]

Okay, I'll try that.

This treatment of auxDecls should probably be extended to all implementationDetail hypotheses.

Should I make a patch for this part?

[Mario Carneiro]

it seems reasonable, no promises you won't get massive breakage though :innocent: