In my proof, I use the `simpl.`

tactic to simplify a hypothesis. Unfortunately, the simplified form that I want has the expression

`if i mod 2 =? 1 then a (i / 2) else b (i / 2)`

in it, but when I simplify, I get

```
if
match snd (Nat.divmod i 1 0 1) with
| 0 => 1
| S _ => 0
end =? 1
then
a (fst (Nat.divmod tree_idx 1 0 1))
else
b (fst (Nat.divmod tree_idx 1 0 1))
```

It seems like it simplified the `mod`

and the division when I didn't want it to. Is there a way to stop it from doing this?

I also tried `unfold`

, but ran into the issue here. `unfold MyDef in h. fold MyDef in h.`

works, but feels like a kludge.

Instead of `simpl`

, `cbn - [Nat.modulo]`

To read more about it: https://coq.inria.fr/distrib/current/refman/proofs/writing-proofs/equality.html?highlight=cbn#applying-conversion-rules

Last updated: Jun 15 2024 at 08:01 UTC