From ed53a28ea315782980198a63a14b2acc6d4d5759 Mon Sep 17 00:00:00 2001 From: jadep Date: Sun, 26 Feb 2017 14:16:02 -0500 Subject: Modified lemma and created tactic to handle it; added reduce step to multiplication operation; introduced modular equality to NewBaseSystem --- src/Util/Sigma.v | 17 +++++++++-------- 1 file changed, 9 insertions(+), 8 deletions(-) (limited to 'src/Util/Sigma.v') diff --git a/src/Util/Sigma.v b/src/Util/Sigma.v index 7a1d0cacb..2f7719ab8 100644 --- a/src/Util/Sigma.v +++ b/src/Util/Sigma.v @@ -16,14 +16,6 @@ Local Arguments f_equal {_ _} _ {_ _} _. (** ** Equality for [sigT] *) Section sigT. - (* Lift foralls out of sigT proofs and leave a sig goal *) - Definition lift2_sig {R S T} f (g:R->S) - (X : forall a b, {prod | g prod = f a b}) : - { op : T -> T -> R & forall a b, g (op a b) = f a b }. - Proof. - exists (fun a b => proj1_sig (X a b)). - exact (fun a b => proj2_sig (X a b)). - Defined. (** *** Projecting an equality of a pair to equality of the first components *) Definition pr1_path {A} {P : A -> Type} {u v : sigT P} (p : u = v) @@ -209,6 +201,15 @@ Section ex. Defined. End ex. +(* Lift foralls out of sig proofs *) +Definition lift2_sig {A B C} (P:A->B->C->Prop) + (op_sig : forall (a:A) (b:B), {c | P a b c}) : + { op : A -> B -> C | forall (a:A) (b:B), P a b (op a b) } + := exist + (fun op => forall a b, P a b (op a b)) + (fun a b => proj1_sig (op_sig a b)) + (fun a b => proj2_sig (op_sig a b)). + (** ** Useful Tactics *) (** *** [inversion_sigma] *) (** The built-in [inversion] will frequently leave equalities of -- cgit v1.2.3