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-03 21:12:43 +01:00
parent 6bf42aa72a
commit 4961ba9f19
1 changed files with 39 additions and 18 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

57
src/mapping.v
View File

@ -326,8 +326,46 @@ Proof.
assert (forall s, (forall y, In y s -> y < length base)
-> map (nth_error p) s = map (nth_error base) (map f s)).
intro s. induction s; intro K. reflexivity.
intro s. induction s; intro K. reflexivity. simpl. rewrite IHs.
rewrite nth_error_nth' with (d := x). rewrite nth_error_nth' with (d := x).
rewrite <- H4. reflexivity. apply K. apply in_eq. apply H2. apply K.
apply in_eq. rewrite H. apply K. apply in_eq. intro y. intro L. apply K.
apply in_cons. assumption. apply H6. intro y. intro L.
assert (forall s z, In z s -> nth_error base z <> None -> z < length base).
intros s z. intros M1 M2. apply nth_error_Some. assumption.
apply H7 with (s := l). assumption.
assert (forall s (t: list X),
map Some t = map (nth_error base) s -> In y s -> nth_error base y <> None).
intro s. induction s; intros t; intros M1 M2.
apply in_nil in M2. contradiction.
apply in_inv in M2. destruct M2. rewrite H8 in M1.
destruct t; inversion M1; easy.
destruct t; inversion M1; apply IHs with (t := t); assumption.
generalize L. generalize H0. apply H8.
(* second case in split *)
rewrite H0.
(*
apply FinFun.bInjective_bSurjective in H3.
apply FinFun.bSurjective_bBijective in H3. destruct H3 as [g].
destruct H3.
*)
assert (forall s, (forall y, In y s -> y < length base)
-> map (nth_error base) s
= map (nth_error (map (fun e => nth (g e) base x) (seq 0 (length base)))) (map f s)).
intro s. rewrite map_map. induction s; intro K. reflexivity.
simpl. rewrite IHs.
rewrite nth_error_nth' with (d := x).
rewrite nth_error_nth' with (d := x).
rewrite <- H4. reflexivity. apply K.
@ -351,23 +389,6 @@ Proof.
apply IHs with (t := t). assumption. assumption.
generalize L. generalize H0. apply H8.
(* second case in split *)
rewrite H0.
(*
apply FinFun.bInjective_bSurjective in H3.
apply FinFun.bSurjective_bBijective in H3. destruct H3 as [g].
destruct H3.
*)
assert (forall s, (forall y, In y s -> y < length base)
-> map (nth_error base) s
= map (nth_error (map (fun e => nth (g e) base x) (seq 0 (length base)))) (map f s)).
intro s. rewrite map_map. induction s; intro K. reflexivity.
simpl. rewrite IHs.