# Zulip Chat Archive

## 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

#### Mario Carneiro (Nov 12 2022 at 20:48):

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