From 305070153c8730ac847e49e418faedc963db61f0 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Tue, 7 Aug 2018 21:44:19 -0400 Subject: Add lemmas about type.and_for_each_lhs_of_arrow --- src/Experiments/NewPipeline/LanguageWf.v | 34 ++++++++++++++++++++++++++++++++ 1 file changed, 34 insertions(+) (limited to 'src') diff --git a/src/Experiments/NewPipeline/LanguageWf.v b/src/Experiments/NewPipeline/LanguageWf.v index 10fe64306..19477a8c6 100644 --- a/src/Experiments/NewPipeline/LanguageWf.v +++ b/src/Experiments/NewPipeline/LanguageWf.v @@ -10,6 +10,7 @@ Require Import Crypto.Util.Tactics.DestructHead. Require Import Crypto.Util.Tactics.UniquePose. Require Import Crypto.Util.Tactics.SpecializeAllWays. Require Import Crypto.Util.Tactics.RewriteHyp. +Require Import Crypto.Util.Tactics.SplitInContext. Require Import Crypto.Util.Option. Require Import Crypto.Util.NatUtil. Require Import Crypto.Util.Sigma. @@ -102,6 +103,39 @@ Hint Extern 10 (Proper ?R ?x) => simple eapply (@PER_valid_r _ R); [ | | solve [ end. eauto. Qed. + + Lemma andb_bool_impl_and_for_each_lhs_of_arrow {base_type} {f g : type base_type -> Type} + (R : forall t, f t -> g t -> bool) + (R' : forall t, f t -> g t -> Prop) + (HR : forall t x y, R t x y = true -> R' t x y) + {t} x y + : @type.andb_bool_for_each_lhs_of_arrow base_type f g R t x y = true + -> @type.and_for_each_lhs_of_arrow base_type f g R' t x y. + Proof. + induction t; cbn in *; rewrite ?Bool.andb_true_iff; destruct_head'_prod; cbn [fst snd]; intuition. + Qed. + + Lemma and_impl_andb_bool_for_each_lhs_of_arrow {base_type} {f g : type base_type -> Type} + (R : forall t, f t -> g t -> bool) + (R' : forall t, f t -> g t -> Prop) + (HR : forall t x y, R' t x y -> R t x y = true) + {t} x y + : @type.and_for_each_lhs_of_arrow base_type f g R' t x y + -> @type.andb_bool_for_each_lhs_of_arrow base_type f g R t x y = true. + Proof. + induction t; cbn in *; rewrite ?Bool.andb_true_iff; destruct_head'_prod; cbn [fst snd]; intuition. + Qed. + + Lemma andb_bool_iff_and_for_each_lhs_of_arrow {base_type} {f g : type base_type -> Type} + (R : forall t, f t -> g t -> bool) + (R' : forall t, f t -> g t -> Prop) + (HR : forall t x y, R t x y = true <-> R' t x y) + {t} x y + : @type.andb_bool_for_each_lhs_of_arrow base_type f g R t x y = true + <-> @type.and_for_each_lhs_of_arrow base_type f g R' t x y. + Proof. + induction t; cbn in *; rewrite ?Bool.andb_true_iff; destruct_head'_prod; cbn [fst snd]; split_iff; intuition. + Qed. End type. Module ident. -- cgit v1.2.3