-
Notifications
You must be signed in to change notification settings - Fork 0
/
Syntax.lean
105 lines (79 loc) · 2.63 KB
/
Syntax.lean
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
import «PCF».Utility
/-
The syntax of PCF consists of objects of four sorts: types, contexts, variables, and terms.
-/
inductive Ty
| bool
| nat
| pow : Ty → Ty → Ty
infixr:100 " ⇒ " => Ty.pow
inductive Cx
| nil
| cons : Cx -> Ty -> Cx
infixl:70 " ∷ " => Cx.cons
inductive Var : Cx → Ty → Type
| z : ∀ {Γ : Cx}, Var (Γ ∷ τ) τ
| s : ∀ {Γ : Cx} {υ : Ty} τ, Var Γ τ → Var (Γ ∷ υ) τ
infix:70 " ∋ " => Var
inductive Tm : Cx → Ty → Type
| var : ∀ τ, Γ ∋ τ → Tm Γ τ
| true : Tm Γ .bool
| false : Tm Γ .bool
| zero : Tm Γ .nat
| succ : Tm Γ .nat → Tm Γ .nat
| pred : Tm Γ .nat → Tm Γ .nat
| zero? : Tm Γ .nat → Tm Γ .bool
| cond : Tm Γ .bool → Tm Γ τ → Tm Γ τ → Tm Γ τ
| fn : Tm (Γ ∷ τ) υ → Tm Γ (τ ⇒ υ)
| app : Tm Γ (τ ⇒ υ) → Tm Γ τ → Tm Γ υ
| fix : Tm Γ (τ ⇒ τ) → Tm Γ τ
infix:70 " ⊢ " => Tm
/-
Certain terms are designated as 'values'.
-/
inductive Tm.IsValue : Γ ⊢ τ → Type
| true : true.IsValue
| false : false.IsValue
| zero : zero.IsValue
| succ {v : Tm ..} : v.IsValue → v.succ.IsValue
| fn {e : Tm ..} : e.fn.IsValue
/-
The types of booleans and naturals are designated as 'ground types'.
-/
inductive Ty.IsGround : Ty → Type
| bool : bool.IsGround
| nat : nat.IsGround
def Ty.IsGround.repr : Ty.IsGround τ → Type
| .bool => Bool
| .nat => Nat
/-
We define functions for converting between mathematical objects and ground values.
-/
def Tm.from_bool : Bool → Γ ⊢ .bool
| .true => .true
| .false => .false
def Tm.from_nat : Nat → Γ ⊢ .nat
| .zero => .zero
| .succ n => .succ (Tm.from_nat n)
def Tm.IsValue.extract_bool : {v : nil ⊢ .bool} → v.IsValue → (n : Bool) ×' v = from_bool n
| .true, .true => ⟨.true, rfl⟩
| .false, .false => ⟨.false, rfl⟩
def Tm.IsValue.extract_nat : {v : nil ⊢ .nat} → v.IsValue → (n : Nat) ×' v = from_nat n
| .zero, .zero => ⟨.zero, rfl⟩
| .succ _, .succ v' => let Φ := Tm.IsValue.extract_nat v'; ⟨Φ.fst.succ, congrArg Tm.succ Φ.snd⟩
def Tm.from_nat_is_value : ∀ n, (Tm.from_nat n : Γ ⊢ .nat).IsValue
| .zero => .zero
| .succ n => .succ (from_nat_is_value n)
/-
We define a notion of appending one context to another.
-/
def Cx.append (Γ : Cx) : Cx → Cx
| .nil => Γ
| .cons Δ τ => (Γ.append Δ) ∷ τ
instance : Append Cx where
append := Cx.append
/-
We also define helper functions for converting terms to variables and weakening variables.
-/
def Var.tm (x : Γ ∋ τ) : Γ ⊢ τ := Tm.var τ x
def Var.succ (x : Γ ∋ τ) {υ : Ty} : (Γ ∷ υ) ∋ τ := s τ x