Skip to content
Snippets Groups Projects
Commit 5e0eed6a authored by Ralf Jung's avatar Ralf Jung
Browse files

hopefully make proof work under older Coq

parent e82ce174
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
Showing
with 2 additions and 2 deletions
stdpp/listZ.v
+ 2
− 2
View file @ 5e0eed6a
...@@ -123,9 +123,9 @@ Lemma lookupZ_app l1 l2 i : ...@@ -123,9 +123,9 @@ Lemma lookupZ_app l1 l2 i :
match l1 !! i with Some x => Some x | None => l2 !! (i - lengthZ l1) end. match l1 !! i with Some x => Some x | None => l2 !! (i - lengthZ l1) end.
Proof. Proof.
rewrite !lookupZ_eq. Z.case_to_onat; simpl. rewrite !lookupZ_eq. Z.case_to_onat; simpl.
- rewrite lookup_app. case_match. 1:done. - rewrite lookup_app. case_match eqn:Hli. 1:done.
assert (lengthZ l1 ≤ i). assert (lengthZ l1 ≤ i).
{ rewrite lookup_ge_None in *. lia. } { apply lookup_ge_None in Hli. lia. }
rewrite Z.to_onat_nonneg by lia. simpl. f_equal. lia. rewrite Z.to_onat_nonneg by lia. simpl. f_equal. lia.
- rewrite Z.to_onat_neg by lia. done. - rewrite Z.to_onat_neg by lia. done.
Qed. Qed.
......
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment