## 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 γ) :=

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 contexts depend on precontexts is that, for example, the definition of App in term (function application) allows the function and argument to have different contexts, i.e. different mults per tp, but they must have the same precontext, i.e. the same list of tps. This way, terms are correct-by-construction, meaning it's impossible to construct a term of an invalid embedded type (tp). Similarly, terms depend on contexts, 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