random collection of lemmas
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
Activity
121 121 end. 122 122 Notation max_list := (max_list_with id). 123 123 124 Lemma max_list_le_in n ns: changed this line in version 6 of the diff
Done !133 (merged)
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. changed this line in version 6 of the diff
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. changed this line in version 6 of the diff
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. changed this line in version 6 of the diff
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). changed this line in version 4 of the diff
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. changed this line in version 6 of the diff
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 : changed this line in version 6 of the diff
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. changed this line in version 6 of the diff
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. changed this line in version 6 of the diff
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. changed this line in version 6 of the diff
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. changed this line in version 6 of the diff
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. changed this line in version 6 of the diff
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. changed this line in version 6 of the diff
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 : changed this line in version 8 of the diff
added 5 commits
-
eb6bc2d6...86cb321a - 3 commits from branch
master - 8fc1b24b - remove trailing whitespace
- ed58fd11 - random collection of lemmas
-
eb6bc2d6...86cb321a - 3 commits from branch
Please register or sign in to reply