Replace a term with its definition

Stream: new members

[Pieter Cuijpers]

I'm running into the following type of problem regularly, and am wondering if there is a simple way to approach it.
I hope I can explain what I mean clearly.

Consider the Lean4 code at the end of this post.
In it, I define a number of classes, an instance, and a property, and subsequently want to check that the instance has the property.
What I run into is illustrated by the first "state" - which I commented in.
The goal simply states: is_associative.
Now it seems that I have to look-up is_associative manually and then conclude I can get on with my prove using intro x y z.
A 'better' way would be if I had a way to let Lean unfold the definition of is_associative automatically.
Is there a tactic for that?

I run into the same problem again after the intro x y z, because the state then indicates Operator while in principle Lean should be able to unfold that definition into the underlying functions. Actually, I don't even know what to use to finish the proof in this case, so any help there would probably be a good hint in the right direction as well.

class Property (α : Type u) where
  contains : α → Prop

class Operation (α : Type u) where
  op : α → α → α

class IOperation (α : Type u) where
  iop : Property α → α

instance [I : IOperation α] : Operation α where
  op := λ x y => I.iop ⟨ λ z => z = x ∨ z = y ⟩

def is_associative [O : Operation α] := ∀ x y z, O.op x (O.op y z) = O.op (O.op x y) z

theorem is_associative_I [I : IOperation α] : @is_associative α (@instOperation α I) := by
  /-
  α : Type u_1
  I : IOperation α
  ⊢ is_associative
  -/
  intro x y z
  /-
  α : Type u_1
  I : IOperation α
  x y z : α
  ⊢ Operation.op x (Operation.op y z) = Operation.op (Operation.op x y) z
  -/
  admit

[Alex J. Best]

One way is to use dsimp, for instance

dsimp only [is_associative]

will work in your case

[Pieter Cuijpers]

Great, that indeed works well on the first step.
But to simplify the "Operation.op" after the intro, it's not so clear to me how I could use it?
dsimp [instOperation I] doesn't seem to help

[Alex J. Best]

dsimp [Operation.op, instOperation]

will unfold everything for the next step, then it gets a bit tricky because I don't quite understand what is being modelled!

[Kevin Buzzard]

PS #backticks (that's a link -- you can edit your first post if you like)

[Pieter Cuijpers]

Wonderful! Thanks a lot. I think I can manage what comes after that :-)

[Pieter Cuijpers]

Reading up a bit on dsimp https://leanprover-community.github.io/extras/simp.html I get the impression I should be careful using simp or dsimp "in the middle of a proof" except in specific cases. Your suggestion of dsimp only [...] is indicated as "safe", but I don't fully grasp the rationale behind these remarks yet. Is it because the execution of "simp" may change when theorems are added to it, so your proof might all of a sudden break if the context changes?

[Kevin Buzzard]

Yes that's it -- it's a PITA to have to fix up someone else's proof in your PR because you added some cool new simp lemmas which broke someone else's poorly-written code.

[Kevin Buzzard]

If simp works and makes progress but doesn't close a goal, you can replace it with squeeze_simp and then click on the blue output which will replace again with simp only [list of lemmas] which should hopefully work.

[Yaël Dillies]

Note that "non-terminal dsimp" are very much accepted, because the goal after is guaranteed to be defeq to the goal after.

[Mario Carneiro]

well, rw can still fail after a non-terminal dsimp

[Yaël Dillies]

Yes but that's much easier to fix than a non-terminal simp where you might get into a completely different goal.

[Yaël Dillies]

Our goal is not that no proof will ever break, right? That's unreachable. Our goal is that when a proof breaks it is fixable easily. And having a goal that's defeq to what it should be makes breakage easily fixable.

[Mario Carneiro]

I'm not sure it's true that defeq is any easier to fix than non-defeq when your goal looks completely different after a big simp. I would say that it is only okay if the follow up tactic is not sensitive to the goal except up to defeq, e.g. if you use exact / refine / apply / change

[Mario Carneiro]

which is similar to the rule we have for nonterminal simp - it is okay as long as you follow up with a tactic that is not sensitive to details of the goal like ring / linarith / tidy / another simp