Coq của: Viết lại nhập nếu tình trạng

Question

Tôi đang cố gắng tìm hiểu ngôn ngữ bằng chứng toán học Coq, nhưng tôi chạy vào một số rắc rối cố gắng để chứng minh một cái gì đó mà tôi giảm xuống còn tuyên bố ngớ ngẩn sau đây:

Lemma foo: forall b: bool, b = true -> (if b then 0 else 1) = 0. 

Dưới đây là nỗ lực của tôi:

proof. 
    let b: bool. 
    let H: (b = true). 

Tại thời điểm này tình trạng giấy tờ chứng minh là:

b : bool 
    H : b = true 
    ============================ 
    thesis := 
    (if b then 0 else 1) = 0 

Bây giờ tôi muốn viết lại điều kiện ifb đến true để có thể chứng minh luận án. Tuy nhiên, cả một "bước nhỏ" của

have ((if b then 0 else 1) = (if true then 0 else 1)) by H. 

và một "bước lớn" của

have ((if b then 0 else 1) = 0) by H. 

thất bại với Warning: Insufficient justification. Tôi không nghĩ rằng có điều gì sai trái với việc viết lại trong tình trạng này, như bình thường rewrite -> H chiến thuật sẽ thực hiện tương tự.

Tôi cũng có thể được điều này để làm việc mà không vấn đề bằng cách gói if trong một chức năng:

Definition ite (cond: bool) (a b: nat) := if cond then a else b. 
Lemma bar: forall b: bool, b = true -> (ite b 0 1) = 0. 
proof. 
    let b: bool. let H: (b = true). 
    have (ite b 0 1 = ite true 0 1) by H. thus ~= 0. 
end proof. 

Đây không phải là rất tốt đẹp, tất nhiên. Tôi có làm gì sai không? Có cách nào để giải cứu bằng chứng gốc của tôi không? Đây có phải chỉ là một thiếu sót của việc thực hiện ngôn ngữ chứng minh toán học?

Tôi lưu ý rằng có một ví dụ có thể có liên quan tại mục 11.3.3 của cuốn cẩm nang (tại https://coq.inria.fr/doc/Reference-Manual013.html):

a := false : bool 
    b := true : bool 
    H : False 
    ============================ 
    thesis := 
    if b then True else False 

Coq < reconsider thesis as True. 

Nhưng tôi không biết làm thế nào để có được những phần b := true vào ngữ cảnh.

Answer 1

Một giải pháp khả thi là sử dụng per cases trên b (xem sect. 11.3.12):

Lemma foo: 
    forall b: bool, b = true -> (if b then 0 else 1) = 0. 
proof. 
    let b : bool. 
    per cases on b. 
    suppose it is true. thus thesis. 
    suppose it is false. thus thesis. 
    end cases. 
end proof. 
Qed. 

Tôi cũng đã cố gắng để tái tạo tình trạng bằng chứng về hướng dẫn tham khảo ví dụ của bạn, bạn có thể sử dụng define cho rằng:

Lemma manual_11_3_3 : 
    if false then True else False -> 
    if true then True else False. 
proof. 
    define a as false. 
    define b as true. 
    assume H : (if a then True else False). 
    reconsider H as False. 
    reconsider thesis as True. 
Abort. 

Answer 2

Dường như từ khóa proof nhập vào chế độ bằng chứng khai báo. Theo constrast, từ khóa Proof nhập vào một chế độ bằng chứng bắt buộc. Trong trường hợp thứ hai này, chúng ta có thể chứng minh nó dễ dàng như sau.

Lemma foo: forall b: bool, b = true -> (if b then 0 else 1) = 0.          
Proof.                        
    intros b H.                      
    rewrite H.                       
    reflexivity.                      
Qed. 

Trong trường hợp đầu tiên, tôi không có câu trả lời. Tôi đã thử một số phương pháp tiếp cận tương tự như của bạn nhưng tìm thấy cùng một vấn đề một lần nữa và một lần nữa. Có lẽ ai đó quen thuộc hơn với các bằng chứng khai báo có thể đưa ra câu trả lời đầy đủ. Vui lòng cho chúng tôi biết nếu bạn tìm thấy giải pháp!