diff --git a/src/permutations.v b/src/permutations.v new file mode 100644 index 0000000..2c27461 --- /dev/null +++ b/src/permutations.v @@ -0,0 +1,197 @@ +Require Import Nat. +Require Import PeanoNat. +Require Import List. +Import ListNotations. + +(* + Definition of a permutation; + We call a list a "permutation" iff it is a permutation + of integers 0, 1, 2, 3, ... + Eg. [1; 3; 2; 0] +*) +Definition permutation (l: list nat) := + forall k:nat, k < List.length l -> In k l. + + +Theorem perm_seq_1 : forall (l: list nat), + permutation l -> incl (seq 0 (length l)) l. +Proof. + intro l. intro H. unfold permutation in H. + induction (length l). apply incl_nil_l. rewrite seq_S. simpl. + apply incl_app. apply IHn. intro k. intro I. + apply Nat.lt_lt_succ_r in I. apply H in I. assumption. + apply incl_cons. apply H. apply Nat.lt_succ_diag_r. easy. +Qed. + + +Theorem perm_nodup : forall (l: list nat), permutation l -> NoDup l. +Proof. + intro l. intro H. apply perm_seq_1 in H. + apply NoDup_incl_NoDup with (l := seq 0 (length l)). + apply seq_NoDup. rewrite seq_length. easy. assumption. +Qed. + + +Theorem perm_seq_2 : forall (l: list nat), + permutation l -> incl l (seq 0 (length l)). +Proof. + intro l. intro H. apply NoDup_length_incl. + apply seq_NoDup. rewrite seq_length. easy. + apply perm_seq_1. assumption. +Qed. + + +Lemma perm_max_alt : forall (l: list nat), + permutation l -> (forall k, In k l -> k < length l). +Proof. + intro l. intro H. intro k. intro I. + apply perm_seq_2 in H. apply incl_Forall_in_iff in H. + rewrite Forall_forall in H. apply H in I. apply in_seq in I. + destruct I. assumption. +Qed. + + +Lemma perm_max : forall (l: list nat), + permutation l -> l <> nil -> In (length l - 1) l. +Proof. + intro l. intros H I. unfold permutation in H. apply H. + rewrite Nat.sub_1_r. apply Nat.lt_pred_l. + destruct l. contradiction I. reflexivity. easy. +Qed. + + +Lemma perm_max_split : forall (l: list nat), + permutation l -> l <> nil + -> exists l1 l2, l = l1 ++ [length(l) - 1] ++ l2. +Proof. + intro l. intros H I. + assert (J: In (length l - 1) l). apply perm_max; assumption. + apply In_nth with (d := 0) in J. destruct J. destruct H0. + apply nth_split with (d := 0) in H0. destruct H0. destruct H0. + destruct H0. exists x0. exists x1. rewrite H1 in H0. assumption. +Qed. + + +Lemma perm_max_remove : forall (l: list nat), + permutation l -> l <> nil + -> exists l1 l2, ((l = l1 ++ [length(l) - 1] ++ l2) + /\ permutation (l1++l2)). +Proof. + intro l. intros H I. + assert (J: exists l1 l2, l = l1 ++ [length l - 1] ++ l2). + apply perm_max_split; assumption. + destruct J. destruct H0. exists x. exists x0. split. assumption. + assert (J: forall k, k < length l - 1 -> In k l -> In k (x ++ x0)). + intro k. intros. rewrite H0 in H2. apply in_elt_inv in H2. + destruct H2. rewrite H2 in H1. apply Nat.lt_irrefl in H1. contradiction H1. + assumption. unfold permutation. intros. + assert (k < length l - 1). rewrite H0. + rewrite app_length. simpl. rewrite <- Nat.add_sub_assoc. + rewrite Nat.sub_1_r. rewrite Nat.pred_succ. rewrite <- app_length. + assumption. rewrite Nat.le_succ_l. apply Nat.lt_0_succ. + apply J. assumption. apply H. apply Nat.lt_lt_succ_r in H2. + rewrite Nat.sub_1_r in H2. rewrite Nat.succ_pred in H2. + assumption. destruct l. contradiction I. reflexivity. easy. +Qed. + + +Lemma perm_max_insert : forall (l1 l2: list nat), + permutation (l1 ++ l2) -> permutation (l1 ++ [ length (l1++l2) ] ++ l2). +Proof. + intros l1 l2. intro H. unfold permutation. intro k. intro I. + rewrite app_length in I. simpl in I. rewrite Nat.add_succ_r in I. + rewrite Nat.lt_succ_r in I. rewrite <- app_length in I. + apply Nat.le_lteq in I. destruct I. apply H in H0. + apply in_app_iff in H0. destruct H0. rewrite in_app_iff. left. + assumption. rewrite in_app_iff. right. apply in_cons. assumption. + rewrite <- H0. rewrite in_app_iff. right. apply in_eq. +Qed. + + +Lemma perm_incl_incl : forall (l: list nat) (n: nat), + incl l (seq 0 n) -> incl (seq 0 n) l -> NoDup l -> permutation l. +Proof. + intros l n. intros H I J. + assert (length l <= n). replace n with (length (seq 0 n)). + apply NoDup_incl_length; assumption. apply seq_length. + assert (n <= length l). replace n with (length (seq 0 n)). + apply NoDup_incl_length. apply seq_NoDup. assumption. + apply seq_length. assert (length l = n). + apply Nat.le_antisymm; assumption. + apply incl_Forall_in_iff in I. rewrite Forall_forall in I. + unfold permutation. intro k. intro K. apply I. rewrite H2 in K. + assert (0 <= k < 0 + n). split. apply Nat.le_0_l. + assumption. apply in_seq in H3. assumption. +Qed. + + +Lemma perm_eq : forall (l1 l2: list nat), + permutation l1 -> permutation l2 -> length l1 = length l2 + -> incl l1 l2 /\ incl l2 l1. +Proof. + intros l1 l2. intros H I J. +Admitted. + + + +Lemma perm_incl : forall (l1 l2: list nat), + permutation l1 -> permutation l2 -> (incl l1 l2 \/ incl l2 l1). +Proof. + intros l1 l2. intros H I. + assert (length l1 < length l2 \/ length l2 <= length l1). + apply Nat.lt_ge_cases. destruct H0. left. + apply perm_seq_2 in H. apply perm_seq_1 in I. + apply incl_appl with (m := seq (length l1) (length l2 - length l1)) in H. + rewrite <- seq_app in H. rewrite Nat.add_sub_assoc in H. + rewrite Nat.add_sub_swap in H. rewrite Nat.sub_diag in H. + apply incl_tran with (m := seq 0 (length l2)); assumption. + apply Nat.le_refl. apply Nat.lt_le_incl. assumption. + apply Nat.le_lteq in H0. destruct H0. right. + apply perm_seq_2 in I. apply perm_seq_1 in H. + apply incl_appl with (m := seq (length l2) (length l1 - length l2)) in I. + rewrite <- seq_app in I. rewrite Nat.add_sub_assoc in I. + rewrite Nat.add_sub_swap in I. rewrite Nat.sub_diag in I. + apply incl_tran with (m := seq 0 (length l1)); assumption. + apply Nat.le_refl. apply Nat.lt_le_incl. assumption. + left. assert (incl l1 l2 /\ incl l2 l1). + symmetry in H0. apply perm_eq; assumption. destruct H1. assumption. +Qed. + + + + + + + + + + + + + + + +Example test1: permutation [1;2;3;0]. +Proof. + unfold permutation. + simpl. intro k. intro H. + + rewrite PeanoNat.Nat.lt_succ_r in H. + rewrite PeanoNat.Nat.le_lteq in H. + rewrite PeanoNat.Nat.lt_succ_r in H. + rewrite PeanoNat.Nat.le_lteq in H. + rewrite PeanoNat.Nat.lt_succ_r in H. + rewrite PeanoNat.Nat.le_lteq in H. + rewrite PeanoNat.Nat.lt_succ_r in H. + rewrite PeanoNat.Nat.le_lteq in H. + destruct H. destruct H. destruct H. destruct H. + apply PeanoNat.Nat.nlt_0_r in H. contradiction. + right. right. right. left. easy. + left. easy. right. left. easy. right. right. left. easy. +Qed. + + +Example test2: permutation []. +Proof. + unfold permutation. intro k. simpl. easy. +Qed.