From e6582563fe7d89c0f91dfbac5da491cd8c39fcf5 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Th=C3=A9ophile=20Wallez?= <theophile@wallez.net>
Date: Fri, 6 Sep 2024 23:39:17 +0200
Subject: [PATCH] fix: use more precise types for `move_requires_*`

and add `move_requires_4`
---
 ulib/FStar.Classical.fst  |  2 ++
 ulib/FStar.Classical.fsti | 35 ++++++++++++++++++++++++++---------
 2 files changed, 28 insertions(+), 9 deletions(-)

diff --git a/ulib/FStar.Classical.fst b/ulib/FStar.Classical.fst
index 8b0fc19fdc0..dc7197a0995 100644
--- a/ulib/FStar.Classical.fst
+++ b/ulib/FStar.Classical.fst
@@ -65,6 +65,8 @@ let move_requires_2 #a #b #p #q f x y = move_requires (f x) y
 
 let move_requires_3 #a #b #c #p #q f x y z = move_requires (f x y) z
 
+let move_requires_4 #a #b #c #d #p #q f x y z w = move_requires (f x y z) w
+
 // Thanks KM, CH and SZ
 let impl_intro_gen #p #q f =
   let g () : Lemma (requires p) (ensures (p ==> q ())) = give_proof #(q ()) (f (get_proof p)) in
diff --git a/ulib/FStar.Classical.fsti b/ulib/FStar.Classical.fsti
index 7c42531e6dc..e58b28d8b03 100644
--- a/ulib/FStar.Classical.fsti
+++ b/ulib/FStar.Classical.fsti
@@ -84,23 +84,40 @@ val move_requires
 
 (** The arity 2 version of [move_requires] *)
 val move_requires_2
-      (#a #b: Type)
-      (#p #q: (a -> b -> Type))
-      ($_: (x: a -> y: b -> Lemma (requires (p x y)) (ensures (q x y))))
+      (#a: Type)
+      (#b: (a -> Type))
+      (#p #q: (x: a -> b x -> Type))
+      ($_: (x: a -> y: b x -> Lemma (requires (p x y)) (ensures (q x y))))
       (x: a)
-      (y: b)
+      (y: b x)
     : Lemma (p x y ==> q x y)
 
 (** The arity 3 version of [move_requires] *)
 val move_requires_3
-      (#a #b #c: Type)
-      (#p #q: (a -> b -> c -> Type))
-      ($_: (x: a -> y: b -> z: c -> Lemma (requires (p x y z)) (ensures (q x y z))))
+      (#a: Type)
+      (#b: (a -> Type))
+      (#c: (x: a -> y: b x -> Type))
+      (#p #q: (x: a -> y: b x -> c x y -> Type))
+      ($_: (x: a -> y: b x -> z: c x y -> Lemma (requires (p x y z)) (ensures (q x y z))))
       (x: a)
-      (y: b)
-      (z: c)
+      (y: b x)
+      (z: c x y)
     : Lemma (p x y z ==> q x y z)
 
+(** The arity 4 version of [move_requires] *)
+val move_requires_4
+      (#a: Type)
+      (#b: (a -> Type))
+      (#c: (x: a -> y: b x -> Type))
+      (#d: (x: a -> y: b x -> z: c x y -> Type))
+      (#p #q: (x: a -> y: b x -> z: c x y -> w: d x y z -> Type))
+      ($_: (x: a -> y: b x -> z: c x y -> w: d x y z -> Lemma (requires (p x y z w)) (ensures (q x y z w))))
+      (x: a)
+      (y: b x)
+      (z: c x y)
+      (w: d x y z)
+    : Lemma (p x y z w ==> q x y z w)
+
 (** When proving predicate [q] whose well-formedness depends on the
     predicate [p], it is convenient to have [q] appear only under a
     context where [p] is know to be valid. *)