Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

adapt to coq/coq#18563 #1814

Merged
merged 1 commit into from
Jan 31, 2024
+7 −7
Merged

adapt to coq/coq#18563 #1814

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 1 addition & 1 deletion rewriter
Open in desktop
Submodule rewriter updated 1 files
+5 −5 src/Rewriter/Util/ListUtil.v
2 changes: 1 addition & 1 deletion src/Assembly/Symbolic.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -1565,7 +1565,7 @@ Module dag <: Dag.
| lia
| exfalso; assumption
| rewrite Nat2N.id in *
| rewrite nth_error_app
| rewrite ListUtil.nth_error_app
| rewrite Nat.sub_diag in *
| rewrite nth_error_length_error in * by lia
| rewrite @nth_error_nil_error in *
Expand Down
10 changes: 5 additions & 5 deletions src/Util/ListUtil.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -2656,7 +2656,7 @@ Lemma nth_error_rev A n ls : List.nth_error (@List.rev A ls) n = if lt_dec n (le
Proof.
destruct lt_dec; [ | rewrite nth_error_length_error; rewrite ?List.rev_length; try reflexivity; lia ].
revert dependent n; induction ls as [|x xs IHxs]; cbn [length List.rev]; try reflexivity; intros; try lia.
{ rewrite nth_error_app, List.rev_length, Nat.sub_succ.
{ rewrite ListUtil.nth_error_app, List.rev_length, Nat.sub_succ.
destruct lt_dec.
{ rewrite IHxs by lia.
rewrite <- (Nat.succ_pred_pos (length xs - n)) by lia.
Expand Down Expand Up @@ -3330,7 +3330,7 @@ Section find_index.
specialize (H' _ eq_refl); congruence. }
{ rewrite find_none_iff_nth_error in H.
intros n a; specialize (H n (n, a)).
rewrite nth_error_combine, nth_error_seq in H.
rewrite nth_error_combine, ListUtil.nth_error_seq in H.
edestruct lt_dec; [ | rewrite nth_error_length_error by lia; congruence ].
edestruct nth_error eqn:?; intros; Option.inversion_option; subst; specialize (H eq_refl); assumption. }
Qed.
Expand All @@ -3343,9 +3343,9 @@ Section find_index.
edestruct find eqn:H; cbn; [ | split; [ congruence | ] ].
{ rewrite find_some_iff in H.
destruct H as [n' H].
rewrite nth_error_combine, nth_error_seq in H.
rewrite nth_error_combine, ListUtil.nth_error_seq in H.
setoid_rewrite nth_error_combine in H.
setoid_rewrite nth_error_seq in H.
setoid_rewrite ListUtil.nth_error_seq in H.
break_innermost_match_hyps; split; intro H'; destruct_head'_and; Option.inversion_option; subst; cbn in *.
all: repeat apply conj; eauto.
{ let H := match goal with H : forall n, n < _ -> _ |- _ => H end in
Expand All @@ -3364,7 +3364,7 @@ Section find_index.
congruence. } } }
{ rewrite find_none_iff_nth_error in H.
intros [ [a [H0 H1]] ?]; specialize (H n (n, a)).
rewrite nth_error_combine, nth_error_seq, H0 in H.
rewrite nth_error_combine, ListUtil.nth_error_seq, H0 in H.
break_innermost_match_hyps; [ | rewrite nth_error_length_error in H0 by lia; congruence ].
specialize (H eq_refl); cbn in *.
congruence. }
Expand Down
Loading