向阿格达证明我们在谈论同一件事

A.J.Rouvoet 发表于 Dev

AJRouvoet

我试图证明一个矛盾，但是遇到一个问题，试图向Agda证明所返回的sigma域类型<>-wt-inv与该证明前面所见的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₂

任何帮助表示赞赏

AJRouvoet

#agda频道上的Saizan足以将我指向正确的方向：使用该函数subst使用相等证明将σ替换为σ，以证明我必须从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∶φ

本文收集自互联网，转载请注明来源。

如有侵权，请联系[email protected] 删除。