# Zulip Chat Archive

## Stream: new members

### Topic: Cryptic errors

#### Wojciech Nawrocki (Feb 11 2019 at 23:28):

I came across this cryptic-sounding error when trying to execute `cases`

on a particular inductive type:

cases tactic failed, unsupported equality between type and constructor indices (only equalities between constructors and/or variables are supported, try cases on the indices): zeros _x = context.add r₁_Γ (r₁_π • r₁_Γ')

Does anyone know what this means?

Also here's an irrelevant, but fun-looking error (it seems Lean got stuck in a loop for a bit?):

https://pastebin.com/779LZsf1

#### Kenny Lau (Feb 11 2019 at 23:29):

It means you want `cases`

to unify some expression that is not a local constant with some other expression that is not a local constant

#### Wojciech Nawrocki (Feb 12 2019 at 13:57):

What do you mean by "local constant" here? I've split the "zeros _x" into a constant by doing a `cases`

of a different variable first, but the error is still the same, trying to prove `nil = context.add r₁_Γ (r₁_π • r₁_Γ')`

.

#### Kevin Buzzard (Feb 12 2019 at 14:36):

Can you post code?

#### Wojciech Nawrocki (Feb 12 2019 at 14:45):

Yep, it arises on this line. It does seem like Lean is trying to automatically prove a propositional equality, which I should do manually, I'm just unsure how to do it with `cases`

- I suppose using `cases_on`

is the way to do it?

#### Kevin Buzzard (Feb 12 2019 at 14:51):

Oh, I mean code that we can run (there's some `import matrix`

line). But maybe this already helps.

#### Kevin Buzzard (Feb 12 2019 at 14:52):

I can't work out the type of anything unless I can run the code, basically.

#### Kevin Buzzard (Feb 12 2019 at 14:53):

you're doing `cases r\1`

. What is the type of r\1?

#### Mario Carneiro (Feb 12 2019 at 15:01):

minimized:

import tactic.ring import algebra run_cmd mk_simp_attr `sop_form [`simp] run_cmd mk_simp_attr `unfold_ [`simp] @[derive decidable_eq] inductive mult: Type namespace mult instance : has_zero mult := sorry instance : has_one mult := sorry instance : has_add mult := sorry instance : has_mul mult := sorry end mult inductive tp: Type | nat: tp | bool: tp | fn: mult → tp → tp → tp notation `⟦`π`⬝`T`⟧⊸`U:90 := tp.fn π T U def precontext := list tp inductive context: precontext → Type | nil: context [] -- You have a dependent pi (n) after a recursive arg (_ : context ns) -- and Lean doesn't like this. | cons {Γ: precontext} (π: mult) (T: tp): context Γ → context (T::Γ) notation `⟦`π`⬝`T`⟧::`Γ:90 := context.cons π T Γ namespace context def zeros: Π γ, context γ | [] := nil | (T::δ) := ⟦0⬝T⟧::(zeros δ) instance {γ: precontext} : has_zero (context γ) := ⟨zeros γ⟩ protected def add: Π {γ}, context γ → context γ → context γ | _ nil nil := nil | _ (⟦π₁⬝T⟧::Γ₁) (⟦π₂⬝.(T)⟧::Γ₂) := ⟦(π₁+π₂)⬝T⟧::(add Γ₁ Γ₂) instance {γ: precontext} : has_add (context γ) := ⟨context.add⟩ protected def smul: Π {γ}, mult → context γ → context γ | _ π nil := nil | _ π (⟦π'⬝T⟧::Γ) := ⟦(π*π')⬝T⟧::(smul π Γ) instance {γ: precontext} : has_scalar mult (context γ) := ⟨context.smul⟩ end context /- Introduces matrices and horrifying linear algebra. -/ open context inductive term: Π {γ}, context γ → tp → Type | Nat (n: ℕ): Π {γ}, -------------------------- term (0: context γ) tp.nat | Bool (b: bool): Π {γ}, --------------------------- term (0: context γ) tp.bool | App: Π {γ: precontext} {Γ Γ': context γ} {T U: tp} {π: mult}, term Γ ⟦π⬝T⟧⊸U → term Γ' T ---------------------- → term (Γ + π•Γ') U open term -- preservation proven by construction inductive reduces: ∀ {γ} {Γ: context γ} {T: tp}, term Γ T → term Γ T → Prop | AppEtaLeft: ∀ {γ} {Γ Γ': context γ} {T U: tp} {π: mult} {fn fn': term Γ ⟦π⬝T⟧⊸U} {arg: term Γ' T}, reduces fn fn' ---------------------------------- → reduces (App fn arg) (App fn' arg) open reduces set_option pp.implicit true lemma diamond_property: ∀ {γ} {Γ: context γ} {T: tp} {e e₁ e₂: term Γ T}, reduces e e₁ → reduces e e₂ ------------------------------ → ∃ e', reduces e₁ e' ∧ reduces e₂ e' /- TODO cases r₁ fails almost everywhere -/ | γ _ _ (Nat n) e₁ e₂ r₁ r₂ := by { cases γ, cases r₁, } | _ _ _ (Bool b) _ _ r₁ _ := by { sorry } | _ _ T (@App γ' Γ' Γ'' T' U' π' fn arg) e₁ e₂ r₁ r₂ := by { sorry }

#### Mario Carneiro (Feb 12 2019 at 15:07):

The type of `r₁`

is `@reduces (@list.nil tp) 0 tp.nat (@Nat n (@list.nil tp)) e₁`

before the cases. In the cases we try to match it against the `AppEtaLeft`

constructor, which has type `@reduces γ (Γ + π • Γ') U (@App γ Γ Γ' T U π fn arg) (@App γ Γ Γ' T U π fn' arg)`

. This involves matching `(@list.nil tp) = γ`

(no problem), `0 = Γ + π • Γ'`

(big problem), `tp.nat = U`

(no problem), before we get to `(@Nat n (@list.nil tp)) = (@App γ Γ Γ' T U π fn arg)`

(ill typed)

#### Mario Carneiro (Feb 12 2019 at 15:08):

The reason `0 = Γ + π • Γ'`

is problematic is because the lhs is a constructor (okay) and the rhs is a function, namely `add`

which is not a constructor. `cases`

doesn't know what to do with this

#### Mario Carneiro (Feb 12 2019 at 15:12):

I'm looking at this definition.

def precontext := list tp inductive context: precontext → Type | nil: context [] -- You have a dependent pi (n) after a recursive arg (_ : context ns) -- and Lean doesn't like this. | cons {Γ: precontext} (π: mult) (T: tp): context Γ → context (T::Γ)

I think you want `context`

to be nondependent. You aren't really using the precontext in the definition - a context is only a list of `mult * tp`

pairs of the same length as the precontext. I would suggest using a well formedness property to express this

#### Mario Carneiro (Feb 12 2019 at 15:14):

Same for `term`

, maybe even more so. A dependent type of terms will lead only to weeping and gnashing of teeth

#### Wojciech Nawrocki (Feb 12 2019 at 15:37):

First of all, thanks a lot! I was just trying to conjure up an artificial example that people could run, but your minimization works better (and TIL about `pp.implicit`

).

On the topic of `cases`

:

As you rightly mentioned, `(@Nat n (@list.nil tp)) = (@App γ Γ Γ' T U π fn arg)`

is ill-typed. What I wanted `cases`

to do in the first place was to simply discharge the cases of `Nat n`

as absurd using this condition (and similar ones for `AppEtaRight`

et al). Do you think it would be possible to modify `cases`

so that it checks for impossible conditions such as this first? That way, even if it runs into something it can't unify such as `0 = Γ + π • Γ'`

, it wouldn't matter as the case cannot occur anyway. It is true that all of `Γ Γ' π`

are used in the ill-typed expression, but `@Nat .. = @App ..`

is ill-typed regardless of argument values.

Alternatively, could the `cases`

tactic simply generate a `0 = Γ + π • Γ'`

goal? Is there a tactic which already does this?

On the dependency of `context`

/`term`

:

This is essentially a strongly-typed representation of a particular lambda calculus, as described e.g. here. The reason why `context`

s depend on `precontext`

s is that, for example, the definition of `App`

in `term`

(function application) allows the function and argument to have different `context`

s, i.e. different `mult`

s per `tp`

, but they must have the same `precontext`

, i.e. the same list of `tp`

s. This way, terms are correct-by-construction, meaning it's impossible to construct a `term`

of an invalid embedded type (`tp`

). Similarly, `term`

s depend on `context`

s, making the definition of `reduces`

trivially uphold the type-preservation property of the described calculus. By "well formedness property", do you mean something that could achieve the same without messing with dependent types?

#### Mario Carneiro (Feb 12 2019 at 15:41):

As you rightly mentioned, (@Nat n (@list.nil tp)) = (@App γ Γ Γ' T U π fn arg)is ill-typed. What I wanted cases to do in the first place was to simply discharge the cases of Nat n as absurd using this condition (and similar ones for AppEtaRight et al). Do you think it would be possible to modify cases so that it checks for impossible conditions such as this first?

That's exactly what it was trying to do. But it never got that far - you can't prove two different constructors are distinct if the proof of distinctness is not even type correct

#### Mario Carneiro (Feb 12 2019 at 15:43):

Alternatively, could the cases tactic simply generate a 0 = Γ + π • Γ' goal? Is there a tactic which already does this?

I wish it did this; `cases`

failing is a kind of messy solution. You can actually capture the error state and attempt to proceed from there, but I don't recommend it. The failure of the equality to be discharged means all later equalities are heterogeneous, which makes them that much harder to work with

#### Mario Carneiro (Feb 12 2019 at 15:46):

In the Coq paper, it is important that all the terms that appear in dependent arguments are constructors. That's what makes them pattern match nicely. You are using `Γ + π • Γ'`

in a dependent argument, which will cause many problems

#### Mario Carneiro (Feb 12 2019 at 15:46):

see the top of p. 7

#### Mario Carneiro (Feb 12 2019 at 15:48):

By "well formedness property", do you mean something that could achieve the same without messing with dependent types?

Yes. The idea is to have two definitions: a weakly typed type of terms, which is really just the syntax of the expressions, and an inductive typechecking relation

#### Mario Carneiro (Feb 12 2019 at 15:50):

The real reason `App`

is badly typed is that you can't really change it out for anything else, even if `Γ + π • Γ' = Γ2 + π • Γ'2`

#### Mario Carneiro (Feb 12 2019 at 15:52):

One way to fix this problem without an overhaul is to give `app`

the type

| App: Π {γ: precontext} {Γ Γ' Γ'' : context γ} {T U: tp} {π: mult}, term Γ ⟦π⬝T⟧⊸U → term Γ' T → Γ'' = Γ + π•Γ' ---------------------- → term Γ'' U

#### Mario Carneiro (Feb 12 2019 at 15:53):

This way `Γ''`

is free to be whatever the context needs it to be, and you get an equality hypothesis out instead

#### Wojciech Nawrocki (Feb 13 2019 at 01:08):

That's exactly what it was trying to do. But it never got that far - you can't prove two different constructors are distinct if the proof of distinctness is not even type correct

If this makes any sense, is there a type theory which could admit a statement of the form, informally, "regardless of the types of LHS and RHS, an equality cannot be constructed since the sides use different constructors"?

Last updated: May 11 2021 at 22:14 UTC