Commit 0cdad2cb authored by Robbert Krebbers's avatar Robbert Krebbers

Merge branch 'big_sepL2_app_inv_2' into 'master'

Add `big_sepL2_app_inv_2`.

See merge request !292
parents cd8f3be9 2a4e4330
Pipeline #18408 passed with stage
in 19 minutes and 28 seconds
......@@ -335,6 +335,16 @@ Section sep_list2.
[by rewrite left_id|by rewrite left_id|apply False_elim|].
by rewrite IH -assoc.
Lemma big_sepL2_app_inv Φ l1 l2 l1' l2' :
length l1 = length l1'
([ list] ky1;y2 l1 ++ l2; l1' ++ l2', Φ k y1 y2) -
([ list] ky1;y2 l1; l1', Φ k y1 y2)
([ list] ky1;y2 l2; l2', Φ (length l1 + k)%nat y1 y2).
revert Φ l1'. induction l1 as [|x1 l1 IH]=> Φ -[|x1' l1'] //= ?; simplify_eq.
- by rewrite left_id.
- by rewrite -assoc IH.
Lemma big_sepL2_mono Φ Ψ l1 l2 :
( k y1 y2, l1 !! k = Some y1 l2 !! k = Some y2 Φ k y1 y2 Ψ 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