Agda에서 유형이 비어 있음을 증명하는 것

Question

나는 agda에서 2 * 3! = 5를 증명하려고 노력하고있다. 이것을하기 위해 서명 2 * 3 ≡ 5 → ⊥를 갖는 함수를 정의 할 것입니다. 내가

1*3≡3 : 1 * 3 ≡ 3 
1*3≡3 = (succ base) znn 

및

3+3≡5 : 3 + 3 ≡ 5 → ⊥ 
3+3≡5 (sns (sns (sns()))) 

그러나 입증

data _*_≡_ : ℕ → ℕ → ℕ → Set where 
    base : ∀ {n} → 0 * n ≡ 0 
    succ : ∀ {n m k j} → m * n ≡ j → j + n ≡ k → suc m * n ≡ k 

곱셈의 나의 정의를 활용

나는 증명하려고하면

m235 : 2 * 3 ≡ 5 → ⊥ 
m235 ((succ 1*3≡3) (x)) = (3+3≡5 x) 

,

컴파일러는 X

.j != (suc 2) of type ℕ 
when checking that the expression x has type 3 + 3 ≡ 5 

이 바보 같은 질문 경우 죄송 약이 오류를 뱉어. 미리 감사드립니다.

Answer 1

우선, _+_≡_의 정의를 포함하는 것을 잊었습니다.

data _+_≡_ : ℕ → ℕ → ℕ → Set where 
    znn : ∀ {n} → 0 + n ≡ n 
    sns : ∀ {n m k} → n + m ≡ k → suc n + m ≡ suc k 

다음, 문제는 올바른 구문을 발견하지,하지만 당신은 당신이 유형 2 * 3 ≡ 5의 값에서 결론을 내릴 수있는 방법을 파악해야 : 나는 다음과 같이 그것의 가정합니다. 패턴 일치와 함께 Agda에게 오른쪽에서?로 바꾸고 Cc C를 호출하여 Cc C-를 컴파일하고 사용하여 컨텍스트를 묻는 질문을 할 수 있습니다.

m235 : 2 * 3 ≡ 5 → ⊥ 
m235 ((succ 1*3≡3) (x)) = ? 

AGDA는 말할 것이다 :

Goal : ⊥ 
----------------------------- 
x  : .j + 3 ≡ 5 
1*3≡3 : 1 * 3 ≡ .j 
.j : ℕ 

을 즉 : 당신이 (가정에서 즉 불일치) 바닥을 증명하기 위해 찾고있는 당신이 상황에서 3 개 개의 값이 있습니다. 알 수없는 번호 .j 및 .j + 3 ≡ 5에 대한 증명 자료 유형이 1 * 3 ≡ .j 인 경우 당신은 Agda가 자동으로 j가 3이되어야한다는 것을 알 수 있다고 가정하는 것처럼 보입니다. 그러나 이것은 너무 어렵습니다. 실제로 통일로부터 결론을 내리고 실제 추론을 수행하지 않습니다.

m235 : 2 * 3 ≡ 5 → ⊥ 
m235 ((succ (succ base znn)) sum) = ? 

지금은 문맥에 보이는 다음과 같습니다 : 그래서 해결책은 .j 당신은 유형 1 * 3 ≡ .j의 증거에 더 패턴 매칭하여이 작업을 수행 할 수 있습니다 3.해야하는 이유 AGDA 이해하는 데 도움이하는 것입니다

Goal: ⊥ 
———————————————————————————————————————————————————————————— 
x : 3 + 3 ≡ 5 

이제 그러한 증거가 존재 할 수없는 이전의 증명 유형 3 + 3 ≡ 5의 증거 x을 결합하여 완료 할 수 있습니다 :

m235 : 2 * 3 ≡ 5 → ⊥ 
m235 (succ (succ base znn) x) = 3+3≡5 x 

---

업데이트 : 첫 번째 읽기에서 빠졌지 만 내가 놓친 질문에 오해가 있습니다. 설명하지 못했습니다.에러는 다음과 같은 코드에 여기

m235 : 2 * 3 ≡ 5 → ⊥ 
m235 (succ 1*3≡3 x) = 3+3≡5 x 

오해 변수 이름이 항목의 좌측 1 * 3≡3 동일한 이름으로 미리 정의 된 값을 참조하지 않기 때문이다. 오히려 Agda가 동일한 유형을 가지고 있지만 그 값이 알려지지 않은 새로운 변수를 소개합니다.

당신이 AGDA 2.3.2에 도입 된 '패턴 동의어 "기능을 사용하여 얻을 수 있습니다 기대하고 있었다 : 참조 the release notes :

pattern 1*3≡3 = (succ base) znn 

m235 : 2 * 3 ≡ 5 → ⊥ 
m235 (succ 1*3≡3 x) = 3+3≡5 x 

만 패턴 동의어 패턴으로 확장된다 , 다른 값은 때로 믿을 수' 티.