## Stream: new members

### Topic: Coq cbn simpl

#### awalterschulze (Oct 30 2022 at 11:50):

Is there a way to evaluate some code inside a proof, just like cbn or simpl does in Coq?
Lean4's simp tactic only seems to work if the goal is completed by the operation, but what about if you only want to take step forward and evaluate the code as much as possible, given some cases have made some of the variables specific.

#### Kyle Miller (Oct 30 2022 at 12:10):

Want to create a #mwe illustrating what you're talking about? I think simp might be what you're looking for, but how you use it might depend on specifics. A general hint: if f is the name of the function you want evaluated, you can do simp [f].

#### awalterschulze (Oct 30 2022 at 12:47):

Thank you simp [f] seems very useful, but what do you do if you don't know the function name?

I'll try to work on a minimal working example

#### awalterschulze (Oct 30 2022 at 13:01):

Here is a minimal working example, we simp didn't work, but simp [ordering_mplus] worked:

def ordering_mplus (x: Ordering) (y: Ordering): Ordering :=
match x with
| Ordering.eq => y
| _ => x

theorem ordering_mplus_assocy (a b c d: Ordering):
ordering_mplus (ordering_mplus a b) (ordering_mplus c d) =
ordering_mplus (ordering_mplus a (ordering_mplus b c)) d  := by
cases a
case lt => rfl
case gt => rfl
case eq =>
simp [ordering_mplus]
cases b <;> rfl


simp [F] seems to evaluate very deeply, much like simpl in Coq, which is great and something I really wanted, thank you.
Now I wonder if we can also get cbn equivalent.

Sometimes you also want a tactic that only steps a small amount like cbn would or even better cbn [F].
For example in this case simp [ordering_mplus] goes a bit far and evaluates up to:

(match b with
| Ordering.eq =>
match c with
| Ordering.eq => d
| x => c
| x => b) =
match
match b with
| Ordering.eq => c
| x => b with
| Ordering.eq => d
| x =>
match b with
| Ordering.eq => c
| x => b


where I would have preferred it evaluated to:

ordering_mplus b (ordering_mplus c d) =
ordering_mplus (ordering_mplus b c) d


Is there a tactic that does not evaluate so deeply
or a way to tell simp to not evaluate so deeply?

#### awalterschulze (Oct 30 2022 at 13:03):

Also if there is a notation used, how do we tell simp to evaluate that function. For example

instance:  Mul Ordering where
mul := ordering_mplus

theorem ordering_mul_assocy (a b c d: Ordering):
(a * b) * (c * d) =
(a * (b * c)) * d  := by
cases a
case lt => rfl
case gt => rfl
case eq =>
simp ?


#### awalterschulze (Nov 11 2022 at 07:59):

Also how does one do simp on a function that is notation like *?

#### Anne Baanen (Nov 11 2022 at 10:14):

Generally you have to figure out which instance is used in the notation and write e.g. simp [has_mul.mul, int.has_mul]

#### Eric Wieser (Nov 11 2022 at 19:31):

You can use simp [(*)]

#### awalterschulze (Nov 12 2022 at 16:37):

I don't think simp [(*)] works, it gave us a syntax error. Maybe this works in lean3? but we are using lean4.

#### awalterschulze (Nov 12 2022 at 16:37):

Also is there a way to search for the instance of the notation, something like a Locate "<" command in Coq?

#### awalterschulze (Nov 12 2022 at 17:16):

Is there a way to do the same as simp [(*)] in lean4?

#### Mario Carneiro (Nov 12 2022 at 19:35):

you should be able to control-click on the *

#### Matt Diamond (Nov 12 2022 at 20:21):

Is there a tactic that does not evaluate so deeply

does Lean 4 have simp only? in Lean 3 you can use that to restrict the simplifications performed

#### Matt Diamond (Nov 12 2022 at 20:23):

I don't know if Lean 4 has simp_rw but that tactic is basically equivalent to simp only and is very useful in Lean 3

yes?

#### Matt Diamond (Nov 12 2022 at 21:08):

I was just thinking that it might be what @awalterschulze was looking for... simp_rw F or simp only [F] instead of simp [F] (or maybe dsimp/dsimp only)

but I only know what's available in Lean 3

Last updated: Dec 20 2023 at 11:08 UTC