Add `lrel_list_unfold` and simplify some proofs.

theories/lib/list.v

@@ -26,14 +26,37 @@ Definition nth : val := rec: "nth" "l" "n" :=
                  else "nth" (Snd "xs") ("n" - #1)
   end.
 
+Lemma lrel_list_unfold `{relocG Σ} A v1 v2:
+  lrel_list A v1 v2 ≡
+   (▷ ((⌜v1 = NILV⌝ ∧ ⌜v2 = NILV⌝)
+      ∨ (∃ w1 w2 t1 t2, ⌜v1 = CONSV w1 t1⌝ ∧
+                        ⌜v2 = CONSV w2 t2⌝ ∗
+                        A w1 w2 ∗ lrel_list A t1 t2)))%I.
+Proof.
+  rewrite /lrel_list.
+  rewrite {1}lrel_rec_unfold /=.
+  unfold lrel_rec1, lrel_car. (* TODO: so much unfolding *)
+  simpl. iSplit.
+  - iIntros "H". iNext.
+    iDestruct "H" as (w1 w2) "H".
+    iDestruct "H" as "[(->&->&H)|(->&->&H)]".
+    + iLeft. iDestruct "H" as "[-> ->]". done.
+    + iRight. iDestruct "H" as (????->->) "[??]".
+      iExists _,_,_,_. repeat iSplit; eauto.
+  - iIntros "H". iNext.
+    iDestruct "H" as "[[-> ->]|H]".
+    + iExists #(),#(). iLeft. eauto with iFrame.
+    + iDestruct "H" as (????->->) "[??]".
+      iExists (_,_)%V,(_,_)%V. iRight.
+      repeat iSplit; eauto with iFrame.
+      iExists _,_,_,_. repeat iSplit; eauto with iFrame.
+Qed.
+
 Lemma lrel_list_nil `{relocG Σ} A :
   lrel_list A NILV NILV.
 Proof.
-  unfold lrel_list.
-  rewrite lrel_rec_unfold /=.
-  unfold lrel_rec1 , lrel_car. (* TODO so much unfolding *)
-  simpl. iNext.
-  iExists _,_. iLeft. repeat iSplit; eauto.
+  rewrite lrel_list_unfold.
+  iNext. by iLeft.
 Qed.
 
 Lemma lrel_list_cons `{relocG Σ} (A : lrel Σ) v1 v2 ls1 ls2 :
@@ -42,12 +65,8 @@ Lemma lrel_list_cons `{relocG Σ} (A : lrel Σ) v1 v2 ls1 ls2 :
   lrel_list A (CONSV v1 ls1) (CONSV v2 ls2).
 Proof.
   iIntros "#HA #Hls".
-  rewrite {2}/lrel_list lrel_rec_unfold /=.
-  rewrite /lrel_rec1 {3}/lrel_car.
-  iNext. simpl. iExists _, _.
-  iRight. repeat iSplit; eauto.
-  rewrite {1}/lrel_prod /lrel_car /=.
-  iExists _,_,_,_. repeat iSplit; eauto.
+  rewrite (lrel_list_unfold A (CONSV _ _)).
+  iNext. iRight. iExists _,_,_,_. eauto with iFrame.
 Qed.
 
 Lemma refines_nth_l `{relocG Σ} (A : lrel Σ) K v w ls (n: nat) t :
@@ -97,3 +116,4 @@ Qed.
 Lemma nth_int_typed `{relocG Σ} :
   REL nth << nth : lrel_list lrel_int → lrel_int → lrel_int.
 Proof. admit. Admitted.
+(* XXX derive this from the fundamental property *)