helped with quote theory

Stream: general

[Frederick Pu]

I'm working on a way to have quoted representations of Type that allow you to embed simpler type theories. I'm wondering if the lemma wompwomp is actually provable:

class UnquoteTy (Ty : Type) where
  -- `syntax T` returns Type describing the syntax of quoted type `T : Ty`
  «syntax» : Ty → Type
  -- `interpret t` returns Type describing the smenatics of quoted type `t : Ty`
  interpret : Ty → Type
  unquote  (T : Ty) (t : «syntax» T) : interpret T
  unquote_inj (T : Ty) : Function.Injective (unquote T)
  imp (α β : Ty) : Ty
  interpret_imp (α β : Ty) : interpret (imp α β) = (interpret α → interpret β)
  unit : Ty
  hUnit : interpret unit = Unit

infixr:30 "→" => UnquoteTy.imp
open UnquoteTy

theorem wompwomp {Ty : Type} [UnquoteTy Ty] {α β : Ty} :  «syntax» (α→β) = («syntax» α → «syntax» β) := by
  have qq := UnquoteTy.interpret_imp α β
  have := unquote (α → β)
  rw [qq] at this
  have := unquote β

[Aaron Liu]

My guess is no. What's your proof idea?

[Robin Arnez]

It's false:

class UnquoteTy (Ty : Type) where
  -- `syntax T` returns Type describing the syntax of quoted type `T : Ty`
  «syntax» : Ty → Type
  -- `interpret t` returns Type describing the smenatics of quoted type `t : Ty`
  interpret : Ty → Type
  unquote  (T : Ty) (t : «syntax» T) : interpret T
  unquote_inj (T : Ty) : Function.Injective (unquote T)
  imp (α β : Ty) : Ty
  interpret_imp (α β : Ty) : interpret (imp α β) = (interpret α → interpret β)
  unit : Ty
  hUnit : interpret unit = Unit

infixr:30 "→" => UnquoteTy.imp
open UnquoteTy

inductive Syntax where
  | imp (a b : Syntax)
  | unit

def Syntax.interpret : Syntax → Type
  | .unit => Unit
  | .imp a b => a.interpret → b.interpret

def Syntax.generate : (stx : Syntax) → stx.interpret
  | .unit => ()
  | .imp _a b => fun _ => b.generate

instance : UnquoteTy Syntax where
  «syntax» _ := Empty
  interpret := Syntax.interpret
  unquote := nofun
  unquote_inj := nofun
  imp := Syntax.imp
  unit := Syntax.unit
  interpret_imp _ _ := rfl
  hUnit := rfl

theorem not_wompwomp : ¬ ∀ {Ty : Type} [UnquoteTy Ty] {α β : Ty}, «syntax» (α→β) = («syntax» α → «syntax» β) := by
  simp only [Classical.not_forall]
  exists Syntax, inferInstance, .unit, .unit
  intro (h : Empty = (Empty → Empty))
  exact (h.mpr id).elim

[Frederick Pu]

what if we also make the syntax function injective?

class UnquoteTy (Ty : Type) where
  -- `syntax T` returns Type describing the syntax of quoted type `T : Ty`
  «syntax» : Ty → Type
  syntax_inj : Function.Injective «syntax»
  -- `interpret t` returns Type describing the smenatics of quoted type `t : Ty`
  interpret : Ty → Type
  unquote  (T : Ty) (t : «syntax» T) : interpret T
  unquote_inj (T : Ty) : Function.Injective (unquote T)
  imp (α β : Ty) : Ty
  interpret_imp (α β : Ty) : interpret (imp α β) = (interpret α → interpret β)
  unit : Ty
  hUnit : interpret unit = Unit

[Edward van de Meent]

that's gonna be hard to prove

[Edward van de Meent]

what's the (or an) intended implementation of the interpret function? I don't quite get what "a type describing the semantics of the quoted type" means...

[Edward van de Meent]

(nor why it should be injective)

[Frederick Pu]

it should be injective cause there's no point of having two elements of T that map to the same type

[Frederick Pu]

cause then you also get two syntaxs for the same type

[Frederick Pu]

i want you to be able reason about it as if it's type theory

[Frederick Pu]

also i think the equality is still unprovable because in theory the quoted functions could be a much smaller set

[Frederick Pu]

the more useful property i want is this anyways

[Frederick Pu]

-- can be defined using map and `UnquoteTy.interpret_imp`
def UnquoteTy.app {Ty : Type} [UnquoteTy Ty] {α β : Ty} : «syntax» (α → β) → «syntax» α → «syntax» β :=
  sorry

[Frederick Pu]

i mean seems like this would be non computable anyways tho lol

[Aaron Liu]

Frederick Pu said:

it should be injective cause there's no point of having two elements of T that map to the same type

Note that you can't prove Nat and Int are unequal in Lean

[Aaron Liu]

You also can't prove String and Int are unequal

[Aaron Liu]

This means you probably will never be able to instantiate a concrete instance of UnquoteTy

[Aaron Liu]

if you want syntax to be injective

[Robin Arnez]

It is constructible but I'm pretty sure you still can't prove your theorem about syntax:

class UnquoteTy (Ty : Type) where
  -- `syntax T` returns Type describing the syntax of quoted type `T : Ty`
  «syntax» : Ty → Type
  syntax_inj : Function.Injective «syntax»
  -- `interpret t` returns Type describing the semantics of quoted type `t : Ty`
  interpret : Ty → Type
  unquote  (T : Ty) (t : «syntax» T) : interpret T
  unquote_inj (T : Ty) : Function.Injective (unquote T)
  imp (α β : Ty) : Ty
  interpret_imp (α β : Ty) : interpret (imp α β) = (interpret α → interpret β)
  unit : Ty
  hUnit : interpret unit = Unit

infixr:30 "→" => UnquoteTy.imp
open UnquoteTy

inductive Syntax where
  | imp (a b : Syntax)
  | unit

def Syntax.interpret : Syntax → Type
  | .unit => Unit
  | .imp a b => a.interpret → b.interpret

def SyntaxTy := Quotient {
  r a b := Syntax.interpret a = Syntax.interpret b
  iseqv := {
    refl _ := rfl
    symm h := h.symm
    trans h h' := h.trans h'
  }
}

def Syntax.generate : (stx : Syntax) → stx.interpret
  | .unit => ()
  | .imp _a b => fun _ => b.generate

instance : UnquoteTy SyntaxTy where
  «syntax» := Quotient.lift Syntax.interpret (fun _ _ h => h)
  syntax_inj a b := by
    induction a, b using Quotient.inductionOn₂ with | _ a b
    exact Quot.sound (r := fun a b : Syntax => a.interpret = b.interpret)
  interpret := Quotient.lift Syntax.interpret (fun _ _ h => h)
  unquote _ := id
  unquote_inj _ := Function.injective_id
  imp := Quotient.lift₂ (fun a b => Quotient.mk _ (a.imp b))
    (fun a b c d h₁ h₂ => Quotient.sound (h₁ ▸ h₂ ▸ rfl : (a.interpret → b.interpret) = (c.interpret → d.interpret)))
  unit := Quotient.mk _ Syntax.unit
  interpret_imp := Quotient.ind₂ fun _ _ => rfl
  hUnit := rfl

[Aaron Liu]

of course why didn't I think of that

[Robin Arnez]

To demonstrate why it isn't provable, we can use the cardinality model:

import Mathlib

class UnquoteTy (Ty : Type) where
  -- `syntax T` returns Type describing the syntax of quoted type `T : Ty`
  «syntax» : Ty → Type
  syntax_inj : Function.Injective «syntax»
  -- `interpret t` returns Type describing the semantics of quoted type `t : Ty`
  interpret : Ty → Type
  unquote  (T : Ty) (t : «syntax» T) : interpret T
  unquote_inj (T : Ty) : Function.Injective (unquote T)
  imp (α β : Ty) : Ty
  interpret_imp (α β : Ty) : interpret (imp α β) = (interpret α → interpret β)
  unit : Ty
  hUnit : interpret unit = Unit

/-- Cardinality model -/
axiom eq_of_equiv (h : α ≃ β) : α = β

infixr:30 "→" => UnquoteTy.imp
open UnquoteTy

instance : UnquoteTy Unit where
  «syntax» _ := Empty
  syntax_inj _ _ _ := rfl
  interpret _ := Unit
  unquote := nofun
  unquote_inj _ := nofun
  imp _ _ := ()
  unit := ()
  interpret_imp _ _ := eq_of_equiv ⟨fun _ _ => (), fun _ => (), fun _ => rfl, fun _ => rfl⟩
  hUnit := rfl

theorem not_wompwomp : ¬ ∀ {Ty : Type} [UnquoteTy Ty] {α β : Ty}, «syntax» (α→β) = («syntax» α → «syntax» β) := by
  simp only [Classical.not_forall]
  exists Unit, inferInstance, .unit, .unit
  intro (h : Empty = (Empty → Empty))
  exact (h.mpr id).elim

[Frederick Pu]

if we do this is it possible to prove interpret_imp as a consequence?

class UnquoteTy (Ty : Type) where
  -- `syntax T` returns Type describing the syntax of quoted type `T : Ty`
  «syntax» : Ty → Type
  syntax_inj : Function.Injective «syntax»
  -- `interpret t` returns Type describing the smenatics of quoted type `t : Ty`
  interpret : Ty → Type
  unquote  (T : Ty) (t : «syntax» T) : interpret T
  unquote_inj (T : Ty) : Function.Injective (unquote T)
  imp (α β : Ty) : Ty
  -- interpret_imp (α β : Ty) : interpret (imp α β) = (interpret α → interpret β)
  app {α β : Ty} : «syntax» (imp α β) → «syntax» α → «syntax» β
  unit : Ty
  hUnit : interpret unit = Unit

[Frederick Pu]

seems like with all the extra injectivity lemmas it's better to just do this:

class UnquoteTy (Ty : Type) where
  -- `syntax T` returns Type describing the syntax of quoted type `T : Ty`
  «syntax» : Ty → Type
  -- `interpret t` returns Type describing the smenatics of quoted type `t : Ty`
  interpret : Ty → Type
  unquote  (T : Ty) (t : «syntax» T) : interpret T
  imp (α β : Ty) : Ty
  interpret_imp (α β : Ty) : interpret (imp α β) = (interpret α → interpret β)
  app {α β : Ty} : «syntax» (imp α β) → «syntax» α → «syntax» β
  unit : Ty
  hUnit : interpret unit = Unit

[Frederick Pu]

also do any of you know a way to have an instance of UnquoteTy for a simple type theory on nat?

[Aaron Liu]

what's the type theorey

[Aaron Liu]

can you describe it in words

[Frederick Pu]

im thinking the only types are Nat and Unit

[Frederick Pu]

and any function between them

[Frederick Pu]

recursive function are defined using something analagous to Nat.rec where the motive is fun (n : Nat) -> Nat

[Frederick Pu]

so like primitive recursion arithmetic

[Frederick Pu]

also im fine with unit not being implemented we can just have

class UnquoteTy (Ty : Type) where
  -- `syntax T` returns Type describing the syntax of quoted type `T : Ty`
  «syntax» : Ty → Type
  -- `interpret t` returns Type describing the smenatics of quoted type `t : Ty`
  interpret : Ty → Type
  unquote  (T : Ty) (t : «syntax» T) : interpret T
  imp (α β : Ty) : Ty
  interpret_imp (α β : Ty) : interpret (imp α β) = (interpret α → interpret β)
  app {α β : Ty} : «syntax» (imp α β) → «syntax» α → «syntax» β

[Frederick Pu]

does anyone know how i can do this recursion for the unquote?

def MyLang.syntax : MyLang → Type
| MyLang.A => Nat
| MyLang.Arrow MyLang.A MyLang.A => Unit
| MyLang.Arrow X Y => MyLang.syntax X → MyLang.syntax Y

def MyLang.interpret : MyLang → Type
| MyLang.A => Nat
| MyLang.Arrow X Y => MyLang.syntax X → MyLang.syntax Y

def MyLang.unquote : (T : MyLang) → T.syntax → T.interpret
| MyLang.A, t => t
| MyLang.Arrow MyLang.A MyLang.A, t => id
| MyLang.Arrow X Y, t => by {
  have : X ≠ Y := by exact?
  unfold MyLang.syntax at t
}

i cant convice lean that these three are disjoint

[Edward van de Meent]

that's because they aren't? T could be MyLang.Arrow (MyLang.Arrow MyLang.A MyLang.A) (MyLang.Arrow MyLang.A MyLang.A)

[Edward van de Meent]

or, at least the X ≠ Y bit isn't true

[Edward van de Meent]

if you're explicit about the cases, this works:

def MyLang.unquote : (T : MyLang) → T.syntax → T.interpret
| MyLang.A, t => t
| MyLang.Arrow (MyLang.A) (MyLang.A), t => id
| MyLang.Arrow MyLang.A (MyLang.Arrow X Y), t => t
| MyLang.Arrow (MyLang.Arrow X Y) Z, t => t

[Frederick Pu]

ah thx

[Frederick Pu]

i think having syntax be an arbitrary type map allows too much leakage from lean's metatheory. I decided to do something more like a rule based sequent calculus on simple types where function are composed by composition (cut rule) in a continuation passing form:

class Unquote (Ty : Type) (rules : List (List Ty × Ty)) where
  -- `interpret t` returns Type describing the smenatics of quoted type `t : Ty`
  interpret : List Ty → Ty → Type
  unquote_intro (ruleIdx : Fin rules.length) : interpret (rules.get ruleIdx).1 (rules.get ruleIdx).2
  unquote_cut (Γ' Γ : List Ty) (T α : Ty) (a : interpret Γ' α) (t : interpret (α::Γ) T) : interpret (Γ' ++ Γ) T

inductive WompWomp (Ty : Type) (rules : List (List Ty × Ty)) : (Γ : List Ty) → (T : Ty) → Type where
| intro (ruleIdx : Fin rules.length) : WompWomp Ty rules (rules.get ruleIdx).1 (rules.get ruleIdx).2
| cut (Γ' Γ : List Ty) (T α : Ty) (a : WompWomp Ty rules Γ' α) (t : WompWomp Ty rules (α::Γ) T) : WompWomp Ty rules (Γ' ++ Γ) T

def WompWomp.unquote
  {Ty : Type} {rules : List (List Ty × Ty)}
  [U : Unquote Ty rules]
  : (Γ : List Ty) → (T : Ty) → WompWomp Ty rules Γ T →
      Unquote.interpret rules Γ T
| _, _, WompWomp.intro ruleIdx => U.unquote_intro ruleIdx
| _, _, WompWomp.cut Γ' Γ T α a t =>
  let ua := WompWomp.unquote Γ' α a
  let ut := WompWomp.unquote (α :: Γ) T t
  U.unquote_cut Γ' Γ T α ua ut

does anyone know if this forms a linear type system? Cause it seems like each value can only be used once and all values must be consumed