From 375fa6522a9685d3a217123ebb3a8c4b13eff5b8 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Thu, 18 Apr 2019 16:43:30 -0400 Subject: Add Primitive.reflect_eq_prod --- src/Util/Bool/Reflect.v | 8 ++++++++ 1 file changed, 8 insertions(+) (limited to 'src/Util') diff --git a/src/Util/Bool/Reflect.v b/src/Util/Bool/Reflect.v index d4a0df069..7fac6d11a 100644 --- a/src/Util/Bool/Reflect.v +++ b/src/Util/Bool/Reflect.v @@ -13,6 +13,7 @@ Require Import Crypto.Util.ListUtil. Require Import Crypto.Util.Sum. Require Import Crypto.Util.Comparison. Require Import Crypto.Util.Tactics.DestructHead. +Require Crypto.Util.PrimitiveProd. Lemma reflect_to_dec_iff {P b1 b2} : reflect P b1 -> (b1 = b2) <-> (if b2 then P else ~P). Proof. @@ -136,6 +137,7 @@ Hint Constructors reflect : typeclass_instances. Local Hint Resolve -> Bool.eqb_true_iff : core. Local Hint Resolve <- Bool.eqb_true_iff : core. Local Hint Resolve internal_prod_dec_bl internal_prod_dec_lb + PrimitiveProd.Primitive.prod_dec_bl PrimitiveProd.Primitive.prod_dec_lb internal_option_dec_bl internal_option_dec_lb internal_list_dec_bl internal_list_dec_lb internal_sum_dec_bl internal_sum_dec_lb @@ -178,6 +180,12 @@ Global Instance reflect_eq_sigT_hprop {A P eqA} `{reflect_rel (@eq A) eqA, foral Global Instance reflect_eq_sig_hprop {A eqA} {P : A -> Prop} `{reflect_rel (@eq A) eqA, forall a : A, IsHProp (P a)} : reflect_rel (@eq (@sig A P)) (sig_beq eqA (fun _ _ _ _ => true)) | 10. exact _. Qed. Global Instance reflect_eq_comparison : reflect_rel (@eq comparison) comparison_beq | 10. exact _. Qed. +Module Export Primitive. + Import PrimitiveProd. + Import PrimitiveProd.Primitive. + Global Instance reflect_eq_prod {A B eqA eqB} `{reflect_rel (@eq A) eqA, reflect_rel (@eq B) eqB} : reflect_rel (@eq (A * B)) (@Primitive.prod_beq A B eqA eqB) | 10. exact _. Qed. +End Primitive. + Module Nat. Definition geb_spec0 : reflect_rel ge (fun x y => Nat.leb y x) := fun _ _ => Nat.leb_spec0 _ _. Definition gtb_spec0 : reflect_rel gt (fun x y => Nat.ltb y x) := fun _ _ => Nat.ltb_spec0 _ _. -- cgit v1.2.3