Hypothetical judgements

Stream: new members

[Ariel Davis]

Hello. I'm trying to use Lean to define the semantics of a simple programming language. To do that, I would like to first define inductive types which represent the expressions and types in the language, respectively. I have done this. I would then like to define the judgements for the typing of expressions. This is where I am running into problems. I believe I have something that works for simple expressions, but I'm not sure how to change what i have to account for 'hypotheses' (like 'the variable x has type t'). This is necessary to write down the typing rules for, for instance, an expression "let x = e in e'" where x is a variable and e, e' are expressions. I have attached my code as it is now. Could anyone help me with this? e.lean

[Wojciech Nawrocki]

There are many ways to deal with this. One approach is to let the context be a partial map from variables to types. Then extracting a variable is function application and adding x is extending the map by adding a new case that handles x. Probably the canonical resource for this is Software Foundations. You would be interested in the section on typing (link), but in general going through the Stlc chapters will explain exactly how to do what you want. Foundations uses Coq, so the Lean code will be a little different, but not by too much.

[Rob Lewis]

To start a bit earlier: you'll want to change your has_typ function to has_typ_in_ctx. Instead of being a binary relation between a term and a type, it will be a three-way relation between a term, a type, and a context.

[Patrick Massot]

I cannot help with this kind of formalization, but I have a practical suggestion. People here usually post their Lean code either in their message when it is short enough or using https://gist.github.com/ or a similar website. We don't want people to get used to opening a Lean file randomly downloaded from the internet into VSCode (or emacs) without seeing its content first, since this is a huge security hole (VScode will start running Lean on that file without letting you inspect its content first).

[Rob Lewis]

You'll need to choose how to represent contexts. There are many possibilities here.

[Rob Lewis]

Wojciech's suggestion of a partial map makes sense, but another simple one (good enough to write down a basic sketch, at least) would be

@[reducible] def context : Type := list (exp × typ)

[Rob Lewis]

So you could do something like

inductive has_typ: context → exp -> typ -> Prop
-- 0 : nat
| z: ∀ ctx, has_typ ctx exp.z typ.num
-- e : nat => Succ(e) : nat
| succ (e: exp) (ctx : context) (_: has_typ ctx e typ.num): has_typ ctx (exp.succ e) typ.num
-- true : bool
| t: ∀ ctx, has_typ ctx exp.t typ.bool
-- false : bool
| f: ∀ ctx, has_typ ctx exp.f typ.bool
-- Γ, x : τ ⊢ x : τ
| id (x : exp) (τ : typ) (ctx : context) : (x, τ) ∈ ctx → has_typ ctx x τ
-- Γ ⊢ e : τ ∧ Γ, x : τ ⊢ e' : τ' => Γ ⊢ let x = e in e' : τ'
-- ???

[Rob Lewis]

I've left the last one for you to think about.

[Ariel Davis]

Thanks everyone for the responses. @Patrick Massot sorry, i hadn't considered that. I'll be more careful in the future.

[Patrick Massot]

No problem.

[Rob Lewis]

We don't want people to get used to opening a Lean file randomly downloaded from the internet into VSCode (or emacs) without seeing its content first

For the record, this one is safe, and I did check first :wink:

[Rob Lewis]

Unrelated, why does Zulip highlight the word context? Was that ever a keyword?