exposing eq compiler def

Stream: general

[Chris B]

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]

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

[Reid Barton]

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

[Reid Barton]

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]

simpa works as well.

[Reid Barton]

That's because the theorem is true by refl

[Chris B]

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]

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

[Reid Barton]

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

[Reid Barton]

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]

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]

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

[Chris B]

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]

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

[Reid Barton]

but I think the answer is no

[Chris B]

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

[Reid Barton]

This has nothing to do with lemmas of any kind

[Chris B]

Oh word, you're right.

[Reid Barton]

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]

(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]

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]

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

[Chris B]

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.