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 11:48:56 +01:00
parent be9262d755
commit ed022ffca7
1 changed files with 16 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

16
src/mapping.v
View File

@ -16,6 +16,7 @@ Definition Permutation_mapping {X: Type} (u v base : list X) :=
/\ map Some v = map (nth_error p) l.
(* TODO : ajouter un truc avec Add pour la base *)
@ -102,6 +103,21 @@ Proof.
Qed.
Lemma Permutation_mapping_swap {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.
Proof.
intros u v base a1 a2 b1 b2. intros H.
destruct H as [p]. destruct H as [l].
destruct H. destruct H0. exists p.
destruct l. inversion H0. destruct l. inversion H0. exists (n0::n::l).
split. assumption. inversion H0. inversion H1.
split; simpl; [ rewrite H3 | rewrite H6]; [ rewrite H4 | rewrite H7];
[ rewrite H5 | rewrite H8]; reflexivity.
Qed.
Lemma Permutation_mapping_app {X: Type} :
forall (u1 u2 v1 v2 base : list X),
Permutation_mapping (u1 ++ u2) (v1 ++ v2) base