Upgrade to Agda v2.6.1. (#492)
This commit is contained in:
Wen Kokke
GitHub
parent
3e64fa40ef
commit
0615638d66
15 changed files with 61 additions and 51 deletions
23
README.md
23
README.md
|
|
@ -6,6 +6,7 @@ permalink: /GettingStarted/
|
|||
|
||||
<!-- Links -->
|
||||
|
||||
[epub]: https://plfa.github.io/out/epub/plfa.epub
|
||||
[plfa]: http://plfa.inf.ed.ac.uk
|
||||
[plfa-dev]: https://github.com/plfa/plfa.github.io/archive/dev.zip
|
||||
[plfa-status]: https://travis-ci.org/plfa/plfa.github.io.svg?branch=dev
|
||||
|
|
@ -14,14 +15,14 @@ permalink: /GettingStarted/
|
|||
[plfa-latest]: https://github.com/plfa/plfa.github.io/releases/latest
|
||||
[plfa-master]: https://github.com/plfa/plfa.github.io/archive/master.zip
|
||||
|
||||
[agda]: https://github.com/agda/agda/releases/tag/v2.6.0.1
|
||||
[agda-version]: https://img.shields.io/badge/agda-v2.6.0.1-blue.svg
|
||||
[agda-docs-emacs-mode]: https://agda.readthedocs.io/en/v2.6.0.1/tools/emacs-mode.html
|
||||
[agda-docs-emacs-notation]: https://agda.readthedocs.io/en/v2.6.0.1/tools/emacs-mode.html#notation-for-key-combinations
|
||||
[agda-docs-package-system]: https://agda.readthedocs.io/en/v2.6.0.1/tools/package-system.html#example-using-the-standard-library
|
||||
[agda]: https://github.com/agda/agda/releases/tag/v2.6.1
|
||||
[agda-version]: https://img.shields.io/badge/agda-v2.6.1-blue.svg
|
||||
[agda-docs-emacs-mode]: https://agda.readthedocs.io/en/v2.6.1/tools/emacs-mode.html
|
||||
[agda-docs-emacs-notation]: https://agda.readthedocs.io/en/v2.6.1/tools/emacs-mode.html#notation-for-key-combinations
|
||||
[agda-docs-package-system]: https://agda.readthedocs.io/en/v2.6.1/tools/package-system.html#example-using-the-standard-library
|
||||
|
||||
[agda-stdlib-version]: https://img.shields.io/badge/agda--stdlib-v1.1-blue.svg
|
||||
[agda-stdlib]: https://github.com/agda/agda-stdlib/releases/tag/v1.1
|
||||
[agda-stdlib-version]: https://img.shields.io/badge/agda--stdlib-v1.3-blue.svg
|
||||
[agda-stdlib]: https://github.com/agda/agda-stdlib/releases/tag/v1.3
|
||||
|
||||
[haskell-stack]: https://docs.haskellstack.org/en/stable/README/
|
||||
[haskell-ghc]: https://www.haskell.org/ghc/
|
||||
|
|
@ -64,11 +65,11 @@ The easiest way to install any specific version of Agda is using [Stack][haskell
|
|||
```bash
|
||||
git clone https://github.com/agda/agda.git
|
||||
cd agda
|
||||
git checkout v2.6.0.1
|
||||
git checkout v2.6.1
|
||||
```
|
||||
To install Agda, run Stack from the Agda source directory:
|
||||
```bash
|
||||
stack install --stack-yaml stack-8.6.5.yaml
|
||||
stack install --stack-yaml stack-8.8.3.yaml
|
||||
```
|
||||
If you want Stack to use you system installation of GHC, you can pass the `--system-ghc` flag and select the appropriate `stack-*.yaml` file. For instance, if you have GHC 8.2.2 installed, run:
|
||||
```bash
|
||||
|
|
@ -81,7 +82,7 @@ You can get the required version of the Agda standard library from GitHub, eithe
|
|||
```bash
|
||||
git clone https://github.com/agda/agda-stdlib.git
|
||||
cd agda-stdlib
|
||||
git checkout v1.1
|
||||
git checkout v1.3
|
||||
```
|
||||
You can get the latest version of Programming Language Foundations in Agda from GitHub, either by cloning the repository, or by downloading [the zip archive][plfa-dev]:
|
||||
```bash
|
||||
|
|
@ -227,7 +228,7 @@ bundle exec jekyll serve
|
|||
|
||||
### Building the EPUB
|
||||
|
||||
The EPUB version of the book is built using Pandoc. Here's how to build the EPUB:
|
||||
The [EPUB version][epub] of the book is built using Pandoc. Here's how to build the EPUB:
|
||||
|
||||
1. Install a recent version of Pandoc, [available here][pandoc].
|
||||
We recommend their official installer (on the linked page),
|
||||
|
|
|
|||
|
|
@ -47,7 +47,7 @@ yourself, or your group in the case of group practicals).
|
|||
```
|
||||
import Relation.Binary.PropositionalEquality as Eq
|
||||
open Eq using (_≡_; refl; cong; sym)
|
||||
open Eq.≡-Reasoning using (begin_; _≡⟨⟩_; _≡⟨_⟩_; _∎)
|
||||
open Eq.≡-Reasoning using (begin_; _≡⟨⟩_; step-≡; _∎)
|
||||
open import Data.Nat using (ℕ; zero; suc; _+_; _*_; _∸_; _≤_; z≤n; s≤s)
|
||||
open import Data.Nat.Properties using (+-assoc; +-identityʳ; +-suc; +-comm;
|
||||
≤-refl; ≤-trans; ≤-antisym; ≤-total; +-monoʳ-≤; +-monoˡ-≤; +-mono-≤)
|
||||
|
|
@ -142,7 +142,7 @@ Give an example of an operator that has an identity and is
|
|||
associative but is not commutative.
|
||||
|
||||
|
||||
#### Exercise `finite-+-assoc` (stretch) {#finite-plus-assoc}
|
||||
#### Exercise `finite-|-assoc` (stretch) {#finite-plus-assoc}
|
||||
|
||||
Write out what is known about associativity of addition on each of the first four
|
||||
days using a finite story of creation, as
|
||||
|
|
@ -196,7 +196,7 @@ Show
|
|||
|
||||
for all naturals `n`. Did your proof require induction?
|
||||
|
||||
#### Exercise `∸-+-assoc` (practice) {#monus-plus-assoc}
|
||||
#### Exercise `∸-|-assoc` (practice) {#monus-plus-assoc}
|
||||
|
||||
Show that monus associates with addition, that is,
|
||||
|
||||
|
|
|
|||
|
|
@ -45,7 +45,7 @@ yourself, or your group in the case of group practicals).
|
|||
```
|
||||
import Relation.Binary.PropositionalEquality as Eq
|
||||
open Eq using (_≡_; refl; cong; sym)
|
||||
open Eq.≡-Reasoning using (begin_; _≡⟨⟩_; _≡⟨_⟩_; _∎)
|
||||
open Eq.≡-Reasoning using (begin_; _≡⟨⟩_; step-≡; _∎)
|
||||
open import Data.Nat using (ℕ; zero; suc; _+_; _*_; _∸_; _≤_; z≤n; s≤s)
|
||||
open import Data.Nat.Properties using (+-assoc; +-identityʳ; +-suc; +-comm;
|
||||
≤-refl; ≤-trans; ≤-antisym; ≤-total; +-monoʳ-≤; +-monoˡ-≤; +-mono-≤)
|
||||
|
|
@ -481,4 +481,3 @@ postulate
|
|||
```
|
||||
-- Your code goes here
|
||||
```
|
||||
|
||||
|
|
|
|||
|
|
@ -42,7 +42,7 @@ yourself, or your group in the case of group practicals).
|
|||
```
|
||||
import Relation.Binary.PropositionalEquality as Eq
|
||||
open Eq using (_≡_; refl; cong; sym)
|
||||
open Eq.≡-Reasoning using (begin_; _≡⟨⟩_; _≡⟨_⟩_; _∎)
|
||||
open Eq.≡-Reasoning using (begin_; _≡⟨⟩_; step-≡; _∎)
|
||||
open import Data.Bool.Base using (Bool; true; false; T; _∧_; _∨_; not)
|
||||
open import Data.Nat using (ℕ; zero; suc; _+_; _*_; _∸_; _≤_; s≤s; z≤n)
|
||||
open import Data.Nat.Properties using
|
||||
|
|
@ -538,4 +538,3 @@ Provide proofs of the three postulates, `unstuck`, `preserves`, and `wttdgs` abo
|
|||
```
|
||||
-- Your code goes here
|
||||
```
|
||||
|
||||
|
|
|
|||
|
|
@ -632,8 +632,10 @@ not fixed by the given arguments.
|
|||
## Evaluation
|
||||
|
||||
```
|
||||
data Gas : Set where
|
||||
gas : ℕ → Gas
|
||||
record Gas : Set where
|
||||
constructor gas
|
||||
field
|
||||
amount : ℕ
|
||||
|
||||
data Finished {Γ A} (N : Γ ⊢ A) : Set where
|
||||
|
||||
|
|
|
|||
|
|
@ -351,8 +351,10 @@ module Problem2 where
|
|||
### Evaluation
|
||||
|
||||
```
|
||||
data Gas : Set where
|
||||
gas : ℕ → Gas
|
||||
record Gas : Set where
|
||||
constructor gas
|
||||
field
|
||||
amount : ℕ
|
||||
|
||||
data Finished {Γ A} (N : Γ ⊢ A) : Set where
|
||||
|
||||
|
|
|
|||
|
|
@ -696,23 +696,27 @@ _∘_ : ∀ {ℓ₁ ℓ₂ ℓ₃ : Level} {A : Set ℓ₁} {B : Set ℓ₂} {C
|
|||
(g ∘ f) x = g (f x)
|
||||
```
|
||||
|
||||
Further information on levels can be found in the [Agda Wiki][wiki].
|
||||
Further information on levels can be found in the [Agda docs][docs].
|
||||
|
||||
[wiki]: http://wiki.portal.chalmers.se/agda/pmwiki.php?n=ReferenceManual.UniversePolymorphism
|
||||
[docs]: https://agda.readthedocs.io/en/v2.6.1/language/universe-levels.html
|
||||
|
||||
|
||||
## Standard library
|
||||
|
||||
Definitions similar to those in this chapter can be found in the
|
||||
standard library:
|
||||
Definitions similar to those in this chapter can be found in the standard
|
||||
library. The Agda standard library defines `_≡⟨_⟩_` as `step-≡`, [which reverses
|
||||
the order of the arguments][step-≡]. The standard library also defines a syntax
|
||||
macro, which is automatically imported whenever you import `step-≡`, which
|
||||
recovers the original argument order:
|
||||
```
|
||||
-- import Relation.Binary.PropositionalEquality as Eq
|
||||
-- open Eq using (_≡_; refl; trans; sym; cong; cong-app; subst)
|
||||
-- open Eq.≡-Reasoning using (begin_; _≡⟨⟩_; _≡⟨_⟩_; _∎)
|
||||
-- open Eq.≡-Reasoning using (begin_; _≡⟨⟩_; step-≡; _∎)
|
||||
```
|
||||
Here the imports are shown as comments rather than code to avoid
|
||||
collisions, as mentioned in the introduction.
|
||||
|
||||
[step-≡]: https://github.com/agda/agda-stdlib/blob/master/CHANGELOG/v1.3.md#changes-to-how-equational-reasoning-is-implemented
|
||||
|
||||
## Unicode
|
||||
|
||||
|
|
|
|||
|
|
@ -28,7 +28,7 @@ and some operations upon them. We also import a couple of new operations,
|
|||
```
|
||||
import Relation.Binary.PropositionalEquality as Eq
|
||||
open Eq using (_≡_; refl; cong; sym)
|
||||
open Eq.≡-Reasoning using (begin_; _≡⟨⟩_; _≡⟨_⟩_; _∎)
|
||||
open Eq.≡-Reasoning using (begin_; _≡⟨⟩_; step-≡; _∎)
|
||||
open import Data.Nat using (ℕ; zero; suc; _+_; _*_; _∸_)
|
||||
```
|
||||
|
||||
|
|
@ -656,7 +656,7 @@ time we are concerned with judgments asserting associativity:
|
|||
|
||||
Now, we apply the rules to all the judgments we know about. The base
|
||||
case tells us that `(zero + n) + p ≡ zero + (n + p)` for every natural
|
||||
`n` and `p`. The inductive case tells us that if
|
||||
`n` and `p`. The inductive case tells us that if
|
||||
`(m + n) + p ≡ m + (n + p)` (on the day before today) then
|
||||
`(suc m + n) + p ≡ suc m + (n + p)` (today).
|
||||
We didn't know any judgments about associativity before today, so that
|
||||
|
|
|
|||
|
|
@ -1106,8 +1106,8 @@ with their corresponding proofs.
|
|||
Definitions similar to those in this chapter can be found in the standard library:
|
||||
```
|
||||
import Data.List using (List; _++_; length; reverse; map; foldr; downFrom)
|
||||
import Data.List.All using (All; []; _∷_)
|
||||
import Data.List.Any using (Any; here; there)
|
||||
import Data.List.Relation.Unary.All using (All; []; _∷_)
|
||||
import Data.List.Relation.Unary.Any using (Any; here; there)
|
||||
import Data.List.Membership.Propositional using (_∈_)
|
||||
import Data.List.Properties
|
||||
using (reverse-++-commute; map-compose; map-++-commute; foldr-++)
|
||||
|
|
|
|||
|
|
@ -1043,8 +1043,10 @@ refer to preservation, since it is built-in to the definition of reduction.
|
|||
|
||||
As previously, gas is specified by a natural number:
|
||||
```
|
||||
data Gas : Set where
|
||||
gas : ℕ → Gas
|
||||
record Gas : Set where
|
||||
constructor gas
|
||||
field
|
||||
amount : ℕ
|
||||
```
|
||||
When our evaluator returns a term `N`, it will either give evidence that
|
||||
`N` is a value or indicate that it ran out of gas:
|
||||
|
|
@ -1375,4 +1377,3 @@ This chapter uses the following unicode:
|
|||
₆ U+2086 SUBSCRIPT SIX (\_6)
|
||||
₇ U+2087 SUBSCRIPT SEVEN (\_7)
|
||||
≠ U+2260 NOT EQUAL TO (\=n)
|
||||
|
||||
|
|
|
|||
|
|
@ -1089,8 +1089,10 @@ progress (case× L M) with progress L
|
|||
## Evaluation
|
||||
|
||||
```
|
||||
data Gas : Set where
|
||||
gas : ℕ → Gas
|
||||
record Gas : Set where
|
||||
constructor gas
|
||||
field
|
||||
amount : ℕ
|
||||
|
||||
data Finished {Γ A} (N : Γ ⊢ A) : Set where
|
||||
|
||||
|
|
|
|||
|
|
@ -382,7 +382,7 @@ which is well typed in the empty context is also well typed in an arbitrary
|
|||
context. The _drop_ lemma asserts that a term which is well typed in a context
|
||||
where the same variable appears twice remains well typed if we drop the shadowed
|
||||
occurrence. The _swap_ lemma asserts that a term which is well typed in a
|
||||
context remains well typed if we swap two variables.
|
||||
context remains well typed if we swap two variables.
|
||||
|
||||
(Renaming is similar to the _context invariance_ lemma in _Software
|
||||
Foundations_, but it does not require the definition of
|
||||
|
|
@ -775,7 +775,7 @@ Where the construct introduces a bound variable we need to compare it
|
|||
with the substituted variable, applying the drop lemma if they are
|
||||
equal and the swap lemma if they are distinct.
|
||||
|
||||
For Agda it makes a difference whether we write `x ≟ y` or
|
||||
For Agda it makes a difference whether we write `x ≟ y` or
|
||||
`y ≟ x`. In an interactive proof, Agda will show which residual `with`
|
||||
clauses in the definition of `_[_:=_]` need to be simplified, and the
|
||||
`with` clauses in `subst` need to match these exactly. The guideline is
|
||||
|
|
@ -918,8 +918,10 @@ per unit of gas.
|
|||
By analogy, we will use the name _gas_ for the parameter which puts a
|
||||
bound on the number of reduction steps. `Gas` is specified by a natural number:
|
||||
```
|
||||
data Gas : Set where
|
||||
gas : ℕ → Gas
|
||||
record Gas : Set where
|
||||
constructor gas
|
||||
field
|
||||
amount : ℕ
|
||||
```
|
||||
When our evaluator returns a term `N`, it will either give evidence that
|
||||
`N` is a value or indicate that it ran out of gas:
|
||||
|
|
@ -950,7 +952,6 @@ data Steps (L : Term) : Set where
|
|||
The evaluator takes gas and evidence that a term is well typed,
|
||||
and returns the corresponding steps:
|
||||
```
|
||||
{-# TERMINATING #-}
|
||||
eval : ∀ {L A}
|
||||
→ Gas
|
||||
→ ∅ ⊢ L ⦂ A
|
||||
|
|
|
|||
|
|
@ -48,7 +48,7 @@ system that _decides_ whether any two substitutions are equal.
|
|||
```
|
||||
import Relation.Binary.PropositionalEquality as Eq
|
||||
open Eq using (_≡_; refl; sym; cong; cong₂; cong-app)
|
||||
open Eq.≡-Reasoning using (begin_; _≡⟨⟩_; _≡⟨_⟩_; _∎)
|
||||
open Eq.≡-Reasoning using (begin_; _≡⟨⟩_; step-≡; _∎)
|
||||
open import Function using (_∘_)
|
||||
open import plfa.part2.Untyped
|
||||
using (Type; Context; _⊢_; ★; _∋_; ∅; _,_; Z; S_; `_; ƛ_; _·_;
|
||||
|
|
|
|||
|
|
@ -467,7 +467,7 @@ _ =
|
|||
∎
|
||||
```
|
||||
After just two steps the top-level term is an abstraction,
|
||||
and `ζ` rules drive the rest of the normalisation.
|
||||
and `ζ` rules drive the rest of the normalisation.
|
||||
|
||||
|
||||
## Progress
|
||||
|
|
@ -547,8 +547,10 @@ As previously, progress immediately yields an evaluator.
|
|||
|
||||
Gas is specified by a natural number:
|
||||
```
|
||||
data Gas : Set where
|
||||
gas : ℕ → Gas
|
||||
record Gas : Set where
|
||||
constructor gas
|
||||
field
|
||||
amount : ℕ
|
||||
```
|
||||
When our evaluator returns a term `N`, it will either give evidence that
|
||||
`N` is normal or indicate that it ran out of gas:
|
||||
|
|
|
|||
|
|
@ -54,9 +54,6 @@ down a denotational semantics of the lambda calculus.
|
|||
|
||||
## Imports
|
||||
|
||||
<!-- JGS: for equational reasoning
|
||||
open import Relation.Binary using (Setoid)
|
||||
-->
|
||||
```
|
||||
open import Agda.Primitive using (lzero; lsuc)
|
||||
open import Data.Empty using (⊥-elim)
|
||||
|
|
@ -589,7 +586,7 @@ denotation-setoid Γ = record
|
|||
-->
|
||||
<!--
|
||||
The following went inside the module ≃-Reasoning:
|
||||
|
||||
|
||||
open import Relation.Binary.Reasoning.Setoid (denotation-setoid Γ)
|
||||
renaming (begin_ to start_; _≈⟨_⟩_ to _≃⟨_⟩_; _∎ to _☐) public
|
||||
-->
|
||||
|
|
@ -854,7 +851,7 @@ Dᶜ n (a[n] ∷ ls) = (D^suc n (a[n] ∷ ls)) ↦ (vec-last (a[n] ∷ ls)) ↦
|
|||
a successor function whose denotation is given by `D^suc`,
|
||||
and the start of the path (last of the vector).
|
||||
It returns the `n + 1` vertex in the path.
|
||||
|
||||
|
||||
(D^suc (suc n) (a[n+1] ∷ a[n] ∷ ls)) ↦ (vec-last (a[n] ∷ ls)) ↦ a[n+1]
|
||||
|
||||
The exercise is to prove that for any path `ls`, the meaning of the
|
||||
|
|
@ -870,7 +867,7 @@ apply-n zero = # 0
|
|||
apply-n (suc n) = # 1 · apply-n n
|
||||
|
||||
church : (n : ℕ) → ∅ ⊢ ★
|
||||
church n = ƛ ƛ apply-n n
|
||||
church n = ƛ ƛ apply-n n
|
||||
```
|
||||
|
||||
Prove the following theorem.
|
||||
|
|
|
|||
Loading…
Reference in a new issue