Stream: Coq users

Topic: ✔ eliminate match in goal

Ricardo (Jan 25 2022 at 23:01):

Hey all, I'm following the Logical Foundations book. In an exercise of the second chapter, I get the goal of a proof into the following state.

nat_to_bin (bin_to_nat c) =
  match
    nat_to_bin (bin_to_nat c)
  with
  | Z | _ =>
      nat_to_bin (bin_to_nat c)
  end

Why is cbn or simpl not able to simplify the match? Is there a tactic that would transform the left-hand side of the equality into nat_to_bin (bin_to_nat c)?

Guillaume Melquiond (Jan 26 2022 at 05:36):

cbn and simpl perform computations, but in your case, there is nothing left to compute, since c is an abstract term (I suppose). What you can do is a case analysis on the matched term: destruct (nat_to_bin (bin_to_nat c)).

Ricardo (Jan 26 2022 at 06:02):

Thank you! That worked :smile:

Notification Bot (Jan 27 2022 at 06:30):

Ricardo has marked this topic as resolved.

Last updated: Oct 03 2023 at 02:34 UTC