Commit 33b3cd0d authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

Rename `Permutation_nil` and `Permutation_singleton` into `Permutation_nil_r`...

Rename `Permutation_nil` and `Permutation_singleton` into `Permutation_nil_r` and `Permutation_singleton_r`.

Add lemmas `Permutation_nil_l` and `Permutation_singleton_l`.
parent 0bb21a4f
......@@ -938,7 +938,7 @@ Qed.
Lemma map_to_list_singleton {A} i (x : A) :
map_to_list ({[i:=x]} : M A) = [(i,x)].
Proof.
apply Permutation_singleton. unfold singletonM, map_singleton.
apply Permutation_singleton_r. unfold singletonM, map_singleton.
by rewrite map_to_list_insert, map_to_list_empty by eauto using lookup_empty.
Qed.
Lemma map_to_list_delete {A} (m : M A) i x :
......
......@@ -85,7 +85,7 @@ Qed.
Lemma elements_empty' X : elements X = [] X .
Proof.
split; intros HX; [by apply elements_empty_inv|].
by rewrite <-Permutation_nil, HX, elements_empty.
by rewrite <-Permutation_nil_r, HX, elements_empty.
Qed.
Lemma elements_union_singleton (X : C) x :
......@@ -99,7 +99,7 @@ Proof.
Qed.
Lemma elements_singleton x : elements ({[ x ]} : C) = [x].
Proof.
apply Permutation_singleton. by rewrite <-(right_id () {[x]}),
apply Permutation_singleton_r. by rewrite <-(right_id () {[x]}),
elements_union_singleton, elements_empty by set_solver.
Qed.
Lemma elements_disj_union (X Y : C) :
......
......@@ -1692,10 +1692,14 @@ Proof.
Qed.
(** ** Properties of the [Permutation] predicate *)
Lemma Permutation_nil l : l [] l = [].
Lemma Permutation_nil_r l : l [] l = [].
Proof. split; [by intro; apply Permutation_nil | by intros ->]. Qed.
Lemma Permutation_singleton l x : l [x] l = [x].
Lemma Permutation_singleton_r l x : l [x] l = [x].
Proof. split; [by intro; apply Permutation_length_1_inv | by intros ->]. Qed.
Lemma Permutation_nil_l l : [] l [] = l.
Proof. by rewrite (symmetry_iff ()), Permutation_nil_r. Qed.
Lemma Permutation_singleton_l l x : [x] l [x] = l.
Proof. by rewrite (symmetry_iff ()), Permutation_singleton_r. Qed.
Lemma Permutation_skip x l l' : l l' x :: l x :: l'.
Proof. apply perm_skip. Qed.
......@@ -1762,7 +1766,7 @@ Proof.
- intros [k ->]. by left.
Qed.
Lemma Permutation_cons_inv l k x :
Lemma Permutation_cons_inv_r l k x :
k x :: l k1 k2, k = k1 ++ x :: k2 l k1 ++ k2.
Proof.
intros Hk. assert ( i, k !! i = Some x) as [i Hi].
......@@ -1772,6 +1776,9 @@ Proof.
- rewrite <-delete_take_drop. apply (inj (x ::.)).
by rewrite <-Hk, <-(delete_Permutation k) by done.
Qed.
Lemma Permutation_cons_inv_l l k x :
x :: l k k1 k2, k = k1 ++ x :: k2 l k1 ++ k2.
Proof. by intros ?%(symmetry_iff ())%Permutation_cons_inv_r. Qed.
Lemma Permutation_cross_split l la lb lc ld :
la ++ lb l
......
......@@ -77,7 +77,7 @@ Section sorted.
intros Hl1; revert l2. induction Hl1 as [|x1 l1 ? IH Hx1]; intros l2 Hl2 E.
{ symmetry. by apply Permutation_nil. }
destruct Hl2 as [|x2 l2 ? Hx2].
{ by apply Permutation_nil in E. }
{ by apply Permutation_nil_r in E. }
assert (x1 = x2); subst.
{ rewrite Forall_forall in Hx1, Hx2.
assert (x2 x1 :: l1) as Hx2' by (by rewrite E; left).
......
Supports Markdown
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