coq тактика для замены bools с помощью Prop

Question

Есть ли тактика доказательства в coq, которая принимает все логические операции в выражении (andb, orb, implb и т. Д.) И заменяет их пропозициональными связями (и, или, impl) и инкапсулирует булевые переменные x в Is_true (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.