Commit 66c3aff9 authored by Ralf Jung's avatar Ralf Jung

more restrictive Proof Using hints in (most files of the) prelude

parent d6b49ab2
Pipeline #3608 passed with stage
in 10 minutes and 28 seconds
...@@ -9,7 +9,7 @@ Global Set Automatic Coercions Import. ...@@ -9,7 +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*". 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,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 bsets as functions into Prop. *) (** This file implements bsets as functions into Prop. *)
From iris.prelude Require Export prelude. From iris.prelude Require Export prelude.
Set Default Proof Using "Type*". 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,7 +13,7 @@ Since [positive]s are bitstrings, we encode [coPset]s as trees that correspond ...@@ -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. *) to the decision function that map bitstrings to bools. *)
From iris.prelude Require Export collections. From iris.prelude Require Export collections.
From iris.prelude Require Import pmap gmap mapset. From iris.prelude Require Import pmap gmap mapset.
Set Default Proof Using "Type*". Set Default Proof Using "Type".
Local Open Scope positive_scope. Local Open Scope positive_scope.
(** * The tree data structure *) (** * The tree data structure *)
......
(* 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 iris.prelude Require Export list. From iris.prelude Require Export list.
Set Default Proof Using "Type*". Set Default Proof Using "Type".
Local Open Scope positive. Local Open Scope positive.
Class Countable A `{EqDecision A} := { Class Countable A `{EqDecision A} := {
......
(* 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 iris.prelude Require Export countable vector. From iris.prelude Require Export countable vector.
Set Default Proof Using "Type*". Set Default Proof Using "Type".
Class Finite A `{EqDecision A} := { Class Finite A `{EqDecision A} := {
enum : list A; enum : list A;
...@@ -181,12 +181,12 @@ Section forall_exists. ...@@ -181,12 +181,12 @@ Section forall_exists.
Context `{ x, Decision (P x)}. Context `{ x, Decision (P x)}.
Global Instance forall_dec: Decision ( x, P x). Global Instance forall_dec: Decision ( x, P x).
Proof. Proof using Type*.
refine (cast_if (decide (Forall P (enum A)))); refine (cast_if (decide (Forall P (enum A))));
abstract by rewrite <-Forall_finite. abstract by rewrite <-Forall_finite.
Defined. Defined.
Global Instance exists_dec: Decision ( x, P x). Global Instance exists_dec: Decision ( x, P x).
Proof. Proof using Type*.
refine (cast_if (decide (Exists P (enum A)))); refine (cast_if (decide (Exists P (enum A))));
abstract by rewrite <-Exists_finite. abstract by rewrite <-Exists_finite.
Defined. Defined.
......
From iris.prelude Require Export base tactics. From iris.prelude Require Export base tactics.
Set Default Proof Using "Type*". Set Default Proof Using "Type".
Section definitions. Section definitions.
Context {A T : Type} `{EqDecision A}. Context {A T : Type} `{EqDecision A}.
......
...@@ -4,7 +4,7 @@ ...@@ -4,7 +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 iris.prelude Require Export countable fin_maps fin_map_dom. From iris.prelude Require Export countable fin_maps fin_map_dom.
From iris.prelude Require Import pmap mapset set. From iris.prelude Require Import pmap mapset set.
Set Default Proof Using "Type*". 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 iris.prelude Require Import gmap. From iris.prelude Require Import gmap.
Set Default Proof Using "Type*". 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,7 +5,7 @@ using radix-2 search trees. Each hash bucket is thus indexed using an binary ...@@ -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. *) integer of type [Z], and contains an unordered list without duplicates. *)
From iris.prelude Require Export fin_maps listset. From iris.prelude Require Export fin_maps listset.
From iris.prelude Require Import zmap. From iris.prelude Require Import zmap.
Set Default Proof Using "Type*". 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 iris.prelude Require Import tactics. From iris.prelude Require Import tactics.
Set Default Proof Using "Type*". 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,7 +3,7 @@ ...@@ -3,7 +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 iris.prelude Require Import numbers. From iris.prelude Require Import numbers.
Set Default Proof Using "Type*". Set Default Proof Using "Type".
Notation cast_trichotomy T := Notation cast_trichotomy T :=
match T with match T with
......
...@@ -3,7 +3,7 @@ ...@@ -3,7 +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 iris.prelude Require Export collections list. From iris.prelude Require Export collections list.
Set Default Proof Using "Type*". 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,7 +4,7 @@ ...@@ -4,7 +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 iris.prelude Require Export collections list. From iris.prelude Require Export collections list.
Set Default Proof Using "Type*". 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,7 +4,7 @@ ...@@ -4,7 +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 iris.prelude Require Import fin_maps mapset. From iris.prelude Require Import fin_maps mapset.
Set Default Proof Using "Type*". 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,7 +4,7 @@ ...@@ -4,7 +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 iris.prelude Require Import pmap mapset. From iris.prelude Require Import pmap mapset.
From iris.prelude Require Export prelude fin_maps. From iris.prelude Require Export prelude fin_maps.
Set Default Proof Using "Type*". Set Default Proof Using "Type".
Local Open Scope N_scope. Local Open Scope N_scope.
......
...@@ -6,7 +6,7 @@ notations. *) ...@@ -6,7 +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 iris.prelude Require Export base decidable option. From iris.prelude Require Export base decidable option.
Set Default Proof Using "Type*". 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,7 +3,7 @@ ...@@ -3,7 +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 iris.prelude Require Export tactics. From iris.prelude 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 := 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,7 +3,7 @@ ...@@ -3,7 +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 iris.prelude Require Export tactics. From iris.prelude Require Export tactics.
Set Default Proof Using "Type*". Set Default Proof Using "Type".
Section orders. Section orders.
Context {A} {R : relation A}. Context {A} {R : relation A}.
......
...@@ -10,7 +10,7 @@ Leibniz equality to become extensional. *) ...@@ -10,7 +10,7 @@ Leibniz equality to become extensional. *)
From Coq Require Import PArith. From Coq Require Import PArith.
From iris.prelude Require Import mapset countable. From iris.prelude Require Import mapset countable.
From iris.prelude Require Export fin_maps. From iris.prelude Require Export fin_maps.
Set Default Proof Using "Type*". 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,7 +3,7 @@ ...@@ -3,7 +3,7 @@
From iris.prelude Require Export strings. From iris.prelude Require Export strings.
From iris.prelude Require Import relations. From iris.prelude Require Import relations.
From Coq Require Import Ascii. From Coq Require Import Ascii.
Set Default Proof Using "Type*". 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,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 facts on proof irrelevant types/propositions. *) (** This file collects facts on proof irrelevant types/propositions. *)
From iris.prelude Require Export base. From iris.prelude Require Export base.
Set Default Proof Using "Type*". Set Default Proof Using "Type".
Hint Extern 200 (ProofIrrel _) => progress (lazy beta) : typeclass_instances. Hint Extern 200 (ProofIrrel _) => progress (lazy beta) : typeclass_instances.
......
...@@ -6,7 +6,7 @@ small step semantics. This file defines a hint database [ars] containing ...@@ -6,7 +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 iris.prelude Require Export tactics base. From iris.prelude Require Export tactics base.
Set Default Proof Using "Type*". Set Default Proof Using "Type".
(** * Definitions *) (** * Definitions *)
Section definitions. Section definitions.
......
...@@ -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 sets as functions into Prop. *) (** This file implements sets as functions into Prop. *)
From iris.prelude Require Export collections. From iris.prelude Require Export collections.
Set Default Proof Using "Type*". 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.
......
...@@ -4,7 +4,7 @@ ...@@ -4,7 +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 iris.prelude Require Export orders list. From iris.prelude Require Export orders list.
Set Default Proof Using "Type*". 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 iris.prelude Require Export tactics. From iris.prelude Require Export tactics.
Set Default Proof Using "Type*". 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,7 +6,7 @@ search trees (uncompressed Patricia trees) as implemented in the file [pmap] ...@@ -6,7 +6,7 @@ search trees (uncompressed Patricia trees) as implemented in the file [pmap]
and guarantees logarithmic-time operations. *) and guarantees logarithmic-time operations. *)
From iris.prelude Require Export fin_maps pretty. From iris.prelude Require Export fin_maps pretty.
From iris.prelude Require Import gmap. From iris.prelude Require Import gmap.
Set Default Proof Using "Type*". Set Default Proof Using "Type".
Notation stringmap := (gmap string). Notation stringmap := (gmap string).
Notation stringset := (gset string). Notation stringset := (gset string).
......
...@@ -4,7 +4,7 @@ From Coq Require Import Ascii. ...@@ -4,7 +4,7 @@ From Coq Require Import Ascii.
From Coq Require Export String. From Coq Require Export String.
From iris.prelude Require Export list. From iris.prelude Require Export list.
From iris.prelude Require Import countable. From iris.prelude 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 (* To avoid randomly ending up with String.length because this module is
imported hereditarily somewhere. *) imported hereditarily somewhere. *)
......
...@@ -5,7 +5,7 @@ the development. *) ...@@ -5,7 +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 iris.prelude Require Export decidable. From iris.prelude 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. 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,7 +6,7 @@ definitions from the standard library, but renames or changes their notations, ...@@ -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 so that it becomes more consistent with the naming conventions in this
development. *) development. *)
From iris.prelude Require Export list. From iris.prelude Require Export list.
Set Default Proof Using "Type*". Set Default Proof Using "Type".
Open Scope vector_scope. Open Scope vector_scope.
(** * The fin type *) (** * The fin type *)
......
...@@ -4,7 +4,7 @@ ...@@ -4,7 +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 iris.prelude Require Import pmap mapset. From iris.prelude Require Import pmap mapset.
From iris.prelude Require Export prelude fin_maps. From iris.prelude Require Export prelude fin_maps.
Set Default Proof Using "Type*". 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