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-04 06:06:25 +01:00
parent 1e27de7157
commit 06acb4fd7e
1 changed files with 69 additions and 2 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

71
src/mapping.v
View File

@ -359,6 +359,62 @@ Proof.
= 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.
assert (forall q p, p < q -> nth p (seq 0 q) 0 = p).
intro q. induction q; intro p'; intro J4.
apply Nat.nlt_0_r in J4. contradiction.
rewrite Nat.lt_succ_r in J4. rewrite Nat.le_lteq in J4. destruct J4.
rewrite seq_S. rewrite app_nth1. apply IHq. assumption.
rewrite seq_length. assumption. rewrite H6. rewrite seq_nth.
reflexivity. apply Nat.lt_succ_diag_r.
assert (N: In a (a::s)). apply in_eq. apply K in N.
rewrite nth_error_nth' with (d := x).
replace (nth_error (map (fun e : nat => nth (g e) base x)
(seq 0 (length base))) (f a))
with (Some ((fun e => nth (g e) base x)
(nth (f a) (seq 0 (length base)) 0))).
assert (forall m n f' g',
FinFun.bFun m f' -> FinFun.bFun m g'
-> (forall x : nat, x < m -> g' (f' x) = x /\ f' (g' x) = x)
-> n < m -> g' (nth (f' n) (seq 0 m) 0) = n).
intros m n f' g'. intros J J1 J2 J3.
rewrite H6. apply J2 in J3. destruct J3. apply H7. apply J. assumption.
rewrite H6. apply H5 in N. destruct N. rewrite H8. reflexivity.
apply H2. assumption. rewrite H6. apply H5 in N. destruct N.
rewrite H7.
rewrite nth_error_nth' with (d := x).
rewrite nth_error_nth' with (d := x).
replace (nth_error (map (fun e : nat => nth (g e) base x)
@ -379,12 +435,23 @@ Proof.
rewrite Nat.lt_succ_r in J4. rewrite Nat.le_lteq in J4. destruct J4.
rewrite seq_S. rewrite app_nth1. apply IHq. assumption.
rewrite seq_length. assumption. rewrite H6. rewrite seq_nth.
reflexivity. apply Nat.lt_succ_diag_r. rewrite H6.
apply J2 in J3. destruct J3. apply H7. apply J. assumption.
reflexivity. apply Nat.lt_succ_diag_r.
rewrite H6. apply J2 in J3. destruct J3. apply H7. apply J. assumption.
rewrite H6. reflexivity. assumption. assumption. assumption.
apply K. apply in_eq.
rewrite nth_error_nth' with (d := x).
(* aboutit à
Some (nth (g (nth (f a) (seq 0 (length base)) 0)) base x) =
Some
(nth (f a) (map (fun e : nat => nth (g e) base x) (seq 0 (length base))) x)
*)
replace (nth (f a) (ma
rewrite <- map_nth at 1.