String/Lemmas

Stream: batteries

[Kim Morrison]

batteries#857: deal with nonterminal simps in String/Lemmas 

Makes a quick pass to turn nonterminal simps into simp onlys, as this file was breaking during an experiment with Nat simp lemmas.

[Kim Morrison]

I have left many -- FIXME nonterminal simp, but `simp?` gives a different result in the file. They don't seem to obstruct my progress, so I wasn't planning on resolving them.

[Kim Morrison]

If one of the authors of the file (@Bulhwi Cha, @Mario Carneiro?) might have a look at these, possibly creating an issue for the underlying simp? problem, that would be lovely.

[Kim Morrison]

Actually, some of these FIXMEs are obstructing further progress. In particular extract.go₂_add_right_cancel and extract.go₁_add_right_cancel are breaking on my branch, and both having an earlier nonterminal <;> simp which requires restructing the whole proof to avoid.

Help on fixing these would be appreciated.

[Mario Carneiro]

@Kim Morrison are you aware of the squeeze_scope tactic?

[Kim Morrison]

Yes, and I promise I did try it! Can't remember why I wasn't satisfied, sorry.

[Mario Carneiro]

I managed to use it and get something that compiles, although I didn't look at the proofs too hard

[Bulhwi Cha]

Kim Morrison said:

Help on fixing these would be appreciated.

I'm a little busy lately, but I'll look into these this week.

[Bulhwi Cha]

Kim Morrison said:

In particular extract.go₂_add_right_cancel and extract.go₁_add_right_cancel are breaking on my branch, and both having an earlier nonterminal <;> simp which requires restructing the whole proof to avoid.

I see that Mario Carneiro has already removed the nonterminal simps from these lemmas.

[Bulhwi Cha]

Bulhwi Cha said:

I've spent too much time proving String.splitOn_of_valid, which hasn't been reviewed for two months. I want to wait until the overhaul is finished.

This discourages me from working on lemmas about strings again. Still, it'll be easy to replace nonterminal simps with simp onlys using set_option tactic.simp.trace true. I'll try it.

[Mario Carneiro]

the easy version of this is to use simp? and accept the "try this" suggestion

[Bulhwi Cha]

Bulhwi Cha said:

Still, it'll be easy to replace nonterminal simps with simp onlys using set_option tactic.simp.trace true. I'll try it.

Oh, this isn't working, and neither is simp?.

[Bulhwi Cha]

The lemmas that still have nonterminal simps aren't created by me. I'll deal with them after the Lean core team completes the planned overhaul of the library work on strings.

[Mario Carneiro]

what do you mean by not working?

[Bulhwi Cha]

When I replaced the nonterminal simp in the proof of the theorem prev with the simp only that simp? suggested, the latter part of the proof broke down.

[Mario Carneiro]

it appears that the issue is the reference to prev which should be Iterator.prev

[Bulhwi Cha]

You're right. I'll look into the other lemmas and see if I can do the same.

[Mario Carneiro]

I guess that's a pretty printer bug

[Bulhwi Cha]

It seems that simp? mixes up a name with the same one in a different namespace.

[Bulhwi Cha]

I've removed all nonterminal simps from the lemmas that had the FIXME comment.

[Bulhwi Cha]

@Kim Morrison Is it okay to create a pull request whose base branch is for another person's PR? I've just created batteries#864.

[Bulhwi Cha]

@Mario Carneiro said:

I guess that's a pretty printer bug

Did you create a bug report? If not, I'll do it.

[Kim Morrison]

Bulhwi Cha said:

Mario Carneiro said:

I guess that's a pretty printer bug

Did you create a bug report? If not, I'll do it.

Thanks!

[Bulhwi Cha]

I've opened lean#4591.