diff options
| author |  Jason Gross <jagro@google.com> | 2018-08-02 18:24:36 -0400 |
|---|---|---|
| committer | Jason Gross <jagro@google.com> | 2018-08-02 18:24:36 -0400 |
| commit | c3199e59f7c8d8e73e653808b50f77dc8e905b0a (patch) | |
| tree | ff89b0f99958c2c46b5e2c8532efdcdac57d5c4b /src | |
| parent | a8c07fa7605eefa2de39000d4c6fce17fb40be43 (diff) | |
Adjust GENERATEDIdentifiersWithoutTypesProofs.v, add eta_ident_cps_correct
Diffstat (limited to 'src')
| -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 |