further work on FreshId and TypedFresh

src/FreshId.lagda

@@ -44,41 +44,11 @@ Id : Set
 Id = String
 
 open Collections (Id) (String._≟_)
+\end{code}
 
-{-
-
-br : Id → String × ℕ
-br x with partition (Char._≟_ '′') (reverse (toList x))
-...     | ⟨ s , t ⟩  =  ⟨ fromList (reverse t) , length s ⟩
-
-br-lemma : (x : Id) → proj₂ (br (proj₁ (br x))) ≡ zero
-br-lemma = {!!}
-
-break : Id → Prefix × ℕ
-break x  =  ⟨ ⟨ s , br-lemma x ⟩ , n ⟩
-  where
-  s = proj₁ (br x)
-  n = proj₂ (br x)
-
-make : Prefix → ℕ → Id
-make s n  =  fromList (toList (proj₁ s) ++ replicate n '′')
-
-x0 = "x"
-x1 = "x′"
-x2 = "x′′"
-x3 = "x′′′"
-y0 = "y"
-y1 = "y′"
-zs4 = "zs′′′′"
-
-_ : fresh x0 [ x0 , x1 , x2 , zs4 ] ≡ x3
-_ = refl
-
-_ : fresh y1 [ x0 , x1 , x2 , zs4 ] ≡ y0
-_ = refl
-
--}
+## Abstract operators prefix, suffix, and make
 
+\begin{code}
 abstract
 
   data Head {A : Set} (P : A → Bool) : List A → Set where
@@ -96,8 +66,11 @@ abstract
   Prefix : Set
   Prefix = ∃[ x ] (isPrefix x)
 
+  body : Prefix → String
+  body = proj₁
+
   make : Prefix → ℕ → Id
-  make ⟨ s , pr ⟩ n = fromList (toList s ++ replicate n prime)
+  make ⟨ s , _ ⟩ n = fromList (toList s ++ replicate n prime)
 
   prefixS : Id → String
   prefixS = fromList ∘ dropWhile isPrime ∘ reverse ∘ toList
@@ -113,20 +86,22 @@ abstract
   suffix : Id → ℕ
   suffix =  length ∘ takeWhile isPrime ∘ reverse ∘ toList
 
-  prefix-lemma : ∀ {s n} → prefix (make s n) ≡ s
-  prefix-lemma {⟨ s , pr ⟩} {n} = {!!}
+  _≟Pr_ : ∀ (p q : Prefix) → Dec (body p ≡ body q)
+  p ≟Pr q = (body p) String.≟ (body q)
 
+  prefix-lemma : ∀ {p n} → prefix (make p n) ≡ p
+  prefix-lemma {p} {n} = {!!}
 
-
-  suffix-lemma : ∀ {s n} → suffix (make s n) ≡ n
+  suffix-lemma : ∀ {p n} → suffix (make p n) ≡ n
   suffix-lemma = {!!}
 
   make-lemma : ∀ {x} → make (prefix x) (suffix x) ≡ x
   make-lemma = {!!}
+\end{code}
 
-  _≟Pr_ : ∀ (s t : Prefix) → Dec (s ≡ t)
-  _≟Pr_ = {!!}
+## Basic lemmas
 
+\begin{code}
 bump : Prefix → Id → ℕ
 bump p x with p ≟Pr prefix x
 ...         | yes _  =  suc (suffix x)
@@ -139,7 +114,29 @@ fresh : Id → List Id → Id
 fresh x xs  =  make p (next p xs)
   where
   p = prefix x
+\end{code}
 
+## Test cases
+
+\begin{code}
+x0 = "x"
+x1 = "x′"
+x2 = "x′′"
+x3 = "x′′′"
+y0 = "y"
+y1 = "y′"
+zs4 = "zs′′′′"
+
+_ : fresh x0 [ x0 , x1 , x2 , zs4 ] ≡ x3
+_ = {!!}
+
+_ : fresh y1 [ x0 , x1 , x2 , zs4 ] ≡ y0
+_ = {!!}
+\end{code}
+
+## Main lemmas
+
+\begin{code}
 ⊔-lemma : ∀ {p w xs} → w ∈ xs → bump p w ≤ next p xs
 ⊔-lemma {p} {_} {_ ∷ xs} here        =  m≤m⊔n _ (next p xs)
 ⊔-lemma {p} {w} {x ∷ xs} (there x∈)  =

src/TypedFresh.lagda

@@ -288,6 +288,7 @@ free (`Y M)                  =  free M
 ### Fresh identifier
 
 \begin{code}
+
 fresh : List Id → Id
 fresh = foldr _⊔_ 0 ∘ map suc
 
@@ -993,11 +994,198 @@ _ =
    ∎
 \end{code}
 
+### An issue
+
+While executing normalise works fine, checking that the
+result is as computed takes forever.  Hence, it is commented
+out below.
+
+\begin{code}
+{-
+_ : normalise 100 ⊢four ≡
+  normal 86 (Suc (Suc (Suc (Suc Zero))))
+  ((`Y
+    (ƛ 0 ⇒
+     (ƛ 1 ⇒
+      (ƛ 2 ⇒
+       `if0 ⌊ 1 ⌋ then ⌊ 2 ⌋ else `suc ⌊ 0 ⌋ · (`pred ⌊ 1 ⌋) · ⌊ 2 ⌋))))
+   · (`suc (`suc `zero))
+   · (`suc (`suc `zero))
+   ⟶⟨ ξ-·₁ (ξ-·₁ (β-Y Fun refl)) ⟩
+   (ƛ 0 ⇒
+    (ƛ 1 ⇒
+     `if0 ⌊ 0 ⌋ then ⌊ 1 ⌋ else
+     `suc
+     (`Y
+      (ƛ 0 ⇒
+       (ƛ 1 ⇒
+        (ƛ 2 ⇒
+         `if0 ⌊ 1 ⌋ then ⌊ 2 ⌋ else `suc ⌊ 0 ⌋ · (`pred ⌊ 1 ⌋) · ⌊ 2 ⌋))))
+     · (`pred ⌊ 0 ⌋)
+     · ⌊ 1 ⌋))
+   · (`suc (`suc `zero))
+   · (`suc (`suc `zero))
+   ⟶⟨ ξ-·₁ (β-⇒ (Suc (Suc Zero))) ⟩
+   (ƛ 0 ⇒
+    `if0 `suc (`suc `zero) then ⌊ 0 ⌋ else
+    `suc
+    (`Y
+     (ƛ 1 ⇒
+      (ƛ 2 ⇒
+       (ƛ 3 ⇒
+        `if0 ⌊ 2 ⌋ then ⌊ 3 ⌋ else `suc ⌊ 1 ⌋ · (`pred ⌊ 2 ⌋) · ⌊ 3 ⌋))))
+    · (`pred (`suc (`suc `zero)))
+    · ⌊ 0 ⌋)
+   · (`suc (`suc `zero))
+   ⟶⟨ β-⇒ (Suc (Suc Zero)) ⟩
+   `if0 `suc (`suc `zero) then `suc (`suc `zero) else
+   `suc
+   (`Y
+    (ƛ 0 ⇒
+     (ƛ 1 ⇒
+      (ƛ 2 ⇒
+       `if0 ⌊ 1 ⌋ then ⌊ 2 ⌋ else `suc ⌊ 0 ⌋ · (`pred ⌊ 1 ⌋) · ⌊ 2 ⌋))))
+   · (`pred (`suc (`suc `zero)))
+   · (`suc (`suc `zero))
+   ⟶⟨ β-if0-suc (Suc Zero) ⟩
+   `suc
+   (`Y
+    (ƛ 0 ⇒
+     (ƛ 1 ⇒
+      (ƛ 2 ⇒
+       `if0 ⌊ 1 ⌋ then ⌊ 2 ⌋ else `suc ⌊ 0 ⌋ · (`pred ⌊ 1 ⌋) · ⌊ 2 ⌋))))
+   · (`pred (`suc (`suc `zero)))
+   · (`suc (`suc `zero))
+   ⟶⟨ ξ-suc (ξ-·₁ (ξ-·₁ (β-Y Fun refl))) ⟩
+   `suc
+   (ƛ 0 ⇒
+    (ƛ 1 ⇒
+     `if0 ⌊ 0 ⌋ then ⌊ 1 ⌋ else
+     `suc
+     (`Y
+      (ƛ 0 ⇒
+       (ƛ 1 ⇒
+        (ƛ 2 ⇒
+         `if0 ⌊ 1 ⌋ then ⌊ 2 ⌋ else `suc ⌊ 0 ⌋ · (`pred ⌊ 1 ⌋) · ⌊ 2 ⌋))))
+     · (`pred ⌊ 0 ⌋)
+     · ⌊ 1 ⌋))
+   · (`pred (`suc (`suc `zero)))
+   · (`suc (`suc `zero))
+   ⟶⟨ ξ-suc (ξ-·₁ (ξ-·₂ Fun (β-pred-suc (Suc Zero)))) ⟩
+   `suc
+   (ƛ 0 ⇒
+    (ƛ 1 ⇒
+     `if0 ⌊ 0 ⌋ then ⌊ 1 ⌋ else
+     `suc
+     (`Y
+      (ƛ 0 ⇒
+       (ƛ 1 ⇒
+        (ƛ 2 ⇒
+         `if0 ⌊ 1 ⌋ then ⌊ 2 ⌋ else `suc ⌊ 0 ⌋ · (`pred ⌊ 1 ⌋) · ⌊ 2 ⌋))))
+     · (`pred ⌊ 0 ⌋)
+     · ⌊ 1 ⌋))
+   · (`suc `zero)
+   · (`suc (`suc `zero))
+   ⟶⟨ ξ-suc (ξ-·₁ (β-⇒ (Suc Zero))) ⟩
+   `suc
+   (ƛ 0 ⇒
+    `if0 `suc `zero then ⌊ 0 ⌋ else
+    `suc
+    (`Y
+     (ƛ 1 ⇒
+      (ƛ 2 ⇒
+       (ƛ 3 ⇒
+        `if0 ⌊ 2 ⌋ then ⌊ 3 ⌋ else `suc ⌊ 1 ⌋ · (`pred ⌊ 2 ⌋) · ⌊ 3 ⌋))))
+    · (`pred (`suc `zero))
+    · ⌊ 0 ⌋)
+   · (`suc (`suc `zero))
+   ⟶⟨ ξ-suc (β-⇒ (Suc (Suc Zero))) ⟩
+   `suc
+   (`if0 `suc `zero then `suc (`suc `zero) else
+    `suc
+    (`Y
+     (ƛ 0 ⇒
+      (ƛ 1 ⇒
+       (ƛ 2 ⇒
+        `if0 ⌊ 1 ⌋ then ⌊ 2 ⌋ else `suc ⌊ 0 ⌋ · (`pred ⌊ 1 ⌋) · ⌊ 2 ⌋))))
+    · (`pred (`suc `zero))
+    · (`suc (`suc `zero)))
+   ⟶⟨ ξ-suc (β-if0-suc Zero) ⟩
+   `suc
+   (`suc
+    (`Y
+     (ƛ 0 ⇒
+      (ƛ 1 ⇒
+       (ƛ 2 ⇒
+        `if0 ⌊ 1 ⌋ then ⌊ 2 ⌋ else `suc ⌊ 0 ⌋ · (`pred ⌊ 1 ⌋) · ⌊ 2 ⌋))))
+    · (`pred (`suc `zero))
+    · (`suc (`suc `zero)))
+   ⟶⟨ ξ-suc (ξ-suc (ξ-·₁ (ξ-·₁ (β-Y Fun refl)))) ⟩
+   `suc
+   (`suc
+    (ƛ 0 ⇒
+     (ƛ 1 ⇒
+      `if0 ⌊ 0 ⌋ then ⌊ 1 ⌋ else
+      `suc
+      (`Y
+       (ƛ 0 ⇒
+        (ƛ 1 ⇒
+         (ƛ 2 ⇒
+          `if0 ⌊ 1 ⌋ then ⌊ 2 ⌋ else `suc ⌊ 0 ⌋ · (`pred ⌊ 1 ⌋) · ⌊ 2 ⌋))))
+      · (`pred ⌊ 0 ⌋)
+      · ⌊ 1 ⌋))
+    · (`pred (`suc `zero))
+    · (`suc (`suc `zero)))
+   ⟶⟨ ξ-suc (ξ-suc (ξ-·₁ (ξ-·₂ Fun (β-pred-suc Zero)))) ⟩
+   `suc
+   (`suc
+    (ƛ 0 ⇒
+     (ƛ 1 ⇒
+      `if0 ⌊ 0 ⌋ then ⌊ 1 ⌋ else
+      `suc
+      (`Y
+       (ƛ 0 ⇒
+        (ƛ 1 ⇒
+         (ƛ 2 ⇒
+          `if0 ⌊ 1 ⌋ then ⌊ 2 ⌋ else `suc ⌊ 0 ⌋ · (`pred ⌊ 1 ⌋) · ⌊ 2 ⌋))))
+      · (`pred ⌊ 0 ⌋)
+      · ⌊ 1 ⌋))
+    · `zero
+    · (`suc (`suc `zero)))
+   ⟶⟨ ξ-suc (ξ-suc (ξ-·₁ (β-⇒ Zero))) ⟩
+   `suc
+   (`suc
+    (ƛ 0 ⇒
+     `if0 `zero then ⌊ 0 ⌋ else
+     `suc
+     (`Y
+      (ƛ 1 ⇒
+       (ƛ 2 ⇒
+        (ƛ 3 ⇒
+         `if0 ⌊ 2 ⌋ then ⌊ 3 ⌋ else `suc ⌊ 1 ⌋ · (`pred ⌊ 2 ⌋) · ⌊ 3 ⌋))))
+     · (`pred `zero)
+     · ⌊ 0 ⌋)
+    · (`suc (`suc `zero)))
+   ⟶⟨ ξ-suc (ξ-suc (β-⇒ (Suc (Suc Zero)))) ⟩
+   `suc
+   (`suc
+    (`if0 `zero then `suc (`suc `zero) else
+     `suc
+     (`Y
+      (ƛ 0 ⇒
+       (ƛ 1 ⇒
+        (ƛ 2 ⇒
+         `if0 ⌊ 1 ⌋ then ⌊ 2 ⌋ else `suc ⌊ 0 ⌋ · (`pred ⌊ 1 ⌋) · ⌊ 2 ⌋))))
+     · (`pred `zero)
+     · (`suc (`suc `zero))))
+   ⟶⟨ ξ-suc (ξ-suc β-if0-zero) ⟩ `suc (`suc (`suc (`suc `zero))) ∎)
+_ = refl
+-}
+\end{code}
 
 ### Discussion
 
-
-
+(Notes to myself)
 
 I can remove the `ys` argument from `subst` by always
 computing it as `frees ρ M`. As I step into an abstraction,
@@ -1007,7 +1195,6 @@ its renaming gets added to `ρ`.
 
 A possible new version.
 Simpler to state, is it simpler to prove?
-
 What may be tricky to establish is that sufficient
 renaming occurs to justify the `≢` term added to `S`.
 
@@ -1041,15 +1228,13 @@ around it.
 
 I expect `⊢rename′` is easy to show.
 
-I think `⊢subst′` is true but hard to show.
+I think `⊢subst′` is hard to show, 
 The difficult part is to establish the argument to `⊢rename′`,
 since I can only create a variable that is fresh with regard to
 names in frees, not all names in the domain of `Δ`.
 
-Can I establish a counter-example, or convince myself that
-`⊢subst′` is true anyway? The latter is easily seen to be true,
-since the simpler formulations are immediate consequences of
-what I have already proved.
+Nonetheless, `⊢subst` is obviously true, since it is a corollary
+of the current version of `⊢subst`.
 
 Stepping into a subterm, just need to precompose `ρ` with a
 lemma stating that the free variables of the subterm are