Skip to content
GitLab
Projects
Groups
Snippets
Help
Loading...
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in / Register
Toggle navigation
C
coq-stdpp
Project overview
Project overview
Details
Activity
Releases
Repository
Repository
Files
Commits
Branches
Tags
Contributors
Graph
Compare
Issues
0
Issues
0
List
Boards
Labels
Service Desk
Milestones
Merge Requests
0
Merge Requests
0
CI / CD
CI / CD
Pipelines
Jobs
Schedules
Operations
Operations
Incidents
Environments
Analytics
Analytics
CI / CD
Repository
Value Stream
Wiki
Wiki
Snippets
Snippets
Members
Members
Collapse sidebar
Close sidebar
Activity
Graph
Create a new issue
Jobs
Commits
Issue Boards
Open sidebar
David Swasey
coq-stdpp
Commits
808b681c
Commit
808b681c
authored
Jan 05, 2017
by
Ralf Jung
Committed by
Robbert Krebbers
Jan 31, 2017
Browse files
Options
Browse Files
Download
Email Patches
Plain Diff
more restrictive Proof Using hints in (most files of the) prelude
parent
24623c52
Changes
30
Hide whitespace changes
Inline
Side-by-side
Showing
30 changed files
with
32 additions
and
32 deletions
+32
-32
theories/base.v
theories/base.v
+1
-1
theories/bset.v
theories/bset.v
+1
-1
theories/coPset.v
theories/coPset.v
+1
-1
theories/countable.v
theories/countable.v
+1
-1
theories/finite.v
theories/finite.v
+3
-3
theories/functions.v
theories/functions.v
+1
-1
theories/gmap.v
theories/gmap.v
+1
-1
theories/gmultiset.v
theories/gmultiset.v
+1
-1
theories/hashset.v
theories/hashset.v
+1
-1
theories/hlist.v
theories/hlist.v
+1
-1
theories/lexico.v
theories/lexico.v
+1
-1
theories/listset.v
theories/listset.v
+1
-1
theories/listset_nodup.v
theories/listset_nodup.v
+1
-1
theories/natmap.v
theories/natmap.v
+1
-1
theories/nmap.v
theories/nmap.v
+1
-1
theories/numbers.v
theories/numbers.v
+1
-1
theories/option.v
theories/option.v
+1
-1
theories/orders.v
theories/orders.v
+1
-1
theories/pmap.v
theories/pmap.v
+1
-1
theories/pretty.v
theories/pretty.v
+1
-1
theories/proof_irrel.v
theories/proof_irrel.v
+1
-1
theories/relations.v
theories/relations.v
+1
-1
theories/set.v
theories/set.v
+1
-1
theories/sorting.v
theories/sorting.v
+1
-1
theories/streams.v
theories/streams.v
+1
-1
theories/stringmap.v
theories/stringmap.v
+1
-1
theories/strings.v
theories/strings.v
+1
-1
theories/tactics.v
theories/tactics.v
+1
-1
theories/vector.v
theories/vector.v
+1
-1
theories/zmap.v
theories/zmap.v
+1
-1
No files found.
theories/base.v
View file @
808b681c
...
...
@@ -9,7 +9,7 @@ Global Set Automatic Coercions Import.
Global
Set
Asymmetric
Patterns
.
Global
Unset
Transparent
Obligations
.
From
Coq
Require
Export
Morphisms
RelationClasses
List
Bool
Utf8
Setoid
.
Set
Default
Proof
Using
"Type
*
"
.
Set
Default
Proof
Using
"Type"
.
Export
ListNotations
.
From
Coq
.
Program
Require
Export
Basics
Syntax
.
Obligation
Tactic
:
=
idtac
.
...
...
theories/bset.v
View file @
808b681c
...
...
@@ -2,7 +2,7 @@
(* This file is distributed under the terms of the BSD license. *)
(** This file implements bsets as functions into Prop. *)
From
stdpp
Require
Export
prelude
.
Set
Default
Proof
Using
"Type
*
"
.
Set
Default
Proof
Using
"Type"
.
Record
bset
(
A
:
Type
)
:
Type
:
=
mkBSet
{
bset_car
:
A
→
bool
}.
Arguments
mkBSet
{
_
}
_
.
...
...
theories/coPset.v
View file @
808b681c
...
...
@@ -13,7 +13,7 @@ Since [positive]s are bitstrings, we encode [coPset]s as trees that correspond
to the decision function that map bitstrings to bools. *)
From
stdpp
Require
Export
collections
.
From
stdpp
Require
Import
pmap
gmap
mapset
.
Set
Default
Proof
Using
"Type
*
"
.
Set
Default
Proof
Using
"Type"
.
Local
Open
Scope
positive_scope
.
(** * The tree data structure *)
...
...
theories/countable.v
View file @
808b681c
(* Copyright (c) 2012-2015, Robbert Krebbers. *)
(* This file is distributed under the terms of the BSD license. *)
From
stdpp
Require
Export
list
.
Set
Default
Proof
Using
"Type
*
"
.
Set
Default
Proof
Using
"Type"
.
Local
Open
Scope
positive
.
Class
Countable
A
`
{
EqDecision
A
}
:
=
{
...
...
theories/finite.v
View file @
808b681c
(* Copyright (c) 2012-2015, Robbert Krebbers. *)
(* This file is distributed under the terms of the BSD license. *)
From
stdpp
Require
Export
countable
vector
.
Set
Default
Proof
Using
"Type
*
"
.
Set
Default
Proof
Using
"Type"
.
Class
Finite
A
`
{
EqDecision
A
}
:
=
{
enum
:
list
A
;
...
...
@@ -181,12 +181,12 @@ Section forall_exists.
Context
`
{
∀
x
,
Decision
(
P
x
)}.
Global
Instance
forall_dec
:
Decision
(
∀
x
,
P
x
).
Proof
.
Proof
using
Type
*
.
refine
(
cast_if
(
decide
(
Forall
P
(
enum
A
))))
;
abstract
by
rewrite
<-
Forall_finite
.
Defined
.
Global
Instance
exists_dec
:
Decision
(
∃
x
,
P
x
).
Proof
.
Proof
using
Type
*
.
refine
(
cast_if
(
decide
(
Exists
P
(
enum
A
))))
;
abstract
by
rewrite
<-
Exists_finite
.
Defined
.
...
...
theories/functions.v
View file @
808b681c
From
stdpp
Require
Export
base
tactics
.
Set
Default
Proof
Using
"Type
*
"
.
Set
Default
Proof
Using
"Type"
.
Section
definitions
.
Context
{
A
T
:
Type
}
`
{
EqDecision
A
}.
...
...
theories/gmap.v
View file @
808b681c
...
...
@@ -4,7 +4,7 @@
type. The implementation is based on [Pmap]s, radix-2 search trees. *)
From
stdpp
Require
Export
countable
fin_maps
fin_map_dom
.
From
stdpp
Require
Import
pmap
mapset
set
.
Set
Default
Proof
Using
"Type
*
"
.
Set
Default
Proof
Using
"Type"
.
(** * The data structure *)
(** We pack a [Pmap] together with a proof that ensures that all keys correspond
...
...
theories/gmultiset.v
View file @
808b681c
(* Copyright (c) 2012-2016, Robbert Krebbers. *)
(* This file is distributed under the terms of the BSD license. *)
From
stdpp
Require
Import
gmap
.
Set
Default
Proof
Using
"Type
*
"
.
Set
Default
Proof
Using
"Type"
.
Record
gmultiset
A
`
{
Countable
A
}
:
=
GMultiSet
{
gmultiset_car
:
gmap
A
nat
}.
Arguments
GMultiSet
{
_
_
_
}
_
.
...
...
theories/hashset.v
View file @
808b681c
...
...
@@ -5,7 +5,7 @@ using radix-2 search trees. Each hash bucket is thus indexed using an binary
integer of type [Z], and contains an unordered list without duplicates. *)
From
stdpp
Require
Export
fin_maps
listset
.
From
stdpp
Require
Import
zmap
.
Set
Default
Proof
Using
"Type
*
"
.
Set
Default
Proof
Using
"Type"
.
Record
hashset
{
A
}
(
hash
:
A
→
Z
)
:
=
Hashset
{
hashset_car
:
Zmap
(
list
A
)
;
...
...
theories/hlist.v
View file @
808b681c
From
stdpp
Require
Import
tactics
.
Set
Default
Proof
Using
"Type
*
"
.
Set
Default
Proof
Using
"Type"
.
Local
Set
Universe
Polymorphism
.
(* Not using [list Type] in order to avoid universe inconsistencies *)
...
...
theories/lexico.v
View file @
808b681c
...
...
@@ -3,7 +3,7 @@
(** This files defines a lexicographic order on various common data structures
and proves that it is a partial order having a strong variant of trichotomy. *)
From
stdpp
Require
Import
numbers
.
Set
Default
Proof
Using
"Type
*
"
.
Set
Default
Proof
Using
"Type"
.
Notation
cast_trichotomy
T
:
=
match
T
with
...
...
theories/listset.v
View file @
808b681c
...
...
@@ -3,7 +3,7 @@
(** This file implements finite set as unordered lists without duplicates
removed. This implementation forms a monad. *)
From
stdpp
Require
Export
collections
list
.
Set
Default
Proof
Using
"Type
*
"
.
Set
Default
Proof
Using
"Type"
.
Record
listset
A
:
=
Listset
{
listset_car
:
list
A
}.
Arguments
listset_car
{
_
}
_
.
...
...
theories/listset_nodup.v
View file @
808b681c
...
...
@@ -4,7 +4,7 @@
Although this implementation is slow, it is very useful as decidable equality
is the only constraint on the carrier set. *)
From
stdpp
Require
Export
collections
list
.
Set
Default
Proof
Using
"Type
*
"
.
Set
Default
Proof
Using
"Type"
.
Record
listset_nodup
A
:
=
ListsetNoDup
{
listset_nodup_car
:
list
A
;
listset_nodup_prf
:
NoDup
listset_nodup_car
...
...
theories/natmap.v
View file @
808b681c
...
...
@@ -4,7 +4,7 @@
over Coq's data type of unary natural numbers [nat]. The implementation equips
a list with a proof of canonicity. *)
From
stdpp
Require
Import
fin_maps
mapset
.
Set
Default
Proof
Using
"Type
*
"
.
Set
Default
Proof
Using
"Type"
.
Notation
natmap_raw
A
:
=
(
list
(
option
A
)).
Definition
natmap_wf
{
A
}
(
l
:
natmap_raw
A
)
:
=
...
...
theories/nmap.v
View file @
808b681c
...
...
@@ -4,7 +4,7 @@
maps whose keys range over Coq's data type of binary naturals [N]. *)
From
stdpp
Require
Import
pmap
mapset
.
From
stdpp
Require
Export
prelude
fin_maps
.
Set
Default
Proof
Using
"Type
*
"
.
Set
Default
Proof
Using
"Type"
.
Local
Open
Scope
N_scope
.
...
...
theories/numbers.v
View file @
808b681c
...
...
@@ -6,7 +6,7 @@ notations. *)
From
Coq
Require
Export
EqdepFacts
PArith
NArith
ZArith
NPeano
.
From
Coq
Require
Import
QArith
Qcanon
.
From
stdpp
Require
Export
base
decidable
option
.
Set
Default
Proof
Using
"Type
*
"
.
Set
Default
Proof
Using
"Type"
.
Open
Scope
nat_scope
.
Coercion
Z
.
of_nat
:
nat
>->
Z
.
...
...
theories/option.v
View file @
808b681c
...
...
@@ -3,7 +3,7 @@
(** This file collects general purpose definitions and theorems on the option
data type that are not in the Coq standard library. *)
From
stdpp
Require
Export
tactics
.
Set
Default
Proof
Using
"Type
*
"
.
Set
Default
Proof
Using
"Type"
.
Inductive
option_reflect
{
A
}
(
P
:
A
→
Prop
)
(
Q
:
Prop
)
:
option
A
→
Type
:
=
|
ReflectSome
x
:
P
x
→
option_reflect
P
Q
(
Some
x
)
...
...
theories/orders.v
View file @
808b681c
...
...
@@ -3,7 +3,7 @@
(** Properties about arbitrary pre-, partial, and total orders. We do not use
the relation [⊆] because we often have multiple orders on the same structure *)
From
stdpp
Require
Export
tactics
.
Set
Default
Proof
Using
"Type
*
"
.
Set
Default
Proof
Using
"Type"
.
Section
orders
.
Context
{
A
}
{
R
:
relation
A
}.
...
...
theories/pmap.v
View file @
808b681c
...
...
@@ -10,7 +10,7 @@ Leibniz equality to become extensional. *)
From
Coq
Require
Import
PArith
.
From
stdpp
Require
Import
mapset
countable
.
From
stdpp
Require
Export
fin_maps
.
Set
Default
Proof
Using
"Type
*
"
.
Set
Default
Proof
Using
"Type"
.
Local
Open
Scope
positive_scope
.
Local
Hint
Extern
0
(@
eq
positive
_
_
)
=>
congruence
.
...
...
theories/pretty.v
View file @
808b681c
...
...
@@ -3,7 +3,7 @@
From
stdpp
Require
Export
strings
.
From
stdpp
Require
Import
relations
.
From
Coq
Require
Import
Ascii
.
Set
Default
Proof
Using
"Type
*
"
.
Set
Default
Proof
Using
"Type"
.
Class
Pretty
A
:
=
pretty
:
A
→
string
.
Definition
pretty_N_char
(
x
:
N
)
:
ascii
:
=
...
...
theories/proof_irrel.v
View file @
808b681c
...
...
@@ -2,7 +2,7 @@
(* This file is distributed under the terms of the BSD license. *)
(** This file collects facts on proof irrelevant types/propositions. *)
From
stdpp
Require
Export
base
.
Set
Default
Proof
Using
"Type
*
"
.
Set
Default
Proof
Using
"Type"
.
Hint
Extern
200
(
ProofIrrel
_
)
=>
progress
(
lazy
beta
)
:
typeclass_instances
.
...
...
theories/relations.v
View file @
808b681c
...
...
@@ -6,7 +6,7 @@ small step semantics. This file defines a hint database [ars] containing
some theorems on abstract rewriting systems. *)
From
Coq
Require
Import
Wf_nat
.
From
stdpp
Require
Export
tactics
base
.
Set
Default
Proof
Using
"Type
*
"
.
Set
Default
Proof
Using
"Type"
.
(** * Definitions *)
Section
definitions
.
...
...
theories/set.v
View file @
808b681c
...
...
@@ -2,7 +2,7 @@
(* This file is distributed under the terms of the BSD license. *)
(** This file implements sets as functions into Prop. *)
From
stdpp
Require
Export
collections
.
Set
Default
Proof
Using
"Type
*
"
.
Set
Default
Proof
Using
"Type"
.
Record
set
(
A
:
Type
)
:
Type
:
=
mkSet
{
set_car
:
A
→
Prop
}.
Add
Printing
Constructor
set
.
...
...
theories/sorting.v
View file @
808b681c
...
...
@@ -4,7 +4,7 @@
standard library, but without using the module system. *)
From
Coq
Require
Export
Sorted
.
From
stdpp
Require
Export
orders
list
.
Set
Default
Proof
Using
"Type
*
"
.
Set
Default
Proof
Using
"Type"
.
Section
merge_sort
.
Context
{
A
}
(
R
:
relation
A
)
`
{
∀
x
y
,
Decision
(
R
x
y
)}.
...
...
theories/streams.v
View file @
808b681c
(* Copyright (c) 2012-2015, Robbert Krebbers. *)
(* This file is distributed under the terms of the BSD license. *)
From
stdpp
Require
Export
tactics
.
Set
Default
Proof
Using
"Type
*
"
.
Set
Default
Proof
Using
"Type"
.
CoInductive
stream
(
A
:
Type
)
:
Type
:
=
scons
:
A
→
stream
A
→
stream
A
.
Arguments
scons
{
_
}
_
_
.
...
...
theories/stringmap.v
View file @
808b681c
...
...
@@ -6,7 +6,7 @@ search trees (uncompressed Patricia trees) as implemented in the file [pmap]
and guarantees logarithmic-time operations. *)
From
stdpp
Require
Export
fin_maps
pretty
.
From
stdpp
Require
Import
gmap
.
Set
Default
Proof
Using
"Type
*
"
.
Set
Default
Proof
Using
"Type"
.
Notation
stringmap
:
=
(
gmap
string
).
Notation
stringset
:
=
(
gset
string
).
...
...
theories/strings.v
View file @
808b681c
...
...
@@ -4,7 +4,7 @@ From Coq Require Import Ascii.
From
Coq
Require
Export
String
.
From
stdpp
Require
Export
list
.
From
stdpp
Require
Import
countable
.
Set
Default
Proof
Using
"Type
*
"
.
Set
Default
Proof
Using
"Type"
.
(* To avoid randomly ending up with String.length because this module is
imported hereditarily somewhere. *)
...
...
theories/tactics.v
View file @
808b681c
...
...
@@ -5,7 +5,7 @@ the development. *)
From
Coq
Require
Import
Omega
.
From
Coq
Require
Export
Lia
.
From
stdpp
Require
Export
decidable
.
Set
Default
Proof
Using
"Type
*
"
.
Set
Default
Proof
Using
"Type"
.
Lemma
f_equal_dep
{
A
B
}
(
f
g
:
∀
x
:
A
,
B
x
)
x
:
f
=
g
→
f
x
=
g
x
.
Proof
.
intros
->
;
reflexivity
.
Qed
.
...
...
theories/vector.v
View file @
808b681c
...
...
@@ -6,7 +6,7 @@ definitions from the standard library, but renames or changes their notations,
so that it becomes more consistent with the naming conventions in this
development. *)
From
stdpp
Require
Export
list
.
Set
Default
Proof
Using
"Type
*
"
.
Set
Default
Proof
Using
"Type"
.
Open
Scope
vector_scope
.
(** * The fin type *)
...
...
theories/zmap.v
View file @
808b681c
...
...
@@ -4,7 +4,7 @@
maps whose keys range over Coq's data type of binary naturals [Z]. *)
From
stdpp
Require
Import
pmap
mapset
.
From
stdpp
Require
Export
prelude
fin_maps
.
Set
Default
Proof
Using
"Type
*
"
.
Set
Default
Proof
Using
"Type"
.
Local
Open
Scope
Z_scope
.
Record
Zmap
(
A
:
Type
)
:
Type
:
=
...
...
Write
Preview
Markdown
is supported
0%
Try again
or
attach a new file
.
Attach a file
Cancel
You are about to add
0
people
to the discussion. Proceed with caution.
Finish editing this message first!
Cancel
Please
register
or
sign in
to comment