Commit 108d1f8d authored by Ralf Jung's avatar Ralf Jung Committed by Robbert Krebbers

make "make quick" quick by adding hints about the used section variables

This patch was created using

  find -name *.v | xargs -L 1 awk -i inplace '{from = 0} /^From/{ from = 1; ever_from = 1} { if (from == 0 && seen == 0 && ever_from == 1) { print "Set Default Proof Using \"Type*\"."; seen = 1 } }1 '

and some minor manual editing
parent 50b9555d
...@@ -9,6 +9,7 @@ Global Set Automatic Coercions Import. ...@@ -9,6 +9,7 @@ Global Set Automatic Coercions Import.
Global Set Asymmetric Patterns. Global Set Asymmetric Patterns.
Global Unset Transparent Obligations. Global Unset Transparent Obligations.
From Coq Require Export Morphisms RelationClasses List Bool Utf8 Setoid. From Coq Require Export Morphisms RelationClasses List Bool Utf8 Setoid.
Set Default Proof Using "Type*".
Export ListNotations. Export ListNotations.
From Coq.Program Require Export Basics Syntax. From Coq.Program Require Export Basics Syntax.
Obligation Tactic := idtac. Obligation Tactic := idtac.
......
...@@ -2,6 +2,7 @@ ...@@ -2,6 +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 bsets as functions into Prop. *) (** This file implements bsets as functions into Prop. *)
From stdpp Require Export prelude. From stdpp Require Export prelude.
Set Default Proof Using "Type*".
Record bset (A : Type) : Type := mkBSet { bset_car : A bool }. Record bset (A : Type) : Type := mkBSet { bset_car : A bool }.
Arguments mkBSet {_} _. Arguments mkBSet {_} _.
......
...@@ -13,6 +13,7 @@ Since [positive]s are bitstrings, we encode [coPset]s as trees that correspond ...@@ -13,6 +13,7 @@ Since [positive]s are bitstrings, we encode [coPset]s as trees that correspond
to the decision function that map bitstrings to bools. *) to the decision function that map bitstrings to bools. *)
From stdpp Require Export collections. From stdpp Require Export collections.
From stdpp Require Import pmap gmap mapset. From stdpp Require Import pmap gmap mapset.
Set Default Proof Using "Type*".
Local Open Scope positive_scope. Local Open Scope positive_scope.
(** * The tree data structure *) (** * The tree data structure *)
......
...@@ -4,6 +4,7 @@ ...@@ -4,6 +4,7 @@
importantly, it implements some tactics to automatically solve goals involving importantly, it implements some tactics to automatically solve goals involving
collections. *) collections. *)
From stdpp Require Export orders list. From stdpp Require Export orders list.
Set Default Proof Using "Type*".
Instance collection_equiv `{ElemOf A C} : Equiv C := λ X Y, Instance collection_equiv `{ElemOf A C} : Equiv 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. *)
From stdpp Require Export list. From stdpp Require Export list.
Set Default Proof Using "Type*".
Local Open Scope positive. Local Open Scope positive.
Class Countable A `{EqDecision A} := { Class Countable A `{EqDecision A} := {
......
...@@ -4,6 +4,7 @@ ...@@ -4,6 +4,7 @@
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. *)
From stdpp Require Export proof_irrel. From stdpp Require Export proof_irrel.
Set Default Proof Using "Type*".
Hint Extern 200 (Decision _) => progress (lazy beta) : typeclass_instances. Hint Extern 200 (Decision _) => progress (lazy beta) : typeclass_instances.
......
...@@ -6,6 +6,7 @@ principles on finite collections . *) ...@@ -6,6 +6,7 @@ principles on finite collections . *)
From Coq Require Import Permutation. From Coq Require Import Permutation.
From stdpp Require Import relations listset. From stdpp Require Import relations listset.
From stdpp Require Export numbers collections. From stdpp Require Export numbers collections.
Set Default Proof Using "Type*".
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}
......
...@@ -4,6 +4,7 @@ ...@@ -4,6 +4,7 @@
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. *)
From stdpp Require Export collections fin_maps. From stdpp Require Export collections fin_maps.
Set Default Proof Using "Type*".
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),
......
...@@ -6,6 +6,7 @@ induction principles for finite maps and implements the tactic ...@@ -6,6 +6,7 @@ induction principles for finite maps and implements the tactic
[simplify_map_eq] to simplify goals involving finite maps. *) [simplify_map_eq] to simplify goals involving finite maps. *)
From Coq Require Import Permutation. From Coq Require Import Permutation.
From stdpp Require Export relations orders vector. From stdpp Require Export relations orders vector.
Set Default Proof Using "Type*".
(** * 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. *)
From stdpp Require Export countable vector. From stdpp Require Export countable vector.
Set Default Proof Using "Type*".
Class Finite A `{EqDecision A} := { Class Finite A `{EqDecision A} := {
enum : list A; enum : list A;
......
From stdpp Require Export base tactics. From stdpp Require Export base tactics.
Set Default Proof Using "Type*".
Section definitions. Section definitions.
Context {A T : Type} `{EqDecision A}. Context {A T : Type} `{EqDecision A}.
......
...@@ -4,6 +4,7 @@ ...@@ -4,6 +4,7 @@
type. The implementation is based on [Pmap]s, radix-2 search trees. *) 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 Export countable fin_maps fin_map_dom.
From stdpp Require Import pmap mapset set. From stdpp Require Import pmap mapset set.
Set Default Proof Using "Type*".
(** * 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
......
(* Copyright (c) 2012-2016, Robbert Krebbers. *) (* Copyright (c) 2012-2016, Robbert Krebbers. *)
(* This file is distributed under the terms of the BSD license. *) (* This file is distributed under the terms of the BSD license. *)
From stdpp Require Import gmap. From stdpp Require Import gmap.
Set Default Proof Using "Type*".
Record gmultiset A `{Countable A} := GMultiSet { gmultiset_car : gmap A nat }. Record gmultiset A `{Countable A} := GMultiSet { gmultiset_car : gmap A nat }.
Arguments GMultiSet {_ _ _} _. Arguments GMultiSet {_ _ _} _.
......
...@@ -5,6 +5,7 @@ using radix-2 search trees. Each hash bucket is thus indexed using an binary ...@@ -5,6 +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. *) integer of type [Z], and contains an unordered list without duplicates. *)
From stdpp Require Export fin_maps listset. From stdpp Require Export fin_maps listset.
From stdpp Require Import zmap. From stdpp Require Import zmap.
Set Default Proof Using "Type*".
Record hashset {A} (hash : A Z) := Hashset { Record hashset {A} (hash : A Z) := Hashset {
hashset_car : Zmap (list A); hashset_car : Zmap (list A);
......
From stdpp Require Import tactics. From stdpp Require Import tactics.
Set Default Proof Using "Type*".
Local Set Universe Polymorphism. Local Set Universe Polymorphism.
(* Not using [list Type] in order to avoid universe inconsistencies *) (* Not using [list Type] in order to avoid universe inconsistencies *)
......
...@@ -3,6 +3,7 @@ ...@@ -3,6 +3,7 @@
(** 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. *)
From stdpp Require Import numbers. From stdpp Require Import numbers.
Set Default Proof Using "Type*".
Notation cast_trichotomy T := Notation cast_trichotomy T :=
match T with match T with
......
...@@ -4,6 +4,7 @@ ...@@ -4,6 +4,7 @@
are not in the Coq standard library. *) are not in the Coq standard library. *)
From Coq Require Export Permutation. From Coq Require Export Permutation.
From stdpp Require Export numbers base option. From stdpp Require Export numbers base option.
Set Default Proof Using "Type*".
Arguments length {_} _. Arguments length {_} _.
Arguments cons {_} _ _. Arguments cons {_} _ _.
......
...@@ -3,6 +3,7 @@ ...@@ -3,6 +3,7 @@
(** 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. *)
From stdpp Require Export collections list. From stdpp Require Export collections list.
Set Default Proof Using "Type*".
Record listset A := Listset { listset_car: list A }. Record listset A := Listset { listset_car: list A }.
Arguments listset_car {_} _. Arguments listset_car {_} _.
......
...@@ -4,6 +4,7 @@ ...@@ -4,6 +4,7 @@
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. *)
From stdpp Require Export collections list. From stdpp Require Export collections list.
Set Default Proof Using "Type*".
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
......
...@@ -4,6 +4,7 @@ ...@@ -4,6 +4,7 @@
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. *)
From stdpp Require Export fin_map_dom. From stdpp Require Export fin_map_dom.
(* FIXME: This file needs a 'Proof Using' hint. *)
Record mapset (M : Type Type) : Type := Record mapset (M : Type Type) : Type :=
Mapset { mapset_car: M (unit : Type) }. Mapset { mapset_car: M (unit : Type) }.
......
...@@ -4,6 +4,7 @@ ...@@ -4,6 +4,7 @@
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. *)
From stdpp Require Import fin_maps mapset. From stdpp Require Import fin_maps mapset.
Set Default Proof Using "Type*".
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) :=
......
...@@ -4,6 +4,7 @@ ...@@ -4,6 +4,7 @@
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]. *)
From stdpp Require Import pmap mapset. From stdpp Require Import pmap mapset.
From stdpp Require Export prelude fin_maps. From stdpp Require Export prelude fin_maps.
Set Default Proof Using "Type*".
Local Open Scope N_scope. Local Open Scope N_scope.
......
...@@ -6,6 +6,7 @@ notations. *) ...@@ -6,6 +6,7 @@ notations. *)
From Coq Require Export EqdepFacts PArith NArith ZArith NPeano. From Coq Require Export EqdepFacts PArith NArith ZArith NPeano.
From Coq Require Import QArith Qcanon. From Coq Require Import QArith Qcanon.
From stdpp Require Export base decidable option. From stdpp Require Export base decidable option.
Set Default Proof Using "Type*".
Open Scope nat_scope. Open Scope nat_scope.
Coercion Z.of_nat : nat >-> Z. Coercion Z.of_nat : nat >-> Z.
......
...@@ -3,6 +3,7 @@ ...@@ -3,6 +3,7 @@
(** 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. *)
From stdpp Require Export tactics. From stdpp Require Export tactics.
Set Default Proof Using "Type*".
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)
......
...@@ -3,6 +3,7 @@ ...@@ -3,6 +3,7 @@
(** Properties about arbitrary pre-, partial, and total orders. We do not use (** Properties about arbitrary pre-, partial, and total orders. We do not use
the relation [⊆] because we often have multiple orders on the same structure *) the relation [⊆] because we often have multiple orders on the same structure *)
From stdpp Require Export tactics. From stdpp Require Export tactics.
Set Default Proof Using "Type*".
Section orders. Section orders.
Context {A} {R : relation A}. Context {A} {R : relation A}.
......
...@@ -10,6 +10,7 @@ Leibniz equality to become extensional. *) ...@@ -10,6 +10,7 @@ Leibniz equality to become extensional. *)
From Coq Require Import PArith. From Coq Require Import PArith.
From stdpp Require Import mapset countable. From stdpp Require Import mapset countable.
From stdpp Require Export fin_maps. From stdpp Require Export fin_maps.
Set Default Proof Using "Type*".
Local Open Scope positive_scope. Local Open Scope positive_scope.
Local Hint Extern 0 (@eq positive _ _) => congruence. Local Hint Extern 0 (@eq positive _ _) => congruence.
......
...@@ -3,6 +3,7 @@ ...@@ -3,6 +3,7 @@
From stdpp Require Export strings. From stdpp Require Export strings.
From stdpp Require Import relations. From stdpp Require Import relations.
From Coq Require Import Ascii. From Coq Require Import Ascii.
Set Default Proof Using "Type*".
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 :=
......
...@@ -2,6 +2,7 @@ ...@@ -2,6 +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 facts on proof irrelevant types/propositions. *) (** This file collects facts on proof irrelevant types/propositions. *)
From stdpp Require Export base. From stdpp Require Export base.
Set Default Proof Using "Type*".
Hint Extern 200 (ProofIrrel _) => progress (lazy beta) : typeclass_instances. Hint Extern 200 (ProofIrrel _) => progress (lazy beta) : typeclass_instances.
......
...@@ -6,6 +6,7 @@ small step semantics. This file defines a hint database [ars] containing ...@@ -6,6 +6,7 @@ small step semantics. This file defines a hint database [ars] containing
some theorems on abstract rewriting systems. *) some theorems on abstract rewriting systems. *)
From Coq Require Import Wf_nat. From Coq Require Import Wf_nat.
From stdpp Require Export tactics base. From stdpp Require Export tactics base.
Set Default Proof Using "Type*".
(** * Definitions *) (** * Definitions *)
Section definitions. Section definitions.
......
...@@ -2,6 +2,7 @@ ...@@ -2,6 +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 sets as functions into Prop. *) (** This file implements sets as functions into Prop. *)
From stdpp Require Export collections. From stdpp Require Export collections.
Set Default Proof Using "Type*".
Record set (A : Type) : Type := mkSet { set_car : A Prop }. Record set (A : Type) : Type := mkSet { set_car : A Prop }.
Add Printing Constructor set. Add Printing Constructor set.
...@@ -51,4 +52,4 @@ Proof. intros HPQ. constructor. apply HPQ. Qed. ...@@ -51,4 +52,4 @@ Proof. intros HPQ. constructor. apply HPQ. Qed.
Global Opaque set_elem_of set_top set_empty set_singleton. Global Opaque set_elem_of set_top set_empty set_singleton.
Global Opaque set_union set_intersection set_difference. Global Opaque set_union set_intersection set_difference.
Global Opaque set_ret set_bind set_fmap set_join. Global Opaque set_ret set_bind set_fmap set_join.
\ No newline at end of file
...@@ -4,6 +4,7 @@ ...@@ -4,6 +4,7 @@
standard library, but without using the module system. *) standard library, but without using the module system. *)
From Coq Require Export Sorted. From Coq Require Export Sorted.
From stdpp Require Export orders list. From stdpp Require Export orders list.
Set Default Proof Using "Type*".
Section merge_sort. Section merge_sort.
Context {A} (R : relation A) `{ x y, Decision (R x y)}. Context {A} (R : relation A) `{ x y, Decision (R 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. *)
From stdpp Require Export tactics. From stdpp Require Export tactics.
Set Default Proof Using "Type*".
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 {_} _ _.
......
...@@ -6,6 +6,7 @@ search trees (uncompressed Patricia trees) as implemented in the file [pmap] ...@@ -6,6 +6,7 @@ search trees (uncompressed Patricia trees) as implemented in the file [pmap]
and guarantees logarithmic-time operations. *) and guarantees logarithmic-time operations. *)
From stdpp Require Export fin_maps pretty. From stdpp Require Export fin_maps pretty.
From stdpp Require Import gmap. From stdpp Require Import gmap.
Set Default Proof Using "Type*".
Notation stringmap := (gmap string). Notation stringmap := (gmap string).
Notation stringset := (gset string). Notation stringset := (gset string).
......
...@@ -4,6 +4,7 @@ From Coq Require Import Ascii. ...@@ -4,6 +4,7 @@ From Coq Require Import Ascii.
From Coq Require Export String. From Coq Require Export String.
From stdpp Require Export list. From stdpp Require Export list.
From stdpp Require Import countable. From stdpp Require Import countable.
Set Default Proof Using "Type*".
(* To avoid randomly ending up with String.length because this module is (* To avoid randomly ending up with String.length because this module is
imported hereditarily somewhere. *) imported hereditarily somewhere. *)
......
...@@ -5,6 +5,7 @@ the development. *) ...@@ -5,6 +5,7 @@ the development. *)
From Coq Require Import Omega. From Coq Require Import Omega.
From Coq Require Export Lia. From Coq Require Export Lia.
From stdpp Require Export decidable. From stdpp Require Export decidable.
Set Default Proof Using "Type*".
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.
......
...@@ -6,6 +6,7 @@ definitions from the standard library, but renames or changes their notations, ...@@ -6,6 +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 so that it becomes more consistent with the naming conventions in this
development. *) development. *)
From stdpp Require Export list. From stdpp Require Export list.
Set Default Proof Using "Type*".
Open Scope vector_scope. Open Scope vector_scope.
(** * The fin type *) (** * The fin type *)
......
...@@ -4,6 +4,7 @@ ...@@ -4,6 +4,7 @@
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]. *)
From stdpp Require Import pmap mapset. From stdpp Require Import pmap mapset.
From stdpp Require Export prelude fin_maps. From stdpp Require Export prelude fin_maps.
Set Default Proof Using "Type*".
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