coq戰術，用prop代替bools

Question

coq是否有一種證明策略，它將表達式（andb，orb，implb等）中的所有布爾操作都替換爲Propositional連接詞（和/或impl）並封裝Is_true（x）中的布爾變量x？

如果不是，我該怎麼寫？

Answer 1

你可以使用一個重寫的數據庫，例如：

Require Import Setoid. 
Require Import Bool. 

Lemma andb_prop_iff x y: Is_true (x && y) <-> Is_true x /\ Is_true y. 
Proof. 
    split; [apply andb_prop_elim | apply andb_prop_intro]. 
Qed. 

Lemma orb_prop_iff x y: Is_true (x || y) <-> Is_true x \/ Is_true y. 
Proof. 
    split; [apply orb_prop_elim | apply orb_prop_intro]. 
Qed. 

Hint Rewrite 
    andb_prop_iff 
    orb_prop_iff 
    : quotebool. 

Goal forall a b c, Is_true (a && b || c && (b || a)). 
    intros. 
    autorewrite with quotebool.