Commit 4ecef793 authored by Ralf Jung's avatar Ralf Jung
Browse files

simplify proofs

parent 8e0fae21
...@@ -188,9 +188,8 @@ Section sep_list. ...@@ -188,9 +188,8 @@ Section sep_list.
rewrite big_sepL_snoc // IH sep_and -pure_and. rewrite big_sepL_snoc // IH sep_and -pure_and.
f_equiv=>-[Hl Hx] k y /lookup_app_Some =>-[Hy|[Hlen Hy]]. f_equiv=>-[Hl Hx] k y /lookup_app_Some =>-[Hy|[Hlen Hy]].
- by apply Hl. - by apply Hl.
- replace k with (length l) in Hy |- *; last first. - apply list_lookup_singleton_Some in Hy as [Hk ->].
{ apply lookup_lt_Some in Hy. simpl in Hy. lia. } replace k with (length l) by lia. done.
rewrite Nat.sub_diag /= in Hy. injection Hy as [= ->]. done.
Qed. Qed.
Lemma big_sepL_affinely_pure_2 (φ : nat A Prop) l : Lemma big_sepL_affinely_pure_2 (φ : nat A Prop) l :
<affine> k x, l !! k = Some x φ k x @{PROP} ([ list] kx l, <affine> ⌜φ k x). <affine> k x, l !! k = Some x φ k x @{PROP} ([ list] kx l, <affine> ⌜φ k x).
...@@ -964,9 +963,8 @@ Section and_list. ...@@ -964,9 +963,8 @@ Section and_list.
rewrite big_andL_snoc // IH -pure_and. rewrite big_andL_snoc // IH -pure_and.
f_equiv=>-[Hl Hx] k y /lookup_app_Some =>-[Hy|[Hlen Hy]]. f_equiv=>-[Hl Hx] k y /lookup_app_Some =>-[Hy|[Hlen Hy]].
- by apply Hl. - by apply Hl.
- replace k with (length l) in Hy |- *; last first. - apply list_lookup_singleton_Some in Hy as [Hk ->].
{ apply lookup_lt_Some in Hy. simpl in Hy. lia. } replace k with (length l) by lia. done.
rewrite Nat.sub_diag /= in Hy. injection Hy as [= ->]. done.
Qed. Qed.
Lemma big_andL_pure_2 (φ : nat A Prop) l : Lemma big_andL_pure_2 (φ : nat A Prop) l :
k x, l !! k = Some x φ k x @{PROP} ([ list] kx l, ⌜φ k x). k x, l !! k = Some x φ k x @{PROP} ([ list] kx l, ⌜φ k x).
......
Supports Markdown
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