## Stream: new members

### Topic: equation compiler failed to prove equation lemma

#### 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: Dec 20 2023 at 11:08 UTC