Это урезанная версия программы с этой ошибкой:
open import Data.Empty using (⊥-elim)
open import Data.Nat using (ℕ; zero; suc)
open import Data.Fin using (Fin; punchOut; punchIn; _≟_)
renaming (zero to fzero; suc to fsuc)
open import Relation.Binary.PropositionalEquality using (_≡_; refl; cong; sym)
open import Relation.Nullary using (yes; no; ¬_)
private
variable
n : ℕ
data Type : Set where
_⇒_ : Type → Type → Type
T : Type
data Term : ℕ → Set where
abs : Type → Term (suc n) → Term n
app : Term n → Term n → Term n
var : Fin n → Term n
data Ctx : ℕ → Set where
● : Ctx 0
_,-_ : Ctx n → Type → Ctx (suc n)
-- | Increments the variables that are free relative to the inserted "pivot" variable.
lift : Term n → Fin (suc n) → Term (suc n)
lift (abs ty body) v = abs ty (lift body (fsuc v))
lift (app f x) v = app (lift f v) (lift x v)
lift (var n) v = var (punchIn v n)
_[_≔_] : Term (suc n) → Fin (suc n) → Term n → Term n
(abs ty body) [ v ≔ def ] = abs ty (body [ fsuc v ≔ lift def fzero ])
(app f x) [ v ≔ def ] = app (f [ v ≔ def ]) (x [ v ≔ def ])
(var n) [ v ≔ def ] with v ≟ n
... | yes refl = def
... | no neq = var (punchOut {i = v} {j = n} λ { refl → neq (sym refl)})
find : Ctx n → Fin n → Type
find (Γ ,- A) fzero = A
find (Γ ,- A) (fsuc n) = find Γ n
private
variable
Γ : Ctx n
a b c f x : Term n
A B C : Type
v : Fin n
data _∋_⦂_ : Ctx n → Fin n → Type → Set where
vzero : (Γ ,- A) ∋ fzero ⦂ A
vsuc : (Γ ∋ v ⦂ A) → (Γ ,- B) ∋ fsuc v ⦂ A
lookup : (Γ : Ctx n) → (v : Fin n) → Γ ∋ v ⦂ find Γ v
lookup (Γ ,- A) fzero = vzero
lookup (Γ ,- B) (fsuc v) = vsuc (lookup Γ v)
data _⊢_⦂_ : Ctx n → Term n → Type → Set where
ty-abs : (Γ ,- A) ⊢ b ⦂ B → Γ ⊢ abs A b ⦂ (A ⇒ B)
ty-app : Γ ⊢ f ⦂ (A ⇒ B) → Γ ⊢ x ⦂ A → Γ ⊢ app f x ⦂ B
ty-var : Γ ∋ v ⦂ A → Γ ⊢ var v ⦂ A
-- | Inserts a binding in the middle of the context.
liftΓ : Ctx n → Fin (suc n) → Type → Ctx (suc n)
liftΓ Γ fzero t = Γ ,- t
liftΓ (Γ ,- A) (fsuc v) t = (liftΓ Γ v t) ,- A
weakening-var
: ∀ {Γ : Ctx n} {v' : Fin (suc n)} → Γ ∋ v ⦂ A → liftΓ Γ v' B ∋ Data.Fin.punchIn v' v ⦂ A
weakening-var {v' = fzero} vzero = vsuc vzero
weakening-var {v' = fsuc n} vzero = vzero
weakening-var {v' = fzero} (vsuc v) = vsuc (vsuc v)
weakening-var {v' = fsuc n} (vsuc v) = vsuc (weakening-var v)
weakening
: ∀ {Γ : Ctx n} {v : Fin (suc n)} {t : Type} → Γ ⊢ a ⦂ A → liftΓ Γ v t ⊢ lift a v ⦂ A
weakening (ty-abs body) = ty-abs (weakening body)
weakening (ty-app f x) = ty-app (weakening f) (weakening x)
weakening (ty-var v) = ty-var (weakening-var v)
lemma : ∀ {Γ : Ctx n} → (v : Fin (suc n)) → liftΓ Γ v B ∋ v ⦂ A → A ≡ B
lemma fzero vzero = refl
lemma {Γ = _ ,- _} (fsuc fin) (vsuc v) = lemma fin v
subst-eq
: (v : Fin (suc n))
→ liftΓ Γ v B ∋ v ⦂ A
→ Γ ⊢ b ⦂ B
→ Γ ⊢ var v [ v ≔ b ] ⦂ A
subst-eq fzero vzero typing = typing
subst-eq {Γ = Γ ,- C} (fsuc fin) (vsuc v) typing with fin ≟ fin
... | yes refl rewrite lemma fin v = typing
... | no neq = ⊥-elim (neq refl)
subst-neq
: (v v' : Fin (suc n))
→ liftΓ Γ v B ∋ v' ⦂ A
→ (prf : ¬ v ≡ v')
→ Γ ∋ (Data.Fin.punchOut prf) ⦂ A
subst-neq v v' v-typing neq with v ≟ v'
... | yes refl = ⊥-elim (neq refl)
subst-neq fzero fzero _ _ | no neq = ⊥-elim (neq refl)
subst-neq {Γ = Γ ,- C} fzero (fsuc fin) (vsuc v-typing) _ | no neq = v-typing
subst-neq {Γ = Γ ,- C} (fsuc fin) fzero vzero _ | no neq = vzero
subst-neq {Γ = Γ ,- C} (fsuc fin) (fsuc fin') (vsuc v-typing) neq | no _ =
vsuc (subst-neq fin fin' v-typing λ { assump → neq (cong fsuc assump) })
subst
: ∀ {Γ : Ctx n}
→ liftΓ Γ v B ⊢ a ⦂ A → Γ ⊢ b ⦂ B
→ Γ ⊢ a [ v ≔ b ] ⦂ A
subst (ty-abs body) typing = ty-abs (subst body (weakening typing))
subst (ty-app f x) typing = ty-app (subst f typing) (subst x typing)
subst {v = v} {Γ = _} (ty-var {v = v'} v-typing) typing with v' ≟ v
... | yes refl = subst-eq v v-typing typing
subst {v = fzero} (ty-var {v = fzero} v-typing) typing | no neq = ⊥-elim (neq refl)
subst {v = fzero} (ty-var {v = fsuc v'} (vsuc v-typing)) typing | no neq = ty-var v-typing
subst {v = fsuc v} {Γ = Γ ,- C} (ty-var {v = fzero} vzero) typing | no neq = ty-var vzero
subst {v = fsuc v} {Γ = Γ ,- C} (ty-var {v = fsuc v'} (vsuc v-typing)) typing | no neq
with v ≟ v'
... | yes eq = ⊥-elim (neq (cong fsuc (sym eq)))
... | no neq' = ty-var (vsuc (subst-neq v v' v-typing {!neq'!}))
Поскольку я не знаю причину ошибки, я не уверен, как воспроизвести ее в более простая программа.
Фокусировка на набранном отверстии дает:
Goal: ¬ v ≡ v'
————————————————————————————————————————————————————————————
typing : (Γ ,- C) ⊢ b ⦂ B
v-typing : liftΓ Γ v B ∋ v' ⦂ A
neq : fsuc v' ≡ fsuc v → Data.Empty.⊥
C : Type
Γ : Ctx n
b : Term (suc n) (not in scope)
A : Type (not in scope)
B : Type (not in scope)
neq' : ¬ v ≡ v'
v' : Fin (suc n)
v : Fin (suc n)
n : ℕ (not in scope)
neq' явно имеет тот же тип, что и отверстие, и никакие равенства не указаны.
Однако , когда я пытаюсь заполнить отверстие с помощью neq', я получаю следующую ошибку:
(neq' x) !=
((λ { refl
→ Relation.Nullary.Reflects.invert (Relation.Nullary.ofⁿ neq')
(Data.Fin.Properties.suc-injective (sym refl))
})
(cong fsuc x))
of type Data.Empty.⊥
when checking that the expression neq' has type ¬ v ≡ v'
Что дает?
- Откуда исходит это ограничение равенства?
- Поскольку
Data.Empty.⊥ необитаем, разве не правда ли, что все жители равны? Почему ограничение равенства имеет значение?
Я использую Agda версии 2.6.1 и стандартную библиотеку версии 1.3.