Skip to content

Commit 54c037b

Browse files
kit-ty-katekit-ty-kate
committed
Setup benchark tests using Coq standard library
1 parent ab4f486 commit 54c037b

File tree

409 files changed

+159032
-1
lines changed

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

409 files changed

+159032
-1
lines changed

‎GNUmakefile

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -14,3 +14,7 @@ check:
1414
cleanall::
1515
@ $(MAKE) --silent clean
1616
@ $(MAKE) --silent -C tests clean
17+
@ $(MAKE) --silent -C stdlib-bench clean
18+
19+
bench:
20+
@ $(MAKE) --silent -C stdlib-benchs

‎scripts/hooks/pre-commit

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -46,7 +46,7 @@ EOF
4646
fi
4747

4848
# If there are whitespace errors, print the offending file names and fail.
49-
git diff-index --check --cached $against -- || exit 1
49+
git diff-index --check --cached $against -- `git ls-files | grep -Ev "^stdlib-benchs/.*.v$"` || exit 1
5050

5151

5252
## Custom rules

‎stdlib-benchs/Arith/Arith.v

Lines changed: 10 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,10 @@
1+
(************************************************************************)
2+
(* v * The Coq Proof Assistant / The Coq Development Team *)
3+
(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *)
4+
(* \VV/ **************************************************************)
5+
(* // * This file is distributed under the terms of the *)
6+
(* * GNU Lesser General Public License Version 2.1 *)
7+
(************************************************************************)
8+
9+
Require Export Arith_base.
10+
Require Export ArithRing.

‎stdlib-benchs/Arith/Arith_base.v

Lines changed: 22 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,22 @@
1+
(************************************************************************)
2+
(* v * The Coq Proof Assistant / The Coq Development Team *)
3+
(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *)
4+
(* \VV/ **************************************************************)
5+
(* // * This file is distributed under the terms of the *)
6+
(* * GNU Lesser General Public License Version 2.1 *)
7+
(************************************************************************)
8+
9+
Require Export PeanoNat.
10+
11+
Require Export Le.
12+
Require Export Lt.
13+
Require Export Plus.
14+
Require Export Gt.
15+
Require Export Minus.
16+
Require Export Mult.
17+
Require Export Between.
18+
Require Export Peano_dec.
19+
Require Export Compare_dec.
20+
Require Export Factorial.
21+
Require Export EqNat.
22+
Require Export Wf_nat.

‎stdlib-benchs/Arith/Between.v

Lines changed: 187 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,187 @@
1+
(************************************************************************)
2+
(* v * The Coq Proof Assistant / The Coq Development Team *)
3+
(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *)
4+
(* \VV/ **************************************************************)
5+
(* // * This file is distributed under the terms of the *)
6+
(* * GNU Lesser General Public License Version 2.1 *)
7+
(************************************************************************)
8+
9+
Require Import Le.
10+
Require Import Lt.
11+
12+
Local Open Scope nat_scope.
13+
14+
Implicit Types k l p q r : nat.
15+
16+
Section Between.
17+
Variables P Q : nat -> Prop.
18+
19+
Inductive between k : nat -> Prop :=
20+
| bet_emp : between k k
21+
| bet_S : forall l, between k l -> P l -> between k (S l).
22+
23+
Hint Constructors between: arith v62.
24+
25+
Lemma bet_eq : forall k l, l = k -> between k l.
26+
Proof.
27+
induction 1; auto with arith.
28+
Qed.
29+
30+
Hint Resolve bet_eq: arith v62.
31+
32+
Lemma between_le : forall k l, between k l -> k <= l.
33+
Proof.
34+
induction 1; auto with arith.
35+
Qed.
36+
Hint Immediate between_le: arith v62.
37+
38+
Lemma between_Sk_l : forall k l, between k l -> S k <= l -> between (S k) l.
39+
Proof.
40+
intros k l H; induction H as [|l H].
41+
intros; absurd (S k <= k); auto with arith.
42+
destruct H; auto with arith.
43+
Qed.
44+
Hint Resolve between_Sk_l: arith v62.
45+
46+
Lemma between_restr :
47+
forall k l (m:nat), k <= l -> l <= m -> between k m -> between l m.
48+
Proof.
49+
induction 1; auto with arith.
50+
Qed.
51+
52+
Inductive exists_between k : nat -> Prop :=
53+
| exists_S : forall l, exists_between k l -> exists_between k (S l)
54+
| exists_le : forall l, k <= l -> Q l -> exists_between k (S l).
55+
56+
Hint Constructors exists_between: arith v62.
57+
58+
Lemma exists_le_S : forall k l, exists_between k l -> S k <= l.
59+
Proof.
60+
induction 1; auto with arith.
61+
Qed.
62+
63+
Lemma exists_lt : forall k l, exists_between k l -> k < l.
64+
Proof exists_le_S.
65+
Hint Immediate exists_le_S exists_lt: arith v62.
66+
67+
Lemma exists_S_le : forall k l, exists_between k (S l) -> k <= l.
68+
Proof.
69+
intros; apply le_S_n; auto with arith.
70+
Qed.
71+
Hint Immediate exists_S_le: arith v62.
72+
73+
Definition in_int p q r := p <= r /\ r < q.
74+
75+
Lemma in_int_intro : forall p q r, p <= r -> r < q -> in_int p q r.
76+
Proof.
77+
red; auto with arith.
78+
Qed.
79+
Hint Resolve in_int_intro: arith v62.
80+
81+
Lemma in_int_lt : forall p q r, in_int p q r -> p < q.
82+
Proof.
83+
induction 1; intros.
84+
apply le_lt_trans with r; auto with arith.
85+
Qed.
86+
87+
Lemma in_int_p_Sq :
88+
forall p q r, in_int p (S q) r -> in_int p q r \/ r = q :>nat.
89+
Proof.
90+
induction 1; intros.
91+
elim (le_lt_or_eq r q); auto with arith.
92+
Qed.
93+
94+
Lemma in_int_S : forall p q r, in_int p q r -> in_int p (S q) r.
95+
Proof.
96+
induction 1; auto with arith.
97+
Qed.
98+
Hint Resolve in_int_S: arith v62.
99+
100+
Lemma in_int_Sp_q : forall p q r, in_int (S p) q r -> in_int p q r.
101+
Proof.
102+
induction 1; auto with arith.
103+
Qed.
104+
Hint Immediate in_int_Sp_q: arith v62.
105+
106+
Lemma between_in_int :
107+
forall k l, between k l -> forall r, in_int k l r -> P r.
108+
Proof.
109+
induction 1; intros.
110+
absurd (k < k); auto with arith.
111+
apply in_int_lt with r; auto with arith.
112+
elim (in_int_p_Sq k l r); intros; auto with arith.
113+
rewrite H2; trivial with arith.
114+
Qed.
115+
116+
Lemma in_int_between :
117+
forall k l, k <= l -> (forall r, in_int k l r -> P r) -> between k l.
118+
Proof.
119+
induction 1; auto with arith.
120+
Qed.
121+
122+
Lemma exists_in_int :
123+
forall k l, exists_between k l -> exists2 m : nat, in_int k l m & Q m.
124+
Proof.
125+
induction 1.
126+
case IHexists_between; intros p inp Qp; exists p; auto with arith.
127+
exists l; auto with arith.
128+
Qed.
129+
130+
Lemma in_int_exists : forall k l r, in_int k l r -> Q r -> exists_between k l.
131+
Proof.
132+
destruct 1; intros.
133+
elim H0; auto with arith.
134+
Qed.
135+
136+
Lemma between_or_exists :
137+
forall k l,
138+
k <= l ->
139+
(forall n:nat, in_int k l n -> P n \/ Q n) ->
140+
between k l \/ exists_between k l.
141+
Proof.
142+
induction 1; intros; auto with arith.
143+
elim IHle; intro; auto with arith.
144+
elim (H0 m); auto with arith.
145+
Qed.
146+
147+
Lemma between_not_exists :
148+
forall k l,
149+
between k l ->
150+
(forall n:nat, in_int k l n -> P n -> ~ Q n) -> ~ exists_between k l.
151+
Proof.
152+
induction 1; red; intros.
153+
absurd (k < k); auto with arith.
154+
absurd (Q l); auto with arith.
155+
elim (exists_in_int k (S l)); auto with arith; intros l' inl' Ql'.
156+
replace l with l'; auto with arith.
157+
elim inl'; intros.
158+
elim (le_lt_or_eq l' l); auto with arith; intros.
159+
absurd (exists_between k l); auto with arith.
160+
apply in_int_exists with l'; auto with arith.
161+
Qed.
162+
163+
Inductive P_nth (init:nat) : nat -> nat -> Prop :=
164+
| nth_O : P_nth init init 0
165+
| nth_S :
166+
forall k l (n:nat),
167+
P_nth init k n -> between (S k) l -> Q l -> P_nth init l (S n).
168+
169+
Lemma nth_le : forall (init:nat) l (n:nat), P_nth init l n -> init <= l.
170+
Proof.
171+
induction 1; intros; auto with arith.
172+
apply le_trans with (S k); auto with arith.
173+
Qed.
174+
175+
Definition eventually (n:nat) := exists2 k : nat, k <= n & Q k.
176+
177+
Lemma event_O : eventually 0 -> Q 0.
178+
Proof.
179+
induction 1; intros.
180+
replace 0 with x; auto with arith.
181+
Qed.
182+
183+
End Between.
184+
185+
Hint Resolve nth_O bet_S bet_emp bet_eq between_Sk_l exists_S exists_le
186+
in_int_S in_int_intro: arith v62.
187+
Hint Immediate in_int_Sp_q exists_le_S exists_S_le: arith v62.

‎stdlib-benchs/Arith/Bool_nat.v

Lines changed: 37 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,37 @@
1+
(************************************************************************)
2+
(* v * The Coq Proof Assistant / The Coq Development Team *)
3+
(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *)
4+
(* \VV/ **************************************************************)
5+
(* // * This file is distributed under the terms of the *)
6+
(* * GNU Lesser General Public License Version 2.1 *)
7+
(************************************************************************)
8+
9+
Require Export Compare_dec.
10+
Require Export Peano_dec.
11+
Require Import Sumbool.
12+
13+
Local Open Scope nat_scope.
14+
15+
Implicit Types m n x y : nat.
16+
17+
(** The decidability of equality and order relations over
18+
type [nat] give some boolean functions with the adequate specification. *)
19+
20+
Definition notzerop n := sumbool_not _ _ (zerop n).
21+
Definition lt_ge_dec : forall x y, {x < y} + {x >= y} :=
22+
fun n m => sumbool_not _ _ (le_lt_dec m n).
23+
24+
Definition nat_lt_ge_bool x y := bool_of_sumbool (lt_ge_dec x y).
25+
Definition nat_ge_lt_bool x y :=
26+
bool_of_sumbool (sumbool_not _ _ (lt_ge_dec x y)).
27+
28+
Definition nat_le_gt_bool x y := bool_of_sumbool (le_gt_dec x y).
29+
Definition nat_gt_le_bool x y :=
30+
bool_of_sumbool (sumbool_not _ _ (le_gt_dec x y)).
31+
32+
Definition nat_eq_bool x y := bool_of_sumbool (eq_nat_dec x y).
33+
Definition nat_noteq_bool x y :=
34+
bool_of_sumbool (sumbool_not _ _ (eq_nat_dec x y)).
35+
36+
Definition zerop_bool x := bool_of_sumbool (zerop x).
37+
Definition notzerop_bool x := bool_of_sumbool (notzerop x).

‎stdlib-benchs/Arith/Compare.v

Lines changed: 53 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,53 @@
1+
(************************************************************************)
2+
(* v * The Coq Proof Assistant / The Coq Development Team *)
3+
(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *)
4+
(* \VV/ **************************************************************)
5+
(* // * This file is distributed under the terms of the *)
6+
(* * GNU Lesser General Public License Version 2.1 *)
7+
(************************************************************************)
8+
9+
(** Equality is decidable on [nat] *)
10+
11+
Local Open Scope nat_scope.
12+
13+
Notation not_eq_sym := not_eq_sym (only parsing).
14+
15+
Implicit Types m n p q : nat.
16+
17+
Require Import Arith_base.
18+
Require Import Peano_dec.
19+
Require Import Compare_dec.
20+
21+
Definition le_or_le_S := le_le_S_dec.
22+
23+
Definition Pcompare := gt_eq_gt_dec.
24+
25+
Lemma le_dec : forall n m, {n <= m} + {m <= n}.
26+
Proof le_ge_dec.
27+
28+
Definition lt_or_eq n m := {m > n} + {n = m}.
29+
30+
Lemma le_decide : forall n m, n <= m -> lt_or_eq n m.
31+
Proof le_lt_eq_dec.
32+
33+
Lemma le_le_S_eq : forall n m, n <= m -> S n <= m \/ n = m.
34+
Proof le_lt_or_eq.
35+
36+
(* By special request of G. Kahn - Used in Group Theory *)
37+
Lemma discrete_nat :
38+
forall n m, n < m -> S n = m \/ (exists r : nat, m = S (S (n + r))).
39+
Proof.
40+
intros m n H.
41+
lapply (lt_le_S m n); auto with arith.
42+
intro H'; lapply (le_lt_or_eq (S m) n); auto with arith.
43+
induction 1; auto with arith.
44+
right; exists (n - S (S m)); simpl.
45+
rewrite (plus_comm m (n - S (S m))).
46+
rewrite (plus_n_Sm (n - S (S m)) m).
47+
rewrite (plus_n_Sm (n - S (S m)) (S m)).
48+
rewrite (plus_comm (n - S (S m)) (S (S m))); auto with arith.
49+
Qed.
50+
51+
Require Export Wf_nat.
52+
53+
Require Export Min Max.

0 commit comments

Comments
 (0)