Coq en matematiksel kanıtı dil: eğer Yeniden Yazma koşul

Question

Ben Coq en matematiksel kanıtı dilini öğrenmeye çalışıyorum, ama şu saçma açıklamaya azaltılmış bir şey kanıtlamaya çalışıyor bazı belaya girdi:

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

İşte benim girişimi:

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

Bu noktada kanıtı durumdur:

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

Şimdi, tezi kanıtlayabilmek için if koşulunu b koşulunu true'a yeniden yazmak istiyorum. Ancak,

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

bir "küçük bir adım" ve

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

bir "daha büyük bir adım" hem normal, ben durumda yeniden yazma yanlış bir şey olduğunu sanmıyorum Warning: Insufficient justification. ile başarısız rewrite -> H taktiği aynı şeyi yapacak.

Ben de bu bir işlevde if sararak sorunsuz çalışması için alabilirsiniz:

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. 

Bu elbette çok güzel değil. Yanlış bir şey yapıyorum? Orijinal kanıtımı kurtarmanın bir yolu var mı? Bu, matematiksel ispat dilinin uygulanmasının bir kusuru mu?

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

Coq < reconsider thesis as True. 

Ama bağlam içine b := true bölümünü almak için nasıl bilmiyorum:

I (https://coq.inria.fr/doc/Reference-Manual013.html de) kılavuzunda Bölüm 11.3.3 bir olasılıkla ilgili bir örnek olduğuna dikkat.

Answer 1

Olası bir çözüm (sect. 11.3.12 bakınız) b üzerine per cases kullanmaktır

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

proof anahtar kelimesi, bildiren bir prova moduna giriyor gibi görünüyor. Constrast ile, Proof anahtar kelimesi, zorunlu olan bir prova moduna girer. Bu ikinci durumda, aşağıdaki gibi kolayca kanıtlayabiliriz.

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

İlk durumda bir yanıt yok. Sizinkilere benzeyen birtakım yaklaşımları denedim ama aynı problemi tekrar tekrar buldum. Belki de bildirici kanıtlarla daha aşina olan biri tam bir cevap verebilir. Çözümü bulursanız lütfen bize bildirin! Bunun için define kullanabilirsiniz,

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. 

Ben de referans manuel örnek ispatı durumunu yeniden çalıştı: