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:31:46 +01:00
parent 7051b17c49
commit be9262d755
1 changed files with 35 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

35
src/mapping.v
View File

@ -83,6 +83,25 @@ Proof.
Qed.
Lemma Permutation_mapping_cons3 {X: Type} :
forall (u v base: list X) a,
Permutation_mapping u v base
-> Permutation_mapping (a::u) (a::v) (a::base).
Proof.
intros u v base a. intros H.
destruct H as [p]. destruct H as [l].
destruct H. destruct H0. exists (a::p). exists (0::(map S l)).
split. apply perm_skip. assumption.
assert (forall x (y: list X),
map (nth_error (a :: y)) (map S x) = map (nth_error y) x).
intro x. induction x; intro y. reflexivity. simpl. rewrite IHx.
reflexivity.
split; simpl; rewrite H2; [ rewrite H0 | rewrite H1]; reflexivity.
Qed.
Lemma Permutation_mapping_app {X: Type} :
forall (u1 u2 v1 v2 base : list X),
Permutation_mapping (u1 ++ u2) (v1 ++ v2) base
@ -301,6 +320,22 @@ Proof.
Qed.
Lemma Permutation_mapping_subset {X: Type} :
forall (u v base u': list X),
Permutation_mapping u v base
-> incl u' u -> (exists v', incl v' v /\ Permutation_mapping u' v' base).
Proof.
intros u v base u'. intros H I. destruct H as [p]. destruct H as [l].
destruct H. destruct H0.
assert (exists l', map Some u' = map (nth_error base) l').
Admitted.
Lemma Permutation_mapping_base {X: Type} :
forall (u v base p: list X),