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