Commit 45690e49 authored by Robbert Krebbers's avatar Robbert Krebbers

Disambiguate Haskell-style notations for partially operators.

For example, change `(!! i)` into `(.!! x)` so that `!!` can also be used as
a prefix, as done in VST for example.

This closes issue #42.

I have used the `sed` script below. This script took care of nearly all uses
apart from a few occurrences where a space was missing, e.g. `(,foo)`. In
this case, `coqc` will just fail, allowing one to patch up things manually.

The script is slightly too eager on Iris developments, where it also replaces
`($ ...)` introduction patterns. When porting Iris developments you thus may
want to remove the line for `$`.

```
sed '
s/(= /(.= /g;
s/ =)/ =.)/g;
s/(≠ /(.≠ /g;
s/ ≠)/ ≠.)/g;
s/(≡ /(.≡ /g;
s/ ≡)/ ≡.)/g;
s/(≢ /(.≢ /g;
s/ ≢)/ ≢.)/g;
s/(∧ /(.∧ /g;
s/ ∧)/ ∧.)/g;
s/(∨ /(.∨ /g;
s/ ∨)/ ∨.)/g;
s/( /(. /g;
s/ )/ .)/g;
s/(→ /(.→ /g;
s/ →)/ →.)/g;
s/($ /(.$ /g;
s/(∘ /(.∘ /g;
s/ ∘)/ ∘.)/g;
s/(, /(., /g;
s/ ,)/ ,.)/g;
s/(∘ /(.∘ /g;
s/ ∘)/ ∘.)/g;
s/(∪ /(.∪ /g;
s/ ∪)/ ∪.)/g;
s/(⊎ /(.⊎ /g;
s/ ⊎)/ ⊎.)/g;
s/(∩ /(.∩ /g;
s/ ∩)/ ∩.)/g;
s/(∖ /(.∖ /g;
s/ ∖)/ ∖.)/g;
s/(⊆ /(.⊆ /g;
s/ ⊆)/ ⊆.)/g;
s/(⊈ /(.⊈ /g;
s/ ⊈)/ ⊈.)/g;
s/(⊂ /(.⊂ /g;
s/ ⊂)/ ⊂.)/g;
s/(⊄ /(.⊄ /g;
s/ ⊄)/ ⊄.)/g;
s/(∈ /(.∈ /g;
s/ ∈)/ ∈.)/g;
s/(∉ /(.∉ /g;
s/ ∉)/ ∉.)/g;
s/(≫= /(.≫= /g;
s/ ≫=)/ ≫=.)/g;
s/(!! /(.!! /g;
s/ !!)/ !!.)/g;
s/(⊑ /(.⊑ /g;
s/ ⊑)/ ⊑.)/g;
s/(⊓ /(.⊓ /g;
s/ ⊓)/ ⊓.)/g;
s/(⊔ /(.⊔ /g;
s/ ⊔)/ ⊔.)/g;
s/(:: /(.:: /g;
s/ ::)/ ::.)/g;
s/(++ /(.++ /g;
s/ ++)/ ++.)/g;
s/(≡ₚ /(.≡ₚ /g;
s/ ≡ₚ)/ ≡ₚ.)/g;
s/(≢ₚ /(.≢ₚ /g;
s/ ≢ₚ)/ ≢ₚ.)/g;
s/(::: /(.::: /g;
s/ :::)/ :::.)/g;
s/(+++ /(.+++ /g;
s/ +++)/ +++.)/g;
' -i $(find -name "*.v")
```
parent b53cbe77
This diff is collapsed.
......@@ -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. *)
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 :=
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
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]}.
Proof. done. Qed.
Lemma insert_non_empty {A} (m : M A) i x : <[i:=x]>m .
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.
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) :
Proof. by rewrite lookup_singleton_None. Qed.
Lemma map_non_empty_singleton {A} i (x : A) : {[i := x]} ( : M A).
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.
Qed.
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 :
Proof. rewrite lookup_union. destruct (m1 !! i), (m2 !! i); naive_solver. Qed.
Lemma map_positive_l {A} (m1 m2 : M A) : m1 m2 = m1 = .
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.
Qed.
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).
Program Definition finite_countable `{Finite A} : Countable A := {|
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)
|}.
Arguments Pos.of_nat : simpl never.
Next Obligation.
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.
destruct (list_find_Some (x =) xs i y); naive_solver.
destruct (list_find_Some (x =.) xs i y); naive_solver.
Qed.
Hint Immediate finite_countable : typeclass_instances.
......@@ -38,7 +38,7 @@ Proof.
destruct finA as [xs Hxs HA]; unfold encode_nat, encode, card; simpl.
rewrite Nat2Pos.id by done; 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.
Qed.
Lemma encode_decode A `{finA: Finite A} i :
......@@ -48,8 +48,8 @@ Proof.
unfold encode_nat, decode_nat, encode, decode, card; simpl.
intros Hi. apply lookup_lt_is_Some in Hi. destruct Hi as [x Hx].
exists x. rewrite !Nat2Pos.id by done; simpl.
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_elem_of (x =.) xs x) as [[j y] Hj]; auto.
destruct (list_find_Some (x =.) xs j y) as [? ->]; auto.
rewrite Hj; csimpl; eauto using NoDup_lookup.
Qed.
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.
Proof. unfold card. simpl. by rewrite app_length, !fmap_length. Qed.
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.
intros ??????. induction (NoDup_enum A) as [|x xs Hx Hxs IH]; simpl.
{ constructor. }
......@@ -312,7 +312,7 @@ Definition list_enum {A} (l : list A) : ∀ n, list { l : list A | length l = n
fix go n :=
match n with
| 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.
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,
(bool_decide_unpack _ Hm1) (bool_decide_unpack _ Hm2))).
Instance gmap_to_list `{Countable K} {A} : FinMapToList K A (gmap K A) := λ m,
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 *)
Instance gmap_finmap `{Countable K} : FinMap K (gmap K).
......@@ -139,12 +139,12 @@ Section curry_uncurry.
(* FIXME: the type annotations `option (gmap K2 A)` are silly. Maybe these are
a consequence of Coq bug #5735 *)
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.
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. }
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 lookup_insert, Hi'; simpl; by rewrite lookup_empty.
- by rewrite lookup_insert_ne by done. }
......@@ -156,9 +156,9 @@ Section curry_uncurry.
Qed.
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.
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. }
clear m; intros [i' j'] x m12 mr Hij' IH.
destruct (decide (i = i')) as [->|].
......@@ -202,7 +202,7 @@ Section curry_uncurry.
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.
+ 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 lookup_gmap_uncurry, lookup_gmap_curry, Hm.
+ rewrite lookup_gmap_uncurry_None in Hcurry.
......
......@@ -218,12 +218,12 @@ Qed.
Global Instance gmultiset_disj_union_right_id : RightId (=@{gmultiset A}) ().
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.
intros Y1 Y2. rewrite !gmultiset_eq. intros HX x; generalize (HX x).
rewrite !multiplicity_disj_union. lia.
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.
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 :=
| [x] => [x]
| _ =>
let n : Z := length l in
elements (foldr (λ x, ({[ x ]} )) l :
elements (foldr (λ x, ({[ x ]} .)) l :
hashset (λ x, hash x `mod` (2 * n))%Z)
end.
Lemma elem_of_remove_dups_fast l x : x remove_dups_fast l x l.
......
......@@ -35,7 +35,7 @@ Section search_infinite.
Lemma search_infinite_R_wf xs : wf (R xs).
Proof.
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].
split; [done|]. apply elem_of_list_filter; naive_solver lia. }
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) :=
inj_infinite inr (maybe inr) (λ _, eq_refl).
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) :=
inj_infinite (inhabitant,) (Some snd) (λ _, eq_refl).
inj_infinite (inhabitant ,.) (Some snd) (λ _, eq_refl).
(** Instance for lists *)
Program Instance list_infinite `{Inhabited A} : Infinite (list A) := {|
......
......@@ -33,20 +33,20 @@ Arguments Forall_cons {_} _ _ _ _ _ : assert.
Remove Hints Permutation_cons : typeclass_instances.
Notation "(::)" := cons (only parsing) : list_scope.
Notation "( x ::)" := (cons x) (only parsing) : list_scope.
Notation "(:: l )" := (λ x, cons x l) (only parsing) : list_scope.
Notation "( x ::.)" := (cons x) (only parsing) : list_scope.
Notation "(.:: l )" := (λ x, cons x l) (only parsing) : list_scope.
Notation "(++)" := app (only parsing) : list_scope.
Notation "( l ++)" := (app l) (only parsing) : list_scope.
Notation "(++ k )" := (λ l, app l k) (only parsing) : list_scope.
Notation "( l ++.)" := (app l) (only parsing) : list_scope.
Notation "(.++ k )" := (λ l, app l k) (only parsing) : list_scope.
Infix "≡ₚ" := Permutation (at level 70, no associativity) : stdpp_scope.
Notation "(≡ₚ)" := Permutation (only parsing) : stdpp_scope.
Notation "( x ≡ₚ)" := (Permutation x) (only parsing) : stdpp_scope.
Notation "(≡ₚ x )" := (λ y, y ≡ₚ 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, ¬x ≡ₚ y) (only parsing) : 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, y ≢ₚ x) (only parsing) : stdpp_scope.
Notation "( x ≢ₚ.)" := (λ y, x ≢ₚ y) (only parsing) : stdpp_scope.
Notation "(.≢ₚ x )" := (λ y, y ≢ₚ x) (only parsing) : stdpp_scope.
Infix "≡ₚ@{ A }" :=
(@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 :=
(** The function [permutations l] yields all permutations of [l]. *)
Fixpoint interleave {A} (x : A) (l : list A) : list (list A) :=
match l with
| [] => [[x]]| y :: l => (x :: y :: l) :: ((y ::) <$> interleave x l)
| [] => [[x]]| y :: l => (x :: y :: l) :: ((y ::.) <$> interleave x l)
end.
Fixpoint permutations {A} (l : list A) : list (list A) :=
match l with [] => [[]] | x :: l => permutations l = interleave x end.
......@@ -261,7 +261,7 @@ Section prefix_suffix_ops.
| l1, [] => (l1, [], [])
| x1 :: l1, x2 :: l2 =>
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.
Definition max_suffix (l1 l2 : list A) : list A * list A * list A :=
match max_prefix (reverse l1) (reverse l2) with
......@@ -296,7 +296,7 @@ Hint Extern 0 (_ ⊆+ _) => reflexivity : core.
Fixpoint list_remove `{EqDecision A} (x : A) (l : list A) : option (list A) :=
match l with
| [] => 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.
(** Removes all elements in the list [k] from the list [l]. The function returns
......@@ -352,7 +352,7 @@ Section list_set.
match l with
| [] => []
| 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 list_set.
......@@ -442,9 +442,9 @@ Implicit Types l k : list A.
Global Instance: Inj2 (=) (=) (=) (@cons A).
Proof. by injection 1. Qed.
Global Instance: k, Inj (=) (=) (k ++).
Global Instance: k, Inj (=) (=) (k ++.).
Proof. intros ???. apply app_inv_head. Qed.
Global Instance: k, Inj (=) (=) (++ k).
Global Instance: k, Inj (=) (=) (.++ k).
Proof. intros ???. apply app_inv_tail. Qed.
Global Instance: Assoc (=) (@app A).
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.
Proof. rewrite elem_of_app. tauto. Qed.
Lemma elem_of_list_singleton x y : x [y] x = y.
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.
Lemma elem_of_list_split l x : x l l1 l2, l = l1 ++ x :: l2.
Proof.
......@@ -1370,7 +1370,7 @@ Proof.
rewrite (Nat.mul_comm _ n) in Hlookup.
unfold sublist_lookup in *; simplify_option_eq;
[|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 (auto using Nat.mod_upper_bound with lia).
Qed.
......@@ -1611,15 +1611,15 @@ Proof.
- by rewrite (right_id_L [] (++)).
- rewrite Permutation_middle, IH. simpl. by rewrite Permutation_middle.
Qed.
Global Instance: x : A, Inj (≡ₚ) (≡ₚ) (x ::).
Global Instance: x : A, Inj (≡ₚ) (≡ₚ) (x ::.).
Proof. red. eauto using Permutation_cons_inv. Qed.
Global Instance: k : list A, Inj (≡ₚ) (≡ₚ) (k ++).
Global Instance: k : list A, Inj (≡ₚ) (≡ₚ) (k ++.).
Proof.
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.
Global Instance: k : list A, Inj (≡ₚ) (≡ₚ) (++ k).
Proof. intros k l1 l2. rewrite !(comm (++) _ k). by apply (inj (k ++)). Qed.
Global Instance: k : list A, Inj (≡ₚ) (≡ₚ) (.++ k).
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.
Proof.
intros Hl. apply replicate_as_elem_of. split.
......@@ -1646,7 +1646,7 @@ Proof.
{ apply elem_of_list_lookup. rewrite Hk, elem_of_cons; auto. }
exists (take i k), (drop (S i) k). split.
- 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.
Qed.
......@@ -2488,7 +2488,7 @@ Section Forall_Exists.
Qed.
Lemma Forall_replicate n x : P x Forall P (replicate n x).
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.
Lemma Forall_take n l : Forall P l Forall P (take n l).
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.
Proof. split. induction xs; naive_solver. induction 1; naive_solver. Qed.
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.
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.
End more_general_properties.
......@@ -3392,14 +3392,14 @@ Section ret_join.
Lemma elem_of_list_join (x : A) (ls : list (list A)) :
x mjoin ls l : list A, x l l ls.
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.
split; [|by induction 1 as [|[|??] ?]].
by induction ls as [|[|??] ?]; constructor; auto.
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.
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.
Lemma Forall_join (P : A Prop) (ls: list (list A)) :
Forall (Forall P) ls Forall P (mjoin ls).
......@@ -4008,7 +4008,7 @@ Section positives_flatten_unflatten.
intros p1 p2 [|y ys] ?; simplify_eq/=; auto.
rewrite !positives_flatten_cons, !(assoc _); intros Hl.
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.
apply (Pdup_suffix_eq _ _ p1 p2) in Hl.
by apply (inj Preverse).
......@@ -4018,7 +4018,7 @@ End positives_flatten_unflatten.
(** * Relection over lists *)
(** We define a simple data structure [rlist] to capture a syntactic
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
a corresponding environment. *)
Inductive rlist (A : Type) :=
......@@ -4071,7 +4071,7 @@ End quote.
Section eval.
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.
induction t; csimpl.
- done.
......
......@@ -170,8 +170,8 @@ Fixpoint Papp (p1 p2 : positive) : positive :=
end.
Infix "++" := Papp : positive_scope.
Notation "(++)" := Papp (only parsing) : positive_scope.
Notation "( p ++)" := (Papp p) (only parsing) : positive_scope.
Notation "(++ q )" := (λ p, Papp p q) (only parsing) : positive_scope.
Notation "( p ++.)" := (Papp p) (only parsing) : positive_scope.
Notation "(.++ q )" := (λ p, Papp p q) (only parsing) : positive_scope.
Fixpoint Preverse_go (p1 p2 : positive) : positive :=
match p2 with
......@@ -187,7 +187,7 @@ Global Instance Papp_1_r : RightId (=) 1 (++).
Proof. done. Qed.
Global Instance Papp_assoc : Assoc (=) (++).
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.
Lemma Preverse_go_app p1 p2 p3 :
......
......@@ -224,14 +224,14 @@ Proof.
apply IHl.
{ intros i x. rewrite Pelem_of_to_list. intros [(?&Hi&?)|Hi].
+ rewrite Preverse_xO, Preverse_xI, !(assoc_L _) in Hi.
by apply (inj (++ _)) in Hi.
by apply (inj (.++ _)) in Hi.
+ apply (Hin (i~0) x). by rewrite Preverse_xO, (assoc_L _) in Hi. }
apply IHr; auto. intros i x Hi.
apply (Hin (i~1) x). by rewrite Preverse_xI, (assoc_L _) in Hi.
- apply IHl.
{ intros i x. rewrite Pelem_of_to_list. intros [(?&Hi&?)|Hi].
+ rewrite Preverse_xO, Preverse_xI, !(assoc_L _) in Hi.
by apply (inj (++ _)) in Hi.
by apply (inj (.++ _)) in Hi.
+ apply (Hin (i~0) x). by rewrite Preverse_xO, (assoc_L _) in Hi. }
apply IHr; auto. intros i x Hi.
apply (Hin (i~1) x). by rewrite Preverse_xI, (assoc_L _) in Hi.
......
......@@ -485,7 +485,7 @@ Section semi_set.
Qed.
Lemma union_list_mono Xs Ys : Xs * Ys Xs Ys.
Proof. induction 1; simpl; auto using union_mono. Qed.
Lemma empty_union_list Xs : Xs Forall ( ) Xs.
Lemma empty_union_list Xs : Xs Forall (. ) Xs.
Proof.
split.
- induction Xs; simpl; rewrite ?empty_union; intuition.
......@@ -554,7 +554,7 @@ Section semi_set.
Proof. unfold_leibniz. apply union_list_app. Qed.
Lemma union_list_reverse_L Xs : (reverse Xs) = Xs.
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.
End leibniz.
......@@ -567,7 +567,7 @@ Section semi_set.
Lemma non_empty_union X Y : X Y X Y .
Proof. rewrite empty_union. destruct (decide (X )); intuition. Qed.
Lemma non_empty_union_list Xs : Xs Exists ( ) Xs.
Lemma non_empty_union_list Xs : Xs Exists (. ) Xs.
Proof. rewrite empty_union_list. apply (not_Forall_Exists _). Qed.
Context `{!LeibnizEquiv C}.
......@@ -577,7 +577,7 @@ Section semi_set.
Proof. unfold_leibniz. apply set_not_subset_inv. Qed.
Lemma non_empty_union_L X Y : X Y X Y .
Proof. unfold_leibniz. apply non_empty_union. Qed.
Lemma non_empty_union_list_L Xs : Xs Exists ( ) Xs.
Lemma non_empty_union_list_L Xs : Xs Exists (. ) Xs.
Proof. unfold_leibniz. apply non_empty_union_list. Qed.
End dec.
End semi_set.
......@@ -973,10 +973,10 @@ End set_monad.
(** Finite sets *)
Definition pred_finite {A} (P : A Prop) := xs : list A, x, P x x xs.
Definition set_finite `{ElemOf A B} (X : B) := pred_finite ( X).
Definition set_finite `{ElemOf A B} (X : B) := pred_finite (. X).
Definition pred_infinite {A} (P : A Prop) := xs : list A, x, P x x xs.
Definition set_infinite `{ElemOf A C} (X : C) := pred_infinite ( X).
Definition set_infinite `{ElemOf A C} (X : C) := pred_infinite (. X).
Section pred_finite_infinite.
Lemma pred_finite_impl {A} (P Q : A Prop) :
......
......@@ -85,7 +85,7 @@ Section sorted.
assert (x2 x1 :: l1) as Hx2' by (by rewrite E; left).
assert (x1 x2 :: l2) as Hx1' by (by rewrite <-E; left).
inversion Hx1'; inversion Hx2'; simplify_eq; auto. }
f_equal. by apply IH, (inj (x2 ::)).
f_equal. by apply IH, (inj (x2 ::.)).
Qed.
Lemma Sorted_unique `{!Transitive R, !AntiSymm (=) R} l1 l2 :
Sorted R l1 Sorted R l2 l1 ≡ₚ l2 l1 = l2.
......
......@@ -21,15 +21,15 @@ Arguments vcons {_} _ {_} _.
Infix ":::" := vcons (at level 60, right associativity) : vector_scope.
Notation "(:::)" := vcons (only parsing) : vector_scope.
Notation "( x :::)" := (vcons x) (only parsing) : vector_scope.
Notation "(::: v )" := (λ x, vcons x v) (only parsing) : vector_scope.
Notation "( x :::.)" := (vcons x) (only parsing) : vector_scope.
Notation "(.::: v )" := (λ x, vcons x v) (only parsing) : vector_scope.
Notation "[# ] " := vnil : vector_scope.
Notation "[# x ] " := (vcons x vnil) : vector_scope.
Notation "[# x ; .. ; y ] " := (vcons x .. (vcons y vnil) ..) : vector_scope.
Infix "+++" := vapp (at level 60, right associativity) : vector_scope.
Notation "(+++)" := vapp (only parsing) : vector_scope.
Notation "( v +++)" := (vapp v) (only parsing) : vector_scope.
Notation "(+++ w )" := (λ v, vapp v w) (only parsing) : vector_scope.
Notation "( v +++.)" := (vapp v) (only parsing) : vector_scope.
Notation "(.+++ w )" := (λ v, vapp v w) (only parsing) : vector_scope.
(** Notice that we cannot define [Vector.nth] as an instance of our [Lookup]
type class, as it has a dependent 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