부울

Question

을 포함하는이 간단한 증거를 완료하는 방법이 운동에 내 진행 여기에서이다 : https://github.com/userhr/MIT-6.826-2017

(** **** Exercise: 2 stars (andb_true_elim2) *) 
(** Prove the following claim, marking cases (and subcases) with 
    bullets when you use [destruct]. *) 

Theorem andb_true_elim2 : forall b c : bool, 
    andb b c = true -> c = true. 
Proof. 
    intros c. 
    (** Prove anything && false == false. *) 
    assert (forall x : bool, andb x false = false) as H. 
    destruct x. 
    -reflexivity. 
    -reflexivity. 
    (** Obviously true at this point since we have shown that no 
     matter what, andb b c will be false if one of them is 
     false. My idea is to use H to show that if it is to be 
     true, than both arguments must be true. 
    *) 
Qed. 

나는 그것이 내가하는 방법을 알아낼 수 없기 때문에 (forall x : bool, andb x false = false)는 것을 보여주기 위해 필요한 펠트 이유 (forall a b : bool, andb a b = true -> a = true, b = true)

Answer 1

나는이 특정 훈련에 관해서는 https://github.com/hckkid/sfsol

에서 대부분의 소프트웨어 재단 문제에 대한 솔루션을 호스팅 한 것을 증명에 의해 명백한 증거를 수행, 0123을 참조하시기 바랍니다

소프트웨어 기초를 해결 한 이후로 장이 변경되었습니다. 당신은 너무 많은 당신의 인생을 복잡하게하는

Theorem andb_true_elim2 : forall b c : bool, 
    andb b c = true -> c = true. 
Proof. 
    intros b c H. 
    destruct c. 
    Case "c = true". 
    reflexivity. 
    Case "c = false". 
    rewrite <- H. 
    destruct b. 
    SCase "b = true". 
    reflexivity. 
    SCase "b = false". 
    reflexivity. 
Qed.