## Stream: general

### Topic: unfolding definitions

#### 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

#### Kenny Lau (Aug 22 2018 at 11:40):

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

#### 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

#### Guy Leroy (Aug 22 2018 at 11:48):

Thank you very much!

#### 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