From ad0bfc518502adc48e94103264bc5d0a1a7d744e Mon Sep 17 00:00:00 2001 From: Robbert Krebbers Date: Thu, 25 May 2017 11:15:13 +0200 Subject: [PATCH] Prove that a permutation on lists corresponds to an injection between the keys. --- theories/list.v | 44 ++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 44 insertions(+) diff --git a/theories/list.v b/theories/list.v index e0e3da5..4bdc361 100644 --- a/theories/list.v +++ b/theories/list.v @@ -1421,6 +1421,50 @@ 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 length_delete l i : + is_Some (l !! i) → length (delete i l) = length l - 1. +Proof. + rewrite lookup_lt_is_Some. revert i. + induction l as [|x l IH]; intros [|i] ?; simpl in *; [lia..|]. + rewrite IH by lia. lia. +Qed. +Lemma lookup_delete_lt l i j : j < i → delete i l !! j = l !! j. +Proof. revert i j; induction l; intros [] []; naive_solver eauto with lia. Qed. +Lemma lookup_delete_ge l i j : i ≤ j → delete i l !! j = l !! S j. +Proof. revert i j; induction l; intros [] []; naive_solver eauto with lia. Qed. + +Lemma Permutation_inj l1 l2 : + Permutation l1 l2 ↔ + length l1 = length l2 ∧ + ∃ f : nat → nat, Inj (=) (=) f ∧ ∀ i, l1 !! i = l2 !! f i. +Proof. + split. + - intros Hl; split; [by apply Permutation_length|]. + induction Hl as [|x l1 l2 _ [f [??]]|x y l|l1 l2 l3 _ [f [? Hf]] _ [g [? Hg]]]. + + exists id; split; [apply _|done]. + + exists (λ i, match i with 0 => 0 | S i => S (f i) end); split. + * by intros [|i] [|j] ?; simplify_eq/=. + * intros [|i]; simpl; auto. + + exists (λ i, match i with 0 => 1 | 1 => 0 | _ => i end); split. + * intros [|[|i]] [|[|j]]; congruence. + * by intros [|[|i]]. + + exists (g ∘ f); split; [apply _|]. intros i; simpl. by rewrite <-Hg, <-Hf. + - intros (Hlen & f & Hf & Hl). revert l2 f Hlen Hf Hl. + 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). + + 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 omega. + apply (inj S), (inj f); lia. + + intros i. unfold g. destruct (lt_eq_lt_dec _ _) as [[?|?]|?]. + * by rewrite lookup_delete_lt, <-Hl. + * simplify_eq. + * rewrite lookup_delete_ge, <-Nat.sub_succ_l by lia; simpl. + by rewrite Nat.sub_0_r, <-Hl. +Qed. + (** ** Properties of the [prefix] and [suffix] predicates *) Global Instance: PreOrder (@prefix A). Proof. -- GitLab