From 626d87804fd0052603c78ce20295f5c661a30168 Mon Sep 17 00:00:00 2001 From: Philip Wadler Date: Fri, 14 Jul 2017 11:02:44 +0100 Subject: [PATCH] merging informal description with bnf --- out/Stlc.md | 5210 ++++++++++++++++++++++++----------------------- out/StlcProp.md | 544 ++--- src/Stlc.lagda | 6 +- 3 files changed, 2884 insertions(+), 2876 deletions(-) diff --git a/out/Stlc.md b/out/Stlc.md index 97120503..677d57e9 100644 --- a/out/Stlc.md +++ b/out/Stlc.md @@ -281,85 +281,87 @@ numbers as a base type. Here is the syntax of types in BNF. - A, B, C ::= A ⇒ B | 𝔹 + A, B, C ::= + A ⇒ B -- functions + 𝔹 -- booleans And here it is formalised in Agda. 
 
-infixr 20 _⇒_
 
 data Type : Set where
-  _⇒_ : Type → Type → Type Type : Set where
   𝔹_⇒_ : Type → Type → Type
+  𝔹 : Type
 
@@ -385,218 +387,220 @@ correspond to introduction rules and deconstructors to eliminators.
 
 Here is the syntax of terms in BNF.
 
+    L, M, N ::= ` x | λ[ x ∶ A ] N 
+
 
 
 
 
 
-infixl 20 _·_
 infix  15 λ[_∶_]_
 infix  15 if_then_else_
 
 data Term : Set where
   ` : Id → Term
   λ[_∶_]_ : Id → Type → Term → Term
-  _·_ : Term → Term → Term
-  true : Term
-  false : Term
-  if_then_else_ : Term → Term
+  _·_ : Term → Term → Term
+  true : Term
+  false : Term
+  if_then_else_ : Term → Term → Term → Term
 
@@ -613,225 +617,225 @@ CONTINUE FROM HERE
 Example terms.
 
 
-f x : Id
 f  =  id 0
 x  =  id 1
 
 not two : Term 
-not =  λ[ x ∶ 𝔹 ] (if ` x then false else true)
-two =  λ[ f ∶ 𝔹 ⇒ 𝔹 ] λ[ x: ∶ 𝔹 ] ` fTerm 
+not ·=  λ[ (` f · ` x ∶ 𝔹 ] (if ` x then false else true)
+two =  λ[ f ∶ 𝔹 ⇒ 𝔹 ] λ[ x ∶ 𝔹 ] ` f · (` f · ` x)
 
@@ -841,130 +845,130 @@ Example terms.
 
 
 
-data Value : Term → Set where
-  value-λ     : ∀ {x A N} → Value (λ[ x ∶ A ] N)
-  value-true  : Value: Term → trueSet where
   value-false value-λ     : ∀ {x A N} → Value (λ[ x ∶ A ] N)
+  value-true  : Value true
+  value-false : Value false
 
@@ -974,472 +978,342 @@ Example terms.
 
 
 
-_[_:=_] : Term → Id → Term → Term
-(` x′) [ x := V ] with x ≟ x′
-... | yes _ = V
-... | no  _ =: `Term x′
-(λ[→ Id → x′ ∶Term A′→ ] N′Term
+(` x′) [ x := Vx ]:= withV ] with x ≟ x′ ≟ x′
 ... | yes _ = λ[ x′= ∶ A′V
+... ]| N′no  _ = ` x′
 ... | no  _ =(λ[ λ[x′ x′ ∶ A′ A′ ] (N′) [ x := := V ]) with x ≟ x′
 (L′ · M′) [... x| :=yes V_ ] =  (L′ λ[ x′ [∶ xA′ :=] V ]N′
+) ·... (M′| [ xno  _ :== Vλ[ ])x′
-(true) ∶ A′ ] [ x(N′ [ x := V ] =V true])
 (falseL′ · M′) [ x := V ] = false
-  (if L′ then[ M′x else:= N′V ]) · (M′ [ x := [V x := V ])
+(true) =[ ifx (L′ [ x := V ] = true
+) then (M′false) [ x := := V ]) else= false
+(N′if [L′ x :=then VM′ else N′) [ x := V ] = if (L′ [ x := V ]) then (M′ [ x := V ]) else (N′ [ x := V ])
 
@@ -1622,569 +1626,569 @@ Example terms.
 
 
 
-infix 10 _⟹_ 
 
 data _⟹_ : Term → Term → Set where
-  βλ· : ∀ {x A N V} → Value V →
-    (λ[ x ∶ A ] N) · V_⟹_ ⟹: NTerm [→ xTerm :=→ VSet ]where
   ξ·₁βλ· : ∀ {L L′ M}: →∀
-    L ⟹{x L′A N V} → Value V →
     L · M ⟹ L′ ·(λ[ Mx
-  ξ·₂ ∶ A ] :N) ∀· {V M⟹ M′}N [ →x
-    Value := V →]
-    Mξ·₁ : ∀ {L ⟹L′ M′M} →
     VL · M ⟹ L′ V · M′
-  βif-true : ∀ {M N} →
     ifL true· then M else N ⟹ L′ · M
   βif-falseξ·₂ : ∀ {V M M′} →
+    Value V →
+    M ⟹ M′ →
+    V · M N} →
-    if false then M else N ⟹ NV · M′
   ξifβif-true : ∀ {L L′ M N} →
     L ⟹ L′ →    
-    if Ltrue then M else N ⟹ M
+  βif-false : ∀ {M N} →
+    if false ⟹ ifthen L′ then M else N ⟹ N
+  ξif : ∀ {L L′ M N} →
+    L ⟹ L′ →    
+    if L then M else N ⟹ if L′ then M else N
 
@@ -2195,665 +2199,665 @@ Example terms.
 
 
 
-infix 10 _⟹*_ 
 infixr 2 _⟹⟨_⟩_
 infix  3 _∎
 
 data _⟹*_ : Term → Term → Set where
-  _∎ : ∀ M → M ⟹* M
-  _⟹⟨_⟩_ : ∀ L {M N} → L ⟹ M → M ⟹* N → L ⟹*→ Term → Set where
+  _∎ : ∀ M → M ⟹* M
+  _⟹⟨_⟩_ : ∀ L {M N} → L ⟹ M → M ⟹* N → L ⟹* N  
 
 reduction₁ : not · true ⟹* false
-reduction₁ =
-    not · true
-  ⟹⟨ βλ· value-true ⟩
-    if true then false else true ⟹* false
-  ⟹⟨reduction₁ βif-true ⟩=
     falsenot · true
   ⟹⟨ βλ· value-true ⟩
+    if true then false else true
+  ⟹⟨ βif-true ⟩
+    false
+  ∎
 
 reduction₂ : two · not · true ⟹* true
-reduction₂ =
-    two · not · true
-  ⟹⟨ ξ·₁ (βλ· value-λ) ⟩
-    (λ[ x ∶ 𝔹 ]⟹* not · (not · ` x)) · true
-  ⟹⟨reduction₂ βλ·=
+    two · not · value-true ⟩true
-    not⟹⟨ ·ξ·₁ (notβλ· value-λ) · true)
-  ⟹⟨ ξ·₂ value-λ (βλ· value-true) ⟩
+    (λ[ x ∶ 𝔹 ] not · (not · ` x)) · true
+  ⟹⟨ βλ· value-true ⟩
     not · (if true then false else· (not · true)
   ⟹⟨ ξ·₂ value-λξ·₂ βif-truevalue-λ (βλ·   value-true) ⟩
     not · false
-  ⟹⟨ βλ·(if value-falsetrue ⟩
-    ifthen false else falsetrue) then
+  ⟹⟨ falseξ·₂ elsevalue-λ true
-  ⟹⟨βif-true βif-false   ⟩
     truenot · false
   ⟹⟨ βλ· value-false ⟩
+    if false then false else true
+  ⟹⟨ βif-false ⟩
+    true
+  ∎
 
@@ -2867,683 +2871,683 @@ Much of the above, though not all, can be filled in using C-c C-r and C-c C-s.
 
 
 
-Context : Set
 Context = PartialMap Type
-
-infix 10 _⊢_∶_
-
-data _⊢_∶_ : Context → Term → Type → Set where
-  Ax : ∀ {Γ x A}Type →
-    Γinfix x10 ≡ just A →_⊢_∶_
-    Γdata ⊢_⊢_∶_ ` x ∶ A
-  ⇒-I : Context → Term ∀→ {Γ xType N→ ASet B} →
-    Γ , x ∶ A ⊢ N ∶ B →
-    Γ ⊢ λ[ x ∶ A ] N ∶ A ⇒ Bwhere
   ⇒-EAx : ∀ {Γ x A} →
+    Γ x ≡ just A →
+    Γ ⊢ ` x ∶ A
+  ⇒-I : ∀ {Γ L MΓ Ax B}N A B} →
     Γ ⊢ L ∶, Ax ⇒∶ BA →⊢
-    Γ N ∶ B ⊢ M ∶ A →
     Γ ⊢ Lλ[ ·x M ∶ A ] N ∶ A ⇒ B
   𝔹-I₁ :⇒-E ∀: {Γ∀ } →
-    {Γ ⊢L M A B} true ∶ 𝔹→
-  𝔹-I₂Γ ⊢ L ∶ A :⇒ ∀B {Γ} →
     Γ ⊢ M ⊢∶ falseA ∶ 𝔹→
-  𝔹-EΓ ⊢ L · :M ∀∶ {Γ L M NB
+  𝔹-I₁ A: ∀ {Γ} →
     Γ ⊢ Ltrue ∶ 𝔹 →
-    Γ
+  𝔹-I₂ ⊢: M∀ ∶{Γ} A →
     Γ ⊢ Nfalse ∶ A →𝔹
-    𝔹-E : ∀ {Γ ⊢ if L then M else N A} →
+    Γ ⊢ L ∶ 𝔹 →
+    Γ ⊢ M ∶ A →
+    Γ ⊢ N ∶ A →
+    Γ ⊢ if L then M else N ∶ A
 
@@ -3553,205 +3557,205 @@ Much of the above, though not all, can be filled in using C-c C-r and C-c C-s.
 
 
 
-typing₁ : ∅ ⊢ not ∶ 𝔹 ⇒ 𝔹
 typing₁ = ⇒-I (𝔹-E (Ax refl) 𝔹-I₂ 𝔹-I₁)
 
 typing₂ : ∅ ⊢ two ∶ (𝔹 ⇒ 𝔹) ⇒ 𝔹 ⇒ 𝔹
-typing₂ = ⇒-I (⇒-I (⇒-E (Ax refl) (⇒-E (Ax refl) (Ax : ∅ ⊢ two ∶ (𝔹 ⇒ 𝔹) ⇒ 𝔹 ⇒ 𝔹
+typing₂ = ⇒-I (⇒-I (⇒-E (Ax refl) (⇒-E (Ax refl) (Ax refl))))
 
diff --git a/out/StlcProp.md b/out/StlcProp.md
index 86a1c3bc..e5da2069 100644
--- a/out/StlcProp.md
+++ b/out/StlcProp.md
@@ -433,7 +433,7 @@ while for boolean types they are values `true` and `false`.
       >: Term → Type  (λ[ x ∶ A ] A ⇒ canonical true for 𝔹
@@ -584,7 +584,7 @@ while for boolean types they are values `true` and `false`.
       >canonical false for 𝔹
@@ -630,7 +630,7 @@ while for boolean types they are values `true` and `false`.
       >∅ ⊢ L ∶ → Value  (Ax  (⇒-I ) value-λ  (⇒-E canonical-forms 𝔹-I₁ value-true canonical-forms 𝔹-I₂ value-false  (𝔹-E : Term M ⟹ → Value ∅ ⊢ M ∶  (Ax  (⇒-I done value-λ
@@ -1123,7 +1123,7 @@ This completes the proof.
       > (⇒-E  (ξ·₁  (ξ·₂  (βλ· progress 𝔹-I₁ done value-true
@@ -1348,7 +1348,7 @@ This completes the proof.
       >progress 𝔹-I₂ done value-false
@@ -1371,7 +1371,7 @@ This completes the proof.
       > (𝔹-E  (ξif steps βif-true
@@ -1517,7 +1517,7 @@ This completes the proof.
       >steps βif-false
 
@@ -1575,7 +1575,7 @@ instead of induction on typing derivations.
       >∅ ⊢ M ∶ → Term ∈ `  (λ[ y ∶ A ] L · L ·  (if L then M else  (if L then M else  (if L then M else → Term : Term : f ≢ x
@@ -2435,7 +2435,7 @@ Here are proofs corresponding to the first two examples above.
       >: x  (λ[ f ∶ (𝔹 ⇒ 𝔹) ] ` f · ` x): f  (λ[ f ∶ (𝔹 ⇒ 𝔹) ] ` f · ` x): x  ((λ[ f ∶ (𝔹 ⇒ 𝔹) ] ` f · ` x) · ` f): f  ((λ[ f ∶ (𝔹 ⇒ 𝔹) ] ` f · ` x) · ` f): x  (λ[ f ∶ (𝔹 ⇒ 𝔹) ] λ[ x ∶ 𝔹 ] ` f · ` x): f  (λ[ f ∶ (𝔹 ⇒ 𝔹) ] λ[ x ∶ 𝔹 ] ` f · ` x)Γ ⊢ M ∶  (Ax  (⇒-E  (⇒-E  (𝔹-E  (𝔹-E  (𝔹-E  (⇒-I ∅ ⊢ M ∶ ∅ ⊢ M ∶ Γ  ⊢ M ∶ Γ′ ⊢ M ∶  (Ax = Ax  {λ[ x ∶ A ]  (⇒-I = ⇒-I  (⇒-E = ⇒-E Γ~Γ′ 𝔹-I₁ = 𝔹-I₁
@@ -4653,7 +4653,7 @@ _Proof_: By induction on the derivation of `Γ ⊢ M ∶ A`.
       >Γ~Γ′ 𝔹-I₂ = 𝔹-I₂
@@ -4676,7 +4676,7 @@ _Proof_: By induction on the derivation of `Γ ⊢ M ∶ A`.
       > (𝔹-E = 𝔹-E ) ⊢ N ∶ ∅ ⊢ V ∶ Γ ⊢ N [ x := V ]) ∶ ∅ ⊢ V ∶ Γ ⊢ V ∶  (Ax =  Ax  {λ[ x′ ∶ A′ ] A′ ⇒  (⇒-I  (⇒-I  (λ[ x′ ∶ A′ ] = ⇒-I A ⊢ N′ ∶ ) ⊢ N′ [ x := V ] ∶  (⇒-E = ⇒-E preservation-[:=] 𝔹-I₁ = 𝔹-I₁
@@ -6296,7 +6296,7 @@ We need a couple of lemmas. A closed term can be weakened to any context, and `j
       >preservation-[:=] 𝔹-I₂ = 𝔹-I₂
@@ -6319,7 +6319,7 @@ We need a couple of lemmas. A closed term can be weakened to any context, and `j
       > (𝔹-E 
   𝔹-E ∅ ⊢ M ∶ M ⟹ ∅ ⊢ N ∶  (Ax  (⇒-I  (⇒-E (⇒-I  (βλ·  (⇒-E  (ξ·₁ = ⇒-E  (⇒-E  (ξ·₂ = ⇒-E preservation 𝔹-I₁ preservation 𝔹-I₂  (𝔹-E 𝔹-I₁ ) βif-true  (𝔹-E 𝔹-I₂ ) βif-false  (𝔹-E  (ξif = 𝔹-E : Term M ⟹ : Term ¬ Value ∅ ⊢ M ∶ M ⟹* ∅ ⊢ M ∶ M ⟹* M ∎) (_⟹⟨_⟩_ ∅ ⊢ M ∶ 
   ‶_#_