Cryptic errors

Stream: new members

[Wojciech Nawrocki]

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]

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]

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]

Can you post code?

[Wojciech Nawrocki]

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]

Oh, I mean code that we can run (there's some import matrix line). But maybe this already helps.

[Kevin Buzzard]

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

[Kevin Buzzard]

you're doing cases r\1. What is the type of r\1?

[Mario Carneiro]

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]

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]

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]

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]

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

[Wojciech Nawrocki]

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]

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]

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]

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]

see the top of p. 7

[Mario Carneiro]

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]

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]

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]

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

[Wojciech Nawrocki]

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"?