Commit 7dd32d7d authored by Robbert Krebbers's avatar Robbert Krebbers

Use new Import/Export syntax everywhere.

Also, make our redefinition of done more robust under different
orders of Importing modules.
parent 86803d3a
...@@ -7,7 +7,7 @@ structures. *) ...@@ -7,7 +7,7 @@ structures. *)
Global Generalizable All Variables. Global Generalizable All Variables.
Global Set Automatic Coercions Import. Global Set Automatic Coercions Import.
Global Set Asymmetric Patterns. Global Set Asymmetric Patterns.
Require Export Morphisms RelationClasses List Bool Utf8 Program Setoid. From Coq Require Export Morphisms RelationClasses List Bool Utf8 Program Setoid.
Obligation Tactic := idtac. Obligation Tactic := idtac.
(** * General *) (** * General *)
......
(* Copyright (c) 2012-2015, Robbert Krebbers. *) (* Copyright (c) 2012-2015, Robbert Krebbers. *)
(* This file is distributed under the terms of the BSD license. *) (* This file is distributed under the terms of the BSD license. *)
(** This file implements bsets as functions into Prop. *) (** This file implements bsets as functions into Prop. *)
Require Export prelude.prelude. From stdpp Require Export prelude.
Record bset (A : Type) : Type := mkBSet { bset_car : A bool }. Record bset (A : Type) : Type := mkBSet { bset_car : A bool }.
Arguments mkBSet {_} _. Arguments mkBSet {_} _.
......
...@@ -2,8 +2,8 @@ ...@@ -2,8 +2,8 @@
(* This file is distributed under the terms of the BSD license. *) (* This file is distributed under the terms of the BSD license. *)
(** This files implements an efficient implementation of finite/cofinite sets (** This files implements an efficient implementation of finite/cofinite sets
of positive binary naturals [positive]. *) of positive binary naturals [positive]. *)
Require Export prelude.collections. From stdpp Require Export collections.
Require Import prelude.pmap prelude.gmap prelude.mapset. From stdpp Require Import pmap gmap mapset.
Local Open Scope positive_scope. Local Open Scope positive_scope.
(** * The tree data structure *) (** * The tree data structure *)
......
...@@ -3,7 +3,7 @@ ...@@ -3,7 +3,7 @@
(** This file collects definitions and theorems on collections. Most (** This file collects definitions and theorems on collections. Most
importantly, it implements some tactics to automatically solve goals involving importantly, it implements some tactics to automatically solve goals involving
collections. *) collections. *)
Require Export prelude.base prelude.tactics prelude.orders. From stdpp Require Export base tactics orders.
Instance collection_subseteq `{ElemOf A C} : SubsetEq C := λ X Y, Instance collection_subseteq `{ElemOf A C} : SubsetEq C := λ X Y,
x, x X x Y. x, x X x Y.
......
(* Copyright (c) 2012-2015, Robbert Krebbers. *) (* Copyright (c) 2012-2015, Robbert Krebbers. *)
(* This file is distributed under the terms of the BSD license. *) (* This file is distributed under the terms of the BSD license. *)
Require Export prelude.list. From stdpp Require Export list.
Local Open Scope positive. Local Open Scope positive.
Class Countable A `{ x y : A, Decision (x = y)} := { Class Countable A `{ x y : A, Decision (x = y)} := {
......
...@@ -3,7 +3,7 @@ ...@@ -3,7 +3,7 @@
(** This file collects theorems, definitions, tactics, related to propositions (** This file collects theorems, definitions, tactics, related to propositions
with a decidable equality. Such propositions are collected by the [Decision] with a decidable equality. Such propositions are collected by the [Decision]
type class. *) type class. *)
Require Export prelude.proof_irrel. From stdpp Require Export proof_irrel.
Hint Extern 200 (Decision _) => progress (lazy beta) : typeclass_instances. Hint Extern 200 (Decision _) => progress (lazy beta) : typeclass_instances.
......
(* Copyright (c) 2012-2015, Robbert Krebbers. *) (* Copyright (c) 2012-2015, Robbert Krebbers. *)
(* This file is distributed under the terms of the BSD license. *) (* This file is distributed under the terms of the BSD license. *)
Require Export prelude.list. From stdpp Require Export list.
Definition error (S E A : Type) : Type := S E + (A * S). Definition error (S E A : Type) : Type := S E + (A * S).
......
...@@ -3,8 +3,9 @@ ...@@ -3,8 +3,9 @@
(** This file collects definitions and theorems on finite collections. Most (** This file collects definitions and theorems on finite collections. Most
importantly, it implements a fold and size function and some useful induction importantly, it implements a fold and size function and some useful induction
principles on finite collections . *) principles on finite collections . *)
Require Import Permutation prelude.relations prelude.listset. From Coq Require Import Permutation.
Require Export prelude.numbers prelude.collections. From stdpp Require Import relations listset.
From stdpp Require Export numbers collections.
Instance collection_size `{Elements A C} : Size C := length elements. Instance collection_size `{Elements A C} : Size C := length elements.
Definition collection_fold `{Elements A C} {B} Definition collection_fold `{Elements A C} {B}
......
...@@ -3,7 +3,7 @@ ...@@ -3,7 +3,7 @@
(** This file provides an axiomatization of the domain function of finite (** This file provides an axiomatization of the domain function of finite
maps. We provide such an axiomatization, instead of implementing the domain maps. We provide such an axiomatization, instead of implementing the domain
function in a generic way, to allow more efficient implementations. *) function in a generic way, to allow more efficient implementations. *)
Require Export prelude.collections prelude.fin_maps. From stdpp Require Export collections fin_maps.
Class FinMapDom K M D `{FMap M, Class FinMapDom K M D `{FMap M,
A, Lookup K A (M A), A, Empty (M A), A, PartialAlter K A (M A), A, Lookup K A (M A), A, Empty (M A), A, PartialAlter K A (M A),
......
...@@ -4,8 +4,8 @@ ...@@ -4,8 +4,8 @@
finite maps and collects some theory on it. Most importantly, it proves useful finite maps and collects some theory on it. Most importantly, it proves useful
induction principles for finite maps and implements the tactic induction principles for finite maps and implements the tactic
[simplify_map_equality] to simplify goals involving finite maps. *) [simplify_map_equality] to simplify goals involving finite maps. *)
Require Import Permutation. From Coq Require Import Permutation.
Require Export prelude.relations prelude.vector prelude.orders. From stdpp Require Export relations vector orders.
(** * Axiomatization of finite maps *) (** * Axiomatization of finite maps *)
(** We require Leibniz equality to be extensional on finite maps. This of (** We require Leibniz equality to be extensional on finite maps. This of
......
(* Copyright (c) 2012-2015, Robbert Krebbers. *) (* Copyright (c) 2012-2015, Robbert Krebbers. *)
(* This file is distributed under the terms of the BSD license. *) (* This file is distributed under the terms of the BSD license. *)
Require Export prelude.countable prelude.list. From stdpp Require Export countable list.
Class Finite A `{ x y : A, Decision (x = y)} := { Class Finite A `{ x y : A, Decision (x = y)} := {
enum : list A; enum : list A;
......
...@@ -2,8 +2,8 @@ ...@@ -2,8 +2,8 @@
(* This file is distributed under the terms of the BSD license. *) (* This file is distributed under the terms of the BSD license. *)
(** This file implements finite maps and finite sets with keys of any countable (** This file implements finite maps and finite sets with keys of any countable
type. The implementation is based on [Pmap]s, radix-2 search trees. *) type. The implementation is based on [Pmap]s, radix-2 search trees. *)
Require Export prelude.countable prelude.fin_maps prelude.fin_map_dom. From stdpp Require Export countable fin_maps fin_map_dom.
Require Import prelude.pmap prelude.mapset. From stdpp Require Import pmap mapset.
(** * The data structure *) (** * The data structure *)
(** We pack a [Pmap] together with a proof that ensures that all keys correspond (** We pack a [Pmap] together with a proof that ensures that all keys correspond
......
...@@ -3,8 +3,8 @@ ...@@ -3,8 +3,8 @@
(** This file implements finite set using hash maps. Hash sets are represented (** This file implements finite set using hash maps. Hash sets are represented
using radix-2 search trees. Each hash bucket is thus indexed using an binary 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. *) integer of type [Z], and contains an unordered list without duplicates. *)
Require Export prelude.fin_maps prelude.listset. From stdpp Require Export fin_maps listset.
Require Import prelude.zmap. From stdpp Require Import zmap.
Record hashset {A} (hash : A Z) := Hashset { Record hashset {A} (hash : A Z) := Hashset {
hashset_car : Zmap (list A); hashset_car : Zmap (list A);
......
...@@ -2,7 +2,7 @@ ...@@ -2,7 +2,7 @@
(* This file is distributed under the terms of the BSD license. *) (* This file is distributed under the terms of the BSD license. *)
(** This files defines a lexicographic order on various common data structures (** 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. *) and proves that it is a partial order having a strong variant of trichotomy. *)
Require Import prelude.numbers. From stdpp Require Import numbers.
Notation cast_trichotomy T := Notation cast_trichotomy T :=
match T with match T with
......
...@@ -2,8 +2,8 @@ ...@@ -2,8 +2,8 @@
(* This file is distributed under the terms of the BSD license. *) (* This file is distributed under the terms of the BSD license. *)
(** This file collects general purpose definitions and theorems on lists that (** This file collects general purpose definitions and theorems on lists that
are not in the Coq standard library. *) are not in the Coq standard library. *)
Require Export Permutation. From Coq Require Export Permutation.
Require Export prelude.numbers prelude.base prelude.decidable prelude.option. From stdpp Require Export numbers base decidable option.
Arguments length {_} _. Arguments length {_} _.
Arguments cons {_} _ _. Arguments cons {_} _ _.
......
...@@ -2,7 +2,7 @@ ...@@ -2,7 +2,7 @@
(* This file is distributed under the terms of the BSD license. *) (* This file is distributed under the terms of the BSD license. *)
(** This file implements finite set as unordered lists without duplicates (** This file implements finite set as unordered lists without duplicates
removed. This implementation forms a monad. *) removed. This implementation forms a monad. *)
Require Export prelude.base prelude.decidable prelude.collections prelude.list. From stdpp Require Export base decidable collections list.
Record listset A := Listset { listset_car: list A }. Record listset A := Listset { listset_car: list A }.
Arguments listset_car {_} _. Arguments listset_car {_} _.
......
...@@ -3,7 +3,7 @@ ...@@ -3,7 +3,7 @@
(** This file implements finite as unordered lists without duplicates. (** This file implements finite as unordered lists without duplicates.
Although this implementation is slow, it is very useful as decidable equality Although this implementation is slow, it is very useful as decidable equality
is the only constraint on the carrier set. *) is the only constraint on the carrier set. *)
Require Export prelude.base prelude.decidable prelude.collections prelude.list. From stdpp Require Export base decidable collections list.
Record listset_nodup A := ListsetNoDup { Record listset_nodup A := ListsetNoDup {
listset_nodup_car : list A; listset_nodup_prf : NoDup listset_nodup_car listset_nodup_car : list A; listset_nodup_prf : NoDup listset_nodup_car
......
...@@ -3,7 +3,7 @@ ...@@ -3,7 +3,7 @@
(** This files gives an implementation of finite sets using finite maps with (** This files gives an implementation of finite sets using finite maps with
elements of the unit type. Since maps enjoy extensional equality, the elements of the unit type. Since maps enjoy extensional equality, the
constructed finite sets do so as well. *) constructed finite sets do so as well. *)
Require Export prelude.fin_map_dom. From stdpp Require Export fin_map_dom.
Record mapset (M : Type Type) : Type := Record mapset (M : Type Type) : Type :=
Mapset { mapset_car: M (unit : Type) }. Mapset { mapset_car: M (unit : Type) }.
......
...@@ -3,7 +3,7 @@ ...@@ -3,7 +3,7 @@
(** This files implements a type [natmap A] of finite maps whose keys range (** This files implements a type [natmap A] of finite maps whose keys range
over Coq's data type of unary natural numbers [nat]. The implementation equips over Coq's data type of unary natural numbers [nat]. The implementation equips
a list with a proof of canonicity. *) a list with a proof of canonicity. *)
Require Import prelude.fin_maps prelude.mapset. From stdpp Require Import fin_maps mapset.
Notation natmap_raw A := (list (option A)). Notation natmap_raw A := (list (option A)).
Definition natmap_wf {A} (l : natmap_raw A) := Definition natmap_wf {A} (l : natmap_raw A) :=
......
...@@ -2,8 +2,8 @@ ...@@ -2,8 +2,8 @@
(* This file is distributed under the terms of the BSD license. *) (* This file is distributed under the terms of the BSD license. *)
(** This files extends the implementation of finite over [positive] to finite (** This files extends the implementation of finite over [positive] to finite
maps whose keys range over Coq's data type of binary naturals [N]. *) maps whose keys range over Coq's data type of binary naturals [N]. *)
Require Import prelude.pmap prelude.mapset. From stdpp Require Import pmap mapset.
Require Export prelude.prelude prelude.fin_maps. From stdpp Require Export prelude fin_maps.
Local Open Scope N_scope. Local Open Scope N_scope.
......
...@@ -3,9 +3,9 @@ ...@@ -3,9 +3,9 @@
(** This file collects some trivial facts on the Coq types [nat] and [N] for (** This file collects some trivial facts on the Coq types [nat] and [N] for
natural numbers, and the type [Z] for integers. It also declares some useful natural numbers, and the type [Z] for integers. It also declares some useful
notations. *) notations. *)
Require Export Eqdep PArith NArith ZArith NPeano. From Coq Require Export Eqdep PArith NArith ZArith NPeano.
Require Import QArith Qcanon. From Coq Require Import QArith Qcanon.
Require Export prelude.base prelude.decidable prelude.option. From stdpp Require Export base decidable option.
Open Scope nat_scope. Open Scope nat_scope.
Coercion Z.of_nat : nat >-> Z. Coercion Z.of_nat : nat >-> Z.
...@@ -50,7 +50,7 @@ Proof. ...@@ -50,7 +50,7 @@ Proof.
* clear nat_le_pi. intros; exfalso; auto with lia. * clear nat_le_pi. intros; exfalso; auto with lia.
* injection 1. intros Hy. by case (nat_le_pi x y p y' q Hy). } * injection 1. intros Hy. by case (nat_le_pi x y p y' q Hy). }
intros x y p q. intros x y p q.
by apply (eq_dep_eq_dec (λ x y, decide (x = y))), aux. by apply (Eqdep_dec.eq_dep_eq_dec (λ x y, decide (x = y))), aux.
Qed. Qed.
Instance nat_lt_pi: x y : nat, ProofIrrel (x < y). Instance nat_lt_pi: x y : nat, ProofIrrel (x < y).
Proof. apply _. Qed. Proof. apply _. Qed.
......
...@@ -2,7 +2,7 @@ ...@@ -2,7 +2,7 @@
(* This file is distributed under the terms of the BSD license. *) (* This file is distributed under the terms of the BSD license. *)
(** This file collects general purpose definitions and theorems on the option (** This file collects general purpose definitions and theorems on the option
data type that are not in the Coq standard library. *) data type that are not in the Coq standard library. *)
Require Export prelude.base prelude.tactics prelude.decidable. From stdpp Require Export base tactics decidable.
Inductive option_reflect {A} (P : A Prop) (Q : Prop) : option A Type := Inductive option_reflect {A} (P : A Prop) (Q : Prop) : option A Type :=
| ReflectSome x : P x option_reflect P Q (Some x) | ReflectSome x : P x option_reflect P Q (Some x)
......
...@@ -2,8 +2,8 @@ ...@@ -2,8 +2,8 @@
(* This file is distributed under the terms of the BSD license. *) (* This file is distributed under the terms of the BSD license. *)
(** This file collects common properties of pre-orders and semi lattices. This (** This file collects common properties of pre-orders and semi lattices. This
theory will mainly be used for the theory on collections and finite maps. *) theory will mainly be used for the theory on collections and finite maps. *)
Require Export Sorted. From Coq Require Export Sorted.
Require Export prelude.base prelude.decidable prelude.tactics prelude.list. From stdpp Require Export base decidable tactics list.
(** * Arbitrary pre-, parial and total orders *) (** * Arbitrary pre-, parial and total orders *)
(** Properties about arbitrary pre-, partial, and total orders. We do not use (** Properties about arbitrary pre-, partial, and total orders. We do not use
......
...@@ -7,8 +7,9 @@ trees (uncompressed Patricia trees) and guarantees logarithmic-time operations. ...@@ -7,8 +7,9 @@ trees (uncompressed Patricia trees) and guarantees logarithmic-time operations.
However, we extend Leroy's implementation by packing the trees into a Sigma However, we extend Leroy's implementation by packing the trees into a Sigma
type such that canonicity of representation is ensured. This is necesarry for type such that canonicity of representation is ensured. This is necesarry for
Leibniz equality to become extensional. *) Leibniz equality to become extensional. *)
Require Import PArith prelude.mapset. From Coq Require Import PArith.
Require Export prelude.fin_maps. From stdpp Require Import mapset.
From stdpp Require Export fin_maps.
Local Open Scope positive_scope. Local Open Scope positive_scope.
Local Hint Extern 0 (@eq positive _ _) => congruence. Local Hint Extern 0 (@eq positive _ _) => congruence.
......
(* Copyright (c) 2012-2015, Robbert Krebbers. *) (* Copyright (c) 2012-2015, Robbert Krebbers. *)
(* This file is distributed under the terms of the BSD license. *) (* This file is distributed under the terms of the BSD license. *)
Require Export From stdpp Require Export
prelude.base base
prelude.tactics tactics
prelude.decidable decidable
prelude.orders orders
prelude.option option
prelude.vector vector
prelude.numbers numbers
prelude.relations relations
prelude.collections collections
prelude.fin_collections fin_collections
prelude.listset listset
prelude.list list
prelude.lexico. lexico.
(* Copyright (c) 2012-2015, Robbert Krebbers. *) (* Copyright (c) 2012-2015, Robbert Krebbers. *)
(* This file is distributed under the terms of the BSD license. *) (* This file is distributed under the terms of the BSD license. *)
Require Export prelude.strings. From stdpp Require Export strings.
Require Import prelude.relations. From stdpp Require Import relations.
Require Import Ascii. From Coq Require Import Ascii.
Class Pretty A := pretty : A string. Class Pretty A := pretty : A string.
Definition pretty_N_char (x : N) : ascii := Definition pretty_N_char (x : N) : ascii :=
......
(* Copyright (c) 2012-2015, Robbert Krebbers. *) (* Copyright (c) 2012-2015, Robbert Krebbers. *)
(* This file is distributed under the terms of the BSD license. *) (* This file is distributed under the terms of the BSD license. *)
(** This file collects facts on proof irrelevant types/propositions. *) (** This file collects facts on proof irrelevant types/propositions. *)
Require Export Eqdep_dec prelude.tactics. From Coq Require Import Eqdep_dec.
From stdpp Require Export tactics.
Hint Extern 200 (ProofIrrel _) => progress (lazy beta) : typeclass_instances. Hint Extern 200 (ProofIrrel _) => progress (lazy beta) : typeclass_instances.
......
...@@ -4,8 +4,8 @@ ...@@ -4,8 +4,8 @@
These are particularly useful as we define the operational semantics as a These are particularly useful as we define the operational semantics as a
small step semantics. This file defines a hint database [ars] containing small step semantics. This file defines a hint database [ars] containing
some theorems on abstract rewriting systems. *) some theorems on abstract rewriting systems. *)
Require Import Wf_nat. From Coq Require Import Wf_nat.
Require Export prelude.tactics prelude.base. From stdpp Require Export tactics base.
(** * Definitions *) (** * Definitions *)
Section definitions. Section definitions.
......
(* Copyright (c) 2012-2015, Robbert Krebbers. *) (* Copyright (c) 2012-2015, Robbert Krebbers. *)
(* This file is distributed under the terms of the BSD license. *) (* This file is distributed under the terms of the BSD license. *)
(** This file implements sets as functions into Prop. *) (** This file implements sets as functions into Prop. *)
Require Export prelude.prelude. From stdpp Require Export prelude.
Record set (A : Type) : Type := mkSet { set_car : A Prop }. Record set (A : Type) : Type := mkSet { set_car : A Prop }.
Arguments mkSet {_} _. Arguments mkSet {_} _.
......
(* Copyright (c) 2012-2015, Robbert Krebbers. *) (* Copyright (c) 2012-2015, Robbert Krebbers. *)
(* This file is distributed under the terms of the BSD license. *) (* This file is distributed under the terms of the BSD license. *)
Require Export prelude.tactics. From stdpp Require Export tactics.
CoInductive stream (A : Type) : Type := scons : A stream A stream A. CoInductive stream (A : Type) : Type := scons : A stream A stream A.
Arguments scons {_} _ _. Arguments scons {_} _ _.
......
...@@ -4,8 +4,8 @@ ...@@ -4,8 +4,8 @@
range over Coq's data type of strings [string]. The implementation uses radix-2 range over Coq's data type of strings [string]. The implementation uses radix-2
search trees (uncompressed Patricia trees) as implemented in the file [pmap] search trees (uncompressed Patricia trees) as implemented in the file [pmap]
and guarantees logarithmic-time operations. *) and guarantees logarithmic-time operations. *)
Require Export prelude.fin_maps prelude.pretty. From stdpp Require Export fin_maps pretty.
Require Import prelude.gmap. From stdpp Require Import gmap.
Notation stringmap := (gmap string). Notation stringmap := (gmap string).
Notation stringset := (gset string). Notation stringset := (gset string).
...@@ -58,4 +58,4 @@ Fixpoint fresh_strings_of_set ...@@ -58,4 +58,4 @@ Fixpoint fresh_strings_of_set
| S n => | S n =>
let x := fresh_string_of_set s X in let x := fresh_string_of_set s X in
x :: fresh_strings_of_set s n ({[ x ]} X) x :: fresh_strings_of_set s n ({[ x ]} X)
end%nat. end%nat.
\ No newline at end of file
(* Copyright (c) 2012-2015, Robbert Krebbers. *) (* Copyright (c) 2012-2015, Robbert Krebbers. *)
(* This file is distributed under the terms of the BSD license. *) (* This file is distributed under the terms of the BSD license. *)
Require Import Ascii. From Coq Require Import Ascii.
Require Export String prelude.countable. From Coq Require Export String.
From stdpp Require Export countable.
(** * Fix scopes *) (** * Fix scopes *)
Open Scope string_scope. Open Scope string_scope.
......
...@@ -2,9 +2,9 @@ ...@@ -2,9 +2,9 @@
(* This file is distributed under the terms of the BSD license. *) (* This file is distributed under the terms of the BSD license. *)
(** This file collects general purpose tactics that are used throughout (** This file collects general purpose tactics that are used throughout
the development. *) the development. *)
Require Import Omega. From Coq Require Import Omega.
Require Export Psatz. From Coq Require Export Psatz.
Require Export prelude.base. From stdpp Require Export base.
Lemma f_equal_dep {A B} (f g : x : A, B x) x : f = g f x = g x. Lemma f_equal_dep {A B} (f g : x : A, B x) x : f = g f x = g x.
Proof. intros ->; reflexivity. Qed. Proof. intros ->; reflexivity. Qed.
......
...@@ -5,7 +5,7 @@ ...@@ -5,7 +5,7 @@
definitions from the standard library, but renames or changes their notations, definitions from the standard library, but renames or changes their notations,
so that it becomes more consistent with the naming conventions in this so that it becomes more consistent with the naming conventions in this
development. *) development. *)
Require Import prelude.list prelude.finite. From stdpp Require Import list finite.
Open Scope vector_scope. Open Scope vector_scope.
(** * The fin type *) (** * The fin type *)
......
...@@ -2,8 +2,8 @@ ...@@ -2,8 +2,8 @@
(* This file is distributed under the terms of the BSD license. *) (* This file is distributed under the terms of the BSD license. *)
(** This files extends the implementation of finite over [positive] to finite (** This files extends the implementation of finite over [positive] to finite
maps whose keys range over Coq's data type of binary naturals [Z]. *) maps whose keys range over Coq's data type of binary naturals [Z]. *)
Require Import prelude.pmap prelude.mapset. From stdpp Require Import pmap mapset.
Require Export prelude.prelude prelude.fin_maps. From stdpp Require Export prelude fin_maps.
Local Open Scope Z_scope. Local Open Scope Z_scope.
Record Zmap (A : Type) : Type := Record Zmap (A : Type) : Type :=
......
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment