Coq cbn simpl

Stream: new members

[awalterschulze]

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]

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]

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]

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]

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]

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

[Anne Baanen]

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]

You can use simp [(*)]

[awalterschulze]

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

[awalterschulze]

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

[awalterschulze]

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

[Mario Carneiro]

you should be able to control-click on the *

[Matt Diamond]

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]

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]

yes?

[Matt Diamond]

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