Add evar_function_package

1 files changed, 24 insertions, 0 deletions

diff --git a/src/Util/SideConditions/CorePackages.v b/src/Util/SideConditions/CorePackages.v
index 19612df0a..8126c5280 100644
--- a/src/Util/SideConditions/CorePackages.v
+++ b/src/Util/SideConditions/CorePackages.v
@@ -5,6 +5,13 @@ Record evar_package {T} (v : T) :=
     evar_package_pf : val = v }.
 Arguments val {T v} _.
 Arguments evar_package_pf {T v} _.
+
+Record evar_function_package {A B} (f : forall x : A, B x) :=
+  { valf : forall x : A, B x;
+    evarf_package_pf : forall x, valf x = f x }.
+Arguments valf {A B f} _.
+Arguments evarf_package_pf {A B f} _ _.
+
 Record evard_package {s d} (v : s) :=
   { vald : d;
     evard_package_pfT : s = d;
@@ -13,4 +20,21 @@ Arguments vald {s d v} _.
 Arguments evard_package_pfT {s d v} _.
 Arguments evard_package_pf {s d v} _.
 
+Local Notation "'rew' 'dependent' H 'in' H'"
+  := (match H with
+      | eq_refl => H'
+      end)
+       (at level 10, H' at level 10,
+        format "'[' 'rew'  'dependent'  '/    ' H  in  '/' H' ']'").
+
+Record evard_function_package {sA sB dA dB} (f : forall x : sA, sB x) :=
+  { valdf : forall x : dA, dB x;
+    evardf_package_pfTA : dA = sA;
+    evardf_package_pfTB : forall x, sB (rew evardf_package_pfTA in x) = dB x;
+    evardf_package_pf : forall x, valdf x = rew dependent evardf_package_pfTB x in (f (rew evardf_package_pfTA in x)) }.
+Arguments valdf {sA sB dA dB f} _ _.
+Arguments evardf_package_pfTA {sA sB dA dB f} _.
+Arguments evardf_package_pfTB {sA sB dA dB f} _.
+Arguments evardf_package_pf {sA sB dA dB f} _ _.
+
 Ltac autosolve else_tac := else_tac ().