## Stream: general

### Topic: Type Reflection in Lean

#### Alcides Fonseca (Mar 11 2021 at 08:59):

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 (Mar 11 2021 at 09:40):

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 (Mar 11 2021 at 09:43):

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 (Mar 11 2021 at 09:45):

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

#### Mario Carneiro (Mar 11 2021 at 09:45):

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

#### Mario Carneiro (Mar 11 2021 at 09:46):

the function f is thus provably equal to

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


#### Mario Carneiro (Mar 11 2021 at 09:46):

although that's probably a side effect of minimization

#### Alcides Fonseca (Mar 11 2021 at 10:36):

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

#### Alcides Fonseca (Mar 11 2021 at 11:12):

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 (Mar 11 2021 at 15:49):

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 (Mar 11 2021 at 15:50):

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 (Mar 11 2021 at 15:51):

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 (Mar 11 2021 at 15:54):

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 (Mar 11 2021 at 16:06):

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 (Mar 11 2021 at 16:26):

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 (Mar 11 2021 at 16:29):

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 (Mar 11 2021 at 16:30):

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 (Mar 11 2021 at 16:31):

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

#### Alcides Fonseca (Mar 22 2021 at 19:08):

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 (Mar 22 2021 at 19:32):

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 (Mar 22 2021 at 21:49):

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

#### Mario Carneiro (Mar 22 2021 at 21:50):

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


Last updated: May 13 2021 at 00:41 UTC