Commit 19950ecc authored by Simon Spies's avatar Simon Spies

more general induction lemma

parent 162d4f32
Pipeline #18041 failed with stage
in 0 seconds
......@@ -3360,7 +3360,7 @@ Section seqZ.
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.
revert m'. induction n as [|n ? IH|] using Z_from_zero_ind; intros m'.
revert m'. induction n as [|n ? IH|] using (Z_succ_pred_induction 0); 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.
......@@ -3369,7 +3369,7 @@ Section seqZ.
Lemma seqZ_lookup_lt m n i: i < n seqZ m n !! i = Some (m + i).
Proof.
revert m i.
induction n as [|n ? IH|] using Z_from_zero_ind; intros m i Hi; try lia.
induction n as [|n ? IH|] using (Z_succ_pred_induction 0); 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.
......@@ -3377,7 +3377,7 @@ Section seqZ.
Lemma seqZ_lookup_ge m n i : n i seqZ m n !! i = None.
Proof.
revert m i.
induction n as [|n ? IH|] using Z_from_zero_ind; intros m i Hi; try lia.
induction n as [|n ? IH|] using (Z_succ_pred_induction 0); 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.
......
......@@ -467,12 +467,12 @@ 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))
Lemma Z_succ_pred_induction y (P : Z Prop) :
P y
( x, y x P x P (Z.succ x))
( x, x y P x P (Z.pred x))
( x, P x).
Proof. intros H0 HS HP. by apply (Z.order_induction' _ _ 0). Qed.
Proof. intros H0 HS HP. by apply (Z.order_induction' _ _ y). Qed.
Close Scope Z_scope.
......
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