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-12-05 12:03:37 +01:00
parent ed022ffca7
commit 50b0970b06
1 changed files with 22 additions and 1 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

23
src/mapping.v
View File

@ -103,7 +103,7 @@ Proof.
Qed.
Lemma Permutation_mapping_swap {X: Type} :
Lemma Permutation_mapping_swap_first {X: Type} :
forall (u v base: list X) a1 a2 b1 b2,
Permutation_mapping (a1::a2::u) (b1::b2::v) base
-> Permutation_mapping (a2::a1::u) (b2::b1::v) base.
@ -118,6 +118,27 @@ Proof.
Qed.
Lemma Permutation_mapping_repeat_first {X: Type} :
forall (u v base: list X) a b,
Permutation_mapping (a::u) (b::v) base
-> Permutation_mapping (a::a::u) (b::b::v) base.
Proof.
intros u v base a b. intros H.
destruct H as [p]. destruct H as [l].
destruct H. destruct H0. exists p.
destruct l. inversion H0. exists (n::n::l).
split. assumption. simpl. simpl in H0. simpl in H1.
rewrite H0. rewrite H1.
assert (forall (l: list (option X)) x y z,
x::l = z::l -> x::y::l = z::y::l).
intros. inversion H2. reflexivity.
split. apply H2. inversion H0. reflexivity.
apply H2. inversion H1. reflexivity.
Qed.
Lemma Permutation_mapping_app {X: Type} :
forall (u1 u2 v1 v2 base : list X),
Permutation_mapping (u1 ++ u2) (v1 ++ v2) base