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.
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: Feb 01 2023 at 13:03 UTC