baruchel/coqbooks
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

Update

Browse Source
This commit is contained in:
Thomas Baruchel 2023-10-21 15:52:23 +02:00
parent 836232e28e
commit e561abd318
1 changed files with 5 additions and 5 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

10
src/permutations.v
View File

@ -97,7 +97,6 @@ Proof.
Qed.
Lemma perm_max : forall (l: list nat),
permutation l -> l <> nil -> In (length l - 1) l.
Proof.
@ -151,6 +150,7 @@ Proof.
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.
@ -168,8 +168,8 @@ 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. assumption. left. assumption. apply incl_app_inv in H0.
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.
@ -177,9 +177,9 @@ Proof.
apply incl_app; assumption.
apply incl_Add_inv
with (a := length (l1++l2)) (v := l1++[length (l1++l2)]++l2).
rewrite in_seq. lia. (* TODO *)
rewrite in_seq. lia.
replace (length (l1 ++ l2) :: seq 0 (length (l1 ++ l2)))
with ([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.