Failing to prove equational lemma

[leodemoura]

@gebner Commit bcf44f7 introduced a bug in the equation compiler. The failure happens when we are proving equational lemmas. Here is a minimal example:

inductive type
| bool : type
| fn : list type → type → type

def f : type → nat
| (type.bool)       := 0
| (type.fn args rt) := 1

This is based on a definition from the smt2_interface package. AFAICT, this problem happens because the prove_eq_rec_invertible procedure is expecting terms that were built using process_transport, but we don't use process_transport anymore because we are using the "user-facing" cases_on recursors produced by the inductive compiler. The inductive compiler uses something similar to the "transport" operation, but it is not identical. Thus, prove_eq_rec_invertible fails. It is not clear what is the ideal solution is here. I don't want to rely on how the inductive_compiler generates the "user facing" cases_on recursor in the equation compiler. The best solution I can think of is: generate equational lemmas for the "user facing" cases_on recursors in the inductive compiler, and use them when proving equational lemmas. @dselsam and I considered this solution, but decided to use the process_transport approach because it was simpler, and we did not have to agree on how the cases_on equational lemmas looked like. Any ideas?

That being said, I'm not looking forward to implement this change :) I bet @dselsam will not be very excited either. So, I will just revert bcf44f7 for now, and leave this issue open.

[leodemoura]

Remark: we were also planning to use bcf44f7 to fix #1518 .

[gebner]

Damn, it was too good to be true... In any case, we should add this example as a test case (ok, just saw that you already added in the commit).

@leodemoura At least in this example, the new terms in prove_eq_rec_invertible are almost the ones we expect. This is the lhs:

@eq.rec.{1 1} _nest_1_1.list.type (type.pack_1_0 (type.unpack_1_0 (type.pack_1_0 args)))
  (λ (a : _nest_1_1.list.type), (λ (a : type), nat) (_nest_1_1.type.fn a rt))
  ((λ (a_1 : list.{0} type) (a_2 : type), id_rhs.{1} nat (@has_one.one.{0} nat nat.has_one))
     (type.unpack_1_0 (type.pack_1_0 args))
     rt)
  (type.pack_1_0 args)
  (type.pack_unpack_1_0 (type.pack_1_0 args))

The only difference is that the minor hypothesis is (fun x _, ...) (unpack (pack a)) dummy instead of (fun x, ..) (unpack (pack a)).

[gebner]

Converting (fun x _, ...) (unpack (pack a)) dummy to (fun x, ..) (unpack (pack a)) fixes this equation lemma.

It works in all tests, except for the non_exhaustive_error.lean test, here it fails because the minor hypothesis is the other way around?!?

const_name._main (term.mk n (@list.nil.{0} term)) ~~>
@eq.rec.{1 1} _nest_1_1.list.term (term.pack_0_1 (term.unpack_0_1 (term.pack_0_1 (@list.nil.{0} term))))
  (λ (a : _nest_1_1.list.term), (λ (a : term), nat) (_nest_1_1.term.mk n a))
  ((λ (a_1 : nat) (a_2 : list.{0} term),
      @list.cases_on.{1 0} term (λ (a_2 : list.{0} term), nat) a_2 (id_rhs.{1} nat a_1)
        (λ (a : term) (a_3 : list.{0} term),
           term.cases_on.{1} (λ (a : term), nat) a (λ (a_2 : nat) (a_4 : list.{0} term), ⁇)))
     n -- HERE: exactly the other way around...
     (term.unpack_0_1 (term.pack_0_1 (@list.nil.{0} term))))
  (term.pack_0_1 (@list.nil.{0} term))
  (term.pack_unpack_0_1 (term.pack_0_1 (@list.nil.{0} term))) = n

[gebner]

here it fails because the minor hypothesis is the other way around?!?

Just for the record, the arguments of the minor premise of the innermost eq.rec in the cases_on construction correspond to the arguments of the introduction rule. I don't think we can easily fix the current approach, since there can be multiple nested arguments.

I don't want to rely on how the inductive_compiler generates the "user facing" cases_on recursor in the equation compiler.

I agree, this seems very brittle.

The best solution I can think of is: generate equational lemmas for the "user facing" cases_on recursors in the inductive compiler, and use them when proving equational lemmas. [..] we did not have to agree on how the cases_on equational lemmas looked like.

I don't see any easier solution. Are there multiple possible lemmas for cases_on?

[leodemoura]

I don't see any easier solution. Are there multiple possible lemmas for cases_on?

Yes, we would have to generate one for each constructor.

[gebner]

@leodemoura I understand that. I was referring to the "we did not have to agree on how the cases_on equational lemmas looked like."

[leodemoura]

@leodemoura I understand that. I was referring to the "we did not have to agree on how the cases_on equational lemmas looked like."

@gebner I see. This comment is just a minor thing. It is just a matter of making sure the arguments for the lemmas have a well defined order, and we have a well defined mechanism for retrieving them (e.g., use a naming convention like we do for equational lemmas; or store them in a new environment extension).