Zulip Chat Archive

Stream: new members

Topic: reduce goal


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

view this post on Zulip Thorsten Altenkirch (Sep 05 2020 at 14:08):


view this post on Zulip Thorsten Altenkirch (Sep 05 2020 at 14:11):

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

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

view this post on Zulip Thorsten Altenkirch (Sep 05 2020 at 14:35):

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

view this post on Zulip Thorsten Altenkirch (Sep 05 2020 at 14:35):

thank you

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

view this post on Zulip Kevin Buzzard (Sep 05 2020 at 14:51):

split_ifs will get rid of the if then else

view this post on Zulip Kevin Buzzard (Sep 05 2020 at 14:52):

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

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

view this post on Zulip Shing Tak Lam (Sep 05 2020 at 15:08):

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

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

view this post on Zulip Thorsten Altenkirch (Sep 05 2020 at 15:11):

I never used ff.

view this post on Zulip 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: May 15 2021 at 00:39 UTC