# Zulip Chat Archive

## 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):

(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 (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: Aug 03 2023 at 10:10 UTC