Commit 705bb406 authored by Simon Spies's avatar Simon Spies

Merge branch 'master' of https://gitlab.mpi-sws.org/iris/stdpp

parents 19950ecc 02687b13
Pipeline #18144 failed with stage
in 0 seconds
From stdpp Require Import namespaces strings.
Lemma test1 (N1 N2 : namespace) :
N1 ## N2 N1 @{coPset} N2.
Proof. solve_ndisj. Qed.
Lemma test2 (N1 N2 : namespace) :
N1 ## N2 N1.@"x" @{coPset} N1.@"y" N2.
Proof. solve_ndisj. Qed.
Lemma test3 (N : namespace) :
N @{coPset} N.@"x".
Proof. solve_ndisj. Qed.
Lemma test4 (N : namespace) :
N @{coPset} N.@"x" N.@"y".
Proof. solve_ndisj. Qed.
Lemma test5 (N1 N2 : namespace) :
N1 N2 @{coPset} N1.@"x" N2 N1.@"y".
Proof. solve_ndisj. Qed.
......@@ -328,6 +328,11 @@ Class Trichotomy {A} (R : relation A) :=
Class TrichotomyT {A} (R : relation A) :=
trichotomyT x y : {R x y} + {x = y} + {R y x}.
Notation Involutive R f := (Cancel R f f).
Lemma involutive {A} {R : relation A} (f : A A) `{Involutive R f} x :
R (f (f x)) x.
Proof. auto. Qed.
Arguments irreflexivity {_} _ {_} _ _ : assert.
Arguments inj {_ _ _ _} _ {_} _ _ _ : assert.
Arguments inj2 {_ _ _ _ _ _} _ {_} _ _ _ _ _: assert.
......@@ -753,6 +758,10 @@ Section sig_map.
End sig_map.
Arguments sig_map _ _ _ _ _ _ !_ / : assert.
Definition proj1_ex {P : Prop} {Q : P Prop} (p : x, Q x) : P :=
let '(ex_intro _ x _) := p in x.
Definition proj2_ex {P : Prop} {Q : P Prop} (p : x, Q x) : Q (proj1_ex p) :=
let '(ex_intro _ x H) := p in H.
(** * Operations on sets *)
(** We define operational type classes for the traditional operations and
......
......@@ -91,6 +91,10 @@ Definition bool_decide (P : Prop) {dec : Decision P} : bool :=
Lemma bool_decide_reflect P `{dec : Decision P} : reflect P (bool_decide P).
Proof. unfold bool_decide. destruct dec; [left|right]; assumption. Qed.
Lemma bool_decide_decide P `{!Decision P} :
bool_decide P = if decide P then true else false.
Proof. reflexivity. Qed.
Tactic Notation "case_bool_decide" "as" ident (Hd) :=
match goal with
| H : context [@bool_decide ?P ?dec] |- _ =>
......@@ -108,14 +112,29 @@ Proof. rewrite bool_decide_spec; trivial. Qed.
Lemma bool_decide_pack (P : Prop) {dec : Decision P} : P bool_decide P.
Proof. rewrite bool_decide_spec; trivial. Qed.
Hint Resolve bool_decide_pack : core.
Lemma bool_decide_true (P : Prop) `{Decision P} : P bool_decide P = true.
Proof. case_bool_decide; tauto. Qed.
Lemma bool_decide_false (P : Prop) `{Decision P} : ¬P bool_decide P = false.
Proof. case_bool_decide; tauto. Qed.
Lemma bool_decide_eq_true (P : Prop) `{Decision P} : bool_decide P = true P.
Proof. case_bool_decide; intuition discriminate. Qed.
Lemma bool_decide_eq_false (P : Prop) `{Decision P} : bool_decide P = false ¬P.
Proof. case_bool_decide; intuition discriminate. Qed.
Lemma bool_decide_iff (P Q : Prop) `{Decision P, Decision Q} :
(P Q) bool_decide P = bool_decide Q.
Proof. repeat case_bool_decide; tauto. Qed.
Lemma bool_decide_eq_true_1 P `{!Decision P}: bool_decide P = true P.
Proof. apply bool_decide_eq_true. Qed.
Lemma bool_decide_eq_true_2 P `{!Decision P}: P bool_decide P = true.
Proof. apply bool_decide_eq_true. Qed.
Lemma bool_decide_eq_false_1 P `{!Decision P}: bool_decide P = false ¬P.
Proof. apply bool_decide_eq_false. Qed.
Lemma bool_decide_eq_false_2 P `{!Decision P}: ¬P bool_decide P = false.
Proof. apply bool_decide_eq_false. Qed.
(** Backwards compatibility notations. *)
Notation bool_decide_true := bool_decide_eq_true_2.
Notation bool_decide_false := bool_decide_eq_false_2.
(** * Decidable Sigma types *)
(** Leibniz equality on Sigma types requires the equipped proofs to be
equal as Coq does not support proof irrelevance. For decidable we
......
......@@ -119,6 +119,17 @@ Proof.
eauto using (empty_finite (C:=D)), (union_finite (C:=D)),
(singleton_finite (C:=D)).
Qed.
Global Instance dom_proper `{!Equiv A} : Proper ((@{M A}) ==> ()) (dom D).
Proof.
intros m1 m2 EQm. apply elem_of_equiv. intros i.
rewrite !elem_of_dom, EQm. done.
Qed.
(** If [D] has Leibniz equality, we can show an even stronger result. This is a
common case e.g. when having a [gmap K A] where the key [K] has Leibniz equality
(and thus also [gset K], the usual domain) but the value type [A] does not. *)
Global Instance dom_proper_L `{!Equiv A, !LeibnizEquiv D} :
Proper ((@{M A}) ==> (=)) (dom D) | 0.
Proof. intros ???. unfold_leibniz. by apply dom_proper. Qed.
Context `{!LeibnizEquiv D}.
Lemma dom_empty_L {A} : dom D (@empty (M A) _) = .
......
......@@ -2253,6 +2253,9 @@ Proof. split; firstorder. Qed.
Lemma list_subseteq_nil l : [] l.
Proof. intros x. by rewrite elem_of_nil. Qed.
Global Instance list_subseteq_Permutation: Proper ((≡ₚ) ==> (≡ₚ) ==> ()) (@{list A}) .
Proof. intros l1 l2 Hl k1 k2 Hk. apply forall_proper; intros x. by rewrite Hl, Hk. Qed.
(** ** Properties of the [Forall] and [Exists] predicate *)
Lemma Forall_Exists_dec (P Q : A Prop) (dec : x, {P x} + {Q x}) :
l, {Forall P l} + {Exists Q l}.
......@@ -2408,6 +2411,10 @@ Section Forall_Exists.
intros ?? l. induction l using rev_ind; auto.
rewrite Forall_app, Forall_singleton; intros [??]; auto.
Qed.
Global Instance Forall_Permutation: Proper ((≡ₚ) ==> ()) (Forall P).
Proof. intros l1 l2 Hl. rewrite !Forall_forall. by setoid_rewrite Hl. Qed.
Lemma Exists_exists l : Exists P l x, x l P x.
Proof.
split.
......@@ -2427,6 +2434,9 @@ Section Forall_Exists.
Exists P l ( x, P x Q x) Exists Q l.
Proof. intros H ?. induction H; auto. Defined.
Global Instance Exists_Permutation: Proper ((≡ₚ) ==> ()) (Exists P).
Proof. intros l1 l2 Hl. rewrite !Exists_exists. by setoid_rewrite Hl. Qed.
Lemma Exists_not_Forall l : Exists (not P) l ¬Forall P l.
Proof. induction 1; inversion_clear 1; contradiction. Qed.
Lemma Forall_not_Exists l : Forall (not P) l ¬Exists P l.
......
......@@ -66,35 +66,37 @@ Section namespace.
Lemma ndot_preserve_disjoint_r N E x : E ## N E ## N.@x.
Proof. intros. by apply symmetry, ndot_preserve_disjoint_l. Qed.
Lemma namespace_subseteq_difference E1 E2 E3 :
E1 ## E3 E1 E2 E1 E2 E3.
Proof. set_solver. Qed.
Lemma namespace_subseteq_difference_l E1 E2 E3 : E1 E3 E1 E2 E3.
Proof. set_solver. Qed.
Lemma ndisj_difference_l E N1 N2 : N2 (N1 : coPset) E N1 ## N2.
Proof. set_solver. Qed.
End namespace.
(* The hope is that registering these will suffice to solve most goals
(** The hope is that registering these will suffice to solve most goals
of the forms:
- [N1 ## N2]
- [↑N1 ⊆ E ∖ ↑N2 ∖ .. ∖ ↑Nn]
- [E1 ∖ ↑N1 ⊆ E2 ∖ ↑N2 ∖ .. ∖ ↑Nn] *)
Create HintDb ndisj.
Hint Resolve namespace_subseteq_difference : ndisj.
Hint Extern 0 (_ ## _) => apply ndot_ne_disjoint; congruence : ndisj.
Hint Resolve ndot_preserve_disjoint_l ndot_preserve_disjoint_r : ndisj.
Hint Resolve nclose_subseteq' ndisj_difference_l : ndisj.
Hint Resolve namespace_subseteq_difference_l | 100 : ndisj.
(** Rules for goals of the form [_ ⊆ _] *)
(** If-and-only-if rules. Well, not quite, but for the fragment we are
considering they are. *)
Hint Resolve (subseteq_difference_r (A:=positive) (C:=coPset)) : ndisj.
Hint Resolve (empty_subseteq (A:=positive) (C:=coPset)) : ndisj.
Hint Resolve (union_least (A:=positive) (C:=coPset)) : ndisj.
(** Fallback, loses lots of information but lets other rules make progress. *)
Hint Resolve (subseteq_difference_l (A:=positive) (C:=coPset)) | 100 : ndisj.
Hint Resolve nclose_subseteq' | 100 : ndisj.
(** Rules for goals of the form [_ ## _] *)
(** The base rule that we want to ultimately get down to. *)
Hint Extern 0 (_ ## _) => apply ndot_ne_disjoint; congruence : ndisj.
(** Fallback, loses lots of information but lets other rules make progress.
Tests show trying [disjoint_difference_l1] first gives better performance. *)
Hint Resolve (disjoint_difference_l1 (A:=positive) (C:=coPset)) | 50 : ndisj.
Hint Resolve (disjoint_difference_l2 (A:=positive) (C:=coPset)) | 100 : ndisj.
Hint Resolve ndot_preserve_disjoint_l ndot_preserve_disjoint_r | 100 : ndisj.
Ltac solve_ndisj :=
repeat match goal with
| H : _ _ _ |- _ => apply union_subseteq in H as [??]
end;
solve [eauto 10 with ndisj].
solve [eauto 12 with ndisj].
Hint Extern 1000 => solve_ndisj : solve_ndisj.
......@@ -286,6 +286,18 @@ Section set_unfold_list.
constructor; unfold subseteq, list_subseteq.
apply forall_proper; naive_solver.
Qed.
Global Instance set_unfold_reverse x l P :
SetUnfoldElemOf x l P SetUnfoldElemOf x (reverse l) P.
Proof. constructor. by rewrite elem_of_reverse, (set_unfold_elem_of x l P). Qed.
Global Instance set_unfold_list_fmap {B} (f : A B) l P :
( y, SetUnfoldElemOf y l (P y))
SetUnfoldElemOf x (f <$> l) ( y, x = f y P y).
Proof.
constructor. rewrite elem_of_list_fmap. f_equiv; intros y.
by rewrite (set_unfold_elem_of y l (P y)).
Qed.
End set_unfold_list.
Ltac set_unfold :=
......@@ -653,9 +665,23 @@ Section set.
Lemma difference_mono_r X1 X2 Y : X1 X2 X1 Y X2 Y.
Proof. set_solver. Qed.
Lemma subseteq_difference_r X Y1 Y2 :
X ## Y2 X Y1 X Y1 Y2.
Proof. set_solver. Qed.
Lemma subseteq_difference_l X1 X2 Y : X1 Y X1 X2 Y.
Proof. set_solver. Qed.
(** Disjointness *)
Lemma disjoint_intersection X Y : X ## Y X Y .
Proof. set_solver. Qed.
Lemma disjoint_difference_l1 X1 X2 Y : Y X2 X1 X2 ## Y.
Proof. set_solver. Qed.
Lemma disjoint_difference_l2 X1 X2 Y : X1 ## Y X1 X2 ## Y.
Proof. set_solver. Qed.
Lemma disjoint_difference_r1 X Y1 Y2 : X Y2 X ## Y1 Y2.
Proof. set_solver. Qed.
Lemma disjoint_difference_r2 X Y1 Y2 : X ## Y1 X ## Y1 Y2.
Proof. set_solver. Qed.
Section leibniz.
Context `{!LeibnizEquiv C}.
......@@ -859,6 +885,8 @@ Section quantifiers.
Proof. unfold set_Forall. set_solver. Qed.
Lemma set_Forall_union_inv_2 X Y : set_Forall P (X Y) set_Forall P Y.
Proof. unfold set_Forall. set_solver. Qed.
Lemma set_Forall_list_to_set l : set_Forall P (list_to_set (C:=C) l) Forall P l.
Proof. rewrite Forall_forall. unfold set_Forall. set_solver. Qed.
Lemma set_Exists_empty : ¬set_Exists P ( : C).
Proof. unfold set_Exists. set_solver. Qed.
......@@ -871,6 +899,8 @@ Section quantifiers.
Lemma set_Exists_union_inv X Y :
set_Exists P (X Y) set_Exists P X set_Exists P Y.
Proof. unfold set_Exists. set_solver. Qed.
Lemma set_Exists_list_to_set l : set_Exists P (list_to_set (C:=C) l) Exists P l.
Proof. rewrite Exists_exists. unfold set_Exists. set_solver. Qed.
End quantifiers.
Section more_quantifiers.
......
......@@ -41,6 +41,11 @@ Section merge_sort.
Definition merge_sort : list A list A := merge_sort_aux [].
End merge_sort.
(** Helper definition for [Sorted_reverse] below *)
Inductive TlRel {A} (R : relation A) (a : A) : list A Prop :=
| TlRel_nil : TlRel R a []
| TlRel_cons b l : R b a TlRel R a (l ++ [b]).
(** ** Properties of the [Sorted] and [StronglySorted] predicate *)
Section sorted.
Context {A} (R : relation A).
......@@ -96,26 +101,52 @@ Section sorted.
end); clear go; abstract first [by constructor | by inversion 1].
Defined.
Context {B} (f : A B).
Lemma HdRel_fmap (R1 : relation A) (R2 : relation B) x l :
( y, R1 x y R2 (f x) (f y)) HdRel R1 x l HdRel R2 (f x) (f <$> l).
Proof. destruct 2; constructor; auto. Qed.
Lemma Sorted_fmap (R1 : relation A) (R2 : relation B) l :
( x y, R1 x y R2 (f x) (f y)) Sorted R1 l Sorted R2 (f <$> l).
Proof. induction 2; simpl; constructor; eauto using HdRel_fmap. Qed.
Lemma StronglySorted_fmap (R1 : relation A) (R2 : relation B) l :
( x y, R1 x y R2 (f x) (f y))
StronglySorted R1 l StronglySorted R2 (f <$> l).
Section fmap.
Context {B} (f : A B).
Lemma HdRel_fmap (R1 : relation A) (R2 : relation B) x l :
( y, R1 x y R2 (f x) (f y)) HdRel R1 x l HdRel R2 (f x) (f <$> l).
Proof. destruct 2; constructor; auto. Qed.
Lemma Sorted_fmap (R1 : relation A) (R2 : relation B) l :
( x y, R1 x y R2 (f x) (f y)) Sorted R1 l Sorted R2 (f <$> l).
Proof. induction 2; simpl; constructor; eauto using HdRel_fmap. Qed.
Lemma StronglySorted_fmap (R1 : relation A) (R2 : relation B) l :
( x y, R1 x y R2 (f x) (f y))
StronglySorted R1 l StronglySorted R2 (f <$> l).
Proof.
induction 2; csimpl; constructor;
rewrite ?Forall_fmap; eauto using Forall_impl.
Qed.
End fmap.
Lemma HdRel_reverse l x : HdRel R x l TlRel (flip R) x (reverse l).
Proof. destruct 1; rewrite ?reverse_cons; by constructor. Qed.
Lemma Sorted_snoc l x : Sorted R l TlRel R x l Sorted R (l ++ [x]).
Proof.
induction 2; csimpl; constructor;
rewrite ?Forall_fmap; eauto using Forall_impl.
induction 1 as [|y l Hsort IH Hhd]; intros Htl; simpl.
{ repeat constructor. }
constructor. apply IH.
- inversion Htl as [|? [|??]]; simplify_list_eq; by constructor.
- destruct Hhd; constructor; [|done].
inversion Htl as [|? [|??]]; by try discriminate_list.
Qed.
End sorted.
Lemma Sorted_reverse {A} (R : relation A) l :
Sorted R l Sorted (flip R) (reverse l).
Proof.
induction 1; rewrite ?reverse_nil, ?reverse_cons;
auto using Sorted_snoc, HdRel_reverse.
Qed.
(** ** Correctness of merge sort *)
Section merge_sort_correct.
Context {A} (R : relation A) `{ x y, Decision (R x y)}.
Lemma list_merge_nil_l l2 : list_merge R [] l2 = l2.
Proof. by destruct l2. Qed.
Lemma list_merge_nil_r l1 : list_merge R l1 [] = l1.
Proof. by destruct l1. Qed.
Lemma list_merge_cons x1 x2 l1 l2 :
list_merge R (x1 :: l1) (x2 :: l2) =
if decide (R x1 x2) then x1 :: list_merge R l1 (x2 :: l2)
......
......@@ -355,7 +355,7 @@ Ltac solve_proper_prepare :=
show up in the goal. To check that we actually have an equivalence relation
on functions, we try to eta expand [f], which will only succeed if [f] is
actually a function. *)
let f' := constr:(λ x y, f x y) in
let f' := constr:(λ x, f x) in
(* Now forcefully introduce the first ∀ and other ∀s that show up in the
goal afterwards. *)
intros ?; intros
......@@ -506,6 +506,8 @@ Tactic Notation "naive_solver" tactic(tac) :=
end;
let rec go n :=
repeat match goal with
(**i solve the goal *)
| |- _ => fast_done
(**i intros *)
| |- _, _ => intro
(**i simplification of assumptions *)
......@@ -522,8 +524,6 @@ Tactic Notation "naive_solver" tactic(tac) :=
| H : Is_true (_ && _) |- _ => apply andb_True in H; destruct H
(**i simplify and solve equalities *)
| |- _ => progress simplify_eq/=
(**i solve the goal *)
| |- _ => fast_done
(**i operations that generate more subgoals *)
| |- _ _ => split
| |- Is_true (bool_decide _) => apply (bool_decide_pack _)
......
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