Commit f4a2763b authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

Merge branch 'strict-bulleting' into 'master'

Switch to strict bulleting everywhere

See merge request iris/stdpp!184
parents d9bb5450 ad1d9f13
...@@ -254,7 +254,7 @@ Hint Mode LeibnizEquiv ! - : typeclass_instances. ...@@ -254,7 +254,7 @@ Hint Mode LeibnizEquiv ! - : typeclass_instances.
Lemma leibniz_equiv_iff `{LeibnizEquiv A, !Reflexive (@{A})} (x y : A) : Lemma leibniz_equiv_iff `{LeibnizEquiv A, !Reflexive (@{A})} (x y : A) :
x y x = y. x y x = y.
Proof. split. apply leibniz_equiv. intros ->; reflexivity. Qed. Proof. split; [apply leibniz_equiv|]. intros ->; reflexivity. Qed.
Ltac fold_leibniz := repeat Ltac fold_leibniz := repeat
match goal with match goal with
...@@ -1009,7 +1009,10 @@ Section disjoint_list. ...@@ -1009,7 +1009,10 @@ Section disjoint_list.
Lemma disjoint_list_nil : ##@{A} [] True. Lemma disjoint_list_nil : ##@{A} [] True.
Proof. split; constructor. Qed. Proof. split; constructor. Qed.
Lemma disjoint_list_cons X Xs : ## (X :: Xs) X ## Xs ## Xs. Lemma disjoint_list_cons X Xs : ## (X :: Xs) X ## Xs ## Xs.
Proof. split. inversion_clear 1; auto. intros [??]. constructor; auto. Qed. Proof.
split; [inversion_clear 1; auto |].
intros [??]. constructor; auto.
Qed.
End disjoint_list. End disjoint_list.
Class Filter A B := filter: (P : A Prop) `{ x, Decision (P x)}, B B. Class Filter A B := filter: (P : A Prop) `{ x, Decision (P x)}, B B.
......
...@@ -22,8 +22,8 @@ Proof. ...@@ -22,8 +22,8 @@ Proof.
split; [split; [split| |]|]. split; [split; [split| |]|].
- by intros x ?. - by intros x ?.
- by intros x y; rewrite <-(bool_decide_spec (x = y)). - by intros x y; rewrite <-(bool_decide_spec (x = y)).
- split. apply orb_prop_elim. apply orb_prop_intro. - split; [apply orb_prop_elim | apply orb_prop_intro].
- split. apply andb_prop_elim. apply andb_prop_intro. - split; [apply andb_prop_elim | apply andb_prop_intro].
- intros X Y x; unfold elem_of, boolset_elem_of; simpl. - intros X Y x; unfold elem_of, boolset_elem_of; simpl.
destruct (boolset_car X x), (boolset_car Y x); simpl; tauto. destruct (boolset_car X x), (boolset_car Y x); simpl; tauto.
- done. - done.
......
...@@ -138,8 +138,9 @@ Definition coGpick `{Countable A, Infinite A} (X : coGset A) : A := ...@@ -138,8 +138,9 @@ Definition coGpick `{Countable A, Infinite A} (X : coGset A) : A :=
Lemma coGpick_elem_of `{Countable A, Infinite A} X : Lemma coGpick_elem_of `{Countable A, Infinite A} X :
¬set_finite X coGpick X X. ¬set_finite X coGpick X X.
Proof. Proof.
unfold coGpick. destruct X as [X|X]; rewrite coGset_finite_spec; simpl. unfold coGpick.
done. by intros _; apply is_fresh. destruct X as [X|X]; rewrite coGset_finite_spec; simpl; [done|].
by intros _; apply is_fresh.
Qed. Qed.
(** * Conversion to and from gset *) (** * Conversion to and from gset *)
...@@ -168,8 +169,8 @@ Definition coGset_to_coPset (X : coGset positive) : coPset := ...@@ -168,8 +169,8 @@ Definition coGset_to_coPset (X : coGset positive) : coPset :=
Lemma elem_of_coGset_to_coPset X x : x coGset_to_coPset X x X. Lemma elem_of_coGset_to_coPset X x : x coGset_to_coPset X x X.
Proof. Proof.
destruct X as [X|X]; simpl. destruct X as [X|X]; simpl.
by rewrite elem_of_gset_to_coPset. - by rewrite elem_of_gset_to_coPset.
by rewrite elem_of_difference, elem_of_gset_to_coPset, (left_id True ()). - by rewrite elem_of_difference, elem_of_gset_to_coPset, (left_id True ()).
Qed. Qed.
(** * Inefficient conversion to arbitrary sets with a top element *) (** * Inefficient conversion to arbitrary sets with a top element *)
......
...@@ -8,7 +8,7 @@ Lemma dec_stable `{Decision P} : ¬¬P → P. ...@@ -8,7 +8,7 @@ Lemma dec_stable `{Decision P} : ¬¬P → P.
Proof. firstorder. Qed. Proof. firstorder. Qed.
Lemma Is_true_reflect (b : bool) : reflect b b. Lemma Is_true_reflect (b : bool) : reflect b b.
Proof. destruct b. left; constructor. right. intros []. Qed. Proof. destruct b; [left; constructor | right; intros []]. Qed.
Instance: Inj (=) () Is_true. Instance: Inj (=) () Is_true.
Proof. intros [] []; simpl; intuition. Qed. Proof. intros [] []; simpl; intuition. Qed.
......
...@@ -234,7 +234,7 @@ End setoid. ...@@ -234,7 +234,7 @@ End setoid.
(** ** General properties *) (** ** General properties *)
Lemma map_eq_iff {A} (m1 m2 : M A) : m1 = m2 i, m1 !! i = m2 !! i. Lemma map_eq_iff {A} (m1 m2 : M A) : m1 = m2 i, m1 !! i = m2 !! i.
Proof. split. by intros ->. apply map_eq. Qed. Proof. split; [by intros ->|]. apply map_eq. Qed.
Lemma map_subseteq_spec {A} (m1 m2 : M A) : Lemma map_subseteq_spec {A} (m1 m2 : M A) :
m1 m2 i x, m1 !! i = Some x m2 !! i = Some x. m1 m2 i x, m1 !! i = Some x m2 !! i = Some x.
Proof. Proof.
...@@ -450,7 +450,9 @@ Lemma delete_empty {A} i : delete i (∅ : M A) = ∅. ...@@ -450,7 +450,9 @@ Lemma delete_empty {A} i : delete i (∅ : M A) = ∅.
Proof. rewrite <-(partial_alter_self ) at 2. by rewrite lookup_empty. Qed. Proof. rewrite <-(partial_alter_self ) at 2. by rewrite lookup_empty. Qed.
Lemma delete_commute {A} (m : M A) i j : Lemma delete_commute {A} (m : M A) i j :
delete i (delete j m) = delete j (delete i m). delete i (delete j m) = delete j (delete i m).
Proof. destruct (decide (i = j)). by subst. by apply partial_alter_commute. Qed. Proof.
destruct (decide (i = j)) as [->|]; [done|]. by apply partial_alter_commute.
Qed.
Lemma delete_insert_ne {A} (m : M A) i j x : Lemma delete_insert_ne {A} (m : M A) i j x :
i j delete i (<[j:=x]>m) = <[j:=x]>(delete i m). i j delete i (<[j:=x]>m) = <[j:=x]>(delete i m).
Proof. intro. by apply partial_alter_commute. Qed. Proof. intro. by apply partial_alter_commute. Qed.
...@@ -591,7 +593,7 @@ Lemma insert_subset_inv {A} (m1 m2 : M A) i x : ...@@ -591,7 +593,7 @@ Lemma insert_subset_inv {A} (m1 m2 : M A) i x :
m2', m2 = <[i:=x]>m2' m1 m2' m2' !! i = None. m2', m2 = <[i:=x]>m2' m1 m2' m2' !! i = None.
Proof. Proof.
intros Hi Hm1m2. exists (delete i m2). split_and?. intros Hi Hm1m2. exists (delete i m2). split_and?.
- rewrite insert_delete, insert_id. done. - rewrite insert_delete, insert_id; [done|].
eapply lookup_weaken, strict_include; eauto. by rewrite lookup_insert. eapply lookup_weaken, strict_include; eauto. by rewrite lookup_insert.
- eauto using insert_delete_subset. - eauto using insert_delete_subset.
- by rewrite lookup_delete. - by rewrite lookup_delete.
...@@ -876,7 +878,7 @@ Lemma map_to_list_empty_inv {A} (m : M A) : map_to_list m = [] → m = ∅. ...@@ -876,7 +878,7 @@ Lemma map_to_list_empty_inv {A} (m : M A) : map_to_list m = [] → m = ∅.
Proof. intros Hm. apply map_to_list_empty_inv_alt. by rewrite Hm. Qed. Proof. intros Hm. apply map_to_list_empty_inv_alt. by rewrite Hm. Qed.
Lemma map_to_list_empty' {A} (m : M A) : map_to_list m = [] m = . Lemma map_to_list_empty' {A} (m : M A) : map_to_list m = [] m = .
Proof. Proof.
split. apply map_to_list_empty_inv. intros ->. apply map_to_list_empty. split; [apply map_to_list_empty_inv|]. intros ->. apply map_to_list_empty.
Qed. Qed.
Lemma map_to_list_insert_inv {A} (m : M A) l i x : Lemma map_to_list_insert_inv {A} (m : M A) l i x :
...@@ -982,7 +984,10 @@ Proof. ...@@ -982,7 +984,10 @@ Proof.
unfold size, map_size. by rewrite length_zero_iff_nil, map_to_list_empty'. unfold size, map_size. by rewrite length_zero_iff_nil, map_to_list_empty'.
Qed. Qed.
Lemma map_size_empty_iff {A} (m : M A) : size m = 0 m = . Lemma map_size_empty_iff {A} (m : M A) : size m = 0 m = .
Proof. split. apply map_size_empty_inv. by intros ->; rewrite map_size_empty. Qed. Proof.
split; [apply map_size_empty_inv|].
by intros ->; rewrite map_size_empty.
Qed.
Lemma map_size_non_empty_iff {A} (m : M A) : size m 0 m . Lemma map_size_non_empty_iff {A} (m : M A) : size m 0 m .
Proof. by rewrite map_size_empty_iff. Qed. Proof. by rewrite map_size_empty_iff. Qed.
...@@ -1703,7 +1708,7 @@ Proof. by apply (partial_alter_merge _). Qed. ...@@ -1703,7 +1708,7 @@ Proof. by apply (partial_alter_merge _). Qed.
Lemma foldr_delete_union_with (m1 m2 : M A) is : Lemma foldr_delete_union_with (m1 m2 : M A) is :
foldr delete (union_with f m1 m2) is = foldr delete (union_with f m1 m2) is =
union_with f (foldr delete m1 is) (foldr delete m2 is). union_with f (foldr delete m1 is) (foldr delete m2 is).
Proof. induction is as [|?? IHis]; simpl. done. by rewrite IHis, delete_union_with. Qed. Proof. induction is as [|?? IHis]; simpl; [done|]. by rewrite IHis, delete_union_with. Qed.
Lemma insert_union_with m1 m2 i x y z : Lemma insert_union_with m1 m2 i x y z :
f x y = Some z f x y = Some z
<[i:=z]>(union_with f m1 m2) = union_with f (<[i:=x]>m1) (<[i:=y]>m2). <[i:=z]>(union_with f m1 m2) = union_with f (<[i:=x]>m1) (<[i:=y]>m2).
...@@ -2065,7 +2070,7 @@ Proof. by apply (partial_alter_merge _). Qed. ...@@ -2065,7 +2070,7 @@ Proof. by apply (partial_alter_merge _). Qed.
Lemma foldr_delete_intersection_with (m1 m2 : M A) is : Lemma foldr_delete_intersection_with (m1 m2 : M A) is :
foldr delete (intersection_with f m1 m2) is = foldr delete (intersection_with f m1 m2) is =
intersection_with f (foldr delete m1 is) (foldr delete m2 is). intersection_with f (foldr delete m1 is) (foldr delete m2 is).
Proof. induction is as [|?? IHis]; simpl. done. by rewrite IHis, delete_intersection_with. Qed. Proof. induction is as [|?? IHis]; simpl; [done|]. by rewrite IHis, delete_intersection_with. Qed.
Lemma insert_intersection_with m1 m2 i x y z : Lemma insert_intersection_with m1 m2 i x y z :
f x y = Some z f x y = Some z
<[i:=z]>(intersection_with f m1 m2) = intersection_with f (<[i:=x]>m1) (<[i:=y]>m2). <[i:=z]>(intersection_with f m1 m2) = intersection_with f (<[i:=x]>m1) (<[i:=y]>m2).
......
...@@ -125,7 +125,7 @@ Proof. ...@@ -125,7 +125,7 @@ Proof.
by rewrite (nil_length_inv (elements X)), ?elem_of_nil. by rewrite (nil_length_inv (elements X)), ?elem_of_nil.
Qed. Qed.
Lemma size_empty_iff (X : C) : size X = 0 X . Lemma size_empty_iff (X : C) : size X = 0 X .
Proof. split. apply size_empty_inv. by intros ->; rewrite size_empty. Qed. Proof. split; [apply size_empty_inv|]. by intros ->; rewrite size_empty. Qed.
Lemma size_non_empty_iff (X : C) : size X 0 X . Lemma size_non_empty_iff (X : C) : size X 0 X .
Proof. by rewrite size_empty_iff. Qed. Proof. by rewrite size_empty_iff. Qed.
...@@ -198,7 +198,7 @@ Proof. ...@@ -198,7 +198,7 @@ Proof.
{ apply set_wf. } { apply set_wf. }
intros X IH. destruct (set_choose_or_empty X) as [[x ?]|HX]. intros X IH. destruct (set_choose_or_empty X) as [[x ?]|HX].
- rewrite (union_difference {[ x ]} X) by set_solver. - rewrite (union_difference {[ x ]} X) by set_solver.
apply Hadd. set_solver. apply IH; set_solver. apply Hadd; [set_solver|]. apply IH; set_solver.
- by rewrite HX. - by rewrite HX.
Qed. Qed.
Lemma set_ind_L `{!LeibnizEquiv C} (P : C Prop) : Lemma set_ind_L `{!LeibnizEquiv C} (P : C Prop) :
...@@ -217,10 +217,10 @@ Proof. ...@@ -217,10 +217,10 @@ Proof.
symmetry. apply elem_of_elements. } symmetry. apply elem_of_elements. }
induction 1 as [|x l ?? IH]; simpl. induction 1 as [|x l ?? IH]; simpl.
- intros X HX. setoid_rewrite elem_of_nil in HX. - intros X HX. setoid_rewrite elem_of_nil in HX.
rewrite equiv_empty. done. set_solver. rewrite equiv_empty; [done|]. set_solver.
- intros X HX. setoid_rewrite elem_of_cons in HX. - intros X HX. setoid_rewrite elem_of_cons in HX.
rewrite (union_difference {[ x ]} X) by set_solver. rewrite (union_difference {[ x ]} X) by set_solver.
apply Hadd. set_solver. apply IH. set_solver. apply Hadd; [set_solver|]. apply IH; set_solver.
Qed. Qed.
Lemma set_fold_ind_L `{!LeibnizEquiv C} Lemma set_fold_ind_L `{!LeibnizEquiv C}
{B} (P : B C Prop) (f : A B B) (b : B) : {B} (P : B C Prop) (f : A B B) (b : B) :
......
...@@ -37,7 +37,8 @@ Proof. ...@@ -37,7 +37,8 @@ Proof.
rewrite Nat2Pos.id by done; simpl. rewrite Nat2Pos.id by done; simpl.
destruct (list_find _ xs) as [[i y]|] eqn:HE; simpl. destruct (list_find _ xs) as [[i y]|] eqn:HE; simpl.
- apply list_find_Some in HE as (?&?&?); eauto using lookup_lt_Some. - apply list_find_Some in HE as (?&?&?); eauto using lookup_lt_Some.
- destruct xs; simpl. exfalso; eapply not_elem_of_nil, (HA x). lia. - destruct xs; simpl; [|lia].
exfalso; eapply not_elem_of_nil, (HA x).
Qed. Qed.
Lemma encode_decode A `{finA: Finite A} i : Lemma encode_decode A `{finA: Finite A} i :
i < card A x : A, decode_nat i = Some x encode_nat x = i. i < card A x : A, decode_nat i = Some x encode_nat x = i.
...@@ -258,9 +259,9 @@ Proof. done. Qed. ...@@ -258,9 +259,9 @@ Proof. done. Qed.
Program Instance bool_finite : Finite bool := {| enum := [true; false] |}. Program Instance bool_finite : Finite bool := {| enum := [true; false] |}.
Next Obligation. Next Obligation.
constructor. by rewrite elem_of_list_singleton. apply NoDup_singleton. constructor; [ by rewrite elem_of_list_singleton | apply NoDup_singleton ].
Qed. Qed.
Next Obligation. intros [|]. left. right; left. Qed. Next Obligation. intros [|]; [ left | right; left ]. Qed.
Lemma bool_card : card bool = 2. Lemma bool_card : card bool = 2.
Proof. done. Qed. Proof. done. Qed.
...@@ -292,7 +293,7 @@ Next Obligation. ...@@ -292,7 +293,7 @@ Next Obligation.
rewrite elem_of_app, elem_of_list_fmap. rewrite elem_of_app, elem_of_list_fmap.
intros [(?&?&?)|?]; simplify_eq. intros [(?&?&?)|?]; simplify_eq.
+ destruct Hx. by left. + destruct Hx. by left.
+ destruct IH. by intro; destruct Hx; right. auto. + destruct IH; [ | by auto ]. by intro; destruct Hx; right.
- done. - done.
Qed. Qed.
Next Obligation. Next Obligation.
...@@ -335,7 +336,7 @@ Next Obligation. ...@@ -335,7 +336,7 @@ Next Obligation.
revert IH. generalize (list_enum (enum A) n). intros k Hk. revert IH. generalize (list_enum (enum A) n). intros k Hk.
induction (elem_of_enum x) as [x xs|x xs]; simpl in *. induction (elem_of_enum x) as [x xs|x xs]; simpl in *.
- rewrite elem_of_app, elem_of_list_fmap. left. injection Hl. intros Hl'. - rewrite elem_of_app, elem_of_list_fmap. left. injection Hl. intros Hl'.
eexists (lHl'). split. by apply (sig_eq_pi _). done. eexists (lHl'). split; [|done]. by apply (sig_eq_pi _).
- rewrite elem_of_app. eauto. - rewrite elem_of_app. eauto.
Qed. Qed.
......
...@@ -144,7 +144,9 @@ Qed. ...@@ -144,7 +144,9 @@ Qed.
Lemma NoDup_remove_dups_fast l : NoDup (remove_dups_fast l). Lemma NoDup_remove_dups_fast l : NoDup (remove_dups_fast l).
Proof. Proof.
unfold remove_dups_fast; destruct l as [|x1 [|x2 l]]. unfold remove_dups_fast; destruct l as [|x1 [|x2 l]].
apply NoDup_nil_2. apply NoDup_singleton. apply NoDup_elements. - apply NoDup_nil_2.
- apply NoDup_singleton.
- apply NoDup_elements.
Qed. Qed.
Definition listset_normalize (X : listset A) : listset A := Definition listset_normalize (X : listset A) : listset A :=
let (l) := X in Listset (remove_dups_fast l). let (l) := X in Listset (remove_dups_fast l).
......
...@@ -33,7 +33,7 @@ Instance sig_lexico `{Lexico A} (P : A → Prop) `{∀ x, ProofIrrel (P x)} : ...@@ -33,7 +33,7 @@ Instance sig_lexico `{Lexico A} (P : A → Prop) `{∀ x, ProofIrrel (P x)} :
Lemma prod_lexico_irreflexive `{Lexico A, Lexico B, !Irreflexive (@lexico A _)} Lemma prod_lexico_irreflexive `{Lexico A, Lexico B, !Irreflexive (@lexico A _)}
(x : A) (y : B) : complement lexico y y complement lexico (x,y) (x,y). (x : A) (y : B) : complement lexico y y complement lexico (x,y) (x,y).
Proof. intros ? [?|[??]]. by apply (irreflexivity lexico x). done. Qed. Proof. intros ? [?|[??]]; [|done]. by apply (irreflexivity lexico x). Qed.
Lemma prod_lexico_transitive `{Lexico A, Lexico B, !Transitive (@lexico A _)} Lemma prod_lexico_transitive `{Lexico A, Lexico B, !Transitive (@lexico A _)}
(x1 x2 x3 : A) (y1 y2 y3 : B) : (x1 x2 x3 : A) (y1 y2 y3 : B) :
lexico (x1,y1) (x2,y2) lexico (x2,y2) (x3,y3) lexico (x1,y1) (x2,y2) lexico (x2,y2) (x3,y3)
...@@ -66,7 +66,11 @@ Proof. ...@@ -66,7 +66,11 @@ Proof.
Defined. Defined.
Instance bool_lexico_po : StrictOrder (@lexico bool _). Instance bool_lexico_po : StrictOrder (@lexico bool _).
Proof. split. by intros [] ?. by intros [] [] [] ??. Qed. Proof.
split.
- by intros [] ?.
- by intros [] [] [] ??.
Qed.
Instance bool_lexico_trichotomy: TrichotomyT (@lexico bool _). Instance bool_lexico_trichotomy: TrichotomyT (@lexico bool _).
Proof. Proof.
red; refine (λ b1 b2, red; refine (λ b1 b2,
...@@ -118,7 +122,7 @@ Instance list_lexico_po `{Lexico A, !StrictOrder (@lexico A _)} : ...@@ -118,7 +122,7 @@ Instance list_lexico_po `{Lexico A, !StrictOrder (@lexico A _)} :
StrictOrder (@lexico (list A) _). StrictOrder (@lexico (list A) _).
Proof. Proof.
split. split.
- intros l. induction l. by intros ?. by apply prod_lexico_irreflexive. - intros l. induction l; [by intros ? | by apply prod_lexico_irreflexive].
- intros l1. induction l1 as [|x1 l1]; intros [|x2 l2] [|x3 l3] ??; try done. - intros l1. induction l1 as [|x1 l1]; intros [|x2 l2] [|x3 l3] ??; try done.
eapply prod_lexico_transitive; eauto. eapply prod_lexico_transitive; eauto.
Qed. Qed.
......
...@@ -468,10 +468,10 @@ Global Instance: RightId (=) [] (@app A). ...@@ -468,10 +468,10 @@ Global Instance: RightId (=) [] (@app A).
Proof. intro. apply app_nil_r. Qed. Proof. intro. apply app_nil_r. Qed.
Lemma app_nil l1 l2 : l1 ++ l2 = [] l1 = [] l2 = []. Lemma app_nil l1 l2 : l1 ++ l2 = [] l1 = [] l2 = [].
Proof. split. apply app_eq_nil. by intros [-> ->]. Qed. Proof. split; [apply app_eq_nil|]. by intros [-> ->]. Qed.
Lemma app_singleton l1 l2 x : Lemma app_singleton l1 l2 x :
l1 ++ l2 = [x] l1 = [] l2 = [x] l1 = [x] l2 = []. l1 ++ l2 = [x] l1 = [] l2 = [x] l1 = [x] l2 = [].
Proof. split. apply app_eq_unit. by intros [[-> ->]|[-> ->]]. Qed. Proof. split; [apply app_eq_unit|]. by intros [[-> ->]|[-> ->]]. Qed.
Lemma cons_middle x l1 l2 : l1 ++ x :: l2 = l1 ++ [x] ++ l2. Lemma cons_middle x l1 l2 : l1 ++ x :: l2 = l1 ++ [x] ++ l2.
Proof. done. Qed. Proof. done. Qed.
Lemma list_eq l1 l2 : ( i, l1 !! i = l2 !! i) l1 = l2. Lemma list_eq l1 l2 : ( i, l1 !! i = l2 !! i) l1 = l2.
...@@ -600,7 +600,11 @@ Proof. revert i. by induction l; intros [|?]; f_equal/=. Qed. ...@@ -600,7 +600,11 @@ Proof. revert i. by induction l; intros [|?]; f_equal/=. Qed.
Lemma insert_length l i x : length (<[i:=x]>l) = length l. Lemma insert_length l i x : length (<[i:=x]>l) = length l.
Proof. revert i. by induction l; intros [|?]; f_equal/=. Qed. Proof. revert i. by induction l; intros [|?]; f_equal/=. Qed.
Lemma list_lookup_alter f l i : alter f i l !! i = f <$> l !! i. Lemma list_lookup_alter f l i : alter f i l !! i = f <$> l !! i.
Proof. revert i. induction l as [|?? IHl]. done. intros [|i]. done. apply (IHl i). Qed. Proof.
revert i.
induction l as [|?? IHl]; [done|].
intros [|i]; [done|]. apply (IHl i).
Qed.
Lemma list_lookup_total_alter `{!Inhabited A} f l i : Lemma list_lookup_total_alter `{!Inhabited A} f l i :
i < length l alter f i l !!! i = f (l !!! i). i < length l alter f i l !!! i = f (l !!! i).
Proof. Proof.
...@@ -792,7 +796,7 @@ Proof. by inversion 1. Qed. ...@@ -792,7 +796,7 @@ Proof. by inversion 1. Qed.
Lemma elem_of_nil x : x [] False. Lemma elem_of_nil x : x [] False.
Proof. intuition. by destruct (not_elem_of_nil x). Qed. Proof. intuition. by destruct (not_elem_of_nil x). Qed.
Lemma elem_of_nil_inv l : ( x, x l) l = []. Lemma elem_of_nil_inv l : ( x, x l) l = [].
Proof. destruct l. done. by edestruct 1; constructor. Qed. Proof. destruct l; [done|]. by edestruct 1; constructor. Qed.
Lemma elem_of_not_nil x l : x l l []. Lemma elem_of_not_nil x l : x l l [].
Proof. intros ? ->. by apply (elem_of_nil x). Qed. Proof. intros ? ->. by apply (elem_of_nil x). Qed.
Lemma elem_of_cons l x y : x y :: l x = y x l. Lemma elem_of_cons l x y : x y :: l x = y x l.
...@@ -882,13 +886,13 @@ Qed. ...@@ -882,13 +886,13 @@ Qed.
Lemma NoDup_nil : NoDup (@nil A) True. Lemma NoDup_nil : NoDup (@nil A) True.
Proof. split; constructor. Qed. Proof. split; constructor. Qed.
Lemma NoDup_cons x l : NoDup (x :: l) x l NoDup l. Lemma NoDup_cons x l : NoDup (x :: l) x l NoDup l.
Proof. split. by inversion 1. intros [??]. by constructor. Qed. Proof. split; [by inversion 1|]. intros [??]. by constructor. Qed.
Lemma NoDup_cons_11 x l : NoDup (x :: l) x l. Lemma NoDup_cons_11 x l : NoDup (x :: l) x l.
Proof. rewrite NoDup_cons. by intros [??]. Qed. Proof. rewrite NoDup_cons. by intros [??]. Qed.
Lemma NoDup_cons_12 x l : NoDup (x :: l) NoDup l. Lemma NoDup_cons_12 x l : NoDup (x :: l) NoDup l.
Proof. rewrite NoDup_cons. by intros [??]. Qed. Proof. rewrite NoDup_cons. by intros [??]. Qed.
Lemma NoDup_singleton x : NoDup [x]. Lemma NoDup_singleton x : NoDup [x].
Proof. constructor. apply not_elem_of_nil. constructor. Qed. Proof. constructor; [apply not_elem_of_nil | constructor]. Qed.
Lemma NoDup_app l k : NoDup (l ++ k) NoDup l ( x, x l x k) NoDup k. Lemma NoDup_app l k : NoDup (l ++ k) NoDup l ( x, x l x k) NoDup k.
Proof. Proof.
induction l; simpl. induction l; simpl.
...@@ -985,7 +989,7 @@ Section list_set. ...@@ -985,7 +989,7 @@ Section list_set.
induction 1; simpl; try case_decide. induction 1; simpl; try case_decide.
- constructor. - constructor.
- done. - done.
- constructor. rewrite elem_of_list_difference; intuition. done. - constructor; [|done]. rewrite elem_of_list_difference; intuition.
Qed. Qed.
Lemma elem_of_list_union l k x : x list_union l k x l x k. Lemma elem_of_list_union l k x : x list_union l k x l x k.
Proof. Proof.
...@@ -1009,7 +1013,7 @@ Section list_set. ...@@ -1009,7 +1013,7 @@ Section list_set.
Proof. Proof.
induction 1; simpl; try case_decide. induction 1; simpl; try case_decide.
- constructor. - constructor.
- constructor. rewrite elem_of_list_intersection; intuition. done. - constructor; [|done]. rewrite elem_of_list_intersection; intuition.
- done. - done.
Qed. Qed.
End list_set. End list_set.
...@@ -1646,9 +1650,9 @@ Qed. ...@@ -1646,9 +1650,9 @@ Qed.
(** ** Properties of the [Permutation] predicate *) (** ** Properties of the [Permutation] predicate *)
Lemma Permutation_nil l : l [] l = []. Lemma Permutation_nil l : l [] l = [].
Proof. split. by intro; apply Permutation_nil. by intros ->. Qed. Proof. split; [by intro; apply Permutation_nil | by intros ->]. Qed.
Lemma Permutation_singleton l x : l [x] l = [x]. Lemma Permutation_singleton l x : l [x] l = [x].
Proof. split. by intro; apply Permutation_length_1_inv. by intros ->. Qed. Proof. split; [by intro; apply Permutation_length_1_inv | by intros ->]. Qed.
Definition Permutation_skip := @perm_skip A. Definition Permutation_skip := @perm_skip A.
Definition Permutation_swap := @perm_swap A. Definition Permutation_swap := @perm_swap A.
Definition Permutation_singleton_inj := @Permutation_length_1 A. Definition Permutation_singleton_inj := @Permutation_length_1 A.
...@@ -2067,7 +2071,7 @@ Proof. induction 1; simpl; auto with arith. Qed. ...@@ -2067,7 +2071,7 @@ Proof. induction 1; simpl; auto with arith. Qed.
Lemma sublist_nil_l l : [] `sublist_of` l. Lemma sublist_nil_l l : [] `sublist_of` l.
Proof. induction l; try constructor; auto. Qed. Proof. induction l; try constructor; auto. Qed.
Lemma sublist_nil_r l : l `sublist_of` [] l = []. Lemma sublist_nil_r l : l `sublist_of` [] l = [].
Proof. split. by inversion 1. intros ->. constructor. Qed. Proof. split; [by inversion 1|]. intros ->. constructor. Qed.
Lemma sublist_app l1 l2 k1 k2 : Lemma sublist_app l1 l2 k1 k2 :
l1 `sublist_of` l2 k1 `sublist_of` k2 l1 ++ k1 `sublist_of` l2 ++ k2. l1 `sublist_of` l2 k1 `sublist_of` k2 l1 ++ k1 `sublist_of` l2 ++ k2.
Proof. induction 1; simpl; try constructor; auto. Qed. Proof. induction 1; simpl; try constructor; auto. Qed.
...@@ -2077,7 +2081,7 @@ Lemma sublist_inserts_r k l1 l2 : l1 `sublist_of` l2 → l1 `sublist_of` l2 ++ k ...@@ -2077,7 +2081,7 @@ Lemma sublist_inserts_r k l1 l2 : l1 `sublist_of` l2 → l1 `sublist_of` l2 ++ k
Proof. induction 1; simpl; try constructor; auto using sublist_nil_l. Qed. Proof. induction 1; simpl; try constructor; auto using sublist_nil_l. Qed.
Lemma sublist_cons_r x l k : Lemma sublist_cons_r x l k :
l `sublist_of` x :: k l `sublist_of` k l', l = x :: l' l' `sublist_of` k. l `sublist_of` x :: k l `sublist_of` k l', l = x :: l' l' `sublist_of` k.
Proof. split. inversion 1; eauto. intros [?|(?&->&?)]; constructor; auto. Qed. Proof. split; [inversion 1; eauto|]. intros [?|(?&->&?)]; constructor; auto. Qed.
Lemma sublist_cons_l x l k : Lemma sublist_cons_l x l k :
x :: l `sublist_of` k k1 k2, k = k1 ++ x :: k2 l `sublist_of` k2. x :: l `sublist_of` k k1 k2, k = k1 ++ x :: k2 l `sublist_of` k2.
Proof. Proof.
...@@ -2177,7 +2181,9 @@ Proof. ...@@ -2177,7 +2181,9 @@ Proof.
- intros l3. by exists l3. - intros l3. by exists l3.
- intros l3. rewrite sublist_cons_l. intros (l3'&l3''&?&?); subst. - intros l3. rewrite sublist_cons_l. intros (l3'&l3''&?&?); subst.
destruct (IH l3'') as (l4&?&Hl4); auto. exists (l3' ++ x :: l4). destruct (IH l3'') as (l4&?&Hl4); auto. exists (l3' ++ x :: l4).
split. by apply sublist_inserts_l, sublist_skip. by rewrite Hl4. split.
+ by apply sublist_inserts_l, sublist_skip.
+ by rewrite Hl4.