diff --git a/src/permutations.v b/src/permutations.v index c10422b..7eb0530 100644 --- a/src/permutations.v +++ b/src/permutations.v @@ -1,6 +1,7 @@ Require Import Nat. Require Import PeanoNat. Require Import List. +Require Import Lia. Import ListNotations. (* @@ -41,73 +42,6 @@ Proof. 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. @@ -164,12 +98,103 @@ 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_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_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. + (* first part of the proof *) + 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_max_insert_alt : forall (l1 l2: list nat), + permutation (l1 ++ [ length (l1++l2) ] ++ l2) -> permutation (l1 ++ l2). +Proof. + intros l1 l2. intro H. + + assert (I: incl (seq 0 (length (l1++l2))) (l1++l2)). + assert (incl ([length (l1++l2)]++l2++l1) (l1++[length (l1++l2)]++l2)). + unfold incl. intro a. intro J. rewrite app_assoc in J. + rewrite in_app_iff. rewrite in_app_iff in J. destruct J. + right. assumption. left. assumption. + apply incl_app_inv in H0. destruct H0. apply incl_app_inv in H1. + destruct H1. + assert (incl (l1++l2) (l1 ++ [length (l1 ++ l2)] ++ l2)). + apply incl_app; assumption. + assert (incl ([length (l1++l2)]++l1++l2) (l1 ++ [length (l1 ++ l2)] ++ l2)). + apply incl_app; assumption. + apply incl_Add_inv + with (a := length (l1++l2)) (v := l1++[length (l1++l2)]++l2). + rewrite in_seq. lia. (* TODO *) + replace (length (l1 ++ l2) :: seq 0 (length (l1 ++ l2))) + with ([length (l1 ++ l2)] ++ seq 0 (length (l1 ++ l2))). + apply incl_app. easy. + apply perm_seq_1 in H. rewrite app_length in H. simpl in H. + rewrite Nat.add_succ_r in H. rewrite seq_S in H. apply incl_app_inv in H. + destruct H. rewrite app_length at 1. assumption. + easy. apply Add_app. + + unfold incl in I. unfold permutation. + intro k. intro. apply I. apply in_seq. lia. (* TODO *) +Qed.