Commit a370c21f authored by Simon Spies's avatar Simon Spies

seqZ: rewrite by, seqZ_lookup_inv iff, case brackets

parent 2b8d69bc
Pipeline #18001 failed with stage
in 0 seconds
......@@ -3354,7 +3354,7 @@ Section seqZ.
intros H. unfold seqZ.
replace (Z.to_nat n) with (S (Z.to_nat (n - 1))) by
(rewrite <-Z2Nat.inj_succ; [f_equal|]; lia).
simpl; f_equal; try lia.
simpl; f_equal.
erewrite <-fmap_seq, map_map, map_ext; eauto.
intros; lia.
Qed.
......@@ -3368,8 +3368,8 @@ Section seqZ.
Proof.
assert (0 n n < 0) as [H|H] by lia.
- revert m'. pattern n. eapply natlike_ind; auto; clear n H.
intros n H1 IH j. rewrite seqZ_cons; try lia.
symmetry. rewrite seqZ_cons; try lia.
intros n H1 IH j. rewrite seqZ_cons by lia.
symmetry. rewrite seqZ_cons by lia.
replace (Z.succ n - 1) with n by lia.
simpl; rewrite IH.
f_equal; try lia; f_equal; lia.
......@@ -3380,10 +3380,11 @@ Section seqZ.
Proof.
assert (0 n n < 0) as [H|H] by lia.
- revert m i. pattern n. eapply natlike_ind; auto; clear n H.
intros; lia.
intros n H1 IH. intros j [|i] ?; rewrite seqZ_cons. 2, 4: lia.
simpl; f_equal; lia. replace (Z.succ n - 1) with n by lia.
simpl; rewrite IH; f_equal; lia.
{ intros; lia. }
intros n H1 IH. intros j [|i] ?; rewrite seqZ_cons by lia.
{ simpl; f_equal; lia. }
replace (Z.succ n - 1) with n by lia.
simpl; rewrite IH by lia; f_equal; lia.
- rewrite !seqZ_nil; auto; lia.
Qed.
......@@ -3391,16 +3392,18 @@ Section seqZ.
Proof.
assert (0 n n < 0) as [H|H] by lia.
- revert m i. pattern n. eapply natlike_ind; auto; clear n H.
intros n H1 IH. intros j [|i] ?; rewrite seqZ_cons. 2, 4: lia.
simpl; f_equal; lia. replace (Z.succ n - 1) with n by lia.
intros n H1 IH. intros j [|i] ?; rewrite seqZ_cons by lia.
{ simpl; f_equal; lia. }
replace (Z.succ n - 1) with n by lia.
simpl; rewrite IH; f_equal; lia.
- rewrite !seqZ_nil; auto; lia.
Qed.
Lemma seqZ_lookup_inv m n i m' : seqZ m n !! i = Some m' m' = m + i i < n.
Lemma seqZ_lookup_inv m n i m' : seqZ m n !! i = Some m' m' = m + i i < n.
Proof.
destruct (Z_le_gt_dec n i); [by rewrite seqZ_lookup_ge|].
rewrite seqZ_lookup by lia. intuition; [congruence|lia].
destruct (Z_le_gt_dec n i).
{ rewrite seqZ_lookup_ge by lia. split; [discriminate|lia]. }
rewrite seqZ_lookup by lia. intuition; [congruence|lia|congruence].
Qed.
End seqZ.
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment