UniAna.util.ConvBoolTac

Require Export Coq.Bool.Bool.
Require Export Coq.Classes.EquivDec.

Lemma beq_true {A : Type} `{EqDec A} (a c : A) :
  (a ==b c) = true <-> (a === c).
Proof.
  unfold equiv_decb; destruct (a == c); firstorder auto with *.
Qed.

Lemma beq_false {A : Type} `{EqDec A} (a b : A) :
  (a ==b b) = false <-> (a =/= b).
Proof.
  unfold equiv_decb; destruct (a == b); firstorder auto with *.
Qed.

Lemma bne_true {A : Type} `{EqDec A} (a c : A) :
  (a <>b c) = true <-> (a =/= c).
Proof.
  unfold nequiv_decb, equiv_decb. rewrite negb_true_iff. destruct (a == c); firstorder auto with *.
Qed.

Lemma bne_false {A : Type} `{EqDec A} (a b : A) :
  (a <>b b) = false <-> (a === b).
Proof.
  unfold nequiv_decb, equiv_decb. rewrite negb_false_iff. destruct (a == b); firstorder auto with *.
Qed.

Definition to_bool {P Q : Prop} (x : {P} + {Q}) := if x then true else false.

Lemma to_bool_true (P : Prop) (x : {P} + {~ P}) : to_bool x = true <-> P.
Proof.
  destruct x; cbn; firstorder auto with *.
Qed.

Lemma to_bool_false (P : Prop) (x : {P} + {~P}) : to_bool x = false <-> ~ P.
Proof.
  destruct x; cbn; firstorder auto with *.
Qed.

Ltac conv_bool := repeat match goal with
                         | [ H: context[_ ==b _ = true] |- _ ] => rewrite beq_true in H
                         | [ H: context[_ ==b _ = false] |- _ ] => rewrite beq_false in H
                         | [ H: context[_ <>b _ = true] |- _ ] => rewrite bne_true in H
                         | [ H: context[_ <>b _ = false] |- _ ] => rewrite bne_false in H
                         | [ H: context[_ || _ = true] |- _ ] => rewrite orb_true_iff in H
                         | [ H: context[_ || _ = false] |- _ ] => rewrite orb_false_iff in H
                         | [ H: context[_ && _ = true] |- _ ] => rewrite andb_true_iff in H
                         | [ H: context[_ && _ = false] |- _ ] => rewrite andb_false_iff in H
                         | [ H: context[to_bool _ = true] |- _ ] => rewrite to_bool_true in H
                         | [ H: context[to_bool _ = false] |- _ ] => rewrite to_bool_false in H
                         | [ H: context[negb (_ && _)] |- _ ] => rewrite negb_andb in H
                         | [ H: context[negb (_ || _ )] |- _ ] => rewrite negb_orb in H
                         | [ |- context[_ ==b _ = true]] => rewrite beq_true
                         | [ |- context[_ ==b _ = false]] => rewrite beq_false
                         | [ |- context[_ <>b _ = true]] => rewrite bne_true
                         | [ |- context[_ <>b _ = false]] => rewrite bne_false
                         | [ |- context[_ || _ = true]] => rewrite orb_true_iff
                         | [ |- context[_ || _ = false]] => rewrite orb_false_iff
                         | [ |- context[_ && _ = true]] => rewrite andb_true_iff
                         | [ |- context[_ && _ = false]] => rewrite andb_false_iff
                         | [ |- context[to_bool _ = true]] => rewrite to_bool_true
                         | [ |- context[to_bool _ = false]] => rewrite to_bool_false
                         | [ |- context[negb (_ && _)]] => rewrite negb_andb
                         | [ |- context[negb (_ || _ )]] => rewrite negb_orb
                         end.