Skip to content

Draft: Port to Coq 8.13.0 #10

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
gstew5 wants to merge 3 commits into
base: master
Choose a base branch
from
Open

Draft: Port to Coq 8.13.0 #10

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
3 commits
Select commit Hold shift + click to select a range
bc0d68e
Port to Coq 8.13.0, except
Mar 9, 2021
ea5fed0
Update README
Mar 9, 2021
251e529
Filled in Dred_idem admits
neewamp Mar 10, 2021
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
333 changes: 202 additions & 131 deletions Makefile
View file
Open in desktop

Large diffs are not rendered by default.

10 changes: 5 additions & 5 deletions README.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -3,10 +3,10 @@ Ohio University Verification Toolsuite

# REQUIREMENTS

coq 8.9.0
mathcomp algebra 1.7.0
mathcomp fingroup 1.7.0
mathcomp ssreflect 1.7.0
coq 8.13.0
mathcomp algebra 1.12.0
mathcomp fingroup 1.12.0
mathcomp ssreflect 1.12.0

# BUILD

Expand All @@ -18,7 +18,7 @@ To build OUVerT, clone it and do:

The latter command installs the OUVerT files in your local `.opam` directory.

To use OUVerT files in another development, simply import them with OUVerT.filename, as in:
To use OUVerT files in another development, simply import them with OUVerT.filename, as in:

> Require Import OUVerT.dyadic.

Expand Down
2 changes: 1 addition & 1 deletion _CoqProject
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,12 +1,12 @@
-R . OUVerT
dist.v
axioms.v
compile.v
dyadic.v
learning.v
numerics.v
vector.v
bigops.v
dist.v
expfacts.v
listlemmas.v
orderedtypes.v
Expand Down
18 changes: 9 additions & 9 deletions axioms.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -11,23 +11,23 @@ Require Import QArith Reals Rpower Ranalysis Fourier Lra.

Require Import dist.

(** The following lemmas (stated here as axioms) are well
(** The following lemmas (stated here as axioms) are well
known but should nevertheless be proved. Until proved,
any paper that uses/references results from OUVerT.axioms
should state explicitly that the formal claims depend upon
the following assumptions:
the following assumptions:

NOTE: We should see whether the results from Affeldt et al's:
https://staff.aist.go.jp/reynald.affeldt/shannon/
NOTE: We should see whether the results from Affeldt et al's:
https://staff.aist.go.jp/reynald.affeldt/shannon/
can be imported here to prove [pinsker] and related theorems
in information theory. *)

Axiom pinsker_Bernoulli :
forall (p q:R) (p_ax:0<p<1) (q_ax:0<q<1),
#[local] Open Scope R_scope.

Axiom pinsker_Bernoulli :
forall (p q:R) (p_ax:0<p<1) (q_ax:0<q<1),
sqrt (RE_Bernoulli p q / 2) >= TV_Bernoulli p q.

Axiom gibbs_Bernoulli :
forall (p q:R) (p_ax:0<p<1) (q_ax:0<q<1),
forall (p q:R) (p_ax:0<p<1) (q_ax:0<q<1),
0 <= RE_Bernoulli p q.


Loading