rename valid -> emp_valid

Fixes #159 (closed)

I don't have time to verify that you have replaced all occurrences, but other than that, it seems fine to me.

I verified that by checking all occurrences of (case-insensitive) "valid" in bi/ and proofmode/. The only thing left is iIntoValid, do we want to change that as well?

Yes, I think so.

Then please help me update the docs. Currently it says something about the goal having to be of the shape uPred_valid, which is certainly not true any more.

added 1 commit

• 42655ec9 - iIntoValid -> iIntoEmpValid

Compare with previous version

The tactic [iIntoEmpValid] tactic solves a goal [bi_emp_valid Q]. The arguments [t] should be a Coq term whose type is of the following shape:

[∀ (x_1 : A_1) .. (x_n : A_n), φ]

So that we have an instance AsValid φ Q.

Examples of such [φ]s are

• [bi_emp_valid P], in which case [Q] should be [P]
• [P1 ⊢ P2], in which case [Q] should be [P1 -∗ P2]
• [P1 ⊣⊢ P2], in which case [Q] should be [P1 P2]

The tactic instantiates each dependent argument [x_i] with an evar and generates a goal [R] for each non-dependent argument [x_i : R].

I just stared at this for 5min, but cannot comprehend the mutual recursion between go and go_specialize.

So, I changed the name, but if we're touching this tactic anyway I'd prefer if we could also update the documentation. But one of you @robbertkrebbers @jjourdan will have to do that.

I just stared at this for 5min, but cannot comprehend the mutual recursion between go and go_specialize.

I have no idea, @jjourdan is responsible for that ;)

Okay, that's a good start, thanks. I still have some questions though: Does it solve the goal? Then it should rather be called iSolveEmpValid. Also that can't be true because how would it even solve arbitrary such goals.^^ Or does it somehow transform the goal into a different goal? Then what exactly happens with all those quantifiers?

In principle, it solves such a goal, and fails if it cannot solve it. For example, if the goal is bi_emp_value False and t is of type P ⊢ True, then the tactic will just fail.

For the quantifiers, these become either evars or new subgoals. Consider the original goal was Q and we t has type ∀ x, P x ⊢ Q, then it generates an evar ?x for x and a subgoal P ?x.

Oh, right, I forgot about the argument -- so the argument has to somehow match the goal, and your doc actually says how. Makes sense, thanks.

Consider the original goal was Q and we t has type ∀ x, P x ⊢ Q, then it generates an evar ?x for x and a subgoal P ?x.

That does not match your previous explanation though: φ would be P x ⊢ Q ("the thing below all the Coq quantifiers"), but then the goal must be sth. with P x -* Q. Did you mean ∀ x, P x -> Q for the type of t, i.e., P is a Coq-level predicate? That'd also make more sense wrt. opening a subgoal.

Did you mean ∀ x, P x -> Q for the type of t, i.e., P is a Coq-level predicate? That'd also make more sense wrt. opening a subgoal.

Yes, thanks for spotting the error in my example!

added 1 commit

• 803d4b3d - update iIntoEmpValid docs

Compare with previous version

All right, updated MR. Good to merge?

Fine to me.

@jjourdan agreed at https://gitlab.mpi-sws.org/FP/iris-coq/issues/159#note_25681. Going ahead and merging.

mentioned in commit 93ef2352

merged

mentioned in issue #159 (closed)

added T-proofmode label

removed T-proofmode label