Zulip Chat Archive

Stream: general

Topic: unfolding definitions


view this post on Zulip Guy Leroy (Aug 22 2018 at 11:33):

I have the following def:

def jacobi_sym :     
| a          1 := 1
| a          b := if b % 2 = 1 then jacobi_sym_aux a b else 0

local notation {a|b} := jacobi_sym a b

and I am trying to prove

h : ¬n = 1
 {a|n} = ite (quadratic_res a n  ¬n  a) 1 (ite (¬quadratic_res a n) (-1) 0)

How can I unfold jacoby_sym such that it shows if b % 2 = 1 then jacobi_sym_aux a b else 0 ?
If I write unfold jacobi_sym the tactic fails

view this post on Zulip Kenny Lau (Aug 22 2018 at 11:37):

MWE please

view this post on Zulip Kenny Lau (Aug 22 2018 at 11:40):

but rw [jacobi_sym.equations._eqn_2 a n h] should work

view this post on Zulip Kenny Lau (Aug 22 2018 at 11:44):

but a better solution would be to not use the equation compiler to define jacobi_sym, but rather use ite

view this post on Zulip Guy Leroy (Aug 22 2018 at 11:48):

Thank you very much!

view this post on Zulip Simon Hudon (Aug 22 2018 at 15:10):

Out of curiosity, have you tried dunfold? It is based on dsimp which is more careful about preserving definitional equality.


Last updated: May 12 2021 at 05:19 UTC