From b8f07f2bb73ea9691c642fd9b32d623bda9b6780 Mon Sep 17 00:00:00 2001 From: Andres Erbsen Date: Wed, 21 Jun 2017 15:02:36 -0400 Subject: src/Demo.v: a 200-line introduction to BaseSystem ideas --- src/Util/Decidable/Bool2Prop.v | 61 ++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 61 insertions(+) create mode 100644 src/Util/Decidable/Bool2Prop.v (limited to 'src/Util/Decidable') diff --git a/src/Util/Decidable/Bool2Prop.v b/src/Util/Decidable/Bool2Prop.v new file mode 100644 index 000000000..072d5c568 --- /dev/null +++ b/src/Util/Decidable/Bool2Prop.v @@ -0,0 +1,61 @@ +Require Coq.ZArith.ZArith. + +Lemma unit_eq (x y:unit) : x = y. destruct x, y; reflexivity. Qed. +Hint Resolve unit_eq. + +Hint Extern 0 (_ = _ :> bool) => ( + match goal with + | [H:Bool.eqb ?a ?b = true |- ?a = ?b ] => apply (proj1 (Bool.eqb_true_iff _ _) H) + | [H:Bool.eqb ?b ?a = true |- ?a = ?b ] => symmetry; apply (proj1 (Bool.eqb_true_iff _ _) H) + end). + +Hint Extern 0 (_ = _ :> nat) => ( + match goal with + | [H:Nat.eqb ?a ?b = true |- ?a = ?b ] => apply (proj1 (PeanoNat.Nat.eqb_eq _ _) H) + | [H:Nat.eqb ?b ?a = true |- ?a = ?b ] => symmetry; apply (proj1 (PeanoNat.Nat.eqb_eq _ _) H) + end). + +Hint Extern 0 (_ <= _) => ( + match goal with + | [H:Nat.ltb ?a ?b = true |- ?a < ?b ] => apply (proj1 (PeanoNat.Nat.ltb_lt _ _) H) + end). + +Hint Extern 0 (_ <= _) => ( + match goal with + | [H:Nat.leb ?a ?b = true |- ?a <= ?b ] => apply (proj1 (PeanoNat.Nat.leb_le _ _) H) + end). + +Hint Extern 0 (_ = _ :> BinNums.N) => ( + match goal with + | [H:BinNat.N.eqb ?a ?b = true |- ?a = ?b ] => apply (proj1 (BinNat.N.eqb_eq _ _) H) + | [H:BinNat.N.eqb ?b ?a = true |- ?a = ?b ] => symmetry; apply (proj1 (BinNat.N.eqb_eq _ _) H) + end). +Hint Extern 0 (_ = _ :> BinInt.Z) => ( + match goal with + | [H:BinInt.Z.eqb ?a ?b = true |- ?a = ?b ] => apply (proj1 (BinInt.Z.eqb_eq _ _) H) + | [H:BinInt.Z.eqb ?a ?b = true |- ?b = ?a ] => symmetry; apply (proj1 (BinInt.Z.eqb_eq _ _) H) + end). +Hint Extern 0 (BinInt.Z.lt _ _) => ( + match goal with + | [H:BinInt.Z.ltb ?a ?b = true |- BinInt.Z.lt ?a ?b ] => apply (proj1 (BinInt.Z.ltb_lt _ _) H) + | [H:BinInt.Z.gtb ?b ?a = true |- BinInt.Z.lt ?a ?b ] => apply (proj1 (BinInt.Z.gtb_lt _ _) H) + end). +Hint Extern 0 (BinInt.Z.le _ _) => ( + match goal with + | [H:BinInt.Z.leb ?a ?b = true |- BinInt.Z.le ?a ?b ] => apply (proj1 (BinInt.Z.leb_le _ _) H) + | [H:BinInt.Z.geb ?b ?a = true |- BinInt.Z.le ?a ?b ] => apply (proj1 (BinInt.Z.geb_le _ _) H) + end). + +Hint Extern 0 (_ = _ :> BinPos.positive) => ( + match goal with + | [H:BinPos.Pos.eqb ?a ?b = true |- ?a = ?b ] => apply (proj1 (BinPos.Pos.eqb_eq _ _) H) + | [H:BinPos.Pos.eqb ?a ?b = true |- ?b = ?a ] => symmetry; apply (proj1 (BinPos.Pos.eqb_eq _ _) H) + end). +Hint Extern 0 (BinPos.Pos.lt _ _) => ( + match goal with + | [H:BinPos.Pos.ltb ?a ?b = true |- BinPos.Pos.lt ?a ?b ] => apply (proj1 (BinPos.Pos.ltb_lt _ _) H) + end). +Hint Extern 0 (BinPos.Pos.le _ _) => ( + match goal with + | [H:BinPos.Pos.leb ?a ?b = true |- BinPos.Pos.le ?a ?b ] => apply (proj1 (BinPos.Pos.leb_le _ _) H) + end). \ No newline at end of file -- cgit v1.2.3