Agda에서 생성자가 분리되어 있습니까? (또는 inj1 x ≡ inj2 y를 증명하는 방법)

Question

Aguch에서 분해되지 않는 결합 유형 (⊎)에 대한 더 큰 정리의 일부로 inj₁ x ≡ inj₂ y이 어리 석다는 것을 나타내는 하나의 보조 정리가 필요합니다.

이 결과는 해체되고, ⊎, 즉 inj₁ 및 inj₂에 대한 두 생성자에서 직접 따를 것입니다. Agda의 사례입니까? 어떻게 증명할 수 있습니까?

open import Relation.Nullary 
open import Relation.Binary.PropositionalEquality 
open import Data.Sum 


lemma : ∀ {a b} {A : Set a} {B : Set b} {x : A} {y : B} → ¬ inj₁ x ≡ inj₂ y 
lemma eq = ? 

Answer 1

데이터 유형 생성자가 해체 있습니다

여기에 전체 보조 정리입니다. 나는 이것이 Agda의 타입 - 시스템 메타 이론의 정리라고 말하고 싶습니다.

당신은 eq 증거 (C-c C-c)를 구분하려고 할 수 있으며, AGDA는 모순을 발견 할 것이다 :

lemma : ∀ {a b} {A : Set a} {B : Set b} {x : A} {y : B} → ¬ inj₁ x ≡ inj₂ y 
lemma() 

이 행복하게-검사를 입력합니다.