diff options
author | 2019-03-08 02:33:39 -0500 | |
---|---|---|
committer | 2019-03-31 09:36:16 -0400 | |
commit | 339ee4ec95624751f84997064a6a985478ca5645 (patch) | |
tree | 1da8b103fa9a46a48270647dfc665f61eb3aebcb /src/RewriterRulesInterpGood.v | |
parent | a8b4394093e61b050406ca952a6d017ad1c737e4 (diff) |
Finish reifying list lemmas
After | File Name | Before || Change | % Change
--------------------------------------------------------------------------------------------
22m23.84s | Total | 21m34.63s || +0m49.21s | +3.80%
--------------------------------------------------------------------------------------------
1m52.62s | RewriterRulesInterpGood.vo | 1m37.14s || +0m15.48s | +15.93%
3m25.91s | p384_32.c | 3m14.24s || +0m11.66s | +6.00%
1m32.94s | RewriterRulesGood.vo | 1m42.36s || -0m09.42s | -9.20%
0m33.72s | RewriterWf1.vo | 0m24.30s || +0m09.41s | +38.76%
1m17.31s | Rewriter.vo | 1m12.10s || +0m05.21s | +7.22%
0m43.01s | ExtractionHaskell/unsaturated_solinas | 0m39.84s || +0m03.16s | +7.95%
0m45.21s | p521_32.c | 0m42.86s || +0m02.35s | +5.48%
1m46.30s | Fancy/Barrett256.vo | 1m45.08s || +0m01.21s | +1.16%
0m38.74s | p521_64.c | 0m37.49s || +0m01.25s | +3.33%
0m23.16s | ExtractionOCaml/word_by_word_montgomery | 0m21.44s || +0m01.71s | +8.02%
0m18.74s | p256_32.c | 0m16.88s || +0m01.85s | +11.01%
0m15.00s | ExtractionOCaml/unsaturated_solinas | 0m13.98s || +0m01.01s | +7.29%
0m11.92s | ExtractionOCaml/saturated_solinas | 0m10.13s || +0m01.78s | +17.67%
0m07.82s | ExtractionOCaml/saturated_solinas.ml | 0m05.98s || +0m01.83s | +30.76%
1m47.42s | RewriterWf2.vo | 1m47.81s || -0m00.39s | -0.36%
0m58.35s | ExtractionHaskell/word_by_word_montgomery | 0m57.41s || +0m00.94s | +1.63%
0m45.47s | RewriterInterpProofs1.vo | 0m45.67s || -0m00.20s | -0.43%
0m37.34s | Fancy/Montgomery256.vo | 0m37.09s || +0m00.25s | +0.67%
0m36.14s | PushButtonSynthesis/UnsaturatedSolinas.vo | 0m36.52s || -0m00.38s | -1.04%
0m29.91s | ExtractionHaskell/saturated_solinas | 0m29.70s || +0m00.21s | +0.70%
0m26.77s | PushButtonSynthesis/WordByWordMontgomery.vo | 0m26.72s || +0m00.05s | +0.18%
0m25.87s | SlowPrimeSynthesisExamples.vo | 0m25.49s || +0m00.38s | +1.49%
0m18.72s | p448_solinas_64.c | 0m19.16s || -0m00.44s | -2.29%
0m16.94s | secp256k1_32.c | 0m17.18s || -0m00.23s | -1.39%
0m13.92s | p434_64.c | 0m13.08s || +0m00.83s | +6.42%
0m13.15s | ExtractionOCaml/word_by_word_montgomery.ml | 0m12.58s || +0m00.57s | +4.53%
0m08.97s | ExtractionOCaml/unsaturated_solinas.ml | 0m08.95s || +0m00.02s | +0.22%
0m08.37s | ExtractionHaskell/word_by_word_montgomery.hs | 0m08.51s || -0m00.14s | -1.64%
0m08.35s | p224_32.c | 0m08.10s || +0m00.25s | +3.08%
0m07.77s | p384_64.c | 0m07.29s || +0m00.47s | +6.58%
0m06.92s | BoundsPipeline.vo | 0m06.85s || +0m00.07s | +1.02%
0m05.70s | ExtractionHaskell/unsaturated_solinas.hs | 0m06.14s || -0m00.43s | -7.16%
0m05.12s | ExtractionHaskell/saturated_solinas.hs | 0m06.09s || -0m00.96s | -15.92%
0m03.53s | PushButtonSynthesis/Primitives.vo | 0m03.55s || -0m00.02s | -0.56%
0m03.38s | PushButtonSynthesis/SmallExamples.vo | 0m03.34s || +0m00.04s | +1.19%
0m03.16s | PushButtonSynthesis/BarrettReduction.vo | 0m03.24s || -0m00.08s | -2.46%
0m03.06s | PushButtonSynthesis/SaturatedSolinas.vo | 0m03.23s || -0m00.16s | -5.26%
0m02.81s | PushButtonSynthesis/MontgomeryReduction.vo | 0m02.84s || -0m00.02s | -1.05%
0m02.62s | curve25519_32.c | 0m02.22s || +0m00.39s | +18.01%
0m01.88s | p224_64.c | 0m01.47s || +0m00.40s | +27.89%
0m01.68s | curve25519_64.c | 0m02.19s || -0m00.51s | -23.28%
0m01.32s | CLI.vo | 0m01.33s || -0m00.01s | -0.75%
0m01.24s | secp256k1_64.c | 0m01.30s || -0m00.06s | -4.61%
0m01.22s | p256_64.c | 0m01.47s || -0m00.25s | -17.00%
0m01.16s | RewriterProofs.vo | 0m01.16s || +0m00.00s | +0.00%
0m01.10s | StandaloneHaskellMain.vo | 0m01.00s || +0m00.10s | +10.00%
0m01.05s | CompilersTestCases.vo | 0m01.09s || -0m00.04s | -3.66%
0m01.04s | StandaloneOCamlMain.vo | 0m01.04s || +0m00.00s | +0.00%
Diffstat (limited to 'src/RewriterRulesInterpGood.v')
-rw-r--r-- | src/RewriterRulesInterpGood.v | 185 |
1 files changed, 174 insertions, 11 deletions
diff --git a/src/RewriterRulesInterpGood.v b/src/RewriterRulesInterpGood.v index 954340fa4..d30366220 100644 --- a/src/RewriterRulesInterpGood.v +++ b/src/RewriterRulesInterpGood.v @@ -119,7 +119,9 @@ Module Compilers. Local Ltac do_cbv0 := cbv [id Compile.rewrite_rules_interp_goodT_curried - Compile.rewrite_rule_data_interp_goodT_curried Compile.under_with_unification_resultT_relation_hetero Compile.under_with_unification_resultT'_relation_hetero Compile.wf_with_unification_resultT Compile.under_type_of_list_relation_cps Compile.under_type_of_list_relation1_cps pattern.pattern_of_anypattern pattern.type_of_anypattern Compile.rew_replacement Compile.rew_should_do_again Compile.rew_with_opt Compile.rew_under_lets Compile.wf_with_unification_resultT Compile.pattern_default_interp pattern.type.under_forall_vars_relation pattern.type.under_forall_vars_relation1 Compile.deep_rewrite_ruleTP_gen Compile.with_unification_resultT' pattern.ident.arg_types pattern.type.lam_forall_vars Compilers.pattern.type.lam_forall_vars_gen Compile.pattern_default_interp' pattern.collect_vars PositiveMap.empty pattern.type.collect_vars PositiveSet.elements PositiveSet.union pattern.base.collect_vars PositiveSet.empty PositiveSet.xelements Compile.lam_type_of_list id pattern.ident.to_typed Compile.under_type_of_list_relation_cps Compile.deep_rewrite_ruleTP_gen_good_relation Compile.normalize_deep_rewrite_rule pattern.type.subst_default PositiveSet.add PositiveSet.rev PositiveSet.rev_append PositiveMap.add Compile.option_bind' Compile.wf_value Compile.value pattern.base.subst_default pattern.base.lookup_default PositiveMap.find Compile.rewrite_ruleTP ident.smart_Literal Compile.value_interp_related]. + Compile.rewrite_rule_data_interp_goodT_curried Compile.under_with_unification_resultT_relation_hetero Compile.under_with_unification_resultT'_relation_hetero Compile.wf_with_unification_resultT Compile.under_type_of_list_relation_cps Compile.under_type_of_list_relation1_cps pattern.pattern_of_anypattern pattern.type_of_anypattern Compile.rew_replacement Compile.rew_should_do_again Compile.rew_with_opt Compile.rew_under_lets Compile.wf_with_unification_resultT Compile.pattern_default_interp pattern.type.under_forall_vars_relation pattern.type.under_forall_vars_relation1 Compile.deep_rewrite_ruleTP_gen Compile.with_unification_resultT' pattern.ident.arg_types pattern.type.lam_forall_vars Compilers.pattern.type.lam_forall_vars_gen Compile.pattern_default_interp' pattern.collect_vars PositiveMap.empty pattern.type.collect_vars PositiveSet.elements PositiveSet.union pattern.base.collect_vars PositiveSet.empty PositiveSet.xelements Compile.lam_type_of_list id pattern.ident.to_typed Compile.under_type_of_list_relation_cps Compile.deep_rewrite_ruleTP_gen_good_relation Compile.normalize_deep_rewrite_rule pattern.type.subst_default PositiveSet.add PositiveSet.rev PositiveSet.rev_append PositiveMap.add Compile.option_bind' Compile.wf_value Compile.value pattern.base.subst_default pattern.base.lookup_default PositiveMap.find Compile.rewrite_ruleTP ident.smart_Literal Compile.value_interp_related + Reify.expr_value_to_rewrite_rule_replacement UnderLets.flat_map Compile.reify_expr_beta_iota Compile.reflect_expr_beta_iota Compile.reflect_ident_iota Compile.reify_to_UnderLets UnderLets.of_expr Compile.Base_value]; + cbn [UnderLets.splice Compile.reflect invert_expr.invert_Literal invert_expr.ident.invert_Literal Compile.splice_under_lets_with_value]. Local Ltac do_cbv := do_cbv0; cbv [List.map List.fold_right List.rev list_rect orb List.app]. @@ -183,11 +185,48 @@ Module Compilers. end; progress cbn [ident_interp fst snd] | [ |- ?x = ?y ] => tryif first [ has_evar x | has_evar y ] then fail else (progress subst) + | [ |- ?x = ?y ] => tryif first [ has_evar x | has_evar y ] then fail else reflexivity | [ |- ?x = ?x ] => tryif has_evar x then fail else reflexivity | [ |- ?ev = _ ] => is_evar ev; reflexivity | [ |- _ = ?ev ] => is_evar ev; reflexivity end. + (* TODO: MOVE ME? *) + Local Ltac recursive_match_to_list_case term := + lazymatch term with + | context G[match ?ls with nil => ?N | cons x xs => @?C x xs end] + => let T := type of N in + let term := context G[list_case (fun _ => T) N C ls] in + recursive_match_to_list_case term + | context[match _ with nil => _ | _ => _ end] + => let G_f + := match term with + | context G[fun x : ?T => @?f x] + => lazymatch f with + | context[match _ with nil => _ | _ => _ end] + => let f' := fresh in + let T' := type of f in + constr:(((fun f' : T' => ltac:(let G' := context G[f'] in exact G')), + f)) + end + end in + lazymatch G_f with + | ((fun f' => ?G), (fun x : ?T => ?f)) + => let x' := fresh in + let rep := constr:(fun x' : T + => ltac:(let f := constr:(match x' with x => f end) in + let f := recursive_match_to_list_case f in + exact f)) in + let term := constr:(match rep with f' => G end) in + recursive_match_to_list_case term + end + | _ => term + end. + Local Ltac recursive_match_to_list_case_in_goal := + let G := match goal with |- ?G => G end in + let G := recursive_match_to_list_case G in + change G. + Local Ltac interp_good_t_step_related := first [ lazymatch goal with | [ |- ?x = ?x ] => reflexivity @@ -199,10 +238,123 @@ Module Compilers. (*| [ |- context[(fst ?x, snd ?x)] ] => progress eta_expand | [ |- context[match ?x with pair a b => _ end] ] => progress eta_expand*) end + | match goal with + | [ |- UnderLets.interp_related ?ii ?R (UnderLets.Base (#ident.list_rect @ _ @ _ @ _)%expr) (@list_rect ?A (fun _ => ?P) ?N ?C ?ls) ] + => progress change (@list_rect A (fun _ => P) N C ls) with (@ident.Thunked.list_rect A P (fun _ => N) C ls) + | [ |- expr.interp_related_gen ?ii ?R (#ident.list_rect @ _ @ _ @ _)%expr (@list_rect ?A (fun _ => ?P) ?N ?C ?ls) ] + => progress change (@list_rect A (fun _ => P) N C ls) with (@ident.Thunked.list_rect A P (fun _ => N) C ls) + | [ |- expr.interp_related_gen ?ii ?R (#ident.list_case @ _ @ _ @ _)%expr (@list_case ?A (fun _ => ?P) ?N ?C ?ls) ] + => progress change (@list_case A (fun _ => P) N C ls) with (@ident.Thunked.list_case A P (fun _ => N) C ls) + | [ |- UnderLets.interp_related _ _ (list_rect _ _ _ _) (List.app ?ls1 ?ls2) ] + => rewrite (eq_app_list_rect ls1 ls2) + | [ |- UnderLets.interp_related _ _ (list_rect _ _ _ _) (@flat_map ?A ?B ?f ?ls) ] + => rewrite (@eq_flat_map_list_rect A B f ls) + | [ |- UnderLets.interp_related _ _ (list_rect _ _ _ _) (@partition ?A ?f ?ls) ] + => rewrite (@eq_partition_list_rect A f ls) + | [ |- UnderLets.interp_related _ _ (list_rect _ _ _ _) (@List.map ?A ?B ?f ?ls) ] + => rewrite (@eq_map_list_rect A B f ls) + | [ |- UnderLets.interp_related _ _ (list_rect _ _ _ _ _) (@List.combine ?A ?B ?xs ?ys) ] + => rewrite (@eq_combine_list_rect A B xs ys) + | [ |- UnderLets.interp_related _ _ (nat_rect _ _ _ _) (List.repeat ?x ?n) ] + => rewrite (eq_repeat_nat_rect x n) + | [ |- ?R (nat_rect _ _ _ _ _) (@List.firstn ?A ?n ?ls) ] + => rewrite (@eq_firstn_nat_rect A n ls) + | [ |- ?R (nat_rect _ _ _ _ _) (@List.skipn ?A ?n ?ls) ] + => rewrite (@eq_skipn_nat_rect A n ls) + | [ |- ?R (list_rect _ _ _ _) (@List.rev ?A ?xs) ] + => rewrite (@eq_rev_list_rect A xs) + | [ |- ?R (list_rect _ _ _ _) (@List.length ?A ?xs) ] + => rewrite (@eq_length_list_rect A xs) + | [ |- ?R (list_rect _ _ _ _) (@List.flat_map ?A ?B ?f ?xs) ] + => rewrite (@eq_flat_map_list_rect A B f xs) + | [ |- ?R (list_rect _ _ _ _) (@List.partition ?A ?f ?xs) ] + => rewrite (@eq_partition_list_rect A f xs) + | [ |- ?R (nat_rect _ _ _ _ _) (@update_nth ?A ?n ?f ?xs) ] + => rewrite (@eq_update_nth_nat_rect A n f xs) + + | [ |- UnderLets.interp_related _ _ (UnderLets.Base (#ident.list_rect @ _ @ _ @ _)%expr) (List.app ?ls1 ?ls2) ] + => rewrite (eq_app_list_rect ls1 ls2) + | [ |- UnderLets.interp_related _ _ (UnderLets.Base (#ident.list_rect @ _ @ _ @ _)%expr) (List.app ?ls1 ?ls2) ] + => rewrite (eq_app_list_rect ls1 ls2) + | [ |- UnderLets.interp_related _ _ (UnderLets.Base (#ident.list_rect @ _ @ _ @ _)%expr) (@flat_map ?A ?B ?f ?ls) ] + => rewrite (@eq_flat_map_list_rect A B f ls) + | [ |- UnderLets.interp_related _ _ (UnderLets.Base (#ident.list_rect @ _ @ _ @ _)%expr) (@partition ?A ?f ?ls) ] + => rewrite (@eq_partition_list_rect A f ls) + | [ |- UnderLets.interp_related _ _ (UnderLets.Base (#ident.list_rect @ _ @ _ @ _)%expr) (@List.map ?A ?B ?f ?ls) ] + => rewrite (@eq_map_list_rect A B f ls) + | [ |- UnderLets.interp_related _ _ (UnderLets.Base (#ident.list_rect_arrow @ _ @ _ @ _ @ _)%expr) (@List.combine ?A ?B ?xs ?ys) ] + => rewrite (@eq_combine_list_rect A B xs ys) + | [ |- UnderLets.interp_related _ _ _ (@fold_right ?A ?B ?f ?v ?ls) ] + => rewrite (@eq_fold_right_list_rect A B f v ls) + | [ |- ?R (#ident.nat_rect_arrow @ _ @ _ @ _ @ _)%expr (@List.firstn ?A ?n ?ls) ] + => rewrite (@eq_firstn_nat_rect A n ls) + | [ |- ?R (#ident.nat_rect_arrow @ _ @ _ @ _ @ _)%expr (@List.skipn ?A ?n ?ls) ] + => rewrite (@eq_skipn_nat_rect A n ls) + | [ |- ?R (#ident.list_rect @ _ @ _ @ _)%expr (@List.rev ?A ?xs) ] + => rewrite (@eq_rev_list_rect A xs) + | [ |- ?R (#ident.list_rect @ _ @ _ @ _)%expr (@List.length ?A ?xs) ] + => rewrite (@eq_length_list_rect A xs) + | [ |- ?R (#ident.list_rect @ _ @ _ @ _)%expr (@List.flat_map ?A ?B ?f ?xs) ] + => rewrite (@eq_flat_map_list_rect A B f xs) + | [ |- ?R (#ident.list_rect @ _ @ _ @ _)%expr (@List.partition ?A ?f ?xs) ] + => rewrite (@eq_partition_list_rect A f xs) + | [ |- ?R (#ident.nat_rect_arrow @ _ @ _ @ _ @ _)%expr (@update_nth ?A ?n ?f ?xs) ] + => rewrite (@eq_update_nth_nat_rect A n f xs) + | [ |- ?R (#ident.list_rect_arrow @ _ @ _ @ _ @ _)%expr (@List.combine ?A ?B ?xs ?ys) ] + => rewrite (@eq_combine_list_rect A B xs ys) + + + | [ |- expr.interp_related_gen _ _ (#ident.list_rect @ _ @ _ @ _)%expr (ident.Thunked.list_rect _ _ _ _) ] + => recurse_interp_related_step; [ recurse_interp_related_step | reflexivity ]; + [ recurse_interp_related_step; [ recurse_interp_related_step | reflexivity ]; + [ recurse_interp_related_step; [ recurse_interp_related_step | reflexivity ]; + [ recurse_interp_related_step; [ recurse_interp_related_step | reflexivity ] + | ] + | ] + | ] + | [ |- expr.interp_related_gen _ _ (#ident.list_rect_arrow @ _ @ _ @ _ @ _)%expr (list_rect _ _ _ _ _) ] + => recurse_interp_related_step; [ recurse_interp_related_step | reflexivity ]; + [ recurse_interp_related_step; [ recurse_interp_related_step | reflexivity ]; + [ recurse_interp_related_step; [ recurse_interp_related_step | reflexivity ]; + [ recurse_interp_related_step; [ recurse_interp_related_step | reflexivity ]; + [ recurse_interp_related_step; [ recurse_interp_related_step | reflexivity ] + | ] + | ] + | ] + | ] + | [ |- expr.interp_related_gen _ _ (#ident.nat_rect @ _ @ _ @ _)%expr (ident.Thunked.nat_rect _ _ _ _) ] + => recurse_interp_related_step; [ recurse_interp_related_step | reflexivity ]; + [ recurse_interp_related_step; [ recurse_interp_related_step | reflexivity ]; + [ recurse_interp_related_step; [ recurse_interp_related_step | reflexivity ]; + [ recurse_interp_related_step; [ recurse_interp_related_step | reflexivity ] + | ] + | ] + | ] + | [ |- expr.interp_related_gen _ _ (#ident.nat_rect_arrow @ _ @ _ @ _ @ _)%expr (nat_rect _ _ _ _ _) ] + => recurse_interp_related_step; [ recurse_interp_related_step | reflexivity ]; + [ recurse_interp_related_step; [ recurse_interp_related_step | reflexivity ]; + [ recurse_interp_related_step; [ recurse_interp_related_step | reflexivity ]; + [ recurse_interp_related_step; [ recurse_interp_related_step | reflexivity ]; + [ recurse_interp_related_step; [ recurse_interp_related_step | reflexivity ] + | ] + | ] + | ] + | ] + | [ |- expr.interp_related_gen _ _ (#ident.list_case @ _ @ _ @ _)%expr (ident.Thunked.list_case _ _ _ _) ] + => recurse_interp_related_step; [ recurse_interp_related_step | reflexivity ]; + [ recurse_interp_related_step; [ recurse_interp_related_step | reflexivity ]; + [ recurse_interp_related_step; [ recurse_interp_related_step | reflexivity ]; + [ recurse_interp_related_step; [ recurse_interp_related_step | reflexivity ] + | ] + | ] + | ] + | [ |- context[match _ with nil => _ | _ => _ end] ] => progress recursive_match_to_list_case_in_goal + end | progress cbn [expr.interp ident.gen_interp fst snd Compile.reify Compile.reflect Compile.wf_value' Compile.value' Option.bind UnderLets.interp list_case type.interp base.interp base.base_interp ident.to_fancy invert_Some ident.fancy.interp ident.fancy.interp_with_wordmax Compile.reify_expr bool_rect UnderLets.interp_related type.related] in * | progress cbv [Compile.option_bind' respectful expr.interp_related] in * | progress fold (@type.interp _ base.interp) | progress fold (@base.interp) + | progress change S with Nat.succ | match goal with | [ |- context[List.map _ (Lists.List.repeat _ _)] ] => rewrite map_repeat | [ |- context[List.map _ (List.map _ _)] ] => rewrite map_map @@ -220,20 +372,13 @@ Module Compilers. | [ |- context[UnderLets.interp _ (list_rect _ _ _ _)] ] => rewrite UnderLets_interp_list_rect | [ |- context[UnderLets.interp _ (UnderLets.splice _ _)] ] => rewrite UnderLets.interp_splice | [ |- context[list_rect _ _ _ (List.map _ _)] ] => rewrite list_rect_map - | [ |- UnderLets.interp_related _ _ (list_rect _ _ _ _) (List.app ?ls1 ?ls2) ] - => rewrite (eq_app_list_rect ls1 ls2) - | [ |- UnderLets.interp_related _ _ (list_rect _ _ _ _) (@flat_map ?A ?B ?f ?ls) ] - => rewrite (@eq_flat_map_list_rect A B f ls) - | [ |- UnderLets.interp_related _ _ (list_rect _ _ _ _) (@partition ?A ?f ?ls) ] - => rewrite (@eq_partition_list_rect A f ls) - | [ |- UnderLets.interp_related _ _ (list_rect _ _ _ _) (@List.map ?A ?B ?f ?ls) ] - => rewrite (@eq_map_list_rect A B f ls) - | [ |- UnderLets.interp_related _ _ _ (@fold_right ?A ?B ?f ?v ?ls) ] - => rewrite (@eq_fold_right_list_rect A B f v ls) | [ |- context[expr.interp_related_gen _ _ (reify_list _)] ] => rewrite expr.reify_list_interp_related_gen_iff | [ H : context[expr.interp_related_gen _ _ (reify_list _)] |- _ ] => rewrite expr.reify_list_interp_related_gen_iff in H + | [ |- expr.interp_related_gen ?ident_interp _ (UnderLets.to_expr ?x) ?y ] + => change (expr.interp_related ident_interp (UnderLets.to_expr x) y); + rewrite <- UnderLets.to_expr_interp_related_iff | [ |- context[Forall2 _ (List.map _ _) _] ] => rewrite Forall2_map_l_iff | [ |- context[Forall2 _ _ (List.map _ _)] ] => rewrite Forall2_map_r_iff | [ |- context[Forall2 _ (List.repeat _ _) (List.repeat _ _)] ] => rewrite Forall2_repeat_iff @@ -266,6 +411,21 @@ Module Compilers. ?Pcons' ?ls') ] => apply (@UnderLets.list_rect_interp_related _ _ _ ident_interp A B Pnil Pcons ls B' Pnil' Pcons' ls' R) + | [ |- UnderLets.interp_related + ?ident_interp ?R + (list_rect + (fun _ : list (expr ?A) => ?B -> UnderLets.UnderLets _ _ _ ?C) + ?Pnil + ?Pcons + ?ls + ?x) + (list_rect + (fun _ : list _ => ?B' -> ?C') + ?Pnil' + ?Pcons' + ?ls' + ?x') ] + => apply (@UnderLets.list_rect_arrow_interp_related _ _ _ ident_interp A B C Pnil Pcons ls x B' C' Pnil' Pcons' ls' x' R (expr.interp_related ident_interp)) | [ |- UnderLets.interp_related _ _ (nat_rect _ _ _ _) (nat_rect _ _ _ _) ] => apply UnderLets.nat_rect_interp_related | [ |- UnderLets.interp_related _ _ (nat_rect _ _ _ _ _) (nat_rect _ _ _ _ _) ] @@ -338,6 +498,7 @@ Module Compilers. | assumption | progress inversion_option | progress destruct_head'_and + | progress destruct_head'_unit | progress split_andb | match goal with | [ |- Lists.List.repeat _ _ = Lists.List.repeat _ _ ] => apply f_equal2 @@ -464,6 +625,8 @@ Module Compilers. => apply H | [ H : forall x x', ?Rx x x' -> forall y y', _ -> forall z z', ?Rz z z' -> ?R (?f x y z) (?f' x' y' z') |- ?R (?f _ _ _) (?f' _ _ _) ] => apply H; clear H + | [ H : forall x x', _ -> forall y y', _ -> forall z z', _ -> forall w w', _ -> ?R (?f x y z w) (?f' x' y' z' w') |- ?R (?f _ _ _ _) (?f' _ _ _ _) ] + => apply H; clear H end | progress cbv [Option.bind] in * | match goal with |