Commit 8f85e406 authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

Merge branch 'robbert/Permutation' into 'master'

Various improvements to `Permutation` lemmas and instances

See merge request iris/stdpp!270
parents d4dcb60b c2d43491
......@@ -30,6 +30,13 @@ API-breaking change is listed.
- Add `Countable` instance for decidable Sigma types. (by Simon Gregersen)
- Add tactics `compute_done` and `compute_by` for solving goals by computation.
- Add `Inj` instances for `fmap` on option and maps.
- Various changes to `Permutation` lemmas:
+ Rename `Permutation_nil``Permutation_nil_r` and
and `Permutation_singleton``Permutation_singleton_r`.
+ Add lemmas `Permutation_nil_l` and `Permutation_singleton_l`.
+ Add new instance `cons_Permutation_inj_l : Inj (=) (≡ₚ) (.:: k).`.
+ Add lemma `Permutation_cross_split`.
+ Make lemma `elem_of_Permutation` a biimplication
The following `sed` script should perform most of the renaming
(on macOS, replace `sed` by `gsed`, installed via e.g. `brew install gnu-sed`):
......@@ -37,6 +44,9 @@ The following `sed` script should perform most of the renaming
sed -i -E '
s/\bdecide_left\b/decide_True_pi/g
s/\bdecide_right\b/decide_False_pi/g
# Permutation
s/\bPermutation_nil\b/Permutation_nil_r/g
s/\bPermutation_singleton\b/Permutation_singleton_r/g
' $(find theories -name "*.v")
```
......
......@@ -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) :
......
......@@ -31,7 +31,6 @@ Global Instance: Params (@drop) 1 := {}.
Global Arguments Permutation {_} _ _ : assert.
Global Arguments Forall_cons {_} _ _ _ _ _ : assert.
Global Remove Hints Permutation_cons : typeclass_instances.
Notation "(::)" := cons (only parsing) : list_scope.
Notation "( x ::.)" := (cons x) (only parsing) : list_scope.
......@@ -1693,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.
......@@ -1705,13 +1708,11 @@ Proof. apply perm_swap. Qed.
Lemma Permutation_singleton_inj x y : [x] [y] x = y.
Proof. apply Permutation_length_1. Qed.
Global Instance Permutation_cons x : Proper (() ==> ()) (@cons A x).
Proof. by constructor. Qed.
Global Existing Instance Permutation_app'.
Global Instance elem_of_list_permutation_proper x : Proper (() ==> iff) (x .).
Global Instance length_Permutation_proper : Proper (() ==> (=)) (@length A).
Proof. induction 1; simpl; auto with lia. Qed.
Global Instance elem_of_Permutation_proper x : Proper (() ==> iff) (x .).
Proof. induction 1; rewrite ?elem_of_nil, ?elem_of_cons; intuition. Qed.
Global Instance NoDup_proper: Proper (() ==> iff) (@NoDup A).
Global Instance NoDup_Permutation_proper: Proper (() ==> iff) (@NoDup A).
Proof.
induction 1 as [|x l k Hlk IH | |].
- by rewrite !NoDup_nil.
......@@ -1720,23 +1721,28 @@ Proof.
- intuition.
Qed.
Global Instance: Proper (() ==> (=)) (@length A).
Proof. induction 1; simpl; auto with lia. Qed.
Global Instance: Comm () (@app A).
Global Instance app_Permutation_comm : Comm () (@app A).
Proof.
intros l1. induction l1 as [|x l1 IH]; intros l2; simpl.
- by rewrite (right_id_L [] (++)).
- rewrite Permutation_middle, IH. simpl. by rewrite Permutation_middle.
Qed.
Global Instance: x : A, Inj () () (x ::.).
Global Instance cons_Permutation_inj_r x : Inj () () (x ::.).
Proof. red. eauto using Permutation_cons_inv. Qed.
Global Instance: k : list A, Inj () () (k ++.).
Global Instance app_Permutation_inj_r k : Inj () () (k ++.).
Proof.
intros k. induction k as [|x k IH]; intros l1 l2; simpl; auto.
induction k as [|x k IH]; intros l1 l2; simpl; auto.
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 cons_Permutation_inj_l k : Inj (=) () (.:: k).
Proof.
intros x1 x2 Hperm. apply Permutation_singleton_inj.
apply (inj (k ++.)). by rewrite !(comm (++) k).
Qed.
Global Instance app_Permutation_inj_l k : Inj () () (.++ k).
Proof. intros 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.
......@@ -1753,10 +1759,14 @@ Proof.
revert i; induction l as [|y l IH]; intros [|i] ?; simplify_eq/=; auto.
by rewrite Permutation_swap, <-(IH i).
Qed.
Lemma elem_of_Permutation l x : x l k, l x :: k.
Proof. intros [i ?]%elem_of_list_lookup. eauto using delete_Permutation. Qed.
Lemma elem_of_Permutation l x : x l k, l x :: k.
Proof.
split.
- intros [i ?]%elem_of_list_lookup. eexists. by apply delete_Permutation.
- 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].
......@@ -1766,6 +1776,30 @@ 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
lc ++ ld l
lac lad lbc lbd,
lac ++ lad la lbc ++ lbd lb lac ++ lbc lc lad ++ lbd ld.
Proof.
intros <-. revert lc ld.
induction la as [|x la IH]; simpl; intros lc ld Hperm.
{ exists [], [], lc, ld. by rewrite !(right_id_L [] (++)). }
assert (x lc ++ ld)
as [[lc' Hlc]%elem_of_Permutation|[ld' Hld]%elem_of_Permutation]%elem_of_app.
{ rewrite Hperm, elem_of_cons. auto. }
- rewrite Hlc in Hperm. simpl in Hperm. apply (inj (x ::.)) in Hperm.
apply IH in Hperm as (lac&lad&lbc&lbd&Ha&Hb&Hc&Hd).
exists (x :: lac), lad, lbc, lbd; simpl. by rewrite Ha, Hb, Hc, Hd.
- rewrite Hld, <-Permutation_middle in Hperm. apply (inj (x ::.)) in Hperm.
apply IH in Hperm as (lac&lad&lbc&lbd&Ha&Hb&Hc&Hd).
exists lac, (x :: lad), lbc, lbd; simpl.
by rewrite <-Permutation_middle, Ha, Hb, Hc, Hd.
Qed.
Lemma Permutation_inj l1 l2 :
Permutation l1 l2
......@@ -1787,7 +1821,7 @@ Proof.
induction l1 as [|x l1 IH]; intros l2 f Hlen Hf Hl; [by destruct l2|].
rewrite (delete_Permutation l2 (f 0) x) by (by rewrite <-Hl).
pose (g n := let m := f (S n) in if lt_eq_lt_dec m (f 0) then m else m - 1).
eapply Permutation_cons, (IH _ g).
apply Permutation_skip, (IH _ g).
+ rewrite length_delete by (rewrite <-Hl; eauto); simpl in *; lia.
+ unfold g. intros i j Hg.
repeat destruct (lt_eq_lt_dec _ _) as [[?|?]|?]; simplify_eq/=; try lia.
......
......@@ -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