Discussion: Simproc blog post

Stream: general

[Paul Lezeau]

@Yaël Dillies and I are currently writing a series of blog posts about simprocs - we'd love to hear if people have suggestions/things they would like to see in the next two posts (which will 1) cover a bit of the internals of simpand 2) give some demos of how to write simprocs).
The current drafts are here and here.

[Marc Huisinga]

Are there any plans for Verso usage in community blogposts?

[Eric Wieser]

I suspect people would be happy to switch and write new posts with verso, but no one is excited to take on the work of switching the current site over

[Eric Wieser]

(probably adapting the existing posts is easy, it's setting up the CI and boilerplate which is tedious)

[Bryan Gin-ge Chen]

I'd be happy to try and set up Verso for the community blog / website but last I looked there wasn't yet enough documentation for me to easily get started. Are there now (public, open-source) examples of Verso sites that we could reference?

[Ayhon]

Sometimes I'm surprised with how rw is able to perform some rewrites that simp only isn't. Admittedly I haven't read the drafts yet, but I'd be interested to know why if they don't answer this already.

Example

Consider the following proof.

@[simp] theorem Vector.getElem!_mk {xs : Array α}[Inhabited α] {size : xs.size = n} {i : Nat} :
    (Vector.mk xs size)[i]! = xs[i]! := by
    if h : i < n then
      simp only [getElem!_pos, h, size, Vector.getElem_mk]
    else
      -- simp only [getElem!_neg, h, size]
      rw [getElem!_neg]
      case h => assumption
      rw [getElem!_neg]
      case h => exact size ▸ h

I would expect that simp only with the necessary information would be able to finish the proof. However, it does not, I need to use rw's independently.

[Floris van Doorn]

@Ayhon There are cases where rw works and simp doesn't, related to matching. But in this case it's just that simp cannot prove the hypothesis by simp. Using simp only [not_false_eq_true, getElem!_neg, h, size] works

[Floris van Doorn]

(which I found using simp? [getElem!_neg, *])

[Ayhon]

Hmm, interesting. I assumed that since not_false_eq_true was not used in my previous proof it was not actually needed

[Floris van Doorn]

I think it's because of this behavior:

example {P : Prop} {Q : Prop → Prop} (h : ¬ P) : Q (¬ P) := by
  simp only [h] -- `P` is rewritten to `False`.

simp doesn't use ¬i < n to rewrite ¬i < n to True, but to rewrite i < n to False.

[Luigi Massacci]

@Paul Lezeau and @Yaël Dillies, thank you so much for this to the both of you, I'm eagerly awaiting the next ones! If I try to run the examples on the web editor though, I get two problems: Finset.Icc_ofNat_ofNat doesn't seem to exist (I can't find it by grepping mathlib either), and I can't get this one to reduce:

example (P : Prop) (a b : Nat) : (if P ∨ ¬ P then a else b) = a := by
  -- Works since `simp` can simplify `P ∨ ¬ P` to `True`.
  simp only [↓reduceIte]

(regardless of whether I add [Decidable P] or open Classical to make the decidablity error go away). Here simp only [↓reduceIte] makes no progress.

[Ayhon]

By default simp does not know P \/ not P to be true. You need to add something like Decidable.em.

example (P : Prop) (a b : Nat)[Decidable P] : (if P ∨ ¬ P then a else b) = a := by
  -- Works since `simp` can simplify `P ∨ ¬ P` to `True`.
  simp only [↓reduceIte, Decidable.em]

That works for me

[Luigi Massacci]

Ayhon said:

By default simp does not know P \/ not P to be true.

I know that, hence my surprise. Funnily enough vanilla simp can close the goal, which undermines one of the points of the blog post somewhat

[Ayhon]

Aaah, sorry, you were copy-pasting from the article

[Luigi Massacci]

Yes, I know the goal is provable in general ; )

[Ayhon]

I had assumed that far, I just thought you were stating that Lean was able to deduce P ∨ ¬ P automatically. However, it's not you but the article which is stating this. There's something amiss then

[Paul Lezeau]

Oups, we definitely wanted Decidable.em in the simp only call - thanks for flagging this!
For Finset.Icc_ofNat_ofNat, I think we were assuming that #22039 would get merged before the blog post.
I'll fix both issues tonight:)

[Luigi Massacci]

Paul Lezeau said:

we were assuming that #22039 would get merged before the blog post.

No one will ever accuse you of being a pessimist :laughing:

[Yaël Dillies]

Paul Lezeau said:

we were assuming that #22039 would get merged before the blog post.

Maybe a maintainer can step in and get it merged? :innocent:

[Ching-Tsun Chou]

Thanks for writing the blog post! I did not even know about the existence of simproc before reading this post. (Simproc is not mentioned in the standard introductory Lean books.) Is there a way to search for available simproc's? Searching for "simproc" at https://leanprover-community.github.io/mathlib4_docs/ returns mostly irrelevant results.

[Ruben Van de Velde]

@Paul Lezeau There seem to be a number of formatting issues in the rendered blog post

[Paul Lezeau]

Indeed - fixing those now:)

[Paul Lezeau]

(it seems like the markdown render I have on my personal laptop doesn't work in the same way as the blog one)

[Paul Lezeau]

leanprover-community/blog#121 should hopefully fix things

[Ruben Van de Velde]

Probably the lean above structure Simp.State is also unintentional

[Paul Lezeau]

Indeed, and some of the bullet point lists have gone astray! Will push some more fixes

[Emilio Jesús Gallego Arias]

Bryan Gin-ge Chen said:

I'd be happy to try and set up Verso for the community blog / website but last I looked there wasn't yet enough documentation for me to easily get started. Are there now (public, open-source) examples of Verso sites that we could reference?

Great Bryan ! I'd be happy to help if that's within my skills; I'd suggest opening a separate topic for that discussion.

There are some examples of Verso websites at:

• https://github.com/leanprover/verso-templates
• https://github.com/leanprover/verso/tree/main/examples
• https://github.com/leanprover/reference-manual
• https://github.com/teorth/analysis

[Bryan Gin-ge Chen]

Unfortunately I didn't have enough time for this before I got busy with other things... If I come back to this, I will make a new thread though, thanks!