Inductive datatype definition failure

Stream: lean4

[bblaxill]

Hi, I'm trying to port some existing work from agda by someone else, as an exercise. I'm currently bumping into an issue with an inductive datatype definition that I believe should pass but does not (maybe I'm wrong?). It can be boiled down to this following example, where Foo1 and Foo2 pass, but Foo3 does not.

inductive Foo1 : Nat -> Nat -> Type where
| bar1 : ∀ (a b: Nat), (Foo1 a b × Foo1 a b) -> Foo1 a b

inductive Foo2 : Nat -> Nat -> Type where
| bar2 : ∀ (a b c: Nat), (Foo2 a b × Foo2 a b) -> Foo2 a b

-- The following fails with:
-- (kernel) invalid nested inductive datatype 'Prod', nested inductive datatypes parameters cannot contain local variables.
inductive Foo3 : Nat -> Nat -> Type where
| bar3 : ∀ (a b c: Nat), (Foo3 a c × Foo3 b c) -> Foo3 a c

Perhaps I am doing something trivially wrong and should not expect this to be accepted?

I posted an issue

[Andrés Goens]

why do you need this to be a product? if you write it as an arrow it seems to work (i.e. this works for me):

inductive Foo3 : Nat -> Nat -> Type where
| bar3 : ∀ (a b c: Nat), Foo3 a c -> Foo3 b c -> Foo3 a c

[bblaxill]

Unpacking is not possible in my real use case, the type is completely abstract.
Here is an example closer to my use case

def implication : (List Ty -> Type _) → (List Ty -> Type _) → (List Ty -> Type _)
| P , Q => fun x => P x → Q x
infix:50 " ⇒ " => implication

inductive Ty where
| unit : Ty
| lollipop : Ty -> Ty -> Ty
infix:50 " ⊸ " => Ty.lollipop

def ternaryRelate (a b c : List Ty): Prop := a ++ b = c

notation a " • " b " ≃ " c => ternaryRelate a b c

structure ProofRelevantSeparation
    (P Q : List Ty -> Type _) (a : List Ty) where
  al : A
  ar : A
  px : P a
  qx : Q a
  proof : al • ar ≃ a
notation a " ★ " b => ProofRelevantSeparation a b

-- The following fails with:
-- (kernel) invalid nested inductive datatype 'ProofRelevantSeparation', nested inductive datatypes parameters cannot contain local variables.
inductive Exp : Ty -> List Ty -> Type _ where
| app : forall x, (Exp (a ⊸ b) ★ Exp a ⇒ Exp b) x -> Exp b ctx

Here ProofRelevantSeparation is quantified over with 'x' and so cannot be unpacked (even if it could, my actual use case is more abstract)

[Mario Carneiro]

Lean only accepts nested inductives if it is sufficiently concrete that it could be unfolded, and it does the unfolding behind the scenes because it needs to use it to generate the recursor. Using an abstract type is definitely not allowed, and is also inconsistent in some cases

[Mario Carneiro]

I think there is a typo in your definition, A in the types of al and ar is not defined, maybe you meant List Ty?

[Mario Carneiro]

Even after inlining everything, I get this:

inductive Exp : Ty → List Ty → Type _ where
| app : forall x,
  (al : List Ty) →
  (ar : List Ty) →
  (proof : al • ar ≃ x) →
  (px : Exp (a ⊸ b) x) →
  (qx : Exp a x → Exp b x) →
  Exp b ctx

which is also invalid because Exp is not used strictly positively

[bblaxill]

Thanks for the response.

Mario Carneiro said:

I think there is a typo in your definition, A in the types of al and ar is not defined, maybe you meant List Ty?

Yes you are right that is a typo, but the error is the same.

[bblaxill]

Mario Carneiro said:

Even after inlining everything, I get this:

inductive Exp : Ty → List Ty → Type _ where
| app : forall x,
  (al : List Ty) →
  (ar : List Ty) →
  (proof : al • ar ≃ x) →
  (px : Exp (a ⊸ b) x) →
  (qx : Exp a x → Exp b x) →
  Exp b ctx

which is also invalid because Exp is not used strictly positively

Ah you're right, although perhaps a separate issue. I'm trying to port some Agda code, do you know if Agda has greater leniency regarding nested inductives? I've seen Agda code being more lenient when constructing fixpoint of inductives even when they are not strictly positive.

[Mario Carneiro]

Violating strict positivity is definitely a no-no. Currently you can prove that Exp is empty, but if you added enough constructors such that it could be proved to have at least two elements:

inductive Exp : Ty → List Ty → Type _ where
| app : forall x,
  (px : Exp (a ⊸ b) x) →
  (qx : Exp a x → Exp b x) →
  Exp b ctx
| zero : Exp a x
| one : Exp a x

you get something which is definitely inconsistent, because (T -> T) injects into T

[bblaxill]

I'm not sure that inlining is correct, or perhaps my notation is incorrect. The ProofRelevantSeparation should be on Exp (a ⊸ b) and Exp a x , Exp b x being after the implication arrow

[Mario Carneiro]

import Mathlib.Logic.Function.Basic
import Mathlib.Tactic.Classical

def implication : (List Ty -> Type _) → (List Ty -> Type _) → (List Ty -> Type _)
| P , Q => fun x => P x → Q x
infix:50 " ⇒ " => implication

inductive Ty where
| unit : Ty
| lollipop : Ty -> Ty -> Ty
infix:50 " ⊸ " => Ty.lollipop

unsafe inductive Exp : Ty → List Ty → Type _ where
| app : forall x,
  (px : Exp (a ⊸ b) x) →
  (qx : Exp a x → Exp b x) →
  Exp b ctx
| zero : Exp a x
| one : Exp a x

unsafe example : False := by
  classical
  let F (f : Exp Ty.unit [] → Exp Ty.unit []) : Exp Ty.unit [] :=
    .app _ .zero f
  have F_inj {x y} (h : F x = F y) : x = y := by cases h; rfl
  let G (p : Prop) : Exp Ty.unit [] := if p then .zero else .one
  have G_inj {x y} : G x = G y → x = y := by simp; split <;> split <;> simp_all
  apply Function.cantor_injective fun P => F (G ∘ P)
  intro P Q h; funext a; exact G_inj (congrFun (F_inj h) a)

[Mario Carneiro]

I'm fairly sure the inlining is correct, but it's possible there were issues in the original statement?

[Mario Carneiro]

I think maybe you might have meant

inductive Exp : Ty -> List Ty -> Type _ where
| app : forall x, (Exp (a ⊸ b) ★ Exp a) x -> Exp b ctx

if the intent is to act like function application

[Mario Carneiro]

If I make that modification I get

inductive Exp : Ty → List Ty → Type _ where
| app : forall x,
  (al : List Ty) →
  (ar : List Ty) →
  (proof : al • ar ≃ x) →
  (px : Exp (a ⊸ b) x) →
  (qx : Exp a x) →
  Exp b ctx

for the inlined form, and this does satisfy strict positivity and is accepted by lean

[Mario Carneiro]

(it still looks wrong because the ctx at the end is not used anywhere else, but possibly this is an artifact of minimizing)

[bblaxill]

Mario Carneiro said:

I think maybe you might have meant

inductive Exp : Ty -> List Ty -> Type _ where
| app : forall x, (Exp (a ⊸ b) ★ Exp a) x -> Exp b ctx

if the intent is to act like function application

Thanks, I think you have solved my problem. My translation from the Agda was not correct.

I'm curious about the original Foo3 tuple example- I would have expected Foo2 to also fail, but I admit I have no intuition for what is happening.

[James Gallicchio]

I'm guessing Foo3 should probably succeed, but the nested inductive compiler is a bit conservative there for simplicity.

[bblaxill]

It's unfortunate that

inductive Exp : Ty -> List Ty -> Type _ where
| app : forall x, (Exp (a ⊸ b) ★ Exp a) x -> Exp b ctx

is not accepted but the inlined version is. If I learn how to extend the elaborator would it be possible to enable this without inlining for my specific case? Or perhaps it is not possible because the check is in the kernel and there is no way to enable this without inlining. It's a syntactic issue of course but I'd very much prefer to avoid extra (un)packing even if it requires me to do additional work with e.g. the elaborator. Thanks!

[Mario Carneiro]

it is the latter, any extensions here have to be performed in the kernel and complicate any metatheory or soundness proofs for the system

[Mario Carneiro]

also, have you thought about what the Exp.rec function would even look like?

[bblaxill]

I hadn't thought about it, but yes I can see there is an issue there. So is it correct to say Agda accepts these definitions because Agda pattern matching is a primitive of the language and doesnt elaborate pattern matching based on induction principles? I have come to theorem proving via non-academic route and am still trying to understand various fundamental concepts. thanks

[Mario Carneiro]

I'm not sure I would say that is an intentional consequence of the design decision, but it is certainly easier to accidentally allow unsound things when you have no conservative core language and just check everything directly in the frontend