Coq의 조건부에 대한 이유는 어떻게 생각합니까?

Question

나는 Coq 표준 라이브러리의 ListSet 모듈을 연구 중이다. 나는 조건문을 증명할 때 어떻게 추론 할 지 확신 할 수 없다. 예를 들어, 다음 증명에 문제가 있습니다. 정의는 문맥을 위해 제공된다.

Fixpoint set_mem (x : A) (xs : set) : bool := 
match xs with 
    | nil  => false 
    | cons y ys => 
     match Aeq_dec x y with 
     | left _ => true 
     | right _ => set_mem x ys 
     end 
end. 

Definition set_In : A -> set -> Prop := In (A := A). 

Lemma set_mem_correct1 : forall (x : A) (xs : set), 
    set_mem x xs = true -> set_In x xs. 
Proof. intros. induction xs. 
    discriminate. 
    simpl; destruct Aeq_dec with a x. 
    intuition. 
    simpl in H. 

전류 방지 상태 가설로서 Aeq_dec의 inr 포함한다. 나는 유도의 기본 경우와 inl이 Aeq_dec 인 참 귀납 경우를 버렸다.

A : Type 
    Aeq_dec : forall x y : A, {x = y} + {x <> y} 
    x : A 
    a : A 
    xs : list A 
    H : (if Aeq_dec x a then true else set_mem x xs) = true 
    IHxs : set_mem x xs = true -> set_In x xs 
    n : a <> x 
    ============================ 
    a = x \/ set_In x xs 

set_mem xs에 해당하는 경우 a <> x 경우 H 사실이 할 수있는 유일한 방법. set_mem xs을 얻으려면 H에 조건부를 a <> x에 적용 할 수 있어야합니다. 그러나, 나는 이것을하는 방법을 이해하지 못한다. 조건을 처리하거나 분해하거나 적용하려면 어떻게해야합니까?

Answer 1

시도해 보셨습니까?

destruct (Aeq_dec x a); 
[ subst; elim (n eq_refl) 
| right; apply (IHxs H) 
]. 

(if <foo>이 더 많거나 적은 같은 match <foo> with있는 그대로 (구문은 기압, 여기에는 coqtop을 버그가있을 수 있음). 당신은 (destruct, case, ...)은 경기가 될 수 있음을 감소해야 (또는 if에 대해서는 사용하는 유형의 첫 번째 또는 두 번째 생성자로 축소해야합니다.) 대부분의 경우 대/소문자 분석을 통해 값을 구해야합니다 (여기서는 아님) . 필요하다면 직접적으로 파괴하는 대신 remember (<value>) as foo; destruct foo을하십시오.)