Commit ad1d9f13 authored by Tej Chajed's avatar Tej Chajed Committed by Robbert Krebbers
Browse files

Start using strict bulleting everywhere

Set Default Goal Selector "!" makes it illegal to ever apply a tactic
with more than one goal (instead, must focus with bullets or braces).
parent d9bb5450
......@@ -254,7 +254,7 @@ Hint Mode LeibnizEquiv ! - : typeclass_instances.
Lemma leibniz_equiv_iff `{LeibnizEquiv A, !Reflexive (@{A})} (x y : A) :
x y x = y.
Proof. split. apply leibniz_equiv. intros ->; reflexivity. Qed.
Proof. split; [apply leibniz_equiv|]. intros ->; reflexivity. Qed.
Ltac fold_leibniz := repeat
match goal with
......@@ -1009,7 +1009,10 @@ Section disjoint_list.
Lemma disjoint_list_nil : ##@{A} [] True.
Proof. split; constructor. Qed.
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.
Class Filter A B := filter: (P : A Prop) `{ x, Decision (P x)}, B B.
......
......@@ -22,8 +22,8 @@ Proof.
split; [split; [split| |]|].
- by intros x ?.
- by intros x y; rewrite <-(bool_decide_spec (x = y)).
- split. apply orb_prop_elim. apply orb_prop_intro.
- split. apply andb_prop_elim. apply andb_prop_intro.
- split; [apply orb_prop_elim | apply orb_prop_intro].
- split; [apply andb_prop_elim | apply andb_prop_intro].
- intros X Y x; unfold elem_of, boolset_elem_of; simpl.
destruct (boolset_car X x), (boolset_car Y x); simpl; tauto.
- done.
......
......@@ -138,8 +138,9 @@ Definition coGpick `{Countable A, Infinite A} (X : coGset A) : A :=
Lemma coGpick_elem_of `{Countable A, Infinite A} X :
¬set_finite X coGpick X X.
Proof.
unfold coGpick. destruct X as [X|X]; rewrite coGset_finite_spec; simpl.
done. by intros _; apply is_fresh.
unfold coGpick.
destruct X as [X|X]; rewrite coGset_finite_spec; simpl; [done|].
by intros _; apply is_fresh.
Qed.
(** * Conversion to and from gset *)
......@@ -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.
Proof.
destruct X as [X|X]; simpl.
by rewrite elem_of_gset_to_coPset.
by rewrite elem_of_difference, elem_of_gset_to_coPset, (left_id True ()).
- by rewrite elem_of_gset_to_coPset.
- by rewrite elem_of_difference, elem_of_gset_to_coPset, (left_id True ()).
Qed.
(** * Inefficient conversion to arbitrary sets with a top element *)
......
......@@ -8,7 +8,7 @@ Lemma dec_stable `{Decision P} : ¬¬P → P.
Proof. firstorder. Qed.
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.
Proof. intros [] []; simpl; intuition. Qed.
......
......@@ -234,7 +234,7 @@ End setoid.
(** ** General properties *)
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) :
m1 m2 i x, m1 !! i = Some x m2 !! i = Some x.
Proof.
......@@ -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.
Lemma delete_commute {A} (m : M A) i j :
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 :
i j delete i (<[j:=x]>m) = <[j:=x]>(delete i m).
Proof. intro. by apply partial_alter_commute. Qed.
......@@ -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.
Proof.
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.
- eauto using insert_delete_subset.
- by rewrite lookup_delete.
......@@ -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.
Lemma map_to_list_empty' {A} (m : M A) : map_to_list m = [] m = .
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.
Lemma map_to_list_insert_inv {A} (m : M A) l i x :
......@@ -982,7 +984,10 @@ Proof.
unfold size, map_size. by rewrite length_zero_iff_nil, map_to_list_empty'.
Qed.
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 .
Proof. by rewrite map_size_empty_iff. Qed.
......@@ -1703,7 +1708,7 @@ Proof. by apply (partial_alter_merge _). Qed.
Lemma foldr_delete_union_with (m1 m2 : M A) is :
foldr delete (union_with f m1 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 :
f x y = Some z
<[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.
Lemma foldr_delete_intersection_with (m1 m2 : M A) is :
foldr delete (intersection_with f m1 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 :
f x y = Some z
<[i:=z]>(intersection_with f m1 m2) = intersection_with f (<[i:=x]>m1) (<[i:=y]>m2).
......
......@@ -125,7 +125,7 @@ Proof.
by rewrite (nil_length_inv (elements X)), ?elem_of_nil.
Qed.
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 .
Proof. by rewrite size_empty_iff. Qed.
......@@ -198,7 +198,7 @@ Proof.
{ apply set_wf. }
intros X IH. destruct (set_choose_or_empty X) as [[x ?]|HX].
- 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.
Qed.
Lemma set_ind_L `{!LeibnizEquiv C} (P : C Prop) :
......@@ -217,10 +217,10 @@ Proof.
symmetry. apply elem_of_elements. }
induction 1 as [|x l ?? IH]; simpl.
- 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.
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.
Lemma set_fold_ind_L `{!LeibnizEquiv C}
{B} (P : B C Prop) (f : A B B) (b : B) :
......
......@@ -37,7 +37,8 @@ Proof.
rewrite Nat2Pos.id by done; simpl.
destruct (list_find _ xs) as [[i y]|] eqn:HE; simpl.
- 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.
Lemma encode_decode A `{finA: Finite A} i :
i < card A x : A, decode_nat i = Some x encode_nat x = i.
......@@ -258,9 +259,9 @@ Proof. done. Qed.
Program Instance bool_finite : Finite bool := {| enum := [true; false] |}.
Next Obligation.
constructor. by rewrite elem_of_list_singleton. apply NoDup_singleton.
constructor; [ by rewrite elem_of_list_singleton | apply NoDup_singleton ].
Qed.
Next Obligation. intros [|]. left. right; left. Qed.
Next Obligation. intros [|]; [ left | right; left ]. Qed.
Lemma bool_card : card bool = 2.
Proof. done. Qed.
......@@ -292,7 +293,7 @@ Next Obligation.
rewrite elem_of_app, elem_of_list_fmap.
intros [(?&?&?)|?]; simplify_eq.
+ destruct Hx. by left.
+ destruct IH. by intro; destruct Hx; right. auto.
+ destruct IH; [ | by auto ]. by intro; destruct Hx; right.
- done.
Qed.
Next Obligation.
......@@ -335,7 +336,7 @@ Next Obligation.
revert IH. generalize (list_enum (enum A) n). intros k Hk.
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'.
eexists (lHl'). split. by apply (sig_eq_pi _). done.
eexists (lHl'). split; [|done]. by apply (sig_eq_pi _).
- rewrite elem_of_app. eauto.
Qed.
......
......@@ -144,7 +144,9 @@ Qed.
Lemma NoDup_remove_dups_fast l : NoDup (remove_dups_fast l).
Proof.
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.
Definition listset_normalize (X : listset A) : listset A :=
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)} :
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).
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 _)}
(x1 x2 x3 : A) (y1 y2 y3 : B) :
lexico (x1,y1) (x2,y2) lexico (x2,y2) (x3,y3)
......@@ -66,7 +66,11 @@ Proof.
Defined.
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 _).
Proof.
red; refine (λ b1 b2,
......@@ -118,7 +122,7 @@ Instance list_lexico_po `{Lexico A, !StrictOrder (@lexico A _)} :
StrictOrder (@lexico (list A) _).
Proof.
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.
eapply prod_lexico_transitive; eauto.
Qed.
......
......@@ -468,10 +468,10 @@ Global Instance: RightId (=) [] (@app A).
Proof. intro. apply app_nil_r. Qed.
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 :
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.
Proof. done. Qed.
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.
Lemma insert_length l i x : length (<[i:=x]>l) = length l.
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.
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 :
i < length l alter f i l !!! i = f (l !!! i).
Proof.
......@@ -792,7 +796,7 @@ Proof. by inversion 1. Qed.
Lemma elem_of_nil x : x [] False.
Proof. intuition. by destruct (not_elem_of_nil x). Qed.
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 [].
Proof. intros ? ->. by apply (elem_of_nil x). Qed.
Lemma elem_of_cons l x y : x y :: l x = y x l.
......@@ -882,13 +886,13 @@ Qed.
Lemma NoDup_nil : NoDup (@nil A) True.
Proof. split; constructor. Qed.
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.
Proof. rewrite NoDup_cons. by intros [??]. Qed.
Lemma NoDup_cons_12 x l : NoDup (x :: l) NoDup l.
Proof. rewrite NoDup_cons. by intros [??]. Qed.
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.
Proof.
induction l; simpl.
......@@ -985,7 +989,7 @@ Section list_set.
induction 1; simpl; try case_decide.
- constructor.
- done.
- constructor. rewrite elem_of_list_difference; intuition. done.
- constructor; [|done]. rewrite elem_of_list_difference; intuition.
Qed.
Lemma elem_of_list_union l k x : x list_union l k x l x k.
Proof.
......@@ -1009,7 +1013,7 @@ Section list_set.
Proof.
induction 1; simpl; try case_decide.
- constructor.
- constructor. rewrite elem_of_list_intersection; intuition. done.
- constructor; [|done]. rewrite elem_of_list_intersection; intuition.
- done.
Qed.
End list_set.
......@@ -1646,9 +1650,9 @@ Qed.
(** ** Properties of the [Permutation] predicate *)
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].
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_swap := @perm_swap A.
Definition Permutation_singleton_inj := @Permutation_length_1 A.
......@@ -2067,7 +2071,7 @@ Proof. induction 1; simpl; auto with arith. Qed.
Lemma sublist_nil_l l : [] `sublist_of` l.
Proof. induction l; try constructor; auto. Qed.
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 :
l1 `sublist_of` l2 k1 `sublist_of` k2 l1 ++ k1 `sublist_of` l2 ++ k2.
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
Proof. induction 1; simpl; try constructor; auto using sublist_nil_l. Qed.
Lemma sublist_cons_r x l 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 :
x :: l `sublist_of` k k1 k2, k = k1 ++ x :: k2 l `sublist_of` k2.
Proof.
......@@ -2177,7 +2181,9 @@ Proof.
- intros l3. by exists l3.
- intros l3. rewrite sublist_cons_l. intros (l3'&l3''&?&?); subst.
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.
- intros l3. rewrite sublist_cons_l. intros (l3'&l3''&?& Hl3); subst.
rewrite sublist_cons_l in Hl3. destruct Hl3 as (l5'&l5''&?& Hl5); subst.
exists (l3' ++ y :: l5' ++ x :: l5''). split.
......@@ -2185,7 +2191,7 @@ Proof.
+ by rewrite !Permutation_middle, Permutation_swap.
- intros l3 ?. destruct (IH2 l3) as (l3'&?&?); trivial.
destruct (IH1 l3') as (l3'' &?&?); trivial. exists l3''.
split. done. etrans; eauto.
split; [done|]. etrans; eauto.
Qed.
Lemma sublist_Permutation l1 l2 l3 :
l1 `sublist_of` l2 l2 l3 l4, l1 l4 l4 `sublist_of` l3.
......@@ -2195,9 +2201,11 @@ Proof.
- intros l1. by exists l1.
- intros l1. rewrite sublist_cons_r. intros [?|(l1'&l1''&?)]; subst.
{ destruct (IH l1) as (l4&?&?); trivial.
exists l4. split. done. by constructor. }
exists l4. split.
- done.
- by constructor. }
destruct (IH l1') as (l4&?&Hl4); auto. exists (x :: l4).
split. by constructor. by constructor.
split; [ by constructor | by constructor ].
- intros l1. rewrite sublist_cons_r. intros [Hl1|(l1'&l1''&Hl1)]; subst.
{ exists l1. split; [done|]. rewrite sublist_cons_r in Hl1.
destruct Hl1 as [?|(l1'&?&?)]; subst; by repeat constructor. }
......@@ -2252,10 +2260,10 @@ Proof. intro. apply submseteq_Permutation_length_le. lia. Qed.
Global Instance: Proper (() ==> () ==> iff) (@submseteq A).
Proof.
intros l1 l2 ? k1 k2 ?. split; intros.
- trans l1. by apply Permutation_submseteq.
trans k1. done. by apply Permutation_submseteq.
- trans l2. by apply Permutation_submseteq.
trans k2. done. by apply Permutation_submseteq.
- trans l1; [by apply Permutation_submseteq|].
trans k1; [done|]. by apply Permutation_submseteq.
- trans l2; [by apply Permutation_submseteq|].
trans k2; [done|]. by apply Permutation_submseteq.
Qed.
Global Instance: AntiSymm () (@submseteq A).
Proof. red. auto using submseteq_Permutation_length_le, submseteq_length. Qed.
......@@ -2335,7 +2343,7 @@ Proof.
split.
- rewrite submseteq_sublist_l. intros (l'&Hl'&E).
rewrite sublist_app_l in Hl'. destruct Hl' as (k1&k2&?&?&?); subst.
exists k1, k2. split. done. eauto using sublist_submseteq.
exists k1, k2. split; [done|]. eauto using sublist_submseteq.
- intros (?&?&E&?&?). rewrite E. eauto using submseteq_app.
Qed.
Lemma submseteq_app_inv_l l1 l2 k : k ++ l1 + k ++ l2 l1 + l2.
......@@ -2491,7 +2499,7 @@ Section Forall_Exists.
Lemma Forall_cons_1 x l : Forall P (x :: l) P x Forall P l.
Proof. by inversion 1. Qed.
Lemma Forall_cons x l : Forall P (x :: l) P x Forall P l.
Proof. split. by inversion 1. intros [??]. by constructor. Qed.
Proof. split; [by inversion 1|]. intros [??]. by constructor. Qed.
Lemma Forall_singleton x : Forall P [x] P x.
Proof. rewrite Forall_cons, Forall_nil; tauto. Qed.
Lemma Forall_app_2 l1 l2 : Forall P l1 Forall P l2 Forall P (l1 ++ l2).
......@@ -2508,7 +2516,7 @@ Section Forall_Exists.
Proof. intros H ?. induction H; auto. Defined.
Lemma Forall_iff l (Q : A Prop) :
( x, P x Q x) Forall P l Forall Q l.
Proof. intros H. apply Forall_proper. red; apply H. done. Qed.
Proof. intros H. apply Forall_proper. { red; apply H. } done. Qed.
Lemma Forall_not l : length l 0 Forall (not P) l ¬Forall P l.
Proof. by destruct 2; inversion 1. Qed.
Lemma Forall_and {Q} l : Forall (λ x, P x Q x) l Forall P l Forall Q l.
......@@ -2631,7 +2639,7 @@ Section Forall_Exists.
split.
- induction 1 as [x|y ?? [x [??]]]; exists x; by repeat constructor.
- intros [x [Hin ?]]. induction l; [by destruct (not_elem_of_nil x)|].
inversion Hin; subst. by left. right; auto.
inversion Hin; subst; [left|right]; auto.
Qed.
Lemma Exists_inv x l : Exists P (x :: l) P x Exists P l.
Proof. inversion 1; intuition trivial. Qed.
......@@ -2690,9 +2698,17 @@ Section Forall_Exists.
End Forall_Exists.
Lemma forallb_True (f : A bool) xs : forallb f xs Forall f xs.
Proof. split. induction xs; naive_solver. induction 1; naive_solver. Qed.
Proof.
split.
- induction xs; naive_solver.
- induction 1; naive_solver.
Qed.
Lemma existb_True (f : A bool) xs : existsb f xs Exists f xs.
Proof. split. induction xs; naive_solver. induction 1; naive_solver. Qed.
Proof.
split.
- induction xs; naive_solver.
- induction 1; naive_solver.
Qed.
Lemma replicate_as_Forall (x : A) n l :
replicate n x = l length l = n Forall (x =.) l.
......@@ -3487,7 +3503,7 @@ Section fmap.
Proof.
induction l as [|y l IH]; simpl; inversion_clear 1.
- exists y. split; [done | by left].
- destruct IH as [z [??]]. done. exists z. split; [done | by right].
- destruct IH as [z [??]]; [done|]. exists z. split; [done | by right].
Qed.
Lemma elem_of_list_fmap l x : x f <$> l y, x = f y y l.
Proof.
......@@ -3664,7 +3680,7 @@ Section bind.
- induction l as [|y l IH]; csimpl; [inversion 1|].
rewrite elem_of_app. intros [?|?].
+ exists y. split; [done | by left].
+ destruct IH as [z [??]]. done. exists z. split; [done | by right].
+ destruct IH as [z [??]]; [done|]. exists z. split; [done | by right].
- intros [y [Hx Hy]]. induction Hy; csimpl; rewrite elem_of_app; intuition.
Qed.
Lemma Forall_bind (P : B Prop) l :
......@@ -3722,10 +3738,10 @@ Section mapM.
Lemma Forall2_mapM_ext (g : A option B) l k :
Forall2 (λ x y, f x = g y) l k mapM f l = mapM g k.
Proof. induction 1 as [|???? Hfg ? IH]; simpl. done. by rewrite Hfg, IH. Qed.
Proof. induction 1 as [|???? Hfg ? IH]; simpl; [done|]. by rewrite Hfg, IH. Qed.
Lemma Forall_mapM_ext (g : A option B) l :
Forall (λ x, f x = g x) l mapM f l = mapM g l.
Proof. induction 1 as [|?? Hfg ? IH]; simpl. done. by rewrite Hfg, IH. Qed.
Proof. induction 1 as [|?? Hfg ? IH]; simpl; [done|]. by rewrite Hfg, IH. Qed.
Lemma mapM_Some_1 l k : mapM f l = Some k Forall2 (λ x y, f x = Some y) l k.
Proof.
......
......@@ -41,5 +41,5 @@ Qed.
Global Instance listset_nodup_elems: Elements A C := listset_nodup_car.
Global Instance listset_nodup_fin_set: FinSet A C.
Proof. split. apply _. done. by intros [??]. Qed.
Proof. split; [apply _|done|]. by intros [??]. Qed.
End list_set.
......@@ -195,7 +195,7 @@ Lemma natmap_map_wf {A B} (f : A → B) l :
natmap_wf l natmap_wf (natmap_map_raw f l).
Proof.
unfold natmap_map_raw, natmap_wf. rewrite fmap_last.
destruct (last l). by apply fmap_is_Some. done.
destruct (last l); [|done]. by apply fmap_is_Some.
Qed.
Lemma natmap_lookup_map_raw {A B} (f : A B) i l :
mjoin (natmap_map_raw f l !! i) = f <$> mjoin (l !! i).
......@@ -215,8 +215,10 @@ Proof.
+ by specialize (E 0).
+ destruct (natmap_wf_lookup (None :: l2)) as (i&?&?); auto with congruence.
+ by specialize (E 0).
+ f_equal. apply (E 0). apply IH; eauto using natmap_wf_inv.
intros i. apply (E (S i)).
+ f_equal.
* apply (E 0).
* apply IH; eauto using natmap_wf_inv.
intros i. apply (E (S i)).
+ by specialize (E 0).
+ destruct (natmap_wf_lookup (None :: l1)) as (i&?&?); auto with congruence.
+ by specialize (E 0).
......
......@@ -53,7 +53,7 @@ Proof.
- intros ? f [? t] [|i]; simpl; [done |]. apply lookup_partial_alter.
- intros ? f [? t] [|i] [|j]; simpl; try intuition congruence.
intros. apply lookup_partial_alter_ne. congruence.
- intros ??? [??] []; simpl. done. apply lookup_fmap.
- intros ??? [??] []; simpl; [done|]. apply lookup_fmap.
- intros ? [[x|] t]; unfold map_to_list; simpl.
+ constructor.
* rewrite elem_of_list_fmap. by intros [[??] [??]].
......
......@@ -64,7 +64,7 @@ Instance nat_lt_pi: ∀ x y : nat, ProofIrrel (x < y).
Proof. unfold lt. apply _. Qed.
Lemma nat_le_sum (x y : nat) : x y z, y = x + z.
Proof. split. exists (y - x); lia. intros [z ->]; lia. Qed.
Proof. split; [exists (y - x); lia | intros [z ->]; lia]. Qed.
Lemma Nat_lt_succ_succ n : n < S (S n).
Proof. auto with arith. Qed.
......@@ -309,7 +309,7 @@ Proof. unfold N.lt. apply _. Qed.