diff options
-rw-r--r-- | src/Experiments/NewPipeline/GENERATEDIdentifiersWithoutTypesProofs.v | 16 |
1 files changed, 10 insertions, 6 deletions
diff --git a/src/Experiments/NewPipeline/GENERATEDIdentifiersWithoutTypesProofs.v b/src/Experiments/NewPipeline/GENERATEDIdentifiersWithoutTypesProofs.v index d5374e8ce..4261617af 100644 --- a/src/Experiments/NewPipeline/GENERATEDIdentifiersWithoutTypesProofs.v +++ b/src/Experiments/NewPipeline/GENERATEDIdentifiersWithoutTypesProofs.v @@ -24,7 +24,11 @@ Module Compilers. end. Proof. subst y; destruct x; constructor. Qed. - Lemma pident_to_typed_invert_bind_args_type__pident_to_typed_invert_bind_args t idc p f + Lemma eta_ident_cps_correct T t idc f + : @eta_ident_cps T t idc f = f t idc. + Proof. cbv [eta_ident_cps]; break_innermost_match; reflexivity. Qed. + + Lemma to_typed_invert_bind_args_gen t idc p f : @invert_bind_args t idc p = Some f -> { pf : t = type_of p f | @to_typed p f = rew [Compilers.ident.ident] pf in idc }. Proof. @@ -42,16 +46,16 @@ Module Compilers. | break_innermost_match_hyps_step ]. Qed. - Lemma pident_to_typed_invert_bind_args_type t idc p f + Lemma type_of_invert_bind_args t idc p f : @invert_bind_args t idc p = Some f -> t = type_of p f. Proof. - intro pf; exact (proj1_sig (@pident_to_typed_invert_bind_args_type__pident_to_typed_invert_bind_args t idc p f pf)). + intro pf; exact (proj1_sig (@to_typed_invert_bind_args_gen t idc p f pf)). Defined. - Lemma pident_to_typed_invert_bind_args t idc p f (pf : @invert_bind_args t idc p = Some f) - : @to_typed p f = rew [Compilers.ident.ident] @pident_to_typed_invert_bind_args_type t idc p f pf in idc. + Lemma to_typed_invert_bind_args t idc p f (pf : @invert_bind_args t idc p = Some f) + : @to_typed p f = rew [Compilers.ident.ident] @type_of_invert_bind_args t idc p f pf in idc. Proof. - exact (proj2_sig (@pident_to_typed_invert_bind_args_type__pident_to_typed_invert_bind_args t idc p f pf)). + exact (proj2_sig (@to_typed_invert_bind_args_gen t idc p f pf)). Defined. Lemma try_make_transport_ident_cps_correct P idc1 idc2 T k |