updated Fresh and FreshId

src/Fresh.lagda

@@ -42,30 +42,30 @@ open Collections (Id) (_≟_)
 prime : Id → Id
 prime x = x Str.++ "′"
 
-lemma₀ : ∀ (us : List Id) → us ++ [] ≡ us
-lemma₀ []        =  refl
-lemma₀ (u ∷ us)  =  cong (u ∷_) (lemma₀ us)
+++-identityʳ : ∀ (us : List Id) → us ++ [] ≡ us
+++-identityʳ []        =  refl
+++-identityʳ (u ∷ us)  =  cong (u ∷_) (++-identityʳ us)
 
-lemma₁ : ∀ (us vs : List Id) (v : Id) →
-  (us ++ [ v ]) ++ vs ≡ us ++ (v ∷ vs)
-lemma₁ [] vs v        =  refl
-lemma₁ (u ∷ us) vs v  =  cong (u ∷_) (lemma₁ us vs v)
+++-assoc : ∀ (us vs ws : List Id) →
+  (us ++ vs) ++ ws ≡ us ++ (vs ++ ws)
+++-assoc [] vs ws        =  refl
+++-assoc (u ∷ us) vs ws  =  cong (u ∷_) (++-assoc us vs ws)
 
-lemma₂ : ∀ (us : List Id) (v w : Id)
+lemma : ∀ (us : List Id) (v w : Id)
   → w ∉ us → w ≢ v → w ∉ (us ++ [ v ])
-lemma₂ []       v w w∉ w≢ =  λ{ here → w≢ refl
+lemma []       v w w∉ w≢ =  λ{ here → w≢ refl
                               ; (there ())
                               }
-lemma₂ (u ∷ us) v w w∉ w≢ =  λ{ here → w∉ here
-                              ; (there y∈) → (lemma₂ us v w (w∉ ∘ there) w≢) y∈
+lemma (u ∷ us) v w w∉ w≢ =  λ{ here → w∉ here
+                              ; (there y∈) → (lemma us v w (w∉ ∘ there) w≢) y∈
                               }
 
 helper : ∀ (n : ℕ) (us vs xs : List Id) (w : Id)
   → w ∉ us → us ++ vs ≡ xs → ∃[ y ]( y ∉ xs)
-helper n us []       xs w w∉ refl rewrite lemma₀ us = ⟨ w , w∉ ⟩
+helper n us []       xs w w∉ refl rewrite ++-identityʳ us = ⟨ w , w∉ ⟩
 helper n us (v ∷ vs) xs w w∉ refl with w ≟ v
 helper n us (v ∷ vs) xs w w∉ refl | no w≢
-  =  helper n (us ++ [ v ]) vs xs w (lemma₂ us v w w∉ w≢) (lemma₁ us vs v)
+  =  helper n (us ++ [ v ]) vs xs w (lemma us v w w∉ w≢) (++-assoc us [ v ] vs)
 helper (suc n) us (v ∷ vs) xs w w∉ refl | yes _
   =  helper n [] xs xs w (λ()) refl
 helper zero us (v ∷ vs) xs w w∉ refl | yes _

src/FreshId.lagda

@@ -21,7 +21,8 @@ open import Data.List using (List; []; _∷_; _++_; map; foldr; filter;
 open import Data.Nat using (ℕ; zero; suc; _+_; _∸_; _≤_; _⊔_)
 open import Data.Nat.Properties using (≤-refl; ≤-trans; m≤m⊔n; n≤m⊔n; 1+n≰n)
 open import Data.String using (String; toList; fromList; _≟_)
-open import Data.Product using (_×_; proj₁; proj₂) renaming (_,_ to ⟨_,_⟩)
+open import Data.Product using (_×_; proj₁; proj₂; ∃; ∃-syntax)
+  renaming (_,_ to ⟨_,_⟩)
 open import Data.Sum using (_⊎_; inj₁; inj₂)
 open import Function using (_∘_)
 open import Relation.Nullary using (¬_; Dec; yes; no)
@@ -41,25 +42,37 @@ Id = String
 
 open Collections (Id) (String._≟_)
 
-break : Id → String × ℕ
-break x with partition (Char._≟_ '′') (reverse (toList x))
+br : Id → String × ℕ
+br x with partition (Char._≟_ '′') (reverse (toList x))
 ... | ⟨ s , t ⟩  =  ⟨ fromList (reverse t) , length s ⟩
 
-make : String → ℕ → Id
-make s n  =  fromList (toList s ++ replicate n '′')
+Prefix : Set
+Prefix = ∃[ x ] (proj₂ (br x) ≡ zero)
 
-bump : String → Id → ℕ
-bump s x with break x
-...         | ⟨ t , n ⟩ with s String.≟ t
-...                        | yes _          = suc n
-...                        | no  _          = 0
+br-lemma : (x : Id) → proj₂ (br (proj₁ (br x))) ≡ zero
+br-lemma = {!!}
 
-next : String → List Id → ℕ
+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 '′')
+
+bump : Prefix → Id → ℕ
+bump s x with proj₁ s String.≟ proj₁ (proj₁ (break x))
+...         | yes _  =  suc (proj₂ (break x))
+...         | no  _  =  zero
+
+next : Prefix → List Id → ℕ
 next s  = foldr _⊔_ 0 ∘ map (bump s)
 
 fresh : Id → List Id → Id
-fresh x xs with break x
-...           | ⟨ s , _ ⟩ = make s (next s xs)
+fresh x xs  =  make s (next s xs)
+  where
+  s = proj₁ (break x)
 
 x0 = "x"
 x1 = "x′"
@@ -69,33 +82,43 @@ y0 = "y"
 y1 = "y′"
 zs4 = "zs′′′′"
 
-_ : break x2 ≡ ⟨ "x" , 2 ⟩
-_ = refl
-
-_ : break zs4 ≡ ⟨ "zs" , 4 ⟩
-_ = refl
-
 _ : fresh x0 [ x0 , x1 , x2 , zs4 ] ≡ x3
 _ = refl
 
 _ : fresh y1 [ x0 , x1 , x2 , zs4 ] ≡ y0
 _ = refl
 
+break-lemma₁ : ∀ {s n} → proj₁ (break (make s n)) ≡ s
+break-lemma₁ = {!!}
+
+break-lemma₂ : ∀ {s n} → proj₂ (break (make s n)) ≡ n
+break-lemma₂ = {!!}
+
+make-lemma : ∀ {x} → x ≡ make (proj₁ (break x)) (proj₂ (break x))
+make-lemma = {!!}
+
 ⊔-lemma : ∀ {s w xs} → w ∈ xs → bump s w ≤ next s xs
 ⊔-lemma {s} {_} {_ ∷ xs} here        =  m≤m⊔n _ (next s xs)
 ⊔-lemma {s} {w} {x ∷ xs} (there x∈)  =
   ≤-trans (⊔-lemma {s} {w} x∈) (n≤m⊔n (bump s x) (next s xs))
 
-{-
 bump-lemma : ∀ {s n} → bump s (make s n) ≡ suc n
-bump-lemma = {!!}
+bump-lemma {s} {n} rewrite break-lemma₁ {s} {n} | break-lemma₂ {s} {n}
+  with proj₁ s ≟ proj₁ s
+...  | yes refl rewrite break-lemma₁ {s} {n} | break-lemma₂ {s} {n} = {! refl!}
+...  | no  s≢s  = ⊥-elim (s≢s refl)
+
+fresh-lemma₁ : ∀ {s n w xs} → w ∈ xs → w ≢ fresh (make s n) xs
+fresh-lemma₁ {s} {n} {w} {xs} w∈ refl
+  with ⊔-lemma {s} {make s (next s xs)} {xs} {!!} -- w∈
+...  | prf rewrite bump-lemma {s} {next s xs} = 1+n≰n prf
 
 fresh-lemma : ∀ {x w xs} → w ∈ xs → w ≢ fresh x xs
-fresh-lemma {x} {w} {xs} w∈ w≡ with break x
-... | ⟨ s , _ ⟩ with w≡
-...    | refl with ⊔-lemma {s} {make s (next s xs)} {xs} w∈
-...        | prf rewrite bump-lemma {s} {next s xs} = 1+n≰n prf
--}
+fresh-lemma {x} {w} {xs} w∈ refl rewrite make-lemma {x}
+  = fresh-lemma₁ {s} {n} {w} {xs} {!!} {- w∈ -} {! refl!} -- refl
+  where
+  s = proj₁ (break x)
+  n = proj₂ (break x)
 \end{code}
 
 Why does `⊔-lemma` imply `fresh x xs ∉ xs`?