Translating Agda's All to Lean

Stream: lean4

[nrs]

image.png

Would you say the following Lean definition is the correct translation of the Agda type above?

inductive All (P : I -> Type) : List I -> Type

def mkAll (P : I -> Type) : (list : List I) -> Type
| .nil => All P .nil
| .cons i xs => P i -> mkAll P xs -> All P (.cons i xs)

I was trying to otherwise think whether there was some way to pattern match during an inductive definition. Or maybe there is a more idiomatic translation (that is nevertheless non-Prop)? I want to keep it as a non-Prop type to be able to use it to construct other types.

[Johan Commelin]

I would rather expect something like

inductive All : (P : I -> Type) → List I -> Type
  | nil : All P .nil
  | cons {i xs} : P i -> All P xs -> All P (.cons i xs)

#check @All.nil  -- @All.nil : {I : Type} → {P : I → Type} → All P []
#check @All.cons -- @All.cons : {I : Type} → {P : I → Type} → {i : I} → {xs : List I} → P i → All P xs → All P (i :: xs)

[nrs]

Johan Commelin said:

I would rather expect something like

inductive All : (P : I -> Type) → List I -> Type
  | nil : All P .nil
  | cons {i xs} : P i -> All P xs -> All P (.cons i xs)

#check @All.nil  -- @All.nil : {I : Type} → {P : I → Type} → All P []
#check @All.cons -- @All.cons : {I : Type} → {P : I → Type} → {i : I} → {xs : List I} → P i → All P xs → All P (i :: xs)

Very cool I have never seen this!! {i xs} is sort of an analogue to pattern matching on List I right?

[nrs]

is there any way to make this implicit pattern match explicit?

[nrs]

just (i : I) (xs : List I) before semicolon I guess, not exactly a pattern match but it would be how the make the above explicit. Edit: hm but making them explicit this way doesn't necessarily guarantee we're making use of the List I in our dependent parameters in the inductive header right? Edit2: it does if we pass (.cons i xs) at the end! Very cool approach thank you!

[Johan Commelin]

nrs said:

{i xs} is sort of an analogue to pattern matching on List I right?

Not exactly. In fact, you can leave it out. But you'll notice that Lean then swaps the order that these implicit arguments appear in, in the type of All.cons.

[Johan Commelin]

Note that you never told Lean that I is a type. This is the autoImplicit functionality kicking in.

[Johan Commelin]

You wrote i and xs in the signature, so Lean figured out, aah those must be some implicit arguments that I should add.

[nrs]

Thanks for the answer! I will be thinking about this

[Kyle Miller]

It's worth using #print (or hovering over the constructors, or doing the #check commands that Johan did) to see the types of the constructors, to understand what {i xs} expands to.

#print All
/-
inductive All : {I : Type} → (I → Type) → List I → Type
number of parameters: 2
constructors:
All.nil : {I : Type} → {P : I → Type} → All P []
All.cons : {I : Type} → {P : I → Type} → {i : I} → {xs : List I} → P i → All P xs → All P (i :: xs)
-/

[nrs]

Kyle Miller said:

It's worth using #print (or hovering over the constructors, or doing the #check commands that Johan did) to see the types of the constructors, to understand what {i xs} expands to.

#print All
/-
inductive All : {I : Type} → (I → Type) → List I → Type
number of parameters: 2
constructors:
All.nil : {I : Type} → {P : I → Type} → All P []
All.cons : {I : Type} → {P : I → Type} → {i : I} → {xs : List I} → P i → All P xs → All P (i :: xs)
-/

very useful tyvm!!