From 07c7a553377bb0cd4f5cff945886ef6690bb98da Mon Sep 17 00:00:00 2001
From: Jacques-Henri Jourdan <jacques-henri.jourdan@normalesup.org>
Date: Wed, 14 Dec 2016 10:10:00 +0100
Subject: [PATCH] uninit : a few lemmas, a proper file.

---
 _CoqProject               |  1 +
 theories/typing/own.v     | 20 +++++---------------
 theories/typing/product.v |  5 ++---
 theories/typing/uninit.v  | 24 ++++++++++++++++++++++++
 4 files changed, 32 insertions(+), 18 deletions(-)
 create mode 100644 theories/typing/uninit.v

diff --git a/_CoqProject b/_CoqProject
index 49f8db42..d1abaecb 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -30,6 +30,7 @@ theories/typing/typing.v
 theories/typing/lft_contexts.v
 theories/typing/type_context.v
 theories/typing/cont_context.v
+theories/typing/uninit.v
 theories/typing/own.v
 theories/typing/uniq_bor.v
 theories/typing/shr_bor.v
diff --git a/theories/typing/own.v b/theories/typing/own.v
index 273b45f5..3b6ad333 100644
--- a/theories/typing/own.v
+++ b/theories/typing/own.v
@@ -4,17 +4,11 @@ From lrust.lifetime Require Import borrow frac_borrow.
 From lrust.lang Require Export new_delete.
 From lrust.lang Require Import heap.
 From lrust.typing Require Export type.
-From lrust.typing Require Import typing product perm.
+From lrust.typing Require Import typing product perm uninit.
 
 Section own.
   Context `{typeG Σ}.
 
-  (* Even though it does not seem too natural to put this here, it is
-     the only place where it is used. *)
-  Program Definition uninit : type :=
-    {| st_own tid vl := ⌜length vl = 1%nat⌝%I |}.
-  Next Obligation. done. Qed.
-
   Program Definition freeable_sz (n : nat) (sz : nat) (l : loc) : iProp Σ :=
     match sz, n return _ with
     | 0%nat, _ => True
@@ -122,7 +116,7 @@ Section own.
   Proof. intros ?? Heq. split; f_equiv; apply Heq. Qed.
 
   Lemma typed_new ρ (n : nat):
-    0 ≤ n → typed_step_ty ρ (new [ #n]%E) (own n (Π(replicate n uninit))).
+    0 ≤ n → typed_step_ty ρ (new [ #n]%E) (own n (uninit n)).
   Proof.
     iIntros (Hn tid) "!#(#HEAP&_&_&$)". iApply (wp_new with "HEAP"); try done.
     iIntros "!>*(% & H† & H↦)". iExists _. iSplit. done. iNext.
@@ -132,9 +126,7 @@ Section own.
       clear Hn. apply (inj Z.of_nat) in Hlen. subst.
       iInduction vl as [|v vl] "IH". done.
       iExists [v], vl. iSplit. done. by iSplit.
-    - assert (ty_size (Π (replicate n uninit)) = n) as ->.
-      { clear. induction n; rewrite //= IHn //. }
-      by rewrite freeable_sz_full.
+    - by rewrite uninit_sz freeable_sz_full.
   Qed.
 
   Lemma typed_delete ty (ν : expr):
@@ -177,8 +169,7 @@ Section own.
   Qed.
 
   Lemma consumes_move ty n:
-    consumes ty (λ ν, ν ◁ own n ty)%P
-             (λ ν, ν ◁ own n (Π(replicate ty.(ty_size) uninit)))%P.
+    consumes ty (λ ν, ν ◁ own n ty)%P (λ ν, ν ◁ own n (uninit ty.(ty_size)))%P.
   Proof.
     iIntros (ν tid Φ E ?) "_ H◁ Htl HΦ". iApply (has_type_wp with "H◁").
     iIntros (v) "Hνv H◁". iDestruct "Hνv" as %Hνv.
@@ -191,7 +182,6 @@ Section own.
     - rewrite -Hlen. iExists vl. iIntros "{$H↦}!>". clear.
       iInduction vl as [|v vl] "IH". done.
       iExists [v], vl. iSplit. done. by iSplit.
-    - assert (ty_size (Π (replicate (ty_size ty) uninit)) = ty_size ty) as ->; last by auto.
-      clear. induction ty.(ty_size). done. by apply (f_equal S).
+    - rewrite uninit_sz; auto.
   Qed.
 End own.
diff --git a/theories/typing/product.v b/theories/typing/product.v
index ba655e51..5efbb086 100644
--- a/theories/typing/product.v
+++ b/theories/typing/product.v
@@ -117,8 +117,7 @@ Section product.
       iMod ("Hclose2" with "[H2 H↦2]") as "[$$]". by iExists _; iFrame. done.
   Qed.
 
-  Definition product := fold_right product2 unit.
-
+  Definition product := foldr product2 unit.
   (* Given that in practice, product will be used with concrete lists,
      there should be no need to declare [Copy] and [Proper] instances
      for [product]. *)
@@ -169,7 +168,7 @@ Section typing.
     - iExists F, ∅. iFrame. by iPureIntro; set_solver.
   Qed.
 
-  Lemma subtype_prod_flatten E L tyl1 tyl2 tyl3 :
+  Lemma eqtype_prod_flatten E L tyl1 tyl2 tyl3 :
     eqtype E L (Π(tyl1 ++ Π tyl2 :: tyl3)) (Π(tyl1 ++ tyl2 ++ tyl3)).
   Proof.
     unfold product. induction tyl1; simpl; last by f_equiv.
diff --git a/theories/typing/uninit.v b/theories/typing/uninit.v
new file mode 100644
index 00000000..7fc9fa0e
--- /dev/null
+++ b/theories/typing/uninit.v
@@ -0,0 +1,24 @@
+From lrust.typing Require Export type.
+From lrust.typing Require Import product.
+
+Section uninit.
+  Context `{typeG Σ}.
+
+  Program Definition uninit_1 : type :=
+    {| st_own tid vl := ⌜length vl = 1%nat⌝%I |}.
+  Next Obligation. done. Qed.
+
+  Definition uninit (n : nat) : type :=
+    Π (replicate n uninit_1).
+
+  Lemma eqtype_uninit_product E L ns :
+    eqtype E L (uninit (foldr plus 0%nat ns)) (Π(uninit <$> ns)).
+  Proof.
+    induction ns as [|n ns IH]. done.
+    rewrite /= /uninit replicate_plus (eqtype_prod_flatten E L []).
+    induction n. done. rewrite /product /=. by f_equiv.
+  Qed.
+
+  Lemma uninit_sz n : ty_size (uninit n) = n.
+  Proof. induction n. done. simpl. by f_equal. Qed.
+End uninit.
\ No newline at end of file
-- 
GitLab