Commit bd7ebdec 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 3a18b722
Require Export algebra.cmra.
Require Import algebra.functor.
From algebra Require Export cmra.
From algebra Require Import functor.
Local Hint Extern 10 (_ _) => omega.
Record agree (A : Type) : Type := Agree {
......
Require Export algebra.excl.
Require Import algebra.functor.
From algebra Require Export excl.
From algebra Require Import functor.
Local Arguments validN _ _ _ !_ /.
Record auth (A : Type) : Type := Auth { authoritative : excl A ; own : A }.
......
Require Export mathcomp.ssreflect.ssreflect.
Require Export prelude.prelude.
From mathcomp.ssreflect Require Export ssreflect.
From prelude Require Export prelude.
Global Set Bullet Behavior "Strict Subproofs".
Global Open Scope general_if_scope.
\ No newline at end of file
Global Open Scope general_if_scope.
Ltac done := prelude.tactics.done.
\ No newline at end of file
Require Export algebra.cofe.
From algebra Require Export cofe.
Class Unit (A : Type) := unit : A A.
Instance: Params (@unit) 2.
......
Require Export algebra.cmra.
Require Import prelude.fin_maps.
From algebra Require Export cmra.
From prelude Require Import fin_maps.
Fixpoint big_op {A : cmraT} `{Empty A} (xs : list A) : A :=
match xs with [] => | x :: xs => x big_op xs end.
......
Require Export algebra.cmra.
Require Import algebra.cmra_big_op.
From algebra Require Export cmra.
From algebra Require Import cmra_big_op.
(** * Simple solver for validity and inclusion by reflection *)
Module ra_reflection. Section ra_reflection.
......
Require Export algebra.base.
From algebra Require Export base.
(** Unbundeled version *)
Class Dist A := dist : nat relation A.
......
Require Export algebra.cofe.
From algebra Require Export cofe.
Record solution (F : cofeT cofeT cofeT) := Solution {
solution_car :> cofeT;
......
Require Export algebra.cmra.
From algebra Require Export cmra.
(** From disjoint pcm *)
Record validity {A} (P : A Prop) : Type := Validity {
......
Require Export algebra.cmra.
Require Import algebra.functor.
From algebra Require Export cmra.
From algebra Require Import functor.
Local Arguments validN _ _ _ !_ /.
Local Arguments valid _ _ !_ /.
......
Require Export algebra.cmra prelude.gmap algebra.option.
Require Import algebra.functor.
From algebra Require Export cmra option.
From prelude Require Export gmap.
From algebra Require Import functor.
Section cofe.
Context `{Countable K} {A : cofeT}.
......
Require Export algebra.cmra.
From algebra Require Export cmra.
(** * Functors from COFE to CMRA *)
(* TODO RJ: Maybe find a better name for this? It is not PL-specific any more. *)
......
Require Export algebra.cmra.
Require Import algebra.functor.
From algebra Require Export cmra.
From algebra Require Import functor.
(** * Indexed product *)
(** Need to put this in a definition to make canonical structures to work. *)
......
Require Export algebra.cmra.
Require Import algebra.functor.
From algebra Require Export cmra.
From algebra Require Import functor.
(* COFE *)
Section cofe.
......
Require Export algebra.cmra.
Require Import prelude.sets algebra.dra.
From algebra Require Export cmra.
From prelude Require Import sets.
From algebra Require Import dra.
Local Arguments valid _ _ !_ /.
Local Arguments op _ _ !_ !_ /.
Local Arguments unit _ _ !_ /.
......
Require Export algebra.cmra.
From algebra Require Export cmra.
Local Hint Extern 1 (_ _) => etransitivity; [eassumption|].
Local Hint Extern 1 (_ _) => etransitivity; [|eassumption].
Local Hint Extern 10 (_ _) => omega.
......
Require Export heap_lang.lifting.
From heap_lang Require Export lifting.
Import uPred.
(** Define some derived forms, and derived lemmas about them. *)
......
Require Export program_logic.language prelude.strings.
Require Import prelude.gmap.
From program_logic Require Export language.
From prelude Require Export strings.
From prelude Require Import gmap.
Module heap_lang.
Open Scope Z_scope.
......
Require Export program_logic.weakestpre heap_lang.heap_lang.
Require Import program_logic.lifting.
Require Import program_logic.ownership. (* for ownP *)
Require Import heap_lang.tactics.
From program_logic Require Export weakestpre.
From heap_lang Require Export heap_lang.
From program_logic Require Import lifting.
From program_logic Require Import ownership. (* for ownP *)
From heap_lang Require Import tactics.
Export heap_lang. (* Prefer heap_lang names over language names. *)
Import uPred.
Local Hint Extern 0 (language.reducible _ _) => do_step ltac:(eauto 2).
......
Require Export heap_lang.derived.
From heap_lang Require Export derived.
(* What about Arguments for hoare triples?. *)
Arguments wp {_ _} _ _%L _.
......@@ -62,4 +62,4 @@ Notation "'rec:' f x y := e" := (RecV f x (Lam y e%L))
Notation "'rec:' f x y z := e" := (Rec f x (Lam y (Lam z e%L)))
(at level 102, f, x, y, z at level 1, e at level 200) : lang_scope.
Notation "'rec:' f x y z := e" := (RecV f x (Lam y (Lam z e%L)))
(at level 102, f, x, y, z at level 1, e at level 200) : lang_scope.
\ No newline at end of file
(at level 102, f, x, y, z at level 1, e at level 200) : lang_scope.
Require Export heap_lang.derived.
From heap_lang Require Export derived.
(** We define an alternative notion of substitution [gsubst e x ev] that
preserves the expression [e] syntactically in case the variable [x] does not
......
Require Export heap_lang.heap_lang.
Require Import prelude.fin_maps.
From heap_lang Require Export heap_lang.
From prelude Require Import fin_maps.
Import heap_lang.
(** The tactic [inv_step] performs inversion on hypotheses of the shape
......
(** This file is essentially a bunch of testcases. *)
Require Import program_logic.ownership.
From program_logic Require Import ownership.
From heap_lang Require Import substitution tactics notation.
Import uPred.
......
......@@ -7,7 +7,7 @@ structures. *)
Global Generalizable All Variables.
Global Set Automatic Coercions Import.
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.
(** * General *)
......
(* Copyright (c) 2012-2015, Robbert Krebbers. *)
(* This file is distributed under the terms of the BSD license. *)
(** This file implements bsets as functions into Prop. *)
Require Export prelude.prelude.
From prelude Require Export prelude.
Record bset (A : Type) : Type := mkBSet { bset_car : A bool }.
Arguments mkBSet {_} _.
......
......@@ -2,8 +2,8 @@
(* This file is distributed under the terms of the BSD license. *)
(** This files implements an efficient implementation of finite/cofinite sets
of positive binary naturals [positive]. *)
Require Export prelude.collections.
Require Import prelude.pmap prelude.gmap prelude.mapset.
From prelude Require Export collections.
From prelude Require Import pmap gmap mapset.
Local Open Scope positive_scope.
(** * The tree data structure *)
......
......@@ -3,7 +3,7 @@
(** This file collects definitions and theorems on collections. Most
importantly, it implements some tactics to automatically solve goals involving
collections. *)
Require Export prelude.base prelude.tactics prelude.orders.
From prelude Require Export base tactics orders.
Instance collection_subseteq `{ElemOf A C} : SubsetEq C := λ X Y,
x, x X x Y.
......
(* Copyright (c) 2012-2015, Robbert Krebbers. *)
(* This file is distributed under the terms of the BSD license. *)
Require Export prelude.list.
From prelude Require Export list.
Local Open Scope positive.
Class Countable A `{ x y : A, Decision (x = y)} := {
......
......@@ -3,7 +3,7 @@
(** This file collects theorems, definitions, tactics, related to propositions
with a decidable equality. Such propositions are collected by the [Decision]
type class. *)
Require Export prelude.proof_irrel.
From prelude Require Export proof_irrel.
Hint Extern 200 (Decision _) => progress (lazy beta) : typeclass_instances.
......
(* Copyright (c) 2012-2015, Robbert Krebbers. *)
(* This file is distributed under the terms of the BSD license. *)
Require Export prelude.list.
From prelude Require Export list.
Definition error (S E A : Type) : Type := S E + (A * S).
......
......@@ -3,8 +3,9 @@
(** This file collects definitions and theorems on finite collections. Most
importantly, it implements a fold and size function and some useful induction
principles on finite collections . *)
Require Import Permutation prelude.relations prelude.listset.
Require Export prelude.numbers prelude.collections.
From Coq Require Import Permutation.
From prelude Require Import relations listset.
From prelude Require Export numbers collections.
Instance collection_size `{Elements A C} : Size C := length elements.
Definition collection_fold `{Elements A C} {B}
......
......@@ -3,7 +3,7 @@
(** This file provides an axiomatization of the domain function of finite
maps. We provide such an axiomatization, instead of implementing the domain
function in a generic way, to allow more efficient implementations. *)
Require Export prelude.collections prelude.fin_maps.
From prelude Require Export collections fin_maps.
Class FinMapDom K M D `{FMap M,
A, Lookup K A (M A), A, Empty (M A), A, PartialAlter K A (M A),
......
......@@ -4,8 +4,8 @@
finite maps and collects some theory on it. Most importantly, it proves useful
induction principles for finite maps and implements the tactic
[simplify_map_equality] to simplify goals involving finite maps. *)
Require Import Permutation.
Require Export prelude.relations prelude.vector prelude.orders.
From Coq Require Import Permutation.
From prelude Require Export relations vector orders.
(** * Axiomatization of finite maps *)
(** We require Leibniz equality to be extensional on finite maps. This of
......
(* Copyright (c) 2012-2015, Robbert Krebbers. *)
(* This file is distributed under the terms of the BSD license. *)
Require Export prelude.countable prelude.list.
From prelude Require Export countable list.
Class Finite A `{ x y : A, Decision (x = y)} := {
enum : list A;
......
......@@ -2,8 +2,8 @@
(* This file is distributed under the terms of the BSD license. *)
(** 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. *)
Require Export prelude.countable prelude.fin_maps prelude.fin_map_dom.
Require Import prelude.pmap prelude.mapset.
From prelude Require Export countable fin_maps fin_map_dom.
From prelude Require Import pmap mapset.
(** * The data structure *)
(** We pack a [Pmap] together with a proof that ensures that all keys correspond
......
......@@ -3,8 +3,8 @@
(** 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
integer of type [Z], and contains an unordered list without duplicates. *)
Require Export prelude.fin_maps prelude.listset.
Require Import prelude.zmap.
From prelude Require Export fin_maps listset.
From prelude Require Import zmap.
Record hashset {A} (hash : A Z) := Hashset {
hashset_car : Zmap (list A);
......
......@@ -2,7 +2,7 @@
(* This file is distributed under the terms of the BSD license. *)
(** 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. *)
Require Import prelude.numbers.
From prelude Require Import numbers.
Notation cast_trichotomy T :=
match T with
......
......@@ -2,8 +2,8 @@
(* This file is distributed under the terms of the BSD license. *)
(** This file collects general purpose definitions and theorems on lists that
are not in the Coq standard library. *)
Require Export Permutation.
Require Export prelude.numbers prelude.base prelude.decidable prelude.option.
From Coq Require Export Permutation.
From prelude Require Export numbers base decidable option.
Arguments length {_} _.
Arguments cons {_} _ _.
......
......@@ -2,7 +2,7 @@
(* This file is distributed under the terms of the BSD license. *)
(** This file implements finite set as unordered lists without duplicates
removed. This implementation forms a monad. *)
Require Export prelude.base prelude.decidable prelude.collections prelude.list.
From prelude Require Export base decidable collections list.
Record listset A := Listset { listset_car: list A }.
Arguments listset_car {_} _.
......
......@@ -3,7 +3,7 @@
(** This file implements finite as unordered lists without duplicates.
Although this implementation is slow, it is very useful as decidable equality
is the only constraint on the carrier set. *)
Require Export prelude.base prelude.decidable prelude.collections prelude.list.
From prelude Require Export base decidable collections list.
Record listset_nodup A := ListsetNoDup {
listset_nodup_car : list A; listset_nodup_prf : NoDup listset_nodup_car
......
......@@ -3,7 +3,7 @@
(** This files gives an implementation of finite sets using finite maps with
elements of the unit type. Since maps enjoy extensional equality, the
constructed finite sets do so as well. *)
Require Export prelude.fin_map_dom.
From prelude Require Export fin_map_dom.
Record mapset (M : Type Type) : Type :=
Mapset { mapset_car: M (unit : Type) }.
......
......@@ -3,7 +3,7 @@
(** 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
a list with a proof of canonicity. *)
Require Import prelude.fin_maps prelude.mapset.
From prelude Require Import fin_maps mapset.
Notation natmap_raw A := (list (option A)).
Definition natmap_wf {A} (l : natmap_raw A) :=
......
......@@ -2,8 +2,8 @@
(* This file is distributed under the terms of the BSD license. *)
(** This files extends the implementation of finite over [positive] to finite
maps whose keys range over Coq's data type of binary naturals [N]. *)
Require Import prelude.pmap prelude.mapset.
Require Export prelude.prelude prelude.fin_maps.
From prelude Require Import pmap mapset.
From prelude Require Export prelude fin_maps.
Local Open Scope N_scope.
......
......@@ -3,9 +3,9 @@
(** 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
notations. *)
Require Export Eqdep PArith NArith ZArith NPeano.
Require Import QArith Qcanon.
Require Export prelude.base prelude.decidable prelude.option.
From Coq Require Export Eqdep PArith NArith ZArith NPeano.
From Coq Require Import QArith Qcanon.
From prelude Require Export base decidable option.
Open Scope nat_scope.
Coercion Z.of_nat : nat >-> Z.
......@@ -50,7 +50,7 @@ Proof.
* clear nat_le_pi. intros; exfalso; auto with lia.
* injection 1. intros Hy. by case (nat_le_pi x y p y' q Hy). }
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.
Instance nat_lt_pi: x y : nat, ProofIrrel (x < y).
Proof. apply _. Qed.
......
......@@ -2,7 +2,7 @@
(* This file is distributed under the terms of the BSD license. *)
(** This file collects general purpose definitions and theorems on the option
data type that are not in the Coq standard library. *)
Require Export prelude.base prelude.tactics prelude.decidable.
From prelude Require Export base tactics decidable.
Inductive option_reflect {A} (P : A Prop) (Q : Prop) : option A Type :=
| ReflectSome x : P x option_reflect P Q (Some x)
......
......@@ -2,8 +2,8 @@
(* This file is distributed under the terms of the BSD license. *)
(** 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. *)
Require Export Sorted.
Require Export prelude.base prelude.decidable prelude.tactics prelude.list.
From Coq Require Export Sorted.
From prelude Require Export base decidable tactics list.
(** * Arbitrary pre-, parial and total orders *)
(** 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.
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
Leibniz equality to become extensional. *)
Require Import PArith prelude.mapset.
Require Export prelude.fin_maps.
From Coq Require Import PArith.
From prelude Require Import mapset.
From prelude Require Export fin_maps.
Local Open Scope positive_scope.
Local Hint Extern 0 (@eq positive _ _) => congruence.
......
(* Copyright (c) 2012-2015, Robbert Krebbers. *)
(* This file is distributed under the terms of the BSD license. *)
Require Export
prelude.base
prelude.tactics
prelude.decidable
prelude.orders
prelude.option
prelude.vector
prelude.numbers
prelude.relations
prelude.collections
prelude.fin_collections
prelude.listset
prelude.list
prelude.lexico.
From prelude Require Export
base
tactics
decidable
orders
option
vector
numbers
relations
collections
fin_collections
listset
list
lexico.
(* Copyright (c) 2012-2015, Robbert Krebbers. *)
(* This file is distributed under the terms of the BSD license. *)
Require Export prelude.strings.
Require Import prelude.relations.
Require Import Ascii.
From prelude Require Export strings.
From prelude Require Import relations.
From Coq Require Import Ascii.
Class Pretty A := pretty : A string.
Definition pretty_N_char (x : N) : ascii :=
......
(* Copyright (c) 2012-2015, Robbert Krebbers. *)
(* This file is distributed under the terms of the BSD license. *)
(** This file collects facts on proof irrelevant types/propositions. *)
Require Export Eqdep_dec prelude.tactics.
From Coq Require Import Eqdep_dec.
From prelude Require Export tactics.
Hint Extern 200 (ProofIrrel _) => progress (lazy beta) : typeclass_instances.
......
......@@ -4,8 +4,8 @@
These are particularly useful as we define the operational semantics as a
small step semantics. This file defines a hint database [ars] containing
some theorems on abstract rewriting systems. *)
Require Import Wf_nat.
Require Export prelude.tactics prelude.base.
From Coq Require Import Wf_nat.
From prelude Require Export tactics base.
(** * Definitions *)
Section definitions.
......
(* Copyright (c) 2012-2015, Robbert Krebbers. *)
(* This file is distributed under the terms of the BSD license. *)
(** This file implements sets as functions into Prop. *)
Require Export prelude.prelude.
From prelude Require Export prelude.
Record set (A : Type) : Type := mkSet { set_car : A Prop }.
Arguments mkSet {_} _.
......
(* Copyright (c) 2012-2015, Robbert Krebbers. *)
(* This file is distributed under the terms of the BSD license. *)
Require Export prelude.tactics.
From prelude Require Export tactics.
CoInductive stream (A : Type) : Type := scons : A stream A stream A.
Arguments scons {_} _ _.
......
......@@ -4,8 +4,8 @@
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]
and guarantees logarithmic-time operations. *)
Require Export prelude.fin_maps prelude.pretty.
Require Import prelude.gmap.
From prelude Require Export fin_maps pretty.
From prelude Require Import gmap.
Notation stringmap := (gmap string).
Notation stringset := (gset string).
......@@ -58,4 +58,4 @@ Fixpoint fresh_strings_of_set
| S n =>
let x := fresh_string_of_set s X in
x :: fresh_strings_of_set s n ({[ x ]} X)
end%nat.
\ No newline at end of file
end%nat.
(* Copyright (c) 2012-2015, Robbert Krebbers. *)
(* This file is distributed under the terms of the BSD license. *)
Require Import Ascii.
Require Export String prelude.countable.
From Coq Require Import Ascii.
From Coq Require Export String.
From prelude Require Export countable.
(** * Fix scopes *)
Open Scope string_scope.
......
......@@ -2,9 +2,9 @@
(* This file is distributed under the terms of the BSD license. *)
(** This file collects general purpose tactics that are used throughout
the development. *)
Require Import Omega.
Require Export Psatz.
Require Export prelude.base.
From Coq Require Import Omega.
From Coq Require Export Psatz.
From prelude Require Export base.
Lemma f_equal_dep {A B} (f g : x : A, B x) x : f = g f x = g x.
Proof. intros ->; reflexivity. Qed.
......
......@@ -5,7 +5,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. *)
Require Import prelude.list prelude.finite.
From prelude Require Import list finite.
Open Scope vector_scope.
(** * The fin type *)
......
......@@ -2,8 +2,8 @@
(* This file is distributed under the terms of the BSD license. *)
(** This files extends the implementation of finite over [positive] to finite
maps whose keys range over Coq's data type of binary naturals [Z]. *)
Require Import prelude.pmap prelude.mapset.
Require Export prelude.prelude prelude.fin_maps.
From prelude Require Import pmap mapset.
From prelude Require Export prelude fin_maps.
Local Open Scope Z_scope.
Record Zmap (A : Type) : Type :=
......
Require Export program_logic.hoare.
Require Import program_logic.wsat program_logic.ownership.
From program_logic Require Export hoare.
From program_logic Require Import wsat ownership.
Local Hint Extern 10 (_ _) => omega.
Local Hint Extern 100 (@eq coPset _ _) => eassumption || solve_elem_of.
Local Hint Extern 10 ({_} _) =>
......
Require Export algebra.auth algebra.functor.
Require Export program_logic.invariants program_logic.ghost_ownership.
From algebra Require Export auth functor.
From program_logic Require Export invariants ghost_ownership.
Import uPred.
Section auth.
......
Require Export algebra.iprod program_logic.pviewshifts.
Require Import program_logic.ownership.
From algebra Require Export iprod.
From program_logic Require Export pviewshifts.
From program_logic Require Import ownership.
Import uPred.
(** Index of a CMRA in the product of global CMRAs. *)
......
Require Export program_logic.weakestpre program_logic.viewshifts.
From program_logic Require Export weakestpre viewshifts.
Definition ht {Λ Σ} (E : coPset) (P : iProp Λ Σ)
(e : expr Λ) (Q : val Λ iProp Λ Σ) : iProp Λ Σ := ( (P wp E e Q))%I.
......
Require Export program_logic.hoare program_logic.lifting.
Require Import program_logic.ownership.
From program_logic Require Export hoare lifting.
From program_logic Require Import ownership.
Import uPred.
Local Notation "{{ P } } ef ?@ E {{ Q } }" :=
......
Require Export algebra.base prelude.countable prelude.co_pset.
Require Import program_logic.ownership.
Require Export program_logic.pviewshifts program_logic.weakestpre.
From algebra Require Export base.
From prelude Require Export countable co_pset.
From program_logic Require Import ownership.
From program_logic Require Export pviewshifts weakestpre.
Import uPred.
Local Hint Extern 100 (@eq coPset _ _) => solve_elem_of.
......