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 12:03:51 +01:00
parent 24c29ad273
commit bf9517f266
1 changed files with 18 additions and 4 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

22
src/mapping.v
View File

@ -362,7 +362,8 @@ Proof.
rewrite seq_length. assumption. rewrite H6. rewrite seq_nth. rewrite seq_length. assumption. rewrite H6. rewrite seq_nth.
reflexivity. apply Nat.lt_succ_diag_r. reflexivity. apply Nat.lt_succ_diag_r.
assert (N: In a (a::s)). apply in_eq. apply K in N. assert (N: In a (a::s)). apply in_eq. apply K in N. assert (M := N).
apply H5 in N. destruct N.
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) replace (nth_error (map (fun e : nat => nth (g e) base x)
@ -376,17 +377,30 @@ Proof.
-> n < m -> g' (nth (f' n) (seq 0 m) 0) = n). -> n < m -> g' (nth (f' n) (seq 0 m) 0) = n).
intros m n f' g'. intros J J1 J2 J3. 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 J2 in J3. destruct J3. apply H9. apply J. assumption.
rewrite H6. apply H5 in N. destruct N. rewrite H8. reflexivity. rewrite H6. rewrite H7. reflexivity. apply H2. assumption. rewrite H6.
apply H2. assumption. rewrite H6. apply H5 in N. destruct N.
symmetry. rewrite map_nth_error with (d := f a). reflexivity. symmetry. rewrite map_nth_error with (d := f a). reflexivity.
rewrite nth_error_nth' with (d := 0). rewrite H6. reflexivity. rewrite nth_error_nth' with (d := 0). rewrite H6. reflexivity.
apply H2. assumption. rewrite seq_length. apply H2. assumption.
apply H2. assumption. assumption. intro y. intro G. apply K.
apply in_cons. assumption.
replace (map (fun e : nat => nth e base x) (map g (seq 0 (length base))))
with (map (fun z => (fun e => nth e base x) (g z)) (seq 0 (length base))).
apply H6.
assert (forall w (u v: list X),
map Some u = map (nth_error v) w -> (forall y, In y w -> y < length v)).
intro w; induction w; intros u0 v0; intro J; intro y; intro J1.
contradiction. destruct u0. inversion J.
apply in_inv in J1. destruct J1. rewrite <- H7.
inversion J. apply nth_error_Some. rewrite <- H9. easy.
apply IHw with (u := u0). inversion J. reflexivity. assumption.
apply H7 with (u := x::u). assumption.