Deriving dependent type from inductive type constructor

Stream: lean4

[Carbon]

Hello! Very new to pure functional programming, and dependent types, so bear with me. I am trying to create a type that depends on the constructor as follows:

inductive ATest  : Nat → Type where
  | c (a : Nat)  : ATest  x
deriving Repr

def ATest_1 := (λ x => (ATest.c x  : ATest x)) 1

Ideally, I should have to just do:

def ATest_1 := ATest.c 1 -- Type is ATest 1

Can I improve on the definition of ATest, so I can achieve that?

[Chris Bailey]

I'm on my phone, but I think you just have a typo. The constructor should be c (a : Nat) : ATest a. You might want to turn off autoimplicits at this stage.

[Carbon]

This was intended to make it work, and not a typo. I am trying to match on the value after:

inductive ATestV1 : Nat → Type where
  | c (a : Nat) : ATestV1 a  -- Use 'a' instead of 'x' won't work, see later
deriving Repr

inductive ATestV2 : Nat → Type where
| c (a : Nat) : ATestV2 x -- This will work
deriving Repr

def ATestV1_1 := (λ x => (ATestV1.c x : ATestV1 x)) 1
def ATestV2_1 := (λ x => (ATestV2.c x : ATestV2 x)) 1


#eval match ATestV1_1 with | .c x => x -- Does not work
#eval match ATestV2_1 with | .c x => x -- This works

[Lucas Allen]

I'm not sure if this helps, but one thing you can do is this,

inductive ATestV3 : Type where
| c : Nat → ATestV3
deriving Repr

def ATestV3_1 := (λ x => (ATestV3.c x : ATestV3)) 1

#eval match ATestV3_1 with | .c x => x

[Marcus Rossel]

To @Chris Bailey 's point, I think you might be shooting yourself in the foot with Lean's "auto implicits" feature. You can turn this off with set_option autoImplicit false and see what happens:

inductive ATestV2 : Nat → Type where
  | c (a : Nat) : ATestV2 x

-- With auto implicits enabled (by default),
-- the definition of `ATestV2.c` contains an implicit argument 'x'
#check ATestV2.c -- ATestV2.c {x : Nat} (a : Nat) : ATestV2 x

set_option autoImplicit false

inductive ATestV2' : Nat → Type where
  | c (a : Nat) : ATestV2' x -- unknown identifier 'x'

[Marcus Rossel]

The only reason Lean could figure out the value of the implicit parameter x in:

def ATestV2_1 := (ATestV2.c 1 : ATestV2 1)

... is because you explicitly provide the type annotation AVTestV2 1. Without the type annotation, Lean won't know what x should be:

def ATestV2_1 := ATestV2.c 1 -- error: don't know how to synthesize implicit argument @ATestV2.c ?x 1

[Markus Schmaus]

Your type ATestV2 probably isn't what you want, since the number in the type and the number in the content are completely unrelated. Your type ATestV1 can only contain numbers that are definitionally equal with the number in the type, this is why the match doesn't accept a generic variable x, but needs a concrete 1. ATestV3 in the example below might be want you are hoping for. The number in the type and content don't need to be definitionally equal (defeq), but the constructor requires a proof that they are propositionally equal (propeq), by default it uses by rfl to proof this equality. The only downside is that deriving Repr doesn't work.

inductive ATestV1 : Nat → Type where
  | c (a : Nat) : ATestV1 a
deriving Repr

inductive ATestV2 : Nat → Type where
| c (a : Nat) : ATestV2 x
deriving Repr

inductive ATestV3 : Nat → Type where
  | c (a : Nat) (property : a = b := by rfl) : ATestV3 b
deriving Repr -- doesn't work

def ATestV1_1 := ATestV1.c 1 -- works

def ATestV2_1' := ATestV2.c 1 -- can't work, since the type is unknown
def ATestV2_1 : ATestV2 0 := ATestV2.c 1 -- works, but the number of the type and the content can be different

def ATestV3_1 := ATestV3.c 1 -- works

#eval match ATestV1_1 with | .c x => x -- doesn't work
#eval match ATestV1_1 with | .c 1 => 1 -- works
#eval match ATestV2_1 with | .c x => x -- works
#eval match ATestV3_1 with | .c x h => x -- works, `h` contains the proof that `x` is 1

[Carbon]

Thanks Markus, this indeed captures what I was trying to achieve. I also will keep this autoImplicit option in mind, thanks all for flagging this.