Commit dcff8ded by Robbert Krebbers

Use qualified module names and coqc -Q instead of -R.

parent 11790649
 ... @@ -6,8 +6,8 @@ main advantage of these association lists compared to search trees, is that it ... @@ -6,8 +6,8 @@ main advantage of these association lists compared to search trees, is that it has canonical representatives and thus extensional Leibniz equality. Compared has canonical representatives and thus extensional Leibniz equality. Compared to a naive unordered association list, the merge operation (used for unions, to a naive unordered association list, the merge operation (used for unions, intersections, and difference) is also linear-time. *) intersections, and difference) is also linear-time. *) Require Import mapset. Require Import prelude.mapset. Require Export fin_maps. Require Export prelude.fin_maps. (** Because the association list is sorted using [strict lexico] instead of (** Because the association list is sorted using [strict lexico] instead of [lexico], it automatically guarantees that no duplicates exist. *) [lexico], it automatically guarantees that no duplicates exist. *) ... ...
 ... @@ -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 base tactics orders. Require Export prelude.base prelude.tactics prelude.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 list. Require Export prelude.list. Local Obligation Tactic := idtac. Local Obligation Tactic := idtac. Local Open Scope positive. Local Open Scope positive. ... ...
 ... @@ -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 proof_irrel. Require Export prelude.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 list. Require Export prelude.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,8 @@ ... @@ -3,8 +3,8 @@ (** 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 relations listset. Require Import Permutation prelude.relations prelude.listset. Require Export numbers collections. Require Export prelude.numbers prelude.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 collections fin_maps. Require Export prelude.collections prelude.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), ... ...
 ... @@ -5,7 +5,7 @@ finite maps and collects some theory on it. Most importantly, it proves useful ... @@ -5,7 +5,7 @@ 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. Require Import Permutation. Require Export relations vector orders. Require Export prelude.relations prelude.vector prelude.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 countable list. Require Export prelude.countable prelude.list. Obligation Tactic := idtac. Obligation Tactic := idtac. Class Finite A `{∀ x y : A, Decision (x = y)} := { Class Finite A `{∀ x y : A, Decision (x = y)} := { ... ...
 ... @@ -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 fin_maps listset. Require Export prelude.fin_maps prelude.listset. Require Import zmap. Require Import prelude.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 numbers. Require Import prelude.numbers. Notation cast_trichotomy T := Notation cast_trichotomy T := match T with match T with ... ...
 ... @@ -3,7 +3,7 @@ ... @@ -3,7 +3,7 @@ (** 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. Require Export Permutation. Require Export numbers base decidable option. Require Export prelude.numbers prelude.base prelude.decidable prelude.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 base decidable collections list. Require Export prelude.base prelude.decidable prelude.collections prelude.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 base decidable collections list. Require Export prelude.base prelude.decidable prelude.collections prelude.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 fin_map_dom. Require Export prelude.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 fin_maps mapset. Require Import prelude.fin_maps prelude.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 pmap mapset. Require Import prelude.pmap prelude.mapset. Require Export prelude fin_maps. Require Export prelude.prelude prelude.fin_maps. Local Open Scope N_scope. Local Open Scope N_scope. ... ...
 ... @@ -5,7 +5,7 @@ natural numbers, and the type [Z] for integers. It also declares some useful ... @@ -5,7 +5,7 @@ natural numbers, and the type [Z] for integers. It also declares some useful notations. *) notations. *) Require Export Eqdep PArith NArith ZArith NPeano. Require Export Eqdep PArith NArith ZArith NPeano. Require Import QArith Qcanon. Require Import QArith Qcanon. Require Export base decidable. Require Export prelude.base prelude.decidable. Open Scope nat_scope. Open Scope nat_scope. Coercion Z.of_nat : nat >-> Z. Coercion Z.of_nat : nat >-> Z. ... ...
 ... @@ -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 base tactics decidable. Require Export prelude.base prelude.tactics prelude.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) ... ...
 (* 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 mapset. Require Import prelude.mapset. Require Export prelude fin_maps. Require Export prelude.prelude prelude.fin_maps. Record optionmap (M : Type → Type) (A : Type) : Type := Record optionmap (M : Type → Type) (A : Type) : Type := OptionMap { optionmap_None : option A; optionmap_Some : M A }. OptionMap { optionmap_None : option A; optionmap_Some : M A }. ... ...
 ... @@ -3,7 +3,7 @@ ... @@ -3,7 +3,7 @@ (** 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. Require Export Sorted. Require Export base decidable tactics list. Require Export prelude.base prelude.decidable prelude.tactics prelude.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,8 @@ trees (uncompressed Patricia trees) and guarantees logarithmic-time operations. ... @@ -7,8 +7,8 @@ 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 mapset. Require Import PArith prelude.mapset. Require Export fin_maps. Require Export prelude.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 Require Export base prelude.base tactics prelude.tactics decidable prelude.decidable orders prelude.orders option prelude.option vector prelude.vector numbers prelude.numbers relations prelude.relations collections prelude.collections fin_collections prelude.fin_collections listset prelude.listset list prelude.list lexico. prelude.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 numbers option. Require Export prelude.numbers prelude.option. Require Import Ascii String relations. Require Import Ascii String prelude.relations. Infix "+:+" := String.append (at level 60, right associativity) : C_scope. Infix "+:+" := String.append (at level 60, right associativity) : C_scope. Arguments String.append _ _ : simpl never. Arguments String.append _ _ : simpl never. ... ...
 (* 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 tactics. Require Export Eqdep_dec prelude.tactics. Hint Extern 200 (ProofIrrel _) => progress (lazy beta) : typeclass_instances. Hint Extern 200 (ProofIrrel _) => progress (lazy beta) : typeclass_instances. ... ...
 ... @@ -5,7 +5,7 @@ These are particularly useful as we define the operational semantics as a ... @@ -5,7 +5,7 @@ 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. Require Import Wf_nat. Require Export tactics base. Require Export prelude.tactics prelude.base. (** * Definitions *) (** * Definitions *) Section definitions. Section definitions. ... ...