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