From 6ba26bbfc819a6e505c90429144d70c457f66974 Mon Sep 17 00:00:00 2001 From: Peter Thiemann Date: Tue, 21 Apr 2020 14:55:12 +0200 Subject: [PATCH 1/4] Agda 2.6.1 doesn't recognize it's terminating --- src/plfa/part2/Properties.lagda.md | 1 + 1 file changed, 1 insertion(+) diff --git a/src/plfa/part2/Properties.lagda.md b/src/plfa/part2/Properties.lagda.md index fa160a4f..7b1a0d35 100644 --- a/src/plfa/part2/Properties.lagda.md +++ b/src/plfa/part2/Properties.lagda.md @@ -942,6 +942,7 @@ 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 From 8b9fc489c35f2539aac92ae3a58fca879140d50c Mon Sep 17 00:00:00 2001 From: Peter Thiemann Date: Tue, 21 Apr 2020 15:05:52 +0200 Subject: [PATCH 2/4] pragmatic note on matching against decidable equality --- src/plfa/part2/Properties.lagda.md | 8 ++++++++ 1 file changed, 8 insertions(+) diff --git a/src/plfa/part2/Properties.lagda.md b/src/plfa/part2/Properties.lagda.md index 7b1a0d35..a61c13bd 100644 --- a/src/plfa/part2/Properties.lagda.md +++ b/src/plfa/part2/Properties.lagda.md @@ -775,6 +775,14 @@ 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. +Testing variable names for equality using the `_≟_` operator has a +catch. For Agda it makes a difference whether we write `x ≟ y` or +`y ≟ x`. If the test matches the constraint that Agda expects, then the +proof goes through as demonstrated. Otherwise, Agda produces a message +that reveals the low-level implementation of string equality. To avoid +this problem, the guideline is to always match literally on the expression +on which Agda's evaluation is currently stuck. + #### Exercise `subst′` (stretch) Rewrite `subst` to work with the modified definition `_[_:=_]′` From 8da824a96aff100c19279cd1cd0abc167e8c56d9 Mon Sep 17 00:00:00 2001 From: Philip Wadler Date: Tue, 21 Apr 2020 10:50:41 -0300 Subject: [PATCH 3/4] =?UTF-8?q?Add=20paragraph=20about=20order=20of=20argu?= =?UTF-8?q?ments=20to=20`x=20=E2=89=9F=20y`?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Thank you to Peter Thiemann for suggesting a paragraph on this subject. --- src/plfa/part2/Properties.lagda.md | 14 +++++++------- 1 file changed, 7 insertions(+), 7 deletions(-) diff --git a/src/plfa/part2/Properties.lagda.md b/src/plfa/part2/Properties.lagda.md index a61c13bd..c45d0a84 100644 --- a/src/plfa/part2/Properties.lagda.md +++ b/src/plfa/part2/Properties.lagda.md @@ -775,13 +775,13 @@ 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. -Testing variable names for equality using the `_≟_` operator has a -catch. For Agda it makes a difference whether we write `x ≟ y` or -`y ≟ x`. If the test matches the constraint that Agda expects, then the -proof goes through as demonstrated. Otherwise, Agda produces a message -that reveals the low-level implementation of string equality. To avoid -this problem, the guideline is to always match literally on the expression -on which Agda's evaluation is currently stuck. +Note that 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 +that Agda knows nothing about symmetry or commutativity, which require +invoking appropriate lemmas, so it is important to think about order of +arguments and to be consistent. #### Exercise `subst′` (stretch) From 77499be10cdc4b26d45f2ee1d4d17e2a3a385b53 Mon Sep 17 00:00:00 2001 From: Philip Wadler Date: Tue, 21 Apr 2020 15:42:33 -0300 Subject: [PATCH 4/4] Modified Peter's proposed text on argument order --- src/plfa/part2/Properties.lagda.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/plfa/part2/Properties.lagda.md b/src/plfa/part2/Properties.lagda.md index c45d0a84..57f4178c 100644 --- a/src/plfa/part2/Properties.lagda.md +++ b/src/plfa/part2/Properties.lagda.md @@ -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. -Note that 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