Type Reflection in Lean

Stream: general

[Alcides Fonseca]

inductive WOptions
| A
| B

attribute [derive decidable_eq] WOptions

inductive Wrapper: WOptions → Type
| W {w} : Wrapper w

open Wrapper

attribute [derive decidable_eq] Wrapper

def f {T U : WOptions} (t:Wrapper T) (u:Wrapper U) : Wrapper T := if h:T=U then u else t

I wrote this MVE that does not work in the dite. I derived decidable_eq to remove the issue of deciding whether T could be U. My goal (in a bigger project) is to do type-safe substitution on a strongly-typed AST. Is this simply not possible?

[Mario Carneiro]

Do you have a sketch for your bigger example? For the general pattern of this if-then, where you check if the indices match and then use a subst, it's usually easiest to work with function.update, but I suspect an #xy problem here

[Mario Carneiro]

In this case

def f {T U : WOptions} (t:Wrapper T) (u:Wrapper U) : Wrapper T :=
if h:T=U then by rw h; exact u else t

works

[Mario Carneiro]

It's also not clear to me in what way this is supposed to represent "type reflection" as in your title

[Mario Carneiro]

the Wrapper types are all singletons so they don't carry any information

[Mario Carneiro]

the function f is thus provably equal to

def f {T U : WOptions} (t:Wrapper T) (u:Wrapper U) : Wrapper T := ⟨⟩

[Mario Carneiro]

although that's probably a side effect of minimization

[Alcides Fonseca]

Thanks, it worked. Somehow I was missing the exact tactic (thinking after the ; I was back in term mode).

[Alcides Fonseca]

This is the full (relevant) code:

@[derive decidable_eq]
inductive TType
| TBool : TType
| TNat : TType
| Fun : TType → TType → TType

open TType

@[reducible]
def context := list (string × TType)

def keys (Γ: context) : list string := list.map (λ x, prod.fst x) Γ

inductive Term : TType → Type
| LiteralNat : ℕ → Term TNat
| LiteralBool : bool → Term TBool
| Var {Γ: context} {T} (x: string) (p: (x, T) ∈ Γ) : Term T
| Abs {Γ: context} {U} (x:string) (T: TType) (e:Term U) (p: x ∉ keys(Γ)) : Term (Fun T U)
| App {T U} (t1: Term (Fun T U)) (t2: Term T) : Term U
| Ite {T} (t1:Term TBool) (t2 t3 : Term T) : Term T

open Term

def substitution {T U} (t: Term T) (n: Term U) (x: string) : Term T :=
  match (t:Term T) with
   | (Var name p) := if h:T = U then by rw h; exact n else t
   -- | (LiteralBool b) := LiteralBool b
   | _ := t
  end

I am troubling getting the interaction between the T and the pattern matching. I knew that using dite, I could apply some tactic to solve it (although the syntax was a mystery to me). But using match, the second (comment) pattern does not work, because it cannot understand that it should only cover when T = TBool.
And even though I have a catch-all wildcard, it complains that I do not cover all the cases.

[Mario Carneiro]

There appears to be an issue in getting the wildcard case to typecheck, that prevents the wildcard from working correctly without some kind of untypechecked macro expansion. Here's a version that works, which is what the wildcard compiles to anyway:

def substitution {T U} (t: Term T) (n: Term U) (x: string) : Term T :=
match T, t with
| T, t@(Var name p) := if h:T = U then by rw h; exact n else t
| _, t@(LiteralNat _) := t
| _, t@(LiteralBool _) := t
| _, t@(Abs _ _ _ _) := t
| _, t@(App _ _) := t
| _, t@(Ite _ _ _) := t
end

[Mario Carneiro]

Note that it is necessary to simultaneously match on T and t, because Term is an inductive type with the TType as an index (it's an inductive family), so it has to be able to vary in recursions

[Mario Carneiro]

By the way, the definition of Term is incorrect, since the contexts used in the Var and Abs constructors are not constrained to relate to anything else. The context should be another index to the inductive type

[Mario Carneiro]

like this:

inductive Term : context → TType → Type
| LiteralNat {Γ} : ℕ → Term Γ TNat
| LiteralBool {Γ} : bool → Term Γ TBool
| Var {Γ T} (x: string) (p: (x, T) ∈ Γ) : Term Γ T
| Abs {Γ U} (x:string) (T: TType) (e:Term ((x,T)::Γ) U) (p: x ∉ keys(Γ)) : Term Γ (Fun T U)
| App {Γ T U} (t1: Term Γ (Fun T U)) (t2: Term Γ T) : Term Γ U
| Ite {Γ T} (t1:Term Γ TBool) (t2 t3 : Term Γ T) : Term Γ T

open Term

def substitution {Γ T U} (x: string) (t: Term ((x, U)::Γ) T) (n: Term Γ U) : Term Γ T :=
sorry

[Alcides Fonseca]

Yes, you are correct in the Term definition. I was actually simplifying it to try and spot the issue on the match.
I was missing the simultaneous matching. That seems to be the key.
Thank you so much again!

[Mario Carneiro]

Here's a setup that I believe to be provable:

def context := alist (λ _: string, TType)

def keys : context → list string := alist.keys

instance : has_mem (string × TType) context := ⟨λ ⟨x, T⟩ Γ, T ∈ Γ.lookup x⟩

def cons (Γ : context) (x:string) (T:TType) (h : x ∉ Γ.keys) : context :=
⟨⟨x,T⟩::Γ.1, list.nodupkeys_cons.2 ⟨h, Γ.2⟩⟩

inductive Term : context → TType → Type
| LiteralNat {Γ} : ℕ → Term Γ TNat
| LiteralBool {Γ} : bool → Term Γ TBool
| Var {Γ : context} {T} (x: string) (p: (x, T) ∈ Γ) : Term Γ T
| Abs {Γ U} (x:string) (T: TType) (p: x ∉ keys Γ) (e:Term (cons Γ x T p) U) : Term Γ (Fun T U)
| App {Γ T U} (t1: Term Γ (Fun T U)) (t2: Term Γ T) : Term Γ U
| Ite {Γ T} (t1:Term Γ TBool) (t2 t3 : Term Γ T) : Term Γ T

open Term

def substitution_aux {Γ U} (x : string) (n : Term Γ U) :
  ∀ {Γ' T}, Term Γ' T → Γ'.1 ~ ⟨x, U⟩::Γ.1 → Term Γ T
| Γ' _ (LiteralNat n) hp := LiteralNat n
| Γ' _ (LiteralBool b) hp := LiteralBool b
| Γ' U' (Var name p) hp :=
  begin
    have other : Term Γ U' := Var name _,
    { exact if name = x then if h : U' = U then by rw h; exact n else other else other },
    sorry
  end
| Γ' _ (@Abs _ U' y T' p e) hp := sorry
| Γ' U' (@App _ T' _ t1 t2) hp := sorry
| Γ' T' (Ite t1 t2 t3) hp := sorry

def substitution {Γ T U} (x: string) (p) (t: Term (cons Γ x U p) T) (n: Term Γ U) : Term Γ T :=
substitution_aux x n t (list.perm.refl _)

[Mario Carneiro]

The point of using alist instead of list here is so that the use of list permutation in the statement of substitution_aux doesn't change the types of existing variables. This is needed in order to commute the cons application in the type of substitution with the one in the type of Abs

[Mario Carneiro]

You can also avoid the use of permutation entirely if you use finmap instead of alist, since that bakes the permutations into the type

[Mario Carneiro]

Alternatively, you can stick with list and use the more precise context Γ ++ (x,U) :: Δ in the type of substitution

[Alcides Fonseca]

(Sorry for the late reply, had a couple of deadlines)
Thank you very much for the reply! It helped much more than just answering the question. I'll have to buy you a drink next time I'll visit CMU (if you are still there)

[Alcides Fonseca]

A follow-up issue: I want to show that a set of term synthesis rules (like the opposite of type-checking). However, using a strongly-typed AST breaks the way I was stating the synthesis rules. I have simplified the problem to this exame, where the language has OptionA and OptionB, with the type indexed by a number (in the larger example it is the context and type). I want to state that I can generate one of each, and then show completeness of the generation (which will not work in this case, unless I add that n < 2)

inductive term : ℕ → Type
| optionA : term 0
| optionB : term 1


inductive synth {n:ℕ} : term n → Prop
| generateOptionA : synth (term.optionA)
| generateOptionB : synth (term.optionB)


theorem completeness {n:ℕ} : ∀ (t:term n), synth n t := by sorry

Lines generateOptionA and B do not compile:

type mismatch at application
  synth term.optionA
term
  term.optionA
has type
  term 0
but is expected to have type
  term n

How can I refined the type to use index 0? I have tried to make n:\Nat explicit, but it did not work.

[Mario Carneiro]

Actually you don't need n < 2 for this proof

[Mario Carneiro]

inductive term : ℕ → Type
| optionA : term 0
| optionB : term 1

inductive synth : ∀ {n:ℕ}, term n → Prop
| generateOptionA : synth term.optionA
| generateOptionB : synth term.optionB

theorem completeness : ∀ {n:ℕ} (t:term n), synth t
| _ term.optionA := synth.generateOptionA
| _ term.optionB := synth.generateOptionB