Commit 9041e6d8 authored by Robbert's avatar Robbert

Merge branch 'robbert/issue42' into 'master'

Disambiguate Haskell-style notations for partially applied operators

Closes #42

See merge request !93
parents b53cbe77 3a1f5195
Pipeline #19783 passed with stage
in 14 minutes and 29 seconds
...@@ -6,6 +6,10 @@ API-breaking change is listed. ...@@ -6,6 +6,10 @@ API-breaking change is listed.
- Rename `dom_map_filter` into `dom_map_filter_subseteq` and repurpose - Rename `dom_map_filter` into `dom_map_filter_subseteq` and repurpose
`dom_map_filter` for the version with the equality. This follows the naming `dom_map_filter` for the version with the equality. This follows the naming
convention for similar lemmas. convention for similar lemmas.
- Disambiguate Haskell-style notations for partially applied operators. For
example, change `(!! i)` into `(.!! x)` so that `!!` can also be used as a
prefix, as done in VST. A sed script to perform the renaming can be found at:
https://gitlab.mpi-sws.org/iris/stdpp/merge_requests/93
## std++ 1.2.1 (released 2019-08-29) ## std++ 1.2.1 (released 2019-08-29)
......
This diff is collapsed.
...@@ -121,7 +121,7 @@ Instance map_difference `{Merge M} {A} : Difference (M A) := ...@@ -121,7 +121,7 @@ Instance map_difference `{Merge M} {A} : Difference (M A) :=
of the elements. Implemented by conversion to lists, so not very efficient. *) of the elements. Implemented by conversion to lists, so not very efficient. *)
Definition map_imap `{ A, Insert K A (M A), A, Empty (M A), Definition map_imap `{ A, Insert K A (M A), A, Empty (M A),
A, FinMapToList K A (M A)} {A B} (f : K A option B) (m : M A) : M B := A, FinMapToList K A (M A)} {A B} (f : K A option B) (m : M A) : M B :=
list_to_map (omap (λ ix, (fst ix,) <$> curry f ix) (map_to_list m)). list_to_map (omap (λ ix, (fst ix ,.) <$> curry f ix) (map_to_list m)).
(* The zip operation on maps combines two maps key-wise. The keys of resulting (* The zip operation on maps combines two maps key-wise. The keys of resulting
map correspond to the keys that are in both maps. *) map correspond to the keys that are in both maps. *)
...@@ -507,7 +507,7 @@ Lemma insert_empty {A} i (x : A) : <[i:=x]>(∅ : M A) = {[i := x]}. ...@@ -507,7 +507,7 @@ Lemma insert_empty {A} i (x : A) : <[i:=x]>(∅ : M A) = {[i := x]}.
Proof. done. Qed. Proof. done. Qed.
Lemma insert_non_empty {A} (m : M A) i x : <[i:=x]>m . Lemma insert_non_empty {A} (m : M A) i x : <[i:=x]>m .
Proof. Proof.
intros Hi%(f_equal (!! i)). by rewrite lookup_insert, lookup_empty in Hi. intros Hi%(f_equal (.!! i)). by rewrite lookup_insert, lookup_empty in Hi.
Qed. Qed.
Lemma insert_subseteq {A} (m : M A) i x : m !! i = None m <[i:=x]>m. Lemma insert_subseteq {A} (m : M A) i x : m !! i = None m <[i:=x]>m.
...@@ -575,7 +575,7 @@ Lemma lookup_singleton_ne {A} i j (x : A) : ...@@ -575,7 +575,7 @@ Lemma lookup_singleton_ne {A} i j (x : A) :
Proof. by rewrite lookup_singleton_None. Qed. Proof. by rewrite lookup_singleton_None. Qed.
Lemma map_non_empty_singleton {A} i (x : A) : {[i := x]} ( : M A). Lemma map_non_empty_singleton {A} i (x : A) : {[i := x]} ( : M A).
Proof. Proof.
intros Hix. apply (f_equal (!! i)) in Hix. intros Hix. apply (f_equal (.!! i)) in Hix.
by rewrite lookup_empty, lookup_singleton in Hix. by rewrite lookup_empty, lookup_singleton in Hix.
Qed. Qed.
Lemma insert_singleton {A} i (x y : A) : <[i:=y]>({[i := x]} : M A) = {[i := y]}. Lemma insert_singleton {A} i (x y : A) : <[i:=y]>({[i := x]} : M A) = {[i := y]}.
...@@ -1625,7 +1625,7 @@ Lemma lookup_union_None {A} (m1 m2 : M A) i : ...@@ -1625,7 +1625,7 @@ Lemma lookup_union_None {A} (m1 m2 : M A) i :
Proof. rewrite lookup_union. destruct (m1 !! i), (m2 !! i); naive_solver. Qed. Proof. rewrite lookup_union. destruct (m1 !! i), (m2 !! i); naive_solver. Qed.
Lemma map_positive_l {A} (m1 m2 : M A) : m1 m2 = m1 = . Lemma map_positive_l {A} (m1 m2 : M A) : m1 m2 = m1 = .
Proof. Proof.
intros Hm. apply map_empty. intros i. apply (f_equal (!! i)) in Hm. intros Hm. apply map_empty. intros i. apply (f_equal (.!! i)) in Hm.
rewrite lookup_empty, lookup_union_None in Hm; tauto. rewrite lookup_empty, lookup_union_None in Hm; tauto.
Qed. Qed.
Lemma map_positive_l_alt {A} (m1 m2 : M A) : m1 m1 m2 . Lemma map_positive_l_alt {A} (m1 m2 : M A) : m1 m1 m2 .
......
...@@ -18,15 +18,15 @@ Definition card A `{Finite A} := length (enum A). ...@@ -18,15 +18,15 @@ Definition card A `{Finite A} := length (enum A).
Program Definition finite_countable `{Finite A} : Countable A := {| Program Definition finite_countable `{Finite A} : Countable A := {|
encode := λ x, encode := λ x,
Pos.of_nat $ S $ default 0 $ fst <$> list_find (x =) (enum A); Pos.of_nat $ S $ default 0 $ fst <$> list_find (x =.) (enum A);
decode := λ p, enum A !! pred (Pos.to_nat p) decode := λ p, enum A !! pred (Pos.to_nat p)
|}. |}.
Arguments Pos.of_nat : simpl never. Arguments Pos.of_nat : simpl never.
Next Obligation. Next Obligation.
intros ?? [xs Hxs HA] x; unfold encode, decode; simpl. intros ?? [xs Hxs HA] x; unfold encode, decode; simpl.
destruct (list_find_elem_of (x =) xs x) as [[i y] Hi]; auto. destruct (list_find_elem_of (x =.) xs x) as [[i y] Hi]; auto.
rewrite Nat2Pos.id by done; simpl; rewrite Hi; simpl. rewrite Nat2Pos.id by done; simpl; rewrite Hi; simpl.
destruct (list_find_Some (x =) xs i y); naive_solver. destruct (list_find_Some (x =.) xs i y); naive_solver.
Qed. Qed.
Hint Immediate finite_countable : typeclass_instances. Hint Immediate finite_countable : typeclass_instances.
...@@ -38,7 +38,7 @@ Proof. ...@@ -38,7 +38,7 @@ Proof.
destruct finA as [xs Hxs HA]; unfold encode_nat, encode, card; simpl. destruct finA as [xs Hxs HA]; unfold encode_nat, encode, card; simpl.
rewrite Nat2Pos.id by done; simpl. rewrite Nat2Pos.id by done; simpl.
destruct (list_find _ xs) as [[i y]|] eqn:?; simpl. destruct (list_find _ xs) as [[i y]|] eqn:?; simpl.
- destruct (list_find_Some (x =) xs i y); eauto using lookup_lt_Some. - destruct (list_find_Some (x =.) xs i y); eauto using lookup_lt_Some.
- destruct xs; simpl. exfalso; eapply not_elem_of_nil, (HA x). lia. - destruct xs; simpl. exfalso; eapply not_elem_of_nil, (HA x). lia.
Qed. Qed.
Lemma encode_decode A `{finA: Finite A} i : Lemma encode_decode A `{finA: Finite A} i :
...@@ -48,8 +48,8 @@ Proof. ...@@ -48,8 +48,8 @@ Proof.
unfold encode_nat, decode_nat, encode, decode, card; simpl. unfold encode_nat, decode_nat, encode, decode, card; simpl.
intros Hi. apply lookup_lt_is_Some in Hi. destruct Hi as [x Hx]. intros Hi. apply lookup_lt_is_Some in Hi. destruct Hi as [x Hx].
exists x. rewrite !Nat2Pos.id by done; simpl. exists x. rewrite !Nat2Pos.id by done; simpl.
destruct (list_find_elem_of (x =) xs x) as [[j y] Hj]; auto. destruct (list_find_elem_of (x =.) xs x) as [[j y] Hj]; auto.
destruct (list_find_Some (x =) xs j y) as [? ->]; auto. destruct (list_find_Some (x =.) xs j y) as [? ->]; auto.
rewrite Hj; csimpl; eauto using NoDup_lookup. rewrite Hj; csimpl; eauto using NoDup_lookup.
Qed. Qed.
Lemma find_Some `{finA: Finite A} P `{ x, Decision (P x)} (x : A) : Lemma find_Some `{finA: Finite A} P `{ x, Decision (P x)} (x : A) :
...@@ -282,7 +282,7 @@ Lemma sum_card `{Finite A, Finite B} : card (A + B) = card A + card B. ...@@ -282,7 +282,7 @@ Lemma sum_card `{Finite A, Finite B} : card (A + B) = card A + card B.
Proof. unfold card. simpl. by rewrite app_length, !fmap_length. Qed. Proof. unfold card. simpl. by rewrite app_length, !fmap_length. Qed.
Program Instance prod_finite `{Finite A, Finite B} : Finite (A * B)%type := Program Instance prod_finite `{Finite A, Finite B} : Finite (A * B)%type :=
{| enum := foldr (λ x, (pair x <$> enum B ++)) [] (enum A) |}. {| enum := foldr (λ x, (pair x <$> enum B ++.)) [] (enum A) |}.
Next Obligation. Next Obligation.
intros ??????. induction (NoDup_enum A) as [|x xs Hx Hxs IH]; simpl. intros ??????. induction (NoDup_enum A) as [|x xs Hx Hxs IH]; simpl.
{ constructor. } { constructor. }
...@@ -312,7 +312,7 @@ Definition list_enum {A} (l : list A) : ∀ n, list { l : list A | length l = n ...@@ -312,7 +312,7 @@ Definition list_enum {A} (l : list A) : ∀ n, list { l : list A | length l = n
fix go n := fix go n :=
match n with match n with
| 0 => [[]eq_refl] | 0 => [[]eq_refl]
| S n => foldr (λ x, (sig_map (x ::) (λ _ H, f_equal S H) <$> (go n) ++)) [] l | S n => foldr (λ x, (sig_map (x ::.) (λ _ H, f_equal S H) <$> (go n) ++.)) [] l
end. end.
Program Instance list_finite `{Finite A} n : Finite { l : list A | length l = n } := Program Instance list_finite `{Finite A} n : Finite { l : list A | length l = n } :=
......
...@@ -73,7 +73,7 @@ Instance gmap_merge `{Countable K} : Merge (gmap K) := λ A B C f m1 m2, ...@@ -73,7 +73,7 @@ Instance gmap_merge `{Countable K} : Merge (gmap K) := λ A B C f m1 m2,
(bool_decide_unpack _ Hm1) (bool_decide_unpack _ Hm2))). (bool_decide_unpack _ Hm1) (bool_decide_unpack _ Hm2))).
Instance gmap_to_list `{Countable K} {A} : FinMapToList K A (gmap K A) := λ m, Instance gmap_to_list `{Countable K} {A} : FinMapToList K A (gmap K A) := λ m,
let (m,_) := m in omap (λ ix : positive * A, let (m,_) := m in omap (λ ix : positive * A,
let (i,x) := ix in (,x) <$> decode i) (map_to_list m). let (i,x) := ix in (., x) <$> decode i) (map_to_list m).
(** * Instantiation of the finite map interface *) (** * Instantiation of the finite map interface *)
Instance gmap_finmap `{Countable K} : FinMap K (gmap K). Instance gmap_finmap `{Countable K} : FinMap K (gmap K).
...@@ -139,12 +139,12 @@ Section curry_uncurry. ...@@ -139,12 +139,12 @@ Section curry_uncurry.
(* FIXME: the type annotations `option (gmap K2 A)` are silly. Maybe these are (* FIXME: the type annotations `option (gmap K2 A)` are silly. Maybe these are
a consequence of Coq bug #5735 *) a consequence of Coq bug #5735 *)
Lemma lookup_gmap_curry (m : gmap K1 (gmap K2 A)) i j : Lemma lookup_gmap_curry (m : gmap K1 (gmap K2 A)) i j :
gmap_curry m !! (i,j) = (m !! i : option (gmap K2 A)) = (!! j). gmap_curry m !! (i,j) = (m !! i : option (gmap K2 A)) = (.!! j).
Proof. Proof.
apply (map_fold_ind (λ mr m, mr !! (i,j) = m !! i = (!! j))). apply (map_fold_ind (λ mr m, mr !! (i,j) = m !! i = (.!! j))).
{ by rewrite !lookup_empty. } { by rewrite !lookup_empty. }
clear m; intros i' m2 m m12 Hi' IH. clear m; intros i' m2 m m12 Hi' IH.
apply (map_fold_ind (λ m2r m2, m2r !! (i,j) = <[i':=m2]> m !! i = (!! j))). apply (map_fold_ind (λ m2r m2, m2r !! (i,j) = <[i':=m2]> m !! i = (.!! j))).
{ rewrite IH. destruct (decide (i' = i)) as [->|]. { rewrite IH. destruct (decide (i' = i)) as [->|].
- rewrite lookup_insert, Hi'; simpl; by rewrite lookup_empty. - rewrite lookup_insert, Hi'; simpl; by rewrite lookup_empty.
- by rewrite lookup_insert_ne by done. } - by rewrite lookup_insert_ne by done. }
...@@ -156,9 +156,9 @@ Section curry_uncurry. ...@@ -156,9 +156,9 @@ Section curry_uncurry.
Qed. Qed.
Lemma lookup_gmap_uncurry (m : gmap (K1 * K2) A) i j : Lemma lookup_gmap_uncurry (m : gmap (K1 * K2) A) i j :
(gmap_uncurry m !! i : option (gmap K2 A)) = (!! j) = m !! (i, j). (gmap_uncurry m !! i : option (gmap K2 A)) = (.!! j) = m !! (i, j).
Proof. Proof.
apply (map_fold_ind (λ mr m, mr !! i = (!! j) = m !! (i, j))). apply (map_fold_ind (λ mr m, mr !! i = (.!! j) = m !! (i, j))).
{ by rewrite !lookup_empty. } { by rewrite !lookup_empty. }
clear m; intros [i' j'] x m12 mr Hij' IH. clear m; intros [i' j'] x m12 mr Hij' IH.
destruct (decide (i = i')) as [->|]. destruct (decide (i = i')) as [->|].
...@@ -202,7 +202,7 @@ Section curry_uncurry. ...@@ -202,7 +202,7 @@ Section curry_uncurry.
intros Hne. apply map_eq; intros i. destruct (m !! i) as [m2|] eqn:Hm. intros Hne. apply map_eq; intros i. destruct (m !! i) as [m2|] eqn:Hm.
- destruct (gmap_uncurry (gmap_curry m) !! i) as [m2'|] eqn:Hcurry. - destruct (gmap_uncurry (gmap_curry m) !! i) as [m2'|] eqn:Hcurry.
+ f_equal. apply map_eq. intros j. + f_equal. apply map_eq. intros j.
trans ((gmap_uncurry (gmap_curry m) !! i : option (gmap _ _)) = (!! j)). trans ((gmap_uncurry (gmap_curry m) !! i : option (gmap _ _)) = (.!! j)).
{ by rewrite Hcurry. } { by rewrite Hcurry. }
by rewrite lookup_gmap_uncurry, lookup_gmap_curry, Hm. by rewrite lookup_gmap_uncurry, lookup_gmap_curry, Hm.
+ rewrite lookup_gmap_uncurry_None in Hcurry. + rewrite lookup_gmap_uncurry_None in Hcurry.
......
...@@ -218,12 +218,12 @@ Qed. ...@@ -218,12 +218,12 @@ Qed.
Global Instance gmultiset_disj_union_right_id : RightId (=@{gmultiset A}) (). Global Instance gmultiset_disj_union_right_id : RightId (=@{gmultiset A}) ().
Proof. intros X. by rewrite (comm_L ()), (left_id_L _ _). Qed. Proof. intros X. by rewrite (comm_L ()), (left_id_L _ _). Qed.
Global Instance gmultiset_disj_union_inj_1 X : Inj (=) (=) (X ). Global Instance gmultiset_disj_union_inj_1 X : Inj (=) (=) (X .).
Proof. Proof.
intros Y1 Y2. rewrite !gmultiset_eq. intros HX x; generalize (HX x). intros Y1 Y2. rewrite !gmultiset_eq. intros HX x; generalize (HX x).
rewrite !multiplicity_disj_union. lia. rewrite !multiplicity_disj_union. lia.
Qed. Qed.
Global Instance gmultiset_disj_union_inj_2 X : Inj (=) (=) ( X). Global Instance gmultiset_disj_union_inj_2 X : Inj (=) (=) (. X).
Proof. intros Y1 Y2. rewrite <-!(comm_L _ X). apply (inj _). Qed. Proof. intros Y1 Y2. rewrite <-!(comm_L _ X). apply (inj _). Qed.
Lemma gmultiset_disj_union_intersection_l X Y Z : X (Y Z) = (X Y) (X Z). Lemma gmultiset_disj_union_intersection_l X Y Z : X (Y Z) = (X Y) (X Z).
......
...@@ -129,7 +129,7 @@ Definition remove_dups_fast (l : list A) : list A := ...@@ -129,7 +129,7 @@ Definition remove_dups_fast (l : list A) : list A :=
| [x] => [x] | [x] => [x]
| _ => | _ =>
let n : Z := length l in let n : Z := length l in
elements (foldr (λ x, ({[ x ]} )) l : elements (foldr (λ x, ({[ x ]} .)) l :
hashset (λ x, hash x `mod` (2 * n))%Z) hashset (λ x, hash x `mod` (2 * n))%Z)
end. end.
Lemma elem_of_remove_dups_fast l x : x remove_dups_fast l x l. Lemma elem_of_remove_dups_fast l x : x remove_dups_fast l x l.
......
...@@ -35,7 +35,7 @@ Section search_infinite. ...@@ -35,7 +35,7 @@ Section search_infinite.
Lemma search_infinite_R_wf xs : wf (R xs). Lemma search_infinite_R_wf xs : wf (R xs).
Proof. Proof.
revert xs. assert (help : xs n n', revert xs. assert (help : xs n n',
Acc (R (filter ( f n') xs)) n n' < n Acc (R xs) n). Acc (R (filter (. f n') xs)) n n' < n Acc (R xs) n).
{ induction 1 as [n _ IH]. constructor; intros n2 [??]. apply IH; [|lia]. { induction 1 as [n _ IH]. constructor; intros n2 [??]. apply IH; [|lia].
split; [done|]. apply elem_of_list_filter; naive_solver lia. } split; [done|]. apply elem_of_list_filter; naive_solver lia. }
intros xs. induction (well_founded_ltof _ length xs) as [xs _ IH]. intros xs. induction (well_founded_ltof _ length xs) as [xs _ IH].
...@@ -127,9 +127,9 @@ Instance sum_infinite_r {A} `{Infinite B} : Infinite (A + B) := ...@@ -127,9 +127,9 @@ Instance sum_infinite_r {A} `{Infinite B} : Infinite (A + B) :=
inj_infinite inr (maybe inr) (λ _, eq_refl). inj_infinite inr (maybe inr) (λ _, eq_refl).
Instance prod_infinite_l `{Infinite A, Inhabited B} : Infinite (A * B) := Instance prod_infinite_l `{Infinite A, Inhabited B} : Infinite (A * B) :=
inj_infinite (,inhabitant) (Some fst) (λ _, eq_refl). inj_infinite (., inhabitant) (Some fst) (λ _, eq_refl).
Instance prod_infinite_r `{Inhabited A, Infinite B} : Infinite (A * B) := Instance prod_infinite_r `{Inhabited A, Infinite B} : Infinite (A * B) :=
inj_infinite (inhabitant,) (Some snd) (λ _, eq_refl). inj_infinite (inhabitant ,.) (Some snd) (λ _, eq_refl).
(** Instance for lists *) (** Instance for lists *)
Program Instance list_infinite `{Inhabited A} : Infinite (list A) := {| Program Instance list_infinite `{Inhabited A} : Infinite (list A) := {|
......
...@@ -33,20 +33,20 @@ Arguments Forall_cons {_} _ _ _ _ _ : assert. ...@@ -33,20 +33,20 @@ Arguments Forall_cons {_} _ _ _ _ _ : assert.
Remove Hints Permutation_cons : typeclass_instances. Remove Hints Permutation_cons : typeclass_instances.
Notation "(::)" := cons (only parsing) : list_scope. Notation "(::)" := cons (only parsing) : list_scope.
Notation "( x ::)" := (cons x) (only parsing) : list_scope. Notation "( x ::.)" := (cons x) (only parsing) : list_scope.
Notation "(:: l )" := (λ x, cons x l) (only parsing) : list_scope. Notation "(.:: l )" := (λ x, cons x l) (only parsing) : list_scope.
Notation "(++)" := app (only parsing) : list_scope. Notation "(++)" := app (only parsing) : list_scope.
Notation "( l ++)" := (app l) (only parsing) : list_scope. Notation "( l ++.)" := (app l) (only parsing) : list_scope.
Notation "(++ k )" := (λ l, app l k) (only parsing) : list_scope. Notation "(.++ k )" := (λ l, app l k) (only parsing) : list_scope.
Infix "≡ₚ" := Permutation (at level 70, no associativity) : stdpp_scope. Infix "≡ₚ" := Permutation (at level 70, no associativity) : stdpp_scope.
Notation "(≡ₚ)" := Permutation (only parsing) : stdpp_scope. Notation "(≡ₚ)" := Permutation (only parsing) : stdpp_scope.
Notation "( x ≡ₚ)" := (Permutation x) (only parsing) : stdpp_scope. Notation "( x ≡ₚ.)" := (Permutation x) (only parsing) : stdpp_scope.
Notation "(≡ₚ x )" := (λ y, y ≡ₚ x) (only parsing) : stdpp_scope. Notation "(.≡ₚ x )" := (λ y, y ≡ₚ x) (only parsing) : stdpp_scope.
Notation "(≢ₚ)" := (λ x y, ¬x ≡ₚ y) (only parsing) : stdpp_scope. Notation "(≢ₚ)" := (λ x y, ¬x ≡ₚ y) (only parsing) : stdpp_scope.
Notation "x ≢ₚ y":= (¬x ≡ₚ y) (at level 70, no associativity) : stdpp_scope. Notation "x ≢ₚ y":= (¬x ≡ₚ y) (at level 70, no associativity) : stdpp_scope.
Notation "( x ≢ₚ)" := (λ y, x ≢ₚ y) (only parsing) : stdpp_scope. Notation "( x ≢ₚ.)" := (λ y, x ≢ₚ y) (only parsing) : stdpp_scope.
Notation "(≢ₚ x )" := (λ y, y ≢ₚ x) (only parsing) : stdpp_scope. Notation "(.≢ₚ x )" := (λ y, y ≢ₚ x) (only parsing) : stdpp_scope.
Infix "≡ₚ@{ A }" := Infix "≡ₚ@{ A }" :=
(@Permutation A) (at level 70, no associativity, only parsing) : stdpp_scope. (@Permutation A) (at level 70, no associativity, only parsing) : stdpp_scope.
...@@ -237,7 +237,7 @@ Fixpoint mask {A} (f : A → A) (βs : list bool) (l : list A) : list A := ...@@ -237,7 +237,7 @@ Fixpoint mask {A} (f : A → A) (βs : list bool) (l : list A) : list A :=
(** The function [permutations l] yields all permutations of [l]. *) (** The function [permutations l] yields all permutations of [l]. *)
Fixpoint interleave {A} (x : A) (l : list A) : list (list A) := Fixpoint interleave {A} (x : A) (l : list A) : list (list A) :=
match l with match l with
| [] => [[x]]| y :: l => (x :: y :: l) :: ((y ::) <$> interleave x l) | [] => [[x]]| y :: l => (x :: y :: l) :: ((y ::.) <$> interleave x l)
end. end.
Fixpoint permutations {A} (l : list A) : list (list A) := Fixpoint permutations {A} (l : list A) : list (list A) :=
match l with [] => [[]] | x :: l => permutations l = interleave x end. match l with [] => [[]] | x :: l => permutations l = interleave x end.
...@@ -261,7 +261,7 @@ Section prefix_suffix_ops. ...@@ -261,7 +261,7 @@ Section prefix_suffix_ops.
| l1, [] => (l1, [], []) | l1, [] => (l1, [], [])
| x1 :: l1, x2 :: l2 => | x1 :: l1, x2 :: l2 =>
if decide_rel (=) x1 x2 if decide_rel (=) x1 x2
then prod_map id (x1 ::) (go l1 l2) else (x1 :: l1, x2 :: l2, []) then prod_map id (x1 ::.) (go l1 l2) else (x1 :: l1, x2 :: l2, [])
end. end.
Definition max_suffix (l1 l2 : list A) : list A * list A * list A := Definition max_suffix (l1 l2 : list A) : list A * list A * list A :=
match max_prefix (reverse l1) (reverse l2) with match max_prefix (reverse l1) (reverse l2) with
...@@ -296,7 +296,7 @@ Hint Extern 0 (_ ⊆+ _) => reflexivity : core. ...@@ -296,7 +296,7 @@ Hint Extern 0 (_ ⊆+ _) => reflexivity : core.
Fixpoint list_remove `{EqDecision A} (x : A) (l : list A) : option (list A) := Fixpoint list_remove `{EqDecision A} (x : A) (l : list A) : option (list A) :=
match l with match l with
| [] => None | [] => None
| y :: l => if decide (x = y) then Some l else (y ::) <$> list_remove x l | y :: l => if decide (x = y) then Some l else (y ::.) <$> list_remove x l
end. end.
(** Removes all elements in the list [k] from the list [l]. The function returns (** Removes all elements in the list [k] from the list [l]. The function returns
...@@ -352,7 +352,7 @@ Section list_set. ...@@ -352,7 +352,7 @@ Section list_set.
match l with match l with
| [] => [] | [] => []
| x :: l => foldr (λ y, | x :: l => foldr (λ y,
match f x y with None => id | Some z => (z ::) end) (go l k) k match f x y with None => id | Some z => (z ::.) end) (go l k) k
end. end.
End list_set. End list_set.
...@@ -442,9 +442,9 @@ Implicit Types l k : list A. ...@@ -442,9 +442,9 @@ Implicit Types l k : list A.
Global Instance: Inj2 (=) (=) (=) (@cons A). Global Instance: Inj2 (=) (=) (=) (@cons A).
Proof. by injection 1. Qed. Proof. by injection 1. Qed.
Global Instance: k, Inj (=) (=) (k ++). Global Instance: k, Inj (=) (=) (k ++.).
Proof. intros ???. apply app_inv_head. Qed. Proof. intros ???. apply app_inv_head. Qed.
Global Instance: k, Inj (=) (=) (++ k). Global Instance: k, Inj (=) (=) (.++ k).
Proof. intros ???. apply app_inv_tail. Qed. Proof. intros ???. apply app_inv_tail. Qed.
Global Instance: Assoc (=) (@app A). Global Instance: Assoc (=) (@app A).
Proof. intros ???. apply app_assoc. Qed. Proof. intros ???. apply app_assoc. Qed.
...@@ -728,7 +728,7 @@ Lemma not_elem_of_app l1 l2 x : x ∉ l1 ++ l2 ↔ x ∉ l1 ∧ x ∉ l2. ...@@ -728,7 +728,7 @@ Lemma not_elem_of_app l1 l2 x : x ∉ l1 ++ l2 ↔ x ∉ l1 ∧ x ∉ l2.
Proof. rewrite elem_of_app. tauto. Qed. Proof. rewrite elem_of_app. tauto. Qed.
Lemma elem_of_list_singleton x y : x [y] x = y. Lemma elem_of_list_singleton x y : x [y] x = y.
Proof. rewrite elem_of_cons, elem_of_nil. tauto. Qed. Proof. rewrite elem_of_cons, elem_of_nil. tauto. Qed.
Global Instance elem_of_list_permutation_proper x : Proper ((≡ₚ) ==> iff) (x ). Global Instance elem_of_list_permutation_proper x : Proper ((≡ₚ) ==> iff) (x .).
Proof. induction 1; rewrite ?elem_of_nil, ?elem_of_cons; intuition. Qed. Proof. induction 1; rewrite ?elem_of_nil, ?elem_of_cons; intuition. Qed.
Lemma elem_of_list_split l x : x l l1 l2, l = l1 ++ x :: l2. Lemma elem_of_list_split l x : x l l1 l2, l = l1 ++ x :: l2.
Proof. Proof.
...@@ -1370,7 +1370,7 @@ Proof. ...@@ -1370,7 +1370,7 @@ Proof.
rewrite (Nat.mul_comm _ n) in Hlookup. rewrite (Nat.mul_comm _ n) in Hlookup.
unfold sublist_lookup in *; simplify_option_eq; unfold sublist_lookup in *; simplify_option_eq;
[|by rewrite !lookup_ge_None_2 by auto]. [|by rewrite !lookup_ge_None_2 by auto].
apply (f_equal (!! i `mod` n)) in Hlookup. apply (f_equal (.!! i `mod` n)) in Hlookup.
by rewrite !lookup_take, !lookup_drop, <-!Nat.div_mod in Hlookup by rewrite !lookup_take, !lookup_drop, <-!Nat.div_mod in Hlookup
by (auto using Nat.mod_upper_bound with lia). by (auto using Nat.mod_upper_bound with lia).
Qed. Qed.
...@@ -1611,15 +1611,15 @@ Proof. ...@@ -1611,15 +1611,15 @@ Proof.
- by rewrite (right_id_L [] (++)). - by rewrite (right_id_L [] (++)).
- rewrite Permutation_middle, IH. simpl. by rewrite Permutation_middle. - rewrite Permutation_middle, IH. simpl. by rewrite Permutation_middle.
Qed. Qed.
Global Instance: x : A, Inj (≡ₚ) (≡ₚ) (x ::). Global Instance: x : A, Inj (≡ₚ) (≡ₚ) (x ::.).
Proof. red. eauto using Permutation_cons_inv. Qed. Proof. red. eauto using Permutation_cons_inv. Qed.
Global Instance: k : list A, Inj (≡ₚ) (≡ₚ) (k ++). Global Instance: k : list A, Inj (≡ₚ) (≡ₚ) (k ++.).
Proof. Proof.
red. induction k as [|x k IH]; intros l1 l2; simpl; auto. red. induction k as [|x k IH]; intros l1 l2; simpl; auto.
intros. by apply IH, (inj (x ::)). intros. by apply IH, (inj (x ::.)).
Qed. Qed.
Global Instance: k : list A, Inj (≡ₚ) (≡ₚ) (++ k). Global Instance: k : list A, Inj (≡ₚ) (≡ₚ) (.++ k).
Proof. intros k l1 l2. rewrite !(comm (++) _ k). by apply (inj (k ++)). Qed. Proof. intros k l1 l2. rewrite !(comm (++) _ k). by apply (inj (k ++.)). Qed.
Lemma replicate_Permutation n x l : replicate n x ≡ₚ l replicate n x = l. Lemma replicate_Permutation n x l : replicate n x ≡ₚ l replicate n x = l.
Proof. Proof.
intros Hl. apply replicate_as_elem_of. split. intros Hl. apply replicate_as_elem_of. split.
...@@ -1646,7 +1646,7 @@ Proof. ...@@ -1646,7 +1646,7 @@ Proof.
{ apply elem_of_list_lookup. rewrite Hk, elem_of_cons; auto. } { apply elem_of_list_lookup. rewrite Hk, elem_of_cons; auto. }
exists (take i k), (drop (S i) k). split. exists (take i k), (drop (S i) k). split.
- by rewrite take_drop_middle. - by rewrite take_drop_middle.
- rewrite <-delete_take_drop. apply (inj (x ::)). - rewrite <-delete_take_drop. apply (inj (x ::.)).
by rewrite <-Hk, <-(delete_Permutation k) by done. by rewrite <-Hk, <-(delete_Permutation k) by done.
Qed. Qed.
...@@ -2488,7 +2488,7 @@ Section Forall_Exists. ...@@ -2488,7 +2488,7 @@ Section Forall_Exists.
Qed. Qed.
Lemma Forall_replicate n x : P x Forall P (replicate n x). Lemma Forall_replicate n x : P x Forall P (replicate n x).
Proof. induction n; simpl; constructor; auto. Qed. Proof. induction n; simpl; constructor; auto. Qed.
Lemma Forall_replicate_eq n (x : A) : Forall (x =) (replicate n x). Lemma Forall_replicate_eq n (x : A) : Forall (x =.) (replicate n x).
Proof using -(P). induction n; simpl; constructor; auto. Qed. Proof using -(P). induction n; simpl; constructor; auto. Qed.
Lemma Forall_take n l : Forall P l Forall P (take n l). Lemma Forall_take n l : Forall P l Forall P (take n l).
Proof. intros Hl. revert n. induction Hl; intros [|?]; simpl; auto. Qed. Proof. intros Hl. revert n. induction Hl; intros [|?]; simpl; auto. Qed.
...@@ -2606,10 +2606,10 @@ Lemma existb_True (f : A → bool) xs : existsb f xs ↔ Exists f xs. ...@@ -2606,10 +2606,10 @@ Lemma existb_True (f : A → bool) xs : existsb f xs ↔ Exists f xs.
Proof. split. induction xs; naive_solver. induction 1; naive_solver. Qed. Proof. split. induction xs; naive_solver. induction 1; naive_solver. Qed.
Lemma replicate_as_Forall (x : A) n l : Lemma replicate_as_Forall (x : A) n l :
replicate n x = l length l = n Forall (x =) l. replicate n x = l length l = n Forall (x =.) l.
Proof. rewrite replicate_as_elem_of, Forall_forall. naive_solver. Qed. Proof. rewrite replicate_as_elem_of, Forall_forall. naive_solver. Qed.
Lemma replicate_as_Forall_2 (x : A) n l : Lemma replicate_as_Forall_2 (x : A) n l :
length l = n Forall (x =) l replicate n x = l. length l = n Forall (x =.) l replicate n x = l.
Proof. by rewrite replicate_as_Forall. Qed. Proof. by rewrite replicate_as_Forall. Qed.
End more_general_properties. End more_general_properties.
...@@ -3392,14 +3392,14 @@ Section ret_join. ...@@ -3392,14 +3392,14 @@ Section ret_join.
Lemma elem_of_list_join (x : A) (ls : list (list A)) : Lemma elem_of_list_join (x : A) (ls : list (list A)) :
x mjoin ls l : list A, x l l ls. x mjoin ls l : list A, x l l ls.
Proof. by rewrite list_join_bind, elem_of_list_bind. Qed. Proof. by rewrite list_join_bind, elem_of_list_bind. Qed.
Lemma join_nil (ls : list (list A)) : mjoin ls = [] Forall (= []) ls. Lemma join_nil (ls : list (list A)) : mjoin ls = [] Forall (.= []) ls.
Proof. Proof.
split; [|by induction 1 as [|[|??] ?]]. split; [|by induction 1 as [|[|??] ?]].
by induction ls as [|[|??] ?]; constructor; auto. by induction ls as [|[|??] ?]; constructor; auto.
Qed. Qed.
Lemma join_nil_1 (ls : list (list A)) : mjoin ls = [] Forall (= []) ls. Lemma join_nil_1 (ls : list (list A)) : mjoin ls = [] Forall (.= []) ls.
Proof. by rewrite join_nil. Qed. Proof. by rewrite join_nil. Qed.
Lemma join_nil_2 (ls : list (list A)) : Forall (= []) ls mjoin ls = []. Lemma join_nil_2 (ls : list (list A)) : Forall (.= []) ls mjoin ls = [].
Proof. by rewrite join_nil. Qed. Proof. by rewrite join_nil. Qed.
Lemma Forall_join (P : A Prop) (ls: list (list A)) : Lemma Forall_join (P : A Prop) (ls: list (list A)) :
Forall (Forall P) ls Forall P (mjoin ls). Forall (Forall P) ls Forall P (mjoin ls).
...@@ -4008,7 +4008,7 @@ Section positives_flatten_unflatten. ...@@ -4008,7 +4008,7 @@ Section positives_flatten_unflatten.
intros p1 p2 [|y ys] ?; simplify_eq/=; auto. intros p1 p2 [|y ys] ?; simplify_eq/=; auto.
rewrite !positives_flatten_cons, !(assoc _); intros Hl. rewrite !positives_flatten_cons, !(assoc _); intros Hl.
assert (xs = ys) as <- by eauto; clear IH H; f_equal. assert (xs = ys) as <- by eauto; clear IH H; f_equal.
apply (inj (++ positives_flatten xs)) in Hl. apply (inj (.++ positives_flatten xs)) in Hl.
rewrite 2!Preverse_Pdup in Hl. rewrite 2!Preverse_Pdup in Hl.
apply (Pdup_suffix_eq _ _ p1 p2) in Hl. apply (Pdup_suffix_eq _ _ p1 p2) in Hl.
by apply (inj Preverse). by apply (inj Preverse).
...@@ -4018,7 +4018,7 @@ End positives_flatten_unflatten. ...@@ -4018,7 +4018,7 @@ End positives_flatten_unflatten.
(** * Relection over lists *) (** * Relection over lists *)
(** We define a simple data structure [rlist] to capture a syntactic (** We define a simple data structure [rlist] to capture a syntactic
representation of lists consisting of constants, applications and the nil list. representation of lists consisting of constants, applications and the nil list.
Note that we represent [(x ::)] as [rapp (rnode [x])]. For now, we abstract Note that we represent [(x ::.)] as [rapp (rnode [x])]. For now, we abstract
over the type of constants, but later we use [nat]s and a list representing over the type of constants, but later we use [nat]s and a list representing
a corresponding environment. *) a corresponding environment. *)
Inductive rlist (A : Type) := Inductive rlist (A : Type) :=
...@@ -4071,7 +4071,7 @@ End quote. ...@@ -4071,7 +4071,7 @@ End quote.
Section eval. Section eval.
Context {A} (E : env A). Context {A} (E : env A).
Lemma eval_alt t : eval E t = to_list t = default [] (E !!). Lemma eval_alt t : eval E t = to_list t = default [] (E !!.).
Proof. Proof.
induction t; csimpl. induction t; csimpl.
- done. - done.
......
...@@ -170,8 +170,8 @@ Fixpoint Papp (p1 p2 : positive) : positive := ...@@ -170,8 +170,8 @@ Fixpoint Papp (p1 p2 : positive) : positive :=
end. end.
Infix "++" := Papp : positive_scope. Infix "++" := Papp : positive_scope.
Notation "(++)" := Papp (only parsing) : positive_scope. Notation "(++)" := Papp (only parsing) : positive_scope.
Notation "( p ++)" := (Papp p) (only parsing) : positive_scope. Notation "( p ++.)" := (Papp p) (only parsing) : positive_scope.
Notation "(++ q )" := (λ p, Papp p q) (only parsing) : positive_scope. Notation "(.++ q )" := (λ p, Papp p q) (only parsing) : positive_scope.
Fixpoint Preverse_go (p1 p2 : positive) : positive := Fixpoint Preverse_go (p1 p2 : positive) : positive :=
match p2 with match p2 with
...@@ -187,7 +187,7 @@ Global Instance Papp_1_r : RightId (=) 1 (++). ...@@ -187,7 +187,7 @@ Global Instance Papp_1_r : RightId (=) 1 (++).
Proof. done. Qed. Proof. done. Qed.
Global Instance Papp_assoc : Assoc (=) (++). Global Instance Papp_assoc : Assoc (=) (++).
Proof. intros ?? p. by induction p; intros; f_equal/=. Qed. Proof. intros ?? p. by induction p; intros; f_equal/=. Qed.
Global Instance Papp_inj p : Inj (=) (=) (++ p). Global Instance Papp_inj p : Inj (=) (=) (.++ p).
Proof. intros ???. induction p; simplify_eq; auto. Qed. Proof. intros ???. induction p; simplify_eq; auto. Qed.
Lemma Preverse_go_app p1 p2 p3 : Lemma Preverse_go_app p1 p2 p3 :
......
...@@ -224,14 +224,14 @@ Proof. ...@@ -224,14 +224,14 @@ Proof.
apply IHl. apply IHl.
{ intros i x. rewrite Pelem_of_to_list. intros [(?&Hi&?)|Hi]. { intros i x. rewrite Pelem_of_to_list. intros [(?&Hi&?)|Hi].
+ rewrite Preverse_xO, Preverse_xI, !(assoc_L _) in Hi. + rewrite Preverse_xO,