three beginner's questions on `dsimp`

Stream: new members

[rzeta0]

I have previously learned to use dsimp to unfold definitions.

For example dsimp Odd changes how a goal or hypothesis involving Odd is displayed, it is displayed as an existence proposition as per the definition in mathlib.

dsimp can be extended eg dsimp [Odd, Even] to unfold both definitions.

Today I saw dsimp used without any parameters, just on its own - eg example 4.1.7 in Mechanics of Proof.

Question 1: What does dsimp on its own do? It would be different from dsimp at *, which I am also not sure about.

Question 2: The mathlib definition of dsimp says it changes goal states, but the beginner course Mechanics of Proof says dsimp only changes how the goal state is displayed, nothing internal is changed. Is that just a useful simplification for beginners?

Question 3: I have found that the effect of dsimp seems to wear off and I need to repeat it further down the code. Is this a bug, or some scoping rule I'm not aware of. Sadly I don't have an MWE to show this.

[Henrik Böving]

I would suggest to read the hover information of dsimp and if that is not enough also read the one of simp.

[rzeta0]

I should have been clearer in my original post - the docs aren't clear for a beginner like me.

[Kevin Buzzard]

Did you read "Theorem proving in Lean"? This has a section on simp.

[rzeta0]

i'll take a look, thanks.

I've been working through the Mechanics of Proof, doing every exercise as I proceed, but suddenly in chapter 4 new syntax is introduced a few times without explanation.

[Kevin Buzzard]

I think you once said that you found #tpil too hard going when you last looked at it, but you're a lot more experienced now and so maybe it's a better fit now. It's a great book. I came into this area knowing nothing about type theory or computer science and it got me started, although I had a strong background in mathematics.