diff options
author | Andres Erbsen <andreser@mit.edu> | 2017-06-21 15:02:36 -0400 |
---|---|---|
committer | Andres Erbsen <andreser@mit.edu> | 2017-06-21 15:03:39 -0400 |
commit | b8f07f2bb73ea9691c642fd9b32d623bda9b6780 (patch) | |
tree | 4c07572b09020060c93389bfb807f91bb3d53b08 /src/Util | |
parent | ac478e7dc72df91dd51586c345ac4c329f644b14 (diff) |
src/Demo.v: a 200-line introduction to BaseSystem ideas
Diffstat (limited to 'src/Util')
-rw-r--r-- | src/Util/Decidable/Bool2Prop.v | 61 | ||||
-rw-r--r-- | src/Util/ListUtil.v | 98 | ||||
-rw-r--r-- | src/Util/QUtil.v | 19 |
3 files changed, 138 insertions, 40 deletions
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 diff --git a/src/Util/ListUtil.v b/src/Util/ListUtil.v index 6c6f96761..ee4fb0b9b 100644 --- a/src/Util/ListUtil.v +++ b/src/Util/ListUtil.v @@ -19,6 +19,10 @@ Create HintDb simpl_firstn discriminated. Create HintDb simpl_skipn discriminated. Create HintDb simpl_fold_right discriminated. Create HintDb simpl_sum_firstn discriminated. +Create HintDb push_map discriminated. +Create HintDb push_flat_map discriminated. +Create HintDb push_fold_right discriminated. +Create HintDb push_partition discriminated. Create HintDb pull_nth_error discriminated. Create HintDb push_nth_error discriminated. Create HintDb pull_nth_default discriminated. @@ -70,11 +74,45 @@ Module Export List. Variables (A : Type) (B : Type). Variable f : A -> B. + Lemma map_nil : forall A B (f : A -> B), map f nil = nil. + Proof. reflexivity. Qed. Lemma map_cons (x:A)(l:list A) : map f (x::l) = (f x) :: (map f l). Proof using Type. reflexivity. Qed. End Map. + Hint Rewrite @map_cons @map_nil : push_map. + + Section FlatMap. + Lemma flat_map_nil {A B} (f:A->list B) : List.flat_map f (@nil A) = nil. + Proof. reflexivity. Qed. + Lemma flat_map_cons {A B} (f:A->list B) x xs : + (List.flat_map f (x::xs) = (f x++List.flat_map f xs))%list. + Proof. reflexivity. Qed. + End FlatMap. + Hint Rewrite @flat_map_cons @flat_map_nil : push_flat_map. + + Section FoldRight. + Context {A B} (f:B->A->A). + Lemma fold_right_nil : forall {A B} (f:B->A->A) a, + List.fold_right f a nil = a. + Proof. reflexivity. Qed. + Lemma fold_right_cons : forall a b bs, + fold_right f a (b::bs) = f b (fold_right f a bs). + Proof. reflexivity. Qed. + End FoldRight. + Hint Rewrite @fold_right_nil @fold_right_cons : simpl_fold_right push_fold_right. + + Section Partition. + Lemma partition_nil {A} (f:A->_) : partition f nil = (nil, nil). + Proof. reflexivity. Qed. + Lemma partition_cons {A} (f:A->_) x xs : partition f (x::xs) = + if f x + then (x :: (fst (partition f xs)), (snd (partition f xs))) + else ((fst (partition f xs)), x :: (snd (partition f xs))). + Proof. cbv [partition]; break_match; reflexivity. Qed. + End Partition. + Hint Rewrite @partition_nil @partition_cons : push_partition. Lemma in_seq len start n : In n (seq start len) <-> start <= n < start+len. @@ -357,22 +395,6 @@ Proof. omega. Qed. -Lemma map_nil : forall A B (f : A -> B), map f nil = nil. -Proof. reflexivity. Qed. - -(* Note: this is a duplicate of a lemma that exists in 8.5, included for - 8.4 support *) -Lemma In_nth : forall {A} (x : A) d xs, In x xs -> - exists i, i < length xs /\ nth i xs d = x. -Proof. - induction xs as [|?? IHxs]; intros; - match goal with H : In _ _ |- _ => simpl in H; destruct H end. - + subst. exists 0. simpl; split; auto || omega. - + destruct IHxs as [i [ ]]; auto. - exists (S i). - split; auto; simpl; try omega. -Qed. - Hint Rewrite @map_nth_default using omega : push_nth_default. Ltac nth_tac := @@ -481,21 +503,6 @@ Qed. Hint Rewrite @length_update_nth : distr_length. -(** TODO: this is in the stdlib in 8.5; remove this when we move to 8.5-only *) -Lemma nth_error_None : forall (A : Type) (l : list A) (n : nat), nth_error l n = None <-> length l <= n. -Proof. - intros A l n. - destruct (le_lt_dec (length l) n) as [H|H]; - split; intro H'; - try omega; - try (apply nth_error_length_error in H; tauto); - try (apply nth_error_error_length in H'; omega). -Qed. - -(** TODO: this is in the stdlib in 8.5; remove this when we move to 8.5-only *) -Lemma nth_error_Some : forall (A : Type) (l : list A) (n : nat), nth_error l n <> None <-> n < length l. -Proof. intros; rewrite nth_error_None; split; omega. Qed. - Lemma nth_set_nth : forall m {T} (xs:list T) (n:nat) x, nth_error (set_nth m x xs) n = if eq_nat_dec n m @@ -742,6 +749,17 @@ Proof. induction xs, xs', ys, ys'; boring; omega. Qed. +Lemma map_fst_combine {A B} (xs:list A) (ys:list B) : List.map fst (List.combine xs ys) = List.firstn (length ys) xs. +Proof. + revert xs; induction ys; destruct xs; simpl; solve [ trivial | congruence ]. +Qed. + +Lemma map_snd_combine {A B} (xs:list A) (ys:list B) : List.map snd (List.combine xs ys) = List.firstn (length xs) ys. +Proof. + revert xs; induction ys; destruct xs; simpl; solve [ trivial | congruence ]. +Qed. +Hint Rewrite @map_fst_combine @map_snd_combine : push_map. + Lemma skipn_nil : forall {A} n, skipn n nil = @nil A. Proof. destruct n; auto. Qed. @@ -873,14 +891,6 @@ Qed. Hint Rewrite @skipn_length : distr_length. -Lemma fold_right_cons : forall {A B} (f:B->A->A) a b bs, - fold_right f a (b::bs) = f b (fold_right f a bs). -Proof. - reflexivity. -Qed. - -Hint Rewrite @fold_right_cons : simpl_fold_right. - Lemma length_cons : forall {T} (x:T) xs, length (x::xs) = S (length xs). reflexivity. Qed. @@ -1456,6 +1466,14 @@ induction m; intros. omega. Qed. +Lemma nth_default_seq_inbounds d s n i (H:(i < n)%nat) : + List.nth_default d (List.seq s n) i = (s+i)%nat. +Proof. + progress cbv [List.nth_default]. + rewrite nth_error_seq. + break_innermost_match; solve [ trivial | omega ]. +Qed. +Hint Rewrite @nth_default_seq_inbounds using lia : push_nth_default. Lemma sum_firstn_prefix_le' : forall l n m, (forall x, In x l -> (0 <= x)%Z) -> (sum_firstn l n <= sum_firstn l (n + m))%Z. @@ -1756,4 +1774,4 @@ Lemma map2_map {A B C A' B'} (f:A -> B -> C) (g:A' -> A) (h:B' -> B) (xs:list A' Proof. revert ys; induction xs as [|a xs IHxs]; destruct ys; intros; try reflexivity; []. simpl. rewrite IHxs. reflexivity. -Qed. +Qed.
\ No newline at end of file diff --git a/src/Util/QUtil.v b/src/Util/QUtil.v new file mode 100644 index 000000000..453cad308 --- /dev/null +++ b/src/Util/QUtil.v @@ -0,0 +1,19 @@ +Require Import Coq.ZArith.ZArith Coq.QArith.QArith QArith.Qround. + +Local Open Scope Z_scope. + +Lemma pow_ceil_mul_nat_nonzero b f + (b_nz:b <> 0) + (f_pos:(0 <= f)%Q) + : forall i, b^Qceiling (f * inject_Z (Z.of_nat i)) <> 0. +Proof. + intros. + eapply Z.pow_nonzero; try omega. + rewrite Zle_Qle. + eapply Qle_trans; [|eapply Qle_ceiling]. + eapply Qle_trans; [|eapply (Qmult_le_compat_r 0)]; trivial. + cbv; discriminate. + apply (Qle_trans _ (inject_Z 0)); [eapply Qle_refl|]. + rewrite <-Zle_Qle. + eapply Zle_0_nat. +Qed.
\ No newline at end of file |