Implement suggestions by Robbert Krebbers on list’s lemmas.

parent 88fa9552
Pipeline #19060 canceled with stage
......@@ -671,38 +671,41 @@ Qed.
Lemma list_inserts_app_l l1 l2 l3 i :
list_inserts i (l1 ++ l2) l3 = list_inserts (length l1 + i) l2 (list_inserts i l1 l3).
Proof.
revert l1 i; induction l1 as [|x xs IH]; [done|].
intro i; simpl; rewrite IH, Nat.add_succ_r; apply list_insert_inserts_lt; lia.
revert l1 i; induction l1 as [|x l1 IH]; [done|].
intro i. simpl. rewrite IH, Nat.add_succ_r. apply list_insert_inserts_lt. lia.
Qed.
Lemma list_inserts_app_r l1 l2 l3 i :
list_inserts (length l2 + i) l1 (l2 ++ l3) = l2 ++ (list_inserts i l1 l3).
list_inserts (length l2 + i) l1 (l2 ++ l3) = l2 ++ list_inserts i l1 l3.
Proof.
revert l1 i; induction l1 as [|x xs IH]; [done|].
intros i; simpl; rewrite plus_n_Sm, IH, insert_app_r; done.
revert l1 i; induction l1 as [|x l1 IH]; [done|].
intros i. simpl. rewrite plus_n_Sm, IH, insert_app_r. done.
Qed.
Lemma list_inserts_nil l1 i : list_inserts i l1 [] = [].
Proof. revert l1 i; induction l1; [| simpl; intro i; rewrite IHl1]; done. Qed.
Proof.
revert i; induction l1 as [|x l1 IH]; [done|].
intro i. simpl. rewrite IH. done.
Qed.
Lemma list_inserts_cons l1 l2 i x :
list_inserts (S i) l1 (x :: l2) = x :: list_inserts i l1 l2.
Proof.
revert l1 i; induction l1 as [|y ys IH]; [done|].
intro i; simpl; rewrite IH; done.
revert i; induction l1 as [|y l1 IH]; [done|].
intro i. simpl. rewrite IH. done.
Qed.
Lemma list_inserts_zero l1 l2 l3 :
length l1 = length l2 -> list_inserts 0 l1 (l2 ++ l3) = l1 ++ l3.
Lemma list_inserts_0_r l1 l2 l3 :
length l1 = length l2 list_inserts 0 l1 (l2 ++ l3) = l1 ++ l3.
Proof.
revert l2 l1; induction l2 as [|y ys IH]; intro l1.
- intro len_zero; rewrite (nil_length_inv _ len_zero); done.
- case l1 as [|x xs]; [done|]; injection 1; clear H; intro same_len; simpl.
rewrite <-(IH _ same_len), list_inserts_cons; done.
revert l1; induction l2 as [|y l2 IH].
- intros l1 len_zero. rewrite (nil_length_inv _ len_zero). done.
- case l1 as [|x l1]; [done|]. injection 1. clear H. intro same_len. simpl.
rewrite <-(IH _ same_len), list_inserts_cons. done.
Qed.
Lemma list_inserts_zero' l1 l2 l3 :
length l1 = length l3 -> list_inserts 0 (l1 ++ l2) l3 = l1.
Lemma list_inserts_0_l l1 l2 l3 :
length l1 = length l3 list_inserts 0 (l1 ++ l2) l3 = l1.
Proof.
revert l1 l3; induction l1 as [|x xs IH]; intro l3.
- intro len_zero; rewrite (nil_length_inv _ (eq_sym len_zero)); apply list_inserts_nil.
- case l3 as [|y ys]; [done|]; injection 1; clear H; intro same_len; simpl.
rewrite list_inserts_cons, (IH _ same_len); done.
revert l3; induction l1 as [|x l1 IH].
- intros l3 len_zero. rewrite (nil_length_inv _ (eq_sym len_zero)). apply list_inserts_nil.
- case l3 as [|y l3]; [done|]. injection 1. clear H. intro same_len. simpl.
rewrite list_inserts_cons, (IH _ same_len). done.
Qed.
(** ** Properties of the [elem_of] predicate *)
......
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