向 Agda 证明我们在谈论同一件事
Proving to Agda that we're talking about the same thing
我试图证明一个矛盾,但我 运行 试图向 Agda 证明 <>-wt-inv
返回的 sigma 域类型与前面看到的 sigma 相同证据。
我希望 uniq 类型的证明能帮到我,但我不能把它们放在一起。
我希望下面代码中的注释能提供足够的上下文。
-- given a type for (f ⟨⟩), we can derive that f is a function type
-- and we can prove that the context yields σ
⟨⟩-wt-inv : ∀ {n m f τ} {K : Ktx n m} → K ⊢ (f ⟨⟩) ∶ τ →
∃ λ σ → K Δ↝ σ × K ⊢ f ∶ (σ ⇒ τ)
⟨⟩-wt-inv (_⟨_⟩ {τ = σ} K⊢f∶σ⇒τ KΔ↝σ) = σ , (KΔ↝σ , K⊢f∶σ⇒τ)
uniq-type : ∀ {n m} {K : Ktx n m} {t τ τ'} → K ⊢ t ∶ τ → K ⊢ t ∶ τ' → τ ≡ τ'
-- excerpt from the typeof decision procedure
typeof : ∀ {n m} (K : Ktx n m) t → Dec (HasType K t)
typeof (Γ , Δ) (f ⟨⟩) with typeof (Γ , Δ) f
typeof (Γ , Δ) (f ⟨⟩) | yes (σ ⇒ τ , _) with (Δ-resolve (Γ , Δ) σ)
typeof (Γ , Δ) (f ⟨⟩) | yes (σ ⇒ τ , f∶φ) | no KΔ↝̸σ =
-- I'm trying to derive a contraction based on the fact that we've proven that
-- K Δ↝̸ σ, but assuming a type for (f ⟨⟩) will yield an instance of K Δ↝ σ' (see ⟨⟩-wt-inv)
-- the problem is that I don't know how to make agda see that σ' ≡ σ
-- such that the following typechecks.
-- (while agda will now complain that the σ in the wt-inv is not the
same one as used in the KΔ↝̸σ instance, which is sensible)
-- I think I have to use the uniq-type prove on f somewhere...
no $ KΔ↝̸σ ∘ proj₁ ∘ proj₂ ⟨⟩-wt-inv ∘ proj₂
感谢任何帮助
#agda 频道上的 Saizan 非常友善地为我指明了正确的方向:使用函数 subst
对 "substitute" σ for σ' 使用等式证明证明我必须从 KΔ↝σ' 获得 KΔ↝σ 的一个实例:
typeof (Γ , Δ) (f ⟨⟩) | yes (σ ⇒ τ , f∶φ) | no KΔ↝̸σ =
no $ KΔ↝̸σ ∘ helper
where
helper : (HasType (Γ , Δ) (f ⟨⟩)) → (Γ , Δ) Δ↝ σ
helper p with (⟨⟩-wt-inv ∘ proj₂) p
helper p | (σ' , KΔ↝σ' , f∶φ') = subst (λ s → (Γ , Δ) Δ↝ s) σ'≡σ KΔ↝σ'
where
σ'≡σ : σ' ≡ σ
σ'≡σ = ≡⇒dom $ uniq-type f∶φ' f∶φ
我试图证明一个矛盾,但我 运行 试图向 Agda 证明 <>-wt-inv
返回的 sigma 域类型与前面看到的 sigma 相同证据。
我希望 uniq 类型的证明能帮到我,但我不能把它们放在一起。
我希望下面代码中的注释能提供足够的上下文。
-- given a type for (f ⟨⟩), we can derive that f is a function type
-- and we can prove that the context yields σ
⟨⟩-wt-inv : ∀ {n m f τ} {K : Ktx n m} → K ⊢ (f ⟨⟩) ∶ τ →
∃ λ σ → K Δ↝ σ × K ⊢ f ∶ (σ ⇒ τ)
⟨⟩-wt-inv (_⟨_⟩ {τ = σ} K⊢f∶σ⇒τ KΔ↝σ) = σ , (KΔ↝σ , K⊢f∶σ⇒τ)
uniq-type : ∀ {n m} {K : Ktx n m} {t τ τ'} → K ⊢ t ∶ τ → K ⊢ t ∶ τ' → τ ≡ τ'
-- excerpt from the typeof decision procedure
typeof : ∀ {n m} (K : Ktx n m) t → Dec (HasType K t)
typeof (Γ , Δ) (f ⟨⟩) with typeof (Γ , Δ) f
typeof (Γ , Δ) (f ⟨⟩) | yes (σ ⇒ τ , _) with (Δ-resolve (Γ , Δ) σ)
typeof (Γ , Δ) (f ⟨⟩) | yes (σ ⇒ τ , f∶φ) | no KΔ↝̸σ =
-- I'm trying to derive a contraction based on the fact that we've proven that
-- K Δ↝̸ σ, but assuming a type for (f ⟨⟩) will yield an instance of K Δ↝ σ' (see ⟨⟩-wt-inv)
-- the problem is that I don't know how to make agda see that σ' ≡ σ
-- such that the following typechecks.
-- (while agda will now complain that the σ in the wt-inv is not the
same one as used in the KΔ↝̸σ instance, which is sensible)
-- I think I have to use the uniq-type prove on f somewhere...
no $ KΔ↝̸σ ∘ proj₁ ∘ proj₂ ⟨⟩-wt-inv ∘ proj₂
感谢任何帮助
#agda 频道上的 Saizan 非常友善地为我指明了正确的方向:使用函数 subst
对 "substitute" σ for σ' 使用等式证明证明我必须从 KΔ↝σ' 获得 KΔ↝σ 的一个实例:
typeof (Γ , Δ) (f ⟨⟩) | yes (σ ⇒ τ , f∶φ) | no KΔ↝̸σ =
no $ KΔ↝̸σ ∘ helper
where
helper : (HasType (Γ , Δ) (f ⟨⟩)) → (Γ , Δ) Δ↝ σ
helper p with (⟨⟩-wt-inv ∘ proj₂) p
helper p | (σ' , KΔ↝σ' , f∶φ') = subst (λ s → (Γ , Δ) Δ↝ s) σ'≡σ KΔ↝σ'
where
σ'≡σ : σ' ≡ σ
σ'≡σ = ≡⇒dom $ uniq-type f∶φ' f∶φ