diff options
author | Jason Gross <jgross@mit.edu> | 2018-09-27 17:21:10 -0400 |
---|---|---|
committer | Jason Gross <jgross@mit.edu> | 2018-09-27 17:21:10 -0400 |
commit | c33a4250e81e47245b83f8793710d6270c2a1c58 (patch) | |
tree | 73a9bac05a6d7a552834e6d5b3af0747216bb427 /src | |
parent | 1bb26e27d97aa102a94751047b309da4b2f75a67 (diff) |
Clean up type_beq_to_eq a bit
Diffstat (limited to 'src')
-rw-r--r-- | src/Experiments/NewPipeline/LanguageInversion.v | 45 |
1 files changed, 13 insertions, 32 deletions
diff --git a/src/Experiments/NewPipeline/LanguageInversion.v b/src/Experiments/NewPipeline/LanguageInversion.v index 962cabcea..eb67f5355 100644 --- a/src/Experiments/NewPipeline/LanguageInversion.v +++ b/src/Experiments/NewPipeline/LanguageInversion.v @@ -8,6 +8,7 @@ Require Import Crypto.Util.HProp. Require Import Crypto.Util.Decidable. Require Import Crypto.Util.Option. Require Import Crypto.Util.Bool. +Require Import Crypto.Util.Bool.Reflect. Require Import Crypto.Util.CPSNotations. Require Import Crypto.Util.Notations. Require Import Crypto.Util.FixCoqMistakes. @@ -99,13 +100,9 @@ Module Compilers. | progress break_innermost_match | progress eliminate_hprop_eq | congruence + | progress Reflect.beq_to_eq base.type.type_beq base.type.internal_type_dec_bl base.type.internal_type_dec_lb + | progress Reflect.beq_to_eq base.type.base_beq base.type.internal_base_dec_bl base.type.internal_base_dec_lb | match goal with - | [ H : base.type.type_beq _ _ = true |- _ ] => apply base.type.internal_type_dec_bl in H; auto - | [ H : context[base.type.type_beq ?x ?x] |- _ ] => rewrite base.type.internal_type_dec_lb in H by auto - | [ |- context[base.type.internal_type_dec_bl ?x ?y ?pf] ] => generalize (base.type.internal_type_dec_bl x y pf); intro - | [ H : base.type.base_beq _ _ = true |- _ ] => apply base.type.internal_base_dec_bl in H; auto - | [ H : context[base.type.base_beq ?x ?x] |- _ ] => rewrite base.type.internal_base_dec_lb in H by auto - | [ |- context[base.type.internal_base_dec_bl ?x ?y ?pf] ] => generalize (base.type.internal_base_dec_bl x y pf); intro | [ H : _ |- _ ] => rewrite H end ]. @@ -146,6 +143,7 @@ Module Compilers. | right _ => None end. Proof. cbv [base.try_transport]; rewrite try_transport_cps_correct; reflexivity. Qed. + End base. Module type. @@ -306,32 +304,15 @@ Module Compilers. := type.type_eq_dec _ base.type.type_beq base.type.internal_type_dec_bl base.type.internal_type_dec_lb. Ltac type_beq_to_eq := - repeat match goal with - | [ H : type.type_beq _ _ _ _ = true |- _ ] - => apply type.internal_type_dec_bl in H; [ | apply base.type.internal_type_dec_bl ] - | [ H : context[type.type_beq _ _ ?x ?x] |- _ ] - => rewrite type.internal_type_dec_lb in H by (reflexivity || exact base.type.internal_type_dec_lb) - | [ H : type.type_beq _ _ ?x ?y = true |- _ ] - => generalize dependent (type.internal_type_dec_bl _ _ base.type.internal_type_dec_bl _ _ H); clear H; intros - | [ |- type.type_beq _ _ _ _ = true ] - => apply type.internal_type_dec_lb; [ apply base.type.internal_type_dec_lb | ] - | [ H : base.type.type_beq _ _ = true |- _ ] - => apply base.type.internal_type_dec_bl in H - | [ H : context[base.type.type_beq ?x ?x] |- _ ] - => rewrite base.type.internal_type_dec_lb in H by reflexivity - | [ H : base.type.type_beq ?x ?y = true |- _ ] - => generalize dependent (base.type.internal_type_dec_bl _ _ H); clear H; intros - | [ |- base.type.type_beq _ _ = true ] - => apply base.type.internal_type_dec_lb - | [ H : base.type.type_beq _ _ = true |- _ ] - => apply base.type.internal_base_dec_bl in H - | [ H : context[base.type.base_beq ?x ?x] |- _ ] - => rewrite base.type.internal_base_dec_lb in H by reflexivity - | [ H : base.type.base_beq ?x ?y = true |- _ ] - => generalize dependent (base.type.internal_base_dec_bl _ _ H); clear H; intros - | [ |- base.type.base_beq _ _ = true ] - => apply base.type.internal_base_dec_lb - end. + repeat first [ progress Reflect.beq_to_eq base.type.base_beq base.type.internal_base_dec_bl base.type.internal_base_dec_lb + | progress Reflect.beq_to_eq base.type.type_beq base.type.internal_type_dec_bl base.type.internal_type_dec_lb + | progress Reflect.beq_to_eq + (@type.type_beq base.type base.type.type_beq) + (@type.internal_type_dec_bl base.type base.type.type_beq base.type.internal_type_dec_bl) + (@type.internal_type_dec_lb base.type base.type.type_beq base.type.internal_type_dec_lb) + | match goal with + | [ H : ?x <> ?x |- _ ] => exfalso; exact (H eq_refl) + end ]. Ltac rewrite_type_transport_correct := cbv [type.try_transport_cps type.try_transport base.try_transport base.try_transport_cps] in *; |