From 8921799671140d98124620e9177af027a52b5759 Mon Sep 17 00:00:00 2001
From: Simon Spies
Date: Thu, 27 Jun 2019 14:24:24 +0200
Subject: [PATCH] simplify proof of seqZ_cons
---
theories/list.v | 10 ++++------
1 file changed, 4 insertions(+), 6 deletions(-)
diff --git a/theories/list.v b/theories/list.v
index dd78fd2..a3d8b70 100644
--- a/theories/list.v
+++ b/theories/list.v
@@ -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.
--
2.26.2