Commit 9e6ebe60 authored by Robbert Krebbers's avatar Robbert Krebbers

Remove some useless Absorbing/Affine constraints for `big_andL`.

parent 25d8d958
......@@ -489,7 +489,7 @@ Section and_list.
Proper (Forall2 () ==> ()) (big_opL (@bi_and PROP) (λ _ P, P)).
Proof. by induction 1 as [|P Q Ps Qs HPQ ? IH]; rewrite /= ?HPQ ?IH. Qed.
Lemma big_andL_lookup Φ l i x `{!Absorbing (Φ i x)} :
Lemma big_andL_lookup Φ l i x :
l !! i = Some x ([ list] ky l, Φ k y) Φ i x.
Proof.
intros. rewrite -(take_drop_middle l i x) // big_andL_app /=.
......@@ -497,7 +497,7 @@ Section and_list.
eauto using lookup_lt_Some, Nat.lt_le_incl, and_elim_l', and_elim_r'.
Qed.
Lemma big_andL_elem_of (Φ : A PROP) l x `{!Absorbing (Φ x)} :
Lemma big_andL_elem_of (Φ : A PROP) l x :
x l ([ list] y l, Φ y) Φ x.
Proof.
intros [i ?]%elem_of_list_lookup; eauto using (big_andL_lookup (λ _, Φ)).
......@@ -521,7 +521,7 @@ Section and_list.
<pers> ([ list] kx l, Φ k x) [ list] kx l, <pers> (Φ k x).
Proof. apply (big_opL_commute _). Qed.
Lemma big_andL_forall `{BiAffine PROP} Φ l :
Lemma big_andL_forall Φ l :
([ list] kx l, Φ k x) ( k x, l !! k = Some x Φ k x).
Proof.
apply (anti_symm _).
......
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