Update
This commit is contained in:
parent
d018b6d30a
commit
33fde1883f
|
@ -152,10 +152,9 @@ Proof.
|
||||||
Qed.
|
Qed.
|
||||||
|
|
||||||
Lemma perm_max_insert : forall (l1 l2: list nat),
|
Lemma perm_max_insert : forall (l1 l2: list nat),
|
||||||
permutation (l1 ++ l2) -> permutation (l1 ++ [ length (l1++l2) ] ++ l2).
|
permutation (l1 ++ l2) <-> permutation (l1 ++ [ length (l1++l2) ] ++ l2).
|
||||||
Proof.
|
Proof.
|
||||||
intros l1 l2. intro H.
|
intros l1 l2. split; intro H.
|
||||||
(* first part of the proof *)
|
|
||||||
unfold permutation. intro k. intro I.
|
unfold permutation. intro k. intro I.
|
||||||
rewrite app_length in I. simpl in I. rewrite Nat.add_succ_r in 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.
|
rewrite Nat.lt_succ_r in I. rewrite <- app_length in I.
|
||||||
|
@ -163,12 +162,6 @@ Proof.
|
||||||
apply in_app_iff in H0. destruct H0. rewrite in_app_iff. left.
|
apply in_app_iff in H0. destruct H0. rewrite in_app_iff. left.
|
||||||
assumption. rewrite in_app_iff. right. apply in_cons. assumption.
|
assumption. rewrite in_app_iff. right. apply in_cons. assumption.
|
||||||
rewrite <- H0. rewrite in_app_iff. right. apply in_eq.
|
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 (I: incl (seq 0 (length (l1++l2))) (l1++l2)).
|
||||||
assert (incl ([length (l1++l2)]++l2++l1) (l1++[length (l1++l2)]++l2)).
|
assert (incl ([length (l1++l2)]++l2++l1) (l1++[length (l1++l2)]++l2)).
|
||||||
|
@ -193,7 +186,8 @@ Proof.
|
||||||
easy. apply Add_app.
|
easy. apply Add_app.
|
||||||
|
|
||||||
unfold incl in I. unfold permutation.
|
unfold incl in I. unfold permutation.
|
||||||
intro k. intro. apply I. apply in_seq. lia. (* TODO *)
|
intro k. intro. apply I. apply in_seq.
|
||||||
|
split. apply Nat.le_0_l. assumption.
|
||||||
Qed.
|
Qed.
|
||||||
|
|
||||||
|
|
||||||
|
|
Loading…
Reference in New Issue
Block a user