Commit 7393911a authored by Simon Spies's avatar Simon Spies

compact proofs using new induction lemma on Z

parent e23cc0c7
Pipeline #18023 canceled with stage
......@@ -3345,13 +3345,11 @@ End mapM.
(** ** Properties of the [seqZ] function *)
Section seqZ.
Implicit Types (m n : Z) (i j: nat).
Implicit Types (m n: Z) (i j: nat).
Local Open Scope Z.
Lemma seqZ_nil m n: n 0 seqZ m n = [].
Proof. intros H; destruct n; simpl; eauto; lia. Qed.
Lemma seqZ_cons m n: n > 0 seqZ m n = m :: seqZ (m + 1) (n - 1).
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
......@@ -3360,52 +3358,38 @@ Section seqZ.
erewrite <-fmap_seq, map_map, map_ext; eauto.
intros; 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.
Proof. unfold seqZ; by rewrite fmap_length, seq_length. Qed.
Lemma seqZ_fmap m m' n: Z.add m <$> seqZ m' n = seqZ (m + m') n.
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 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.
- rewrite !seqZ_nil; auto; lia.
revert m'. induction n as [|n ? IH|] using Z_from_zero_ind; intros m'.
- by rewrite seqZ_nil.
- rewrite (seqZ_cons m') by lia. rewrite (seqZ_cons (m + m')) by lia.
f_equal/=. rewrite Z.pred_succ, IH; simpl. f_equal; lia.
- by rewrite !seqZ_nil by lia.
Qed.
Lemma seqZ_lookup m n i: i < n seqZ m n !! i = Some (m + i).
Lemma seqZ_lookup_lt m n i: i < n seqZ m n !! i = Some (m + i).
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 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.
revert m i.
induction n as [|n ? IH|] using Z_from_zero_ind; intros m i Hi; try lia.
rewrite seqZ_cons by lia. destruct i as [|i]; simpl.
- f_equal; lia.
- rewrite Z.pred_succ, IH by lia. f_equal; lia.
Qed.
Lemma seqZ_lookup_ge m n i: n i seqZ m n !! i = None.
Lemma seqZ_lookup_ge m n i : n i seqZ m n !! i = None.
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 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.
revert m i.
induction n as [|n ? IH|] using Z_from_zero_ind; intros m i Hi; try lia.
- by rewrite seqZ_nil.
- rewrite seqZ_cons by lia.
destruct i as [|i]; simpl; [lia|]. by rewrite Z.pred_succ, IH by lia.
- by rewrite seqZ_nil by lia.
Qed.
Lemma seqZ_lookup_inv m n i m' : seqZ m n !! i = Some m' m' = m + i i < n.
Lemma seqZ_lookup m n i m' : seqZ m n !! i = Some m' m' = m + i i < n.
Proof.
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].
{ rewrite seqZ_lookup_ge by lia. naive_solver lia. }
rewrite seqZ_lookup_lt by lia. naive_solver lia.
Qed.
End seqZ.
......
......@@ -467,6 +467,13 @@ Proof.
apply Nat.mod_bound_pos; lia. }
by rewrite <-Nat2Z.inj_mul, <-Nat2Z.inj_add, <-Nat.div_mod.
Qed.
Lemma Z_from_zero_ind (P : Z Prop) :
P 0
( x, 0 x P x P (Z.succ x))
( x, x 0 P x P (Z.pred x))
( x, P x).
Proof. intros H0 HS HP. by apply (Z.order_induction' _ _ 0). Qed.
Close Scope Z_scope.
(** * Injectivity of casts *)
......
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