Commit 0bb21a4f authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

Name instances for `Permutation` and add new instance `cons_Permutation_inj_l`.

Naming scheme: `operation_Permutation_{Proper,inj,inj_l,inj_r}`.
parent 3f893ee4
......@@ -1704,9 +1704,11 @@ Proof. apply perm_swap. Qed.
Lemma Permutation_singleton_inj x y : [x] [y] x = y.
Proof. apply Permutation_length_1. Qed.
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.
......@@ -1715,23 +1717,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.
......
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