STCC-SystemT-solver: Dec (x ≈ y) for System T.

combinatory-logic/STCC-SK-solver.agda

@@ -42,32 +42,35 @@ open import Relation.Binary.HeterogeneousEquality as H
 open import STCC-SK
 
 --
--- Now the goal is to prove the decidability of ≈
--- The proof is very simple, but is based on the decidability
--- of the equality of Tm-values, which is conceptually simple
--- but is rather tedious...
+-- Now the goal is to prove the decidability of ≈ :
+--     Dec (x ≈ y)
+-- The proof is very simple, but it is based on
+--     Dec (x ≡ y)
+-- whose proof is rather tedious...
 
 --
 -- The equality of Ty-values is decidable.
 --
 
 -- ⇒-injective
 
-⇒-injective : ∀ {α₁ α₂ β₁ β₂} →
-  α₁ ⇒ β₁ ≡ α₂ ⇒ β₂ →  α₁ ≡ α₂ × β₁ ≡ β₂
+⇒-injective : ∀ {α α′ β β′} →
+  α ⇒ α′ ≡ β ⇒ β′ →  α ≡ β × α′ ≡ β′
+
 ⇒-injective refl = refl , refl
 
--- _≟ty_
+-- Dec (α ≡ β)
+
+_≟ty_ : (α β : Ty) → Dec (α ≡ β)
 
-_≟ty_ : (α₁ α₂ : Ty) → Dec (α₁ ≡ α₂)
 ⋆ ≟ty ⋆ = yes refl
-⋆ ≟ty (α₂ ⇒ α₃) = no (λ ())
-(α₁ ⇒ β₁) ≟ty ⋆ = no (λ ())
-(α₁ ⇒ β₁) ≟ty (α₂ ⇒ β₂) with α₁ ≟ty α₂
-... | no  α₁≢α₂ = no (α₁≢α₂ ∘ proj₁ ∘ ⇒-injective)
-... | yes α₁≡α₂ with β₁ ≟ty β₂
-... | no  β₁≢β₂ = no (β₁≢β₂ ∘ proj₂ ∘ ⇒-injective)
-... | yes β₁≡β₂ = yes (cong₂ _⇒_ α₁≡α₂ β₁≡β₂)
+⋆ ≟ty (β ⇒ β′) = no (λ ())
+(α ⇒ α′) ≟ty ⋆ = no (λ ())
+(α ⇒ α′) ≟ty (β ⇒ β′) with α ≟ty β
+... | no  α≢β = no (α≢β ∘ proj₁ ∘ ⇒-injective)
+... | yes α≡β with α′ ≟ty β′
+... | no  α′≢β′ = no (α′≢β′ ∘ proj₂ ∘ ⇒-injective)
+... | yes α′≡β′ = yes (cong₂ _⇒_ α≡β α′≡β′)
 
 --
 -- The equality of Tm-values is decidable.
@@ -78,24 +81,27 @@ _≟ty_ : (α₁ α₂ : Ty) → Dec (α₁ ≡ α₂)
 ∙-≅injective :
   ∀ {α α′ β β′} {x : Tm (α ⇒ α′)} {x′ : Tm α} {y : Tm (β ⇒ β′)} {y′ : Tm β} →
   x ∙ x′ ≅ y ∙ y′ →  x ≅ y × x′ ≅ y′
+
 ∙-≅injective H.refl = H.refl , H.refl
 
--- α₁ ≢ α₂ → x₁ ≇ x₂
+-- α ≢ β → x ≇ y
 
-≢ty→≇tm : ∀ {α₁} (x₁ : Tm α₁) {α₂} (x₂ : Tm α₂) → α₁ ≢ α₂ → x₁ ≇ x₂
-≢ty→≇tm K K α₁≢α₂ H.refl = α₁≢α₂ refl
-≢ty→≇tm K S α₁≢α₂ ()
-≢ty→≇tm K (x₂ ∙ y₂) α₁≢α₂ ()
-≢ty→≇tm S K α₁≢α₂ ()
-≢ty→≇tm S S α₁≢α₂ H.refl = α₁≢α₂ refl
-≢ty→≇tm S (x₂ ∙ x₃) α₁≢α₂ ()
-≢ty→≇tm (x₁ ∙ y₁) K α₁≢α₂ ()
-≢ty→≇tm (x₁ ∙ y₁) S α₁≢α₂ ()
-≢ty→≇tm (x₂ ∙ y₂) (.x₂ ∙ .y₂) α₁≢α₂ H.refl = α₁≢α₂ refl
+≢ty→≇tm : ∀ {α} (x : Tm α) {β} (y : Tm β) → α ≢ β → x ≇ y
+
+≢ty→≇tm K K α≢β H.refl = α≢β refl
+≢ty→≇tm K S α≢β ()
+≢ty→≇tm K (y ∙ y′) α≢β ()
+≢ty→≇tm S K α≢β ()
+≢ty→≇tm S S α≢β H.refl = α≢β refl
+≢ty→≇tm S (y ∙ y′) α≢β ()
+≢ty→≇tm (x ∙ x′) K α≢β ()
+≢ty→≇tm (x ∙ x′) S α≢β ()
+≢ty→≇tm (x ∙ x′) (.x ∙ .x′) α≢β H.refl = α≢β refl
 
 -- x ≅ y → α ≡ β
 
 ≅tm→≡ty : ∀ {α} (x : Tm α) {β} (y : Tm β) → x ≅ y → α ≡ β
+
 ≅tm→≡ty K K H.refl = refl
 ≅tm→≡ty K S ()
 ≅tm→≡ty K (y ∙ y′) ()
@@ -113,11 +119,13 @@ _≟ty_ : (α₁ α₂ : Ty) → Dec (α₁ ≡ α₂)
 mutual
 
   _≅tm?_ : ∀ {α} (x : Tm α) {β} (y : Tm β) → Dec (x ≅ y)
+
   _≅tm?_ {α} x {β} y with α ≟ty β
   ... | yes α≡β rewrite α≡β = x ≅tm?′ y
   ... | no  α≢β = no (≢ty→≇tm x y α≢β)
 
   _≅tm?′_ : ∀ {α} (x : Tm α) (y : Tm α) → Dec (x ≅ y)
+
   K ≅tm?′ K = yes H.refl
   K ≅tm?′ (y ∙ y′) = no (λ ())
   S ≅tm?′ S = yes H.refl
@@ -132,13 +140,15 @@ mutual
 
   ∙≅tm∙ : ∀ {α β γ} {x : Tm (α ⇒ γ)} {x′ : Tm α} {y : Tm (β ⇒ γ)} {y′ : Tm β} →
     α ≡ β → x ≅ y → x′ ≅ y′ → x ∙ x′ ≅ y ∙ y′
+
   ∙≅tm∙ α≡β x≅y x′≅y′ rewrite α≡β = H.cong₂ _∙_ x≅y x′≅y′
 
 --
 -- Dec (x ≡ y)
 --
 
 _≟tm_ : ∀ {α} (x y : Tm α) → Dec (x ≡ y)
+
 x ≟tm y with x ≅tm? y
 ... | yes x≅y = yes (≅-to-≡ x≅y)
 ... | no  x≇y = no (λ z → x≇y (≡-to-≅ z))
@@ -148,18 +158,19 @@ x ≟tm y with x ≅tm? y
 --
 
 _≈?_ : ∀ {α} (x y : Tm α) → Dec (x ≈ y)
-x ≈? y with ⟪ ⟦ x ⟧ ⟫ ≟tm ⟪ ⟦ y ⟧ ⟫
-... | yes u≡v = yes x≈y
+
+x ≈? y with norm x ≟tm norm  y
+... | yes nx≡ny = yes x≈y
   where
   open ≈-Reasoning
   x≈y = begin
     x
       ≈⟨ norm-sound x ⟩
     norm x
-      ≡⟨ u≡v ⟩
+      ≡⟨ nx≡ny ⟩
     norm y
       ≈⟨ ≈sym $ norm-sound y ⟩
     y
     ∎
-... | no  u≢v =
-  no (λ x≈y → u≢v (norm-complete x≈y))
+... | no  nx≢ny =
+  no (λ x≈y → nx≢ny (norm-complete x≈y))

combinatory-logic/STCC-SK.agda

@@ -341,7 +341,6 @@ norm-sound (x ∙ y) = begin
   ∎
   where open ≈-Reasoning
 
-
 --
 -- Reduction.
 --
@@ -377,10 +376,10 @@ reduction-example x = there ⟶S (there ⟶K here)
 -- `reify u` does return a term that cannot be reduced).
 --
 
-Normal-form : ∀ {α} (x : Tm α) → Set
-Normal-form x = ∄ (λ y → x ⟶ y)
+Irreducible : ∀ {α} (x : Tm α) → Set
+Irreducible x = ∄ (λ y → x ⟶ y)
 
-reify→nf : ∀ {α} (u : Nf α) → Normal-form (reify u)
+reify→nf : ∀ {α} (u : Nf α) → Irreducible (reify u)
 
 reify→nf K0 (y , ())
 reify→nf (K1 u) (._ , ⟶AL ())