직관 주의적 정의에있어서 놀랄만 한 암시 적 가정

Question

나는 나를 놀라게하는 것을 이해하려고 노력하고있다. 다음 두 가지 정의를 고려하십시오.

Require Import List. 
Variable A:Type. 

Inductive NoDup : list A -> Prop := 
    NoDup_nil : NoDup nil 
| NoDup_cons : forall x l, ~ In x l -> NoDup l -> NoDup (x :: l). 

Inductive Dup : list A -> Prop := 
    Dup_hd : forall x l, In x l -> Dup (x :: l) 
| Dup_tl : forall x l, Dup l -> Dup (x :: l). 

내 첫 번째 직관은 똑같은 말 (하지만 부정)입니다. 그러나 @Arthur Azevedo De Amorim은 정확히 일치하지 않음을 나타냅니다 (or see here). ~ NoDup l -> Dup l 인 경우 forall (a b:A), ~ a <> b -> a = b 인 경우 여야합니다. 따라서, A 유형에 대한 추가 가정은 증명 목표를 나타낼 때 Dup이 아닌 ~ NoDup을 사용하면 잠식합니다.

나는이 여분의 가정이 도입 된 곳을 찾아 내서 무슨 일이 일어 났는지에 대한 정신적 모델을 얻으려고 노력 했으므로 다음 번에 직접 볼 것입니다.

~ In x l 용어 만 생성 할 수 있기 때문에 하나는 첫 번째 요소에서 특정 x이라고 다른을 입증 할 수 있다면 내 현재의 설명은, 그것은 책임 NoDup_cons에 ~ In x l 인수가

• 이다 나는 용어 ​​옴 유형 NoDup (_::_)을 파괴 할 때 등 목록, 목록의 두 번째 요소,

그래서 난 단지 유형생성 된 수있는 용어 ~ In _ _를 얻을 수에 대해 ~ a <> b -> a = b이 있어야합니다.

Q : 괜찮은 '비공식적 인 방식으로 생각하고 계신가요? 아니면 그것을 이해하는 더 좋은 방법이 있습니까? 그렇기 때문에 나는 다시 그 함정에 빠지지 않습니까?

또한, 나는 그들이 NoDup 대신 Dup의를 사용하여 공식화 되었기 때문에 Coq library contains NoDup하지 Dup, 그래서 아마 약간의 보조 정리, 그들은 할 필요가보다 약한 것으로 나타났습니다. 그러나 으로 공식화 될 수 있으므로 ~Dup l -> NoDup l입니다.

Answer 1

이 예제에서 알 수있는 교훈은 직관 론에서 부정을 생각할 때 좀 더주의해야한다는 것입니다. 특히 "똑같은 것을 말하지만 (부인 된)"진술은 고전 논리에서 의미가 있습니다. 즉, 또는 ~P <-> Q 중 하나를 의미합니다. 그러나 직관주의 논리에서이 두 문장은 이 아니기 때문에이 아니므로이 두 가지 중 어느 것이 맞는지에 대해 더 구체적으로 설명해야합니다.

이 경우 은이고 NoDup l은 ~ Dup l과 같습니다. 이 아닌 것은입니다. 일반적으로 Dup l은 일반적인 제안입니다 (은 ~~P -> P 인 경우 일반이라고하며이 경우 P <-> ~~P이라고 결론 지어 짐). 따라서 ~ NoDup l은 ~~ Dup l과 동일하며 일반적으로 Dup l보다 엄격하게 약합니다.

둘 사이의 차이점에 대해 생각해 볼 수있는 한 가지 방법은 구체적 증명 Dup l에서 일치 항목 l이 동일하도록 인덱스 쌍을 추출하는 것입니다 (말 그대로 함수의 의미는 아닙니다). Coq를 Prop에서 Type까지 제거하는 제한으로 인하여, 그런 인덱스 쌍이 존재한다는 사실을 분명히 증명할 수 있습니다.반면에 ~ NoDup l이라는 구체적인 증거는 단순히 NoDup l이라는 증명을 가져와 모순을 파생시킬 수있는 방법을 제공합니다.이 모순에서 특정 색인 쌍을 추출 할 수는 없습니다.

NoDup l`이 ~ Dup는 l` '에 해당`것을, 그것은 * * 사실이다