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 05:59:11 +01:00
parent 55bb6b865b
commit 3a679921ae
1 changed files with 67 additions and 12 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

79
src/mapping.v
View File

@ -46,6 +46,47 @@ Qed.
*)
Lemma permutation_mapping_nil {X: Type} :
forall (base : list X), permutation_mapping nil nil base.
Proof.
intro base. exists base. exists nil. split; easy.
Qed.
Lemma permutation_mapping_nil_l {X: Type} :
forall (u base : list X), permutation_mapping nil u base -> u = nil.
Proof.
intro u. induction u; intro base; intro H. reflexivity.
destruct H as [p]. destruct H as [l]. destruct H. destruct H0.
inversion H1. symmetry in H0. apply map_eq_nil in H0. rewrite H0 in H3.
inversion H3.
Qed.
Lemma permutation_mapping_nil_r {X: Type} :
forall (u base : list X), permutation_mapping u nil base -> u = nil.
Proof.
intro u. induction u; intro base; intro H. reflexivity.
destruct H as [p]. destruct H as [l]. destruct H. destruct H0.
inversion H1. symmetry in H3. apply map_eq_nil in H3. rewrite H3 in H0.
inversion H0.
Qed.
Lemma permutation_mapping_cons {X: Type} :
forall (u v base : list X) a b,
permutation_mapping (a::u) (b::v) base -> permutation_mapping u v base.
Proof.
intros u v base a b. intro H. destruct H as [p]. destruct H as [l].
destruct H. destruct H0. exists p. destruct l. inversion H0. exists l.
split. assumption. split; [ inversion H0 | inversion H1]; reflexivity.
Qed.
Lemma permutation_mapping_self {X: Type} :
forall (u base : list X), incl u base -> permutation_mapping u u base.
Proof.
@ -177,9 +218,7 @@ Proof.
intros m n f' g'. intros J J1 J2 J3.
rewrite H6. apply J2 in J3. destruct J3. apply H9. apply J. assumption.
rewrite H6. rewrite H7. reflexivity. apply H2. assumption. rewrite H6.
symmetry. rewrite map_nth_error with (d := f a). reflexivity.
rewrite nth_error_nth' with (d := 0). rewrite H6. reflexivity.
@ -206,10 +245,6 @@ Qed.
(*
Lemma permutation_mapping_base {X: Type} :
forall (u v base p: list X),
Permutation base p -> permutation_mapping u v base
@ -233,8 +268,6 @@ Proof.
apply FinFun.bSurjective_bBijective in H4. destruct H4 as [g].
destruct H4.
exists base. exists (map g l). split.
apply Permutation_trans with (l' := base). apply Permutation_sym.
assumption. apply Permutation_refl. split.
@ -269,9 +302,9 @@ Proof.
intro s. induction s; intros t; intros M1 M2.
apply in_nil in M2. contradiction.
apply in_inv in M2. destruct M2. rewrite H9 in M1.
destruct t. inversion M1. inversion M1. easy.
destruct t. inversion M1. inversion M1.
apply IHs with (t := t). assumption. assumption.
destruct t; inversion M1. easy.
destruct t; inversion M1.
apply IHs with (t := t); assumption.
generalize N. generalize H1. apply H9.
(* second case in split *)
@ -284,7 +317,29 @@ Proof.
rewrite nth_error_nth' with (d := x).
rewrite nth_error_nth' with (d := x).
replace a with (g (f a)) at 1.
rewrite Permutation_nth in H0. destruct H0. destruct H7 as [h].
destruct H7. destruct H8.
apply FinFun.bInjective_bSurjective in H8.
apply FinFun.bSurjective_bBijective in H8. destruct H8 as [h'].
destruct H8.
rewrite H9.
assert (forall n, n < length base -> h n = g n).
intro n. intro J.
replace a with (f (g a)) at 1.
rewrite <- H5. reflexivity.
apply H4. assumption.
apply H6 in M. destruct M. assumption.