Zulip Chat Archive

Stream: new members

Topic: equation compiler failed to prove equation lemma


view this post on Zulip Horatiu Cheval (Feb 20 2021 at 10:36):

Sorry for the long example, I didn't manage to further isolate the problem.
I get equation compiler failed to prove equation lemma when defining match_lcase, but I don't see what's wrong with this recursion. What's happening?

inductive type
| zero : type
| comp : type  type  type

infixr `>>` : 50 := type.comp

inductive var (τ : type)
| mk :   var

inductive term : type  Type
| app :  {τ σ : type}, term (σ.comp τ)  term σ  term τ
| const :  {τ : type}, term τ
| S :  {ρ τ σ : type}, term $ (τ >> σ >> ρ) >> (τ >> σ) >> τ >> ρ

open term
inductive lcase :  {σ τ : type}, var σ  term τ  Type
| mk_const :  {σ τ : type} {x : var σ} {t : term τ}, lcase x t
| mk_app :  {ρ σ τ : type} {x : var ρ} {u : term (σ.comp τ)} {v : term σ},
    lcase x u  lcase x v  lcase x (u.app v)

@[simp]
def match_lcase :  {σ τ : type} {x : var σ} {t : term τ}, lcase x t  term (σ >> τ)
| σ τ x t (lcase.mk_const) := @const (σ >> τ)
| σ τ x t (lcase.mk_app lu lv) := (S.app $ match_lcase lu).app $ match_lcase lv

Last updated: May 16 2021 at 21:11 UTC