Update
This commit is contained in:
Thomas Baruchel
parent
bc25f2d521
commit
c9a99e597b
|
|
@ -1,264 +0,0 @@
|
|||
Require Import Nat.
|
||||
Require Import PeanoNat.
|
||||
Require Import List.
|
||||
Require Import Lia.
|
||||
Require Import Arith.Factorial.
|
||||
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.
|
||||
|
||||
|
||||
Example example_0: permutation [].
|
||||
Proof.
|
||||
unfold permutation. intro k. simpl. easy.
|
||||
Qed.
|
||||
|
||||
|
||||
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_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.
|
||||
assert (K1 := H). assert (K2 := H). assert (K3 := I). assert (K4 := I).
|
||||
apply perm_seq_1 in K1. apply perm_seq_2 in K2.
|
||||
apply perm_seq_1 in K3. apply perm_seq_2 in K4.
|
||||
rewrite J in K1. rewrite J in K2.
|
||||
split. apply incl_tran with (m := seq 0 (length l2)); assumption.
|
||||
apply incl_tran with (m := seq 0 (length l2)); assumption.
|
||||
Qed.
|
||||
|
||||
|
||||
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.
|
||||
|
||||
|
||||
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. split; 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.
|
||||
|
||||
(* second part of the proof *)
|
||||
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 | 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.
|
||||
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. split. apply Nat.le_0_l. assumption.
|
||||
Qed.
|
||||
|
||||
|
||||
Lemma perm_max_insert_alt : forall (l1 l2: list nat),
|
||||
permutation l1 -> Add (length l1) l1 l2 -> permutation l2.
|
||||
Proof.
|
||||
intros l1 l2. intros H I.
|
||||
apply Add_split in I. destruct I. destruct H0. destruct H0.
|
||||
rewrite H0 in H. rewrite H1. rewrite H0.
|
||||
replace (length (x++x0) :: x0) with ([length (x++x0)] ++ x0).
|
||||
rewrite <- perm_max_insert. assumption. easy.
|
||||
Qed.
|
||||
|
||||
|
||||
Lemma perm_max_insert_alt_2 : forall (l1 l2: list nat),
|
||||
Add (length l1) l1 l2 -> permutation l2 -> permutation l1.
|
||||
Proof.
|
||||
intros l1 l2. intros H I.
|
||||
apply Add_split in H. destruct H. destruct H. destruct H.
|
||||
rewrite H0 in I. rewrite H. apply perm_max_insert.
|
||||
simpl. rewrite H in I. assumption.
|
||||
Qed.
|
||||
|
||||
|
||||
Lemma perm_count : forall (n: nat) (E: list (list nat)),
|
||||
NoDup E -> (forall l, In l E <-> (length l = n /\ permutation l))
|
||||
-> length E = fact n.
|
||||
Proof.
|
||||
intro n. induction n; intro E; intros H1 H2. simpl.
|
||||
|
||||
assert (I: length (nil: list nat) = 0 /\ permutation nil).
|
||||
easy. apply H2 in I.
|
||||
|
||||
apply In_nth with (d := nil) in I.
|
||||
destruct I. destruct (length E). destruct H.
|
||||
apply Nat.nlt_0_r in H. contradiction H.
|
||||
destruct n. reflexivity. destruct H.
|
||||
|
||||
assert (J: 0 < length E). apply In_nth with (d := nil) in I.
|
||||
destruct I. destruct (length E). destruct H.
|
||||
apply Nat.nlt_0_r in H. contradiction H.
|
||||
apply Arith_prebase.gt_Sn_O_stt.
|
||||
|
||||
assert (K: length E
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
(*
|
||||
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.
|
||||
*)
|
||||
|
|
@ -4,7 +4,7 @@ Require Import List.
|
|||
Import ListNotations.
|
||||
|
||||
|
||||
(** * Various definitions of a subsequences
|
||||
(** * Various definitions
|
||||
|
||||
Different definitions of a subsequence are given; they are proved
|
||||
below to be equivalent, allowing to choose the most convenient at
|
||||
|
|
@ -27,8 +27,7 @@ Fixpoint subsequence3 {X: Type} (l s : list X) : Prop :=
|
|||
end.
|
||||
|
||||
|
||||
(**
|
||||
Identical elementary properties of all definitions of a subsequence.
|
||||
(** * Elementary properties
|
||||
*)
|
||||
|
||||
Theorem subsequence_nil_r {X: Type}: forall (l : list X), subsequence l nil.
|
||||
|
|
@ -187,8 +186,13 @@ Proof.
|
|||
Qed.
|
||||
|
||||
|
||||
(**
|
||||
Equivalence of all definitions of a subsequence.
|
||||
(** * Equivalence of all definitions
|
||||
|
||||
The following three implications are proved:
|
||||
|
||||
- subsequence l s -> subsequence2 l s
|
||||
- subsequence2 l s -> subsequence3 l s
|
||||
- subsequence3 l s -> subsequence l s
|
||||
*)
|
||||
|
||||
Theorem subsequence_eq_def_1 {X: Type} :
|
||||
|
|
@ -270,8 +274,7 @@ Proof.
|
|||
Qed.
|
||||
|
||||
|
||||
(**
|
||||
Decidability of all definitions of a subsequence.
|
||||
(** * Decidability of all definitions
|
||||
*)
|
||||
|
||||
Theorem subsequence2_dec {X: Type}:
|
||||
|
|
@ -333,8 +336,7 @@ Proof.
|
|||
Qed.
|
||||
|
||||
|
||||
(**
|
||||
Various general properties of a subsequence.
|
||||
(** * Various general properties
|
||||
*)
|
||||
|
||||
Theorem subsequence_app {X: Type} :
|
||||
|
|
@ -435,6 +437,8 @@ Proof.
|
|||
Qed.
|
||||
|
||||
|
||||
(** * Tests
|
||||
*)
|
||||
|
||||
Example test1: subsequence [1;2;3;4;5] [1;3;5].
|
||||
Proof.
|
||||
|
|
|
|||
Loading…
Reference in New Issue