Merge pull request #489 from plfa/issue488

Fix #488

extra/Issue488.agda

@@ -0,0 +1,120 @@
+module Issue488 where
+
+open import Data.Product using (∃-syntax; -,_; _×_; _,_)
+open import Relation.Nullary using (¬_)
+open import Relation.Binary.PropositionalEquality using (_≡_; refl; sym; trans)
+
+module CounterExample where
+
+  data Term : Set where
+    A B C D : Term
+
+  data _—→_ : (M N : Term) → Set where
+    B—→C : B —→ C
+    C—→B : C —→ B
+    B—→A : B —→ A
+    C—→D : C —→ D
+
+  infix  2 _—↠_
+  infix  1 begin_
+  infixr 2 _—→⟨_⟩_
+  infix  3 _∎
+
+  data _—↠_ : Term → Term → Set where
+    _∎ : ∀ M
+      ---------
+      → M —↠ M
+
+    _—→⟨_⟩_ : ∀ L {M N}
+      → L —→ M
+      → M —↠ N
+        ---------
+      → L —↠ N
+
+  begin_ : ∀ {M N}
+    → M —↠ N
+      ------
+    → M —↠ N
+  begin M—↠N = M—↠N
+
+  diamond : ∀ {L M N}
+    → ((L —→ M) × (L —→ N))
+      -----------------------------
+    → ∃[ P ] ((M —↠ P) × (N —↠ P))
+  diamond (B—→A , B—→A) = -, ((A ∎) , (A ∎))
+  diamond (C—→B , C—→B) = -, ((B ∎) , (B ∎))
+  diamond (B—→C , B—→C) = -, ((C ∎) , (C ∎))
+  diamond (C—→D , C—→D) = -, ((D ∎) , (D ∎))
+  diamond (B—→C , B—→A) = -, ((begin C —→⟨ C—→B ⟩ B —→⟨ B—→A ⟩ A ∎) , (A ∎))
+  diamond (C—→B , C—→D) = -, ((begin B —→⟨ B—→C ⟩ C —→⟨ C—→D ⟩ D ∎) , (D ∎))
+  diamond (B—→A , B—→C) = -, ((A ∎) , (begin C —→⟨ C—→B ⟩ B —→⟨ B—→A ⟩ A ∎))
+  diamond (C—→D , C—→B) = -, ((D ∎) , (begin B —→⟨ B—→C ⟩ C —→⟨ C—→D ⟩ D ∎))
+
+  A—↠A : ∀ {P} → A —↠ P → P ≡ A
+  A—↠A (.A ∎) = refl
+
+  D—↠D : ∀ {P} → D —↠ P → P ≡ D
+  D—↠D (.D ∎) = refl
+
+  ¬confluence : ¬ (∀ {L M N}
+    → ((L —↠ M) × (L —↠ N))
+      -----------------------------
+    → ∃[ P ] ((M —↠ P) × (N —↠ P)))
+  ¬confluence confluence
+    with confluence ( (begin B —→⟨ B—→A ⟩ A ∎)
+                    , (begin B —→⟨ B—→C ⟩ C —→⟨ C—→D ⟩ D ∎) )
+  ... | (P , (A—↠P , D—↠P))
+    with trans (sym (A—↠A A—↠P)) (D—↠D D—↠P)
+  ... | ()
+
+module DeterministicImpliesDiamondPropertyAndConfluence where
+
+  infix  2 _—↠_
+  infix  1 begin_
+  infixr 2 _—→⟨_⟩_
+  infix  3 _∎
+
+  postulate
+    Term : Set
+    _—→_ : Term → Term → Set
+
+  postulate
+    deterministic : ∀ {L M N}
+      → L —→ M
+      → L —→ N
+      ------
+      → M ≡ N
+
+  data _—↠_ : Term → Term → Set where
+    _∎ : ∀ M
+      ---------
+      → M —↠ M
+
+    _—→⟨_⟩_ : ∀ L {M N}
+      → L —→ M
+      → M —↠ N
+        -------
+      → L —↠ N
+
+  begin_ : ∀ {M N}
+    → M —↠ N
+      ------
+    → M —↠ N
+  begin M—↠N = M—↠N
+
+  diamond : ∀ {L M N}
+    → ((L —→ M) × (L —→ N))
+      --------------------
+    → ∃[ P ] ((M —↠ P) × (N —↠ P))
+  diamond (L—→M , L—→N)
+    rewrite deterministic L—→M L—→N = -, ((_ ∎) , (_ ∎))
+
+  confluence : ∀ {L M N}
+    → (L —↠ M)
+    → (L —↠ N)
+      --------------------
+    → ∃[ P ] ((M —↠ P) × (N —↠ P))
+  confluence {L} {.L} { N} (.L ∎) L—↠N = -, (L—↠N , (N ∎))
+  confluence {L} { M} {.L} L—↠M (.L ∎) = -, ((M ∎) , L—↠M)
+  confluence {L} { M} { N} (.L —→⟨ L—→M′ ⟩ M′—↠M) (.L —→⟨ L—→N′ ⟩ N′—↠N)
+    rewrite deterministic L—→M′ L—→N′ = confluence M′—↠M N′—↠N

src/plfa/part2/Lambda.lagda.md

@@ -53,12 +53,13 @@ four.
 ## Imports
 
 ```
-open import Relation.Binary.PropositionalEquality using (_≡_; _≢_; refl)
-open import Data.String using (String; _≟_)
-open import Data.Nat using (ℕ; zero; suc)
 open import Data.Empty using (⊥; ⊥-elim)
-open import Relation.Nullary using (Dec; yes; no; ¬_)
 open import Data.List using (List; _∷_; [])
+open import Data.Nat using (ℕ; zero; suc)
+open import Data.Product using (∃-syntax; _×_)
+open import Data.String using (String; _≟_)
+open import Relation.Nullary using (Dec; yes; no; ¬_)
+open import Relation.Binary.PropositionalEquality using (_≡_; _≢_; refl)
 ```
 
 ## Syntax of terms
@@ -582,7 +583,7 @@ replaces the formal parameter by the actual parameter.
 
 If a term is a value, then no reduction applies; conversely,
 if a reduction applies to a term then it is not a value.
-We will show in the next chapter that 
+We will show in the next chapter that
 this exhausts the possibilities: every well-typed term
 either reduces or is a value.
 
@@ -788,28 +789,33 @@ while if the top two lines stand for a single reduction
 step and the bottom two stand for zero or more reduction
 steps it is called the diamond property. In symbols:
 
-    confluence : ∀ {L M N} → ∃[ P ]
-      ( ((L —↠ M) × (L —↠ N))
-        --------------------
-      → ((M —↠ P) × (N —↠ P)) )
+```
+postulate
+  confluence : ∀ {L M N}
+    → ((L —↠ M) × (L —↠ N))
+      --------------------
+    → ∃[ P ] ((M —↠ P) × (N —↠ P))
 
-    diamond : ∀ {L M N} → ∃[ P ]
-      ( ((L —→ M) × (L —→ N))
-        --------------------
-      → ((M —↠ P) × (N —↠ P)) )
+  diamond : ∀ {L M N}
+    → ((L —→ M) × (L —→ N))
+      --------------------
+    → ∃[ P ] ((M —↠ P) × (N —↠ P))
+```
 
 The reduction system studied in this chapter is deterministic.
 In symbols:
 
-    deterministic : ∀ {L M N}
-      → L —→ M
-      → L —→ N
-        ------
-      → M ≡ N
+```
+postulate
+  deterministic : ∀ {L M N}
+    → L —→ M
+    → L —→ N
+      ------
+    → M ≡ N
+```
 
 It is easy to show that every deterministic relation satisfies
-the diamond property, and that every relation that satisfies
-the diamond property is confluent.  Hence, all the reduction
+the diamond and confluence properties. Hence, all the reduction
 systems studied in this text are trivially confluent.
 
 
@@ -1104,13 +1110,13 @@ infix  4  _⊢_⦂_
 
 data _⊢_⦂_ : Context → Term → Type → Set where
 
-  -- Axiom 
+  -- Axiom
   ⊢` : ∀ {Γ x A}
     → Γ ∋ x ⦂ A
       -----------
     → Γ ⊢ ` x ⦂ A
 
-  -- ⇒-I 
+  -- ⇒-I
   ⊢ƛ : ∀ {Γ x N A B}
     → Γ , x ⦂ A ⊢ N ⦂ B
       -------------------