Bolton Bailey (Jun 02 2022 at 18:53): Bolton Bailey (Jun 02 2022 at 18:53):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?
Bolton Bailey (Jun 02 2022 at 19:00):I also tried unfold, but ran into the issue here. unfold MyDef in h. fold MyDef in h. works, but feels like a kludge.
Li-yao (Jun 02 2022 at 19:24):Instead of simpl, cbn - [Nat.modulo]
Li-yao (Jun 02 2022 at 19:25):To read more about it: https://coq.inria.fr/distrib/current/refman/proofs/writing-proofs/equality.html?highlight=cbn#applying-conversion-rules
Last updated: Oct 13 2024 at 01:02 UTC