Zulip Chat Archive

Stream: general

Topic: exposing eq compiler def


view this post on Zulip Chris B (Oct 15 2020 at 14:09):

Why can't I unfold this equation compiler definition (it only fails in the _ catch-all case)?

def isA : char -> bool
| 'a' := tt
| _ := ff

example : isA 'z' = ff :=
begin
  -- simplify tactic failed to simplify
  --unfold isA,
  -- simplify tactic failed to simplify
  --simp only [isA],
  sorry
end

The definition isA._main unfolds to λ (a : char), ite (a = 'a') (id_rhs bool tt) (id_rhs bool ff) which seems to work fine even when it's behind a definition not marked reducible:

def isA' := λ (a : char), ite (a = 'a') (id_rhs bool tt) (id_rhs bool ff)
def isA'.main := isA'

example : isA'.main 'z' = ff :=
begin
  unfold isA'.main,
  unfold isA',
  refl,
end

example : isA'.main 'z' = ff :=
begin
  simp only [isA'.main, isA'],
  refl,
end

view this post on Zulip Reid Barton (Oct 15 2020 at 14:14):

The equational lemma for isA has a hypothesis ¬ ('z' = 'a') which simp doesn't know how to discharge

view this post on Zulip Reid Barton (Oct 15 2020 at 14:15):

If you just want to replace isA by its definition, you can use delta isA

view this post on Zulip Reid Barton (Oct 15 2020 at 14:20):

actually, even if I pass a proof of ¬ ('z' = 'a') to simp as well, it still doesn't want to apply the equational lemma, which I don't understand

view this post on Zulip Chris B (Oct 15 2020 at 14:21):

simpa works as well.

view this post on Zulip Reid Barton (Oct 15 2020 at 14:22):

That's because the theorem is true by refl

view this post on Zulip Chris B (Oct 15 2020 at 14:22):

I didn't think to look at the equational lemmas though after I saw the ite main function, so thank you for that (and the delta suggestion).

view this post on Zulip Reid Barton (Oct 15 2020 at 14:22):

heh, looks like my guess about the failure was wrong. Try turning on trace.simplify

view this post on Zulip Reid Barton (Oct 15 2020 at 14:22):

simp knows how to reduce 'z' = 'a' to false but it doesn't know how to prove ¬false

view this post on Zulip Reid Barton (Oct 15 2020 at 14:24):

This works, but seems very silly:

def isA : char -> bool
| 'a' := tt
| _ := ff

lemma not_false_iff_true : (¬ false)  true := sorry

example : isA 'z' = ff :=
begin
  have : ¬ 'z' = 'a' := sorry,
  simp only [isA, this, not_false_iff_true],
end

view this post on Zulip Chris B (Oct 15 2020 at 14:24):

Mine says

[simplify.failure] proof stuck at: ¬'z' = 'a'
[simplify.failure] failed to prove: ?x_1 : ¬'z' = 'a'

but I'm on an older mathlib

view this post on Zulip Reid Barton (Oct 15 2020 at 14:25):

Maybe my trace was with ¬ 'z' = 'a' included as an argument, I'm not sure

view this post on Zulip Chris B (Oct 15 2020 at 14:26):

Do you know if that inequality in the equational lemma plus the ite in _main means this does two checks when it's evaluating?

view this post on Zulip Reid Barton (Oct 15 2020 at 14:26):

Well, simp doesn't "evaluate"--I don't know what you mean

view this post on Zulip Reid Barton (Oct 15 2020 at 14:27):

but I think the answer is no

view this post on Zulip Chris B (Oct 15 2020 at 14:27):

Just if somewhere else, in a lean program you computed isA c for some character.

view this post on Zulip Reid Barton (Oct 15 2020 at 14:27):

This has nothing to do with lemmas of any kind

view this post on Zulip Chris B (Oct 15 2020 at 14:28):

Oh word, you're right.

view this post on Zulip Reid Barton (Oct 15 2020 at 14:29):

I'm not sure whether the compiler works on the equations directly or on the output of the equation compiler, but either way there should be only one test

view this post on Zulip Reid Barton (Oct 15 2020 at 14:30):

(by the output of the equation compiler, I mean the defs: def isA : char → bool := isA._main, def isA._main : char → bool := λ (a : char), ite (a = 'a') (id_rhs bool tt) (id_rhs bool ff))

view this post on Zulip Chris B (Oct 15 2020 at 14:35):

It's early, for some reason I was reading the equational lemmas like they were the match discriminator instead of just lemmas.
Thanks for helping me figure this out.

view this post on Zulip Reid Barton (Oct 15 2020 at 14:36):

Interestingly this has nothing to do with char--I get the same behavior with nat

view this post on Zulip Chris B (Oct 15 2020 at 14:55):

In hindsight I guess it makes sense that the extra hypothesis would be there for any patterns that aren't just applications of a constructor.


Last updated: May 18 2021 at 16:25 UTC