Stream: Coq users

Topic: simp only


view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip Li-yao (Jun 02 2022 at 19:24):

Instead of simpl, cbn - [Nat.modulo]

view this post on Zulip 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: Feb 01 2023 at 13:03 UTC