posets에서 null 요소의 유일성 증명에 매달려

Posets에서 사실을 구현하여 COQ를 배우려고합니다. 내 첫 번째 정리를 증명하는 동안 나는 여기에서 붙어있다.posets에서 null 요소의 유일성 증명에 매달려

Class Poset {A: Type} (leq : A -> A -> Prop) : Prop := { 
    reflexivity: forall x y : A, x = y -> (leq x y); 
    antisymmetry: forall x y : A, ((leq x y) /\ (leq y x)) -> x = y; 
    transitivity: forall x y z :A, ((leq x y) /\ (leq y z) -> (leq x z)) 
}. 

Module Poset. 
    Parameter A : Type. 
    Parameter leq : A -> A -> Prop. 
    Parameter poset : @Poset A leq. 
    Definition null_element (n : A) := 
     forall a : A, leq n a. 
    Theorem uniqueness_of_null_element (n1 : A) (n2 : A) : null_element(n1) /\ null_element(n2) -> n1 = n2. 
    Proof. 
     unfold null_element. 
    Qed. 

End Poset.

이 작업을 수행하는 방법을 잘 모르겠습니다. 누군가 도울 수 있습니까?

출처

2017-12-28 Vinothkumar Raman

'antisymmetry'를 적용하면 기본적으로 완료됩니다. 단계별 증명 :'intros [h1 h2]. antisymmetry를 적용하십시오. 스플릿. h1을 적용하십시오. apply h2.' 더 많은 숙련 된 증명. 이제는 소개 [h1 h2]; 반 비대칭을 적용하라. " – ejgallego

내가 생각했던 것보다 훨씬 간단하다. 그러나 나는 이것을 '지금'이해하지 못한다. –

접선에서 : Coq에서, 예를 들어 다음과 같이 쓰는 것이 더 관용적입니다. forall x y : A, leq x y -> leq y x -> x = y'와 같은 '반 비대칭 성' –

나는 그것을 얻었습니다. 이것은 내가 한 일입니다.

Proof. 
    unfold null_element. 
    intros [H1 H2]. 
    specialize H1 with n2. 
    specialize H2 with n1. 
    apply antisymmetry. 
    split. 
    - apply H1. 
    - apply H2. 
Qed.

출처

2017-12-28 16:09:21

'specialize'를 사용할 필요가 없습니다.'apply'는 일치를 사용하여 적절한 인스턴스를 계산할만큼 똑똑합니다. – ejgallego

'지금 intros; 반 비대칭을 적용하라. '는 보조 정리를 처리 할 수있다. '쉬운'전술 ('now '은'; 쉬운 것')은 목표를 나눌만큼 똑똑하고'apply'는 결합을 추출 할 수 있습니다. –

posets에서 null 요소의 유일성 증명에 매달려

답변

관련 문제