Commit 89217996 authored by Simon Spies's avatar Simon Spies

simplify proof of seqZ_cons

parent 7393911a
Pipeline #18024 canceled with stage
......@@ -3351,12 +3351,10 @@ Section seqZ.
Proof. by destruct n. Qed.
Lemma seqZ_cons m n: n > 0 seqZ m n = m :: seqZ (Z.succ m) (Z.pred n).
Proof.
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.
erewrite <-fmap_seq, map_map, map_ext; eauto.
intros; lia.
intros H. unfold seqZ. replace n with (Z.succ (Z.pred n)) at 1 by lia.
rewrite Z2Nat.inj_succ by lia. f_equal/=.
rewrite <-fmap_seq, <-list_fmap_compose.
apply map_ext; naive_solver lia.
Qed.
Lemma seqZ_length m n: length (seqZ m n) = Z.to_nat n.
Proof. unfold seqZ; by rewrite fmap_length, seq_length. Qed.
......
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