From 18bb966497600b992bc53e94c41766ff06cb053e Mon Sep 17 00:00:00 2001
From: Jacques-Henri Jourdan <jacques-henri.jourdan@normalesup.org>
Date: Fri, 11 Nov 2016 00:43:24 +0100
Subject: [PATCH] Add Hint Extern for Is_true/ty_dup. Make product simpl never
 (but that does not work in many cases).

---
 theories/perm.v   | 2 ++
 theories/type.v   | 3 ++-
 theories/typing.v | 2 +-
 3 files changed, 5 insertions(+), 2 deletions(-)

diff --git a/theories/perm.v b/theories/perm.v
index 52f9eb2e..ff983766 100644
--- a/theories/perm.v
+++ b/theories/perm.v
@@ -91,6 +91,8 @@ Section duplicable.
 
 End duplicable.
 
+Hint Extern 0 (Is_true _.(ty_dup)) => exact I.
+
 Section has_type.
 
   Context `{iris_typeG Σ}.
diff --git a/theories/type.v b/theories/type.v
index 0e93d48f..ab514846 100644
--- a/theories/type.v
+++ b/theories/type.v
@@ -340,7 +340,7 @@ Section types.
       iMod ("Hclose2" with "[H2 H↦2]") as "[$$]". by iExists _; iFrame. done.
   Qed.
 
-  Definition product (tyl : list type) := fold_right product2 unit tyl.
+  Definition product := fold_right product2 unit.
 
   Lemma split_sum_mt l tid q tyl :
     (l ↦∗{q}: λ vl,
@@ -475,6 +475,7 @@ Notation "&uniq{ κ } ty" := (uniq_borrow κ ty)
 Notation "&shr{ κ } ty" := (shared_borrow κ ty)
   (format "&shr{ κ } ty", at level 20, right associativity) : lrust_type_scope.
 
+Arguments product : simpl never.
 Notation Π := product.
 (* Σ is commonly used for the current functor. So it cannot be defined
    as Π for products. We stick to the following form. *)
diff --git a/theories/typing.v b/theories/typing.v
index f797361a..c78fec77 100644
--- a/theories/typing.v
+++ b/theories/typing.v
@@ -209,7 +209,7 @@ Section typing.
       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. simpl in *. congruence.
+      clear. induction ty.(ty_size). done. by apply (f_equal S).
   Qed.
 
   Lemma consumes_copy_uniq_borrow ty κ κ' q:
-- 
GitLab