Skip to content
Snippets Groups Projects

random collection of lemmas

Merged Michael Sammler requested to merge ci/msammler/list into master

These are some lemmas which I need in my development. @robbertkrebbers and I talked about some of them today. I will make another MR with the rotate function. Let me know what you think and which lemmas seem useful. Also better proofs are always appreciated.

Merge request reports

Pipeline #25874 passed

Pipeline passed for ef163e26 on ci/msammler/list

Approval is optional

Merged by Robbert KrebbersRobbert Krebbers 5 years ago (Mar 31, 2020 11:23am UTC)

Merge details

  • Changes merged into master with 46844f29.
  • Deleted the source branch.

Pipeline #25875 passed

Pipeline passed for 46844f29 on master

Activity

Filter activity
  • Approvals
  • Assignees & reviewers
  • Comments (from bots)
  • Comments (from users)
  • Commits & branches
  • Edits
  • Labels
  • Lock status
  • Mentions
  • Merge request status
  • Tracking
121 121 end.
122 122 Notation max_list := (max_list_with id).
123 123
124 Lemma max_list_le_in n ns:
  • 153 153 Existing Instance TCEq_refl.
    154 154 Hint Mode TCEq ! - - : typeclass_instances.
    155 155
    156 Lemma TCEq_eq {A} (x1 x2 : A) : TCEq x1 x2 x1 = x2.
    157 Proof. split; inversion 1; reflexivity. Qed.
  • 629 629 Lemma list_insert_commute l i j x y :
    630 630 i j <[i:=x]>(<[j:=y]>l) = <[j:=y]>(<[i:=x]>l).
    631 631 Proof. revert i j. by induction l; intros [|?] [|?] ?; f_equal/=; auto. Qed.
    632 Lemma list_insert_id' l i x : ((i < length l)%nat l !! i = Some x) <[i:=x]>l = l.
  • 629 629 Lemma list_insert_commute l i j x y :
    630 630 i j <[i:=x]>(<[j:=y]>l) = <[j:=y]>(<[i:=x]>l).
    631 631 Proof. revert i j. by induction l; intros [|?] [|?] ?; f_equal/=; auto. Qed.
    632 Lemma list_insert_id' l i x : ((i < length l)%nat l !! i = Some x) <[i:=x]>l = l.
    633 Proof.
    634 revert i. induction l; intros [|i]; simpl; intros Heq; try done; simpl; f_equal; eauto with lia.
    635 injection Heq; try lia. done.
    636 Qed.
    632 637 Lemma list_insert_id l i x : l !! i = Some x <[i:=x]>l = l.
  • 629 629 Lemma list_insert_commute l i j x y :
    630 630 i j <[i:=x]>(<[j:=y]>l) = <[j:=y]>(<[i:=x]>l).
    631 631 Proof. revert i j. by induction l; intros [|?] [|?] ?; f_equal/=; auto. Qed.
    632 Lemma list_insert_id' l i x : ((i < length l)%nat l !! i = Some x) <[i:=x]>l = l.
    633 Proof.
    634 revert i. induction l; intros [|i]; simpl; intros Heq; try done; simpl; f_equal; eauto with lia.
  • 1162 1167 intros. apply list_eq. intros j.
    1163 1168 by rewrite !lookup_drop, !list_lookup_alter_ne by lia.
    1164 1169 Qed.
    1170 Lemma drop_insert' l n i x : n i drop n (<[i:=x]>l) = <[i - n := x]>(drop n l).
  • 1162 1167 intros. apply list_eq. intros j.
    1163 1168 by rewrite !lookup_drop, !list_lookup_alter_ne by lia.
    1164 1169 Qed.
    1170 Lemma drop_insert' l n i x : n i drop n (<[i:=x]>l) = <[i - n := x]>(drop n l).
    1171 Proof.
  • 473 476 ( x, x y P x P (Z.pred x))
    474 477 ( x, P x).
    475 478 Proof. intros H0 HS HP. by apply (Z.order_induction' _ _ y). Qed.
    479 Lemma Zmod_almost_small a b c :
  • 473 476 ( x, x y P x P (Z.pred x))
    474 477 ( x, P x).
    475 478 Proof. intros H0 HS HP. by apply (Z.order_induction' _ _ y). Qed.
    479 Lemma Zmod_almost_small a b c :
    480 0 a 0 b
    481 c (a + b)
    482 a < c b < c
    483 (a + b) `mod` c = a + b - c.
    484 Proof.
  • 473 476 ( x, x y P x P (Z.pred x))
    474 477 ( x, P x).
    475 478 Proof. intros H0 HS HP. by apply (Z.order_induction' _ _ y). Qed.
    479 Lemma Zmod_almost_small a b c :
    480 0 a 0 b
    481 c (a + b)
    482 a < c b < c
    483 (a + b) `mod` c = a + b - c.
  • 3829 3922 Lemma foldl_app {A B} (f : A B A) (l k : list B) (a : A) :
    3830 3923 foldl f a (l ++ k) = foldl f (foldl f a l) k.
    3831 3924 Proof. revert a. induction l; simpl; auto. Qed.
    3925 Lemma foldr_fmap {A B C} (f : B A A) x (l : list C) g :
    3926 foldr f x (g <$> l) = foldr (λ b a, f (g b) a) x l.
    3927 Proof. by induction l as [|?? IH]; csimpl; try done; rewrite IH. Qed.
  • 3829 3922 Lemma foldl_app {A B} (f : A B A) (l k : list B) (a : A) :
    3830 3923 foldl f a (l ++ k) = foldl f (foldl f a l) k.
    3831 3924 Proof. revert a. induction l; simpl; auto. Qed.
    3925 Lemma foldr_fmap {A B C} (f : B A A) x (l : list C) g :
    3926 foldr f x (g <$> l) = foldr (λ b a, f (g b) a) x l.
    3927 Proof. by induction l as [|?? IH]; csimpl; try done; rewrite IH. Qed.
    3928 Lemma foldr_ext {A B} (f1 f2 : B A A) x1 x2 l1 l2:
    3929 ( b a, f1 b a = f2 b a) l1 = l2 x1 = x2 foldr f1 x1 l1 = foldr f2 x2 l2.
    3930 Proof. intros Hf -> ->. induction l2 as [|?? IH]; try done; simpl. rewrite IH. apply Hf. Qed.
  • 3174 3190 intros HPQ. induction l as [|x l IH]; simpl; [done|].
    3175 3191 by rewrite (decide_iff (P x) (Q x)), IH by done.
    3176 3192 Qed.
    3193
    3194 Lemma list_find_app l1 l2:
    3195 list_find P l1 = None list_find P (l1 ++ l2) = prod_map (λ x, x + length l1)%nat id <$> list_find P l2.
  • 3174 3190 intros HPQ. induction l as [|x l IH]; simpl; [done|].
    3175 3191 by rewrite (decide_iff (P x) (Q x)), IH by done.
    3176 3192 Qed.
    3193
    3194 Lemma list_find_app l1 l2:
    3195 list_find P l1 = None list_find P (l1 ++ l2) = prod_map (λ x, x + length l1)%nat id <$> list_find P l2.
  • 3174 3190 intros HPQ. induction l as [|x l IH]; simpl; [done|].
    3175 3191 by rewrite (decide_iff (P x) (Q x)), IH by done.
    3176 3192 Qed.
    3193
    3194 Lemma list_find_app l1 l2:
    3195 list_find P l1 = None list_find P (l1 ++ l2) = prod_map (λ x, x + length l1)%nat id <$> list_find P l2.
    3196 Proof.
    3197 induction l1 as [|a l1 IH].
    3198 - intros ?; simpl. destruct (list_find P l2) as [[??] |]; try done; simpl. do 2 f_equal. lia.
    3199 - simpl. case_decide; try done. destruct (list_find P l1) eqn:?; try done. intros _.
    3200 rewrite IH by done. destruct (list_find P (l2)) as [[??] |]; try done; simpl. do 2 f_equal. lia.
    3201 Qed.
    3202
    3203 Lemma list_find_app_None_l l1 l2 :
  • Michael Sammler added 5 commits

    added 5 commits

    Compare with previous version

  • Loading
  • Loading
  • Loading
  • Loading
  • Loading
  • Loading
  • Loading
  • Loading
  • Loading
  • Loading
  • Please register or sign in to reply
    Loading