Commit 8fc1b24b authored by Michael Sammler's avatar Michael Sammler

remove trailing whitespace

This was done using `sed --in-place 's/[[:space:]]\+$//' theories/*.v`.
parent 86cb321a
Pipeline #25853 passed with stage
in 16 minutes and 27 seconds
...@@ -1000,7 +1000,7 @@ Hint Mode UpClose - ! : typeclass_instances. ...@@ -1000,7 +1000,7 @@ Hint Mode UpClose - ! : typeclass_instances.
Notation "↑ x" := (up_close x) (at level 20, format "↑ x"). Notation "↑ x" := (up_close x) (at level 20, format "↑ x").
(** * Monadic operations *) (** * Monadic operations *)
(** We define operational type classes for the monadic operations bind, join (** We define operational type classes for the monadic operations bind, join
and fmap. We use these type classes merely for convenient overloading of and fmap. We use these type classes merely for convenient overloading of
notations and do not formalize any theory on monads (we do not even define a notations and do not formalize any theory on monads (we do not even define a
class with the monad laws). *) class with the monad laws). *)
...@@ -1106,7 +1106,7 @@ Arguments alter {_ _ _ _} _ !_ !_ / : simpl nomatch, assert. ...@@ -1106,7 +1106,7 @@ Arguments alter {_ _ _ _} _ !_ !_ / : simpl nomatch, assert.
(** The function [partial_alter f k m] should update the value at key [k] using the (** The function [partial_alter f k m] should update the value at key [k] using the
function [f], which is called with the original value at key [k] or [None] function [f], which is called with the original value at key [k] or [None]
if [k] is not a member of [m]. The value at [k] should be deleted if [f] if [k] is not a member of [m]. The value at [k] should be deleted if [f]
yields [None]. *) yields [None]. *)
Class PartialAlter (K A M : Type) := Class PartialAlter (K A M : Type) :=
partial_alter: (option A option A) K M M. partial_alter: (option A option A) K M M.
......
...@@ -24,7 +24,7 @@ Proof. ...@@ -24,7 +24,7 @@ Proof.
- by intros x y; rewrite <-(bool_decide_spec (x = y)). - by intros x y; rewrite <-(bool_decide_spec (x = y)).
- split. apply orb_prop_elim. apply orb_prop_intro. - split. apply orb_prop_elim. apply orb_prop_intro.
- split. apply andb_prop_elim. apply andb_prop_intro. - split. apply andb_prop_elim. apply andb_prop_intro.
- intros X Y x; unfold elem_of, boolset_elem_of; simpl. - intros X Y x; unfold elem_of, boolset_elem_of; simpl.
destruct (boolset_car X x), (boolset_car Y x); simpl; tauto. destruct (boolset_car X x), (boolset_car Y x); simpl; tauto.
- done. - done.
Qed. Qed.
......
...@@ -41,7 +41,7 @@ Class FinMap K M `{FMap M, ∀ A, Lookup K A (M A), ∀ A, Empty (M A), ∀ A, ...@@ -41,7 +41,7 @@ Class FinMap K M `{FMap M, ∀ A, Lookup K A (M A), ∀ A, Empty (M A), ∀ A,
elem_of_map_to_list {A} (m : M A) i x : elem_of_map_to_list {A} (m : M A) i x :
(i,x) map_to_list m m !! i = Some x; (i,x) map_to_list m m !! i = Some x;
lookup_omap {A B} (f : A option B) (m : M A) i : lookup_omap {A B} (f : A option B) (m : M A) i :
omap f m !! i = m !! i = f; omap f m !! i = m !! i = f;
lookup_merge {A B C} (f : option A option B option C) lookup_merge {A B C} (f : option A option B option C)
`{!DiagNone f} (m1 : M A) (m2 : M B) i : `{!DiagNone f} (m1 : M A) (m2 : M B) i :
merge f m1 m2 !! i = f (m1 !! i) (m2 !! i) merge f m1 m2 !! i = f (m1 !! i) (m2 !! i)
......
...@@ -50,7 +50,7 @@ Section definitions. ...@@ -50,7 +50,7 @@ Section definitions.
Global Instance gmultiset_dom : Dom (gmultiset A) (gset A) := λ X, Global Instance gmultiset_dom : Dom (gmultiset A) (gset A) := λ X,
let (X) := X in dom _ X. let (X) := X in dom _ X.
End definitions. End definitions.
Typeclasses Opaque gmultiset_elem_of gmultiset_subseteq. Typeclasses Opaque gmultiset_elem_of gmultiset_subseteq.
Typeclasses Opaque gmultiset_elements gmultiset_size gmultiset_empty. Typeclasses Opaque gmultiset_elements gmultiset_size gmultiset_empty.
......
...@@ -29,7 +29,7 @@ Next Obligation. ...@@ -29,7 +29,7 @@ Next Obligation.
Qed. Qed.
Global Program Instance hashset_union: Union (hashset hash) := λ m1 m2, Global Program Instance hashset_union: Union (hashset hash) := λ m1 m2,
let (m1,Hm1) := m1 in let (m2,Hm2) := m2 in let (m1,Hm1) := m1 in let (m2,Hm2) := m2 in
Hashset (union_with (λ l k, Some (list_union l k)) m1 m2) _. Hashset (union_with (λ l k, Some (list_union l k)) m1 m2) _.
Next Obligation. Next Obligation.
intros _ _ m1 Hm1 m2 Hm2 n l'; rewrite lookup_union_with_Some. intros _ _ m1 Hm1 m2 Hm2 n l'; rewrite lookup_union_with_Some.
intros [[??]|[[??]|(l&k&?&?&?)]]; simplify_eq/=; auto. intros [[??]|[[??]|(l&k&?&?&?)]]; simplify_eq/=; auto.
......
...@@ -141,7 +141,7 @@ Instance sig_lexico_po `{Lexico A, !StrictOrder (@lexico A _)} ...@@ -141,7 +141,7 @@ Instance sig_lexico_po `{Lexico A, !StrictOrder (@lexico A _)}
(P : A Prop) `{ x, ProofIrrel (P x)} : StrictOrder (@lexico (sig P) _). (P : A Prop) `{ x, ProofIrrel (P x)} : StrictOrder (@lexico (sig P) _).
Proof. Proof.
unfold lexico, sig_lexico. split. unfold lexico, sig_lexico. split.
- intros [x ?] ?. by apply (irreflexivity lexico x). - intros [x ?] ?. by apply (irreflexivity lexico x).
- intros [x1 ?] [x2 ?] [x3 ?] ??. by trans x2. - intros [x1 ?] [x2 ?] [x3 ?] ??. by trans x2.
Qed. Qed.
Instance sig_lexico_trichotomy `{Lexico A, tA : !TrichotomyT (@lexico A _)} Instance sig_lexico_trichotomy `{Lexico A, tA : !TrichotomyT (@lexico A _)}
......
...@@ -401,7 +401,7 @@ used by [positives_flatten]. *) ...@@ -401,7 +401,7 @@ used by [positives_flatten]. *)
Definition positives_unflatten (p : positive) : option (list positive) := Definition positives_unflatten (p : positive) : option (list positive) :=
positives_unflatten_go p [] 1. positives_unflatten_go p [] 1.
(** [seqZ m n] generates the sequence [m], [m + 1], ..., [m + n - 1] (** [seqZ m n] generates the sequence [m], [m + 1], ..., [m + n - 1]
over integers, provided [0 ≤ n]. If [n < 0], then the range is empty. **) over integers, provided [0 ≤ n]. If [n < 0], then the range is empty. **)
Definition seqZ (m len: Z) : list Z := Definition seqZ (m len: Z) : list Z :=
(λ i: nat, Z.add i m) <$> (seq 0 (Z.to_nat len)). (λ i: nat, Z.add i m) <$> (seq 0 (Z.to_nat len)).
...@@ -4144,7 +4144,7 @@ Section positives_flatten_unflatten. ...@@ -4144,7 +4144,7 @@ Section positives_flatten_unflatten.
rewrite 2!(assoc_L (++)). rewrite 2!(assoc_L (++)).
reflexivity. reflexivity.
Qed. Qed.
Lemma positives_unflatten_go_app p suffix xs acc : Lemma positives_unflatten_go_app p suffix xs acc :
positives_unflatten_go (suffix ++ Preverse (Pdup p)) xs acc = positives_unflatten_go (suffix ++ Preverse (Pdup p)) xs acc =
positives_unflatten_go suffix xs (acc ++ p). positives_unflatten_go suffix xs (acc ++ p).
...@@ -4161,7 +4161,7 @@ Section positives_flatten_unflatten. ...@@ -4161,7 +4161,7 @@ Section positives_flatten_unflatten.
reflexivity. reflexivity.
- reflexivity. - reflexivity.
Qed. Qed.
Lemma positives_unflatten_flatten_go suffix xs acc : Lemma positives_unflatten_flatten_go suffix xs acc :
positives_unflatten_go (suffix ++ positives_flatten_go xs 1) acc 1 = positives_unflatten_go (suffix ++ positives_flatten_go xs 1) acc 1 =
positives_unflatten_go suffix (xs ++ acc) 1. positives_unflatten_go suffix (xs ++ acc) 1.
...@@ -4178,7 +4178,7 @@ Section positives_flatten_unflatten. ...@@ -4178,7 +4178,7 @@ Section positives_flatten_unflatten.
rewrite (left_id_L 1 (++)). rewrite (left_id_L 1 (++)).
reflexivity. reflexivity.
Qed. Qed.
Lemma positives_unflatten_flatten xs : Lemma positives_unflatten_flatten xs :
positives_unflatten (positives_flatten xs) = Some xs. positives_unflatten (positives_flatten xs) = Some xs.
Proof. Proof.
...@@ -4191,7 +4191,7 @@ Section positives_flatten_unflatten. ...@@ -4191,7 +4191,7 @@ Section positives_flatten_unflatten.
rewrite (right_id_L [] (++)%list). rewrite (right_id_L [] (++)%list).
reflexivity. reflexivity.
Qed. Qed.
Lemma positives_flatten_app xs ys : Lemma positives_flatten_app xs ys :
positives_flatten (xs ++ ys) = positives_flatten xs ++ positives_flatten ys. positives_flatten (xs ++ ys) = positives_flatten xs ++ positives_flatten ys.
Proof. Proof.
...@@ -4205,7 +4205,7 @@ Section positives_flatten_unflatten. ...@@ -4205,7 +4205,7 @@ Section positives_flatten_unflatten.
rewrite (assoc_L (++)). rewrite (assoc_L (++)).
reflexivity. reflexivity.
Qed. Qed.
Lemma positives_flatten_cons x xs : Lemma positives_flatten_cons x xs :
positives_flatten (x :: xs) = 1~1~0 ++ Preverse (Pdup x) ++ positives_flatten xs. positives_flatten (x :: xs) = 1~1~0 ++ Preverse (Pdup x) ++ positives_flatten xs.
Proof. Proof.
...@@ -4214,7 +4214,7 @@ Section positives_flatten_unflatten. ...@@ -4214,7 +4214,7 @@ Section positives_flatten_unflatten.
rewrite (assoc_L (++)). rewrite (assoc_L (++)).
reflexivity. reflexivity.
Qed. Qed.
Lemma positives_flatten_suffix (l k : list positive) : Lemma positives_flatten_suffix (l k : list positive) :
l `suffix_of` k → ∃ q, positives_flatten k = q ++ positives_flatten l. l `suffix_of` k → ∃ q, positives_flatten k = q ++ positives_flatten l.
Proof. Proof.
...@@ -4222,7 +4222,7 @@ Section positives_flatten_unflatten. ...@@ -4222,7 +4222,7 @@ Section positives_flatten_unflatten.
exists (positives_flatten l'). exists (positives_flatten l').
apply positives_flatten_app. apply positives_flatten_app.
Qed. Qed.
Lemma positives_flatten_suffix_eq p1 p2 (xs ys : list positive) : Lemma positives_flatten_suffix_eq p1 p2 (xs ys : list positive) :
length xs = length ys → length xs = length ys →
p1 ++ positives_flatten xs = p2 ++ positives_flatten ys → p1 ++ positives_flatten xs = p2 ++ positives_flatten ys →
......
...@@ -29,7 +29,7 @@ Proof. ...@@ -29,7 +29,7 @@ Proof.
destruct X as [l]; split; [|by intros; simplify_eq/=]. destruct X as [l]; split; [|by intros; simplify_eq/=].
rewrite elem_of_equiv_empty; intros Hl. rewrite elem_of_equiv_empty; intros Hl.
destruct l as [|x l]; [done|]. feed inversion (Hl x). left. destruct l as [|x l]; [done|]. feed inversion (Hl x). left.
Qed. Qed.
Global Instance listset_empty_dec (X : listset A) : Decision (X ). Global Instance listset_empty_dec (X : listset A) : Decision (X ).
Proof. Proof.
refine (cast_if (decide (listset_car X = []))); refine (cast_if (decide (listset_car X = [])));
......
...@@ -213,7 +213,7 @@ Proof. ...@@ -213,7 +213,7 @@ Proof.
- by rewrite Preverse_xO, Preverse_app, IH. - by rewrite Preverse_xO, Preverse_app, IH.
- reflexivity. - reflexivity.
Qed. Qed.
Instance Preverse_inj : Inj (=) (=) Preverse. Instance Preverse_inj : Inj (=) (=) Preverse.
Proof. Proof.
intros p q eq. intros p q eq.
...@@ -571,7 +571,7 @@ Proof. ...@@ -571,7 +571,7 @@ Proof.
by apply Qcplus_le_mono_l. by apply Qcplus_le_mono_l.
Qed. Qed.
Lemma Qcplus_nonneg_pos (x y : Qc) : 0 x 0 < y 0 < x + y. Lemma Qcplus_nonneg_pos (x y : Qc) : 0 x 0 < y 0 < x + y.
Proof. rewrite (Qcplus_comm x). auto using Qcplus_pos_nonneg. Qed. Proof. rewrite (Qcplus_comm x). auto using Qcplus_pos_nonneg. Qed.
Lemma Qcplus_pos_pos (x y : Qc) : 0 < x 0 < y 0 < x + y. Lemma Qcplus_pos_pos (x y : Qc) : 0 < x 0 < y 0 < x + y.
Proof. auto using Qcplus_pos_nonneg, Qclt_le_weak. Qed. Proof. auto using Qcplus_pos_nonneg, Qclt_le_weak. Qed.
Lemma Qcplus_nonneg_nonneg (x y : Qc) : 0 x 0 y 0 x + y. Lemma Qcplus_nonneg_nonneg (x y : Qc) : 0 x 0 y 0 x + y.
......
...@@ -564,7 +564,7 @@ Section semi_set. ...@@ -564,7 +564,7 @@ Section semi_set.
Lemma union_list_reverse_L Xs : (reverse Xs) = Xs. Lemma union_list_reverse_L Xs : (reverse Xs) = Xs.
Proof. unfold_leibniz. apply union_list_reverse. Qed. Proof. unfold_leibniz. apply union_list_reverse. Qed.
Lemma empty_union_list_L Xs : Xs = Forall (.= ) Xs. Lemma empty_union_list_L Xs : Xs = Forall (.= ) Xs.
Proof. unfold_leibniz. by rewrite empty_union_list. Qed. Proof. unfold_leibniz. by rewrite empty_union_list. Qed.
End leibniz. End leibniz.
Lemma not_elem_of_iff `{!RelDecision (@{C})} X Y x : Lemma not_elem_of_iff `{!RelDecision (@{C})} X Y x :
...@@ -604,7 +604,7 @@ Section set. ...@@ -604,7 +604,7 @@ Section set.
(** Intersection *) (** Intersection *)
Lemma subseteq_intersection X Y : X Y X Y X. Lemma subseteq_intersection X Y : X Y X Y X.
Proof. set_solver. Qed. Proof. set_solver. Qed.
Lemma subseteq_intersection_1 X Y : X Y X Y X. Lemma subseteq_intersection_1 X Y : X Y X Y X.
Proof. apply subseteq_intersection. Qed. Proof. apply subseteq_intersection. Qed.
Lemma subseteq_intersection_2 X Y : X Y X X Y. Lemma subseteq_intersection_2 X Y : X Y X X Y.
......
...@@ -520,7 +520,7 @@ Ltac find_pat pat tac := ...@@ -520,7 +520,7 @@ Ltac find_pat pat tac :=
tryif tac x then idtac else fail 2 tryif tac x then idtac else fail 2
end. end.
(** Coq's [firstorder] tactic fails or loops on rather small goals already. In (** Coq's [firstorder] tactic fails or loops on rather small goals already. In
particular, on those generated by the tactic [unfold_elem_ofs] which is used particular, on those generated by the tactic [unfold_elem_ofs] which is used
to solve propositions on sets. The [naive_solver] tactic implements an to solve propositions on sets. The [naive_solver] tactic implements an
ad-hoc and incomplete [firstorder]-like solver using Ltac's backtracking ad-hoc and incomplete [firstorder]-like solver using Ltac's backtracking
......
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