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)`

?

`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)).`

Thank you! That worked :smile:

Ricardo has marked this topic as resolved.

Last updated: Oct 03 2023 at 02:34 UTC