Stream: general

Topic: exposing eq compiler def

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


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

Reid Barton (Oct 15 2020 at 14:15):

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

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

Chris B (Oct 15 2020 at 14:21):

simpa works as well.

Reid Barton (Oct 15 2020 at 14:22):

That's because the theorem is true by refl

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

Reid Barton (Oct 15 2020 at 14:22):

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

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

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


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

Reid Barton (Oct 15 2020 at 14:25):

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

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?

Reid Barton (Oct 15 2020 at 14:26):

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

Reid Barton (Oct 15 2020 at 14:27):

but I think the answer is no

Chris B (Oct 15 2020 at 14:27):

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

Reid Barton (Oct 15 2020 at 14:27):

This has nothing to do with lemmas of any kind

Chris B (Oct 15 2020 at 14:28):

Oh word, you're right.

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

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

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.

Reid Barton (Oct 15 2020 at 14:36):

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

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