behaviour of simp in Lean vs Coq

Stream: general

[Arthur Paulino]

Johan Commelin said:

Arthur Paulino simp already exists, and is used a lot.

Hm, shouldn't I see true = true in the Lean Infoview here?
image.png
I tested simp but it didn't seem to do anything. And it doesn't show anything on hover. Also I can't crtl+click on it :thinking:

[Eric Wieser]

Using ; makes the goal view behave unhelpfully (at least in Lean 3, but it seems you're using Lean 4)

[Sebastian Ullrich]

Please note that this is Lean 4

[Yaël Dillies]

Johan Commelin said:

All my colleagues work with things like Kähler manifolds, or triangulated categories of motives.

Do you know we have a branch trying to define Kähler manifolds?

[Arthur Paulino]

You mean it behaves as expected in Lean 3?

[Sebastian Ullrich]

No, simp here behaves as expected. It applies all registered and explicitly passed equations, none of which are applicable here. Use @[simp] def orr or simp [orr] to add orr's equations to either set.

[Sebastian Ullrich]

Coq-Equations' simp also needs to be passed explicit arguments, doesn't it?

[Yaël Dillies]

Ahah! @Johan Commelin, not Kähler manifolds but Kähler modules: it's #4753.

[Johan Commelin]

Ooh, I know that one. It's important, but quite different from Kähler manifolds (-;

[Arthur Paulino]

In Coq you can just call simpl.:
image.png

[Johan Commelin]

(I've renamed this tail of the thread, because it was going in a different direction.)

[Sebastian Ullrich]

Ah, that is yet another Coq tactic. We don't have a normalization tactic like that. It seems most people prefer passing the defs to reduce explicitly.

[Arthur Paulino]

simp [orr] did the simplification and Lean was already satisfied with true = true
image.png

[Arthur Paulino]

maybe it simplified true = true further to true?

[Sebastian Ullrich]

to True, but yes :)

[Sebastian Ullrich]

In other words, Lean's simp is modelled after Isabelle, not Coq

[Arthur Paulino]

I see, but now it got me thinking because I asked Lean to explicitly simplify the orr and it feels like it did more than I wanted

[Yaël Dillies]

That's why you can use simp only [orr].

[Arthur Paulino]

simp only [orr] goes all the way down too

[Eric Wieser]

That's because one of the equation lemmas for "orr" is precisely your goal

[Eric Wieser]

If you're trying to prove a = b and you have h : a = b, you wouldn't say "rewrite to b = b, then reflexivity", you'd jump directly to "h is the proof"

[Mario Carneiro]

Sebastian Ullrich said:

Ah, that is yet another Coq tactic. We don't have a normalization tactic like that. It seems most people prefer passing the defs to reduce explicitly.

It would be really really nice to get a reduction tactic in lean. simp is the best we have but it's a poor approximation of kernel reduction. whnf can be made to work but is not configurable, and often goes too far.

[Mario Carneiro]

And yes, there are a lot of open design questions about how far to reduce given what input

[Arthur Paulino]

From an user standpoint, I'd want it to go as far as I want so I feel like I have complete control of what I'm doing

[Mario Carneiro]

I'd want it to go as far as I want

well yes, the hard part is reading the user's mind about this

[Mario Carneiro]

you can reduce too much and you can reduce not enough and both are bad

[Mario Carneiro]

simp has some control over reduction in the form of specifying what functions to reduce (plus some basic simp things like x = x is true)

[Arthur Paulino]

Hm, what if I could tell the number of reduction rounds? Lean would be able to know how many recursive calls would be allowed

[Mario Carneiro]

I think there is a cfg for that

[Mario Carneiro]

but it's really not a good way to write proof scripts because it is very specific to the particular rewrite sequence

[Mario Carneiro]

and if it has to backtrack then it gets much harder to specify where in the tree you want to go

[Arthur Paulino]

Right, I might want to take baby steps for a particularly hard step

[Mario Carneiro]

rw is better suited for baby steps. simp is more like "do all these things until you can't find anything to do"

[Arthur Paulino]

let me try rw

[Arthur Paulino]

How do I make rw accept one of my matches for orr?
image.png

[Mario Carneiro]

rw [orr]

[Mario Carneiro]

also, post code, not images

[Mario Carneiro]

see #backticks

[Arthur Paulino]

ah, the code itself doesn't show where the error lies. but now orr is underlined in red and the error says

tactic 'rewrite' failed, equality or iff proof expected
  Bool
b : Bool
⊢ orr true b = true

[Mario Carneiro]

this will work in lean 3, but I think lean 4 doesn't support it yet and you have to make do with simp

[Mario Carneiro]

There are some settings you can give to simp to make it act basically like rw, this is the simp_rw tactic in lean 3

[Mario Carneiro]

eh, could you post your code?

[Arthur Paulino]

def orr : Bool → Bool → Bool
| true, _ => true
| false, b => b

theorem orr_true (b : Bool) : orr true b = true := by
  {rw [orr]}

[Arthur Paulino]

I'm satisfied if it's because it's still WIP tho, no worries :smiley:

[Yaël Dillies]

rfl does it :wink:

[Arthur Paulino]

Oh, I know. I'm not just trying to prove the theorem. I'm trying to do it in a controlled way. Going directly to reflexivity might be a big leap for people who are trying to understand how computers handle programmed proofs

[Mario Carneiro]

Oh, it looks like you can't turn off eq_self, even if you use simp only. There should probably be a config option for that

[Mario Carneiro]

lean 3 has a whole collection of more controlled unfolding tactics, like dsimp, unfold, delta and others. As far as I know most of them don't exist in lean 4 yet

[Mario Carneiro]

and some of them might be "won't fix" since the number of unfolding tactics in lean 3 is a little ridiculous

[Mario Carneiro]

One way to prevent it from closing the goal is to change the rhs to something less trivial:

theorem orr_true (b : Bool) : orr true b = c := by
  simp only [orr]
  -- |- true = c

[Arthur Paulino]

Makes sense. Let's see how the API design will evolve. For me it was very impactful to my learning process to see how Coq processed everything until it ends up with types I defined on both ends of the equation

[Mario Carneiro]

well, API design doesn't evolve on its own, it needs input from people "in the field" to see what works. Generally things don't change unless someone (usually one of the developers) runs across a paper cut and tries to fix it

[Arthur Paulino]

Right, that's what I meant :smiley:

[Arthur Paulino]

But just to rephrase what I meant before. It would make more sense to me for simp to go all the way until it can't progress if it didn't accept parameters. But if I have to explicit the orr as a parameter, I would expect it to be more surgical on what to simplify.

[Mario Carneiro]

it is being surgical; it is just that your definition of surgical doesn't include reflexivity and simp's does

[Mario Carneiro]

also, keep in mind that simp only is not only for teaching; mathlib uses it a lot, because the default simp set is expensive in many circumstances, and adding eq_self all the time for proofs of e.g. (x + y) + z = x + (z + y) by simp only [add_comm, add_assoc] would get tiresome

[Arthur Paulino]

Mario Carneiro said:

it is being surgical; it is just that your definition of surgical doesn't include reflexivity and simp's does

Thanks for the clarification. That's precisely it. You were surgical :smiley: