From f92069a3ddddf551ac313d58dcf02abeb098069e Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Tue, 7 Nov 2017 14:50:20 -0500 Subject: Add evar_function_package --- src/Util/SideConditions/CorePackages.v | 24 ++++++++++++++++++++++++ 1 file changed, 24 insertions(+) (limited to 'src/Util/SideConditions') 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 (). -- cgit v1.2.3