차별화 된 전술은 어떻게 작동합니까?

Question

discriminate 전술이 커튼 뒤에 어떻게 작동하는지 궁금합니다. 그래서 나는 실험을했다.

먼저 간단한 유도 정의 :

Print l1. 

l1 = 
fun H : A = B => 
(fun H0 : False => False_ind False H0) 
    (eq_ind A 
    (fun e : AB => match e with 
        | A => True 
        | B => False 
        end) I B H) 
    : A = B -> False 

:

Lemma l1: A=B -> False. 
intro. 
discriminate. 
Defined. 

이의이 증거의 모습을 보자 : 다음

Inductive AB:=A|B. 

discriminate 전술에 의해 증명 될 수있는 간단한 보조 정리

이것은 다소 복잡해 보이며 여기서 무슨 일이 일어나고 있는지 이해하지 못합니다. . 따라서 좀 더 명시 적으로 같은 보조 정리를 증명하기 위해 노력 :

Lemma l2: A=B -> False. 
apply (fun e:(A=B) => match e with end). 
Defined. 

하자 다시 COQ이로 만든 것을 참조 :

Print l2. 

l2 = 
fun e : A = B => 
match 
    e as e0 in (_ = a) 
    return 
    (match a as x return (A = x -> Type) with 
    | A => fun _ : A = A => IDProp 
    | B => fun _ : A = B => False 
    end e0) 
with 
| eq_refl => idProp 
end 
    : A = B -> False 

가 지금은 완전히 혼란 스러워요. 이것은 여전히 ​​더 복잡합니다. 누군가 여기서 일어나는 일을 설명 할 수 있습니까?

Answer 1

이 l1 용어를 살펴보고 모든 부분을 설명해 보겠습니다.

fun H : A = B => 

이제 우리는 유형 False이 있어야 우리의 추상화의 몸을 구성해야합니다

l1 : A = B -> False 

l1

는 추상화 (기능)의 카레 - 하워드 대응에 의해 따라서 함의이다. discriminate 전술은 본문을 응용 프로그램 f x으로 구현하기로 선택합니다. 여기서는 f = fun H0 : False => False_ind False H0이고 False에 대한 유도 원리를 둘러싼 래퍼에 불과합니다. 이는 증명 자료가 False 인 경우 원하는 제안을 증명할 수 있음을 나타냅니다 ( False_ind : forall P : Prop, False -> P) : 우리가 베타 감소의 한 단계를 수행하면

(fun H0 : False => False_ind False H0) 
    (eq_ind A 
    (fun e : AB => match e with 
        | A => True 
        | B => False 
        end) I B H) 

, 우리는 False_ind의 첫 번째 인수는 우리가 구축하는 용어의 유형입니다

False_ind False 
      (eq_ind A 
      (fun e : AB => match e with 
          | A => True 
          | B => False 
          end) I B H) 

에 위의 단순화 것이다. A = B -> True을 증명하면 False_ind True (eq_ind A ...)이됩니다.

덧붙여서 False_ind이 작동하려면 False이라는 증거가 필요하지만 정확히 여기에서 작성하려고하는 것입니다.따라서, 우리는지고, 완전히 False_ind 제거 할 수있는 사항은 다음과 같습니다

eq_ind A 
    (fun e : AB => match e with 
       | A => True 
       | B => False 
       end) I B H 

eq_ind이 어떤지 유도 원리, 즉이 동등한 대체 할 수 일치 한 말 : 즉

eq_ind : forall (A : Type) (x : A) (P : A -> Prop), 
    P x -> forall y : A, x = y -> P y 

, 경우 하나의 증명은 P x이고, 그 다음에 모두 y은 x과 같으며, P y이됩니다.

eq_ind을 사용하여 단계별로 False이라는 증명을 만듭니다 (나중에 eq_ind A (fun e : AB ...)이라는 용어를 사용해야 함).

eq_ind으로 시작한 다음 x에 적용합니다. 그 목적으로 A을 사용합시다. 다음 술어 P이 필요합니다. P을 쓰는 동안 명심해야 할 중요한 점은 우리가 P x을 증명할 수 있어야한다는 것입니다. 이 목표는 달성하기 쉽습니다. 우리는 True 명제를 사용하려고합니다. 이는 간단한 증거입니다. 기억할 또 다른 사항은 우리가 증명하려고하는 명제 (False)입니다. 입력 매개 변수가 A이 아닌 경우이를 반환해야합니다.

fun x : AB => match x with 
       | A => True 
       | B => False 
       end 

우리는 eq_ind의 처음 두 인수를 가지고 우리는 세 더 필요 : 술어 위의 모든으로 거의 자체를 기록 True의 증거입니다 x이 A되는 지점, 즉에 대한 증거를 I. 일부 y은 우리가 증명하고자하는 명제 (예 : B)와 A = B이라는 증명 (이 답의 맨 앞에 H)을 안내합니다. 서로에 이러한 스태킹 우리는

eq_ind A 
     (fun x : AB => match x with 
        | A => True 
        | B => False 
        end) 
     I 
     B 
     H 

을 얻을 그리고 이것은 discriminate가 (일부 포장 모듈로) 우리에게 준 정확히 것입니다.

Answer 2

다른 답변은 차별 부분에 초점을 맞추고 있으며, 나는 수동 증거에 초점을 맞출 것입니다. 당신은 시도 : 지적과 COQ를 사용하여 저를 종종 불편하게한다 무엇

Lemma l2: A=B -> False. 
apply (fun e:(A=B) => match e with end). 
Defined. 

이 COQ는 내부적으로 잘 입력 한 용어로 다시 쓰는 잘못 정의 된 정의를 받아들이는 것입니다. 이것은 Coq가 일부분을 추가하기 때문에 덜 장황하게된다. 그러나 반면에, Coq는 우리가 입력 한 용어와 다른 용어를 조작합니다.

귀하의 증빙 자료입니다. 물론 e의 패턴 일치에는 eq 유형의 단일 생성자 인 생성자 eq_refl이 포함되어야합니다. 여기에서 Coq는 평등이 존재하지 않으므로 코드를 수정하는 방법을 이해하지만 입력 한 내용은 적절한 패턴 매칭이 아닙니다.

두 성분은 여기에서 무슨 일이 일어나고 있는지 이해하는 데 도움이 :

• as, in 및 return 용어

첫 번째와 eq

전체 패턴 일치 구문의 정의, 우리는 eq의 정의를 볼 수 있습니다.

이 정의는 더 자연스러운 (어떤 경우에는 더 대칭이되는) 것과 다릅니다.

Inductive eq {A : Type} : A -> A -> Prop := eq_refl : forall (x:A), x = x. 

이것은 eq는 첫 번째 정의가 아니라 두 번째로 정의하는 것이 정말 중요합니다. 특히, 우리가 겪고있는 문제에서 중요한 것은 x = y에서 x은 매개 변수이고 y은 색인 인 것입니다. 즉, x은 모든 생성자에서 일정하지만 y은 각 생성자에서 다를 수 있습니다. 유형이 Vector.t 인 경우와 동일한 차이가 있습니다. 요소를 추가하면 벡터의 요소 유형이 변경되지 않으므로 매개 변수로 구현됩니다. 그러나 크기가 변경 될 수 있으므로 인덱스로 구현됩니다.

이제 확장 패턴 일치 구문을 살펴 보겠습니다. 나는 여기서 내가 이해 한 것을 간략하게 설명한다. 더 안전한 정보에 대한 참조를 주저하지 마십시오 (https://coq.inria.fr/refman/Reference-Manual020.html). return 절은 각 분기마다 다른 리턴 유형을 지정할 때 도움이 될 수 있습니다. 이 절은 패턴 일치의 as 및 in 절에 정의 된 변수를 사용할 수 있습니다.이 변수는 일치하는 용어와 유형 인덱스를 각각 바인드합니다. return 절은이 컨텍스트를 사용하여 as 및 in의 변수를 대체하는 분기의 컨텍스트에서 해석되며 분기를 하나씩 입력 확인하고 외부 관점에서 match을 입력하는 데 사용됩니다.

Definition test n := 
    match n as n0 return (match n0 with | 0 => nat | S _ => bool end) with 
    | 0 => 17 
    | _ => true 
    end. 

n의 값에 따라, 우리는 동일한 유형을 반환되지 않습니다

은 여기 as 절 인위적인 예입니다. test의 유형은 forall n : nat, match n with | 0 => nat | S _ => bool end입니다. 그러나 Coq가 우리가 어떤 일치하는 경우를 결정할 수 있으면 유형을 단순화 할 수 있습니다. 예를 들면 다음과 같습니다

Definition test2 n : bool := test (S n). 

는 COQ는 test에게 주어진 S n 유형 bool의 무언가로 발생합니다 n, 무엇이든, 것을 알고있다.

동등 함을 위해 이번에는 in 절을 사용하여 비슷한 작업을 수행 할 수 있습니다.

Definition test3 (e:A=B) : False := 
    match e in (_ = c) return (match c with | B => False | _ => True end) with 
    | eq_refl => I 
    end. 

여기에 무슨 일이 일어나고있는가요? 기본적으로 Coq는 match 및 match 브랜치를 별도로 확인합니다.유일한 지점 eq_refl에서 c은 (매개 변수와 동일한 값으로 인덱스를 인스턴스화하는 eq_refl의 정의로 인해) A과 동일하므로 유형 True 인 여기에 I의 값이 반환되었다고 주장했습니다. 그러나 외부에서 볼 때 c은 B (e은 A=B 유형이므로)이고 return 절은 match이 False 유형의 일부 값을 반환한다고 주장합니다. 이제는 test2으로 본 유형의 패턴 일치를 단순화하기 위해 Coq의 기능을 사용합니다. 다른 케이스에서는 B보다 True을 사용했지만 특히 True은 필요하지 않습니다. eq_refl 브랜치에서 뭔가를 반환 할 수 있도록 일부 서식 만 있으면됩니다.

Coq에서 생성 된 이상한 용어로 돌아 가면 Coq에서 사용한 방법이 비슷하지만이 예제에서는 분명히 더 복잡합니다. 특히 Coq는 쓸모없는 유형과 용어가 필요한 경우 에 idProp이 자주 사용됩니다. 바로 위에 사용 된 True 및 I에 해당합니다.

마지막으로, link에 coq-club에 대한 토론을 제공하여 확장 패턴 일치가 Coq에서 어떻게 입력되었는지 이해할 수있었습니다.