Update
This commit is contained in:
Thomas Baruchel
parent
a949320a6f
commit
d018b6d30a
@ -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.
|
||||
|
||||
|
||||
|
||||
|
||||
Loading…
x
Reference in New Issue
Block a user