[Merged by Bors] - feat: rcases and rintro tactics

[digama0]

I finally got around to porting rcases for real. There are a few things that should probably be upstreamed: generalizeExceptFVar is a piece of a function in cases, and FVarSubst.append does not belong here. Indeed FVarSubst.append is only needed because cases does not expose a FVarSubst argument even though it talks about having one in the comments.

obtain, rcases, and rintro are fully implemented, but rcases? and rintro? have not been implemented yet; I intend to do these in a follow up PR.

[digama0]

This is in one sense a failed test: the original had -|-|- to test that the parser hack for |- worked, but the new parser has no hack and fails to parse this correctly. Is this an argument for removing the |- token?

[gebner]

Yes, I believe we wanted to remove it from Lean 3 as well.

[pechersky]

Would it be possible to add tests for how rfl works as a pattern, and how _ works as a pattern?

Separately, iirc, in mathlib3, unpatterened rcases does the same thing as cases. Reading the implementation here, it seems that unpatterened rcases is not supported. Is that right?

[digama0]

@pechersky rcases does not accept the plain list-of-names syntax of cases in mathlib. The plan is to have a separate cases' tactic to handle that (which is needed for mathport). I think for lean 4 we should try not to ever use cases' though; I think rcases is strictly better than cases', and cases is also often an option although the syntax is significantly different.

[gebner]

Suggested change

	This satisfies `(s.append t).apply e = t.apply (s.apply e)` -/
	This satisfies `(s.append t).apply e = t.apply (s.apply e)`
	for `e` that are in the domain of `s`. -/

AFAICT, most tactics only return substitutions for the variables that they changed (i.e. subst x would not return a substitution for an α : Type at the beginning of the local context).

[digama0]

No, the original statement is correct. Note that s.apply e will return e unchanged if it is not in the substitution map. BTW, I think that any tactic that provides a FVarSubst should also take a FVarSubst as input, which serves no purpose other than to be the base for insertion. This is essentially the same as the dlist encoding of lists: it is more efficient to carry along a running substitution and add to it rather than using append (which is a workaround for those tactics that don't provide differential FVarSubst output).

[gebner]

Note that s.apply e will return e unchanged if it is not in the substitution map.

This is precisely the issue. If s doesn't contain e but t does, then e won't appear in the result of append.

Say you have the following context:

x y : Nat
h1 : x = y
z w : Nat
h2 : z = w
k : Fin y

Then subst h2 will return s = {w ↦ w', h2 ↦ h2'}. If you call subst h1 after that, you get t = {y ↦ y', h1 ↦ h1', k ↦ k'}. Note that s.append t = s keeps y and k unchanged even though they were renamed by the second subst. (This is all based on just reading the code; I didn't run it. I hope I'm wrong.)

[digama0]

Let me put it another way: (s.append t).apply e = t.apply (s.apply e) is the definition of append, and the implementation is whatever is necessary to make this equation true. In your example s and t have disjoint domains, so s.append t should just be the union of the maps. As far as I can tell this is also the behavior of the implementation: it inserts every element in s to t (the t.apply v call just reduces to v). We get {y ↦ y', h1 ↦ h1', k ↦ k'} |>.insert w w' |>.insert h2 h2' = {y ↦ y', h1 ↦ h1', k ↦ k', w ↦ w', h2 ↦ h2'} as expected.

[gebner]

Ah, nevermind. You're right. I missed the t at the end.

[gebner]

bors r+

[bors]

Pull request successfully merged into master.

Build succeeded:

• Build