Batteries.Data.List.Perm and Universe Issues

Stream: lean4

[Chris Henson]

I am relatively new to Lean, and have been working on formalizing the categorical semantics of lambda calculi. One problem I run into when trying to make use of some limited use of Batteries for lists is universe issues. As an mwe, consider:

import Batteries.Data.List

inductive Ex {X : Type} : List X → Type

def fails {X : Type} {xs ys : List X} (h : List.Perm xs ys) (ex1 : Ex xs) : Ex ys := by
  /-
  error:
  type mismatch when assigning motive
    fun a a_1 t => xs = a → ys = a_1 → HEq h t → Ex ys
  has type
    (a a_1 : List X) → a.Perm a_1 → Type : Type 1
  but is expected to have type
    (a a_1 : List X) → a.Perm a_1 → Prop : Type
  -/
  cases h

I don't understand the error message completely, but can see that switching out Type for Prop resolves the error. However, Ex would be typing derivations in my actual use case, so that's not really useful. For now, I've just taken the inductive type I want and changed its type (in this example, a new List.Perm with type List α → List α → Type). Is there a better way to handle this generally?

[Eric Wieser]

docs#List.Perm.rec_heq looks close to what you want

[Eric Wieser]

I think the summary here is that you have to do things the hard way. What you want to show is that using the Prop-valued List.Perm, you can manually assemble a Type-valued inductive principle

[Mario Carneiro]

We usually call that sorting

[Mario Carneiro]

I think it would be good to present your actual problem @Chris Henson here, this is an #xy question

[Mario Carneiro]

With no additional assumptions, it is not possible to take a List.Perm and get a data carrying variant. You need at least decidable equality of the elements

[Mario Carneiro]

and preferably a total order so you can do sorting sensibly

[Eric Wieser]

Mario Carneiro said:

We usually call that sorting

Maybe the missing piece here is a version of insertion sort / bubble sort that records the swaps / insertions?

[Daniel Weber]

Would sorting docs#List.enum (with a comparator ignoring the index) not work?

[Eric Wieser]

I have an application where I specifically need to know what the adjacent swaps were; while I can certainly recover it from such indexes, it might be faster to compute them directly

[Eric Wieser]

(though in the end I effectively just wrote my own merge for pre-sorted lists that concatenated then performed the adjacent swaps one by one)

[Chris Henson]

Mario Carneiro said:

I think it would be good to present your actual problem Chris Henson here, this is an #xy question

I see. I asked this way because I was generally curious if there was any way to lift from something Prop-valued to Type-valued, but maybe that is the wrong question. Here I wanted to show typing derivations are maintained under permutations of a context. Sorry this is a bit long, but here's the minimal amount of code to state what I wanted:

import Batteries.Data.List

/--
Product and function types.

Types are parameterized by some existing type `K`.
-/
inductive Ty (K : Type)
  /-- Unit Type -/
  | Unit : Ty K
  /-- A basic type-/
  | Basic : K → Ty K
  /-- A function type (σ ⇒ τ) -/
  | Arr : Ty K → Ty K → Ty K
  /-- A product type (σ ⨯ τ) -/
  | Prod : Ty K → Ty K → Ty K
  deriving Repr

infixr:60 " ⨯ " => Ty.Prod
infixr:70 " ⇒ " => Ty.Arr
prefix:90 "~ " => Ty.Basic

/--
A list of types.
-/
abbrev Context (K : Type) : Type := List (Ty K)

/--
Membership of a type within a context.
-/
inductive Context.member {K : Type} : Context K → Ty K → Type
  | hd : Context.member (t :: Γ) t
  | tl : Context.member Γ t → Context.member (t' :: Γ) t
  deriving Repr

infix:40 " ∋ " => Context.member

/--
Terms in the simply-typed lambda calculus with couples.
-/
inductive Term {K : Type} : Context K → Ty K → Type
  /-- A "variable" found within a context. -/
  | var : Γ ∋ a → Term Γ a
  /-- A lambda abstraction. -/
  | lam : Term (a :: Γ) b → Term Γ (a ⇒ b)
  /-- Function application. -/
  | app : Term Γ (a ⇒ b) → Term Γ a → Term Γ b
  /-- Constructor for couples -/
  | cop : Term Γ a → Term Γ b → Term Γ (a ⨯ b)
  /-- First projection of a couple. -/
  | fst : Term Γ (a ⨯ b) → Term Γ a
  /-- Second projection of a couple. -/
  | snd : Term Γ (a ⨯ b) → Term Γ b
  /-- the unit value -/
  | uni : Term Γ Ty.Unit
  deriving Repr

infix:40 " ⊢ " => Term

/--
Typing derivation for a permuted context
-/
def Term.perm {K : Type} {Γ Δ : Context K} {T : Ty K} (h : List.Perm Γ Δ) (Γ_T : Γ ⊢ T) : Δ ⊢ T := sorry

[Daniel Weber]

Why is Context a List and not a Finset?

[Chris Henson]

Daniel Weber said:

Why is Context a List and not a Finset?

Could you explain what the benefit of Finest over List would be here? My thought is that I don't really care so much here if there are duplicates within the context. They would just be different proofs of the variable lookup judgement.

[Daniel Weber]

A Finset is unordered, so you get Term.perm for free

[Chris Henson]

Oh, I see. What would the Term.lam constructor look like in that case?

[Daniel Weber]

If you don't mind duplicates being erased you can use docs#insert, if you do use docs#Finset.cons

[Eric Wieser]

Or you can use Multiset if you want to keep duplicates around, which still gives you perm for free

[Chris Henson]

Thank you. I've been trying these out, I think Multiset is a good suggestion here. I've not used it before, so one quick question. As my goal is play around with categorical semantics, I currently have the beginnings of an instance that looks like this

import Mathlib.CategoryTheory.Category.Basic

-- if you actually want to run something, paste code from earlier in the thread here...

open CategoryTheory
open Ty

-- this would change to using `Multiset`

/--
Transform a type into its corresponding context
-/
def Ty.to_ctx {K : Type} (ty : Ty K) : Context K :=
  match ty with
  | Ty.Unit => []
  | l ⨯ r => l :: r.to_ctx
  | _ => [ty]

/--
The category with types as objects and simply-typed lambda calculus derivations as morphisms
-/
instance Cat_STLC (K : Type) : Category (Ty K) where
  Hom Γ_prod T := Γ_prod.to_ctx ⊢ T
  -- other fields here eventually...

This should be a CartesianClosed instance eventually, but I started here to learn the basics of the library first. With this in mind, are there any pitfalls of using Multiset?

[Chris Henson]

After spending a little more time, I see I'll have the same issue, just with docs#Multiset.Mem instead of lists, right? Seems like an inherent mismatch. Maybe it's just not a common use case to need Type-valued membership.

[Eric Wieser]

Why do you need type-valued membership?

[Chris Henson]

Maybe another xy situation here. As an example, here was my attempt to use Multiset.

import Mathlib.Data.Multiset.Basic

inductive Ty (K : Type)
  | Unit : Ty K
  | Basic : K → Ty K
  | Arr : Ty K → Ty K → Ty K
  | Prod : Ty K → Ty K → Ty K
  deriving Repr, DecidableEq

infixr:60 " ⨯ " => Ty.Prod
infixr:70 " ⟶  " => Ty.Arr
prefix:90 "~ " => Ty.Basic

abbrev Context (K : Type) : Type := Multiset (Ty K)

inductive Term {K : Type} [DecidableEq K] : Context K → Ty K → Type
  | var : a ∈ Γ → Term Γ a
  | lam : Term (a ::ₘ Γ) b → Term Γ (a ⟶  b)
  | app : Term Γ (a ⟶  b) → Term Γ a → Term Γ b
  | cop : Term Γ a → Term Γ b → Term Γ (a ⨯ b)
  | fst : Term Γ (a ⨯ b) → Term Γ a
  | snd : Term Γ (a ⨯ b) → Term Γ b
  | uni : Term Γ Ty.Unit

infix:40 " ⊢ " => Term

abbrev Term.context_map {K : Type} [DecidableEq K] (Γ Δ : Context K) := ∀ {T}, T ∈ Γ → Δ ⊢ T

/--
Given a mapping `Γ ⇒ Δ`, extend the mapping to extended contexts
-/
def Term.ext
  {K : Type}
  [DecidableEq K]
  {Γ Δ : Context K}
  {σ T : Ty K}
  (ρ : Term.context_map Γ Δ)
  (Γ_mem : T ∈ σ ::ₘ Γ )
  : σ ::ₘ Δ ⊢ T
  := by
  rw [Multiset.mem_cons] at Γ_mem
  -- motive error here...
  cases Γ_mem

[Eric Wieser]

You can instead case on whether T = \sigma

[Eric Wieser]

Or use docs#Or.by_cases which does that for you

[Eric Wieser]

Perhaps cases ... using Or.by_cases works

[Chris Henson]

@Eric Wieser Thank you so much, I think I finally have some headway in understanding the root issue. This is exactly what I needed and I don't think I could have found it myself.

For the benefit of anyone else following along, here's the previous definition completed:

import Mathlib.Data.Multiset.Basic

inductive Ty (K : Type)
  | Unit : Ty K
  | Basic : K → Ty K
  | Arr : Ty K → Ty K → Ty K
  | Prod : Ty K → Ty K → Ty K
  deriving Repr, DecidableEq

infixr:60 " ⨯ " => Ty.Prod
infixr:70 " ⟶  " => Ty.Arr
prefix:90 "~ " => Ty.Basic

abbrev Context (K : Type) : Type := Multiset (Ty K)

def Context.weaken [DecidableEq K] {Γ : Context K} {σ : Ty K} : Γ ⊆ σ ::ₘ Γ := Multiset.subset_cons Γ σ

inductive Term {K : Type} [DecidableEq K] : Context K → Ty K → Type
  | var : a ∈ Γ → Term Γ a
  | lam : Term (a ::ₘ Γ) b → Term Γ (a ⟶  b)
  | app : Term Γ (a ⟶  b) → Term Γ a → Term Γ b
  | cop : Term Γ a → Term Γ b → Term Γ (a ⨯ b)
  | fst : Term Γ (a ⨯ b) → Term Γ a
  | snd : Term Γ (a ⨯ b) → Term Γ b
  | uni : Term Γ Ty.Unit

infix:40 " ⊢ " => Term

abbrev Term.context_map {K : Type} [DecidableEq K] (Γ Δ : Context K) := ∀ {T}, T ∈ Γ → Δ ⊢ T

def Term.rename {K : Type} {Γ Δ : Context K} {T : Ty K} [DecidableEq K] (ρ : Γ ⊆ Δ) (Γ_T : Γ ⊢ T) : Δ ⊢ T :=
  match Γ_T with
  | var x => var (ρ x)
  | lam x => by
      apply lam
      refine rename ?_ x
      exact Multiset.cons_subset_cons ρ
  | app l r => app (rename ρ l) (rename ρ r)
  | «fst» prod => fst (rename ρ prod)
  | «snd» prod => snd (rename ρ prod)
  | cop l r => cop (rename ρ l) (rename ρ r)
  | uni => uni

def Term.weakening
  {K : Type }
  [DecidableEq K]
  {Γ : Context K}
  {T : Ty K}
  (σ : Ty K) (Γ_T : Γ ⊢ T) : (σ ::ₘ Γ) ⊢ T := rename Context.weaken Γ_T

/--
Given a mapping `Γ ⇒ Δ`, extend the mapping to extended contexts
-/
def Term.ext
  {K : Type}
  [DecidableEq K]
  {Γ Δ : Context K}
  {σ T : Ty K}
  (ρ : Term.context_map Γ Δ)
  (Γ_mem : T ∈ σ ::ₘ Γ )
  : σ ::ₘ Δ ⊢ T
  := by
  rw [Multiset.mem_cons] at Γ_mem
  refine Or.by_cases Γ_mem ?_ ?_ <;> intros h
  . rw [h]
    apply var
    simp
  . exact weakening σ (ρ h)