diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/Reflection/BoundByCastInterp.v | 119 | ||||
| -rw-r--r-- | src/Reflection/EtaInterp.v | 33 | ||||
| -rw-r--r-- | src/Reflection/InterpByIsoProofs.v | 26 | ||||
| -rw-r--r-- | src/Reflection/Relations.v | 31 | ||||
| -rw-r--r-- | src/Reflection/SmartBound.v | 3 | ||||
| -rw-r--r-- | src/Reflection/SmartBoundInterp.v | 146 | ||||
| -rw-r--r-- | src/Reflection/SmartMap.v | 50 | ||||
| -rw-r--r-- | src/Reflection/Z/Syntax/Util.v | 18 |
8 files changed, 421 insertions, 5 deletions
diff --git a/src/Reflection/BoundByCastInterp.v b/src/Reflection/BoundByCastInterp.v new file mode 100644 index 000000000..2eda88a78 --- /dev/null +++ b/src/Reflection/BoundByCastInterp.v @@ -0,0 +1,119 @@ +Require Import Crypto.Reflection.Syntax. +Require Import Crypto.Reflection.InterpWfRel. +Require Import Crypto.Reflection.TypeUtil. +Require Import Crypto.Reflection.Relations. +Require Import Crypto.Reflection.Wf. +Require Import Crypto.Reflection.BoundByCast. +Require Import Crypto.Reflection.SmartBound. +Require Import Crypto.Reflection.SmartBoundInterp. +Require Import Crypto.Reflection.SmartBoundWf. +Require Import Crypto.Reflection.InlineCastInterp. +Require Import Crypto.Reflection.ExprInversion. +Require Import Crypto.Reflection.InlineInterp. +Require Import Crypto.Reflection.LinearizeInterp. +Require Import Crypto.Reflection.LinearizeWf. +Require Import Crypto.Reflection.MapCastInterp. +Require Import Crypto.Reflection.MapCastWf. +Require Import Crypto.Reflection.EtaInterp. + +Local Open Scope expr_scope. +Local Open Scope ctype_scope. +Section language. + Context {base_type_code : Type} + {op : flat_type base_type_code -> flat_type base_type_code -> Type} + (interp_base_type interp_base_type_bounds : base_type_code -> Type) + (interp_op : forall src dst, op src dst -> interp_flat_type interp_base_type src -> interp_flat_type interp_base_type dst) + (interp_op_bounds : forall src dst, op src dst -> interp_flat_type interp_base_type_bounds src -> interp_flat_type interp_base_type_bounds dst) + (bound_base_type : forall t, interp_base_type_bounds t -> base_type_code) + (base_type_beq : base_type_code -> base_type_code -> bool) + (base_type_bl_transparent : forall x y, base_type_beq x y = true -> x = y) + (base_type_leb : base_type_code -> base_type_code -> bool) + (Cast : forall var A A', exprf base_type_code op (var:=var) (Tbase A) -> exprf base_type_code op (var:=var) (Tbase A')) + (cast_val : forall A A', interp_base_type A -> interp_base_type A') + (is_cast : forall src dst, op src dst -> bool) + (is_const : forall src dst, op src dst -> bool) + (genericize_op : forall src dst (opc : op src dst) (new_bounded_type_in new_bounded_type_out : base_type_code), + option { src'dst' : _ & op (fst src'dst') (snd src'dst') }) + (failf : forall var t, @exprf base_type_code op var (Tbase t)) + (bound_is_good : forall t, interp_base_type_bounds t -> Prop) + (is_bounded_by_base : forall t, interp_base_type t -> interp_base_type_bounds t -> Prop) + (interpf_Cast_id : forall A x, interpf interp_op (Cast _ A A x) = interpf interp_op x) + (interpf_cast : forall A A' e, interpf interp_op (Cast _ A A' e) = cast_val A A' (interpf interp_op e)) + (cast_val_squash : forall a b c v, + base_type_min base_type_leb b (base_type_min base_type_leb a c) = base_type_min base_type_leb a c + -> cast_val b c (cast_val a b v) = cast_val a c v) + (is_cast_correct : forall s d opc e, is_cast (Tbase s) (Tbase d) opc = true + -> interp_op _ _ opc (interpf interp_op e) + = interpf interp_op (Cast _ s d e)) + (wff_Cast : forall var1 var2 G A A' e1 e2, + wff G e1 e2 -> wff G (Cast var1 A A' e1) (Cast var2 A A' e2)) + (strip_cast_val + : forall t x y, + is_bounded_by_base t y x -> + cast_val (bound_base_type t x) t (cast_val t (bound_base_type t x) y) = y). + Local Notation is_bounded_by (*{T} : interp_flat_type interp_base_type T -> interp_flat_type interp_base_type_bounds T -> Prop*) + := (interp_flat_type_rel_pointwise is_bounded_by_base). + Context (is_bounded_by_interp_op + : forall src dst opc sv1 sv2, + is_bounded_by sv1 sv2 -> + is_bounded_by (interp_op src dst opc sv1) (interp_op_bounds src dst opc sv2)). + Local Notation bounds_are_good + := (@interp_flat_type_rel_pointwise1 _ _ bound_is_good). + Local Notation bound_op := (@bound_op _ _ _ interp_op_bounds bound_base_type _ base_type_bl_transparent base_type_leb Cast genericize_op). + Local Notation G_invariant_holds G + := (forall t x x', + List.In (existT _ t (x, x')%core) G -> is_bounded_by_base t x x') + (only parsing). + Context (interpf_bound_op + : forall G t tR opc ein eout ebounds, + wff G ein ebounds + -> G_invariant_holds G + -> interpf interp_op ein = interpf interp_op eout + -> bounds_are_recursively_good interp_op_bounds bound_is_good ebounds + -> bounds_are_good (interp_op_bounds t tR opc (interpf interp_op_bounds ebounds)) + -> interpf interp_op (@bound_op interp_base_type t tR t tR opc opc eout (interpf interp_op_bounds ebounds)) + = interpf interp_op (Op opc ein)). + + Context (is_bounded_by_bound_op + : forall G t tR opc ein eout ebounds, + wff G ein ebounds + -> G_invariant_holds G + -> interpf interp_op ein = interpf interp_op eout + -> bounds_are_recursively_good interp_op_bounds bound_is_good ebounds + -> bounds_are_good (interp_op_bounds t tR opc (interpf interp_op_bounds ebounds)) + -> is_bounded_by + (interpf interp_op (@bound_op interp_base_type t tR t tR opc opc eout (interpf interp_op_bounds ebounds))) + (interpf interp_op_bounds (Op opc ebounds))). + + Local Notation Expr := (@Expr base_type_code op). + Local Notation Boundify := (@Boundify _ _ _ interp_op_bounds bound_base_type _ base_type_bl_transparent base_type_leb Cast is_cast is_const genericize_op failf). + Local Notation interpf_smart_unbound := (@interpf_smart_unbound _ interp_base_type_bounds bound_base_type interp_base_type cast_val). + + (* + Lemma InterpBoundifyAndRel {t} + (e : Expr t) + (Hwf : Wf e) + (input_bounds : interp_flat_type interp_base_type_bounds (domain t)) + (output_bounds := Interp interp_op_bounds e input_bounds) + (e' := Boundify e input_bounds) + (Hgood : bounds_are_recursively_good + (@interp_op_bounds) bound_is_good + (invert_Abs (e _) input_bounds)) + : forall x, + is_bounded_by (interpf_smart_unbound input_bounds x) input_bounds + -> is_bounded_by (Interp interp_op e (interpf_smart_unbound input_bounds x)) output_bounds + /\ interpf_smart_unbound _ (Interp interp_op e' x) + = Interp interp_op e (interpf_smart_unbound input_bounds x). + Proof. + intros; subst e' output_bounds. + unfold Boundify. + erewrite InterpExprEta, InterpInlineCast, InterpLinearize by eauto with wf. + match goal with |- ?A /\ ?B => cut (A /\ (A -> B)); [ tauto | ] end. + split. + { apply interp_wf; auto. } + { intro Hbounded_out. + erewrite InterpSmartBound, InterpMapInterpCast by eauto with wf. + reflexivity. } + Qed. +*) +End language. diff --git a/src/Reflection/EtaInterp.v b/src/Reflection/EtaInterp.v index 95732ad3d..54240947a 100644 --- a/src/Reflection/EtaInterp.v +++ b/src/Reflection/EtaInterp.v @@ -1,5 +1,6 @@ Require Import Crypto.Reflection.Syntax. Require Import Crypto.Reflection.Eta. +Require Import Crypto.Reflection.Relations. Require Import Crypto.Reflection.ExprInversion. Require Import Crypto.Util.Tactics.BreakMatch. Require Import Crypto.Util.Tactics.DestructHead. @@ -37,11 +38,31 @@ Section language. (* Local *) Hint Rewrite @eq_interp_flat_type_eta_gen. + Section gen_type. + Context (exprf_eta : forall {t} (e : exprf t), exprf t) + (eq_interp_exprf_eta : forall t e, interpf (@interp_op) (@exprf_eta t e) = interpf (@interp_op) e). + Lemma interp_expr_eta_gen {t e} + : interp_type_gen_rel_pointwise + (fun _ => eq) + (interp (@interp_op) (expr_eta_gen eta exprf_eta (t:=t) e)) + (interp (@interp_op) e). + Proof. t. Admitted. + End gen_type. + (* Local *) Hint Rewrite @interp_expr_eta_gen. + Lemma interpf_exprf_eta_gen {t e} : interpf (@interp_op) (exprf_eta_gen eta (t:=t) e) = interpf (@interp_op) e. Proof. induction e; t. Qed. + + Lemma InterpExprEtaGen {t e} + : interp_type_gen_rel_pointwise + (fun _ => eq) + (Interp (@interp_op) (ExprEtaGen eta (t:=t) e)) + (Interp (@interp_op) e). + Proof. apply interp_expr_eta_gen; intros; apply interpf_exprf_eta_gen. Qed. End gen_flat_type. (* Local *) Hint Rewrite @eq_interp_flat_type_eta_gen. + (* Local *) Hint Rewrite @interp_expr_eta_gen. (* Local *) Hint Rewrite @interpf_exprf_eta_gen. Lemma eq_interp_flat_type_eta {var t T f} x @@ -60,4 +81,16 @@ Section language. : interpf (@interp_op) (exprf_eta' (t:=t) e) = interpf (@interp_op) e. Proof. t. Qed. (* Local *) Hint Rewrite @interpf_exprf_eta'. + Lemma interp_expr_eta {t e} + : interp_type_gen_rel_pointwise (fun _ => eq) (interp (@interp_op) (expr_eta (t:=t) e)) (interp (@interp_op) e). + Proof. t. Qed. + Lemma interp_expr_eta' {t e} + : interp_type_gen_rel_pointwise (fun _ => eq) (interp (@interp_op) (expr_eta' (t:=t) e)) (interp (@interp_op) e). + Proof. t. Qed. + Lemma InterpExprEta {t e} + : interp_type_gen_rel_pointwise (fun _ => eq) (Interp (@interp_op) (ExprEta (t:=t) e)) (Interp (@interp_op) e). + Proof. apply interp_expr_eta. Qed. + Lemma InterpExprEta' {t e} + : interp_type_gen_rel_pointwise (fun _ => eq) (Interp (@interp_op) (ExprEta' (t:=t) e)) (Interp (@interp_op) e). + Proof. apply interp_expr_eta'. Qed. End language. diff --git a/src/Reflection/InterpByIsoProofs.v b/src/Reflection/InterpByIsoProofs.v index f1bde4a59..c5006c3a4 100644 --- a/src/Reflection/InterpByIsoProofs.v +++ b/src/Reflection/InterpByIsoProofs.v @@ -45,6 +45,32 @@ Section language. (interp_of_var12 : forall t x, interp_of_var1 t (var1_of_interp t x) = interp_of_var2 t (var2_of_interp t x)). Hint Rewrite @flatten_binding_list_SmartVarfMap @List.in_map_iff @List.in_app_iff. + Lemma interp_of_var12_SmartVarfMap + t1 e1 t x1 x2 + (H : List.In (existT _ t (x1, x2)) + (flatten_binding_list + (SmartVarfMap (t:=t1) var1_of_interp e1) + (SmartVarfMap var2_of_interp e1))) + : interp_of_var1 t x1 = interp_of_var2 t x2. + Proof. + repeat first [ progress repeat autorewrite with core in * + | progress subst + | progress inversion_sigma + | progress inversion_prod + | progress simpl in * + | progress destruct_head' ex + | progress destruct_head' and + | progress destruct_head' or + | progress destruct_head' sigT + | progress destruct_head' prod + | progress rewrite_hyp !* + | solve [ auto ] ]. + do 2 apply f_equal. + eapply interp_flat_type_rel_pointwise_flatten_binding_list with (R':=fun _ => eq); [ eassumption | ]. + apply lift_interp_flat_type_rel_pointwise_f_eq; reflexivity. + Qed. + Local Hint Resolve List.in_app_or interp_of_var12_SmartVarfMap. + Lemma wff_interpf_retr G {t} (e1 : @exprf var1 t) (e2 : @exprf var2 t) (HG : forall t x1 x2, List.In (existT _ t (x1, x2)) G diff --git a/src/Reflection/Relations.v b/src/Reflection/Relations.v index a7f7bf7fc..4a277d2b1 100644 --- a/src/Reflection/Relations.v +++ b/src/Reflection/Relations.v @@ -120,7 +120,28 @@ Section language. : interp_flat_type_rel_pointwise (fun t => R t t) t x y <-> interp_flat_type_rel_pointwise_hetero R t t x y. Proof. induction t; simpl; rewrite_hyp ?*; reflexivity. Qed. + + Lemma interp_flat_type_rel_pointwise_impl {R1 R2 : forall t, _ -> _ -> Prop} t x y + : interp_flat_type_rel_pointwise (fun t x y => (R1 t x y -> R2 t x y)%type) t x y + -> (interp_flat_type_rel_pointwise R1 t x y + -> interp_flat_type_rel_pointwise R2 t x y). + Proof. induction t; simpl; intuition. Qed. + + Lemma interp_flat_type_rel_pointwise_always {R : forall t, _ -> _ -> Prop} + : (forall t x y, R t x y) + -> forall t x y, interp_flat_type_rel_pointwise R t x y. + Proof. induction t; simpl; intuition. Qed. End flat_type. + Section flat_type_extra. + Context {interp_base_type1 interp_base_type2 : base_type_code -> Type}. + Lemma interp_flat_type_rel_pointwise_impl' {R1 R2 : forall t, _ -> _ -> Prop} t x y + : @interp_flat_type_rel_pointwise + interp_base_type1 interp_base_type2 + (fun t x y => (R1 t y x -> R2 t x y)%type) t x y + -> (interp_flat_type_rel_pointwise R1 t y x + -> interp_flat_type_rel_pointwise R2 t x y). + Proof. induction t; simpl; intuition. Qed. + End flat_type_extra. Section type. Section hetero. @@ -276,6 +297,16 @@ Section language. t x y <-> SmartVarfMap f x = y. Proof. rewrite lift_interp_flat_type_rel_pointwise_f_eq, SmartVarfMap_id; reflexivity. Qed. + Lemma lift_interp_flat_type_rel_pointwise_f_eq2 {T} (f g : forall t, _ -> _ -> T t) t x y + : @interp_flat_type_rel_pointwise + interp_base_type1 interp_base_type2 + (fun t x y => f t x y = g t x y) + t x y + <-> SmartVarfMap2 f x y = SmartVarfMap2 g x y. + Proof. + induction t; unfold SmartVarfMap2 in *; simpl in *; destruct_head_hnf unit; try tauto. + rewrite_hyp !*; intuition congruence. + Qed. End lifting. Local Ltac t := diff --git a/src/Reflection/SmartBound.v b/src/Reflection/SmartBound.v index 74345ef98..d86771216 100644 --- a/src/Reflection/SmartBound.v +++ b/src/Reflection/SmartBound.v @@ -161,3 +161,6 @@ Section language. := fun var => smart_bound (e var) (interp (@interp_op_bounds) (e _)) input_bounds. End smart_bound. End language. + +Global Arguments bound_flat_type _ _ _ !_ _ / . +Global Arguments bound_type _ _ _ !_ _ _ / . diff --git a/src/Reflection/SmartBoundInterp.v b/src/Reflection/SmartBoundInterp.v new file mode 100644 index 000000000..34824e5ce --- /dev/null +++ b/src/Reflection/SmartBoundInterp.v @@ -0,0 +1,146 @@ +Require Import Crypto.Reflection.Syntax. +Require Import Crypto.Reflection.Wf. +Require Import Crypto.Reflection.InterpWfRel. +Require Import Crypto.Reflection.Relations. +Require Import Crypto.Reflection.SmartMap. +(*Require Import Crypto.Reflection.TypeUtil. +Require Import Crypto.Reflection.BoundByCast.*) +Require Import Crypto.Reflection.SmartBound. +Require Import Crypto.Reflection.ExprInversion. +(*Require Import Crypto.Reflection.SmartBoundWf. +Require Import Crypto.Reflection.InlineCastInterp. +Require Import Crypto.Reflection.InlineInterp. +Require Import Crypto.Reflection.LinearizeInterp. +Require Import Crypto.Reflection.LinearizeWf. +Require Import Crypto.Reflection.MapCastInterp. +Require Import Crypto.Reflection.MapCastWf. +Require Import Crypto.Reflection.EtaInterp.*) +Require Import Crypto.Util.Tactics.DestructHead. + +Local Open Scope expr_scope. +Local Open Scope ctype_scope. +Section language. + Context {base_type_code : Type} + {op : flat_type base_type_code -> flat_type base_type_code -> Type} + (interp_base_type interp_base_type_bounds : base_type_code -> Type) + (interp_op : forall src dst, op src dst -> interp_flat_type interp_base_type src -> interp_flat_type interp_base_type dst) + (interp_op_bounds : forall src dst, op src dst -> interp_flat_type interp_base_type_bounds src -> interp_flat_type interp_base_type_bounds dst) + (bound_base_type : forall t, interp_base_type_bounds t -> base_type_code) + (base_type_beq : base_type_code -> base_type_code -> bool) + (base_type_bl_transparent : forall x y, base_type_beq x y = true -> x = y) + (base_type_leb : base_type_code -> base_type_code -> bool) + (Cast : forall var A A', exprf base_type_code op (var:=var) (Tbase A) -> exprf base_type_code op (var:=var) (Tbase A')) + (cast_val : forall A A', interp_base_type A -> interp_base_type A') + (genericize_op : forall src dst (opc : op src dst) (new_bounded_type_in new_bounded_type_out : base_type_code), + option { src'dst' : _ & op (fst src'dst') (snd src'dst') }) + (failf : forall var t, @exprf base_type_code op var (Tbase t)) + (is_bounded_by_base : forall t, interp_base_type t -> interp_base_type_bounds t -> Prop) + (interpf_cast : forall A A' e, interpf interp_op (Cast _ A A' e) = cast_val A A' (interpf interp_op e)) + (strip_cast_val + : forall t x y, + is_bounded_by_base t y x -> + cast_val (bound_base_type t x) t (cast_val t (bound_base_type t x) y) = y). +(* + (wff_Cast : forall var1 var2 G A A' e1 e2, + wff G e1 e2 -> wff G (Cast var1 A A' e1) (Cast var2 A A' e2)).*) + + Local Notation is_bounded_by (*{T} : interp_flat_type interp_base_type T -> interp_flat_type interp_base_type_bounds T -> Prop*) + := (interp_flat_type_rel_pointwise is_bounded_by_base). + Context (is_bounded_by_interp_op + : forall src dst opc sv1 sv2, + is_bounded_by sv1 sv2 -> + is_bounded_by (interp_op src dst opc sv1) (interp_op_bounds src dst opc sv2)). + Local Notation Expr := (@Expr base_type_code op). + Local Notation expr := (@expr base_type_code op). + Local Notation exprf := (@exprf base_type_code op). + Local Notation SmartBound := (@SmartBound _ _ _ interp_op_bounds bound_base_type Cast). + Local Notation smart_bound := (@smart_bound _ _ interp_base_type_bounds bound_base_type Cast). + Local Notation interpf_smart_bound := (@interpf_smart_bound _ interp_base_type_bounds bound_base_type interp_base_type cast_val). + Local Notation interpf_smart_unbound := (@interpf_smart_unbound _ interp_base_type_bounds bound_base_type interp_base_type cast_val). + Local Notation interpf_smart_bound_exprf := (@interpf_smart_bound_exprf _ op interp_base_type_bounds bound_base_type Cast). + Local Notation interpf_smart_unbound_exprf := (@interpf_smart_unbound_exprf _ op interp_base_type_bounds bound_base_type Cast). + Local Notation bound_op := (@bound_op _ _ _ interp_op_bounds bound_base_type _ base_type_bl_transparent base_type_leb Cast genericize_op). + + Local Ltac t := + unfold SmartPairf, SmartBound.interpf_smart_bound, SmartBound.interpf_smart_bound_exprf; + repeat first [ reflexivity + | progress destruct_head' unit + | progress simpl in * + | rewrite !interpf_cast + | match goal with H : _ |- _ => setoid_rewrite H end ]. + Lemma interpf_SmartPairf_interpf_smart_bound_exprf + {t} e bounds + : interpf interp_op (SmartPairf (interpf_smart_bound_exprf (t:=t) e bounds)) + = interpf_smart_bound e bounds. + Proof. clear -interpf_cast; induction t; t. Qed. + + Lemma interpf_SmartPairf_interpf_smart_unbound_exprf + {t} bounds e + : interpf interp_op (SmartPairf (interpf_smart_unbound_exprf (t:=t) bounds e)) + = interpf_smart_unbound bounds (SmartVarfMap (fun _ e => interpf interp_op e) e). + Proof. clear -interpf_cast; induction t; t. Qed. + + (* + Lemma interp_smart_bound_and_rel {t} + (e : expr t) (ebounds : expr t) + (Hwf : wf e ebounds) + (input_bounds : interp_flat_type interp_base_type_bounds (domain t)) + (output_bounds := interp interp_op_bounds ebounds input_bounds) + (e' := smart_bound e (interp interp_op_bounds ebounds) input_bounds) + : forall x, + is_bounded_by (interpf_smart_unbound input_bounds x) input_bounds + -> is_bounded_by (interp interp_op e (interpf_smart_unbound input_bounds x)) output_bounds + /\ interpf_smart_unbound _ (interp interp_op e' x) + = interp interp_op e (interpf_smart_unbound input_bounds x). + Proof. + intros; subst e' output_bounds. + match goal with |- ?A /\ ?B => cut (A /\ (A -> B)); [ tauto | ] end. + split. + { apply interp_wf; auto. } + { intro Hbounded_out. + unfold smart_bound; simpl. + cbv [LetIn.Let_In]. + rewrite interpf_invert_Abs, interpf_SmartPairf_interpf_smart_bound_exprf, interpf_SmartPairf_interpf_smart_unbound_exprf, SmartVarfMap_compose; simpl. + rewrite SmartVarfMap_id. + setoid_rewrite SmartFlatTypeMapUnInterp2_SmartFlatTypeMap2Interp2. + etransitivity; [ | eapply SmartVarfMap2_snd_arg ]. + apply lift_interp_flat_type_rel_pointwise_f_eq2. + eauto using interp_flat_type_rel_pointwise_impl', interp_flat_type_rel_pointwise_always. } + Qed. + + Lemma InterpSmartBoundAndRel {t} + (e : Expr t) + (Hwf : Wf e) + (input_bounds : interp_flat_type interp_base_type_bounds (domain t)) + (output_bounds := Interp interp_op_bounds e input_bounds) + (e' := SmartBound e input_bounds) + (*(Hgood : bounds_are_recursively_good + (@interp_op_bounds) bound_is_good + (invert_Abs (e _) input_bounds))*) + : forall x, + is_bounded_by (interpf_smart_unbound input_bounds x) input_bounds + -> is_bounded_by (Interp interp_op e (interpf_smart_unbound input_bounds x)) output_bounds + /\ interpf_smart_unbound _ (Interp interp_op e' x) + = Interp interp_op e (interpf_smart_unbound input_bounds x). + Proof. + apply interp_smart_bound_and_rel; auto. + Qed. + + Lemma InterpSmartBound {t} + (e : Expr t) + (Hwf : Wf e) + (input_bounds : interp_flat_type interp_base_type_bounds (domain t)) + (output_bounds := Interp interp_op_bounds e input_bounds) + (e' := SmartBound e input_bounds) + (*(Hgood : bounds_are_recursively_good + (@interp_op_bounds) bound_is_good + (invert_Abs (e _) input_bounds))*) + : forall x, + is_bounded_by (interpf_smart_unbound input_bounds x) input_bounds + -> interpf_smart_unbound _ (Interp interp_op e' x) + = Interp interp_op e (interpf_smart_unbound input_bounds x). + Proof. + intros; eapply InterpSmartBoundAndRel; auto. + Qed. + *) +End language. diff --git a/src/Reflection/SmartMap.v b/src/Reflection/SmartMap.v index 0cc16745e..8915bff90 100644 --- a/src/Reflection/SmartMap.v +++ b/src/Reflection/SmartMap.v @@ -120,14 +120,37 @@ Section homogenous_type. Definition SmartVarfMap {var var'} (f : forall t, var t -> var' t) {t} : interp_flat_type var t -> interp_flat_type var' t := @smart_interp_flat_map var (interp_flat_type var') f tt (fun A B x y => pair x y) t. + Lemma SmartVarfMap_compose {var' var'' var''' t} f g x + : @SmartVarfMap var'' var''' g t (@SmartVarfMap var' var'' f t x) + = @SmartVarfMap _ _ (fun t v => g t (f t v)) t x. + Proof. + unfold SmartVarfMap; clear; induction t; simpl; destruct_head_hnf unit; destruct_head_hnf prod; + rewrite_hyp ?*; congruence. + Qed. Lemma SmartVarfMap_id {var' t} x : @SmartVarfMap var' var' (fun _ x => x) t x = x. Proof. - unfold SmartVarfMap; induction t; simpl; destruct_head_hnf unit; destruct_head_hnf prod; + unfold SmartVarfMap; clear; induction t; simpl; destruct_head_hnf unit; destruct_head_hnf prod; rewrite_hyp ?*; congruence. Qed. Definition SmartVarfMap2 {var var' var''} (f : forall t, var t -> var' t -> var'' t) {t} : interp_flat_type var t -> interp_flat_type var' t -> interp_flat_type var'' t := @smart_interp_flat_map2 var var' (interp_flat_type var'') f tt (fun A B x y => pair x y) t. + Lemma SmartVarfMap2_fst_arg {var' var''} {t} + (x : interp_flat_type var' t) + (y : interp_flat_type var'' t) + : SmartVarfMap2 (fun _ a b => a) x y = x. + Proof. + unfold SmartVarfMap2; clear; induction t; simpl; destruct_head_hnf unit; destruct_head_hnf prod; + rewrite_hyp ?*; congruence. + Qed. + Lemma SmartVarfMap2_snd_arg {var' var''} {t} + (x : interp_flat_type var' t) + (y : interp_flat_type var'' t) + : SmartVarfMap2 (fun _ a b => b) x y = y. + Proof. + unfold SmartVarfMap2; clear; induction t; simpl; destruct_head_hnf unit; destruct_head_hnf prod; + rewrite_hyp ?*; congruence. + Qed. Definition SmartVarfTypeMap {var} (f : forall t, var t -> Type) {t} : interp_flat_type var t -> Type := @smart_interp_flat_map var (fun _ => Type) f unit (fun _ _ P Q => P * Q)%type t. @@ -181,8 +204,8 @@ Global Arguments SmartVarf {_ _ _ _} _. Global Arguments SmartPairf {_ _ _ t} _. Global Arguments SmartValf {_} T _ t. Global Arguments SmartVarVarf {_ _ _ _} _. -Global Arguments SmartVarfMap {_ _ _} _ {_} _. -Global Arguments SmartVarfMap2 {_ _ _ _} _ {t} _ _. +Global Arguments SmartVarfMap {_ _ _} _ {!_} _ / . +Global Arguments SmartVarfMap2 {_ _ _ _} _ {!t} _ _ / . Global Arguments SmartVarfTypeMap {_ _} _ {_} _. Global Arguments SmartVarfPropMap {_ _} _ {_} _. Global Arguments SmartVarfTypeMap2 {_ _ _} _ {t} _ _. @@ -192,7 +215,7 @@ Global Arguments SmartFlatTypeUnMap {_} _. Global Arguments SmartFlatTypeMapInterp {_ _ _ _} _ {_} _. Global Arguments SmartFlatTypeMapUnInterp {_ _ _ _ _} fv {_ _} _. Global Arguments SmartVarMap_hetero {_ _ _ _ _} _ _ {_} _. -Global Arguments SmartVarMap {_ _ _} _ _ {_} _. +Global Arguments SmartVarMap {_ _ _} _ _ {!_} _ / . Global Arguments SmartAbs {_ _ _ _ _} _. Section hetero_type. @@ -239,10 +262,27 @@ Section hetero_type. | Prod A B => fun xy x'y' => (@SmartFlatTypeMap2Interp2 _ _ _ f fv A (fst xy) (fst x'y'), @SmartFlatTypeMap2Interp2 _ _ _ f fv B (snd xy) (snd x'y')) end. + + Lemma SmartFlatTypeMapUnInterp2_SmartFlatTypeMap2Interp2 + var' var'' var''' + (f : forall t, var' t -> flat_type base_type_code2) + (fv : forall t (v : var' t), interp_flat_type var'' (f t v) -> var''' t) + (gv : forall t v, var''' t -> interp_flat_type var'' (f t v)) + {t} v + (e : interp_flat_type var''' t) + : @SmartFlatTypeMapUnInterp2 + _ _ _ f fv t v + (@SmartFlatTypeMap2Interp2 + _ _ _ f gv t v e) + = SmartVarfMap2 (fun t v e => fv t v (gv t v e)) v e. + Proof. + induction t; simpl in *; destruct_head' unit; + rewrite_hyp ?*; reflexivity. + Qed. End smart_flat_type_map2. End hetero_type. -Global Arguments SmartFlatTypeMap2 {_ _ _} _ {_} _. +Global Arguments SmartFlatTypeMap2 {_ _ _} _ {!_} _ / . Global Arguments SmartFlatTypeMapInterp2 {_ _ _ _ _} fv {_} _. Global Arguments SmartFlatTypeMap2Interp2 {_ _ _ _ _ _} fv {t} v _. Global Arguments SmartFlatTypeMapUnInterp2 {_ _ _ _ _ _} fv {_ _} _. diff --git a/src/Reflection/Z/Syntax/Util.v b/src/Reflection/Z/Syntax/Util.v index 0feaa08d3..42569daf8 100644 --- a/src/Reflection/Z/Syntax/Util.v +++ b/src/Reflection/Z/Syntax/Util.v @@ -1,7 +1,25 @@ Require Import Crypto.Reflection.Syntax. +Require Import Crypto.Reflection.TypeUtil. +Require Import Crypto.Reflection.TypeInversion. Require Import Crypto.Reflection.Z.Syntax. +Require Import Crypto.Util.FixedWordSizesEquality. +Require Import Crypto.Util.NatUtil. +Require Import Crypto.Util.Tactics.BreakMatch. +Require Import Crypto.Util.Tactics.DestructHead. +Require Import Crypto.Util.Notations. Definition make_const t : interp_base_type t -> op Unit (Tbase t) := match t with TZ => OpConst end. Definition is_const s d (v : op s d) : bool := match v with OpConst _ => true | _ => false end. +Arguments is_const [s d] v. +Definition is_cast s d (v : op s d) : bool + := false. +Arguments is_cast [s d] v. + +Definition base_type_leb (v1 v2 : base_type) : bool + := true. + +Definition base_type_min := base_type_min base_type_leb. +Global Arguments base_type_min !_ !_ / . +Global Arguments TypeUtil.base_type_min _ _ _ / . |