Additional changes in list's lemmas.

parent 0c6f8fb1
Pipeline #19061 canceled with stage
......@@ -678,34 +678,31 @@ Lemma list_inserts_app_r l1 l2 l3 i :
list_inserts (length l2 + i) l1 (l2 ++ l3) = l2 ++ list_inserts i l1 l3.
Proof.
revert l1 i; induction l1 as [|x l1 IH]; [done|].
intros i. simpl. rewrite plus_n_Sm, IH, insert_app_r. done.
intros i. simpl. by rewrite plus_n_Sm, IH, insert_app_r.
Qed.
Lemma list_inserts_nil l1 i : list_inserts i l1 [] = [].
Proof.
revert i; induction l1 as [|x l1 IH]; [done|].
intro i. simpl. rewrite IH. done.
intro i. simpl. by rewrite IH.
Qed.
Lemma list_inserts_cons l1 l2 i x :
list_inserts (S i) l1 (x :: l2) = x :: list_inserts i l1 l2.
Proof.
revert i; induction l1 as [|y l1 IH]; [done|].
intro i. simpl. rewrite IH. done.
intro i. simpl. by rewrite IH.
Qed.
Lemma list_inserts_0_r l1 l2 l3 :
length l1 = length l2 list_inserts 0 l1 (l2 ++ l3) = l1 ++ l3.
Proof.
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.
revert l2. induction l1 as [|x l1 IH]; intros [|y l2] ?; simplify_eq/=; [done|].
rewrite list_inserts_cons. simpl. by rewrite IH.
Qed.
Lemma list_inserts_0_l l1 l2 l3 :
length l1 = length l3 list_inserts 0 (l1 ++ l2) l3 = l1.
Proof.
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.
revert l3. induction l1 as [|x l1 IH]; intros [|z l3] ?; simplify_eq/=.
{ by rewrite list_inserts_nil. }
rewrite list_inserts_cons. simpl. by rewrite IH.
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