## Stream: new members

### Topic: reduce goal

#### Thorsten Altenkirch (Sep 05 2020 at 14:08):

When I have a goal, e.g.

case nat.succ
n : ℕ
⊢ bin2nat (nat2bin (succ n)) = succ n


how can I see a reduced version of the goal? (nat2bin (such n)) reduces and then bin2nat reduces.

#### Thorsten Altenkirch (Sep 05 2020 at 14:08):




#### Thorsten Altenkirch (Sep 05 2020 at 14:11):

In particular I want to apply rewrite to the reduced goal.

#### Patrick Massot (Sep 05 2020 at 14:18):

Probably dsimp [bin2nat, nat2bin], but it would be easier to answer if you had provided a #mwe.

#### Thorsten Altenkirch (Sep 05 2020 at 14:35):

seems you found it easy enough to answer without a #mwe

thank you

#### Thorsten Altenkirch (Sep 05 2020 at 14:50):

Actually this reduces functions I have defined but now I have used if-then-else which ends up with

⊢ natpos2bin (ite ↥ff (2 * binpos2nat bs' + 1) (2 * binpos2nat bs')) = bsuccpos (ext bs' ff)


If I reduce its I get some more crap.

Here is my file.
binary.lean

#### Kevin Buzzard (Sep 05 2020 at 14:51):

split_ifs will get rid of the if then else

#### Kevin Buzzard (Sep 05 2020 at 14:52):

Alternatively you can use if_neg because the thing you're iffing is false

#### Thorsten Altenkirch (Sep 05 2020 at 15:06):

Actually how do I use if_neg.?
I have a goal

⊢ nat2bin (ite ↥ff (2 * binpos2nat bs' + 1) (2 * binpos2nat bs')) = pos (ext bs' ff)


but if I say if_neg, it says you are stupid:

111:3: type mismatch at application
tactic.istep 111 2 111 2 if_neg
term
if_neg
has type
¬?m_1 → ∀ {α : Sort ?} {t e : α}, ite ?m_1 t e = e : Prop
but is expected to have type
tactic ?m_1 : Type ?


#### Shing Tak Lam (Sep 05 2020 at 15:08):

if_neg is a lemma, not a tactic, so rw if_neg (or something similar)

#### Kevin Buzzard (Sep 05 2020 at 15:09):

Well you are being a bit CS using this weird ff stuff -- what's wrong with false? You will need to rewrite it but I need to go and talk to my sister in law and I'm not sure the rewrite will work because of this ff business.

I never used ff.

#### Thorsten Altenkirch (Sep 05 2020 at 15:12):

I was wondering what your sister-in-law has to do with ff but I guess you were just indicating that you are going off-line. :-)

Last updated: Dec 20 2023 at 11:08 UTC