Simp extension

Stream: lean4

[Florian Würmseer]

Hey everyone,

I'm currently trying to typecheck inputs of a heterogeneous nested list (eventually I want to extend it to more than just Nat and Char). The goal is that the following typechecks:
[['A', 2, 5, 'T'],
['B', 100, 7, 'X']]
and not the following:
[['A' 2, 5, 'T'],
[100, 'B', 7]]
Considering the sequence of the types and the length of the sublists.

The typechecking works when providing a proof h with Or and simp can solve the goal.:

inductive NTup : List Type → Type 1 where
  | nil : NTup []
  | cons {α : Type} (x : α) {αs : List Type} (xs : NTup αs) (h : α = Char ∨ α = Nat := by simp) : NTup (α :: αs)

set_option trace.Meta.Tactic.simp true
def foo : NTup [Char] := NTup.cons 'a' NTup.nil

according to the simp trace the theorems "eq_self" and "true_or" are used for the goal.

In order to match and extract the values of the hypothesis I wanted to use PSum:

def IsValidSqlType (α : Type) := (α = Char) ⊕' (α = Nat)

def myCast (x : α) (h : IsValidSqlType α) : A :=
  match h with
  | PSum.inl h => A.char $ cast h x
  | PSum.inr h => A.nat $ cast h x

When changing NTup to use PSum instead of Or, simp is not able to solve it. Even when giving it the theorems:

@[simp]
theorem true_psum (p : Prop) : (True ⊕' p) := PSum.inl True.intro
@[simp]
theorem psum_true (p : Prop) : (p ⊕' True) := PSum.inr True.intro

(eq_self remains in scope)
simp cannot solve it anymore.
Is simp applying any other theorems in the background that I don't see via "set_option trace.Meta.Tactic.simp true"?
And also is there a better approach for typechecking a list of unique types?

[Horatiu Cheval]

For a nice implementation of heterogeneous lists, you can look at: https://github.com/crabbo-rave/Soup made by @Joseph O which seems to be using essentialy the same approach you are going for (except for the Nat or Char restriction)

[Horatiu Cheval]

Also, I think it's not clear what A is in your second example, thus people may have a harder time helping you. I guess it's a form of a sum between Nat and Char?

[Florian Würmseer]

Thank you for your answer Horatiu.
Yes indeed. A would be something like:

inductive A where
| nat : Nat → A
| char : Char → A

and is only included to show my need of getting actual values from NTup. And my question is considering the Nat or Char restriction that I want to eventually extend to Nat or Char or ...
So my usecase is different from https://github.com/crabbo-rave/Soup.

[Horatiu Cheval]

If you are only interested in some types, couldn't you simply use List (Nat ⊕ Char)? Maybe with other types the sum, or even your own inductive type for all the possible values if there are many of them (like you did with A)?

[Jannis Limperg]

Bit of an #xy but whenever you want to consider a specific subset ('universe') of types, I would make a syntactic representation of this subset and work with that (which is also basically what Horatiu suggests):

inductive Univ
| nat
| char

def Univ.interp : Univ → Type
  | nat => Nat
  | char => Char

inductive Tuple : List Univ → Type
| nil : Tuple []
| cons (x : u.interp) (xs : Tuple us) : Tuple (u :: us)

def Tuple.uncons : Tuple (u :: us) → u.interp × Tuple us
  | Tuple.cons x xs => (x, xs)

Prepare for universe issues, btw, if you ever need to go higher than Type.

[François G. Dorais]

The main issue is that equality between types doesn't behave as you expect. There is no real guarantee that Nat and Char are not the same! In fact, in the cardinal model, two types are equal iff they have the same cardinality.

[Leonardo de Moura]

In the CPDT book, Adam Chlipala uses heterogeneous lists that are still general and relevant to this discussion. We have recently translated some of his examples to Lean 4. Here is one of the examples.
https://leanprover.github.io/lean4/doc/examples/deBruijn.lean.html

[Leonardo de Moura]

In the standard HList definition, we have the "universe bump" that has been mentioned in many threads.

inductive HList : List (Type u) → Type (u+1) -- << we need the "+1" here because Lean does not have pseudo parameters
  | nil  : HList []
  | cons : α → HList αs → HList (α::αs)

Chlipala's version does not have this bump.

inductive HList {α : Type v} (β : α → Type u) : List α → Type (max u v)
  | nil  : HList β []
  | cons : β i → HList β is → HList β (i::is)

The Tuple example above is just HList Univ.interp, and we can write

abbrev Tuple := HList Univ.interp

def Tuple.uncons : Tuple (u :: us) → u.interp × Tuple us
  | HList.cons x xs => (x, xs)

[Henrik Böving]

Are there advantages of this definition over the other? So of leaving out the universe bump in exchange for this approach?

[Leonardo de Moura]

Yes, it avoids the universe bump. It also has the benefits that @Jannis Limperg suggested above. We can view Chlipala's HList as a generic version of Jannis' Tupleexample where he used elements of type Univ to index the Tuple instead of Type. Another plus is that we can pattern match on Univ, but we cannot on Type.

[Florian Würmseer]

Thank you for your answers! This was indeed what I was looking for and helped me a lot to understand more about HLists. When experimenting I found that in this instance Lean cannot infer types here and thus they have to be specified:

def x : Tuple [Univ.char] := Tuple.cons 'c' Tuple.nil

I tried to work around that by creating a macro (very similar to the one List uses) and can provide the types with pattern matching.

For testing I hardcoded the base case:

declare_syntax_cat sqlType
syntax char : sqlType
syntax num : sqlType

syntax "tuple(" sqlType,* ")" : term
macro_rules
  | `(tuple( $elems,* )) => do
    let rec expandListLit (i : Nat) (skip : Bool) (result : Lean.Syntax) : Lean.MacroM Lean.Syntax := do
      match i, skip with
      | 0,   _     => pure result
      | i+1, true  => expandListLit i false result
      | i+1, false => match elems.elemsAndSeps[i] with
        | `(sqlType|$c:charLit) => expandListLit i true (← ``((Tuple.cons $c $result : Tuple [Univ.char]))) -- Hardcoded for char
        | `(sqlType|$n:numLit) => expandListLit i true (← ``((Tuple.cons ($n : Nat) $result : Tuple [Univ.nat]))) -- Hardcoded for nat
        | _ => expandListLit i true  (← ``(Tuple.cons $(elems.elemsAndSeps[i]) $result))
    if elems.elemsAndSeps.size < 64 then
      expandListLit elems.elemsAndSeps.size false (← ``(Tuple.nil))
    else
      `(%[ $elems,* | Tuple.nil ])


#check tuple(3) -- Has correct type
#check tuple('c') -- Has correct type
#check tuple('c', 1) -- Not case provided yet

However for the n+1 case I'm struggling to read and extend the the type of the "$results" macro.

Now I'm wondering if there's a way for Lean to infer the type in the first place (whether or not this is reasonable for HLists) and/or if the macro can be extended to determine the type for n+1 elements.