Commit 7bb46268 authored by Ralf Jung's avatar Ralf Jung
parents b6d60979 0d0be97b
......@@ -5,18 +5,32 @@ that are used throughout the whole development. Most importantly it contains
abstract interfaces for ordered structures, collections, and various other data
structures. *)
Global Generalizable All Variables.
Global Unset Transparent Obligations.
From Coq Require Export Morphisms RelationClasses List Bool Utf8 Setoid.
Set Default Proof Using "Type".
Export ListNotations.
From Coq.Program Require Export Basics Syntax.
(* Tweak program: don't let it automatically simplify obligations and hide
them from the results of the [Search] commands. *)
(** * Tweak program *)
(** 1. Since we only use Program to solve logical side-conditions, they should
always be made Opaque, otherwise we end up with performance problems due to
Coq blindly unfolding them.
Note that in most cases we use [Next Obligation. (* ... *) Qed.], for which
this option does not matter. However, sometimes we write things like
[Solve Obligations with naive_solver (* ... *)], and then the obligations
should surely be opaque. *)
Global Unset Transparent Obligations.
(** 2. Do not let Program automatically simplify obligations. The default
obligation tactic is [Tactics.program_simpl], which, among other things,
introduces all variables and gives them fresh names. As such, it becomes
impossible to refer to hypotheses in a robust way. *)
Obligation Tactic := idtac.
(** 3. Hide obligations from the results of the [Search] commands. *)
Add Search Blacklist "_obligation_".
(** Sealing off definitions *)
(** * Sealing off definitions *)
Section seal.
Local Set Primitive Projections.
Record seal {A} (f : A) := { unseal : A; seal_eq : unseal = f }.
......@@ -24,7 +38,7 @@ End seal.
Arguments unseal {_ _} _ : assert.
Arguments seal_eq {_ _} _ : assert.
(** Typeclass opaque definitions *)
(** * Typeclass opaque definitions *)
(* The constant [tc_opaque] is used to make definitions opaque for just type
class search. Note that [simpl] is set up to always unfold [tc_opaque]. *)
Definition tc_opaque {A} (x : A) : A := x.
......@@ -865,23 +879,26 @@ Notation "(≫= f )" := (mbind f) (only parsing) : C_scope.
Notation "(≫=)" := (λ m f, mbind f m) (only parsing) : C_scope.
Notation "x ← y ; z" := (y = (λ x : _, z))
(at level 65, only parsing, right associativity) : C_scope.
(at level 100, only parsing, right associativity) : C_scope.
Infix "<$>" := fmap (at level 60, right associativity) : C_scope.
Notation "' ( x1 , x2 ) ← y ; z" :=
(y = (λ x : _, let ' (x1, x2) := x in z))
(at level 65, only parsing, right associativity) : C_scope.
(at level 100, z at level 200, only parsing, right associativity) : C_scope.
Notation "' ( x1 , x2 , x3 ) ← y ; z" :=
(y = (λ x : _, let ' (x1,x2,x3) := x in z))
(at level 65, only parsing, right associativity) : C_scope.
(at level 100, z at level 200, only parsing, right associativity) : C_scope.
Notation "' ( x1 , x2 , x3 , x4 ) ← y ; z" :=
(y = (λ x : _, let ' (x1,x2,x3,x4) := x in z))
(at level 65, only parsing, right associativity) : C_scope.
(at level 100, z at level 200, only parsing, right associativity) : C_scope.
Notation "' ( x1 , x2 , x3 , x4 , x5 ) ← y ; z" :=
(y = (λ x : _, let ' (x1,x2,x3,x4,x5) := x in z))
(at level 65, only parsing, right associativity) : C_scope.
(at level 100, z at level 200, only parsing, right associativity) : C_scope.
Notation "' ( x1 , x2 , x3 , x4 , x5 , x6 ) ← y ; z" :=
(y = (λ x : _, let ' (x1,x2,x3,x4,x5,x6) := x in z))
(at level 65, only parsing, right associativity) : C_scope.
(at level 100, z at level 200, only parsing, right associativity) : C_scope.
Notation "x ;; z" := (x = λ _, z)
(at level 100, z at level 200, only parsing, right associativity): C_scope.
Notation "ps .*1" := (fmap (M:=list) fst ps)
(at level 10, format "ps .*1").
......@@ -891,11 +908,10 @@ Notation "ps .*2" := (fmap (M:=list) snd ps)
Class MGuard (M : Type Type) :=
mguard: P {dec : Decision P} {A}, (P M A) M A.
Arguments mguard _ _ _ !_ _ _ / : assert.
Notation "'guard' P ; o" := (mguard P (λ _, o))
(at level 65, only parsing, right associativity) : C_scope.
Notation "'guard' P 'as' H ; o" := (mguard P (λ H, o))
(at level 65, only parsing, right associativity) : C_scope.
Notation "'guard' P ; z" := (mguard P (λ _, z))
(at level 100, z at level 200, only parsing, right associativity) : C_scope.
Notation "'guard' P 'as' H ; z" := (mguard P (λ H, z))
(at level 100, z at level 200, only parsing, right associativity) : C_scope.
(** * Operations on maps *)
(** In this section we define operational type classes for the operations
......
......@@ -797,7 +797,7 @@ Global Instance collection_guard `{CollectionMonad M} : MGuard M :=
Section collection_monad_base.
Context `{CollectionMonad M}.
Lemma elem_of_guard `{Decision P} {A} (x : A) (X : M A) :
x guard P; X P x X.
(x guard P; X) P x X.
Proof.
unfold mguard, collection_guard; simpl; case_match;
rewrite ?elem_of_empty; naive_solver.
......@@ -805,7 +805,7 @@ Section collection_monad_base.
Lemma elem_of_guard_2 `{Decision P} {A} (x : A) (X : M A) :
P x X x guard P; X.
Proof. by rewrite elem_of_guard. Qed.
Lemma guard_empty `{Decision P} {A} (X : M A) : guard P; X ¬P X .
Lemma guard_empty `{Decision P} {A} (X : M A) : (guard P; X) ¬P X .
Proof.
rewrite !elem_of_equiv_empty; setoid_rewrite elem_of_guard.
destruct (decide P); naive_solver.
......@@ -945,7 +945,7 @@ Section collection_monad.
Lemma collection_bind_singleton {A B} (f : A M B) x : {[ x ]} = f f x.
Proof. set_solver. Qed.
Lemma collection_guard_True {A} `{Decision P} (X : M A) : P guard P; X X.
Lemma collection_guard_True {A} `{Decision P} (X : M A) : P (guard P; X) X.
Proof. set_solver. Qed.
Lemma collection_fmap_compose {A B C} (f : A B) (g : B C) (X : M A) :
g f <$> X g <$> (f <$> X).
......
......@@ -1212,7 +1212,7 @@ End more_merge.
(** Properties of the zip_with function *)
Lemma map_lookup_zip_with {A B C} (f : A B C) (m1 : M A) (m2 : M B) i :
map_zip_with f m1 m2 !! i = x m1 !! i; y m2 !! i; Some (f x y).
map_zip_with f m1 m2 !! i = (x m1 !! i; y m2 !! i; Some (f x y)).
Proof.
unfold map_zip_with. rewrite lookup_merge by done.
by destruct (m1 !! i), (m2 !! i).
......
......@@ -72,7 +72,7 @@ Definition encode_fin `{Finite A} (x : A) : fin (card A) :=
Fin.of_nat_lt (encode_lt_card x).
Program Definition decode_fin `{Finite A} (i : fin (card A)) : A :=
match Some_dec (decode_nat i) return _ with
| inleft (exist _ x _) => x | inright _ => _
| inleft (x _) => x | inright _ => _
end.
Next Obligation.
intros A ?? i ?; exfalso.
......
......@@ -40,10 +40,10 @@ Definition hlam {A As B} (f : A → himpl As B) : himpl (tcons A As) B := f.
Arguments hlam _ _ _ _ _ / : assert.
Definition hcurry {As B} (f : himpl As B) (xs : hlist As) : B :=
(fix go As xs :=
(fix go {As} xs :=
match xs in hlist As return himpl As B B with
| hnil => λ f, f
| @hcons A As x xs => λ f, go As xs (f x)
| hcons x xs => λ f, go xs (f x)
end) _ xs f.
Coercion hcurry : himpl >-> Funclass.
......
......@@ -3394,7 +3394,7 @@ Section zip_with.
Forall2 P l k length (zip_with f l k) = length k.
Proof. induction 1; simpl; auto. Qed.
Lemma lookup_zip_with l k i :
zip_with f l k !! i = x l !! i; y k !! i; Some (f x y).
zip_with f l k !! i = (x l !! i; y k !! i; Some (f x y)).
Proof.
revert k i. induction l; intros [|??] [|?]; f_equal/=; auto.
by destruct (_ !! _).
......
......@@ -336,13 +336,13 @@ Tactic Notation "case_option_guard" :=
let H := fresh in case_option_guard as H.
Lemma option_guard_True {A} P `{Decision P} (mx : option A) :
P guard P; mx = mx.
P (guard P; mx) = mx.
Proof. intros. by case_option_guard. Qed.
Lemma option_guard_False {A} P `{Decision P} (mx : option A) :
¬P guard P; mx = None.
¬P (guard P; mx) = None.
Proof. intros. by case_option_guard. Qed.
Lemma option_guard_iff {A} P Q `{Decision P, Decision Q} (mx : option A) :
(P Q) guard P; mx = guard Q; mx.
(P Q) (guard P; mx) = guard Q; mx.
Proof. intros [??]. repeat case_option_guard; intuition. Qed.
Tactic Notation "simpl_option" "by" tactic3(tac) :=
......
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