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

Update

This commit is contained in:
Thomas Baruchel 2023-10-21 15:31:33 +02:00
parent 33fde1883f
commit 1e18bbe495
1 changed files with 2 additions and 1 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

3
src/permutations.v
View File

@ -155,6 +155,7 @@ 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.
@ -163,6 +164,7 @@ Proof.
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.
@ -184,7 +186,6 @@ Proof.
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.