COQ 변경 전제 '동일'을 '의 부정과 같지 않은'

Question

가정하자이 같은 전제가 :

H2: ~ a b c <> a b c 

을 그리고 난 그것을 변경하려면 :

a b c = a b c 

경우

a 용어 -> 용어 -> 용어

b 및 c는 모두 용어

어떻게해야합니까? 감사!

Answer 1

당신이 ~ 및 <>의 정의를 전개하는 경우, 가설은 다음과 같은 유형이 있습니다

이

H2: (a b c = a b c -> False) -> False 

따라서, 당신이 달성하고자하는 논리 학자는 일반적으로 "이중 부정 제거"라고 부릅니다을. 그것은 intuitionistically-증명 정리하지, 따라서 COQ의 Classical 모듈 (자세한 내용은 http://coq.inria.fr/distrib/V8.4/stdlib/Coq.Logic.Classical_Prop.html 참조)에 정의되어

Classical.NNPP : forall (p : Prop), ~ ~ p -> p 

내가 실제 문제가 a b c = a b c 것보다 더 복잡하지만, 가정 언급을 위해서 실제 예를 즉시 반사적하지 않고 평등이 경우

assert (abc_refl : a b c = a b c) by reflexivity. 

---

: 그것은 당신이 정말로 특정 가설을 얻는 걱정, 당신은 안전하게에도 H2를 보지 않고 그것을 증명할 수 ctually false, 아마 당신은 H2가 어리 석다는 것을 보여주기 위해 목표를 바꾸고 싶을 것입니다. 당신은 (기본적으로 False 유형에 상처를하고있다 elim H2.) H2를 제거함으로써 그렇게 할 수 있습니다, 당신은 상황에서 종료됩니다 :

H2 : ~ a b c <> a b c 
EQ : a b c = a b c 
===================== 
False 

---

잘 모르겠어요이 모든 여부 도움이되지만 문제를 지나치게 단순화하여 실제 문제가 무엇인지 더 자세히 파악할 수는 없습니다.

Answer 2

그냥 약간의 생각은 Ptival의 대답에 추가 - 원하는 목표를 하찮게 reflexivity 해결되지 않은 경우, 당신은 여전히 ​​예를 들어, 진행은 당신이 당신의 Term에 decidable 평등을 가지고 제공 할 수있는이 작은 보조 정리 적용하여 :

을

Section S. 
    Parameter T : Type. 
    Parameter T_eq_dec : forall (x y : T), {x = y} + {x <> y}. 

    Lemma not_ne : forall (x y : T), ~ (x <> y) -> x = y. 
    Proof. 
    intros. 
    destruct (T_eq_dec x y); auto. 
    unfold not in *. 
    assert False. 
    apply (H n). 
    contradiction. 
    Qed. 
End S.