From 8da824a96aff100c19279cd1cd0abc167e8c56d9 Mon Sep 17 00:00:00 2001 From: Philip Wadler Date: Tue, 21 Apr 2020 10:50:41 -0300 Subject: [PATCH] =?UTF-8?q?Add=20paragraph=20about=20order=20of=20argument?= =?UTF-8?q?s=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)