From 8a4d828e05bca153f12370d08d3b4ad404fbbee2 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Tue, 23 Apr 2019 01:38:50 -0400 Subject: Do less reduction in GENERATEDIdentifiersWithoutTypes Since more of the definitions are now done in Gallina, hopefully these should be easier to factor out / parameterize over the type of identifiers, now. After | File Name | Before || Change | % Change ----------------------------------------------------------------------------------------------- 21m28.78s | Total | 21m49.80s || -0m21.01s | -1.60% ----------------------------------------------------------------------------------------------- 0m22.98s | GENERATEDIdentifiersWithoutTypesProofs.vo | 0m49.53s || -0m26.55s | -53.60% 0m47.26s | p521_32.c | 0m44.08s || +0m03.17s | +7.21% 0m36.30s | ExtractionHaskell/saturated_solinas | 0m32.96s || +0m03.33s | +10.13% 1m00.34s | ExtractionHaskell/word_by_word_montgomery | 1m02.45s || -0m02.10s | -3.37% 0m26.90s | SlowPrimeSynthesisExamples.vo | 0m24.35s || +0m02.54s | +10.47% 0m16.06s | GENERATEDIdentifiersWithoutTypes.vo | 0m19.05s || -0m02.99s | -15.69% 0m14.89s | ExtractionOCaml/unsaturated_solinas | 0m12.83s || +0m02.06s | +16.05% 0m43.92s | ExtractionHaskell/unsaturated_solinas | 0m42.40s || +0m01.52s | +3.58% 0m20.11s | ExtractionOCaml/word_by_word_montgomery | 0m21.19s || -0m01.08s | -5.09% 0m20.06s | p256_32.c | 0m21.81s || -0m01.75s | -8.02% 0m17.96s | secp256k1_32.c | 0m19.45s || -0m01.48s | -7.66% 0m13.58s | ExtractionOCaml/word_by_word_montgomery.ml | 0m14.89s || -0m01.31s | -8.79% 0m07.27s | ExtractionOCaml/saturated_solinas.ml | 0m05.75s || +0m01.51s | +26.43% 3m23.62s | p384_32.c | 3m23.29s || +0m00.33s | +0.16% 1m42.18s | Fancy/Barrett256.vo | 1m41.69s || +0m00.49s | +0.48% 1m33.94s | RewriterWf2.vo | 1m34.43s || -0m00.49s | -0.51% 0m55.14s | Rewriter/ToFancyWithCasts.vo | 0m55.92s || -0m00.78s | -1.39% 0m46.15s | Rewriter/NBE.vo | 0m46.06s || +0m00.08s | +0.19% 0m44.70s | Rewriter/ArithWithCasts.vo | 0m44.55s || +0m00.15s | +0.33% 0m43.96s | RewriterInterpProofs1.vo | 0m44.18s || -0m00.21s | -0.49% 0m39.78s | p521_64.c | 0m38.84s || +0m00.93s | +2.42% 0m36.72s | PushButtonSynthesis/UnsaturatedSolinas.vo | 0m36.54s || +0m00.17s | +0.49% 0m35.92s | RewriterWf1.vo | 0m36.26s || -0m00.33s | -0.93% 0m34.57s | Fancy/Montgomery256.vo | 0m34.64s || -0m00.07s | -0.20% 0m27.29s | PushButtonSynthesis/WordByWordMontgomery.vo | 0m27.17s || +0m00.11s | +0.44% 0m23.67s | Rewriter/Arith.vo | 0m24.59s || -0m00.91s | -3.74% 0m20.78s | PushButtonSynthesis/BarrettReduction.vo | 0m20.69s || +0m00.08s | +0.43% 0m18.97s | p448_solinas_64.c | 0m18.10s || +0m00.86s | +4.80% 0m14.02s | p434_64.c | 0m13.37s || +0m00.65s | +4.86% 0m11.26s | ExtractionOCaml/unsaturated_solinas.ml | 0m10.61s || +0m00.65s | +6.12% 0m10.76s | ExtractionOCaml/saturated_solinas | 0m11.65s || -0m00.89s | -7.63% 0m08.76s | p224_32.c | 0m09.58s || -0m00.82s | -8.55% 0m08.07s | ExtractionHaskell/word_by_word_montgomery.hs | 0m07.96s || +0m00.11s | +1.38% 0m07.88s | p384_64.c | 0m08.81s || -0m00.93s | -10.55% 0m06.98s | BoundsPipeline.vo | 0m06.97s || +0m00.01s | +0.14% 0m06.41s | ExtractionHaskell/unsaturated_solinas.hs | 0m05.52s || +0m00.89s | +16.12% 0m05.21s | ExtractionHaskell/saturated_solinas.hs | 0m04.48s || +0m00.72s | +16.29% 0m03.54s | PushButtonSynthesis/Primitives.vo | 0m03.61s || -0m00.06s | -1.93% 0m03.33s | PushButtonSynthesis/SmallExamples.vo | 0m03.38s || -0m00.04s | -1.47% 0m03.20s | PushButtonSynthesis/SaturatedSolinas.vo | 0m03.22s || -0m00.02s | -0.62% 0m03.05s | curve25519_32.c | 0m02.76s || +0m00.29s | +10.50% 0m02.63s | PushButtonSynthesis/FancyMontgomeryReduction.vo | 0m02.70s || -0m00.07s | -2.59% 0m02.53s | Rewriter.vo | 0m02.04s || +0m00.48s | +24.01% 0m02.10s | curve25519_64.c | 0m01.80s || +0m00.30s | +16.66% 0m01.94s | p224_64.c | 0m01.52s || +0m00.41s | +27.63% 0m01.85s | secp256k1_64.c | 0m01.55s || +0m00.30s | +19.35% 0m01.40s | CLI.vo | 0m01.33s || +0m00.06s | +5.26% 0m01.36s | p256_64.c | 0m01.84s || -0m00.48s | -26.08% 0m01.33s | Rewriter/StripLiteralCasts.vo | 0m01.22s || +0m00.11s | +9.01% 0m01.23s | CompilersTestCases.vo | 0m01.14s || +0m00.09s | +7.89% 0m01.15s | StandaloneOCamlMain.vo | 0m01.11s || +0m00.03s | +3.60% 0m01.13s | StandaloneHaskellMain.vo | 0m01.17s || -0m00.04s | -3.41% 0m01.11s | Rewriter/ToFancy.vo | 0m01.07s || +0m00.04s | +3.73% 0m00.80s | RewriterAll.vo | 0m00.80s || +0m00.00s | +0.00% 0m00.74s | RewriterAllTactics.vo | 0m00.91s || -0m00.17s | -18.68% The diff in the .ml files is quite small, and is effectively just variable renaming: ```diff diff --git a/src/ExtractionOCaml/saturated_solinas.ml b/src/ExtractionOCaml/saturated_solinas.ml index fd8a9d3..e9afa49 100644 --- a/src/ExtractionOCaml/saturated_solinas.ml +++ b/src/ExtractionOCaml/saturated_solinas.ml @@ -39856,7 +39856,7 @@ module Coq2_Compilers = | Compilers.Coq_ident.Literal (t1, v) -> (match t1 with | Compilers.Coq_base.Coq_type.Coq_unit -> - (fun v0 -> Some (Obj.magic (v0, ()))) + (fun x -> Some (Obj.magic (x, ()))) | Compilers.Coq_base.Coq_type.Z -> (fun _ -> None) | Compilers.Coq_base.Coq_type.Coq_bool -> (fun _ -> None) | Compilers.Coq_base.Coq_type.Coq_nat -> (fun _ -> None) @@ -39962,7 +39962,7 @@ module Coq2_Compilers = (match t1 with | Compilers.Coq_base.Coq_type.Coq_unit -> (fun _ -> None) | Compilers.Coq_base.Coq_type.Z -> - (fun v0 -> Some (Obj.magic (v0, ()))) + (fun x -> Some (Obj.magic (x, ()))) | Compilers.Coq_base.Coq_type.Coq_bool -> (fun _ -> None) | Compilers.Coq_base.Coq_type.Coq_nat -> (fun _ -> None) | Compilers.Coq_base.Coq_type.Coq_zrange -> (fun _ -> None)) @@ -40068,7 +40068,7 @@ module Coq2_Compilers = | Compilers.Coq_base.Coq_type.Coq_unit -> (fun _ -> None) | Compilers.Coq_base.Coq_type.Z -> (fun _ -> None) | Compilers.Coq_base.Coq_type.Coq_bool -> - (fun v0 -> Some (Obj.magic (v0, ()))) + (fun x -> Some (Obj.magic (x, ()))) | Compilers.Coq_base.Coq_type.Coq_nat -> (fun _ -> None) | Compilers.Coq_base.Coq_type.Coq_zrange -> (fun _ -> None)) v @@ -40174,7 +40174,7 @@ module Coq2_Compilers = | Compilers.Coq_base.Coq_type.Z -> (fun _ -> None) | Compilers.Coq_base.Coq_type.Coq_bool -> (fun _ -> None) | Compilers.Coq_base.Coq_type.Coq_nat -> - (fun v0 -> Some (Obj.magic (v0, ()))) + (fun x -> Some (Obj.magic (x, ()))) | Compilers.Coq_base.Coq_type.Coq_zrange -> (fun _ -> None)) v | Compilers.Coq_ident.Nat_succ -> None @@ -40280,7 +40280,7 @@ module Coq2_Compilers = | Compilers.Coq_base.Coq_type.Coq_bool -> (fun _ -> None) | Compilers.Coq_base.Coq_type.Coq_nat -> (fun _ -> None) | Compilers.Coq_base.Coq_type.Coq_zrange -> - (fun v0 -> Some (Obj.magic (v0, ())))) v + (fun x -> Some (Obj.magic (x, ())))) v | Compilers.Coq_ident.Nat_succ -> None | Compilers.Coq_ident.Nat_pred -> None | Compilers.Coq_ident.Nat_max -> None @@ -49466,8 +49466,8 @@ module Coq2_Compilers = | Compilers.Coq_ident.Coq_fancy_mullh _ -> None | Compilers.Coq_ident.Coq_fancy_mulhl _ -> None | Compilers.Coq_ident.Coq_fancy_mulhh _ -> None - | Compilers.Coq_ident.Coq_fancy_rshi (log2wordmax, z0) -> - Some (Obj.magic (log2wordmax, (z0, ()))) + | Compilers.Coq_ident.Coq_fancy_rshi (log2wordmax, x) -> + Some (Obj.magic (log2wordmax, (x, ()))) | Compilers.Coq_ident.Coq_fancy_selc -> None | Compilers.Coq_ident.Coq_fancy_selm _ -> None | Compilers.Coq_ident.Coq_fancy_sell -> None diff --git a/src/ExtractionOCaml/unsaturated_solinas.ml b/src/ExtractionOCaml/unsaturated_solinas.ml index 473992c..4d4d604 100644 --- a/src/ExtractionOCaml/unsaturated_solinas.ml +++ b/src/ExtractionOCaml/unsaturated_solinas.ml @@ -40045,7 +40045,7 @@ module Coq2_Compilers = | Compilers.Coq_ident.Literal (t1, v) -> (match t1 with | Compilers.Coq_base.Coq_type.Coq_unit -> - (fun v0 -> Some (Obj.magic (v0, ()))) + (fun x -> Some (Obj.magic (x, ()))) | Compilers.Coq_base.Coq_type.Z -> (fun _ -> None) | Compilers.Coq_base.Coq_type.Coq_bool -> (fun _ -> None) | Compilers.Coq_base.Coq_type.Coq_nat -> (fun _ -> None) @@ -40151,7 +40151,7 @@ module Coq2_Compilers = (match t1 with | Compilers.Coq_base.Coq_type.Coq_unit -> (fun _ -> None) | Compilers.Coq_base.Coq_type.Z -> - (fun v0 -> Some (Obj.magic (v0, ()))) + (fun x -> Some (Obj.magic (x, ()))) | Compilers.Coq_base.Coq_type.Coq_bool -> (fun _ -> None) | Compilers.Coq_base.Coq_type.Coq_nat -> (fun _ -> None) | Compilers.Coq_base.Coq_type.Coq_zrange -> (fun _ -> None)) @@ -40257,7 +40257,7 @@ module Coq2_Compilers = | Compilers.Coq_base.Coq_type.Coq_unit -> (fun _ -> None) | Compilers.Coq_base.Coq_type.Z -> (fun _ -> None) | Compilers.Coq_base.Coq_type.Coq_bool -> - (fun v0 -> Some (Obj.magic (v0, ()))) + (fun x -> Some (Obj.magic (x, ()))) | Compilers.Coq_base.Coq_type.Coq_nat -> (fun _ -> None) | Compilers.Coq_base.Coq_type.Coq_zrange -> (fun _ -> None)) v @@ -40363,7 +40363,7 @@ module Coq2_Compilers = | Compilers.Coq_base.Coq_type.Z -> (fun _ -> None) | Compilers.Coq_base.Coq_type.Coq_bool -> (fun _ -> None) | Compilers.Coq_base.Coq_type.Coq_nat -> - (fun v0 -> Some (Obj.magic (v0, ()))) + (fun x -> Some (Obj.magic (x, ()))) | Compilers.Coq_base.Coq_type.Coq_zrange -> (fun _ -> None)) v | Compilers.Coq_ident.Nat_succ -> None @@ -40469,7 +40469,7 @@ module Coq2_Compilers = | Compilers.Coq_base.Coq_type.Coq_bool -> (fun _ -> None) | Compilers.Coq_base.Coq_type.Coq_nat -> (fun _ -> None) | Compilers.Coq_base.Coq_type.Coq_zrange -> - (fun v0 -> Some (Obj.magic (v0, ())))) v + (fun x -> Some (Obj.magic (x, ())))) v | Compilers.Coq_ident.Nat_succ -> None | Compilers.Coq_ident.Nat_pred -> None | Compilers.Coq_ident.Nat_max -> None @@ -49655,8 +49655,8 @@ module Coq2_Compilers = | Compilers.Coq_ident.Coq_fancy_mullh _ -> None | Compilers.Coq_ident.Coq_fancy_mulhl _ -> None | Compilers.Coq_ident.Coq_fancy_mulhh _ -> None - | Compilers.Coq_ident.Coq_fancy_rshi (log2wordmax, z0) -> - Some (Obj.magic (log2wordmax, (z0, ()))) + | Compilers.Coq_ident.Coq_fancy_rshi (log2wordmax, x) -> + Some (Obj.magic (log2wordmax, (x, ()))) | Compilers.Coq_ident.Coq_fancy_selc -> None | Compilers.Coq_ident.Coq_fancy_selm _ -> None | Compilers.Coq_ident.Coq_fancy_sell -> None diff --git a/src/ExtractionOCaml/word_by_word_montgomery.ml b/src/ExtractionOCaml/word_by_word_montgomery.ml index f955bc6..a672b5d 100644 --- a/src/ExtractionOCaml/word_by_word_montgomery.ml +++ b/src/ExtractionOCaml/word_by_word_montgomery.ml @@ -39944,7 +39944,7 @@ module Coq2_Compilers = | Compilers.Coq_ident.Literal (t1, v) -> (match t1 with | Compilers.Coq_base.Coq_type.Coq_unit -> - (fun v0 -> Some (Obj.magic (v0, ()))) + (fun x -> Some (Obj.magic (x, ()))) | Compilers.Coq_base.Coq_type.Z -> (fun _ -> None) | Compilers.Coq_base.Coq_type.Coq_bool -> (fun _ -> None) | Compilers.Coq_base.Coq_type.Coq_nat -> (fun _ -> None) @@ -40050,7 +40050,7 @@ module Coq2_Compilers = (match t1 with | Compilers.Coq_base.Coq_type.Coq_unit -> (fun _ -> None) | Compilers.Coq_base.Coq_type.Z -> - (fun v0 -> Some (Obj.magic (v0, ()))) + (fun x -> Some (Obj.magic (x, ()))) | Compilers.Coq_base.Coq_type.Coq_bool -> (fun _ -> None) | Compilers.Coq_base.Coq_type.Coq_nat -> (fun _ -> None) | Compilers.Coq_base.Coq_type.Coq_zrange -> (fun _ -> None)) @@ -40156,7 +40156,7 @@ module Coq2_Compilers = | Compilers.Coq_base.Coq_type.Coq_unit -> (fun _ -> None) | Compilers.Coq_base.Coq_type.Z -> (fun _ -> None) | Compilers.Coq_base.Coq_type.Coq_bool -> - (fun v0 -> Some (Obj.magic (v0, ()))) + (fun x -> Some (Obj.magic (x, ()))) | Compilers.Coq_base.Coq_type.Coq_nat -> (fun _ -> None) | Compilers.Coq_base.Coq_type.Coq_zrange -> (fun _ -> None)) v @@ -40262,7 +40262,7 @@ module Coq2_Compilers = | Compilers.Coq_base.Coq_type.Z -> (fun _ -> None) | Compilers.Coq_base.Coq_type.Coq_bool -> (fun _ -> None) | Compilers.Coq_base.Coq_type.Coq_nat -> - (fun v0 -> Some (Obj.magic (v0, ()))) + (fun x -> Some (Obj.magic (x, ()))) | Compilers.Coq_base.Coq_type.Coq_zrange -> (fun _ -> None)) v | Compilers.Coq_ident.Nat_succ -> None @@ -40368,7 +40368,7 @@ module Coq2_Compilers = | Compilers.Coq_base.Coq_type.Coq_bool -> (fun _ -> None) | Compilers.Coq_base.Coq_type.Coq_nat -> (fun _ -> None) | Compilers.Coq_base.Coq_type.Coq_zrange -> - (fun v0 -> Some (Obj.magic (v0, ())))) v + (fun x -> Some (Obj.magic (x, ())))) v | Compilers.Coq_ident.Nat_succ -> None | Compilers.Coq_ident.Nat_pred -> None | Compilers.Coq_ident.Nat_max -> None @@ -49554,8 +49554,8 @@ module Coq2_Compilers = | Compilers.Coq_ident.Coq_fancy_mullh _ -> None | Compilers.Coq_ident.Coq_fancy_mulhl _ -> None | Compilers.Coq_ident.Coq_fancy_mulhh _ -> None - | Compilers.Coq_ident.Coq_fancy_rshi (log2wordmax, z0) -> - Some (Obj.magic (log2wordmax, (z0, ()))) + | Compilers.Coq_ident.Coq_fancy_rshi (log2wordmax, x) -> + Some (Obj.magic (log2wordmax, (x, ()))) | Compilers.Coq_ident.Coq_fancy_selc -> None | Compilers.Coq_ident.Coq_fancy_selm _ -> None | Compilers.Coq_ident.Coq_fancy_sell -> None ``` --- src/GENERATEDIdentifiersWithoutTypesProofs.v | 472 ++++++++++++++++++++++++--- 1 file changed, 419 insertions(+), 53 deletions(-) (limited to 'src/GENERATEDIdentifiersWithoutTypesProofs.v') diff --git a/src/GENERATEDIdentifiersWithoutTypesProofs.v b/src/GENERATEDIdentifiersWithoutTypesProofs.v index 2bab688dc..7c3ec0e35 100644 --- a/src/GENERATEDIdentifiersWithoutTypesProofs.v +++ b/src/GENERATEDIdentifiersWithoutTypesProofs.v @@ -1,6 +1,7 @@ Require Import Coq.ZArith.ZArith. Require Import Coq.MSets.MSetPositive. Require Import Coq.FSets.FMapPositive. +Require Import Crypto.Util.PrimitiveSigma. Require Import Crypto.Util.MSetPositive.Facts. Require Import Crypto.Util.CPSNotations. Require Import Crypto.Util.ZRange. @@ -9,6 +10,8 @@ Require Import Crypto.Util.Tactics.DestructHead. Require Import Crypto.Util.Option. Require Import Crypto.Util.Decidable. Require Import Crypto.Util.HProp. +Require Import Crypto.Util.Equality. +Require Import Crypto.Util.Tactics.SpecializeBy. Require Import Crypto.Language. Require Import Crypto.LanguageInversion. Require Import Crypto.GENERATEDIdentifiersWithoutTypes. @@ -17,6 +20,7 @@ Require Import Crypto.Util.FixCoqMistakes. Import EqNotations. Module Compilers. Import Language.Compilers. + Import LanguageInversion.Compilers. Import GENERATEDIdentifiersWithoutTypes.Compilers. Module pattern. @@ -59,14 +63,24 @@ Module Compilers. -> P v. Proof. destruct v'; congruence. Qed. + Local Notation type_of_list := (List.fold_right (fun A B => prod A B) unit). + Fixpoint eta_type_of_list {ls} : type_of_list ls -> type_of_list ls + := match ls with + | nil => fun _ => tt + | cons x xs => fun v => (fst v, @eta_type_of_list xs (snd v)) + end. + Lemma eq_eta_type_of_list ls v + : @eta_type_of_list ls v = v. + Proof. induction ls; destruct v; cbn; reflexivity + apply f_equal; auto with nocore. Defined. + Module base. - Definition eq_subst_default_relax {t evm} : base.subst_default (base.relax t) evm = t. + Fixpoint eq_subst_default_relax {t evm} : base.subst_default (base.relax t) evm = t. Proof. - induction t; cbn; + destruct t; cbn; first [ reflexivity | apply f_equal | apply f_equal2 ]; - assumption. + auto with nocore. Defined. End base. @@ -79,6 +93,93 @@ Module Compilers. Defined. End type. + Local Lemma fast_sig_forall1_eq_ind {A T g} + (P : { f : forall a : A, T a | forall a, f a = g a } -> Type) + : (forall x : forall a, { f : T a | f = g a }, + P (exist (fun f => forall a, f a = g a) + (fun a => proj1_sig (x a)) + (fun a => proj2_sig (x a)))) + -> forall x, P x. + Proof. + intros H [x p]; refine (H (fun a => exist _ (x a) (p a))). + Defined. + + Local Lemma fast_sig_forall2_eq_ind {A B T g} + (P : { f : forall (a : A) (b : B a), T a b | forall a b, f a b = g a b } -> Type) + : (forall x : forall a b, { f : T a b | f = g a b }, + P (exist (fun f => forall a b, f a b = g a b) + (fun a b => proj1_sig (x a b)) + (fun a b => proj2_sig (x a b)))) + -> forall x, P x. + Proof. + intros H [x p]; refine (H (fun a b => exist _ (x a b) (p a b))). + Defined. + + Local Ltac my_generalize_dependent_intros v := + let k := fresh in + set (k := v) in *; clearbody k. + Ltac my_prerevert_dependent H := (* apparently this is faster *) + move H at bottom; + repeat lazymatch goal with H' : _ |- _ => tryif constr_eq H H' then fail else revert H' end. + Local Ltac generalize_proj1_sig_step := + match goal with + | [ |- context[@proj1_sig _ (fun x => forall y, _ = _) ?p] ] + => tryif is_var p then fail else my_generalize_dependent_intros p + | [ |- context[@proj1_sig _ (fun x => forall y z, _ = _) ?p] ] + => tryif is_var p then fail else my_generalize_dependent_intros p + | [ H : context[@proj1_sig _ (fun x => forall y, _ = _) ?p] |- _ ] + => tryif is_var p then fail else my_generalize_dependent_intros p + | [ H : context[@proj1_sig _ (fun x => forall y z, _ = _) ?p] |- _ ] + => tryif is_var p then fail else my_generalize_dependent_intros p + end. + Local Ltac specialize_sig_step := + match goal with + | [ H : { f : forall (a : ?A), @?T a | forall a', f a' = @?g a' } |- _ ] + => my_prerevert_dependent H; + revert H; + let P := lazymatch goal with |- forall x, @?P x => P end in + refine (@fast_sig_forall1_eq_ind A T g P _); + cbn [proj1_sig proj2_sig]; intros + | [ H : { f : forall (a : ?A) (b : @?B a), @?T a b | forall a' b', f a' b' = @?g a' b' } |- _ ] + => my_prerevert_dependent H; + revert H; + let P := lazymatch goal with |- forall x, @?P x => P end in + refine (@fast_sig_forall2_eq_ind A B T g P _); + cbn [proj1_sig proj2_sig]; intros + end. + Local Ltac rewrite_sig_step := + match goal with + | [ p : forall t idc, sig (fun y => y = _) |- _ ] + => lazymatch goal with + | [ H : context[proj1_sig (p ?t ?idc)] |- _ ] => destruct (p t idc) + | [ |- context[proj1_sig (p ?t ?idc)] ] => destruct (p t idc) + end; + subst; cbn [proj1_sig proj2_sig] in *; try clear p + | [ p : forall idc, sig (fun y => y = _) |- _ ] + => lazymatch goal with + | [ H : context[proj1_sig (p ?idc)] |- _ ] => destruct (p idc) + | [ |- context[proj1_sig (p ?idc)] ] => destruct (p idc) + end; + subst; cbn [proj1_sig proj2_sig] in *; try clear p + | [ p : sig (fun y => y = _) |- _ ] + => destruct p; subst; cbn [proj1_sig proj2_sig] in * + end. + Local Ltac clear_useless_step := + match goal with + | [ H : forall t, { f : _ | f = _ } |- _ ] => clear H + | [ H : forall t idc, { f : _ | f = _ } |- _ ] => clear H + end. + + Local Ltac do_rew_proj2_sig := + repeat first [ progress cbn [eq_rect eq_sym] in * + | progress intros + | clear_useless_step + | rewrite_sig_step + | specialize_sig_step + | generalize_proj1_sig_step ]. + + Local Notation iffT x y := ((x -> y) * (y -> x))%type. + Module Raw. Module ident. Import GENERATEDIdentifiersWithoutTypes.Compilers.pattern.Raw.ident. @@ -87,22 +188,106 @@ Module Compilers. Global Instance eq_ident_Decidable : DecidableRel (@eq ident) := dec_rel_of_bool_dec_rel ident_beq ident_bl ident_lb. + Lemma is_simple_correct0 p + : is_simple p = true + <-> (forall f1 f2, type_of p f1 = type_of p f2). + Proof. + destruct p; cbn; cbv -[Datatypes.fst Datatypes.snd projT1 projT2] in *; split; intro H; + try solve [ reflexivity | exfalso; discriminate ]. + all: repeat first [ match goal with + | [ H : nat -> ?A |- _ ] => specialize (H O) + | [ H : unit -> ?A |- _ ] => specialize (H tt) + | [ H : forall x y : PrimitiveProd.Primitive.prod _ _, _ |- _ ] => specialize (fun x1 y1 x2 y2 => H (PrimitiveProd.Primitive.pair x1 x2) (PrimitiveProd.Primitive.pair y1 y2)); cbn in H + | [ H : forall x y : Datatypes.prod _ _, _ |- _ ] => specialize (fun x1 y1 x2 y2 => H (Datatypes.pair x1 x2) (Datatypes.pair y1 y2)); cbn in H + | [ H : forall x y : PrimitiveSigma.Primitive.sigT ?P, _ |- _ ] => specialize (fun x1 y1 x2 y2 => H (PrimitiveSigma.Primitive.existT P x1 x2) (PrimitiveSigma.Primitive.existT P y1 y2)); cbn in H + | [ H : forall x y : Compilers.base.type, _ |- _ ] => specialize (fun x y => H (Compilers.base.type.type_base x) (Compilers.base.type.type_base y)) + | [ H : forall x y : Compilers.base.type.base, _ |- _ ] => specialize (H Compilers.base.type.unit Compilers.base.type.nat); try congruence; cbn in H + end + | congruence ]. + Qed. + + Lemma invert_bind_args_to_typed p f + : invert_bind_args (to_typed p f) p = Some f. + Proof. + destruct p; cbv in *; + destruct_head' (@Primitive.sigT); destruct_head'_prod; destruct_head'_unit; reflexivity. + Qed. + + Lemma fold_invert_bind_args : @invert_bind_args = @folded_invert_bind_args. + Proof. reflexivity. Qed. + + Lemma split_ident_to_ident ridc x y z + : PrimitiveSigma.Primitive.projT1 (split_ident_gen (to_ident (ident_infos_of ridc) x y z)) + = ridc. + Proof. destruct ridc; reflexivity. Defined. + + Lemma eq_indep_types_of_eq_types (ridc : ident) + (dt1 dt2 : type_of_list (dep_types (ident_infos_of ridc))) + (idt1 idt2 : type_of_list_of_kind (indep_types (ident_infos_of ridc))) + (Hty : to_type (ident_infos_of ridc) dt1 idt1 = to_type (ident_infos_of ridc) dt2 idt2) + : idt1 = idt2. + Proof. + destruct ridc; cbv in *; + destruct_head'_prod; destruct_head'_unit; try reflexivity; + type.inversion_type; reflexivity. + Qed. + + Lemma ident_transport_opt_correct P x y v + : (@ident_transport_opt P x y v <> None -> x = y) + * (forall pf : x = y, @ident_transport_opt P x y v = Some (rew pf in v)). + Proof. + cbv [ident_transport_opt]. + generalize (ident_beq_if x y), (ident_lb x y); destruct (ident_beq x y); + intros; subst; split; try congruence; intros; subst; + try intuition congruence. + eliminate_hprop_eq; reflexivity. + Qed. + + Lemma ident_transport_opt_correct' P x y v + : @ident_transport_opt P x y v <> None + -> { pf : x = y + | @ident_transport_opt P x y v = Some (rew pf in v) }. + Proof. + intro H; apply ident_transport_opt_correct in H; exists H; apply ident_transport_opt_correct. + Qed. + + Lemma ident_transport_opt_correct'' P x y v v' + : @ident_transport_opt P x y v = Some v' + -> { pf : x = y + | v' = rew pf in v }. + Proof. + intro H. + pose proof (@ident_transport_opt_correct' P x y v) as H'. + rewrite H in H'. + specialize (H' ltac:(congruence)). + destruct H'; inversion_option; subst; (exists eq_refl); 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. - cbv [invert_bind_args type_of full_types]. - repeat first [ reflexivity - | (exists eq_refl) - | progress intros - | match goal with - | [ H : Some _ = None |- ?P ] => exact (@quick_invert_eq_option _ P _ _ H) - | [ H : None = Some _ |- ?P ] => exact (@quick_invert_eq_option _ P _ _ H) - end - | progress inversion_option - | progress subst - | break_innermost_match_step - | break_innermost_match_hyps_step ]. + rewrite fold_invert_bind_args. + cbv [folded_invert_bind_args type_of full_types to_typed] in *. + do_rew_proj2_sig. + all: repeat first [ match goal with + | [ |- context[@split_ident_gen ?t ?idc] ] + => destruct (@split_ident_gen t idc) + | [ H : context[@split_ident_gen ?t ?idc] |- _ ] + => destruct (@split_ident_gen t idc) + | [ H : Some _ = @ident_transport_opt _ _ _ _ |- _ ] => symmetry in H + | [ H : None = @ident_transport_opt _ _ _ _ |- _ ] => symmetry in H + | [ H : @ident_transport_opt ?P ?x ?y ?v = Some _ |- _ ] + => apply (@ident_transport_opt_correct'' P x y v) in H; destruct H + | [ H : @ident_transport_opt ?P ?x ?y ?v = None |- _ ] + => repeat intro; unshelve (erewrite (Datatypes.snd (ident_transport_opt_correct P x y v)) in H; inversion_option); [] + end + | progress destruct_head'_sig + | progress subst + | progress cbv [eq_rect assemble_ident] in * + | (exists eq_refl) + | reflexivity + | break_innermost_match_step ]. Qed. Lemma type_of_invert_bind_args t idc p f @@ -117,33 +302,6 @@ Module Compilers. exact (proj2_sig (@to_typed_invert_bind_args_gen t idc p f pf)). Defined. - Lemma invert_bind_args_to_typed p f - : invert_bind_args (to_typed p f) p = Some f. - Proof. - destruct p; cbn in *; - repeat first [ reflexivity - | progress destruct_head'_unit - | progress destruct_head'_prod - | progress destruct_head' (@PrimitiveSigma.Primitive.sigT) ]. - Qed. - - Lemma is_simple_correct0 p - : is_simple p = true - <-> (forall f1 f2, type_of p f1 = type_of p f2). - Proof. - destruct p; cbn; split; intro H; - try solve [ reflexivity | exfalso; discriminate ]. - all: repeat first [ match goal with - | [ H : nat -> ?A |- _ ] => specialize (H O) - | [ H : unit -> ?A |- _ ] => specialize (H tt) - | [ H : forall x y : Datatypes.prod _ _, _ |- _ ] => specialize (fun x1 y1 x2 y2 => H (Datatypes.pair x1 x2) (Datatypes.pair y1 y2)); cbn in H - | [ H : forall x y : PrimitiveSigma.Primitive.sigT ?P, _ |- _ ] => specialize (fun x1 y1 x2 y2 => H (PrimitiveSigma.Primitive.existT P x1 x2) (PrimitiveSigma.Primitive.existT P y1 y2)); cbn in H - | [ H : forall x y : Compilers.base.type, _ |- _ ] => specialize (fun x y => H (Compilers.base.type.type_base x) (Compilers.base.type.type_base y)) - | [ H : forall x y : Compilers.base.type.base, _ |- _ ] => specialize (H Compilers.base.type.unit Compilers.base.type.nat); try congruence; cbn in H - end - | congruence ]. - Qed. - Lemma is_simple_correct p : is_simple p = true <-> (forall t1 idc1 t2 idc2, @invert_bind_args t1 idc1 p <> None -> @invert_bind_args t2 idc2 p <> None -> t1 = t2). @@ -157,6 +315,64 @@ Module Compilers. apply (H _ (to_typed p f1) _ (to_typed p f2)); rewrite invert_bind_args_to_typed; congruence. } Qed. + + Lemma try_unify_split_args_Some_correct ridc1 ridc2 dt1 dt2 (*idt1 idt2*) args v + : iffT + (@try_unify_split_args ridc1 ridc2 dt1 dt2 (*idt1 idt2*) args = Some v) + { pf : existT _ ridc1 dt1 = existT _ ridc2 dt2 :> { ridc : _ & type_of_list (dep_types (preinfos (ident_infos_of ridc))) } + | (rew [fun rdt => type_of_list (indep_args _ (projT2 rdt))] pf in + (args : type_of_list (indep_args _ (projT2 (existT _ ridc1 dt1))))) + = v + (*/\ (rew [fun ridc => type_of_list_of_kind (indep_types (preinfos (ident_infos_of ridc)))] f_equal (@projT1 _ _) pf in + idt1) + = idt2*) }. + Proof. + pose proof (dep_types_dec_transparent (ident_infos_of ridc1) : DecidableRel eq). + cbv [try_unify_split_args]. + generalize (Raw.ident.ident_beq_if ridc1 ridc2). + generalize (Raw.ident.ident_lb ridc1 ridc2). + destruct (Raw.ident.ident_beq ridc1 ridc2); + [ + | split; + [ congruence + | intros; destruct_head'_sig; Sigma.inversion_sigma; subst; specialize_by reflexivity; congruence ] ]. + intros ? ?; subst. + (*pose proof (@Reflect.reflect_bool _ _ (indep_types_reflect _ idt1 idt2)) as H'. + pose proof (indep_types_reflect _ idt1 idt2) as H''.*) + repeat first [ break_innermost_match_step + | apply pair + | progress intros + | progress inversion_option + | progress subst + | progress specialize_by reflexivity + | apply conj + | progress destruct_head'_and + | progress destruct_head'_sig + | progress Sigma.inversion_sigma + | progress cbn [eq_rect eq_sym eq_rect_r Sigma.path_sigT Sigma.path_sigT_uncurried f_equal] in * + | (exists eq_refl) + | reflexivity + | progress eliminate_hprop_eq + | match goal with + | [ H : Bool.reflect _ false |- _ ] => inversion H; clear H + end + | congruence ]. + Qed. + + Lemma try_unify_split_args_None_correct ridc1 ridc2 dt1 dt2 (*idt1 idt2*) args + : @try_unify_split_args ridc1 ridc2 dt1 dt2 (*idt1 idt2*) args = None + -> forall pf : existT _ ridc1 dt1 = existT _ ridc2 dt2 :> { ridc : _ & type_of_list (dep_types (preinfos (ident_infos_of ridc))) }, + (*(rew [fun ridc => type_of_list_of_kind (indep_types (preinfos (ident_infos_of ridc)))] f_equal (@projT1 _ _) pf in + idt1) + = idt2 + ->*) False. + Proof. + intros H pf (*pf'*). + pose proof (fun v => snd (@try_unify_split_args_Some_correct ridc1 ridc2 dt1 dt2 (*idt1 idt2*) args v)) as H'. + rewrite H in H'. + specialize (H' _ (exist _ pf eq_refl(*(conj eq_refl pf')*))); cbv beta in *. + congruence. + Qed. End ident. End Raw. @@ -164,30 +380,180 @@ Module Compilers. Import GENERATEDIdentifiersWithoutTypes.Compilers.pattern.ident. Import Datatypes. (* for Some, None, option *) + Lemma fold_eta_ident_cps T t idc f : @eta_ident_cps T t idc f = proj1_sig (@pattern.eta_ident_cps_gen (fun t _ => T t) f) t idc. + Proof. reflexivity. Qed. + + Lemma fold_unify : @unify = @folded_unify. + Proof. vm_cast_no_check (eq_refl (@unify)). Qed. + + Lemma to_typed_of_typed_ident t idc evm + : (rew [Compilers.ident] type.eq_subst_default_relax in + @to_typed _ (@of_typed_ident t idc) evm (@arg_types_of_typed_ident t idc)) + = idc. + Proof. + destruct idc; + try (vm_compute; reflexivity); + cbv -[type.type_ind type.relax type.subst_default Compilers.base.type.type_ind f_equal f_equal2 base.relax base.subst_default base.eq_subst_default_relax]; + cbn [type.type_ind type.relax type.subst_default f_equal f_equal2 base.relax base.subst_default base.eq_subst_default_relax]; + repeat first [ progress subst + | progress intros + | progress cbn [f_equal f_equal2] + | reflexivity + | match goal with + | [ |- context[@base.eq_subst_default_relax ?t ?evm] ] + => generalize (base.subst_default (base.relax t) evm), (@base.eq_subst_default_relax t evm) + end ]. + Qed. + + Lemma eq_indep_types_of_eq_types {t1 t2} {idc1 : ident t1} {idc2 : ident t2} evm1 evm2 + (Hty : type.subst_default t1 evm1 = type.subst_default t2 evm2) + (pf : Primitive.projT1 (@split_types_subst_default _ idc1 evm1) + = Primitive.projT1 (@split_types_subst_default _ idc2 evm2)) + : Datatypes.snd (Primitive.projT2 (@split_types_subst_default _ idc1 evm1)) + = rew <- [fun r => full_type_of_list_of_kind (Raw.ident.indep_types (Raw.ident.preinfos (Raw.ident.ident_infos_of r)))] pf in + Datatypes.snd (Primitive.projT2 (@split_types_subst_default _ idc2 evm2)). + Proof. + pose proof (@to_type_split_types_subst_default_eq _ idc1 evm1). + pose proof (@to_type_split_types_subst_default_eq _ idc2 evm2). + generalize dependent (type.subst_default t1 evm1); + generalize dependent (type.subst_default t2 evm2); intros; subst. + cbv [split_types_subst_default] in *; cbn [Primitive.projT1 Primitive.projT2 fst snd] in *. + destruct (split_types idc1), (split_types idc2); + destruct_head'_prod; + cbn [Primitive.projT1 Primitive.projT2 fst snd] in *; + subst; cbn [eq_rect eq_rect_r eq_sym]. + eapply Raw.ident.eq_indep_types_of_eq_types; eassumption. + Qed. + 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. + Proof. rewrite fold_eta_ident_cps; apply (proj2_sig (@pattern.eta_ident_cps_gen _ f)). Qed. Lemma unify_to_typed {t t' pidc idc} : forall v, @unify t t' pidc idc = Some v -> forall evm pf, - rew [Compilers.ident] pf in @to_typed t pidc evm v = idc. + rew [Compilers.ident] pf in @to_typed t pidc evm v = idc. Proof. - refine (@option_case_fast _ _ _ _). - Time destruct pidc, idc; cbv [unify to_typed]; try exact I. - Time all: break_innermost_match; try exact I. - Time all: repeat first [ reflexivity - | progress intros - | progress eliminate_hprop_eq - | progress cbn [type.subst_default base.subst_default] in * - | progress Compilers.type.inversion_type ]. + intros v H evm pf; subst t'; cbn [eq_rect]. + pose proof (@eq_indep_types_of_eq_types _ _ (@of_typed_ident _ idc) pidc evm evm type.eq_subst_default_relax) as H'. + revert v H. + set (idc' := idc) at 1; rewrite <- (@to_typed_of_typed_ident _ idc evm); subst idc'. + rewrite fold_unify. + cbv [folded_unify arg_types Raw.ident.assemble_ident]; + cbn [Primitive.projT1 Primitive.projT2]. + intros v. + Time do_rew_proj2_sig. + Time + repeat first [ progress cbn [eq_rect eq_sym] in * + | progress cbn [Primitive.projT1 Primitive.projT2 fst snd] in * + | clear_useless_step + | rewrite_sig_step + | specialize_sig_step + | generalize_proj1_sig_step + | progress cbv [to_typed Raw.ident.assemble_ident] in * + | match goal with + | [ |- context[@arg_types_of_typed_ident _ ?idc] ] + => is_var idc; + generalize dependent (@arg_types_of_typed_ident _ idc); + generalize dependent (@of_typed_ident _ idc); + clear idc; + intros + end + | progress cbv [arg_types prearg_types] in * ]. + repeat first [ progress cbn [Primitive.projT1 Primitive.projT2 fst snd] in * + | match goal with + | [ |- context[(rew [fun x : ?T => @?A x -> @?B x] ?pf in ?f) ?y] ] + => rewrite (@push_rew_fun_dep T A B _ _ pf f y) + | [ |- context[rew [fun _ : ?T => ?P] ?pf in ?f] ] + => rewrite (@Equality.transport_const T P _ _ pf f) + | [ |- context[(rew [?P] ?pf in ?x) = ?y] ] + => rewrite <- (@eq_rew_moveR _ P _ _ pf x y) + | [ |- context[rew [fun x : ?T => option (@?P x)] ?pf in Some ?v] ] + => rewrite <- (@commute_eq_rect _ P (fun x => option (P x)) (fun _ => Some) _ _ pf v) + | [ |- iffT (Raw.ident.try_unify_split_args _ (*_ _*) = Some _) _ ] + => eapply iffT_trans; [ apply Raw.ident.try_unify_split_args_Some_correct | ] + | [ H : Raw.ident.try_unify_split_args _ (*_ _*) = Some _ |- _ ] + => apply Raw.ident.try_unify_split_args_Some_correct in H + | [ |- context[to_type_split_types_subst_default_eq ?t ?i ?evm] ] + => generalize (to_type_split_types_subst_default_eq t i evm); intro + end + | progress cbv [eq_rect_r] in * + | progress cbv [split_types_subst_default] in * + | progress cbn [eq_rect] in * + | progress destruct_head'_prod + | progress subst + | match goal with + | [ |- context[existT _ (Primitive.projT1 (split_types ?x)) _ = _] ] + => destruct (split_types x); clear x + | [ H : context[existT _ (Primitive.projT1 (split_types ?x)) _ = _] |- _ ] + => destruct (split_types x); clear x + | [ |- context[@eq_trans (type.type ?base_type) ?x ?y ?z ?pf1 ?pf2] ] + => generalize (@eq_trans (type.type base_type) x y z pf1 pf2); intro + end + | rewrite <- !eq_trans_rew_distr ]. + Time + all: + repeat first [ apply pair + | progress cbn [eq_rect eq_rect_r eq_sym Sigma.path_sigT Sigma.path_sigT_uncurried f_equal] in * + | progress intros + | progress destruct_head'_sig + | progress destruct_head'_ex + | progress destruct_head'_and + | progress Sigma.inversion_sigma + | progress subst + | match goal with + | [ H : forall pf : ?x = ?x, _ |- _ ] => specialize (H eq_refl) + | [ H : lift_type_of_list_map _ ?f = _ |- _ ] + => is_var f; symmetry in H; destruct H; clear f + | [ H : context[@eq_trans (type.type ?base_type) ?x ?y ?z ?pf1 ?pf2] |- _ ] + => generalize dependent (@eq_trans (type.type base_type) x y z pf1 pf2); intros + | [ H : context[type.subst_default (type.relax _) _] |- _ ] + => rewrite type.eq_subst_default_relax in H + | [ H : ?x = ?x |- _ ] => clear H + | [ H : type.subst_default ?t ?evm = type.subst_default ?t ?evm' + |- context[lift_type_of_list_map (@subst_default_kind_of_type ?evm) (snd (Primitive.projT2 (split_types ?idc)))] ] + => let H' := fresh in + pose proof (@eq_indep_types_of_eq_types t idc idc evm evm' H eq_refl) as H'; + cbv [split_types_subst_default] in H'; + cbn [eq_rect_r eq_rect eq_sym Primitive.projT2 Primitive.projT1 fst snd] in H'; + rewrite H' in *; clear H'; + generalize dependent (type.subst_default t evm); intros; subst; clear evm + end + | rewrite <- !eq_trans_rew_distr in * + | eexists; rewrite <- !eq_trans_rew_distr, concat_pV + | match goal with + | [ H : _ = type.subst_default ?t ?evm |- _ ] + => is_var t; is_var evm; + generalize dependent (type.subst_default t evm); intros + end + | progress eliminate_hprop_eq ]. Qed. Lemma unify_of_typed_ident {t idc} : unify (@of_typed_ident t idc) idc <> None. Proof. - destruct idc; cbn; break_innermost_match; exact Some_neq_None. + rewrite fold_unify. + cbv [folded_unify]. + Time do_rew_proj2_sig. + generalize (of_typed_ident idc), (arg_types_of_typed_ident idc); intros. + repeat first [ progress rewrite ?push_rew_fun_dep, ?transport_const + | progress cbv [eq_rect_r] in * + | intro + | match goal with + | [ H : (rew [?P] ?pf in ?v) = ?v2 |- _ ] => apply (@rew_r_moveL _ P _ _ pf v v2) in H + | [ H : context[rew [fun x : ?T => option (@?P x)] ?pf in @None ?K] |- _ ] + => let H' := fresh in + pose proof (@commute_eq_rect _ (fun _ => True) (fun x => option (P x)) (fun _ _ => @None _) _ _ pf I) as H'; + setoid_rewrite <- H' in H; + clear H' + | [ H : @Raw.ident.try_unify_split_args ?a ?b ?c ?d ?e = None |- _ ] + => let H' := fresh in + pose proof (@Raw.ident.try_unify_split_args_None_correct a b c d e H) as H'; + clear H + | [ H : forall pf : _ = _, _ |- _ ] => specialize (H eq_refl) + end + | assumption ]. Qed. End ident. End pattern. -- cgit v1.2.3