reduce goal

Stream: new members

[Thorsten Altenkirch]

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]

[Thorsten Altenkirch]

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

[Patrick Massot]

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

[Thorsten Altenkirch]

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

[Thorsten Altenkirch]

thank you

[Thorsten Altenkirch]

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]

split_ifs will get rid of the if then else

[Kevin Buzzard]

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

[Thorsten Altenkirch]

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]

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

[Kevin Buzzard]

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.

[Thorsten Altenkirch]

I never used ff.

[Thorsten Altenkirch]

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. :-)