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

Merge branch 'big_sepL-inv' into 'master'

Add big_sepL2_nil_inv_l/r.

See merge request !442
parents 976b02f6 b31d8c00
Pipeline #28164 passed with stage
in 21 minutes and 4 seconds
...@@ -292,6 +292,12 @@ Section sep_list2. ...@@ -292,6 +292,12 @@ Section sep_list2.
Proof. done. Qed. Proof. done. Qed.
Lemma big_sepL2_nil' `{BiAffine PROP} P Φ : P [ list] ky1;y2 [];[], Φ k y1 y2. Lemma big_sepL2_nil' `{BiAffine PROP} P Φ : P [ list] ky1;y2 [];[], Φ k y1 y2.
Proof. apply (affine _). Qed. Proof. apply (affine _). Qed.
Lemma big_sepL2_nil_inv_l Φ l2 :
([ list] ky1;y2 []; l2, Φ k y1 y2) - l2 = [].
Proof. destruct l2; simpl; auto using False_elim, pure_intro. Qed.
Lemma big_sepL2_nil_inv_r Φ l1 :
([ list] ky1;y2 l1; [], Φ k y1 y2) - l1 = [].
Proof. destruct l1; simpl; auto using False_elim, pure_intro. Qed.
Lemma big_sepL2_cons Φ x1 x2 l1 l2 : Lemma big_sepL2_cons Φ x1 x2 l1 l2 :
([ list] ky1;y2 x1 :: l1; x2 :: l2, Φ k y1 y2) ([ list] ky1;y2 x1 :: l1; x2 :: l2, Φ k y1 y2)
......
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