diff options
Diffstat (limited to 'src/Reflection')
62 files changed, 1280 insertions, 1831 deletions
diff --git a/src/Reflection/Application.v b/src/Reflection/Application.v deleted file mode 100644 index 59b6740ca..000000000 --- a/src/Reflection/Application.v +++ /dev/null @@ -1,200 +0,0 @@ -Require Import Crypto.Reflection.Syntax. - -Section language. - Context {base_type : Type} - {interp_base_type : base_type -> Type} - {op : flat_type base_type -> flat_type base_type -> Type} - {interp_op : forall src dst, op src dst -> interp_flat_type interp_base_type src -> interp_flat_type interp_base_type dst}. - Fixpoint count_binders (t : type base_type) : nat - := match t with - | Arrow A B => S (count_binders B) - | Tflat _ => 0 - end. - - Fixpoint remove_binders' (n : nat) (t : type base_type) {struct t} : type base_type - := match t, n with - | Tflat _, _ => t - | Arrow _ B, 0 => B - | Arrow A B, S n' - => remove_binders' n' B - end. - - Definition remove_binders (n : nat) (t : type base_type) : type base_type - := match n with - | 0 => t - | S n' => remove_binders' n' t - end. - - Fixpoint remove_all_binders (t : type base_type) : flat_type base_type - := match t with - | Tflat T => T - | Arrow A B => remove_all_binders B - end. - - Fixpoint binders_for' (n : nat) (t : type base_type) (var : base_type -> Type) {struct t} - := match n, t return Type with - | 0, Arrow A B => var A - | S n', Arrow A B => var A * binders_for' n' B var - | _, _ => unit - end%type. - Definition binders_for (n : nat) (t : type base_type) (var : base_type -> Type) - := match n return Type with - | 0 => unit - | S n' => binders_for' n' t var - end. - - Fixpoint all_binders_for' (t : type base_type) - := match t return flat_type base_type with - | Tflat T => Unit - | Arrow A B - => (Tbase A * all_binders_for' B)%ctype - end. - - Fixpoint all_binders_for (t : type base_type) - := match t return match t with - | Tflat _ => unit - | _ => flat_type base_type - end with - | Tflat T => tt - | Arrow A B - => match B return match B with Tflat _ => _ | _ => _ end -> _ with - | Tflat T => fun _ => Tbase A - | Arrow _ _ => fun T => Tbase A * T - end%ctype (all_binders_for B) - end. - - Definition interp_all_binders_for T var - := match T return Type with - | Tflat _ => unit - | Arrow A B => interp_flat_type var (all_binders_for (Arrow A B)) - end. - - Definition interp_all_binders_for' (T : type base_type) var - := interp_flat_type var (all_binders_for' T). - - Fixpoint interp_all_binders_for_of' T var {struct T} - : interp_all_binders_for' T var -> interp_all_binders_for T var - := match T return interp_all_binders_for' T var -> interp_all_binders_for T var with - | Tflat _ => fun x => x - | Arrow A B => - match B - return (interp_all_binders_for' B var -> interp_all_binders_for B var) - -> interp_all_binders_for' (Arrow A B) var - -> interp_all_binders_for (Arrow A B) var - with - | Tflat _ => fun _ => @fst _ _ - | Arrow C D => fun interp x => (fst x, interp (snd x)) - end (@interp_all_binders_for_of' B var) - end. - - Fixpoint interp_all_binders_for_to' T var {struct T} - : interp_all_binders_for T var -> interp_all_binders_for' T var - := match T return interp_all_binders_for T var -> interp_all_binders_for' T var with - | Tflat _ => fun x => x - | Arrow A B => - match B - return (interp_all_binders_for B var -> interp_all_binders_for' B var) - -> interp_all_binders_for (Arrow A B) var - -> interp_all_binders_for' (Arrow A B) var - with - | Tflat _ => fun _ x => (x, tt) - | Arrow C D => fun interp x => (fst x, interp (snd x)) - end (@interp_all_binders_for_to' B var) - end. - - Definition fst_binder {A B var} (args : interp_flat_type var (all_binders_for (Arrow A B))) : var A - := match B return interp_flat_type var (all_binders_for (Arrow A B)) -> var A with - | Tflat _ => fun x => x - | Arrow _ _ => fun x => fst x - end args. - Definition snd_binder {A B var} (args : interp_flat_type var (all_binders_for (Arrow A B))) - : interp_all_binders_for B var - := match B return interp_flat_type var (all_binders_for (Arrow A B)) - -> interp_all_binders_for B var - with - | Tflat _ => fun _ => tt - | Arrow _ _ => fun x => snd x - end args. - - Fixpoint Apply' n {var t} (x : @expr base_type op var t) - : forall (args : binders_for' n t var), - @expr base_type op var (remove_binders' n t) - := match x in (@expr _ _ _ t), n return (binders_for' n t var -> @expr _ _ _ (remove_binders' n t)) with - | Return _ _ as y, _ => fun _ => y - | Abs _ _ f, 0 => f - | Abs src dst f, S n' => fun args => @Apply' n' var dst (f (fst args)) (snd args) - end. - - Definition Apply n {var t} (x : @expr base_type op var t) - : forall (args : binders_for n t var), - @expr base_type op var (remove_binders n t) - := match n return binders_for n t var -> @expr _ _ _ (remove_binders n t) with - | 0 => fun _ => x - | S n' => @Apply' n' var t x - end. - - Fixpoint ApplyAll {var t} (x : @expr base_type op var t) - : forall (args : interp_all_binders_for t var), - @exprf base_type op var (remove_all_binders t) - := match x in @expr _ _ _ t - return (forall (args : interp_all_binders_for t var), - @exprf base_type op var (remove_all_binders t)) - with - | Return _ x => fun _ => x - | Abs src dst f => fun args => @ApplyAll var dst (f (fst_binder args)) (snd_binder args) - end. - - Fixpoint ApplyInterped' n {t} {struct t} - : forall (x : interp_type interp_base_type t) - (args : binders_for' n t interp_base_type), - interp_type interp_base_type (remove_binders' n t) - := match t, n return (forall (x : interp_type interp_base_type t) - (args : binders_for' n t interp_base_type), - interp_type interp_base_type (remove_binders' n t)) with - | Tflat _, _ => fun x _ => x - | Arrow s d, 0 => fun x => x - | Arrow s d, S n' => fun f args => @ApplyInterped' n' d (f (fst args)) (snd args) - end. - - Definition ApplyInterped (n : nat) {t} (x : interp_type interp_base_type t) - : forall (args : binders_for n t interp_base_type), - interp_type interp_base_type (remove_binders n t) - := match n return (binders_for n t interp_base_type -> interp_type interp_base_type (remove_binders n t)) with - | 0 => fun _ => x - | S n' => @ApplyInterped' n' t x - end. - - Fixpoint ApplyInterpedAll' {t} - : forall (x : interp_type interp_base_type t) - (args : interp_all_binders_for' t interp_base_type), - interp_flat_type interp_base_type (remove_all_binders t) - := match t return (forall (x : interp_type _ t) - (args : interp_all_binders_for' t _), - interp_flat_type _ (remove_all_binders t)) - with - | Tflat _ => fun x _ => x - | Arrow A B => fun f x => @ApplyInterpedAll' B (f (fst x)) (snd x) - end. - - Definition ApplyInterpedAll {t} - (x : interp_type interp_base_type t) - (args : interp_all_binders_for t interp_base_type) - : interp_flat_type interp_base_type (remove_all_binders t) - := ApplyInterpedAll' x (interp_all_binders_for_to' _ _ args). -End language. - -Arguments all_binders_for {_} !_ / . -Arguments interp_all_binders_for {_} !_ _ / . -Arguments interp_all_binders_for_of' {_ !_ _} !_ / . -Arguments interp_all_binders_for_to' {_ !_ _} !_ / . -Arguments count_binders {_} !_ / . -Arguments binders_for {_} !_ !_ _ / . -Arguments remove_binders {_} !_ !_ / . -(* Work around bug #5175 *) -Arguments Apply {_ _ _ _ _} _ _ , {_ _} _ {_ _} _ _. -Arguments Apply _ _ !_ _ _ !_ !_ / . -Arguments ApplyInterped {_ _ !_ !_} _ _ / . -Arguments ApplyInterped' {_ _} _ {_} _ _. -Arguments ApplyAll {_ _ _ !_} !_ _ / . -Arguments ApplyInterpedAll' {_ _ !_} _ _ / . -Arguments ApplyInterpedAll {_ _ !_} _ _ / . diff --git a/src/Reflection/ApplicationLemmas.v b/src/Reflection/ApplicationLemmas.v deleted file mode 100644 index e8105c2f0..000000000 --- a/src/Reflection/ApplicationLemmas.v +++ /dev/null @@ -1,104 +0,0 @@ -Require Import Crypto.Reflection.Syntax. -Require Import Crypto.Reflection.Application. - -Section language. - Context {base_type : Type} - {interp_base_type : base_type -> Type} - {op : flat_type base_type -> flat_type base_type -> Type} - {interp_op : forall src dst, op src dst -> interp_flat_type interp_base_type src -> interp_flat_type interp_base_type dst}. - - Lemma interp_apply' {n t} - (x : @expr base_type op _ t) - (args : binders_for' n t interp_base_type) - : interp interp_op (Apply' n x args) = ApplyInterped' n (interp interp_op x) args. - Proof. - generalize dependent t; induction n as [|n IHn]; intros. - { destruct x; reflexivity. } - { destruct x as [|?? x]; simpl; [ reflexivity | ]. - apply IHn. } - Qed. - - Lemma interp_apply {n t} - (x : @expr base_type op _ t) - (args : binders_for n t interp_base_type) - : interp interp_op (Apply n x args) = ApplyInterped (interp interp_op x) args. - Proof. - destruct n; [ reflexivity | ]. - apply interp_apply'. - Qed. - - Lemma fst_interp_all_binders_for_of' {A B} - (args : interp_all_binders_for' (Arrow A B) interp_base_type) - : fst_binder (interp_all_binders_for_of' args) = fst args. - Proof. - destruct B; reflexivity. - Qed. - - Lemma snd_interp_all_binders_for_of' {A B} - (args : interp_all_binders_for' (Arrow A B) interp_base_type) - : snd_binder (interp_all_binders_for_of' args) = interp_all_binders_for_of' (snd args). - Proof. - destruct B. - { destruct args as [? []]; reflexivity. } - { destruct args; reflexivity. } - Qed. - - Lemma fst_interp_all_binders_for_to' {A B} - (args : interp_all_binders_for (Arrow A B) interp_base_type) - : fst (interp_all_binders_for_to' args) = fst_binder args. - Proof. - destruct B; reflexivity. - Qed. - - Lemma snd_interp_all_binders_for_to' {A B} - (args : interp_all_binders_for (Arrow A B) interp_base_type) - : snd (interp_all_binders_for_to' args) = interp_all_binders_for_to' (snd_binder args). - Proof. - destruct B; reflexivity. - Qed. - - Lemma interp_all_binders_for_to'_of' {t} (args : interp_all_binders_for' t interp_base_type) - : interp_all_binders_for_to' (interp_all_binders_for_of' args) = args. - Proof. - induction t; destruct args; [ reflexivity | ]. - apply injective_projections; - [ rewrite fst_interp_all_binders_for_to', fst_interp_all_binders_for_of'; reflexivity - | rewrite snd_interp_all_binders_for_to', snd_interp_all_binders_for_of', IHt; reflexivity ]. - Qed. - - Lemma interp_all_binders_for_of'_to' {t} (args : interp_all_binders_for t interp_base_type) - : interp_all_binders_for_of' (interp_all_binders_for_to' args) = args. - Proof. - induction t as [|A B IHt]. - { destruct args; reflexivity. } - { destruct B; [ reflexivity | ]. - destruct args; simpl; rewrite IHt; reflexivity. } - Qed. - - Lemma interp_apply_all' {t} - (x : @expr base_type op _ t) - (args : interp_all_binders_for' t interp_base_type) - : interp interp_op (ApplyAll x (interp_all_binders_for_of' args)) = ApplyInterpedAll' (interp interp_op x) args. - Proof. - induction x as [|?? x IHx]; [ reflexivity | ]. - simpl; rewrite <- IHx; destruct args. - rewrite snd_interp_all_binders_for_of', fst_interp_all_binders_for_of'; reflexivity. - Qed. - - Lemma interp_apply_all {t} - (x : @expr base_type op _ t) - (args : interp_all_binders_for t interp_base_type) - : interp interp_op (ApplyAll x args) = ApplyInterpedAll (interp interp_op x) args. - Proof. - unfold ApplyInterpedAll. - rewrite <- interp_apply_all', interp_all_binders_for_of'_to'; reflexivity. - Qed. - - Lemma interp_apply_all_to' {t} - (x : @expr base_type op _ t) - (args : interp_all_binders_for t interp_base_type) - : interp interp_op (ApplyAll x args) = ApplyInterpedAll' (interp interp_op x) (interp_all_binders_for_to' args). - Proof. - rewrite <- interp_apply_all', interp_all_binders_for_of'_to'; reflexivity. - Qed. -End language. diff --git a/src/Reflection/ApplicationRelations.v b/src/Reflection/ApplicationRelations.v deleted file mode 100644 index 9a1daa97e..000000000 --- a/src/Reflection/ApplicationRelations.v +++ /dev/null @@ -1,28 +0,0 @@ -Require Import Crypto.Reflection.Syntax. -Require Import Crypto.Reflection.Application. - -Section language. - Context {base_type1 base_type2 : Type} - {interp_base_type1 : base_type1 -> Type} - {interp_base_type2 : base_type2 -> Type} - {op1 : flat_type base_type1 -> flat_type base_type1 -> Type} - {op2 : flat_type base_type2 -> flat_type base_type2 -> Type} - {interp_op1 : forall src dst, op1 src dst -> interp_flat_type interp_base_type1 src -> interp_flat_type interp_base_type1 dst} - {interp_op2 : forall src dst, op2 src dst -> interp_flat_type interp_base_type2 src -> interp_flat_type interp_base_type2 dst} - (R : forall t1 t2, interp_base_type1 t1 -> interp_base_type2 t2 -> Prop). - - Fixpoint rel_interp_all_binders_for' {t1 : type base_type1} {t2 : type base_type2} - : interp_all_binders_for' t1 interp_base_type1 -> interp_all_binders_for' t2 interp_base_type2 -> Prop - := match t1, t2 return interp_all_binders_for' t1 _ -> interp_all_binders_for' t2 _ -> Prop with - | Tflat T1, Tflat T2 => fun _ _ => True - | Arrow A1 B1, Arrow A2 B2 - => fun x y => R _ _ (fst x) (fst y) /\ @rel_interp_all_binders_for' _ _ (snd x) (snd y) - | Tflat _, _ - | Arrow _ _, _ - => fun _ _ => False - end. - Definition rel_interp_all_binders_for {t1 : type base_type1} {t2 : type base_type2} - (x : interp_all_binders_for t1 interp_base_type1) (y : interp_all_binders_for t2 interp_base_type2) - : Prop - := rel_interp_all_binders_for' (interp_all_binders_for_to' x) (interp_all_binders_for_to' y). -End language. diff --git a/src/Reflection/BoundByCast.v b/src/Reflection/BoundByCast.v index 89170ec2f..d65e67919 100644 --- a/src/Reflection/BoundByCast.v +++ b/src/Reflection/BoundByCast.v @@ -1,7 +1,7 @@ Require Import Crypto.Reflection.Syntax. Require Import Crypto.Reflection.SmartBound. Require Import Crypto.Reflection.InlineCast. -Require Import Crypto.Reflection.Application. +Require Import Crypto.Reflection.ExprInversion. Require Import Crypto.Reflection.Inline. Require Import Crypto.Reflection.Linearize. Require Import Crypto.Reflection.MapCast. @@ -43,6 +43,6 @@ Section language. op (@interp_op_bounds) (@failf) (@bound_op _ _ _ interp_op_bounds bound_base_type _ base_type_bl_transparent base_type_leb Cast genericize_op) - t1 e1 (interp_all_binders_for_to' args2)) - (interp_all_binders_for_to' args2)))). + t1 e1 args2) + args2))). End language. diff --git a/src/Reflection/BoundByCastInterp.v b/src/Reflection/BoundByCastInterp.v index 2eda88a78..cf6131a5e 100644 --- a/src/Reflection/BoundByCastInterp.v +++ b/src/Reflection/BoundByCastInterp.v @@ -89,7 +89,6 @@ Section language. 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) @@ -115,5 +114,4 @@ Section language. erewrite InterpSmartBound, InterpMapInterpCast by eauto with wf. reflexivity. } Qed. -*) End language. diff --git a/src/Reflection/CommonSubexpressionElimination.v b/src/Reflection/CommonSubexpressionElimination.v index 560551f44..433c45aa8 100644 --- a/src/Reflection/CommonSubexpressionElimination.v +++ b/src/Reflection/CommonSubexpressionElimination.v @@ -174,11 +174,10 @@ Section symbolic. | x :: xs => LetIn (projT2 x) (fun _ => @prepend_prefix _ e xs) end. - Fixpoint cse {t} (v : @expr fsvar t) (xs : mapping) {struct v} : @expr var t + Definition cse {t} (v : @expr fsvar t) (xs : mapping) : @expr var t := match v in @Syntax.expr _ _ _ t return expr t with - | Return _ x => Return (csef (prepend_prefix x prefix) xs) - | Abs _ _ f => Abs (fun x => let x' := symbolicify_var x xs in - @cse _ (f (x, x')) (add_mapping x x' xs)) + | Abs _ _ f => Abs (fun x => let x' := symbolicify_smart_var xs None x in + csef (prepend_prefix (f x') prefix) (smart_add_mapping xs x')) end. End with_var. diff --git a/src/Reflection/Conversion.v b/src/Reflection/Conversion.v index 77d4eed34..3520db4e2 100644 --- a/src/Reflection/Conversion.v +++ b/src/Reflection/Conversion.v @@ -27,11 +27,10 @@ Section language. (@mapf _ ey) end. - Fixpoint map {t} (e : @expr base_type_code op var1 t) + Definition map {t} (e : @expr base_type_code op var1 t) : @expr base_type_code op var2 t := match e with - | Return _ x => Return (mapf x) - | Abs _ _ f => Abs (fun x => @map _ (f (f_var21 _ x))) + | Abs _ _ f => Abs (fun x => mapf (f (mapf_interp_flat_type f_var21 x))) end. End map. diff --git a/src/Reflection/CountLets.v b/src/Reflection/CountLets.v index 00aca28ed..643bb1bf5 100644 --- a/src/Reflection/CountLets.v +++ b/src/Reflection/CountLets.v @@ -27,7 +27,7 @@ Section language. Section gen. Context (count_type_let : flat_type -> nat). - Context (count_type_abs : base_type_code -> nat). + Context (count_type_abs : flat_type -> nat). Fixpoint count_lets_genf {t} (e : exprf t) : nat := match e with @@ -35,11 +35,9 @@ Section language. => count_type_let tx + @count_lets_genf _ (eC (SmartValf var mkVar tx)) | _ => 0 end. - Fixpoint count_lets_gen {t} (e : expr t) : nat + Definition count_lets_gen {t} (e : expr t) : nat := match e with - | Return _ x - => count_lets_genf x - | Abs tx _ f => count_type_abs tx + @count_lets_gen _ (f (mkVar tx)) + | Abs tx _ f => count_type_abs tx + @count_lets_genf _ (f (SmartValf _ mkVar tx)) end. End gen. @@ -52,10 +50,10 @@ Section language. Definition count_lets {t} (e : expr t) : nat := count_lets_gen (fun _ => 1) (fun _ => 0) e. Definition count_binders {t} (e : expr t) : nat - := count_lets_gen count_pairs (fun _ => 1) e. + := count_lets_gen count_pairs count_pairs e. End with_var. - Definition CountLetsGen (count_type_let : flat_type -> nat) (count_type_abs : base_type_code -> nat) {t} (e : Expr t) : nat + Definition CountLetsGen (count_type_let : flat_type -> nat) (count_type_abs : flat_type -> nat) {t} (e : Expr t) : nat := count_lets_gen (fun _ => tt) count_type_let count_type_abs (e _). Definition CountLetBinders {t} (e : Expr t) : nat := count_let_binders (fun _ => tt) (e _). diff --git a/src/Reflection/Equality.v b/src/Reflection/Equality.v index ce2390a64..ad642fe2d 100644 --- a/src/Reflection/Equality.v +++ b/src/Reflection/Equality.v @@ -33,7 +33,6 @@ Section language. | [ |- Prod _ _ = Prod _ _ ] => apply f_equal2 | [ |- Arrow _ _ = Arrow _ _ ] => apply f_equal2 | [ |- Tbase _ = Tbase _ ] => apply f_equal - | [ |- Tflat _ = Tflat _ ] => apply f_equal | [ H : forall Y, _ = true -> _ = Y |- _ = ?Y' ] => is_var Y'; apply H; solve [ t ] | [ H : forall X Y, X = Y -> _ = true |- _ = true ] @@ -59,13 +58,9 @@ Section language. | right pf => right (fun pf' => let pf'' := eq_sym (flat_type_dec_lb _ _ pf') in Bool.diff_true_false (eq_trans pf'' pf)) end. - Fixpoint type_beq (X Y : type) {struct X} : bool + Definition type_beq (X Y : type) : bool := match X, Y with - | Tflat T, Tflat T0 => flat_type_beq T T0 - | Arrow A B, Arrow A0 B0 => (eq_base_type_code A A0 && type_beq B B0)%bool - | Tflat _, _ - | Arrow _ _, _ - => false + | Arrow A B, Arrow A0 B0 => (flat_type_beq A A0 && flat_type_beq B B0)%bool end. Lemma type_dec_bl X : forall Y, type_beq X Y = true -> X = Y. Proof. clear base_type_code_lb; pose proof flat_type_dec_bl; induction X, Y; t. Defined. diff --git a/src/Reflection/Eta.v b/src/Reflection/Eta.v index 62e0a525e..6a15ce60e 100644 --- a/src/Reflection/Eta.v +++ b/src/Reflection/Eta.v @@ -27,16 +27,8 @@ Section language. Section gen_type. Context (exprf_eta : forall {t} (e : exprf t), exprf t). - Fixpoint expr_eta_gen {t} (e : expr t) : expr t - := match e with - | Return _ v => exprf_eta _ v - | Abs src dst f => @Abs - _ _ _ - src dst - (interp_flat_type_eta_gen - (fun x : interp_flat_type var (Tbase src) - => @expr_eta_gen _ (f x))) - end. + Definition expr_eta_gen {t} (e : expr t) : expr (Arrow (domain t) (codomain t)) + := Abs (interp_flat_type_eta_gen (fun x => exprf_eta _ (invert_Abs e x))). End gen_type. Fixpoint exprf_eta_gen {t} (e : exprf t) : exprf t @@ -64,10 +56,10 @@ Section language. Definition expr_eta' {t} := @expr_eta_gen (fun _ _ x => (fst x, snd x)) (@exprf_eta') t. End with_var. - Definition ExprEtaGen eta {t} (e : Expr t) : Expr t + Definition ExprEtaGen eta {t} (e : Expr t) : Expr (Arrow (domain t) (codomain t)) := fun var => expr_eta_gen eta (@exprf_eta_gen var eta) (e var). - Definition ExprEta {t} (e : Expr t) : Expr t + Definition ExprEta {t} (e : Expr t) : Expr (Arrow (domain t) (codomain t)) := fun var => expr_eta (e var). - Definition ExprEta' {t} (e : Expr t) : Expr t + Definition ExprEta' {t} (e : Expr t) : Expr (Arrow (domain t) (codomain t)) := fun var => expr_eta' (e var). End language. diff --git a/src/Reflection/EtaInterp.v b/src/Reflection/EtaInterp.v index 54240947a..52e816df5 100644 --- a/src/Reflection/EtaInterp.v +++ b/src/Reflection/EtaInterp.v @@ -1,6 +1,5 @@ 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. @@ -42,11 +41,9 @@ Section language. 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. + : forall x, + interp (@interp_op) (expr_eta_gen eta exprf_eta (t:=t) e) x = interp (@interp_op) e x. + Proof. t. Qed. End gen_type. (* Local *) Hint Rewrite @interp_expr_eta_gen. @@ -55,10 +52,7 @@ Section language. 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). + : forall x, Interp (@interp_op) (ExprEtaGen eta (t:=t) e) x = Interp (@interp_op) e x. 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. @@ -82,15 +76,15 @@ Section language. 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). + : forall x, interp (@interp_op) (expr_eta (t:=t) e) x = interp (@interp_op) e x. 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). + : forall x, interp (@interp_op) (expr_eta' (t:=t) e) x = interp (@interp_op) e x. 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). + : forall x, Interp (@interp_op) (ExprEta (t:=t) e) x = Interp (@interp_op) e x. 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). + : forall x, Interp (@interp_op) (ExprEta' (t:=t) e) x = Interp (@interp_op) e x. Proof. apply interp_expr_eta'. Qed. End language. diff --git a/src/Reflection/EtaWf.v b/src/Reflection/EtaWf.v index 97da7d1d9..abfef410b 100644 --- a/src/Reflection/EtaWf.v +++ b/src/Reflection/EtaWf.v @@ -24,7 +24,7 @@ Section language. | _ => progress destruct_head' @expr | _ => progress invert_expr_step | [ |- iff _ _ ] => split - | [ |- wf _ _ _ ] => constructor + | [ |- wf _ _ ] => constructor | _ => progress split_iff | _ => rewrite eq_interp_flat_type_eta_gen by assumption | [ H : _ |- _ ] => rewrite eq_interp_flat_type_eta_gen in H by assumption @@ -49,12 +49,11 @@ Section language. (exprf_eta2 : forall {t} (e : exprf t), exprf t) (wff_exprf_eta : forall G t e1 e2, @wff _ _ var1 var2 G t e1 e2 <-> @wff _ _ var1 var2 G t (@exprf_eta1 t e1) (@exprf_eta2 t e2)). - Lemma wf_expr_eta_gen {t e1 e2} G - : wf G - (expr_eta_gen eta exprf_eta1 (t:=t) e1) + Lemma wf_expr_eta_gen {t e1 e2} + : wf (expr_eta_gen eta exprf_eta1 (t:=t) e1) (expr_eta_gen eta exprf_eta2 (t:=t) e2) - <-> wf G e1 e2. - Proof. Admitted. + <-> wf e1 e2. + Proof. unfold expr_eta_gen; t; inversion_wf_step; t. Qed. End gen_type. Lemma wff_exprf_eta_gen {t e1 e2} G @@ -62,7 +61,7 @@ Section language. <-> @wff base_type_code op var1 var2 G t e1 e2. Proof. revert G; induction e1; first [ progress invert_expr | destruct e2 ]; - t; inversion_wff_step; t. + t; inversion_wf_step; t. Qed. End gen_flat_type. @@ -77,16 +76,16 @@ Section language. : wff G (exprf_eta' (t:=t) e1) (exprf_eta' (t:=t) e2) <-> @wff base_type_code op var1 var2 G t e1 e2. Proof. setoid_rewrite wff_exprf_eta_gen; intuition. Qed. - Lemma wf_expr_eta {t e1 e2} G - : wf G (expr_eta (t:=t) e1) (expr_eta (t:=t) e2) - <-> @wf base_type_code op var1 var2 G t e1 e2. + Lemma wf_expr_eta {t e1 e2} + : wf (expr_eta (t:=t) e1) (expr_eta (t:=t) e2) + <-> @wf base_type_code op var1 var2 t e1 e2. Proof. unfold expr_eta, exprf_eta. setoid_rewrite wf_expr_eta_gen; intuition (solve [ eapply wff_exprf_eta_gen; [ | eassumption ]; intuition ] || eauto). Qed. - Lemma wf_expr_eta' {t e1 e2} G - : wf G (expr_eta' (t:=t) e1) (expr_eta' (t:=t) e2) - <-> @wf base_type_code op var1 var2 G t e1 e2. + Lemma wf_expr_eta' {t e1 e2} + : wf (expr_eta' (t:=t) e1) (expr_eta' (t:=t) e2) + <-> @wf base_type_code op var1 var2 t e1 e2. Proof. unfold expr_eta', exprf_eta'. setoid_rewrite wf_expr_eta_gen; intuition (solve [ eapply wff_exprf_eta_gen; [ | eassumption ]; intuition ] || eauto). diff --git a/src/Reflection/ExprInversion.v b/src/Reflection/ExprInversion.v index 6a4523408..450824f2f 100644 --- a/src/Reflection/ExprInversion.v +++ b/src/Reflection/ExprInversion.v @@ -19,12 +19,6 @@ Section language. Local Notation interp_flat_type := (interp_flat_type interp_base_type). Local Notation Expr := (@Expr base_type_code op). - Fixpoint codomain (t : type) : flat_type - := match t with - | Tflat T => T - | Arrow src dst => codomain dst - end. - Section with_var. Context {var : base_type_code -> Type}. @@ -57,10 +51,8 @@ Section language. | Pair _ x _ y => Some (x, y)%core | _ => None end. - Definition invert_Abs {A B} (e : expr (Arrow A B)) : var A -> expr B + Definition invert_Abs {T} (e : expr T) : interp_flat_type_gen var (domain T) -> exprf (codomain T) := match e with Abs _ _ f => f end. - Definition invert_Return {t} (e : expr (Tflat t)) : exprf t - := match e with Return _ v => v end. Definition exprf_code {t} (e : exprf t) : exprf t -> Prop := match e with @@ -71,11 +63,8 @@ Section language. | LetIn _ ex _ eC => fun e' => invert_LetIn e' = Some (existT _ _ (ex, eC)%core) end. - Definition expr_code {t} (e : expr t) : expr t -> Prop - := match e with - | Abs _ _ f => fun e' => invert_Abs e' = f - | Return _ v => fun e' => invert_Return e' = v - end. + Definition expr_code {t} (e1 e2 : expr t) : Prop + := invert_Abs e1 = invert_Abs e2. Definition exprf_encode {t} (x y : exprf t) : x = y -> exprf_code x y. Proof. intro p; destruct p, x; reflexivity. Defined. @@ -104,7 +93,6 @@ Section language. => revert v; refine match e with | Abs _ _ _ => _ - | Return _ _ => _ end end; t'. @@ -126,11 +114,7 @@ Section language. Proof. t. Defined. Lemma invert_Abs_Some {A B e v} - : @invert_Abs A B e = v -> e = Abs v. - Proof. t. Defined. - - Lemma invert_Return_Some {t e v} - : @invert_Return t e = v -> e = Return v. + : @invert_Abs (Arrow A B) e = v -> e = Abs v. Proof. t. Defined. Definition exprf_decode {t} (x y : exprf t) : exprf_code x y -> x = y. @@ -145,11 +129,10 @@ Section language. Defined. Definition expr_decode {t} (x y : expr t) : expr_code x y -> x = y. Proof. - destruct x; simpl; - intro H; - first [ apply invert_Abs_Some in H - | apply invert_Return_Some in H ]; - symmetry; assumption. + destruct x; unfold expr_code; simpl. + intro H; symmetry in H. + apply invert_Abs_Some in H. + symmetry; assumption. Defined. Definition path_exprf_rect {t} {x y : exprf t} (Q : x = y -> Type) (f : forall p, Q (exprf_decode x y p)) @@ -161,31 +144,17 @@ Section language. Proof. intro p; specialize (f (expr_encode x y p)); destruct x, p; exact f. Defined. End with_var. - Lemma interpf_invert_Abs interp_op {A B e} x - : Syntax.interp interp_op (@invert_Abs interp_base_type A B e x) + Lemma interpf_invert_Abs interp_op {T e} x + : Syntax.interpf interp_op (@invert_Abs interp_base_type T e x) = Syntax.interp interp_op e x. - Proof. - refine (match e in expr _ _ t - return match t return expr _ _ t -> _ with - | Arrow src dst - => fun e - => (forall x : interp_base_type src, - interp _ (invert_Abs e x) = interp _ e x) - | Tflat _ => fun _ => True - end e with - | Abs _ _ _ => fun _ => eq_refl - | Return _ _ => I - end x). - Qed. + Proof. destruct e; reflexivity. Qed. End language. -Global Arguments codomain {_} _. Global Arguments invert_Var {_ _ _ _} _. Global Arguments invert_Op {_ _ _ _} _. Global Arguments invert_LetIn {_ _ _ _} _. Global Arguments invert_Pair {_ _ _ _ _} _. -Global Arguments invert_Abs {_ _ _ _ _} _ _. -Global Arguments invert_Return {_ _ _ _} _. +Global Arguments invert_Abs {_ _ _ _} _ _. Ltac invert_one_expr e := preinvert_one_type e; @@ -198,7 +167,6 @@ Ltac invert_expr_step := | [ e : exprf _ _ (Tbase _) |- _ ] => invert_one_expr e | [ e : exprf _ _ (Prod _ _) |- _ ] => invert_one_expr e | [ e : exprf _ _ Unit |- _ ] => invert_one_expr e - | [ e : expr _ _ (Tflat _) |- _ ] => invert_one_expr e | [ e : expr _ _ (Arrow _ _) |- _ ] => invert_one_expr e end. @@ -208,11 +176,11 @@ Ltac invert_match_expr_step := match goal with | [ |- appcontext[match ?e with TT => _ | _ => _ end] ] => invert_one_expr e - | [ |- appcontext[match ?e with Abs _ _ _ => _ | _ => _ end] ] + | [ |- appcontext[match ?e with Abs _ _ _ => _ end] ] => invert_one_expr e | [ H : appcontext[match ?e with TT => _ | _ => _ end] |- _ ] => invert_one_expr e - | [ H : appcontext[match ?e with Abs _ _ _ => _ | _ => _ end] |- _ ] + | [ H : appcontext[match ?e with Abs _ _ _ => _ end] |- _ ] => invert_one_expr e end. @@ -224,7 +192,7 @@ Ltac invert_expr_subst_step_helper guard_tac := | [ H : invert_Op ?e = Some _ |- _ ] => guard_tac H; apply invert_Op_Some in H | [ H : invert_LetIn ?e = Some _ |- _ ] => guard_tac H; apply invert_LetIn_Some in H | [ H : invert_Pair ?e = Some _ |- _ ] => guard_tac H; apply invert_Pair_Some in H - | [ e : expr _ _ (Arrow _ _) |- _ ] + | [ e : expr _ _ _ |- _ ] => guard_tac e; let f := fresh e in let H := fresh in @@ -234,7 +202,6 @@ Ltac invert_expr_subst_step_helper guard_tac := apply invert_Abs_Some in H; subst f | [ H : invert_Abs ?e = _ |- _ ] => guard_tac H; apply invert_Abs_Some in H - | [ H : invert_Return ?e = _ |- _ ] => guard_tac H; apply invert_Return_Some in H end. Ltac invert_expr_subst_step := first [ invert_expr_subst_step_helper ltac:(fun _ => idtac) @@ -243,7 +210,7 @@ Ltac invert_expr_subst := repeat invert_expr_subst_step. Ltac induction_expr_in_using H rect := induction H as [H] using (rect _ _ _); - cbv [exprf_code expr_code invert_Var invert_LetIn invert_Pair invert_Op invert_Abs invert_Return] in H; + cbv [exprf_code expr_code invert_Var invert_LetIn invert_Pair invert_Op invert_Abs] in H; try lazymatch type of H with | Some _ = Some _ => apply option_leq_to_eq in H; unfold option_eq in H | Some _ = None => exfalso; clear -H; solve [ inversion H ] @@ -271,8 +238,6 @@ Ltac inversion_expr_step := => induction_expr_in_using H @path_exprf_rect | [ H : _ = Abs _ |- _ ] => induction_expr_in_using H @path_expr_rect - | [ H : _ = Return _ |- _ ] - => induction_expr_in_using H @path_expr_rect | [ H : Var _ = _ |- _ ] => induction_expr_in_using H @path_exprf_rect | [ H : TT = _ |- _ ] @@ -285,7 +250,5 @@ Ltac inversion_expr_step := => induction_expr_in_using H @path_exprf_rect | [ H : Abs _ = _ |- _ ] => induction_expr_in_using H @path_expr_rect - | [ H : Return _ = _ |- _ ] - => induction_expr_in_using H @path_expr_rect end. Ltac inversion_expr := repeat inversion_expr_step. diff --git a/src/Reflection/FilterLive.v b/src/Reflection/FilterLive.v index 7a22cd9f4..68144c0f7 100644 --- a/src/Reflection/FilterLive.v +++ b/src/Reflection/FilterLive.v @@ -54,17 +54,16 @@ Section language. (@filter_live_namesf prefix remaining _ ey) end. - Fixpoint filter_live_names (prefix remaining : list Name) {t} (e : expr t) : list Name + Definition filter_live_names (prefix remaining : list Name) {t} (e : expr t) : list Name := match e with - | Return _ x => filter_live_namesf prefix remaining x | Abs src _ ef - => let '(ns, remaining') := eta (split_names (Tbase src) remaining) in + => let '(ns, remaining') := eta (split_names src remaining) in match ns with | Some n => let prefix' := (prefix ++ names_to_list n)%list in - @filter_live_names - prefix' remaining' _ - (ef (SmartValf _ (fun _ => prefix') (Tbase src))) + filter_live_namesf + prefix' remaining' + (ef (SmartValf _ (fun _ => prefix') src)) | None => nil end end. diff --git a/src/Reflection/Inline.v b/src/Reflection/Inline.v index fac4d973f..946e84316 100644 --- a/src/Reflection/Inline.v +++ b/src/Reflection/Inline.v @@ -53,10 +53,9 @@ Section language. | Op _ _ op args => Op op (@inline_const_genf _ args) end. - Fixpoint inline_const_gen {t} (e : @expr (@exprf var) t) : @expr var t + Definition inline_const_gen {t} (e : @expr (@exprf var) t) : @expr var t := match e in Syntax.expr _ _ t return @expr var t with - | Return _ x => Return (inline_const_genf x) - | Abs _ _ f => Abs (fun x => @inline_const_gen _ (f (Var x))) + | Abs _ _ f => Abs (fun x => inline_const_genf (f (SmartVarVarf x))) end. Section with_is_const. diff --git a/src/Reflection/InlineCastInterp.v b/src/Reflection/InlineCastInterp.v index 5cf2bf7fe..8e6719f0c 100644 --- a/src/Reflection/InlineCastInterp.v +++ b/src/Reflection/InlineCastInterp.v @@ -106,8 +106,8 @@ Section language. Local Hint Resolve interpf_exprf_of_push_cast. Lemma InterpInlineCast {t} e (Hwf : Wf e) - : interp_type_gen_rel_pointwise (fun _ => @eq _) - (Interp interp_op (@InlineCast t e)) - (Interp interp_op e). + : forall x, + Interp interp_op (@InlineCast t e) x + = Interp interp_op e x. Proof. apply InterpInlineConstGen; auto. Qed. End language. diff --git a/src/Reflection/InlineCastWf.v b/src/Reflection/InlineCastWf.v index 9f5b0b348..c973335d0 100644 --- a/src/Reflection/InlineCastWf.v +++ b/src/Reflection/InlineCastWf.v @@ -69,7 +69,7 @@ Section language. | [ H : forall e, Some _ = Some e -> _ |- _ ] => specialize (H _ eq_refl) | _ => solve [ auto with wf ] - | _ => progress inversion_wff_constr + | _ => progress inversion_wf_constr | _ => progress inversion_flat_type | [ H : context[match ?e with _ => _ end] |- _ ] => invert_one_expr e | [ |- context[match ?e with _ => _ end] ] => invert_one_expr e diff --git a/src/Reflection/InlineInterp.v b/src/Reflection/InlineInterp.v index 707a23fee..7d3909c79 100644 --- a/src/Reflection/InlineInterp.v +++ b/src/Reflection/InlineInterp.v @@ -96,39 +96,20 @@ Section language. Local Hint Resolve interpf_inline_constf. - Lemma interp_inline_const_gen postprocess G {t} e1 e2 - (wf : @wf _ _ G t e1 e2) - (H : forall t x x', - List.In - (existT (fun t : base_type_code => (exprf (Tbase t) * interp_base_type t)%type) t - (x, x')) G - -> interpf interp_op x = x') + Lemma interp_inline_const_gen postprocess {t} e1 e2 + (wf : @wf _ _ t e1 e2) (Hpostprocess : forall t e, interpf interp_op (exprf_of_inline_directive (postprocess t e)) = interpf interp_op e) - : interp_type_gen_rel_pointwise (fun _ => @eq _) - (interp interp_op (inline_const_gen postprocess e1)) - (interp interp_op e2). + : forall x, interp interp_op (inline_const_gen postprocess e1) x = interp interp_op e2 x. Proof. - induction wf. - { eapply (interpf_inline_const_genf postprocess); eauto. } - { simpl in *; intro. - match goal with - | [ H : _ |- _ ] - => apply H; intuition (inversion_sigma; inversion_prod; subst; eauto) - end. } + destruct wf. + simpl in *; intro; eapply (interpf_inline_const_genf postprocess); eauto. Qed. Local Hint Resolve interp_inline_const_gen. - Lemma interp_inline_const is_const G {t} e1 e2 - (wf : @wf _ _ G t e1 e2) - (H : forall t x x', - List.In - (existT (fun t : base_type_code => (exprf (Tbase t) * interp_base_type t)%type) t - (x, x')) G - -> interpf interp_op x = x') - : interp_type_gen_rel_pointwise (fun _ => @eq _) - (interp interp_op (inline_const is_const e1)) - (interp interp_op e2). + Lemma interp_inline_const is_const {t} e1 e2 + (wf : @wf _ _ t e1 e2) + : forall x, interp interp_op (inline_const is_const e1) x = interp interp_op e2 x. Proof. eapply interp_inline_const_gen; eauto. Qed. @@ -136,19 +117,15 @@ Section language. Lemma InterpInlineConstGen postprocess {t} (e : Expr t) (wf : Wf e) (Hpostprocess : forall t e, interpf interp_op (exprf_of_inline_directive (postprocess _ t e)) = interpf interp_op e) - : interp_type_gen_rel_pointwise (fun _ => @eq _) - (Interp interp_op (InlineConstGen postprocess e)) - (Interp interp_op e). + : forall x, Interp interp_op (InlineConstGen postprocess e) x = Interp interp_op e x. Proof. unfold Interp, InlineConst. - eapply (interp_inline_const_gen (postprocess _)); simpl in *; intuition (simpl in *; intuition eauto). + eapply (interp_inline_const_gen (postprocess _)); simpl; intuition. Qed. Lemma InterpInlineConst is_const {t} (e : Expr t) (wf : Wf e) - : interp_type_gen_rel_pointwise (fun _ => @eq _) - (Interp interp_op (InlineConst is_const e)) - (Interp interp_op e). + : forall x, Interp interp_op (InlineConst is_const e) x = Interp interp_op e x. Proof. eapply InterpInlineConstGen; eauto. Qed. diff --git a/src/Reflection/InlineWf.v b/src/Reflection/InlineWf.v index 46f4824b3..64ecb9247 100644 --- a/src/Reflection/InlineWf.v +++ b/src/Reflection/InlineWf.v @@ -117,7 +117,7 @@ Section language. | _ => progress inversion_sigma | _ => progress inversion_prod | _ => progress destruct_head' and - | _ => inversion_wff_step; progress subst + | _ => inversion_wf_step; progress subst | _ => progress specialize_by_assumption | _ => progress break_match | _ => progress invert_inline_directive @@ -168,7 +168,7 @@ Section language. | progress destruct_head' False | progress simpl in * | progress invert_expr - | progress inversion_wff + | progress inversion_wf | progress break_innermost_match_step | congruence | solve [ auto ] ]. @@ -183,26 +183,20 @@ Section language. : @wff var1 var2 G t (inline_constf is_const e1) (inline_constf is_const e2). Proof. eapply wff_inline_const_genf; eauto. Qed. - Lemma wf_inline_const_gen postprocess1 postprocess2 {t} e1 e2 G G' - (H : forall t x x', List.In (existT (fun t : base_type_code => (exprf (Tbase t) * exprf (Tbase t))%type) t (x, x')) G' - -> wff G x x') - (Hwf : wf G' e1 e2) + Lemma wf_inline_const_gen postprocess1 postprocess2 {t} e1 e2 + (Hwf : wf e1 e2) (wf_postprocess : forall G t e1 e2, wff G e1 e2 -> wff_inline_directive G (postprocess1 t e1) (postprocess2 t e2)) - : @wf var1 var2 G t (inline_const_gen postprocess1 e1) (inline_const_gen postprocess2 e2). + : @wf var1 var2 t (inline_const_gen postprocess1 e1) (inline_const_gen postprocess2 e2). Proof. - revert dependent G; induction Hwf; simpl; constructor; intros. - { eapply wff_inline_const_genf; eauto using wff_SmartVarVarf_nil. } - { match goal with H : _ |- _ => apply H end. - intros; destruct_head_hnf' or; t_fin. } + destruct Hwf; constructor; intros. + eapply wff_inline_const_genf; eauto using wff_SmartVarVarf_nil. Qed. - Lemma wf_inline_const is_const {t} e1 e2 G G' - (H : forall t x x', List.In (existT (fun t : base_type_code => (exprf (Tbase t) * exprf (Tbase t))%type) t (x, x')) G' - -> wff G x x') - (Hwf : wf G' e1 e2) - : @wf var1 var2 G t (inline_const is_const e1) (inline_const is_const e2). + Lemma wf_inline_const is_const {t} e1 e2 + (Hwf : wf e1 e2) + : @wf var1 var2 t (inline_const is_const e1) (inline_const is_const e2). Proof. eapply wf_inline_const_gen; eauto. Qed. End with_var. @@ -214,7 +208,7 @@ Section language. : Wf (InlineConstGen postprocess e). Proof. intros var1 var2. - apply (@wf_inline_const_gen var1 var2 (postprocess _) (postprocess _) t (e _) (e _) nil nil); simpl; auto; tauto. + apply (@wf_inline_const_gen var1 var2 (postprocess _) (postprocess _) t (e _) (e _)); simpl; auto. Qed. Lemma Wf_InlineConst is_const {t} (e : Expr t) @@ -222,7 +216,7 @@ Section language. : Wf (InlineConst is_const e). Proof. intros var1 var2. - apply (@wf_inline_const var1 var2 is_const t (e _) (e _) nil nil); simpl; try tauto. + apply (@wf_inline_const var1 var2 is_const t (e _) (e _)); simpl. apply Hwf. Qed. End language. diff --git a/src/Reflection/InputSyntax.v b/src/Reflection/InputSyntax.v index 258241391..12810d20d 100644 --- a/src/Reflection/InputSyntax.v +++ b/src/Reflection/InputSyntax.v @@ -2,7 +2,7 @@ Require Import Coq.Strings.String. Require Import Crypto.Reflection.Syntax. Require Import Crypto.Reflection.SmartMap. -Require Import Crypto.Reflection.Relations. +Require Import Crypto.Reflection.ExprInversion. Require Import Crypto.Reflection.InterpProofs. Require Import Crypto.Util.Tuple. Require Import Crypto.Util.Tactics. @@ -17,14 +17,20 @@ Section language. Context (base_type_code : Type). Local Notation flat_type := (flat_type base_type_code). - Local Notation type := (type base_type_code). + Inductive type := Tflat (A : flat_type) | Arrow (A : flat_type) (B : type). Section expr_param. Context (interp_base_type : base_type_code -> Type). Context (op : flat_type (* input tuple *) -> flat_type (* output type *) -> Type). - Local Notation interp_type := (interp_type interp_base_type). Local Notation interp_flat_type_gen := interp_flat_type. Local Notation interp_flat_type := (interp_flat_type interp_base_type). + + Fixpoint interp_type (t : type) := + match t with + | Tflat A => interp_flat_type A + | Arrow A B => (interp_flat_type A -> interp_type B)%type + end. + Section expr. Context {var : flat_type -> Type}. @@ -37,9 +43,11 @@ Section language. | Pair : forall {t1}, exprf t1 -> forall {t2}, exprf t2 -> exprf (Prod t1 t2) | MatchPair : forall {t1 t2}, exprf (Prod t1 t2) -> forall {tC}, (var t1 -> var t2 -> exprf tC) -> exprf tC. Inductive expr : type -> Type := - | Return {t} : exprf t -> expr t - | Abs {src dst} : (var (Tbase src) -> expr dst) -> expr (Arrow src dst). - Global Coercion Return : exprf >-> expr. + | Return {T} : exprf T -> expr (Tflat T) + | Abs {src dst} : (var src -> expr dst) -> expr (Arrow src dst). + + Definition Fst {t1 t2} (v : exprf (Prod t1 t2)) : exprf t1 := MatchPair v (fun x y => Var x). + Definition Snd {t1 t2} (v : exprf (Prod t1 t2)) : exprf t2 := MatchPair v (fun x y => Var y). End expr. Definition Expr (t : type) := forall var, @expr var t. @@ -69,6 +77,19 @@ Section language. Context {var : base_type_code -> Type} (make_const : forall t, interp_base_type t -> op Unit (Tbase t)). + Fixpoint compilet (t : type) : Syntax.type base_type_code + := Syntax.Arrow + match t with + | Tflat T => Unit + | Arrow A (Tflat B) => A + | Arrow A B + => A * domain (compilet B) + end%ctype + match t with + | Tflat T => T + | Arrow A B => codomain (compilet B) + end. + Fixpoint SmartConst (t : flat_type) : interp_flat_type t -> Syntax.exprf base_type_code op (var:=var) t := match t return interp_flat_type t -> Syntax.exprf _ _ t with | Unit => fun _ => TT @@ -87,16 +108,36 @@ Section language. | MatchPair _ _ ex _ eC => Syntax.LetIn (@compilef _ ex) (fun xy => @compilef _ (eC (fst xy) (snd xy))) end. - Fixpoint compile {t} (e : @expr (interp_flat_type_gen var) t) : @Syntax.expr base_type_code op var t - := match e in expr t return @Syntax.expr _ _ _ t with - | Return _ x => Syntax.Return (compilef x) - | Abs a _ f => Syntax.Abs (fun x : var a => @compile _ (f x)) - end. + (* ugh, so much manual annotation *) + Fixpoint compile {t} (e : @expr (interp_flat_type_gen var) t) : @Syntax.expr base_type_code op var (compilet t) + := match e in expr t return @Syntax.expr _ _ _ (compilet t) with + | Return _ v => Syntax.Abs (fun _ => compilef v) + | Abs src dst f + => let res := fun x => @compile _ (f x) in + match dst + return (_ -> Syntax.expr _ _ (compilet dst)) + -> Syntax.expr _ _ (compilet (Arrow src dst)) + with + | Tflat T + => fun resf => Syntax.Abs (fun x => invert_Abs (resf x) tt) + | Arrow A B as dst' + => match compilet dst' as cdst + return (_ -> Syntax.expr _ _ cdst) + -> Syntax.expr _ _ (Syntax.Arrow + (_ * domain cdst) + (codomain cdst)) + with + | Syntax.Arrow A' B' + => fun resf => Syntax.Abs (fun x : interp_flat_type_gen var (_ * _) + => invert_Abs (resf (fst x)) (snd x)) + end + end res + end. End compile. Definition Compile (make_const : forall t, interp_base_type t -> op Unit (Tbase t)) - {t} (e : Expr t) : Syntax.Expr base_type_code op t + {t} (e : Expr t) : Syntax.Expr base_type_code op (compilet t) := fun var => compile make_const (e _). Section compile_correct. @@ -127,32 +168,83 @@ Section language. end. Qed. - Lemma Compile_correct {t} (e : @Expr t) - : interp_type_gen_rel_pointwise (fun _ => @eq _) - (Syntax.Interp interp_op (Compile make_const e)) - (Interp interp_op e). + Lemma compile_flat_correct {T} (e : expr (Tflat T)) + : forall x, Syntax.interp interp_op (compile make_const e) x = interp interp_op e. + Proof. + intros []; simpl. + let G := match goal with |- ?G => G end in + let G := match (eval pattern T, e in G) with ?G _ _ => G end in + refine match e in expr t return match t return expr t -> _ with + | Tflat T => G T + | _ => fun _ => True + end e + with + | Return _ _ => _ + | Abs _ _ _ => I + end; simpl. + apply compilef_correct. + Qed. + + Lemma Compile_flat_correct_flat {T} (e : Expr (Tflat T)) + : forall x, Syntax.Interp interp_op (Compile make_const e) x = Interp interp_op e. + Proof. apply compile_flat_correct. Qed. + + Lemma Compile_correct {src dst} (e : @Expr (Arrow src (Tflat dst))) + : forall x, Syntax.Interp interp_op (Compile make_const e) x = Interp interp_op e x. Proof. unfold Interp, Compile, Syntax.Interp; simpl. pose (e interp_flat_type) as E. repeat match goal with |- context[e ?f] => change (e f) with E end. clearbody E; clear e. - induction E. - { apply compilef_correct. } - { simpl; auto. } + let G := match goal with |- ?G => G end in + let G := match (eval pattern src, dst, E in G) with ?G _ _ _ => G end in + refine match E in expr t return match t return expr t -> _ with + | Arrow src (Tflat dst) => G src dst + | _ => fun _ => True + end E + with + | Abs src dst e + => match dst + return (forall e : _ -> expr dst, + match dst return expr (Arrow src dst) -> _ with + | Tflat dst => G src dst + | _ => fun _ => True + end (Abs e)) + with + | Tflat _ + => fun e0 x + => _ + | Arrow _ _ => fun _ => I + end e + | Return _ _ => I + end; simpl. + refine match e0 x as e0x in expr t + return match t return expr t -> _ with + | Tflat _ + => fun e0x + => Syntax.interpf _ (invert_Abs (compile _ e0x) _) + = interp _ e0x + | _ => fun _ => True + end e0x + with + | Abs _ _ _ => I + | Return _ _ => _ + end; simpl. + apply compilef_correct. Qed. - - Lemma Compile_flat_correct {t : flat_type} (e : @Expr t) - : Syntax.Interp interp_op (Compile make_const e) = Interp interp_op e. - Proof. exact (@Compile_correct t e). Qed. End compile_correct. End expr_param. End language. +Global Arguments Arrow {_} _ _. +Global Arguments Tflat {_} _. Global Arguments Const {_ _ _ _ _} _. Global Arguments Var {_ _ _ _ _} _. Global Arguments Op {_ _ _ _ _ _} _ _. Global Arguments LetIn {_ _ _ _ _} _ {_} _. Global Arguments MatchPair {_ _ _ _ _ _} _ {_} _. +Global Arguments Fst {_ _ _ _ _ _} _. +Global Arguments Snd {_ _ _ _ _ _} _. Global Arguments Pair {_ _ _ _ _} _ {_} _. Global Arguments Return {_ _ _ _ _} _. Global Arguments Abs {_ _ _ _ _ _} _. diff --git a/src/Reflection/InterpByIso.v b/src/Reflection/InterpByIso.v index 436ac1d96..a971b8e88 100644 --- a/src/Reflection/InterpByIso.v +++ b/src/Reflection/InterpByIso.v @@ -1,5 +1,6 @@ (** * PHOAS interpretation function for any retract of [var:=interp_base_type] *) Require Import Crypto.Reflection.Syntax. +Require Import Crypto.Reflection.ExprInversion. Require Import Crypto.Reflection.SmartMap. Section language. @@ -24,10 +25,9 @@ Section language. | Pair tx ex ty ey => (@interpf_retr _ ex, @interpf_retr _ ey) end. - Fixpoint interp_retr {t} (e : @expr base_type_code op var t) + Definition interp_retr {t} (e : @expr base_type_code op var t) : interp_type interp_base_type t - := match e in expr _ _ t return interp_type interp_base_type t with - | Return t ex => interpf_retr ex - | Abs src dst f => fun x => @interp_retr _ (f (SmartVarfMap var_of_interp x)) - end. + := fun x => interpf_retr (invert_Abs e (SmartVarfMap var_of_interp x)). End language. + +Global Arguments interp_retr _ _ _ _ _ _ _ _ !_ / _ . diff --git a/src/Reflection/InterpByIsoProofs.v b/src/Reflection/InterpByIsoProofs.v index c5006c3a4..2612a1c79 100644 --- a/src/Reflection/InterpByIsoProofs.v +++ b/src/Reflection/InterpByIsoProofs.v @@ -27,13 +27,10 @@ Section language. induction e; simpl; cbv [LetIn.Let_In]; rewrite_hyp ?*; rewrite ?SmartVarfMap_id; reflexivity. Qed. Lemma interp_retr_id {t} (e : @expr interp_base_type t) - : interp_type_gen_rel_pointwise_hetero - (fun _ => eq) - (fun _ => eq) - (interp_retr (fun _ x => x) (fun _ x => x) e) - (interp interp_op e). + : forall x, + interp_retr (fun _ x => x) (fun _ x => x) e x = interp interp_op e x. Proof. - induction e; simpl; repeat intro; subst; auto using interpf_retr_id. + destruct e; simpl; intros; rewrite interpf_retr_id, SmartVarfMap_id; reflexivity. Qed. Section with_var2. @@ -80,38 +77,17 @@ Section language. = interpf_retr var2_of_interp interp_of_var2 e2. Proof. induction Hwf; simpl; rewrite_hyp ?*; try reflexivity; auto. - { match goal with H : _ |- _ => apply H end; intros. - 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. } + { match goal with H : _ |- _ => apply H end. + intros ???; rewrite List.in_app_iff. + intros [?|?]; eauto. } Qed. - Lemma wf_interp_retr G {t} (e1 : @expr var1 t) (e2 : @expr var2 t) - (HG : forall t x1 x2, - List.In (existT _ t (x1, x2)) G - -> interp_of_var1 t x1 = interp_of_var2 t x2) - (Hwf : wf G e1 e2) - : interp_type_gen_rel_pointwise_hetero - (fun _ => eq) - (fun _ => eq) - (interp_retr var1_of_interp interp_of_var1 e1) - (interp_retr var2_of_interp interp_of_var2 e2). + Lemma wf_interp_retr {t} (e1 : @expr var1 t) (e2 : @expr var2 t) + (Hwf : wf e1 e2) + : forall x, + interp_retr var1_of_interp interp_of_var1 e1 x + = interp_retr var2_of_interp interp_of_var2 e2 x. Proof. - induction Hwf; simpl; repeat intro; subst; eauto using wff_interpf_retr. - match goal with H : _ |- _ => apply H end. - simpl; intros; destruct_head' or; auto. - inversion_sigma; inversion_prod; repeat subst; unfold SmartVarfMap; simpl; auto. + destruct Hwf; simpl; repeat intro; subst; eapply wff_interpf_retr; eauto. Qed. End with_var2. @@ -129,17 +105,13 @@ Section language. Proof. erewrite wff_interpf_retr, interpf_retr_id; eauto. Qed. - Lemma wf_interp_retr_correct G {t} (e1 : @expr var t) (e2 : @expr interp_base_type t) - (HG : forall t x1 x2, - List.In (existT _ t (x1, x2)) G - -> interp_of_var t x1 = x2) - (Hwf : wf G e1 e2) - : interp_type_gen_rel_pointwise_hetero - (fun _ => eq) - (fun _ => eq) - (interp_retr var_of_interp interp_of_var e1) - (interp interp_op e2). + Lemma wf_interp_retr_correct {t} (e1 : @expr var t) (e2 : @expr interp_base_type t) + (Hwf : wf e1 e2) + x + : interp_retr var_of_interp interp_of_var e1 x + = interp interp_op e2 x. Proof. - Admitted. + erewrite wf_interp_retr, interp_retr_id; eauto. + Qed. End with_var. End language. diff --git a/src/Reflection/InterpWf.v b/src/Reflection/InterpWf.v index 50d05d032..b3b83698e 100644 --- a/src/Reflection/InterpWf.v +++ b/src/Reflection/InterpWf.v @@ -69,19 +69,10 @@ Section language. Lemma interp_wf {t} {e1 e2 : expr t} - {G} - (HG : forall t x x', - List.In (existT (fun t : base_type_code => (interp_base_type t * interp_base_type t)%type) t (x, x')%core) G - -> x = x') - (Rwf : wf G e1 e2) - : interp_type_gen_rel_pointwise (fun _ => eq) (interp e1) (interp e2). + (Rwf : wf e1 e2) + : forall x, interp e1 x = interp e2 x. Proof. - induction Rwf; simpl; repeat intro; simpl in *; subst; eauto. - match goal with - | [ H : _ |- _ ] - => apply H; intros; progress destruct_head' or; [ | solve [ eauto ] ] - end. - inversion_sigma; inversion_prod; repeat subst; simpl; auto. + destruct Rwf; simpl; eauto. Qed. End wf. End language. diff --git a/src/Reflection/InterpWfRel.v b/src/Reflection/InterpWfRel.v index 9106ecb5a..59ff53ffe 100644 --- a/src/Reflection/InterpWfRel.v +++ b/src/Reflection/InterpWfRel.v @@ -77,27 +77,18 @@ Section language. Lemma interp_wf {t} {e1 : expr1 t} {e2 : expr2 t} - {G} - (HG : forall t x x', - List.In (existT (fun t : base_type_code => (interp_base_type1 t * interp_base_type2 t)%type) t (x, x')%core) G - -> R t x x') - (Rwf : wf G e1 e2) - : interp_type_rel_pointwise2 R (interp1 e1) (interp2 e2). + (Rwf : wf e1 e2) + : interp_type_rel_pointwise R (interp1 e1) (interp2 e2). Proof. - induction Rwf; simpl; repeat intro; simpl in *; eauto. - match goal with - | [ H : _ |- _ ] - => apply H; intros; progress destruct_head' or; [ | solve [ eauto ] ] - end. - inversion_sigma; inversion_prod; repeat subst; simpl; auto. + destruct Rwf; simpl; repeat intro; eauto. Qed. Lemma InterpWf {t} {e : Expr t} (Rwf : Wf e) - : interp_type_rel_pointwise2 R (Interp1 e) (Interp2 e). + : interp_type_rel_pointwise R (Interp1 e) (Interp2 e). Proof. - unfold Interp, Wf in *; apply (interp_wf (G:=nil)); simpl; intuition. + unfold Interp, Wf in *; apply interp_wf; simpl; intuition. Qed. End wf. End language. diff --git a/src/Reflection/Linearize.v b/src/Reflection/Linearize.v index c251c67c7..42ae9c14f 100644 --- a/src/Reflection/Linearize.v +++ b/src/Reflection/Linearize.v @@ -47,10 +47,9 @@ Section language. SmartVarf (t:=Prod A B) (x, y))) end. - Fixpoint linearize {t} (e : expr t) : expr t + Definition linearize {t} (e : expr t) : expr t := match e in Syntax.expr _ _ t return expr t with - | Return _ x => linearizef x - | Abs _ _ f => Abs (fun x => @linearize _ (f x)) + | Abs _ _ f => Abs (fun x => linearizef (f x)) end. End with_var. diff --git a/src/Reflection/LinearizeInterp.v b/src/Reflection/LinearizeInterp.v index 0679fe437..e124ced5b 100644 --- a/src/Reflection/LinearizeInterp.v +++ b/src/Reflection/LinearizeInterp.v @@ -69,18 +69,13 @@ Section language. Local Hint Resolve interpf_linearizef. Lemma interp_linearize {t} e - : interp_type_gen_rel_pointwise (fun _ => @eq _) - (interp interp_op (linearize (t:=t) e)) - (interp interp_op e). + : forall x, interp interp_op (linearize (t:=t) e) x = interp interp_op e x. Proof. - induction e; eauto. - eapply interpf_linearizef. + induction e; simpl; eauto. Qed. Lemma InterpLinearize {t} (e : Expr t) - : interp_type_gen_rel_pointwise (fun _ => @eq _) - (Interp interp_op (Linearize e)) - (Interp interp_op e). + : forall x, Interp interp_op (Linearize e) x = Interp interp_op e x. Proof. unfold Interp, Linearize. eapply interp_linearize. diff --git a/src/Reflection/LinearizeWf.v b/src/Reflection/LinearizeWf.v index 1c21e76be..b58ae654f 100644 --- a/src/Reflection/LinearizeWf.v +++ b/src/Reflection/LinearizeWf.v @@ -159,11 +159,11 @@ Section language. Local Hint Resolve wff_linearizef. - Lemma wf_linearize G {t} e1 e2 - : @wf var1 var2 G t e1 e2 - -> @wf var1 var2 G t (linearize e1) (linearize e2). + Lemma wf_linearize {t} e1 e2 + : @wf var1 var2 t e1 e2 + -> @wf var1 var2 t (linearize e1) (linearize e2). Proof. - induction 1; t_fin idtac. + destruct 1; constructor; auto. Qed. End with_var. diff --git a/src/Reflection/MapCast.v b/src/Reflection/MapCast.v index 50c5198ce..56736fa20 100644 --- a/src/Reflection/MapCast.v +++ b/src/Reflection/MapCast.v @@ -1,6 +1,6 @@ Require Import Crypto.Reflection.Syntax. Require Import Crypto.Reflection.SmartMap. -Require Import Crypto.Reflection.Application. +Require Import Crypto.Reflection.ExprInversion. Require Import Crypto.Util.Sigma. Require Import Crypto.Util.Prod. Require Import Crypto.Util.Option. @@ -28,11 +28,6 @@ Section language. := (SmartValf _ (@failv _)). Local Notation failf t (* {t} : @exprf base_type_code1 op1 ovar t*) := (SmartPairf (SmartFail t)). - Fixpoint fail t : @expr base_type_code1 op1 ovar t - := match t with - | Tflat T => @failf _ - | Arrow A B => Abs (fun _ => @fail B) - end. (** We only ever make use of this when [e1] and [e2] are the same type, and, in fact, the same syntax tree instantiated to @@ -81,24 +76,14 @@ Section language. end. Arguments mapf_interp_cast {_} _ {_} _. (* 8.4 workaround for bad arguments *) - Fixpoint map_interp_cast + Definition map_interp_cast {t1} (e1 : @expr base_type_code1 op1 ovar t1) {t2} (e2 : @expr base_type_code2 op2 interp_base_type2 t2) - {struct e2} - : forall (args2 : interp_all_binders_for' t2 interp_base_type2), - @expr base_type_code1 op1 ovar t1 - := match e1 in expr _ _ t1, e2 in expr _ _ t2 - return forall (args2 : interp_all_binders_for' t2 _), expr _ _ t1 with - | Return t1 ex1, Return t2 ex2 - => fun _ => mapf_interp_cast ex1 ex2 - | Abs src1 dst1 f1, Abs src2 dst2 f2 - => fun args2 - => Abs (fun x - => @map_interp_cast _ (f1 x) _ (f2 (fst args2)) (snd args2)) - | Return _ _, _ - | Abs _ _ _, _ - => fun _ => @fail _ - end. + (args2 : interp_flat_type interp_base_type2 (domain t2)) + : @expr base_type_code1 op1 ovar (Arrow (domain t1) (codomain t1)) + := let f1 := invert_Abs e1 in + let f2 := invert_Abs e2 in + Abs (fun x => @mapf_interp_cast _ (f1 x) _ (f2 args2)). End with_var. End language. @@ -114,7 +99,7 @@ Section homogenous. Definition MapInterpCast transfer_op - {t} (e : Expr base_type_code op t) args - : Expr base_type_code op t + {t} (e : Expr base_type_code op t) (args : interp_flat_type interp_base_type2 (domain t)) + : Expr base_type_code op (Arrow (domain t) (codomain t)) := fun var => map_interp_cast interp_op2 (@failv) transfer_op (e _) (e _) args. End homogenous. diff --git a/src/Reflection/MapCastInterp.v b/src/Reflection/MapCastInterp.v index cb5b57986..e3f93af86 100644 --- a/src/Reflection/MapCastInterp.v +++ b/src/Reflection/MapCastInterp.v @@ -2,7 +2,6 @@ Require Import Crypto.Reflection.Syntax. Require Import Crypto.Reflection.Wf. Require Import Crypto.Reflection.SmartMap. Require Import Crypto.Reflection.ExprInversion. -Require Import Crypto.Reflection.Application. Require Import Crypto.Reflection.MapCast. Require Import Crypto.Reflection.Relations. Require Import Crypto.Reflection.WfProofs. @@ -133,7 +132,7 @@ Section language. Local Ltac break_t := first [ progress subst - | progress inversion_wff + | progress inversion_wf | progress invert_expr_subst | progress inversion_sigma | progress inversion_prod @@ -243,61 +242,50 @@ Section language. Proof. eapply interpf_mapf_interp_cast_and_rel; eassumption. Qed. Lemma interp_map_interp_cast_and_rel - G {t1} e1 ebounds + {t1} e1 ebounds args2 - (Hgood : bounds_are_recursively_good bound_is_good (ApplyAll ebounds (interp_all_binders_for_of' args2))) - (HG : G_invariant_holds G) - (Hwf : wf G e1 ebounds) + (Hgood : bounds_are_recursively_good bound_is_good (invert_Abs ebounds args2)) + (Hwf : wf e1 ebounds) : forall x, R x args2 - -> ApplyInterpedAll' - (interp interp_op1 (@map_interp_cast interp_base_type1 t1 e1 t1 ebounds args2)) x - = ApplyInterpedAll' (interp interp_op1 e1) x - /\ R (ApplyInterpedAll' - (interp interp_op1 (@map_interp_cast interp_base_type1 t1 e1 t1 ebounds args2)) x) - (ApplyInterpedAll' (interp interp_op2 ebounds) args2). - Proof. - induction Hwf; intros. - { eapply interpf_mapf_interp_cast_and_rel; eauto. } - { simpl; match goal with H : _ |- _ => apply H end; eauto. - admit. - admit. - admit. } - Admitted. + -> interp interp_op1 (@map_interp_cast interp_base_type1 t1 e1 t1 ebounds args2) x + = interp interp_op1 e1 x + /\ R (interp interp_op1 (@map_interp_cast interp_base_type1 t1 e1 t1 ebounds args2) x) + (interp interp_op2 ebounds args2). + Proof. destruct Hwf; intros; eapply interpf_mapf_interp_cast_and_rel; eauto. Qed. Lemma interp_map_interp_cast - G {t1} e1 ebounds + {t1} e1 ebounds args2 - (Hgood : bounds_are_recursively_good bound_is_good (ApplyAll ebounds (interp_all_binders_for_of' args2))) - (HG : G_invariant_holds G) - (Hwf : wf G e1 ebounds) + (Hgood : bounds_are_recursively_good bound_is_good (invert_Abs ebounds args2)) + (Hwf : wf e1 ebounds) : forall x, R x args2 - -> ApplyInterpedAll' (interp interp_op1 (@map_interp_cast interp_base_type1 t1 e1 t1 ebounds args2)) x - = ApplyInterpedAll' (interp interp_op1 e1) x. + -> interp interp_op1 (@map_interp_cast interp_base_type1 t1 e1 t1 ebounds args2) x + = interp interp_op1 e1 x. Proof. intros; eapply interp_map_interp_cast_and_rel; eassumption. Qed. Lemma InterpMapInterpCastAndRel {t} e args (Hwf : Wf e) - (Hgood : bounds_are_recursively_good bound_is_good (ApplyAll (e interp_base_type2) (interp_all_binders_for_of' args))) + (Hgood : bounds_are_recursively_good bound_is_good (invert_Abs (e interp_base_type2) args)) : forall x, R x args - -> ApplyInterpedAll' (Interp interp_op1 (@MapInterpCast t e args)) x - = ApplyInterpedAll' (Interp interp_op1 e) x - /\ R (ApplyInterpedAll' (Interp interp_op1 (@MapInterpCast t e args)) x) - (ApplyInterpedAll' (Interp interp_op2 e) args). - Proof. eapply interp_map_interp_cast_and_rel; eauto; simpl; tauto. Qed. + -> Interp interp_op1 (@MapInterpCast t e args) x + = Interp interp_op1 e x + /\ R (Interp interp_op1 (@MapInterpCast t e args) x) + (Interp interp_op2 e args). + Proof. apply interp_map_interp_cast_and_rel; auto. Qed. Lemma InterpMapInterpCast {t} e args (Hwf : Wf e) - (Hgood : bounds_are_recursively_good bound_is_good (ApplyAll (e interp_base_type2) (interp_all_binders_for_of' args))) + (Hgood : bounds_are_recursively_good bound_is_good (invert_Abs (e interp_base_type2) args)) : forall x, R x args - -> ApplyInterpedAll' (Interp interp_op1 (@MapInterpCast t e args)) x - = ApplyInterpedAll' (Interp interp_op1 e) x. - Proof. eapply interp_map_interp_cast; eauto; simpl; tauto. Qed. + -> Interp interp_op1 (@MapInterpCast t e args) x + = Interp interp_op1 e x. + Proof. apply interp_map_interp_cast; auto. Qed. End language. diff --git a/src/Reflection/MapCastWf.v b/src/Reflection/MapCastWf.v index 72a818608..717f8de60 100644 --- a/src/Reflection/MapCastWf.v +++ b/src/Reflection/MapCastWf.v @@ -83,7 +83,7 @@ Section language. Local Ltac break_t := first [ progress subst - | progress inversion_wff + | progress inversion_wf | progress invert_expr_subst | progress inversion_sigma | progress inversion_prod @@ -123,7 +123,7 @@ Section language. end. Qed. - (*Lemma wf_map_interp_cast + Lemma wf_map_interp_cast {t1} e1 e2 ebounds args2 (Hwf_bounds : wf e1 ebounds) @@ -141,7 +141,7 @@ Section language. | [ |- wf _ _ ] => constructor | _ => solve [ eauto using wff_SmartVarf, wff_in_impl_Proper ] end. - Qed.*) + Qed. End with_var. Section gen. @@ -152,7 +152,6 @@ Section language. (@transfer_op ovar1 src1 dst1 src2 dst2 opc1 opc2 e1 args2) (@transfer_op ovar2 src1 dst1 src2 dst2 opc1 opc2 e2 args2)). - Axiom proof_admitted : False. Local Notation MapInterpCast := (@MapInterpCast base_type_code interp_base_type @@ -165,9 +164,7 @@ Section language. (Hwf : Wf e) : Wf (@MapInterpCast t e args). Proof. - revert wff_transfer_op. - case proof_admitted. - (*intros ??; apply wf_map_interp_cast; auto.*) + intros ??; apply wf_map_interp_cast; auto. Qed. End gen. End language. diff --git a/src/Reflection/MultiSizeTest2.v b/src/Reflection/MultiSizeTest2.v index afd53bd19..575b8978a 100644 --- a/src/Reflection/MultiSizeTest2.v +++ b/src/Reflection/MultiSizeTest2.v @@ -151,19 +151,20 @@ Definition Boundify {t1} (e1 : Expr base_type op t1) args2 (** * Examples *) -Example ex1 : Expr base_type op TNat := fun var => +Example ex1 : Expr base_type op (Arrow Unit TNat) := fun var => + Abs (fun _ => LetIn (Constf (t:=Nat) 127) (fun a : var Nat => LetIn (Constf (t:=Nat) 63) (fun b : var Nat => LetIn (Op (tR:=TNat) (Plus Nat) (Pair (Var a) (Var b))) (fun c : var Nat => - Op (Plus Nat) (Pair (Var c) (Var c))))). + Op (Plus Nat) (Pair (Var c) (Var c)))))). -Example ex1f : Expr base_type op (Arrow Nat (Arrow Nat TNat)) := fun var => - Abs (fun a0 => - Abs (fun b0 => +Example ex1f : Expr base_type op (Arrow (TNat * TNat) TNat) := fun var => + Abs (fun a0b0 : interp_flat_type _ (TNat * TNat) => + let a0 := fst a0b0 in let b0 := snd a0b0 in LetIn (Var a0) (fun a : var Nat => LetIn (Var b0) (fun b : var Nat => LetIn (Op (tR:=TNat) (Plus Nat) (Pair (Var a) (Var b))) (fun c : var Nat => - Op (Plus Nat) (Pair (Var c) (Var c))))))). + Op (Plus Nat) (Pair (Var c) (Var c)))))). Eval compute in (Interp (@interp_op) ex1). Eval cbv -[plus] in (Interp (@interp_op) ex1f). diff --git a/src/Reflection/Named/Compile.v b/src/Reflection/Named/Compile.v index 7ffc5fded..55f4aba70 100644 --- a/src/Reflection/Named/Compile.v +++ b/src/Reflection/Named/Compile.v @@ -38,14 +38,13 @@ Section language. end end. - Fixpoint ocompile {t} (e : expr t) (ls : list (option Name)) {struct e} + Definition ocompile {t} (e : expr t) (ls : list (option Name)) : option (nexpr t) := match e in @Syntax.expr _ _ _ t return option (nexpr t) with - | Return _ x => option_map Named.Return (ocompilef x ls) - | Abs _ _ f - => match ls with - | cons (Some n) ls' - => option_map (Named.Abs n) (@ocompile _ (f n) ls') + | Abs src _ f + => match split_onames src ls with + | (Some n, ls')%core + => option_map (Named.Abs n) (@ocompilef _ (f n) ls') | _ => None end end. diff --git a/src/Reflection/Named/EstablishLiveness.v b/src/Reflection/Named/EstablishLiveness.v index bd9a46b9a..7509d5f7a 100644 --- a/src/Reflection/Named/EstablishLiveness.v +++ b/src/Reflection/Named/EstablishLiveness.v @@ -68,15 +68,14 @@ Section language. Fixpoint compute_livenessf ctx {t} e prefix := @compute_livenessf_step (@compute_livenessf) ctx t e prefix. - Fixpoint compute_liveness (ctx : Context) + Definition compute_liveness (ctx : Context) {t} (e : expr Name t) (prefix : list liveness) : list liveness := match e with - | Return _ x => compute_livenessf ctx x prefix | Abs src _ n f - => let prefix := prefix ++ repeat live (count_pairs (Tbase src)) in - let ctx := extend (t:=Tbase src) ctx n (SmartValf _ (fun _ => prefix) (Tbase src)) in - @compute_liveness ctx _ f prefix + => let prefix := prefix ++ repeat live (count_pairs src) in + let ctx := extend (t:=src) ctx n (SmartValf _ (fun _ => prefix) src) in + compute_livenessf ctx f prefix end. Section insert_dead. diff --git a/src/Reflection/Named/RegisterAssign.v b/src/Reflection/Named/RegisterAssign.v index ce8188ee5..70ee5a203 100644 --- a/src/Reflection/Named/RegisterAssign.v +++ b/src/Reflection/Named/RegisterAssign.v @@ -67,18 +67,17 @@ Section language. Fixpoint register_reassignf ctxi ctxr {t} e new_names := @register_reassignf_step (@register_reassignf) ctxi ctxr t e new_names. - Fixpoint register_reassign (ctxi : InContext) (ctxr : ReverseContext) + Definition register_reassign (ctxi : InContext) (ctxr : ReverseContext) {t} (e : expr InName t) (new_names : list (option OutName)) : option (expr OutName t) := match e in Named.expr _ _ _ t return option (expr _ t) with - | Return _ x => option_map Return (register_reassignf ctxi ctxr x new_names) | Abs src _ n f - => let '(n', new_names') := eta (split_onames (Tbase src) new_names) in + => let '(n', new_names') := eta (split_onames src new_names) in match n' with | Some n' - => let ctxi := extendb (t:=src) ctxi n n' in - let ctxr := extendb (t:=src) ctxr n' n in - option_map (Abs n') (@register_reassign ctxi ctxr _ f new_names') + => let ctxi := extend (t:=src) ctxi n n' in + let ctxr := extend (t:=src) ctxr n' n in + option_map (Abs n') (register_reassignf ctxi ctxr f new_names') | None => None end end. diff --git a/src/Reflection/Named/Syntax.v b/src/Reflection/Named/Syntax.v index 2c1f3bd23..996d707a3 100644 --- a/src/Reflection/Named/Syntax.v +++ b/src/Reflection/Named/Syntax.v @@ -47,10 +47,8 @@ Module Export Named. | Pair : forall {t1}, exprf t1 -> forall {t2}, exprf t2 -> exprf (Prod t1 t2). Bind Scope nexpr_scope with exprf. Inductive expr : type -> Type := - | Return {t} : exprf t -> expr t - | Abs {src dst} : Name -> expr dst -> expr (Arrow src dst). + | Abs {src dst} : interp_flat_type_gen (fun _ => Name) src -> exprf dst -> expr (Arrow src dst). Bind Scope nexpr_scope with expr. - Global Coercion Return : exprf >-> expr. (** [SmartVar] is like [Var], except that it inserts pair-projections and [Pair] as necessary to handle [flat_type], and not just [base_type_code] *) @@ -110,10 +108,9 @@ Module Export Named. | Pair _ ex _ ey => @wff ctx _ ex /\ @wff ctx _ ey end%option_pointed_prop. - Fixpoint wf (ctx : Context) {t} (e : expr t) : Prop + Definition wf (ctx : Context) {t} (e : expr t) : Prop := match e with - | Return _ x => prop_of_option (wff ctx x) - | Abs src _ n f => forall v, @wf (extend ctx (t:=Tbase src) n v) _ f + | Abs src _ n f => forall v, prop_of_option (@wff (extend ctx (t:=src) n v) _ f) end. End wf. @@ -166,11 +163,10 @@ Module Export Named. tt (fun _ x => x) interp_op (fun _ y _ f => let x := y in f x) (fun _ x _ y => (x, y)%core). - Fixpoint interp (ctx : Context) {t} (e : expr t) + Definition interp (ctx : Context) {t} (e : expr t) : wf ctx e -> interp_type t := match e in expr t return wf ctx e -> interp_type t with - | Return _ x => interpf ctx x - | Abs _ _ n f => fun good v => @interp _ _ f (good v) + | Abs _ _ n f => fun good v => @interpf _ _ f (good v) end. End with_val_context. End expr_param. @@ -183,7 +179,6 @@ Global Arguments SmartVar {_ _ _ _} _. Global Arguments Op {_ _ _ _ _} _ _. Global Arguments LetIn {_ _ _} _ _ _ {_} _. Global Arguments Pair {_ _ _ _} _ {_} _. -Global Arguments Return {_ _ _ _} _. Global Arguments Abs {_ _ _ _ _} _ _. Global Arguments extend {_ _ _ _} ctx {_} _ _. Global Arguments remove {_ _ _ _} ctx {_} _. diff --git a/src/Reflection/Reify.v b/src/Reflection/Reify.v index 9b3c70d49..99518657b 100644 --- a/src/Reflection/Reify.v +++ b/src/Reflection/Reify.v @@ -81,16 +81,21 @@ Ltac reify_flat_type T := => let v := reify_base_type T in constr:(@Tbase _ v) end. -Ltac reify_type T := +Ltac reify_input_type T := let dummy := debug_enter_reify_type T in lazymatch T with | (?A -> ?B)%type - => let a := reify_base_type A in - let b := reify_type B in + => let a := reify_flat_type A in + let b := reify_input_type B in constr:(@Arrow _ a b) - | _ - => let v := reify_flat_type T in - constr:(@Tflat _ v) + end. +Ltac reify_type T := + let dummy := debug_enter_reify_type T in + lazymatch T with + | (?A -> ?B)%type + => let a := reify_flat_type A in + let b := reify_flat_type B in + constr:(@Syntax.Arrow _ a b) end. Ltac reifyf_var x mkVar := @@ -140,6 +145,8 @@ Ltac reifyf base_type_code interp_base_type op var e := let mkConst T ex := constr:(Const (base_type_code:=base_type_code) (interp_base_type:=interp_base_type) (op:=op) (var:=var) (t:=T) ex) in let mkOp T retT op_code args := constr:(Op (base_type_code:=base_type_code) (interp_base_type:=interp_base_type) (op:=op) (var:=var) (t1:=T) (tR:=retT) op_code args) in let mkMatchPair tC ex eC := constr:(MatchPair (base_type_code:=base_type_code) (interp_base_type:=interp_base_type) (op:=op) (var:=var) (tC:=tC) ex eC) in + let mkFst ex := constr:(Fst (base_type_code:=base_type_code) (interp_base_type:=interp_base_type) (op:=op) (var:=var) ex) in + let mkSnd ex := constr:(Snd (base_type_code:=base_type_code) (interp_base_type:=interp_base_type) (op:=op) (var:=var) ex) in let reify_tag := constr:(@exprf base_type_code interp_base_type op var) in let dummy := debug_enter_reifyf e in lazymatch e with @@ -172,10 +179,20 @@ Ltac reifyf base_type_code interp_base_type op var e := with fun _ v _ => @?C v => C end | match ?ev with pair a b => @?eC a b end => let dummy := debug_reifyf_case "matchpair" in - let t := (let T := match type of eC with _ -> _ -> ?T => T end in reify_flat_type T) in + let T := type of eC in + let t := (let T := match (eval cbv beta in T) with _ -> _ -> ?T => T end in reify_flat_type T) in let v := reify_rec ev in let C := reify_rec eC in - mkMatchPair t v C + let ret := mkMatchPair t v C in + ret + | @fst ?A ?B ?ev => + let dummy := debug_reifyf_case "fst" in + let v := reify_rec ev in + mkFst v + | @snd ?A ?B ?ev => + let dummy := debug_reifyf_case "snd" in + let v := reify_rec ev in + mkSnd v | ?x => let dummy := debug_reifyf_case "generic" in let t := lazymatch type of x with ?t => reify_flat_type t end in @@ -256,14 +273,14 @@ Ltac reify_abs base_type_code interp_base_type op var e := let dummy := debug_enter_reify_abs e in lazymatch e with | (fun x : ?T => ?C) => - let t := reify_base_type T in + let t := reify_flat_type T in (* Work around Coq 8.5 and 8.6 bug *) (* <https://coq.inria.fr/bugs/show_bug.cgi?id=4998> *) (* Avoid re-binding the Gallina variable referenced by Ltac [x] *) (* even if its Gallina name matches a Ltac in this tactic. *) let maybe_x := fresh x in let not_x := fresh x in - lazymatch constr:(fun (x : T) (not_x : var (Tbase t)) (_ : reify_var_for_in_is base_type_code x (Tbase t) not_x) => + lazymatch constr:(fun (x : T) (not_x : var t) (_ : reify_var_for_in_is base_type_code x t not_x) => (_ : reify_abs reify_tag C)) (* [C] here is an open term that references "x" by name *) with fun _ v _ => @?C v => mkAbs t C end | ?x => @@ -280,29 +297,44 @@ Ltac Reify' base_type_code interp_base_type op e := end. Ltac Reify base_type_code interp_base_type op make_const e := let r := Reify' base_type_code interp_base_type op e in + let r := lazymatch type of r with + | forall var, exprf _ _ _ _ => constr:(fun var => Abs (src:=Unit) (fun _ => r var)) + | _ => r + end in constr:(@InputSyntax.Compile base_type_code interp_base_type op make_const _ r). -Ltac lhs_of_goal := lazymatch goal with |- ?R ?LHS ?RHS => LHS end. -Ltac rhs_of_goal := lazymatch goal with |- ?R ?LHS ?RHS => RHS end. +Ltac rhs_of_goal := + lazymatch goal with + | [ |- ?R ?LHS ?RHS ] => RHS + | [ |- forall x, ?R (@?LHS x) (@?RHS x) ] => RHS + end. + +Ltac transitivity_tt term := + first [ transitivity term + | transitivity (term tt) + | let x := fresh in intro x; transitivity (term x); revert x ]. Ltac Reify_rhs_gen Reify prove_interp_compile_correct interp_op try_tac := let rhs := rhs_of_goal in let RHS := Reify rhs in let RHS' := (eval vm_compute in RHS) in - transitivity (Syntax.Interp interp_op RHS'); + transitivity_tt (Syntax.Interp interp_op RHS'); [ - | transitivity (Syntax.Interp interp_op RHS); + | transitivity_tt (Syntax.Interp interp_op RHS); [ lazymatch goal with | [ |- ?R ?x ?y ] => cut (x = y) + | [ |- forall k, ?R (?x k) (?y k) ] + => cut (x = y) end; [ let H := fresh in intro H; rewrite H; reflexivity | apply f_equal; vm_compute; reflexivity ] - | etransitivity; (* first we strip off the [InputSyntax.Compile] - bit; Coq is bad at inferring the type, so we - help it out by providing it *) - [ prove_interp_compile_correct () + | intros; etransitivity; (* first we strip off the [InputSyntax.Compile] + bit; Coq is bad at inferring the type, so we + help it out by providing it *) + [ cbv [InputSyntax.compilet]; + prove_interp_compile_correct () | try_tac ltac:(fun _ => (* now we unfold the interpretation function, @@ -311,7 +343,7 @@ Ltac Reify_rhs_gen Reify prove_interp_compile_correct interp_op try_tac := functions that we're parameterized over. *) abstract ( lazymatch goal with - | [ |- ?R (@InputSyntax.Interp ?base_type_code ?interp_base_type ?op ?interp_op ?t ?e) _ ] + | [ |- appcontext[@InputSyntax.Interp ?base_type_code ?interp_base_type ?op ?interp_op ?t ?e] ] => let interp_base_type' := (eval hnf in interp_base_type) in let interp_op' := (eval hnf in interp_op) in change interp_base_type with interp_base_type'; @@ -320,13 +352,15 @@ Ltac Reify_rhs_gen Reify prove_interp_compile_correct interp_op try_tac := cbv iota beta delta [InputSyntax.Interp interp_type interp_type_gen interp_type_gen_hetero interp_flat_type interp interpf]; reflexivity)) ] ] ]. Ltac prove_compile_correct := - fun _ => lazymatch goal with - | [ |- @Syntax.Interp ?base_type_code ?interp_base_type ?op ?interp_op (@Tflat _ ?t) (@Compile _ _ _ ?make_const _ ?e) = _ ] - => apply (fun pf => @InputSyntax.Compile_flat_correct base_type_code interp_base_type op make_const interp_op pf t e) - | [ |- interp_type_gen_rel_pointwise _ (@Syntax.Interp ?base_type_code ?interp_base_type ?op ?interp_op ?t (@Compile _ _ _ ?make_const _ ?e)) _ ] - => apply (fun pf => @InputSyntax.Compile_correct base_type_code interp_base_type op make_const interp_op pf t e) - end; - let T := fresh in intro T; destruct T; reflexivity. + fun _ => intros; + lazymatch goal with + | [ |- @Syntax.Interp ?base_type_code ?interp_base_type ?op ?interp_op _ (@Compile _ _ _ ?make_const (InputSyntax.Arrow ?src (Tflat ?dst)) ?e) ?x = _ ] + => apply (fun pf => @InputSyntax.Compile_correct base_type_code interp_base_type op make_const interp_op pf src dst e x); + let T := fresh in intro T; destruct T; reflexivity + | [ |- @Syntax.Interp ?base_type_code ?interp_base_type ?op ?interp_op _ (@Compile _ _ _ ?make_const (Tflat ?T) ?e) ?x = _ ] + => apply (fun pf => @InputSyntax.Compile_flat_correct_flat base_type_code interp_base_type op make_const interp_op pf T e x); + let T := fresh in intro T; destruct T; reflexivity + end. Ltac Reify_rhs base_type_code interp_base_type op make_const interp_op := Reify_rhs_gen diff --git a/src/Reflection/Relations.v b/src/Reflection/Relations.v index 4109651c8..160d76b56 100644 --- a/src/Reflection/Relations.v +++ b/src/Reflection/Relations.v @@ -162,20 +162,17 @@ Section language. Section type. Section hetero. - Context (interp_src1 interp_src2 : base_type_code -> Type) + Context (interp_src1 interp_src2 : flat_type -> Type) (interp_dst1 interp_dst2 : flat_type -> Type). Section hetero. Context (Rsrc : forall t, interp_src1 t -> interp_src2 t -> Prop) (Rdst : forall t, interp_dst1 t -> interp_dst2 t -> Prop). - Fixpoint interp_type_gen_rel_pointwise_hetero (t : type) + Definition interp_type_gen_rel_pointwise_hetero (t : type) : interp_type_gen_hetero interp_src1 interp_dst1 t -> interp_type_gen_hetero interp_src2 interp_dst2 t -> Prop - := match t with - | Tflat t => Rdst t - | Arrow src dst => @respectful_hetero _ _ _ _ (Rsrc src) (fun _ _ => interp_type_gen_rel_pointwise_hetero dst) - end. + := @respectful_hetero _ _ _ _ (Rsrc _) (fun _ _ => Rdst _). Global Arguments interp_type_gen_rel_pointwise_hetero _ _ _ / . End hetero. Section hetero_hetero. @@ -186,14 +183,7 @@ Section language. : interp_type_gen_hetero interp_src1 interp_dst1 t1 -> interp_type_gen_hetero interp_src2 interp_dst2 t2 -> Prop - := match t1, t2 with - | Tflat t1, Tflat t2 => Rdst t1 t2 - | Arrow src1 dst1, Arrow src2 dst2 - => @respectful_hetero _ _ _ _ (Rsrc src1 src2) (fun _ _ => interp_type_gen_rel_pointwise_hetero_hetero dst1 dst2) - | Tflat _, _ - | Arrow _ _, _ - => fun _ _ => False - end. + := @respectful_hetero _ _ _ _ (Rsrc _ _) (fun _ _ => Rdst _ _). Global Arguments interp_type_gen_rel_pointwise_hetero_hetero _ _ _ _ / . End hetero_hetero. End hetero. @@ -202,63 +192,36 @@ Section language. Context (interp_flat_type1 interp_flat_type2 : flat_type -> Type) (R : forall t, interp_flat_type1 t -> interp_flat_type2 t -> Prop). - Definition interp_type_gen_rel_pointwise2 + Definition interp_type_gen_rel_pointwise : forall t, interp_type_gen interp_flat_type1 t -> interp_type_gen interp_flat_type2 t -> Prop := interp_type_gen_rel_pointwise_hetero - (fun t => interp_flat_type1 (Tbase t)) (fun t => interp_flat_type2 (Tbase t)) interp_flat_type1 interp_flat_type2 - (fun t => R (Tbase t)) R. - Global Arguments interp_type_gen_rel_pointwise2 _ _ _ / . + interp_flat_type1 interp_flat_type2 + R R. + Global Arguments interp_type_gen_rel_pointwise _ _ _ / . End partially_hetero. - - Section homogenous. - Context (interp_flat_type : flat_type -> Type) - (R : forall t, interp_flat_type t -> interp_flat_type t -> Prop). - Local Notation interp_type_gen := (interp_type_gen interp_flat_type). - Fixpoint interp_type_gen_rel_pointwise (t : type) - : interp_type_gen t -> interp_type_gen t -> Prop := - match t with - | Tflat t => R t - | Arrow _ y => fun f g => forall x, interp_type_gen_rel_pointwise y (f x) (g x) - end. - Global Instance interp_type_gen_rel_pointwise_Reflexive {H : forall t, Reflexive (R t)} - : forall t, Reflexive (interp_type_gen_rel_pointwise t). - Proof. induction t; repeat intro; reflexivity. Qed. - Global Instance interp_type_gen_rel_pointwise_Symmetric {H : forall t, Symmetric (R t)} - : forall t, Symmetric (interp_type_gen_rel_pointwise t). - Proof. induction t; simpl; repeat intro; symmetry; eauto. Qed. - Global Instance interp_type_gen_rel_pointwise_Transitive {H : forall t, Transitive (R t)} - : forall t, Transitive (interp_type_gen_rel_pointwise t). - Proof. induction t; simpl; repeat intro; etransitivity; eauto. Qed. - End homogenous. End type. Section specialized_type. Section hetero. Context (interp_base_type1 interp_base_type2 : base_type_code -> Type). - Definition interp_type_rel_pointwise2 R + Definition interp_type_rel_pointwise R : forall t, interp_type interp_base_type1 t -> interp_type interp_base_type2 t -> Prop - := interp_type_gen_rel_pointwise2 _ _ (interp_flat_type_rel_pointwise R). - Global Arguments interp_type_rel_pointwise2 _ !_ _ _ / . + := interp_type_gen_rel_pointwise _ _ (interp_flat_type_rel_pointwise R). + Global Arguments interp_type_rel_pointwise _ !_ _ _ / . - Definition interp_type_rel_pointwise2_hetero R + Definition interp_type_rel_pointwise_hetero R : forall t1 t2, interp_type interp_base_type1 t1 -> interp_type interp_base_type2 t2 -> Prop - := interp_type_gen_rel_pointwise_hetero_hetero _ _ _ _ (fun t1 t2 => interp_flat_type_rel_pointwise_hetero R (Tbase t1) (Tbase t2)) (interp_flat_type_rel_pointwise_hetero R). - Global Arguments interp_type_rel_pointwise2_hetero _ !_ !_ _ _ / . + := interp_type_gen_rel_pointwise_hetero_hetero _ _ _ _ (interp_flat_type_rel_pointwise_hetero R) (interp_flat_type_rel_pointwise_hetero R). + Global Arguments interp_type_rel_pointwise_hetero _ !_ !_ _ _ / . End hetero. - - Section homogenous. - Context {interp_base_type : base_type_code -> Type}. - Definition interp_type_rel_pointwise R - := interp_type_gen_rel_pointwise _ (@interp_flat_type_rel_pointwise interp_base_type interp_base_type R). - End homogenous. End specialized_type. Section lifting. @@ -324,6 +287,30 @@ Section language. induction t; unfold SmartVarfMap2 in *; simpl in *; destruct_head_hnf unit; try tauto. rewrite_hyp !*; intuition congruence. Qed. + Lemma lift_interp_type_rel_pointwise_f_eq {T} (f g : forall t, _ -> T t) t x y + : interp_type_rel_pointwise + interp_base_type1 interp_base_type2 + (fun t x y => f t x = g t y) + t x y + <-> (forall a b, SmartVarfMap f a = SmartVarfMap g b -> SmartVarfMap f (x a) = SmartVarfMap g (y b)). + Proof. + destruct t; simpl; unfold interp_type_rel_pointwise, respectful_hetero. + setoid_rewrite lift_interp_flat_type_rel_pointwise_f_eq; reflexivity. + Qed. + Lemma lift_interp_type_rel_pointwise_f_eq_id1 (f : forall t, _ -> _) t x y + : interp_type_rel_pointwise + interp_base_type1 interp_base_type2 + (fun t x y => x = f t y) + t x y + <-> (forall a, x (SmartVarfMap f a) = SmartVarfMap f (y a)). + Proof. rewrite lift_interp_type_rel_pointwise_f_eq; setoid_rewrite SmartVarfMap_id; firstorder (subst; eauto). Qed. + Lemma lift_interp_type_rel_pointwise_f_eq_id2 (f : forall t, _ -> _) t x y + : interp_type_rel_pointwise + interp_base_type1 interp_base_type2 + (fun t x y => f t x = y) + t x y + <-> (forall a, SmartVarfMap f (x a) = y (SmartVarfMap f a)). + Proof. rewrite lift_interp_type_rel_pointwise_f_eq; setoid_rewrite SmartVarfMap_id; firstorder (subst; eauto). Qed. End lifting. Local Ltac t := @@ -359,11 +346,11 @@ Section language. Qed. End language. -Global Arguments interp_type_rel_pointwise2 {_ _ _} R {t} _ _. -Global Arguments interp_type_rel_pointwise2_hetero {_ _ _} R {t1 t2} _ _. +Global Arguments interp_type_rel_pointwise {_ _ _} R {t} _ _. +Global Arguments interp_type_rel_pointwise_hetero {_ _ _} R {t1 t2} _ _. Global Arguments interp_type_gen_rel_pointwise_hetero_hetero {_ _ _ _ _} Rsrc Rdst {t1 t2} _ _. Global Arguments interp_type_gen_rel_pointwise_hetero {_ _ _ _ _} Rsrc Rdst {t} _ _. -Global Arguments interp_type_gen_rel_pointwise2 {_ _ _} R {t} _ _. +Global Arguments interp_type_gen_rel_pointwise {_ _ _} R {t} _ _. Global Arguments interp_flat_type_rel_pointwise_gen_Prop {_ _ _ P} and True R {t} _ _. Global Arguments interp_flat_type_rel_pointwise_hetero_gen_Prop {_ _ _ P} and True False R {t1 t2} _ _. Global Arguments interp_flat_type_rel_pointwise_hetero {_ _ _} R {t1 t2} _ _. @@ -372,5 +359,3 @@ Global Arguments interp_flat_type_rel_pointwise1 {_ _} R {t} _. Global Arguments interp_flat_type_relb_pointwise1 {_ _} R {t} _. Global Arguments interp_flat_type_rel_pointwise {_ _ _} R {t} _ _. Global Arguments interp_flat_type_relb_pointwise {_ _ _} R {t} _ _. -Global Arguments interp_type_rel_pointwise {_} _ _ {_} _ _. -Global Arguments interp_type_gen_rel_pointwise {_ _} _ {_} _ _. diff --git a/src/Reflection/SmartBound.v b/src/Reflection/SmartBound.v index d86771216..15eeb7b12 100644 --- a/src/Reflection/SmartBound.v +++ b/src/Reflection/SmartBound.v @@ -1,7 +1,7 @@ Require Import Crypto.Reflection.Syntax. +Require Import Crypto.Reflection.ExprInversion. Require Import Crypto.Reflection.TypeUtil. Require Import Crypto.Reflection.SmartCast. -Require Import Crypto.Reflection.Application. Require Import Crypto.Reflection.SmartMap. Require Import Crypto.Util.Notations. @@ -35,16 +35,12 @@ Section language. Definition bound_flat_type {t} : interp_flat_type interp_base_type_bounds t -> flat_type := @SmartFlatTypeMap2 _ _ interp_base_type_bounds (fun t v => Tbase (bound_base_type t v)) t. - Fixpoint bound_type {t} : forall (e_bounds : interp_type interp_base_type_bounds t) - (input_bounds : interp_all_binders_for' t interp_base_type_bounds), - type - := match t return interp_type _ t -> interp_all_binders_for' t _ -> type with - | Tflat T => fun e_bounds _ => @bound_flat_type T e_bounds - | Arrow A B - => fun e_bounds input_bounds - => Arrow (@bound_base_type A (fst input_bounds)) - (@bound_type B (e_bounds (fst input_bounds)) (snd input_bounds)) - end. + Definition bound_type {t} + (e_bounds : interp_type interp_base_type_bounds t) + (input_bounds : interp_flat_type interp_base_type_bounds (domain t)) + : type + := Arrow (@bound_flat_type (domain t) input_bounds) + (@bound_flat_type (codomain t) (e_bounds input_bounds)). Definition bound_op ovar src1 dst1 src2 dst2 (opc1 : op src1 dst1) (opc2 : op src2 dst2) : exprf (var:=ovar) src1 @@ -117,46 +113,19 @@ Section language. Definition smart_boundf {var t1} (e1 : exprf (var:=var) t1) (bounds : interp_flat_type interp_base_type_bounds t1) : exprf (var:=var) (bound_flat_type bounds) := LetIn e1 (fun e1' => SmartPairf (var:=var) (interpf_smart_bound_exprf e1' bounds)). - Fixpoint UnSmartArrow {P t} - : forall (e_bounds : interp_type interp_base_type_bounds t) - (input_bounds : interp_all_binders_for' t interp_base_type_bounds) - (e : P (SmartArrow (bound_flat_type input_bounds) - (bound_flat_type (ApplyInterpedAll' e_bounds input_bounds)))), - P (bound_type e_bounds input_bounds) - := match t - return (forall (e_bounds : interp_type interp_base_type_bounds t) - (input_bounds : interp_all_binders_for' t interp_base_type_bounds) - (e : P (SmartArrow (bound_flat_type input_bounds) - (bound_flat_type (ApplyInterpedAll' e_bounds input_bounds)))), - P (bound_type e_bounds input_bounds)) - with - | Tflat T => fun _ _ x => x - | Arrow A B => fun e_bounds input_bounds - => @UnSmartArrow - (fun t => P (Arrow (bound_base_type A (fst input_bounds)) t)) - B - (e_bounds (fst input_bounds)) - (snd input_bounds) - end. Definition smart_bound {var t1} (e1 : expr (var:=var) t1) (e_bounds : interp_type interp_base_type_bounds t1) - (input_bounds : interp_all_binders_for' t1 interp_base_type_bounds) + (input_bounds : interp_flat_type interp_base_type_bounds (domain t1)) : expr (var:=var) (bound_type e_bounds input_bounds) - := UnSmartArrow - e_bounds - input_bounds - (SmartAbs - (fun args - => LetIn - args - (fun args - => LetIn - (SmartPairf (interpf_smart_unbound_exprf input_bounds (SmartVarfMap (fun _ => Var) args))) - (fun v => smart_boundf - (ApplyAll e1 (interp_all_binders_for_of' v)) - (ApplyInterpedAll' e_bounds input_bounds))))). + := Abs + (fun args + => LetIn + (SmartPairf (interpf_smart_unbound_exprf input_bounds (SmartVarfMap (fun _ => Var) args))) + (fun v => smart_boundf + (invert_Abs e1 v) + (e_bounds input_bounds))). Definition SmartBound {t1} (e : Expr t1) - (input_bounds : interp_all_binders_for' t1 interp_base_type_bounds) + (input_bounds : interp_flat_type interp_base_type_bounds (domain t1)) : Expr (bound_type _ input_bounds) := fun var => smart_bound (e var) (interp (@interp_op_bounds) (e _)) input_bounds. End smart_bound. diff --git a/src/Reflection/SmartBoundInterp.v b/src/Reflection/SmartBoundInterp.v index 34824e5ce..7723d98c4 100644 --- a/src/Reflection/SmartBoundInterp.v +++ b/src/Reflection/SmartBoundInterp.v @@ -80,7 +80,6 @@ Section language. = 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) @@ -142,5 +141,4 @@ Section language. Proof. intros; eapply InterpSmartBoundAndRel; auto. Qed. - *) End language. diff --git a/src/Reflection/SmartBoundWf.v b/src/Reflection/SmartBoundWf.v index 0b16577d0..6c2846337 100644 --- a/src/Reflection/SmartBoundWf.v +++ b/src/Reflection/SmartBoundWf.v @@ -31,8 +31,7 @@ Section language. Local Notation Expr := (@Expr 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 UnSmartArrow := (@UnSmartArrow _ interp_base_type_bounds bound_base_type). - Local Notation interpf_smart_bound := (@interpf_smart_bound _ op interp_base_type_bounds bound_base_type Cast). + 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 Notation wff_SmartCast_match := (@wff_SmartCast_match _ op _ base_type_bl_transparent Cast wff_Cast). @@ -61,64 +60,6 @@ Section language. | solve [ auto ] ]. Qed. - Fixpoint wf_UnSmartArrow {var1 var2} k t1 G e_bounds input_bounds e1 e2 - (Hwf : wf G e1 e2) - {struct t1} - : wf G - (@UnSmartArrow (fun t => @expr base_type_code op var1 (k t)) t1 e_bounds input_bounds e1) - (@UnSmartArrow (fun t => @expr base_type_code op var2 (k t)) t1 e_bounds input_bounds e2). - Proof. - clear -Hwf wf_UnSmartArrow. - destruct t1 as [t1|s d]; - [ clear wf_UnSmartArrow - | specialize (wf_UnSmartArrow var1 var2 (fun t => k (Arrow (bound_base_type _ (fst input_bounds)) t)) d G (e_bounds (fst input_bounds)) (snd input_bounds)) ]; - set (e1' := e1); set (e2' := e2); - let t := match type of Hwf with wf (t:=?t) _ _ _ => t end in - set (Tt := t) in e1, e2, Hwf; - pose (eq_refl : Tt = t) as Ht; - generalize (eq_refl : e1' = match Ht in (_ = y) return expr _ _ y with eq_refl => e1 end); - generalize (eq_refl : e2' = match Ht in (_ = y) return expr _ _ y with eq_refl => e2 end); - clearbody Ht; revert Ht; - clearbody e1' e2'; revert e1' e2'; - clearbody Tt; - destruct Hwf; - intros; simpl in *; repeat subst; try discriminate; - break_innermost_match; - inversion_type; subst; simpl. - { constructor; assumption. } - { constructor; assumption. } - { apply wf_UnSmartArrow; clear wf_UnSmartArrow. - match goal with - | [ |- context[match k ?x with _ => _ end] ] - => set (kx := k x) in * - end. - repeat match goal with - | [ H : context[k ?x] |- _ ] - => change (k x) with kx in H - | [ |- context[k ?x] ] - => change (k x) with kx - end. - destruct kx; - inversion_type; subst; simpl; - try tauto; - try (constructor; assumption). } - { apply wf_UnSmartArrow; clear wf_UnSmartArrow. - match goal with - | [ |- context[match k ?x with _ => _ end] ] - => set (kx := k x) in * - end. - repeat match goal with - | [ H : context[k ?x] |- _ ] - => change (k x) with kx in H - | [ |- context[k ?x] ] - => change (k x) with kx - end. - destruct kx; - inversion_type; break_innermost_match; subst; simpl; - try tauto; - try (constructor; assumption). } - Qed. - Local Hint Resolve List.in_app_or List.in_or_app. Lemma wff_SmartPairf_interpf_smart_unbound_exprf var1 var2 t input_bounds x1 x2 @@ -149,23 +90,41 @@ Section language. Local Hint Resolve wff_SmartPairf_interpf_smart_unbound_exprf : wf. - Axiom proof_admitted : False. + Lemma wff_SmartPairf_interpf_smart_bound_exprf var1 var2 t x1 x2 output_bounds + : wff (flatten_binding_list x1 x2) + (SmartPairf + (var:=var1) + (interpf_smart_bound_exprf (t:=t) x1 output_bounds)) + (SmartPairf + (var:=var2) + (interpf_smart_bound_exprf x2 output_bounds)). + Proof. + clear -wff_Cast. + unfold SmartPairf, SmartVarfMap, interpf_smart_bound_exprf; induction t; + repeat match goal with + | _ => progress simpl in * + | [ |- wff _ (Cast _ _ _ _) (Cast _ _ _ _) ] + => apply wff_Cast + | [ |- wff _ _ _ ] + => constructor + | _ => solve [ auto with wf ] + | _ => eapply wff_in_impl_Proper; [ solve [ eauto ] | ] + | _ => intro + end. + Qed. + + Local Hint Resolve wff_SmartPairf_interpf_smart_bound_exprf : wf. - Lemma wf_smart_bound {var1 var2 t1} G e1 e2 e_bounds input_bounds - (Hwf : wf G e1 e2) - : wf G - (@smart_bound var1 t1 e1 e_bounds input_bounds) + Lemma wf_smart_bound {var1 var2 t1} e1 e2 e_bounds input_bounds + (Hwf : wf e1 e2) + : wf (@smart_bound var1 t1 e1 e_bounds input_bounds) (@smart_bound var2 t1 e2 e_bounds input_bounds). Proof. clear -wff_Cast Hwf. - unfold SmartBound.smart_bound. - apply wf_UnSmartArrow with (k:=fun x => x). - apply wf_SmartAbs; intros. - repeat constructor; auto with wf; + destruct Hwf; unfold SmartBound.smart_bound. + repeat constructor; auto with wf; intros; try (eapply wff_in_impl_Proper; [ solve [ eauto with wf ] | ]); auto. - { case proof_admitted. } - { case proof_admitted. } Qed. Lemma Wf_SmartBound {t1} e input_bounds diff --git a/src/Reflection/SmartMap.v b/src/Reflection/SmartMap.v index c18b2b8fb..5cddc0418 100644 --- a/src/Reflection/SmartMap.v +++ b/src/Reflection/SmartMap.v @@ -24,7 +24,6 @@ Section homogenous_type. another kind, and simultaneously mapping a function over the base values (e.g., [Var] (for turning [var] into [exprf]) or [Const] (for turning [interp_base_type] into [exprf])). *) - Fixpoint smart_interp_flat_map {f g} (h : forall x, f x -> g (Tbase x)) (tt : g Unit) @@ -51,58 +50,23 @@ Section homogenous_type. (@smart_interp_flat_map2 f1 f2 g h tt pair A (fst v1) (fst v2)) (@smart_interp_flat_map2 f1 f2 g h tt pair B (snd v1) (snd v2)) end. - Fixpoint smart_interp_map_hetero {f g g'} - (h : forall x, f x -> g (Tflat (Tbase x))) - (tt : g Unit) - (pair : forall A B, g (Tflat A) -> g (Tflat B) -> g (Prod A B)) - (abs : forall A B, (g' A -> g B) -> g (Arrow A B)) - {t} - : interp_type_gen_hetero g' (interp_flat_type f) t -> g t - := match t return interp_type_gen_hetero g' (interp_flat_type f) t -> g t with - | Tflat _ => @smart_interp_flat_map f (fun x => g (Tflat x)) h tt pair _ - | Arrow A B => fun v => abs _ _ - (fun x => @smart_interp_map_hetero f g g' h tt pair abs B (v x)) - end. - Fixpoint smart_interp_map_gen {f g} - (h : forall x, f x -> g (Tflat (Tbase x))) - (h' : forall x, g (Tflat (Tbase x)) -> f x) - (flat_map : forall t, interp_flat_type f t -> g t) - (abs : forall A B, (g (Tflat (Tbase A)) -> g B) -> g (Arrow A B)) - {t} - : interp_type_gen (interp_flat_type f) t -> g t - := match t return interp_type_gen (interp_flat_type f) t -> g t with - | Tflat T => flat_map T - | Arrow A B => fun v => abs _ _ - (fun x => @smart_interp_map_gen f g h h' flat_map abs B (v (h' _ x))) - end. - Definition smart_interp_map {f g} - (h : forall x, f x -> g (Tflat (Tbase x))) - (h' : forall x, g (Tflat (Tbase x)) -> f x) + Definition smart_interp_map_hetero {f g g'} + (h : forall x, f x -> g (Tbase x)) (tt : g Unit) - (pair : forall A B, g (Tflat A) -> g (Tflat B) -> g (Prod A B)) - (abs : forall A B, (g (Tflat (Tbase A)) -> g B) -> g (Arrow A B)) + (pair : forall A B, g A -> g B -> g (Prod A B)) + (abs : forall A B, (g A -> g B) -> g' (Arrow A B)) {t} - : interp_type_gen (interp_flat_type f) t -> g t - := @smart_interp_map_gen f g h h' (@smart_interp_flat_map f (fun x => g (Tflat x)) h tt pair) abs t. + : interp_type_gen_hetero g (interp_flat_type f) t -> g' t + := match t return interp_type_gen_hetero g (interp_flat_type f) t -> g' t with + | Arrow A B => fun v => abs _ _ + (fun x => @smart_interp_flat_map f g h tt pair _ (v x)) + end. Fixpoint SmartValf {T} (val : forall t : base_type_code, T t) t : interp_flat_type T t := match t return interp_flat_type T t with | Syntax.Tbase _ => val _ | Unit => tt | Prod A B => (@SmartValf T val A, @SmartValf T val B) end. - Fixpoint SmartArrow (A : flat_type) (B : type) : type - := match A with - | Syntax.Tbase A' => Arrow A' B - | Unit => B - | Prod A0 A1 - => SmartArrow A0 (SmartArrow A1 B) - end. - Fixpoint SmartAbs {A B} {struct A} : forall (f : exprf A -> expr B), expr (SmartArrow A B) - := match A return (exprf A -> expr B) -> expr (SmartArrow A B) with - | Syntax.Tbase x => fun f => Abs (fun x => f (Var x)) - | Unit => fun f => f TT - | Prod x y => fun f => @SmartAbs x _ (fun x' => @SmartAbs y _ (fun y' => f (Pair x' y'))) - end. (** [SmartVar] is like [Var], except that it inserts pair-projections and [Pair] as necessary to handle [flat_type], @@ -209,12 +173,13 @@ Section homogenous_type. | Prod A B => fun v xy => (@SmartFlatTypeMapUnInterp _ _ _ f fv A _ (fst xy), @SmartFlatTypeMapUnInterp _ _ _ f fv B _ (snd xy)) end. - Definition SmartVarMap {var var'} (f : forall t, var t -> var' t) (f' : forall t, var' t -> var t) {t} - : interp_type_gen (interp_flat_type var) t -> interp_type_gen (interp_flat_type var') t - := @smart_interp_map var (interp_type_gen (interp_flat_type var')) f f' tt (fun A B x y => pair x y) (fun A B f x => f x) t. - Definition SmartVarMap_hetero {vars vars' var var'} (f : forall t, var t -> var' t) (f' : forall t, vars' t -> vars t) {t} - : interp_type_gen_hetero vars (interp_flat_type var) t -> interp_type_gen_hetero vars' (interp_flat_type var') t - := @smart_interp_map_hetero var (interp_type_gen_hetero vars' (interp_flat_type var')) vars f tt (fun A B x y => pair x y) (fun A B f x => f (f' _ x)) t. + Definition SmartVarMap {var' var''} (f : forall t, var' t -> var'' t) (f' : forall t, var'' t -> var' t) {t} + : interp_type_gen (interp_flat_type var') t -> interp_type_gen (interp_flat_type var'') t + := match t return interp_type_gen (interp_flat_type var') t -> interp_type_gen (interp_flat_type var'') t with + | Arrow src dst => fun F x => SmartVarfMap f (F (SmartVarfMap f' x)) + end. + Lemma SmartVarMap_id {var' t} x v : @SmartVarMap var' var' (fun _ x => x) (fun _ x => x) t x v = x v. + Proof. destruct t; simpl; rewrite !SmartVarfMap_id; reflexivity. Qed. Definition SmartVarVarf {t} : interp_flat_type var t -> interp_flat_type exprfb t := SmartVarfMap (fun t => Var). End homogenous_type. @@ -233,9 +198,7 @@ Global Arguments SmartFlatTypeMap {_ _} _ {_} _. Global Arguments SmartFlatTypeUnMap {_} _. Global Arguments SmartFlatTypeMapInterp {_ _ _ _} _ {_} _. Global Arguments SmartFlatTypeMapUnInterp {_ _ _ _ _} fv {_ _} _. -Global Arguments SmartVarMap_hetero {_ _ _ _ _} _ _ {_} _. Global Arguments SmartVarMap {_ _ _} _ _ {!_} _ / . -Global Arguments SmartAbs {_ _ _ _ _} _. Section hetero_type. Fixpoint flatten_flat_type {base_type_code} (t : flat_type (flat_type base_type_code)) : flat_type base_type_code diff --git a/src/Reflection/Syntax.v b/src/Reflection/Syntax.v index ee60265e0..d77731633 100644 --- a/src/Reflection/Syntax.v +++ b/src/Reflection/Syntax.v @@ -16,10 +16,9 @@ Section language. Inductive flat_type := Tbase (T : base_type_code) | Unit | Prod (A B : flat_type). Bind Scope ctype_scope with flat_type. - Inductive type := Tflat (T : flat_type) | Arrow (A : base_type_code) (B : type). + Inductive type := Arrow (A : flat_type) (B : flat_type). Bind Scope ctype_scope with type. - Global Coercion Tflat : flat_type >-> type. Infix "*" := Prod : ctype_scope. Notation "A -> B" := (Arrow A B) : ctype_scope. Local Coercion Tbase : base_type_code >-> flat_type. @@ -38,20 +37,16 @@ Section language. end. End tuple. + Definition domain (t : type) : flat_type + := match t with Arrow src dst => src end. + Definition codomain (t : type) : flat_type + := match t with Arrow src dst => dst end. + Section interp. - Section type. - Section hetero. - Context (interp_src_type : base_type_code -> Type). - Context (interp_flat_type : flat_type -> Type). - Fixpoint interp_type_gen_hetero (t : type) := - match t with - | Tflat t => interp_flat_type t - | Arrow x y => (interp_src_type x -> interp_type_gen_hetero y)%type - end. - End hetero. - Definition interp_type_gen (interp_flat_type : flat_type -> Type) - := interp_type_gen_hetero interp_flat_type interp_flat_type. - End type. + Definition interp_type_gen_hetero (interp_src interp_dst : flat_type -> Type) (t : type) := + (interp_src match t with Arrow x y => x end -> interp_dst match t with Arrow x y => y end)%type. + Definition interp_type_gen (interp_flat_type : flat_type -> Type) + := interp_type_gen_hetero interp_flat_type interp_flat_type. Section flat_type. Context (interp_base_type : base_type_code -> Type). Fixpoint interp_flat_type (t : flat_type) := @@ -82,10 +77,8 @@ Section language. | Pair {tx} (ex : exprf tx) {ty} (ey : exprf ty) : exprf (Prod tx ty). Bind Scope expr_scope with exprf. Inductive expr : type -> Type := - | Return {t} (ex : exprf t) : expr t - | Abs {src dst} (f : var src -> expr dst) : expr (Arrow src dst). + | Abs {src dst} (f : interp_flat_type_gen var src -> exprf dst) : expr (Arrow src dst). Bind Scope expr_scope with expr. - Global Coercion Return : exprf >-> expr. End expr. Definition Expr (t : type) := forall var, @expr var t. @@ -107,11 +100,16 @@ Section language. Fixpoint interpf {t} e := @interpf_step (@interpf) t e. - Fixpoint interp {t} (e : @expr interp_type t) : interp_type t - := match e in expr t return interp_type t with - | Return _ x => interpf x - | Abs _ _ f => fun x => @interp _ (f x) - end. + Definition interp {t} (e : @expr interp_base_type t) : interp_type t + := fun x + => @interpf + _ + (match e in @expr _ t + return interp_flat_type (domain t) + -> exprf (codomain t) + with + | Abs _ _ f => f + end x). Definition Interp {t} (E : Expr t) : interp_type t := interp (E _). End interp. @@ -123,14 +121,14 @@ Global Arguments Unit {_}%type_scope. Global Arguments Prod {_}%type_scope (_ _)%ctype_scope. Global Arguments Arrow {_}%type_scope (_ _)%ctype_scope. Global Arguments Tbase {_}%type_scope _%ctype_scope. -Global Arguments Tflat {_}%type_scope _%ctype_scope. +Global Arguments domain {_}%type_scope _%ctype_scope. +Global Arguments codomain {_}%type_scope _%ctype_scope. Global Arguments Var {_ _ _ _} _. Global Arguments TT {_ _ _}. Global Arguments Op {_ _ _ _ _} _ _. Global Arguments LetIn {_ _ _ _} _ {_} _. Global Arguments Pair {_ _ _ _} _ {_} _. -Global Arguments Return {_ _ _ _} _. Global Arguments Abs {_ _ _ _ _} _. Global Arguments interp_type_gen_hetero {_} _ _ _. Global Arguments interp_type_gen {_} _ _. @@ -139,6 +137,7 @@ Global Arguments interp_type {_} _ _. Global Arguments Interp {_ _ _} interp_op {t} _. Global Arguments interp {_ _ _} interp_op {t} _. Global Arguments interpf {_ _ _} interp_op {t} _. +Global Arguments interp _ _ _ _ _ !_ / . Module Export Notations. Notation "()" := (@Unit _) : ctype_scope. diff --git a/src/Reflection/TestCase.v b/src/Reflection/TestCase.v index c4287239e..3cbe70594 100644 --- a/src/Reflection/TestCase.v +++ b/src/Reflection/TestCase.v @@ -60,17 +60,26 @@ Goal (flat_type base_type -> Type) -> False. let x := reifyf base_type interp_base_type op var (1 + 1)%nat in pose x. let x := Reify' (1 + 1)%nat in unify x (fun var => Return (Op Add (Pair (InputSyntax.Const (interp_base_type:=interp_base_type) (var:=var) (t:=Tbase Tnat) (op:=op) 1) (InputSyntax.Const (interp_base_type:=interp_base_type) (var:=var) (t:=Tbase Tnat) (op:=op) 1)))). let x := reify_abs base_type interp_base_type op var (fun x => x + 1)%nat in pose x. - let x := Reify' (fun x => x + 1)%nat in unify x (fun var => Abs (fun y => Op Add (Pair (Var y) (InputSyntax.Const (interp_base_type:=interp_base_type) (var:=var) (t:=Tbase Tnat) (op:=op) 1)))). + let x := Reify' (fun x => x + 1)%nat in unify x (fun var => Abs (fun y => Return (Op Add (Pair (Var y) (InputSyntax.Const (interp_base_type:=interp_base_type) (var:=var) (t:=Tbase Tnat) (op:=op) 1))))). let x := reifyf base_type interp_base_type op var (let '(a, b) := (1, 1) in a + b)%nat in pose x. let x := reifyf base_type interp_base_type op var (let '(a, b, c) := (1, 1, 1) in a + b + c)%nat in pose x. let x := Reify' (fun x => let '(a, b) := (1, 1) in a + x)%nat in let x := (eval vm_compute in x) in pose x. + let x := Reify' (fun x => let '(a, b, c, (d, e), f) := x in a + b + c + d + e + f)%nat in let x := (eval vm_compute in x) in pose x. + let x := Reify' (fun x => let '(a, b) := x in let '(a, c) := a in let '(a, d) := a in a + b + c + d)%nat in let x := (eval vm_compute in x) in pose x. + let x := Reify' (fun ab0 : nat * nat * nat * nat => let (f, g6) := fst ab0 in + let (f0, g7) := f in + let ab3 := (1, 1) in + let ab21 := (1, 1) in + let z := snd ab3 + snd ab21 in z + z)%nat in let x := (eval vm_compute in x) in pose x. + let x := Reify' (fun ab0 : nat * nat * nat => let (f, g7) := fst ab0 in 1 + 1) in let x := (eval vm_compute in x) in pose x. let x := Reify' (fun x => let '(a, b) := (1, 1) in a + x)%nat in unify x (fun var => Abs (fun x' => let c1 := (InputSyntax.Const (interp_base_type:=interp_base_type) (var:=var) (t:=Tbase Tnat) (op:=op) 1) in - MatchPair (tC:=tnat) (Pair c1 c1) - (fun x0 _ : var tnat => Op Add (Pair (Var x0) (Var x'))))). + Return (MatchPair (tC:=tnat) (Pair c1 c1) + (fun x0 y0 : var tnat => Op Add (Pair (Var x0) (Var x')))))). let x := reifyf base_type interp_base_type op var (let x := 5 in let y := 6 in (let a := 1 in let '(c, d) := (2, 3) in a + x + c + d) + y)%nat in pose x. - let x := Reify' (fun x y => (let a := 1 in let '(c, d) := (2, 3) in a + x + c + d) + y)%nat in pose x. + let x := Reify' (let x := 1 in let y := 1 in (let a := 1 in let '(c, d) := (2, 3) in a + x + c + d) + y)%nat in pose x. + let x := Reify' (fun xy => let '(x, y) := xy in (let a := 1 in let '(c, d) := (2, 3) in a + x + c + d) + y)%nat in pose x. Abort. @@ -85,14 +94,14 @@ Abort. Import Linearize Inline. Goal True. - let x := Reify (fun x y => (let a := 1 in let '(c, d) := (2, 3) in a + x - a + c + d) + y)%nat in + let x := Reify (fun xy => let '(x, y) := xy in (let a := 1 in let '(c, d) := (2, 3) in a + x - a + c + d) + y)%nat in pose (InlineConst is_const (Linearize x)) as e. vm_compute in e. Abort. -Definition example_expr : Syntax.Expr base_type op (Arrow Tnat (Arrow Tnat (Tflat tnat))). +Definition example_expr : Syntax.Expr base_type op (Syntax.Arrow (tnat * tnat) tnat). Proof. - let x := Reify (fun z w => let unused := 1 + 1 in let x := 1 in let y := 1 in (let a := 1 in let '(c, d) := (2, 3) in a + x + (x + x) + (x + x) - (x + x) - a + c + d) + y + z + w)%nat in + let x := Reify (fun zw => let '(z, w) := zw in let unused := 1 + 1 in let x := 1 in let y := 1 in (let a := 1 in let '(c, d) := (2, 3) in a + x + (x + x) + (x + x) - (x + x) - a + c + d) + y + z + w)%nat in exact x. Defined. @@ -138,7 +147,7 @@ Lemma example_expr_wf_slow : Wf example_expr. Proof. Time (vm_compute; intros; repeat match goal with - | [ |- wf _ _ _ ] => constructor; intros + | [ |- wf _ _ ] => constructor; intros | [ |- wff _ _ _ ] => constructor; intros | [ |- List.In _ _ ] => vm_compute | [ |- ?x = ?x \/ _ ] => left; reflexivity @@ -222,6 +231,6 @@ Module bounds. end. Compute (fun x xpf y ypf => proj1_sig (Syntax.Interp interp_op_bounds example_expr - (exist _ {| lower := 0 ; value := x ; upper := 10 |} xpf) - (exist _ {| lower := 100 ; value := y ; upper := 1000 |} ypf))). + (exist _ {| lower := 0 ; value := x ; upper := 10 |} xpf, + exist _ {| lower := 100 ; value := y ; upper := 1000 |} ypf))). End bounds. diff --git a/src/Reflection/TypeInversion.v b/src/Reflection/TypeInversion.v index 8a10a36a8..7d0999061 100644 --- a/src/Reflection/TypeInversion.v +++ b/src/Reflection/TypeInversion.v @@ -49,23 +49,12 @@ Section language. Definition preinvert_Arrow (P : type base_type_code -> Type) (Q : forall A B, P (Arrow A B) -> Type) : (forall t (p : P t), match t return P t -> Type with | Arrow A B => Q A B - | _ => fun _ => True end p) -> forall A B p, Q A B p. Proof. intros H A B p; specialize (H _ p); assumption. Defined. - Definition preinvert_Tflat (P : type base_type_code -> Type) (Q : forall T, P (Tflat T) -> Type) - : (forall t (p : P t), match t return P t -> Type with - | Tflat T => Q T - | _ => fun _ => True - end p) - -> forall T p, Q T p. - Proof. - intros H T p; specialize (H _ p); assumption. - Defined. - Section encode_decode. Definition flat_type_code (t1 t2 : flat_type base_type_code) : Prop := match t1, t2 with @@ -79,13 +68,7 @@ Section language. end. Definition type_code (t1 t2 : type base_type_code) : Prop - := match t1, t2 with - | Tflat t1, Tflat t2 => t1 = t2 - | Arrow A B, Arrow A' B' => A = A' /\ B = B' - | Tflat _, _ - | Arrow _ _, _ - => False - end. + := domain t1 = domain t2 /\ codomain t1 = codomain t2. Definition flat_type_encode (x y : flat_type base_type_code) : x = y -> flat_type_code x y. Proof. intro p; destruct p, x; repeat constructor. Defined. @@ -151,11 +134,6 @@ Ltac preinvert_one_type e := | ?P Unit => revert dependent e; refine (preinvert_Unit P _ _) - | ?P (Tflat ?T) - => is_var T; - move e at top; - revert dependent T; - refine (preinvert_Tflat P _ _) | ?P (Arrow ?A ?B) => is_var A; is_var B; move e at top; revert dependent A; intros A e; @@ -192,10 +170,6 @@ Ltac inversion_flat_type := repeat inversion_flat_type_step. Ltac inversion_type_step := lazymatch goal with - | [ H : _ = Tflat _ |- _ ] - => induction_type_in_using H @path_type_rect - | [ H : Tflat _ = _ |- _ ] - => induction_type_in_using H @path_type_rect | [ H : _ = Arrow _ _ |- _ ] => induction_type_in_using H @path_type_rect | [ H : Arrow _ _ = _ |- _ ] diff --git a/src/Reflection/Wf.v b/src/Reflection/Wf.v index 3b48853c6..91a99b150 100644 --- a/src/Reflection/Wf.v +++ b/src/Reflection/Wf.v @@ -50,14 +50,13 @@ Section language. wff G e1 e1' -> wff G e2 e2' -> wff G (Pair e1 e2) (Pair e1' e2'). - Inductive wf : list (sigT eP) -> forall {t}, @expr var1 t -> @expr var2 t -> Prop := - | WfReturn : forall t G e e', @wff G t e e' -> wf G (Return e) (Return e') - | WfAbs : forall A B G e e', - (forall x x', @wf ((x == x') :: G) B (e x) (e' x')) - -> @wf G (Arrow A B) (Abs e) (Abs e'). + Inductive wf : forall {t}, @expr var1 t -> @expr var2 t -> Prop := + | WfAbs : forall A B e e', + (forall x x', @wff (flatten_binding_list x x') B (e x) (e' x')) + -> @wf (Arrow A B) (Abs e) (Abs e'). End with_var. - Definition Wf {t} (E : @Expr t) := forall var1 var2, wf nil (E var1) (E var2). + Definition Wf {t} (E : @Expr t) := forall var1 var2, wf (E var1) (E var2). Axiom Wf_admitted : forall {t} (E:Expr t), @Wf t E. End language. @@ -65,7 +64,7 @@ End language. Ltac admit_Wf := apply Wf_admitted. Global Arguments wff {_ _ _ _} G {t} _ _. -Global Arguments wf {_ _ _ _} G {t} _ _. +Global Arguments wf {_ _ _ _ t} _ _. Global Arguments Wf {_ _ t} _. Hint Constructors wf wff : wf. diff --git a/src/Reflection/WfInversion.v b/src/Reflection/WfInversion.v index cdaa7ffb5..111c8a4a4 100644 --- a/src/Reflection/WfInversion.v +++ b/src/Reflection/WfInversion.v @@ -132,6 +132,40 @@ Section language. end; t. Qed. + + Definition wf_code {t} (e1 : @expr var1 t) : forall (e2 : @expr var2 t), Prop + := match e1 in Syntax.expr _ _ t return expr t -> Prop with + | Abs src dst f1 + => fun e2 + => let f2 := invert_Abs e2 in + forall (x : interp_flat_type var1 src) (x' : interp_flat_type var2 src), + wff (flatten_binding_list x x') (f1 x) (f2 x') + end. + + Definition wf_encode {t e1 e2} (v : @wf var1 var2 t e1 e2) : @wf_code t e1 e2. + Proof. + destruct v; t. + Defined. + + Definition wf_decode {t e1 e2} (v : @wf_code t e1 e2) : @wf var1 var2 t e1 e2. + Proof. + destruct e1; t. + Defined. + + Definition wf_endecode {t e1 e2} v : @wf_decode t e1 e2 (@wf_encode t e1 e2 v) = v. + Proof. + destruct v; reflexivity. + Qed. + + Definition wf_deencode {t e1 e2} v : @wf_encode t e1 e2 (@wf_decode t e1 e2 v) = v. + Proof. + destruct e1 as [src dst f1]. + revert dependent f1. + refine match e2 with + | Abs _ _ f2 => _ + end. + reflexivity. + Qed. End with_var. End language. @@ -143,12 +177,11 @@ Ltac is_expr_constructor arg := | LetIn _ _ => idtac | Pair _ _ => idtac | Abs _ => idtac - | Return _ => idtac end. -Ltac inversion_wff_step_gen guard_tac := +Ltac inversion_wf_step_gen guard_tac := let postprocess H := - (cbv [wff_code] in H; + (cbv [wff_code wf_code] in H; simpl in H; try match type of H with | True => clear H @@ -158,11 +191,14 @@ Ltac inversion_wff_step_gen guard_tac := | [ H : wff _ ?x ?y |- _ ] => guard_tac x y; apply wff_encode in H; postprocess H + | [ H : wf ?x ?y |- _ ] + => guard_tac x y; + apply wf_encode in H; postprocess H end. -Ltac inversion_wff_step_constr := - inversion_wff_step_gen ltac:(fun x y => is_expr_constructor x; is_expr_constructor y). -Ltac inversion_wff_step_var := - inversion_wff_step_gen ltac:(fun x y => first [ is_var x; is_var y; fail 1 | idtac ]). -Ltac inversion_wff_step := first [ inversion_wff_step_constr | inversion_wff_step_var ]. -Ltac inversion_wff_constr := repeat inversion_wff_step_constr. -Ltac inversion_wff := repeat inversion_wff_step. +Ltac inversion_wf_step_constr := + inversion_wf_step_gen ltac:(fun x y => is_expr_constructor x; is_expr_constructor y). +Ltac inversion_wf_step_var := + inversion_wf_step_gen ltac:(fun x y => first [ is_var x; is_var y; fail 1 | idtac ]). +Ltac inversion_wf_step := first [ inversion_wf_step_constr | inversion_wf_step_var ]. +Ltac inversion_wf_constr := repeat inversion_wf_step_constr. +Ltac inversion_wf := repeat inversion_wf_step. diff --git a/src/Reflection/WfProofs.v b/src/Reflection/WfProofs.v index 937d53533..2b9197858 100644 --- a/src/Reflection/WfProofs.v +++ b/src/Reflection/WfProofs.v @@ -117,23 +117,9 @@ Section language. | _ => progress simpl in * | _ => progress destruct_head' or | _ => solve [ eauto with nocore ] - | _ => progress inversion_wff + | _ => progress inversion_wf end. Qed. - - Lemma wf_SmartAbs {A B} G e1 e2 - (Hwf : forall G' x y, wff (G' ++ G) x y -> wf (G' ++ G) (e1 x) (e2 y)) - : @wf _ op var1 var2 G _ (@SmartAbs _ _ _ A B e1) (@SmartAbs _ _ _ A B e2). - Proof. - revert dependent G; revert dependent B; induction A; intros. - { simpl; constructor; intros. - apply (Hwf (_::nil)%list); constructor; left; reflexivity. } - { apply (Hwf nil); constructor. } - { simpl in *. - do 2 match goal with H : _ |- _ => apply H; intros end. - rewrite List.app_assoc; apply Hwf; rewrite <- List.app_assoc. - eauto with wf. } - Qed. End with_var. Definition duplicate_type {var1 var2} diff --git a/src/Reflection/WfReflective.v b/src/Reflection/WfReflective.v index da731d511..aafe67c84 100644 --- a/src/Reflection/WfReflective.v +++ b/src/Reflection/WfReflective.v @@ -50,6 +50,7 @@ Require Import Coq.Arith.Arith Coq.Logic.Eqdep_dec. Require Import Crypto.Reflection.Syntax. Require Import Crypto.Reflection.Wf. +Require Import Crypto.Reflection.EtaWf. Require Import Crypto.Reflection.WfReflectiveGen. Require Import Crypto.Util.Notations Crypto.Util.Tactics Crypto.Util.Option Crypto.Util.Sigma Crypto.Util.Prod Crypto.Util.Decidable Crypto.Util.ListUtil. Require Export Crypto.Util.PartiallyReifiedProp. (* export for the [bool >-> reified_Prop] coercion *) @@ -136,8 +137,10 @@ Section language. | [ H : List.In _ (duplicate_type _) |- _ ] => eapply duplicate_type_in in H; [ | eassumption.. ] | [ H : context[match _ with _ => _ end] |- _ ] => revert H; progress break_innermost_match | [ |- wff _ _ _ ] => constructor - | [ |- wf _ _ _ ] => constructor + | [ |- wf _ _ ] => constructor | _ => progress unfold and_reified_Prop in * + | [ |- wff (flatten_binding_list ?x ?y) _ _ ] + => rewrite <- (List.app_nil_r (flatten_binding_list x y)) end. Local Ltac t := repeat t_step. Fixpoint reflect_wff (G : list (sigT (fun t => var1 t * var2 t)%type)) @@ -177,33 +180,29 @@ Section language. { t. } { t. } Qed. - Fixpoint reflect_wf (G : list (sigT (fun t => var1 t * var2 t)%type)) + Definition reflect_wf {t1 t2 : type} (e1 : @expr (fun t => nat * var1 t)%type t1) (e2 : @expr (fun t => nat * var2 t)%type t2) - : let reflective_obligation := reflect_wfT (duplicate_type G) e1 e2 in + : let reflective_obligation := reflect_wfT nil e1 e2 in match type_eq_semidec_transparent t1 t2 with | Some p => to_prop reflective_obligation - -> @wf base_type_code op var1 var2 G t2 (eq_rect _ expr (unnatize_expr (List.length G) e1) _ p) (unnatize_expr (List.length G) e2) + -> @wf base_type_code op var1 var2 t2 (eq_rect _ expr (unnatize_expr 0 e1) _ p) (unnatize_expr 0 e2) | None => True end. Proof. - destruct e1 as [ t1 e1 | tx tR f ], - e2 as [ t2 e2 | tx' tR' f' ]; simpl; try solve [ exact I ]; - [ clear reflect_wf; - pose proof (@reflect_wff G t1 t2 e1 e2) - | pose proof (fun x x' - => match preflatten_binding_list2 (Tbase tx) (Tbase tx') as v return match v with Some _ => _ | None => True end with - | Some G0 - => reflect_wf - (G0 x x' ++ G)%list _ _ - (f (snd (natize_interp_flat_type (length (duplicate_type G)) x))) - (f' (snd (natize_interp_flat_type (length (duplicate_type G)) x'))) - | None => I - end); - clear reflect_wf ]. - { t. } - { t. } + destruct e1 as [ tx tR f ], + e2 as [ tx' tR' f' ]; simpl; try solve [ exact I ]. + pose proof (fun x x' + => match preflatten_binding_list2 tx tx' as v return match v with Some _ => _ | None => True end with + | Some G0 + => reflect_wff + (G0 x x' ++ nil)%list + (f (snd (natize_interp_flat_type 0 x))) + (f' (snd (natize_interp_flat_type 0 x'))) + | None => I + end). + t. Qed. End language. @@ -224,7 +223,7 @@ Section Wf. -> Wf (fun var => unnatize_expr 0 (e (fun t => (nat * var t)%type))). Proof. intros H var1 var2; specialize (H var1 var2). - pose proof (@reflect_wf base_type_code base_type_eq_semidec_transparent base_type_eq_semidec_is_dec op op_beq op_beq_bl var1 var2 nil t t (e _) (e _)) as H'. + pose proof (@reflect_wf base_type_code base_type_eq_semidec_transparent base_type_eq_semidec_is_dec op op_beq op_beq_bl var1 var2 t t (e _) (e _)) as H'. rewrite type_eq_semidec_transparent_refl in H' by assumption; simpl in *. edestruct @reflect_wfT; simpl in *; tauto. Qed. @@ -243,7 +242,13 @@ Section Wf. Qed. End Wf. - +(** Using [ExprEta'] ensures that reduction and conversion don't block + on destructuring the variable arguments. *) +Ltac preapply_eta'_Wf := + lazymatch goal with + | [ |- @Wf ?base_type_code ?op ?t ?e ] + => apply (proj1 (@Wf_ExprEta'_iff base_type_code op t e)) + end. Ltac generalize_reflect_Wf base_type_eq_semidec_is_dec op_beq_bl := lazymatch goal with | [ |- @Wf ?base_type_code ?op ?t ?e ] @@ -268,5 +273,6 @@ Ltac fin_reflect_Wf := (** The tactic [reflect_Wf] is the main tactic of this file, used to prove [Syntax.Wf] goals *) Ltac reflect_Wf base_type_eq_semidec_is_dec op_beq_bl := + preapply_eta'_Wf; generalize_reflect_Wf base_type_eq_semidec_is_dec op_beq_bl; use_reflect_Wf; fin_reflect_Wf. diff --git a/src/Reflection/WfReflectiveGen.v b/src/Reflection/WfReflectiveGen.v index d4c0b45d0..0e745f059 100644 --- a/src/Reflection/WfReflectiveGen.v +++ b/src/Reflection/WfReflectiveGen.v @@ -109,18 +109,13 @@ Section language. end | Prod _ _, _ => None end. - Fixpoint type_eq_semidec_transparent (t1 t2 : type) : option (t1 = t2) + Definition type_eq_semidec_transparent (t1 t2 : type) : option (t1 = t2) := match t1, t2 return option (t1 = t2) with - | Syntax.Tflat t1, Syntax.Tflat t2 - => option_map (@f_equal _ _ (@Tflat _) _ _) - (flat_type_eq_semidec_transparent t1 t2) - | Syntax.Tflat _, _ => None | Arrow A B, Arrow A' B' - => match base_type_eq_semidec_transparent A A', type_eq_semidec_transparent B B' with - | Some p, Some q => Some (f_equal2 (@Arrow base_type_code) p q) - | _, _ => None - end - | Arrow _ _, _ => None + => match flat_type_eq_semidec_transparent A A', flat_type_eq_semidec_transparent B B' with + | Some p, Some q => Some (f_equal2 (@Arrow base_type_code) p q) + | _, _ => None + end end. Lemma base_type_eq_semidec_transparent_refl t : base_type_eq_semidec_transparent t t = Some eq_refl. Proof. @@ -139,11 +134,10 @@ Section language. Lemma type_eq_semidec_transparent_refl t : type_eq_semidec_transparent t t = Some eq_refl. Proof. clear -base_type_eq_semidec_is_dec. - induction t as [t | A B IHt]; simpl. - { rewrite flat_type_eq_semidec_transparent_refl; reflexivity. } - { rewrite base_type_eq_semidec_transparent_refl; rewrite_hyp !*; reflexivity. } + destruct t; simpl; rewrite !flat_type_eq_semidec_transparent_refl; reflexivity. Qed. + Definition op_beq' t1 tR t1' tR' (x : op t1 tR) (y : op t1' tR') : reified_Prop := match flat_type_eq_semidec_transparent t1 t1', flat_type_eq_semidec_transparent tR tR' with | Some p, Some q @@ -236,7 +230,7 @@ Section language. let base := fst ret in let b := snd ret in (base, (a, b)) - | Unit => fun _ => (base, tt) + | Unit => fun v => (base, v) | Tbase t => fun v => (S base, (base, v)) end v. Arguments natize_interp_flat_type {var t} _ _. @@ -263,18 +257,20 @@ Section language. | TT => TT | Var _ x => Var (snd x) | Op _ _ op args => Op op (@unnatize_exprf _ _ base args) - | LetIn _ ex _ eC => LetIn (@unnatize_exprf _ _ base ex) - (fun x => let v := natize_interp_flat_type base x in - @unnatize_exprf _ _ (fst v) (eC (snd v))) - | Pair _ x _ y => Pair (@unnatize_exprf _ _ base x) (@unnatize_exprf _ _ base y) + | LetIn _ ex _ eC + => LetIn (@unnatize_exprf _ _ base ex) + (fun x => let v := natize_interp_flat_type base x in + @unnatize_exprf _ _ (fst v) (eC (snd v))) + | Pair _ x _ y + => Pair (@unnatize_exprf _ _ base x) (@unnatize_exprf _ _ base y) end. - Fixpoint unnatize_expr {var t} (base : nat) - (e : @Syntax.expr base_type_code op (fun t => nat * var t)%type t) + Definition unnatize_expr {var t} (base : nat) + (e : @Syntax.expr base_type_code op (fun t => nat * var t)%type t) : @Syntax.expr base_type_code op var t := match e in @Syntax.expr _ _ _ t return Syntax.expr _ _ t with - | Return _ x => unnatize_exprf base x - | Abs tx tR f => Abs (fun x : var tx => let v := natize_interp_flat_type (t:=Tbase tx) base x in - @unnatize_expr _ _ (fst v) (f (snd v))) + | Abs tx tR f => Abs (fun x : interp_flat_type var tx => + let v := natize_interp_flat_type (t:=tx) base x in + @unnatize_exprf _ _ (fst v) (f (snd v))) end. Fixpoint reflect_wffT (G : list (sigT (fun t => var1 (fst t) * var2 (snd t))%type)) @@ -312,31 +308,26 @@ Section language. | Pair _ _ _ _, _ => rFalse end%reified_prop. - Fixpoint reflect_wfT (G : list (sigT (fun t => var1 (fst t) * var2 (snd t))%type)) + Definition reflect_wfT (G : list (sigT (fun t => var1 (fst t) * var2 (snd t))%type)) {t1 t2 : type} (e1 : @expr (fun t => nat * var1 t)%type t1) (e2 : @expr (fun t => nat * var2 t)%type t2) - {struct e1} : reified_Prop := match e1, e2 with - | Return _ x, Return _ y - => reflect_wffT G x y - | Return _ _, _ => rFalse | Abs tx tR f, Abs tx' tR' f' - => match @flatten_binding_list2 (Tbase tx) (Tbase tx'), type_eq_semidec_transparent tR tR' with + => match @flatten_binding_list2 tx tx', flat_type_eq_semidec_transparent tR tR' with | Some G0, Some _ - => ∀ (x : interp_flat_type var1 (Tbase tx)) (x' : interp_flat_type var2 (Tbase tx')), - @reflect_wfT (G0 x x' ++ G)%list _ _ - (f (snd (natize_interp_flat_type (List.length G) x))) - (f' (snd (natize_interp_flat_type (List.length G) x'))) + => ∀ (x : interp_flat_type var1 tx) (x' : interp_flat_type var2 tx'), + @reflect_wffT (G0 x x' ++ G)%list _ _ + (f (snd (natize_interp_flat_type (List.length G) x))) + (f' (snd (natize_interp_flat_type (List.length G) x'))) | _, _ => rFalse end - | Abs _ _ _, _ => rFalse end%reified_prop. End language. -Global Arguments reflect_wffT {_} _ {op} _ {var1 var2} G {t1 t2} _ _. -Global Arguments reflect_wfT {_} _ {op} _ {var1 var2} G {t1 t2} _ _. +Global Arguments reflect_wffT {_} _ {op} op_beq {var1 var2} G {t1 t2} _ _. +Global Arguments reflect_wfT {_} _ {op} op_beq {var1 var2} G {t1 t2} _ _. Global Arguments unnatize_exprf {_ _ _ _} _ _. Global Arguments unnatize_expr {_ _ _ _} _ _. Global Arguments natize_interp_flat_type {_ _ t} _ _. diff --git a/src/Reflection/Z/BoundsInterpretations.v b/src/Reflection/Z/BoundsInterpretations.v index 8da4ef39f..722ee40ec 100644 --- a/src/Reflection/Z/BoundsInterpretations.v +++ b/src/Reflection/Z/BoundsInterpretations.v @@ -123,17 +123,18 @@ Module Import Bounds. Definition interp_op {src dst} (f : op src dst) : interp_flat_type interp_base_type src -> interp_flat_type interp_base_type dst := match f in op src dst return interp_flat_type interp_base_type src -> interp_flat_type interp_base_type dst with - | OpConst v => fun _ => SmartBuildBounds None v v - | Add => fun xy => add (bit_width_of_base_type TZ) (fst xy) (snd xy) - | Sub => fun xy => sub (bit_width_of_base_type TZ) (fst xy) (snd xy) - | Mul => fun xy => mul (bit_width_of_base_type TZ) (fst xy) (snd xy) - | Shl => fun xy => shl (bit_width_of_base_type TZ) (fst xy) (snd xy) - | Shr => fun xy => shr (bit_width_of_base_type TZ) (fst xy) (snd xy) - | Land => fun xy => land (bit_width_of_base_type TZ) (fst xy) (snd xy) - | Lor => fun xy => lor (bit_width_of_base_type TZ) (fst xy) (snd xy) - | Neg int_width => fun x => neg (bit_width_of_base_type TZ) int_width x - | Cmovne => fun xyzw => let '(x, y, z, w) := eta4 xyzw in cmovne (bit_width_of_base_type TZ) x y z w - | Cmovle => fun xyzw => let '(x, y, z, w) := eta4 xyzw in cmovle (bit_width_of_base_type TZ) x y z w + | OpConst TZ v => fun _ => SmartBuildBounds None v v + | Add T => fun xy => add (bit_width_of_base_type T) (fst xy) (snd xy) + | Sub T => fun xy => sub (bit_width_of_base_type T) (fst xy) (snd xy) + | Mul T => fun xy => mul (bit_width_of_base_type T) (fst xy) (snd xy) + | Shl T => fun xy => shl (bit_width_of_base_type T) (fst xy) (snd xy) + | Shr T => fun xy => shr (bit_width_of_base_type T) (fst xy) (snd xy) + | Land T => fun xy => land (bit_width_of_base_type T) (fst xy) (snd xy) + | Lor T => fun xy => lor (bit_width_of_base_type T) (fst xy) (snd xy) + | Neg T int_width => fun x => neg (bit_width_of_base_type T) int_width x + | Cmovne T => fun xyzw => let '(x, y, z, w) := eta4 xyzw in cmovne (bit_width_of_base_type T) x y z w + | Cmovle T => fun xyzw => let '(x, y, z, w) := eta4 xyzw in cmovle (bit_width_of_base_type T) x y z w + | Cast _ T => fun x => SmartRebuildBounds (bit_width_of_base_type T) x end%bounds. Ltac inversion_bounds := @@ -163,12 +164,10 @@ Module Import Bounds. | Some b' => bounds_to_base_type' b' end. - (* Definition ComputeBounds {t} (e : Expr base_type op t) (input_bounds : interp_flat_type interp_base_type (domain t)) : interp_flat_type interp_base_type (codomain t) := Interp (@interp_op) e input_bounds. - *) Definition bound_is_goodb : forall t, interp_base_type t -> bool := fun t bs diff --git a/src/Reflection/Z/CNotations.v b/src/Reflection/Z/CNotations.v index 764094c99..bfd173094 100644 --- a/src/Reflection/Z/CNotations.v +++ b/src/Reflection/Z/CNotations.v @@ -44,18 +44,18 @@ Notation "'(uint32_t)' x" := (Op (Cast _ (TWord 5)) (Var x)). Notation "'(uint64_t)' x" := (Op (Cast _ (TWord 6)) (Var x)). Notation "'(uint128_t)' x" := (Op (Cast _ (TWord 7)) (Var x)). *) -Notation "x + y" := (Op (Add) (Pair x y)). -Notation "x + y" := (Op (Add) (Pair (Var x) y)). -Notation "x + y" := (Op (Add) (Pair x (Var y))). -Notation "x + y" := (Op (Add) (Pair (Var x) (Var y))). -Notation "x - y" := (Op (Sub) (Pair x y)). -Notation "x - y" := (Op (Sub) (Pair (Var x) y)). -Notation "x - y" := (Op (Sub) (Pair x (Var y))). -Notation "x - y" := (Op (Sub) (Pair (Var x) (Var y))). -Notation "x * y" := (Op (Mul) (Pair x y)). -Notation "x * y" := (Op (Mul) (Pair (Var x) y)). -Notation "x * y" := (Op (Mul) (Pair x (Var y))). -Notation "x * y" := (Op (Mul) (Pair (Var x) (Var y))). +Notation "x + y" := (Op (Add _) (Pair x y)). +Notation "x + y" := (Op (Add _) (Pair (Var x) y)). +Notation "x + y" := (Op (Add _) (Pair x (Var y))). +Notation "x + y" := (Op (Add _) (Pair (Var x) (Var y))). +Notation "x - y" := (Op (Sub _) (Pair x y)). +Notation "x - y" := (Op (Sub _) (Pair (Var x) y)). +Notation "x - y" := (Op (Sub _) (Pair x (Var y))). +Notation "x - y" := (Op (Sub _) (Pair (Var x) (Var y))). +Notation "x * y" := (Op (Mul _) (Pair x y)). +Notation "x * y" := (Op (Mul _) (Pair (Var x) y)). +Notation "x * y" := (Op (Mul _) (Pair x (Var y))). +Notation "x * y" := (Op (Mul _) (Pair (Var x) (Var y))). (* python: << for opn, op in (('*', 'Mul'), ('+', 'Add'), ('&', 'Land')): @@ -119,20 +119,18 @@ Notation "x + y" := (Op (Add (TWord 7)) (Pair x (Op (Cast _ (TWord 7)) (Var y))) Notation "x + y" := (Op (Add (TWord 7)) (Pair (Var x) (Op (Cast _ (TWord 7)) y))). Notation "x + y" := (Op (Add (TWord 7)) (Pair (Var x) (Op (Cast _ (TWord 7)) (Var y)))). *) -Notation "x >> y" := (Op (Shr) (Pair x y)). -Notation "x >> y" := (Op (Shr) (Pair (Var x) y)). -Notation "x >> y" := (Op (Shr) (Pair x (Var y))). -Notation "x >> y" := (Op (Shr) (Pair (Var x) (Var y))). -(* +Notation "x >> y" := (Op (Shr _) (Pair x y)). +Notation "x >> y" := (Op (Shr _) (Pair (Var x) y)). +Notation "x >> y" := (Op (Shr _) (Pair x (Var y))). +Notation "x >> y" := (Op (Shr _) (Pair (Var x) (Var y))). Notation "x >> y" := (Op (Shr _) (Pair x (Op (Cast _ _) y))). Notation "x >> y" := (Op (Shr _) (Pair (Var x) (Op (Cast _ _) y))). Notation "x >> y" := (Op (Shr _) (Pair x (Op (Cast _ _) (Var y)))). Notation "x >> y" := (Op (Shr _) (Pair (Var x) (Op (Cast _ _) (Var y)))). -*) -Notation "x & y" := (Op (Land) (Pair x y)). -Notation "x & y" := (Op (Land) (Pair (Var x) y)). -Notation "x & y" := (Op (Land) (Pair x (Var y))). -Notation "x & y" := (Op (Land) (Pair (Var x) (Var y))). +Notation "x & y" := (Op (Land _) (Pair x y)). +Notation "x & y" := (Op (Land _) (Pair (Var x) y)). +Notation "x & y" := (Op (Land _) (Pair x (Var y))). +Notation "x & y" := (Op (Land _) (Pair (Var x) (Var y))). (* Notation "x & y" := (Op (Land (TWord 5)) (Pair (Op (Cast _ (TWord 5)) x) y)). Notation "x & y" := (Op (Land (TWord 5)) (Pair (Op (Cast _ (TWord 5)) x) (Var y))). diff --git a/src/Reflection/Z/Interpretations128/Relations.v b/src/Reflection/Z/Interpretations128/Relations.v index 7f6f67fa2..8ea7de125 100644 --- a/src/Reflection/Z/Interpretations128/Relations.v +++ b/src/Reflection/Z/Interpretations128/Relations.v @@ -340,11 +340,12 @@ Local Ltac unfold_related_const := Lemma related_wordW_op : related_op related_wordW (@BoundedWordW.interp_op) (@WordW.interp_op). Proof. - (let op := fresh in intros ?? op; destruct op; simpl); + (let op := fresh in intros ?? op; destruct op; simpl); destruct_head' base_type; try first [ apply related_wordW_t_map1 | apply related_wordW_t_map2 | apply related_wordW_t_map4 - | unfold_related_const; break_innermost_match; reflexivity ]. + | unfold_related_const; break_innermost_match; reflexivity + | exact (fun _ _ x => x) ]. Qed. Lemma related_bounds_t_map1 opW opB pf @@ -411,7 +412,7 @@ Local Ltac related_const_op_t := Lemma related_bounds_op : related_op related_bounds (@BoundedWordW.interp_op) (@ZBounds.interp_op). Proof. - let op := fresh in intros ?? op; destruct op; simpl. + let op := fresh in intros ?? op; destruct op; simpl; destruct_head' base_type. { related_const_op_t. } { apply related_bounds_t_map2; intros; destruct_head' option; reflexivity. } { apply related_bounds_t_map2; intros; destruct_head' option; reflexivity. } @@ -423,6 +424,7 @@ Proof. { apply related_bounds_t_map1; intros; destruct_head' option; unfold ZBounds.neg; break_match; reflexivity. } { apply related_bounds_t_map4; intros; destruct_head' option; reflexivity. } { apply related_bounds_t_map4; intros; destruct_head' option; reflexivity. } + { exact (fun _ _ x => x). } Qed. Local Ltac WordW.Rewrites.wordW_util_arith ::= @@ -541,7 +543,7 @@ Local Arguments ZBounds.neg _ !_ / . Lemma related_Z_op : related_op related_Z (@BoundedWordW.interp_op) (@Z.interp_op). Proof. - let op := fresh in intros ?? op; destruct op; simpl. + let op := fresh in intros ?? op; destruct op; simpl; destruct_head' base_type. { related_const_op_t. } { apply related_Z_t_map2; related_Z_op_fin_t. } { apply related_Z_t_map2; related_Z_op_fin_t. } @@ -553,6 +555,7 @@ Proof. { apply related_Z_t_map1; related_Z_op_fin_t. } { apply related_Z_t_map4; related_Z_op_fin_t. } { apply related_Z_t_map4; related_Z_op_fin_t. } + { exact (fun _ _ x => x). } Qed. Create HintDb interp_related discriminated. diff --git a/src/Reflection/Z/Interpretations128/RelationsCombinations.v b/src/Reflection/Z/Interpretations128/RelationsCombinations.v index 68fca675e..6e7eb2865 100644 --- a/src/Reflection/Z/Interpretations128/RelationsCombinations.v +++ b/src/Reflection/Z/Interpretations128/RelationsCombinations.v @@ -1,9 +1,9 @@ Require Import Coq.ZArith.ZArith. +Require Import Coq.Classes.RelationClasses. Require Import Crypto.Reflection.Z.Syntax. Require Import Crypto.Reflection.Syntax. Require Import Crypto.Reflection.SmartMap. Require Import Crypto.Reflection.Relations. -Require Import Crypto.Reflection.Application. Require Import Crypto.Reflection.Z.InterpretationsGen. Require Import Crypto.Reflection.Z.Interpretations128. Require Import Crypto.Reflection.Z.Interpretations128.Relations. @@ -14,36 +14,6 @@ Require Import Crypto.Util.Prod. Require Import Crypto.Util.Tactics. Module Relations. - Section lift. - Context {interp_base_type1 interp_base_type2 : base_type -> Type} - (R : forall t, interp_base_type1 t -> interp_base_type2 t -> Prop). - - Definition interp_type_rel_pointwise2_uncurried - {t : type base_type} - := match t return interp_type interp_base_type1 t -> interp_type interp_base_type2 t -> _ with - | Tflat T => fun f g => interp_flat_type_rel_pointwise (t:=T) R f g - | Arrow A B - => fun f g - => forall x y, interp_flat_type_rel_pointwise R x y - -> interp_flat_type_rel_pointwise R (ApplyInterpedAll f x) (ApplyInterpedAll g y) - end. - - Lemma uncurry_interp_type_rel_pointwise2 - {t f g} - : interp_type_rel_pointwise2 (t:=t) R f g - <-> interp_type_rel_pointwise2_uncurried (t:=t) f g. - Proof. - unfold interp_type_rel_pointwise2_uncurried. - induction t as [|A B IHt]; [ reflexivity | ]. - { simpl; unfold Morphisms.respectful_hetero in *; destruct B. - { reflexivity. } - { setoid_rewrite IHt; clear IHt. - split; intro H; intros. - { destruct_head_hnf' prod; simpl in *; intuition. } - { eapply (H (_, _) (_, _)); simpl in *; intuition. } } } - Qed. - End lift. - Section proj. Context {interp_base_type1 interp_base_type2} (proj : forall t : base_type, interp_base_type1 t -> interp_base_type2 t). @@ -51,43 +21,27 @@ Module Relations. Let R {t : flat_type base_type} f g := SmartVarfMap (t:=t) proj f = g. - Definition interp_type_rel_pointwise2_uncurried_proj + Definition interp_type_rel_pointwise_uncurried_proj {t : type base_type} : interp_type interp_base_type1 t -> interp_type interp_base_type2 t -> Prop - := match t return interp_type interp_base_type1 t -> interp_type interp_base_type2 t -> Prop with - | Tflat T => @R _ - | Arrow A B - => fun f g - => forall x : interp_flat_type interp_base_type1 (all_binders_for (Arrow A B)), - let y := SmartVarfMap proj x in - let fx := ApplyInterpedAll f x in - let gy := ApplyInterpedAll g y in - @R _ fx gy - end. - - Lemma uncurry_interp_type_rel_pointwise2_proj + := fun f g + => forall x : interp_flat_type interp_base_type1 (domain t), + let y := SmartVarfMap proj x in + let fx := f x in + let gy := g y in + @R _ fx gy. + + Lemma uncurry_interp_type_rel_pointwise_proj {t : type base_type} - {f : interp_type interp_base_type1 t} + {f} {g} - : interp_type_rel_pointwise2 (t:=t) (fun t => @R _) f g - -> interp_type_rel_pointwise2_uncurried_proj (t:=t) f g. + : (forall x y, @R (domain t) x y -> @R (codomain t) (f x) (g y)) + -> interp_type_rel_pointwise_uncurried_proj (t:=t) f g. Proof. - unfold interp_type_rel_pointwise2_uncurried_proj. - induction t as [t|A B IHt]; simpl; unfold Morphisms.respectful_hetero in *. - { induction t as [t| |A IHA B IHB]; simpl; destruct_head_hnf' unit; - [ solve [ trivial | reflexivity ] | reflexivity | ]. - intros [HA HB]. - specialize (IHA _ _ HA); specialize (IHB _ _ HB). - unfold R in *. - repeat first [ progress destruct_head_hnf' prod - | progress simpl in * - | progress subst - | reflexivity ]. } - { destruct B; intros H ?; apply IHt, H; clear IHt; - repeat first [ reflexivity - | progress simpl in * - | progress unfold R, LiftOption.of' in * - | progress break_match ]. } + unfold interp_type_rel_pointwise_uncurried_proj. + destruct t as [A B]; simpl in *. + subst R; simpl in *. + eauto. Qed. End proj. @@ -102,49 +56,28 @@ Module Relations. | None => True end. - Definition interp_type_rel_pointwise2_uncurried_proj_option + Definition interp_type_rel_pointwise_uncurried_proj_option {t : type base_type} : interp_type (LiftOption.interp_base_type' interp_base_type1) t -> interp_type interp_base_type2 t -> Prop - := match t return interp_type (LiftOption.interp_base_type' interp_base_type1) t -> interp_type interp_base_type2 t -> Prop with - | Tflat T => @R _ - | Arrow A B - => fun f g - => forall x : interp_flat_type (fun _ => interp_base_type1) (all_binders_for (Arrow A B)), - let y := SmartVarfMap proj_option x in - let fx := ApplyInterpedAll f (LiftOption.to' (Some x)) in - let gy := ApplyInterpedAll g y in - @R _ fx gy - end. - - Lemma uncurry_interp_type_rel_pointwise2_proj_option + := fun f g + => forall x : interp_flat_type (fun _ => interp_base_type1) (domain t), + let y := SmartVarfMap proj_option x in + let fx := f (LiftOption.to' (Some x)) in + let gy := g y in + @R _ fx gy. + + Lemma uncurry_interp_type_rel_pointwise_proj_option {t : type base_type} - {f : interp_type (LiftOption.interp_base_type' interp_base_type1) t} + {f} {g} - : interp_type_rel_pointwise2 (t:=t) (fun t => @R _) f g - -> interp_type_rel_pointwise2_uncurried_proj_option (t:=t) f g. + : (forall x y, @R (domain t) x y -> @R (codomain t) (f x) (g y)) + -> interp_type_rel_pointwise_uncurried_proj_option (t:=t) f g. Proof. - unfold interp_type_rel_pointwise2_uncurried_proj_option. - induction t as [t|A B IHt]; simpl; unfold Morphisms.respectful_hetero in *. - { induction t as [t| |A IHA B IHB]; simpl; destruct_head_hnf' unit; - [ solve [ trivial | reflexivity ] | reflexivity | ]. - intros [HA HB]. - specialize (IHA _ _ HA); specialize (IHB _ _ HB). - unfold R in *. - repeat first [ progress destruct_head_hnf' prod - | progress simpl in * - | progress unfold LiftOption.of' in * - | progress break_match - | progress break_match_hyps - | progress inversion_prod - | progress inversion_option - | reflexivity - | progress intuition subst ]. } - { destruct B; intros H ?; apply IHt, H; clear IHt. - { repeat first [ progress simpl in * - | progress unfold R, LiftOption.of' in * - | progress break_match - | reflexivity ]. } - { simpl in *; break_match; reflexivity. } } + unfold interp_type_rel_pointwise_uncurried_proj_option. + destruct t as [A B]; simpl in *. + subst R; simpl in *. + intros H x; apply H; simpl. + rewrite LiftOption.of'_to'; reflexivity. Qed. End proj_option. @@ -162,52 +95,58 @@ Module Relations. | None, _ => False end. - Definition interp_type_rel_pointwise2_uncurried_proj_option2 + Definition interp_type_rel_pointwise_uncurried_proj_option2 {t : type base_type} : interp_type (LiftOption.interp_base_type' interp_base_type1) t -> interp_type (LiftOption.interp_base_type' interp_base_type2) t -> Prop - := match t return interp_type (LiftOption.interp_base_type' interp_base_type1) t -> interp_type (LiftOption.interp_base_type' interp_base_type2) t -> Prop with - | Tflat T => @R _ - | Arrow A B - => fun f g - => forall x : interp_flat_type (fun _ => interp_base_type1) (all_binders_for (Arrow A B)), - let y := SmartVarfMap (fun _ => proj) x in - let fx := ApplyInterpedAll f (LiftOption.to' (Some x)) in - let gy := ApplyInterpedAll g (LiftOption.to' (Some y)) in - @R _ fx gy - end. - - Lemma uncurry_interp_type_rel_pointwise2_proj_option2 + := fun f g + => forall x : interp_flat_type (fun _ => interp_base_type1) (domain t), + let y := SmartVarfMap (fun _ => proj) x in + let fx := f (LiftOption.to' (Some x)) in + let gy := g (LiftOption.to' (Some y)) in + @R _ fx gy. + + Lemma uncurry_interp_type_rel_pointwise_proj_option2 {t : type base_type} - {f : interp_type (LiftOption.interp_base_type' interp_base_type1) t} - {g : interp_type (LiftOption.interp_base_type' interp_base_type2) t} - : interp_type_rel_pointwise2 (t:=t) (fun t => @R _) f g - -> interp_type_rel_pointwise2_uncurried_proj_option2 (t:=t) f g. + {f} + {g} + : (forall x y, @R (domain t) x y -> @R (codomain t) (f x) (g y)) + -> interp_type_rel_pointwise_uncurried_proj_option2 (t:=t) f g. Proof. - unfold interp_type_rel_pointwise2_uncurried_proj_option2. - induction t as [t|A B IHt]; simpl; unfold Morphisms.respectful_hetero in *. - { induction t as [t| |A IHA B IHB]; simpl; destruct_head_hnf' unit; - [ solve [ trivial | reflexivity ] | reflexivity | ]. - intros [HA HB]. - specialize (IHA _ _ HA); specialize (IHB _ _ HB). - unfold R in *. - repeat first [ progress destruct_head_hnf' prod - | progress simpl in * - | progress unfold LiftOption.of' in * - | progress break_match - | progress break_match_hyps - | progress inversion_prod - | progress inversion_option - | reflexivity - | progress intuition subst ]. } - { destruct B; intros H ?; apply IHt, H; clear IHt. - { repeat first [ progress simpl in * - | progress unfold R, LiftOption.of' in * - | progress break_match - | reflexivity ]. } - { simpl in *; break_match; reflexivity. } } + unfold interp_type_rel_pointwise_uncurried_proj_option2. + destruct t as [A B]; simpl in *. + subst R; simpl in *. + intros H x; apply H; simpl. + rewrite !LiftOption.of'_to'; reflexivity. Qed. End proj_option2. + Local Ltac t proj012 := + repeat match goal with + | _ => progress cbv beta in * + | _ => progress break_match; try tauto; [] + | _ => progress subst + | [ H : _ |- _ ] + => first [ rewrite !LiftOption.lift_relation_flat_type_pointwise in H + by (eassumption || rewrite LiftOption.of'_to'; reflexivity) + | rewrite !LiftOption.lift_relation2_flat_type_pointwise in H + by (eassumption || rewrite LiftOption.of'_to'; reflexivity) + | rewrite !@lift_interp_flat_type_rel_pointwise_f_eq_id2 in H + | rewrite !@lift_interp_flat_type_rel_pointwise_f_eq in H ] + | _ => progress unfold proj_eq_rel in * + | _ => progress specialize_by reflexivity + | _ => rewrite SmartVarfMap_compose + | _ => setoid_rewrite proj012 + | [ |- context G[fun x y => ?f x y] ] + => let G' := context G[f] in change G' + | [ |- context G[fun (_ : ?T) x => ?f x] ] + => let G' := context G[fun _ : T => f] in change G' + | [ H : context G[fun (_ : ?T) x => ?f x] |- _ ] + => let G' := context G[fun _ : T => f] in change G' in H + | _ => rewrite_hyp <- !*; [] + | _ => reflexivity + | _ => rewrite interp_flat_type_rel_pointwise_SmartVarfMap + end. + Section proj_from_option2. Context {interp_base_type0 : Type} {interp_base_type1 interp_base_type2 : base_type -> Type} (proj01 : forall t, interp_base_type0 -> interp_base_type1 t) @@ -217,64 +156,41 @@ Module Relations. Let R {t : flat_type base_type} f g := proj_eq_rel (SmartVarfMap proj (t:=t)) f g. - Definition interp_type_rel_pointwise2_uncurried_proj_from_option2 + Definition interp_type_rel_pointwise_uncurried_proj_from_option2 {t : type base_type} : interp_type (LiftOption.interp_base_type' interp_base_type0) t -> interp_type interp_base_type1 t -> interp_type interp_base_type2 t -> Prop - := match t return interp_type _ t -> interp_type _ t -> interp_type _ t -> Prop with - | Tflat T => fun f0 f g => match LiftOption.of' f0 with - | Some _ => True - | None => False - end -> @R _ f g - | Arrow A B - => fun f0 f g - => forall x : interp_flat_type (fun _ => interp_base_type0) (all_binders_for (Arrow A B)), - let x' := SmartVarfMap proj01 x in - let y' := SmartVarfMap proj x' in - let fx := ApplyInterpedAll f x' in - let gy := ApplyInterpedAll g y' in - let f0x := LiftOption.of' (ApplyInterpedAll f0 (LiftOption.to' (Some x))) in - match f0x with - | Some _ => True - | None => False - end - -> @R _ fx gy - end. - - Lemma uncurry_interp_type_rel_pointwise2_proj_from_option2 + := fun f0 f g + => forall x : interp_flat_type (fun _ => interp_base_type0) (domain t), + let x' := SmartVarfMap proj01 x in + let y' := SmartVarfMap proj x' in + let fx := f x' in + let gy := g y' in + let f0x := LiftOption.of' (f0 (LiftOption.to' (Some x))) in + match f0x with + | Some _ => True + | None => False + end + -> @R _ fx gy. + + Lemma uncurry_interp_type_rel_pointwise_proj_from_option2 {t : type base_type} {f0} {f : interp_type interp_base_type1 t} {g : interp_type interp_base_type2 t} (proj012 : forall t x, proj t (proj01 t x) = proj02 t x) - : interp_type_rel_pointwise2 (t:=t) (LiftOption.lift_relation (fun t => proj_eq_rel (proj01 t))) f0 f - -> interp_type_rel_pointwise2 (t:=t) (LiftOption.lift_relation (fun t => proj_eq_rel (proj02 t))) f0 g - -> interp_type_rel_pointwise2_uncurried_proj_from_option2 (t:=t) f0 f g. + : interp_type_rel_pointwise (t:=t) (LiftOption.lift_relation (fun t => proj_eq_rel (proj01 t))) f0 f + -> interp_type_rel_pointwise (t:=t) (LiftOption.lift_relation (fun t => proj_eq_rel (proj02 t))) f0 g + -> interp_type_rel_pointwise_uncurried_proj_from_option2 (t:=t) f0 f g. Proof. - unfold interp_type_rel_pointwise2_uncurried_proj_from_option2. - induction t as [t|A B IHt]; simpl; unfold Morphisms.respectful_hetero in *. - { induction t as [t| |A IHA B IHB]; simpl; destruct_head_hnf' unit; try reflexivity. - { cbv [LiftOption.lift_relation proj_eq_rel R]. - break_match; try tauto; intros; subst. - apply proj012. } - { intros [HA HB] [HA' HB'] Hrel. - specialize (IHA _ _ _ HA HA'); specialize (IHB _ _ _ HB HB'). - unfold R, proj_eq_rel in *. - repeat first [ progress destruct_head_hnf' prod - | progress simpl in * - | progress unfold LiftOption.of' in * - | progress break_match - | progress break_match_hyps - | progress inversion_prod - | progress inversion_option - | reflexivity - | progress intuition subst ]. } } - { destruct B; intros H0 H1 ?; apply IHt; clear IHt; first [ apply H0 | apply H1 ]; - repeat first [ progress simpl in * - | progress unfold R, LiftOption.of', proj_eq_rel, LiftOption.lift_relation in * - | break_match; rewrite <- ?proj012; reflexivity ]. } + unfold interp_type_rel_pointwise_uncurried_proj_from_option2, Morphisms.respectful_hetero. + intros H0 H1 x. + specialize (H0 (LiftOption.to' (Some x)) (SmartVarfMap proj01 x)). + specialize (H1 (LiftOption.to' (Some x)) (SmartVarfMap proj02 x)). + subst R. + t proj012. Qed. End proj_from_option2. - Global Arguments uncurry_interp_type_rel_pointwise2_proj_from_option2 {_ _ _ _ _} proj {t f0 f g} _ _ _. + Global Arguments uncurry_interp_type_rel_pointwise_proj_from_option2 {_ _ _ _ _} proj {t f0 f g} _ _ _. Section proj1_from_option2. Context {interp_base_type0 interp_base_type1 : Type} {interp_base_type2 : base_type -> Type} @@ -282,70 +198,43 @@ Module Relations. (proj02 : forall t, interp_base_type0 -> interp_base_type2 t) (R : forall t, interp_base_type1 -> interp_base_type2 t -> Prop). - Definition interp_type_rel_pointwise2_uncurried_proj1_from_option2 + Definition interp_type_rel_pointwise_uncurried_proj1_from_option2 {t : type base_type} : interp_type (LiftOption.interp_base_type' interp_base_type0) t -> interp_type (LiftOption.interp_base_type' interp_base_type1) t -> interp_type interp_base_type2 t -> Prop - := match t return interp_type _ t -> interp_type _ t -> interp_type _ t -> Prop with - | Tflat T => fun f0 f g => match LiftOption.of' f0 with - | Some _ => True - | None => False - end -> match LiftOption.of' f with - | Some f' => interp_flat_type_rel_pointwise (@R) f' g - | None => True - end - | Arrow A B - => fun f0 f g - => forall x : interp_flat_type (fun _ => interp_base_type0) (all_binders_for (Arrow A B)), - let x' := SmartVarfMap (fun _ => proj01) x in - let y' := SmartVarfMap proj02 x in - let fx := LiftOption.of' (ApplyInterpedAll f (LiftOption.to' (Some x'))) in - let gy := ApplyInterpedAll g y' in - let f0x := LiftOption.of' (ApplyInterpedAll f0 (LiftOption.to' (Some x))) in - match f0x with - | Some _ => True - | None => False - end - -> match fx with - | Some fx' => interp_flat_type_rel_pointwise (@R) fx' gy - | None => True - end - end. - - Lemma uncurry_interp_type_rel_pointwise2_proj1_from_option2 + := fun f0 f g + => forall x : interp_flat_type (fun _ => interp_base_type0) (domain t), + let x' := SmartVarfMap (fun _ => proj01) x in + let y' := SmartVarfMap proj02 x in + let fx := LiftOption.of' (f (LiftOption.to' (Some x'))) in + let gy := g y' in + let f0x := LiftOption.of' (f0 (LiftOption.to' (Some x))) in + match f0x with + | Some _ => True + | None => False + end + -> match fx with + | Some fx' => interp_flat_type_rel_pointwise (@R) fx' gy + | None => True + end. + + Lemma uncurry_interp_type_rel_pointwise_proj1_from_option2 {t : type base_type} {f0} {f : interp_type (LiftOption.interp_base_type' interp_base_type1) t} {g : interp_type interp_base_type2 t} - (proj012R : forall t x, @R _ (proj01 x) (proj02 t x)) - : interp_type_rel_pointwise2 (t:=t) (LiftOption.lift_relation2 (proj_eq_rel proj01)) f0 f - -> interp_type_rel_pointwise2 (t:=t) (LiftOption.lift_relation (fun t => proj_eq_rel (proj02 t))) f0 g - -> interp_type_rel_pointwise2_uncurried_proj1_from_option2 (t:=t) f0 f g. + (proj012R : forall t, Reflexive (fun x y => @R _ (proj01 x) (proj02 t y))) + : interp_type_rel_pointwise (t:=t) (LiftOption.lift_relation2 (proj_eq_rel proj01)) f0 f + -> interp_type_rel_pointwise (t:=t) (LiftOption.lift_relation (fun t => proj_eq_rel (proj02 t))) f0 g + -> interp_type_rel_pointwise_uncurried_proj1_from_option2 (t:=t) f0 f g. Proof. - unfold interp_type_rel_pointwise2_uncurried_proj1_from_option2. - induction t as [t|A B IHt]; simpl; unfold Morphisms.respectful_hetero in *. - { induction t as [t| |A IHA B IHB]; simpl; destruct_head_hnf' unit; try reflexivity. - { cbv [LiftOption.lift_relation proj_eq_rel LiftOption.lift_relation2]. - break_match; try tauto; intros; subst. - apply proj012R. } - { intros [HA HB] [HA' HB'] Hrel. - specialize (IHA _ _ _ HA HA'); specialize (IHB _ _ _ HB HB'). - unfold proj_eq_rel in *. - repeat first [ progress destruct_head_hnf' prod - | progress simpl in * - | progress unfold LiftOption.of' in * - | progress break_match - | progress break_match_hyps - | progress inversion_prod - | progress inversion_option - | reflexivity - | progress intuition subst ]. } } - { destruct B; intros H0 H1 ?; apply IHt; clear IHt; first [ apply H0 | apply H1 ]; - repeat first [ progress simpl in * - | progress unfold R, LiftOption.of', proj_eq_rel, LiftOption.lift_relation in * - | break_match; reflexivity ]. } + unfold interp_type_rel_pointwise_uncurried_proj1_from_option2, Morphisms.respectful_hetero. + intros H0 H1 x. + specialize (H0 (LiftOption.to' (Some x)) (LiftOption.to' (Some (SmartVarfMap (fun _ => proj01) x)))). + specialize (H1 (LiftOption.to' (Some x)) (SmartVarfMap proj02 x)). + t proj012. Qed. End proj1_from_option2. - Global Arguments uncurry_interp_type_rel_pointwise2_proj1_from_option2 {_ _ _ _ _} R {t f0 f g} _ _ _. + Global Arguments uncurry_interp_type_rel_pointwise_proj1_from_option2 {_ _ _ _ _} R {t f0 f g} _ _ _. Section combine_related. Lemma related_flat_transitivity {interp_base_type1 interp_base_type2 interp_base_type3} diff --git a/src/Reflection/Z/Interpretations64/Relations.v b/src/Reflection/Z/Interpretations64/Relations.v index 02934c46a..3491c9be5 100644 --- a/src/Reflection/Z/Interpretations64/Relations.v +++ b/src/Reflection/Z/Interpretations64/Relations.v @@ -341,10 +341,12 @@ Local Ltac unfold_related_const := Lemma related_wordW_op : related_op related_wordW (@BoundedWordW.interp_op) (@WordW.interp_op). Proof. (let op := fresh in intros ?? op; destruct op; simpl); + destruct_head' base_type; try first [ apply related_wordW_t_map1 | apply related_wordW_t_map2 | apply related_wordW_t_map4 - | unfold_related_const; break_innermost_match; reflexivity ]. + | unfold_related_const; break_innermost_match; reflexivity + | exact (fun _ _ x => x) ]. Qed. Lemma related_bounds_t_map1 opW opB pf @@ -411,7 +413,7 @@ Local Ltac related_const_op_t := Lemma related_bounds_op : related_op related_bounds (@BoundedWordW.interp_op) (@ZBounds.interp_op). Proof. - let op := fresh in intros ?? op; destruct op; simpl. + let op := fresh in intros ?? op; destruct op; simpl; destruct_head' base_type. { related_const_op_t. } { apply related_bounds_t_map2; intros; destruct_head' option; reflexivity. } { apply related_bounds_t_map2; intros; destruct_head' option; reflexivity. } @@ -423,6 +425,7 @@ Proof. { apply related_bounds_t_map1; intros; destruct_head' option; unfold ZBounds.neg; break_match; reflexivity. } { apply related_bounds_t_map4; intros; destruct_head' option; reflexivity. } { apply related_bounds_t_map4; intros; destruct_head' option; reflexivity. } + { exact (fun _ _ x => x). } Qed. Local Ltac WordW.Rewrites.wordW_util_arith ::= @@ -541,7 +544,7 @@ Local Arguments ZBounds.neg _ !_ / . Lemma related_Z_op : related_op related_Z (@BoundedWordW.interp_op) (@Z.interp_op). Proof. - let op := fresh in intros ?? op; destruct op; simpl. + let op := fresh in intros ?? op; destruct op; simpl; destruct_head' base_type. { related_const_op_t. } { apply related_Z_t_map2; related_Z_op_fin_t. } { apply related_Z_t_map2; related_Z_op_fin_t. } @@ -553,6 +556,7 @@ Proof. { apply related_Z_t_map1; related_Z_op_fin_t. } { apply related_Z_t_map4; related_Z_op_fin_t. } { apply related_Z_t_map4; related_Z_op_fin_t. } + { exact (fun _ _ x => x). } Qed. Create HintDb interp_related discriminated. diff --git a/src/Reflection/Z/Interpretations64/RelationsCombinations.v b/src/Reflection/Z/Interpretations64/RelationsCombinations.v index 3a95bcc51..2e05b18de 100644 --- a/src/Reflection/Z/Interpretations64/RelationsCombinations.v +++ b/src/Reflection/Z/Interpretations64/RelationsCombinations.v @@ -1,9 +1,9 @@ Require Import Coq.ZArith.ZArith. +Require Import Coq.Classes.RelationClasses. Require Import Crypto.Reflection.Z.Syntax. Require Import Crypto.Reflection.Syntax. Require Import Crypto.Reflection.SmartMap. Require Import Crypto.Reflection.Relations. -Require Import Crypto.Reflection.Application. Require Import Crypto.Reflection.Z.InterpretationsGen. Require Import Crypto.Reflection.Z.Interpretations64. Require Import Crypto.Reflection.Z.Interpretations64.Relations. @@ -14,36 +14,6 @@ Require Import Crypto.Util.Prod. Require Import Crypto.Util.Tactics. Module Relations. - Section lift. - Context {interp_base_type1 interp_base_type2 : base_type -> Type} - (R : forall t, interp_base_type1 t -> interp_base_type2 t -> Prop). - - Definition interp_type_rel_pointwise2_uncurried - {t : type base_type} - := match t return interp_type interp_base_type1 t -> interp_type interp_base_type2 t -> _ with - | Tflat T => fun f g => interp_flat_type_rel_pointwise (t:=T) R f g - | Arrow A B - => fun f g - => forall x y, interp_flat_type_rel_pointwise R x y - -> interp_flat_type_rel_pointwise R (ApplyInterpedAll f x) (ApplyInterpedAll g y) - end. - - Lemma uncurry_interp_type_rel_pointwise2 - {t f g} - : interp_type_rel_pointwise2 (t:=t) R f g - <-> interp_type_rel_pointwise2_uncurried (t:=t) f g. - Proof. - unfold interp_type_rel_pointwise2_uncurried. - induction t as [|A B IHt]; [ reflexivity | ]. - { simpl; unfold Morphisms.respectful_hetero in *; destruct B. - { reflexivity. } - { setoid_rewrite IHt; clear IHt. - split; intro H; intros. - { destruct_head_hnf' prod; simpl in *; intuition. } - { eapply (H (_, _) (_, _)); simpl in *; intuition. } } } - Qed. - End lift. - Section proj. Context {interp_base_type1 interp_base_type2} (proj : forall t : base_type, interp_base_type1 t -> interp_base_type2 t). @@ -51,43 +21,27 @@ Module Relations. Let R {t : flat_type base_type} f g := SmartVarfMap (t:=t) proj f = g. - Definition interp_type_rel_pointwise2_uncurried_proj + Definition interp_type_rel_pointwise_uncurried_proj {t : type base_type} : interp_type interp_base_type1 t -> interp_type interp_base_type2 t -> Prop - := match t return interp_type interp_base_type1 t -> interp_type interp_base_type2 t -> Prop with - | Tflat T => @R _ - | Arrow A B - => fun f g - => forall x : interp_flat_type interp_base_type1 (all_binders_for (Arrow A B)), - let y := SmartVarfMap proj x in - let fx := ApplyInterpedAll f x in - let gy := ApplyInterpedAll g y in - @R _ fx gy - end. - - Lemma uncurry_interp_type_rel_pointwise2_proj + := fun f g + => forall x : interp_flat_type interp_base_type1 (domain t), + let y := SmartVarfMap proj x in + let fx := f x in + let gy := g y in + @R _ fx gy. + + Lemma uncurry_interp_type_rel_pointwise_proj {t : type base_type} - {f : interp_type interp_base_type1 t} + {f} {g} - : interp_type_rel_pointwise2 (t:=t) (fun t => @R _) f g - -> interp_type_rel_pointwise2_uncurried_proj (t:=t) f g. + : (forall x y, @R (domain t) x y -> @R (codomain t) (f x) (g y)) + -> interp_type_rel_pointwise_uncurried_proj (t:=t) f g. Proof. - unfold interp_type_rel_pointwise2_uncurried_proj. - induction t as [t|A B IHt]; simpl; unfold Morphisms.respectful_hetero in *. - { induction t as [t| |A IHA B IHB]; simpl; destruct_head_hnf' unit; - [ solve [ trivial | reflexivity ] | reflexivity | ]. - intros [HA HB]. - specialize (IHA _ _ HA); specialize (IHB _ _ HB). - unfold R in *. - repeat first [ progress destruct_head_hnf' prod - | progress simpl in * - | progress subst - | reflexivity ]. } - { destruct B; intros H ?; apply IHt, H; clear IHt; - repeat first [ reflexivity - | progress simpl in * - | progress unfold R, LiftOption.of' in * - | progress break_match ]. } + unfold interp_type_rel_pointwise_uncurried_proj. + destruct t as [A B]; simpl in *. + subst R; simpl in *. + eauto. Qed. End proj. @@ -102,49 +56,28 @@ Module Relations. | None => True end. - Definition interp_type_rel_pointwise2_uncurried_proj_option + Definition interp_type_rel_pointwise_uncurried_proj_option {t : type base_type} : interp_type (LiftOption.interp_base_type' interp_base_type1) t -> interp_type interp_base_type2 t -> Prop - := match t return interp_type (LiftOption.interp_base_type' interp_base_type1) t -> interp_type interp_base_type2 t -> Prop with - | Tflat T => @R _ - | Arrow A B - => fun f g - => forall x : interp_flat_type (fun _ => interp_base_type1) (all_binders_for (Arrow A B)), - let y := SmartVarfMap proj_option x in - let fx := ApplyInterpedAll f (LiftOption.to' (Some x)) in - let gy := ApplyInterpedAll g y in - @R _ fx gy - end. - - Lemma uncurry_interp_type_rel_pointwise2_proj_option + := fun f g + => forall x : interp_flat_type (fun _ => interp_base_type1) (domain t), + let y := SmartVarfMap proj_option x in + let fx := f (LiftOption.to' (Some x)) in + let gy := g y in + @R _ fx gy. + + Lemma uncurry_interp_type_rel_pointwise_proj_option {t : type base_type} - {f : interp_type (LiftOption.interp_base_type' interp_base_type1) t} + {f} {g} - : interp_type_rel_pointwise2 (t:=t) (fun t => @R _) f g - -> interp_type_rel_pointwise2_uncurried_proj_option (t:=t) f g. + : (forall x y, @R (domain t) x y -> @R (codomain t) (f x) (g y)) + -> interp_type_rel_pointwise_uncurried_proj_option (t:=t) f g. Proof. - unfold interp_type_rel_pointwise2_uncurried_proj_option. - induction t as [t|A B IHt]; simpl; unfold Morphisms.respectful_hetero in *. - { induction t as [t| |A IHA B IHB]; simpl; destruct_head_hnf' unit; - [ solve [ trivial | reflexivity ] | reflexivity | ]. - intros [HA HB]. - specialize (IHA _ _ HA); specialize (IHB _ _ HB). - unfold R in *. - repeat first [ progress destruct_head_hnf' prod - | progress simpl in * - | progress unfold LiftOption.of' in * - | progress break_match - | progress break_match_hyps - | progress inversion_prod - | progress inversion_option - | reflexivity - | progress intuition subst ]. } - { destruct B; intros H ?; apply IHt, H; clear IHt. - { repeat first [ progress simpl in * - | progress unfold R, LiftOption.of' in * - | progress break_match - | reflexivity ]. } - { simpl in *; break_match; reflexivity. } } + unfold interp_type_rel_pointwise_uncurried_proj_option. + destruct t as [A B]; simpl in *. + subst R; simpl in *. + intros H x; apply H; simpl. + rewrite LiftOption.of'_to'; reflexivity. Qed. End proj_option. @@ -162,52 +95,58 @@ Module Relations. | None, _ => False end. - Definition interp_type_rel_pointwise2_uncurried_proj_option2 + Definition interp_type_rel_pointwise_uncurried_proj_option2 {t : type base_type} : interp_type (LiftOption.interp_base_type' interp_base_type1) t -> interp_type (LiftOption.interp_base_type' interp_base_type2) t -> Prop - := match t return interp_type (LiftOption.interp_base_type' interp_base_type1) t -> interp_type (LiftOption.interp_base_type' interp_base_type2) t -> Prop with - | Tflat T => @R _ - | Arrow A B - => fun f g - => forall x : interp_flat_type (fun _ => interp_base_type1) (all_binders_for (Arrow A B)), - let y := SmartVarfMap (fun _ => proj) x in - let fx := ApplyInterpedAll f (LiftOption.to' (Some x)) in - let gy := ApplyInterpedAll g (LiftOption.to' (Some y)) in - @R _ fx gy - end. - - Lemma uncurry_interp_type_rel_pointwise2_proj_option2 + := fun f g + => forall x : interp_flat_type (fun _ => interp_base_type1) (domain t), + let y := SmartVarfMap (fun _ => proj) x in + let fx := f (LiftOption.to' (Some x)) in + let gy := g (LiftOption.to' (Some y)) in + @R _ fx gy. + + Lemma uncurry_interp_type_rel_pointwise_proj_option2 {t : type base_type} - {f : interp_type (LiftOption.interp_base_type' interp_base_type1) t} - {g : interp_type (LiftOption.interp_base_type' interp_base_type2) t} - : interp_type_rel_pointwise2 (t:=t) (fun t => @R _) f g - -> interp_type_rel_pointwise2_uncurried_proj_option2 (t:=t) f g. + {f} + {g} + : (forall x y, @R (domain t) x y -> @R (codomain t) (f x) (g y)) + -> interp_type_rel_pointwise_uncurried_proj_option2 (t:=t) f g. Proof. - unfold interp_type_rel_pointwise2_uncurried_proj_option2. - induction t as [t|A B IHt]; simpl; unfold Morphisms.respectful_hetero in *. - { induction t as [t| |A IHA B IHB]; simpl; destruct_head_hnf' unit; - [ solve [ trivial | reflexivity ] | reflexivity | ]. - intros [HA HB]. - specialize (IHA _ _ HA); specialize (IHB _ _ HB). - unfold R in *. - repeat first [ progress destruct_head_hnf' prod - | progress simpl in * - | progress unfold LiftOption.of' in * - | progress break_match - | progress break_match_hyps - | progress inversion_prod - | progress inversion_option - | reflexivity - | progress intuition subst ]. } - { destruct B; intros H ?; apply IHt, H; clear IHt. - { repeat first [ progress simpl in * - | progress unfold R, LiftOption.of' in * - | progress break_match - | reflexivity ]. } - { simpl in *; break_match; reflexivity. } } + unfold interp_type_rel_pointwise_uncurried_proj_option2. + destruct t as [A B]; simpl in *. + subst R; simpl in *. + intros H x; apply H; simpl. + rewrite !LiftOption.of'_to'; reflexivity. Qed. End proj_option2. + Local Ltac t proj012 := + repeat match goal with + | _ => progress cbv beta in * + | _ => progress break_match; try tauto; [] + | _ => progress subst + | [ H : _ |- _ ] + => first [ rewrite !LiftOption.lift_relation_flat_type_pointwise in H + by (eassumption || rewrite LiftOption.of'_to'; reflexivity) + | rewrite !LiftOption.lift_relation2_flat_type_pointwise in H + by (eassumption || rewrite LiftOption.of'_to'; reflexivity) + | rewrite !@lift_interp_flat_type_rel_pointwise_f_eq_id2 in H + | rewrite !@lift_interp_flat_type_rel_pointwise_f_eq in H ] + | _ => progress unfold proj_eq_rel in * + | _ => progress specialize_by reflexivity + | _ => rewrite SmartVarfMap_compose + | _ => setoid_rewrite proj012 + | [ |- context G[fun x y => ?f x y] ] + => let G' := context G[f] in change G' + | [ |- context G[fun (_ : ?T) x => ?f x] ] + => let G' := context G[fun _ : T => f] in change G' + | [ H : context G[fun (_ : ?T) x => ?f x] |- _ ] + => let G' := context G[fun _ : T => f] in change G' in H + | _ => rewrite_hyp <- !*; [] + | _ => reflexivity + | _ => rewrite interp_flat_type_rel_pointwise_SmartVarfMap + end. + Section proj_from_option2. Context {interp_base_type0 : Type} {interp_base_type1 interp_base_type2 : base_type -> Type} (proj01 : forall t, interp_base_type0 -> interp_base_type1 t) @@ -217,64 +156,41 @@ Module Relations. Let R {t : flat_type base_type} f g := proj_eq_rel (SmartVarfMap proj (t:=t)) f g. - Definition interp_type_rel_pointwise2_uncurried_proj_from_option2 + Definition interp_type_rel_pointwise_uncurried_proj_from_option2 {t : type base_type} : interp_type (LiftOption.interp_base_type' interp_base_type0) t -> interp_type interp_base_type1 t -> interp_type interp_base_type2 t -> Prop - := match t return interp_type _ t -> interp_type _ t -> interp_type _ t -> Prop with - | Tflat T => fun f0 f g => match LiftOption.of' f0 with - | Some _ => True - | None => False - end -> @R _ f g - | Arrow A B - => fun f0 f g - => forall x : interp_flat_type (fun _ => interp_base_type0) (all_binders_for (Arrow A B)), - let x' := SmartVarfMap proj01 x in - let y' := SmartVarfMap proj x' in - let fx := ApplyInterpedAll f x' in - let gy := ApplyInterpedAll g y' in - let f0x := LiftOption.of' (ApplyInterpedAll f0 (LiftOption.to' (Some x))) in - match f0x with - | Some _ => True - | None => False - end - -> @R _ fx gy - end. - - Lemma uncurry_interp_type_rel_pointwise2_proj_from_option2 + := fun f0 f g + => forall x : interp_flat_type (fun _ => interp_base_type0) (domain t), + let x' := SmartVarfMap proj01 x in + let y' := SmartVarfMap proj x' in + let fx := f x' in + let gy := g y' in + let f0x := LiftOption.of' (f0 (LiftOption.to' (Some x))) in + match f0x with + | Some _ => True + | None => False + end + -> @R _ fx gy. + + Lemma uncurry_interp_type_rel_pointwise_proj_from_option2 {t : type base_type} {f0} {f : interp_type interp_base_type1 t} {g : interp_type interp_base_type2 t} (proj012 : forall t x, proj t (proj01 t x) = proj02 t x) - : interp_type_rel_pointwise2 (t:=t) (LiftOption.lift_relation (fun t => proj_eq_rel (proj01 t))) f0 f - -> interp_type_rel_pointwise2 (t:=t) (LiftOption.lift_relation (fun t => proj_eq_rel (proj02 t))) f0 g - -> interp_type_rel_pointwise2_uncurried_proj_from_option2 (t:=t) f0 f g. + : interp_type_rel_pointwise (t:=t) (LiftOption.lift_relation (fun t => proj_eq_rel (proj01 t))) f0 f + -> interp_type_rel_pointwise (t:=t) (LiftOption.lift_relation (fun t => proj_eq_rel (proj02 t))) f0 g + -> interp_type_rel_pointwise_uncurried_proj_from_option2 (t:=t) f0 f g. Proof. - unfold interp_type_rel_pointwise2_uncurried_proj_from_option2. - induction t as [t|A B IHt]; simpl; unfold Morphisms.respectful_hetero in *. - { induction t as [t| |A IHA B IHB]; simpl; destruct_head_hnf' unit; try reflexivity. - { cbv [LiftOption.lift_relation proj_eq_rel R]. - break_match; try tauto; intros; subst. - apply proj012. } - { intros [HA HB] [HA' HB'] Hrel. - specialize (IHA _ _ _ HA HA'); specialize (IHB _ _ _ HB HB'). - unfold R, proj_eq_rel in *. - repeat first [ progress destruct_head_hnf' prod - | progress simpl in * - | progress unfold LiftOption.of' in * - | progress break_match - | progress break_match_hyps - | progress inversion_prod - | progress inversion_option - | reflexivity - | progress intuition subst ]. } } - { destruct B; intros H0 H1 ?; apply IHt; clear IHt; first [ apply H0 | apply H1 ]; - repeat first [ progress simpl in * - | progress unfold R, LiftOption.of', proj_eq_rel, LiftOption.lift_relation in * - | break_match; rewrite <- ?proj012; reflexivity ]. } + unfold interp_type_rel_pointwise_uncurried_proj_from_option2, Morphisms.respectful_hetero. + intros H0 H1 x. + specialize (H0 (LiftOption.to' (Some x)) (SmartVarfMap proj01 x)). + specialize (H1 (LiftOption.to' (Some x)) (SmartVarfMap proj02 x)). + subst R. + t proj012. Qed. End proj_from_option2. - Global Arguments uncurry_interp_type_rel_pointwise2_proj_from_option2 {_ _ _ _ _} proj {t f0 f g} _ _ _. + Global Arguments uncurry_interp_type_rel_pointwise_proj_from_option2 {_ _ _ _ _} proj {t f0 f g} _ _ _. Section proj1_from_option2. Context {interp_base_type0 interp_base_type1 : Type} {interp_base_type2 : base_type -> Type} @@ -282,70 +198,43 @@ Module Relations. (proj02 : forall t, interp_base_type0 -> interp_base_type2 t) (R : forall t, interp_base_type1 -> interp_base_type2 t -> Prop). - Definition interp_type_rel_pointwise2_uncurried_proj1_from_option2 + Definition interp_type_rel_pointwise_uncurried_proj1_from_option2 {t : type base_type} : interp_type (LiftOption.interp_base_type' interp_base_type0) t -> interp_type (LiftOption.interp_base_type' interp_base_type1) t -> interp_type interp_base_type2 t -> Prop - := match t return interp_type _ t -> interp_type _ t -> interp_type _ t -> Prop with - | Tflat T => fun f0 f g => match LiftOption.of' f0 with - | Some _ => True - | None => False - end -> match LiftOption.of' f with - | Some f' => interp_flat_type_rel_pointwise (@R) f' g - | None => True - end - | Arrow A B - => fun f0 f g - => forall x : interp_flat_type (fun _ => interp_base_type0) (all_binders_for (Arrow A B)), - let x' := SmartVarfMap (fun _ => proj01) x in - let y' := SmartVarfMap proj02 x in - let fx := LiftOption.of' (ApplyInterpedAll f (LiftOption.to' (Some x'))) in - let gy := ApplyInterpedAll g y' in - let f0x := LiftOption.of' (ApplyInterpedAll f0 (LiftOption.to' (Some x))) in - match f0x with - | Some _ => True - | None => False - end - -> match fx with - | Some fx' => interp_flat_type_rel_pointwise (@R) fx' gy - | None => True - end - end. - - Lemma uncurry_interp_type_rel_pointwise2_proj1_from_option2 + := fun f0 f g + => forall x : interp_flat_type (fun _ => interp_base_type0) (domain t), + let x' := SmartVarfMap (fun _ => proj01) x in + let y' := SmartVarfMap proj02 x in + let fx := LiftOption.of' (f (LiftOption.to' (Some x'))) in + let gy := g y' in + let f0x := LiftOption.of' (f0 (LiftOption.to' (Some x))) in + match f0x with + | Some _ => True + | None => False + end + -> match fx with + | Some fx' => interp_flat_type_rel_pointwise (@R) fx' gy + | None => True + end. + + Lemma uncurry_interp_type_rel_pointwise_proj1_from_option2 {t : type base_type} {f0} {f : interp_type (LiftOption.interp_base_type' interp_base_type1) t} {g : interp_type interp_base_type2 t} - (proj012R : forall t x, @R _ (proj01 x) (proj02 t x)) - : interp_type_rel_pointwise2 (t:=t) (LiftOption.lift_relation2 (proj_eq_rel proj01)) f0 f - -> interp_type_rel_pointwise2 (t:=t) (LiftOption.lift_relation (fun t => proj_eq_rel (proj02 t))) f0 g - -> interp_type_rel_pointwise2_uncurried_proj1_from_option2 (t:=t) f0 f g. + (proj012R : forall t, Reflexive (fun x y => @R _ (proj01 x) (proj02 t y))) + : interp_type_rel_pointwise (t:=t) (LiftOption.lift_relation2 (proj_eq_rel proj01)) f0 f + -> interp_type_rel_pointwise (t:=t) (LiftOption.lift_relation (fun t => proj_eq_rel (proj02 t))) f0 g + -> interp_type_rel_pointwise_uncurried_proj1_from_option2 (t:=t) f0 f g. Proof. - unfold interp_type_rel_pointwise2_uncurried_proj1_from_option2. - induction t as [t|A B IHt]; simpl; unfold Morphisms.respectful_hetero in *. - { induction t as [t| |A IHA B IHB]; simpl; destruct_head_hnf' unit; try reflexivity. - { cbv [LiftOption.lift_relation proj_eq_rel LiftOption.lift_relation2]. - break_match; try tauto; intros; subst. - apply proj012R. } - { intros [HA HB] [HA' HB'] Hrel. - specialize (IHA _ _ _ HA HA'); specialize (IHB _ _ _ HB HB'). - unfold proj_eq_rel in *. - repeat first [ progress destruct_head_hnf' prod - | progress simpl in * - | progress unfold LiftOption.of' in * - | progress break_match - | progress break_match_hyps - | progress inversion_prod - | progress inversion_option - | reflexivity - | progress intuition subst ]. } } - { destruct B; intros H0 H1 ?; apply IHt; clear IHt; first [ apply H0 | apply H1 ]; - repeat first [ progress simpl in * - | progress unfold R, LiftOption.of', proj_eq_rel, LiftOption.lift_relation in * - | break_match; reflexivity ]. } + unfold interp_type_rel_pointwise_uncurried_proj1_from_option2, Morphisms.respectful_hetero. + intros H0 H1 x. + specialize (H0 (LiftOption.to' (Some x)) (LiftOption.to' (Some (SmartVarfMap (fun _ => proj01) x)))). + specialize (H1 (LiftOption.to' (Some x)) (SmartVarfMap proj02 x)). + t proj012. Qed. End proj1_from_option2. - Global Arguments uncurry_interp_type_rel_pointwise2_proj1_from_option2 {_ _ _ _ _} R {t f0 f g} _ _ _. + Global Arguments uncurry_interp_type_rel_pointwise_proj1_from_option2 {_ _ _ _ _} R {t f0 f g} _ _ _. Section combine_related. Lemma related_flat_transitivity {interp_base_type1 interp_base_type2 interp_base_type3} diff --git a/src/Reflection/Z/InterpretationsGen.v b/src/Reflection/Z/InterpretationsGen.v index f11837e60..6fa2ff8da 100644 --- a/src/Reflection/Z/InterpretationsGen.v +++ b/src/Reflection/Z/InterpretationsGen.v @@ -3,7 +3,7 @@ Require Import Coq.ZArith.ZArith. Require Import Crypto.Reflection.Z.Syntax. Require Import Crypto.Reflection.Syntax. Require Import Crypto.Reflection.SmartMap. -Require Import Crypto.Reflection.Application. +Require Import Crypto.Reflection.Relations. Require Import Crypto.ModularArithmetic.ModularBaseSystemListZOperations. Require Import Crypto.Util.Equality. Require Import Crypto.Util.ZUtil. @@ -53,9 +53,7 @@ Module InterpretationsGen (Bit : BitSize). := option (interp_flat_type (fun _ => T) t). Definition interp_base_type' (t : base_type) - := match t with - | TZ => option T - end. + := option T. Definition of' {t} : Syntax.interp_flat_type interp_base_type' t -> interp_flat_type t := @smart_interp_flat_map @@ -69,41 +67,115 @@ Module InterpretationsGen (Bit : BitSize). end) t. + Lemma of'_pair {A B} x + : @of' (A * B) x = match of' (fst x), of' (snd x) with + | Some x', Some y' => Some (x', y') + | _, _ => None + end. + Proof. reflexivity. Qed. + Fixpoint to' {t} : interp_flat_type t -> Syntax.interp_flat_type interp_base_type' t := match t return interp_flat_type t -> Syntax.interp_flat_type interp_base_type' t with - | Tbase TZ => fun x => x + | Tbase _ => fun x => x | Unit => fun _ => tt | Prod A B => fun x => (@to' A (option_map (@fst _ _) x), @to' B (option_map (@snd _ _) x)) end. - Definition lift_relation {interp_base_type2} - (R : forall t, T -> interp_base_type2 t -> Prop) - : forall t, interp_base_type' t -> interp_base_type2 t -> Prop - := fun t x y => match of' (t:=Tbase t) x with - | Some x' => R t x' y - | None => True - end. - - Definition Some {t} (x : T) : interp_base_type' t - := match t with - | TZ => Some x - end. + Lemma of'_to' {t} v : of' (@to' t (Some v)) = Some v. + Proof. + induction t; + repeat first [ progress simpl + | progress destruct_head_hnf prod + | progress destruct_head_hnf unit + | progress destruct_head base_type + | rewrite of'_pair + | rewrite_hyp !* + | reflexivity ]. + Qed. + + Section lift_relation. + Context {interp_base_type2 : base_type -> Type} + (R : forall t, T -> interp_base_type2 t -> Prop). + Definition lift_relation + : forall t, interp_base_type' t -> interp_base_type2 t -> Prop + := fun t x y => match of' (t:=Tbase t) x with + | Some x' => R t x' y + | None => True + end. + + Lemma lift_relation_flat_type_pointwise t x y x' + (Hx : of' x = Some x') + : interp_flat_type_rel_pointwise lift_relation x y + <-> interp_flat_type_rel_pointwise (t:=t) R x' y. + Proof. + induction t; simpl; try tauto. + { unfold lift_relation; rewrite Hx; reflexivity. } + { rewrite of'_pair in Hx. + destruct (of' (fst x)) eqn:?, (of' (snd x)) eqn:?; try congruence. + inversion_option; subst. + destruct_head_hnf prod; split_iff; intuition eauto. } + Qed. + + Lemma lift_relation_type_pointwise t f g f' + (Hx : forall x x', of' x = Some x' -> of' (f x) = Some (f' x')) + : interp_type_rel_pointwise lift_relation f g + -> interp_type_rel_pointwise (t:=t) R f' g. + Proof. + destruct t; simpl; unfold Morphisms.respectful_hetero. + intros H x y p; specialize (H (to' (Some x)) y). + eapply lift_relation_flat_type_pointwise in p; [ | apply of'_to'.. ]. + specialize (H p). + eapply lift_relation_flat_type_pointwise in H; [ exact H | ]. + erewrite Hx; [ reflexivity | ]. + rewrite of'_to'; reflexivity. + Qed. + End lift_relation. End lift_option. Global Arguments of' {T t} _. Global Arguments to' {T t} _. - Global Arguments Some {T t} _. Global Arguments lift_relation {T _} R _ _ _. Section lift_option2. - Context (T U : Type). - Definition lift_relation2 (R : T -> U -> Prop) + Context (T U : Type) (R : T -> U -> Prop). + Definition lift_relation2 : forall t, interp_base_type' T t -> interp_base_type' U t -> Prop := fun t x y => match of' (t:=Tbase t) x, of' (t:=Tbase t) y with | Datatypes.Some x', Datatypes.Some y' => R x' y' | None, None => True | _, _ => False end. + + Lemma lift_relation2_flat_type_pointwise t x y x' y' + (Hx : of' x = Datatypes.Some x') + (Hy : of' y = Datatypes.Some y') + : interp_flat_type_rel_pointwise lift_relation2 x y + <-> interp_flat_type_rel_pointwise (t:=t) (fun _ => R) x' y'. + Proof. + induction t; simpl; try tauto. + { unfold lift_relation2; rewrite Hx, Hy; reflexivity. } + { rewrite of'_pair in Hx, Hy. + destruct (of' (fst x)) eqn:?, (of' (snd x)) eqn:?; try congruence. + destruct (of' (fst y)) eqn:?, (of' (snd y)) eqn:?; try congruence. + inversion_option; subst. + destruct_head_hnf prod; split_iff; intuition eauto. } + Qed. + + Lemma lift_relation2_type_pointwise t f g f' g' + (Hx : forall x x', of' x = Datatypes.Some x' -> of' (f x) = Datatypes.Some (f' x')) + (Hy : forall x x', of' x = Datatypes.Some x' -> of' (g x) = Datatypes.Some (g' x')) + : interp_type_rel_pointwise lift_relation2 f g + -> interp_type_rel_pointwise (t:=t) (fun _ => R) f' g'. + Proof. + destruct t; simpl; unfold Morphisms.respectful_hetero. + intros H x y p; specialize (H (to' (Datatypes.Some x)) (to' (Datatypes.Some y))). + eapply lift_relation2_flat_type_pointwise in p; [ | apply of'_to'.. ]. + specialize (H p). + eapply lift_relation2_flat_type_pointwise in H; [ exact H | .. ]; + [ erewrite Hx; [ reflexivity | ] + | erewrite Hy; [ reflexivity | ] ]; + rewrite of'_to'; reflexivity. + Qed. End lift_option2. Global Arguments lift_relation2 {T U} R _ _ _. End LiftOption. @@ -271,17 +343,18 @@ Module InterpretationsGen (Bit : BitSize). end. Definition interp_op {src dst} (f : op src dst) : interp_flat_type interp_base_type src -> interp_flat_type interp_base_type dst := match f in op src dst return interp_flat_type interp_base_type src -> interp_flat_type interp_base_type dst with - | OpConst v => fun _ => ZToWordW v - | Add => fun xy => fst xy + snd xy - | Sub => fun xy => fst xy - snd xy - | Mul => fun xy => fst xy * snd xy - | Shl => fun xy => fst xy << snd xy - | Shr => fun xy => fst xy >> snd xy - | Land => fun xy => land (fst xy) (snd xy) - | Lor => fun xy => lor (fst xy) (snd xy) - | Neg int_width => fun x => neg int_width x - | Cmovne => fun xyzw => let '(x, y, z, w) := eta4 xyzw in cmovne x y z w - | Cmovle => fun xyzw => let '(x, y, z, w) := eta4 xyzw in cmovle x y z w + | OpConst TZ v => fun _ => ZToWordW v + | Add TZ => fun xy => fst xy + snd xy + | Sub TZ => fun xy => fst xy - snd xy + | Mul TZ => fun xy => fst xy * snd xy + | Shl TZ => fun xy => fst xy << snd xy + | Shr TZ => fun xy => fst xy >> snd xy + | Land TZ => fun xy => land (fst xy) (snd xy) + | Lor TZ => fun xy => lor (fst xy) (snd xy) + | Neg TZ int_width => fun x => neg int_width x + | Cmovne TZ => fun xyzw => let '(x, y, z, w) := eta4 xyzw in cmovne x y z w + | Cmovle TZ => fun xyzw => let '(x, y, z, w) := eta4 xyzw in cmovle x y z w + | Cast TZ TZ => fun x => x end%wordW. Definition of_Z ty : Z.interp_base_type ty -> interp_base_type ty @@ -416,20 +489,21 @@ Module InterpretationsGen (Bit : BitSize). End Notations. Definition interp_base_type (ty : base_type) : Type - := LiftOption.interp_base_type' bounds ty. + := option bounds. Definition interp_op {src dst} (f : op src dst) : interp_flat_type interp_base_type src -> interp_flat_type interp_base_type dst := match f in op src dst return interp_flat_type interp_base_type src -> interp_flat_type interp_base_type dst with - | OpConst v => fun _ => SmartBuildBounds v v - | Add => fun xy => fst xy + snd xy - | Sub => fun xy => fst xy - snd xy - | Mul => fun xy => fst xy * snd xy - | Shl => fun xy => fst xy << snd xy - | Shr => fun xy => fst xy >> snd xy - | Land => fun xy => land (fst xy) (snd xy) - | Lor => fun xy => lor (fst xy) (snd xy) - | Neg int_width => fun x => neg int_width x - | Cmovne => fun xyzw => let '(x, y, z, w) := eta4 xyzw in cmovne x y z w - | Cmovle => fun xyzw => let '(x, y, z, w) := eta4 xyzw in cmovle x y z w + | OpConst TZ v => fun _ => SmartBuildBounds v v + | Add _ => fun xy => fst xy + snd xy + | Sub _ => fun xy => fst xy - snd xy + | Mul _ => fun xy => fst xy * snd xy + | Shl _ => fun xy => fst xy << snd xy + | Shr _ => fun xy => fst xy >> snd xy + | Land _ => fun xy => land (fst xy) (snd xy) + | Lor _ => fun xy => lor (fst xy) (snd xy) + | Neg _ int_width => fun x => neg int_width x + | Cmovne _ => fun xyzw => let '(x, y, z, w) := eta4 xyzw in cmovne x y z w + | Cmovle _ => fun xyzw => let '(x, y, z, w) := eta4 xyzw in cmovle x y z w + | Cast _ _ => fun x => x end%bounds. Definition of_wordW ty : WordW.interp_base_type ty -> interp_base_type ty @@ -804,17 +878,18 @@ Module InterpretationsGen (Bit : BitSize). Definition interp_op {src dst} (f : op src dst) : interp_flat_type interp_base_type src -> interp_flat_type interp_base_type dst := match f in op src dst return interp_flat_type interp_base_type src -> interp_flat_type interp_base_type dst with - | OpConst v => fun _ => SmartBuildBoundedWord v - | Add => fun xy => fst xy + snd xy - | Sub => fun xy => fst xy - snd xy - | Mul => fun xy => fst xy * snd xy - | Shl => fun xy => fst xy << snd xy - | Shr => fun xy => fst xy >> snd xy - | Land => fun xy => land (fst xy) (snd xy) - | Lor => fun xy => lor (fst xy) (snd xy) - | Neg int_width => fun x => neg int_width x - | Cmovne => fun xyzw => let '(x, y, z, w) := eta4 xyzw in cmovne x y z w - | Cmovle => fun xyzw => let '(x, y, z, w) := eta4 xyzw in cmovle x y z w + | OpConst TZ v => fun _ => SmartBuildBoundedWord v + | Add TZ => fun xy => fst xy + snd xy + | Sub TZ => fun xy => fst xy - snd xy + | Mul TZ => fun xy => fst xy * snd xy + | Shl TZ => fun xy => fst xy << snd xy + | Shr TZ => fun xy => fst xy >> snd xy + | Land TZ => fun xy => land (fst xy) (snd xy) + | Lor TZ => fun xy => lor (fst xy) (snd xy) + | Neg TZ int_width => fun x => neg int_width x + | Cmovne TZ => fun xyzw => let '(x, y, z, w) := eta4 xyzw in cmovne x y z w + | Cmovle TZ => fun xyzw => let '(x, y, z, w) := eta4 xyzw in cmovle x y z w + | Cast TZ TZ => fun x => x end%bounded_word. End BoundedWordW. diff --git a/src/Reflection/Z/JavaNotations.v b/src/Reflection/Z/JavaNotations.v index 4a33a6330..8dc23ec82 100644 --- a/src/Reflection/Z/JavaNotations.v +++ b/src/Reflection/Z/JavaNotations.v @@ -40,18 +40,18 @@ Notation "'(int)' x" := (Op (Cast _ (TWord 5)) (Var x)). Notation "'M32' & x" := (Op (Cast _ (TWord 6)) (Var x)). Notation "'(uint128_t)' x" := (Op (Cast _ (TWord 7)) (Var x)). *) -Notation "x + y" := (Op (Add) (Pair x y)). -Notation "x + y" := (Op (Add) (Pair (Var x) y)). -Notation "x + y" := (Op (Add) (Pair x (Var y))). -Notation "x + y" := (Op (Add) (Pair (Var x) (Var y))). -Notation "x - y" := (Op (Sub) (Pair x y)). -Notation "x - y" := (Op (Sub) (Pair (Var x) y)). -Notation "x - y" := (Op (Sub) (Pair x (Var y))). -Notation "x - y" := (Op (Sub) (Pair (Var x) (Var y))). -Notation "x * y" := (Op (Mul) (Pair x y)). -Notation "x * y" := (Op (Mul) (Pair (Var x) y)). -Notation "x * y" := (Op (Mul) (Pair x (Var y))). -Notation "x * y" := (Op (Mul) (Pair (Var x) (Var y))). +Notation "x + y" := (Op (Add _) (Pair x y)). +Notation "x + y" := (Op (Add _) (Pair (Var x) y)). +Notation "x + y" := (Op (Add _) (Pair x (Var y))). +Notation "x + y" := (Op (Add _) (Pair (Var x) (Var y))). +Notation "x - y" := (Op (Sub _) (Pair x y)). +Notation "x - y" := (Op (Sub _) (Pair (Var x) y)). +Notation "x - y" := (Op (Sub _) (Pair x (Var y))). +Notation "x - y" := (Op (Sub _) (Pair (Var x) (Var y))). +Notation "x * y" := (Op (Mul _) (Pair x y)). +Notation "x * y" := (Op (Mul _) (Pair (Var x) y)). +Notation "x * y" := (Op (Mul _) (Pair x (Var y))). +Notation "x * y" := (Op (Mul _) (Pair (Var x) (Var y))). (* python: << for opn, op in (('*', 'Mul'), ('+', 'Add'), ('&', 'Land')): @@ -115,20 +115,18 @@ Notation "x + y" := (Op (Add (TWord 7)) (Pair x (Op (Cast _ (TWord 7)) (Var y))) Notation "x + y" := (Op (Add (TWord 7)) (Pair (Var x) (Op (Cast _ (TWord 7)) y))). Notation "x + y" := (Op (Add (TWord 7)) (Pair (Var x) (Op (Cast _ (TWord 7)) (Var y)))). *) -Notation "x >>> y" := (Op (Shr) (Pair x y)). -Notation "x >>> y" := (Op (Shr) (Pair (Var x) y)). -Notation "x >>> y" := (Op (Shr) (Pair x (Var y))). -Notation "x >>> y" := (Op (Shr) (Pair (Var x) (Var y))). -(* +Notation "x >>> y" := (Op (Shr _) (Pair x y)). +Notation "x >>> y" := (Op (Shr _) (Pair (Var x) y)). +Notation "x >>> y" := (Op (Shr _) (Pair x (Var y))). +Notation "x >>> y" := (Op (Shr _) (Pair (Var x) (Var y))). Notation "x >>> y" := (Op (Shr _) (Pair x (Op (Cast _ _) y))). Notation "x >>> y" := (Op (Shr _) (Pair (Var x) (Op (Cast _ _) y))). Notation "x >>> y" := (Op (Shr _) (Pair x (Op (Cast _ _) (Var y)))). Notation "x >>> y" := (Op (Shr _) (Pair (Var x) (Op (Cast _ _) (Var y)))). -*) -Notation "x & y" := (Op (Land) (Pair x y)). -Notation "x & y" := (Op (Land) (Pair (Var x) y)). -Notation "x & y" := (Op (Land) (Pair x (Var y))). -Notation "x & y" := (Op (Land) (Pair (Var x) (Var y))). +Notation "x & y" := (Op (Land _) (Pair x y)). +Notation "x & y" := (Op (Land _) (Pair (Var x) y)). +Notation "x & y" := (Op (Land _) (Pair x (Var y))). +Notation "x & y" := (Op (Land _) (Pair (Var x) (Var y))). (* Notation "x & y" := (Op (Land (TWord 6)) (Pair (Op (Cast _ (TWord 6)) x) y)). Notation "x & y" := (Op (Land (TWord 6)) (Pair (Op (Cast _ (TWord 6)) x) (Var y))). diff --git a/src/Reflection/Z/OpInversion.v b/src/Reflection/Z/OpInversion.v index 3ef7b7e5a..6b2cdd85b 100644 --- a/src/Reflection/Z/OpInversion.v +++ b/src/Reflection/Z/OpInversion.v @@ -19,9 +19,9 @@ Ltac invert_op := repeat invert_op_step. Ltac invert_match_op_step := match goal with - | [ |- appcontext[match ?e with OpConst _ => _ | _ => _ end] ] + | [ |- appcontext[match ?e with OpConst _ _ => _ | _ => _ end] ] => invert_one_op e - | [ H : appcontext[match ?e with OpConst _ => _ | _ => _ end] |- _ ] + | [ H : appcontext[match ?e with OpConst _ _ => _ | _ => _ end] |- _ ] => invert_one_op e end. diff --git a/src/Reflection/Z/Reify.v b/src/Reflection/Z/Reify.v index e200b2e9e..84bc6f078 100644 --- a/src/Reflection/Z/Reify.v +++ b/src/Reflection/Z/Reify.v @@ -10,22 +10,24 @@ Require Import Crypto.Reflection.Inline. Require Import Crypto.Reflection.InlineInterp. Require Import Crypto.Reflection.Linearize. Require Import Crypto.Reflection.LinearizeInterp. +Require Import Crypto.Reflection.Eta. +Require Import Crypto.Reflection.EtaInterp. Ltac base_reify_op op op_head extra ::= lazymatch op_head with - | @Z.add => constr:(reify_op op op_head 2 Add) - | @Z.mul => constr:(reify_op op op_head 2 Mul) - | @Z.sub => constr:(reify_op op op_head 2 Sub) - | @Z.shiftl => constr:(reify_op op op_head 2 Shl) - | @Z.shiftr => constr:(reify_op op op_head 2 Shr) - | @Z.land => constr:(reify_op op op_head 2 Land) - | @Z.lor => constr:(reify_op op op_head 2 Lor) - | @ModularBaseSystemListZOperations.cmovne => constr:(reify_op op op_head 4 Cmovne) - | @ModularBaseSystemListZOperations.cmovl => constr:(reify_op op op_head 4 Cmovle) + | @Z.add => constr:(reify_op op op_head 2 (Add TZ)) + | @Z.mul => constr:(reify_op op op_head 2 (Mul TZ)) + | @Z.sub => constr:(reify_op op op_head 2 (Sub TZ)) + | @Z.shiftl => constr:(reify_op op op_head 2 (Shl TZ)) + | @Z.shiftr => constr:(reify_op op op_head 2 (Shr TZ)) + | @Z.land => constr:(reify_op op op_head 2 (Land TZ)) + | @Z.lor => constr:(reify_op op op_head 2 (Lor TZ)) + | @ModularBaseSystemListZOperations.cmovne => constr:(reify_op op op_head 4 (Cmovne TZ)) + | @ModularBaseSystemListZOperations.cmovl => constr:(reify_op op op_head 4 (Cmovle TZ)) | @ModularBaseSystemListZOperations.neg => lazymatch extra with | @ModularBaseSystemListZOperations.neg ?int_width _ - => constr:(reify_op op op_head 1 (Neg int_width)) + => constr:(reify_op op op_head 1 (Neg TZ int_width)) | _ => fail 100 "Anomaly: In Reflection.Z.base_reify_op: head is neg but body is wrong:" extra end end. @@ -36,12 +38,13 @@ Ltac base_reify_type T ::= Ltac Reify' e := Reflection.Reify.Reify' base_type interp_base_type op e. Ltac Reify e := let v := Reflection.Reify.Reify base_type interp_base_type op make_const e in - constr:((*Inline _*) ((*CSE _*) (InlineConst is_const (Linearize v)))). -Ltac prove_InlineConst_Linearize_Compile_correct := + constr:(ExprEta ((*Inline _*) ((*CSE _*) (InlineConst is_const (Linearize v))))). +Ltac prove_ExprEta_InlineConst_Linearize_Compile_correct := fun _ => intros; + rewrite ?InterpExprEta; lazymatch goal with - | [ |- ?R (@Syntax.Interp ?base_type_code ?interp_base_type ?op ?interp_op ?t (InlineConst ?is_const (Linearize _))) _ ] + | [ |- ?R (@Syntax.Interp ?base_type_code ?interp_base_type ?op ?interp_op ?t (InlineConst ?is_const (Linearize _)) ?x) _ ] => etransitivity; [ apply (@InterpInlineConst base_type_code interp_base_type op interp_op is_const t); reflect_Wf base_type_eq_semidec_is_dec op_beq_bl @@ -50,4 +53,4 @@ Ltac prove_InlineConst_Linearize_Compile_correct := | prove_compile_correct () ] ] end. Ltac Reify_rhs := - Reflection.Reify.Reify_rhs_gen Reify prove_InlineConst_Linearize_Compile_correct interp_op ltac:(fun tac => tac ()). + Reflection.Reify.Reify_rhs_gen Reify prove_ExprEta_InlineConst_Linearize_Compile_correct interp_op ltac:(fun tac => tac ()). diff --git a/src/Reflection/Z/Syntax.v b/src/Reflection/Z/Syntax.v index 2060c6852..9b009386c 100644 --- a/src/Reflection/Z/Syntax.v +++ b/src/Reflection/Z/Syntax.v @@ -16,17 +16,18 @@ Definition interp_base_type (v : base_type) : Type := end. Inductive op : flat_type base_type -> flat_type base_type -> Type := -| OpConst (z : Z) : op Unit tZ -| Add : op (tZ * tZ) tZ -| Sub : op (tZ * tZ) tZ -| Mul : op (tZ * tZ) tZ -| Shl : op (tZ * tZ) tZ -| Shr : op (tZ * tZ) tZ -| Land : op (tZ * tZ) tZ -| Lor : op (tZ * tZ) tZ -| Neg (int_width : Z) : op tZ tZ -| Cmovne : op (tZ * tZ * tZ * tZ) tZ -| Cmovle : op (tZ * tZ * tZ * tZ) tZ. +| OpConst {T} (z : interp_base_type T) : op Unit (Tbase T) +| Add T : op (Tbase T * Tbase T) (Tbase T) +| Sub T : op (Tbase T * Tbase T) (Tbase T) +| Mul T : op (Tbase T * Tbase T) (Tbase T) +| Shl T : op (Tbase T * Tbase T) (Tbase T) +| Shr T : op (Tbase T * Tbase T) (Tbase T) +| Land T : op (Tbase T * Tbase T) (Tbase T) +| Lor T : op (Tbase T * Tbase T) (Tbase T) +| Neg T (int_width : Z) : op (Tbase T) (Tbase T) +| Cmovne T : op (Tbase T * Tbase T * Tbase T * Tbase T) (Tbase T) +| Cmovle T : op (Tbase T * Tbase T * Tbase T * Tbase T) (Tbase T) +| Cast T1 T2 : op (Tbase T1) (Tbase T2). Definition interpToZ {t} : interp_base_type t -> Z := match t with @@ -45,15 +46,16 @@ Local Notation eta4 x := (eta3 (fst x), snd x). Definition interp_op src dst (f : op src dst) : interp_flat_type interp_base_type src -> interp_flat_type interp_base_type dst := match f in op src dst return interp_flat_type interp_base_type src -> interp_flat_type interp_base_type dst with - | OpConst v => fun _ => v - | Add => fun xy => fst xy + snd xy - | Sub => fun xy => fst xy - snd xy - | Mul => fun xy => fst xy * snd xy - | Shl => fun xy => Z.shiftl (fst xy) (snd xy) - | Shr => fun xy => Z.shiftr (fst xy) (snd xy) - | Land => fun xy => Z.land (fst xy) (snd xy) - | Lor => fun xy => Z.lor (fst xy) (snd xy) - | Neg int_width => fun x => ModularBaseSystemListZOperations.neg int_width x - | Cmovne => fun xyzw => let '(x, y, z, w) := eta4 xyzw in cmovne x y z w - | Cmovle => fun xyzw => let '(x, y, z, w) := eta4 xyzw in cmovl x y z w + | OpConst _ v => fun _ => v + | Add TZ => fun xy => fst xy + snd xy + | Sub TZ => fun xy => fst xy - snd xy + | Mul TZ => fun xy => fst xy * snd xy + | Shl TZ => fun xy => Z.shiftl (fst xy) (snd xy) + | Shr TZ => fun xy => Z.shiftr (fst xy) (snd xy) + | Land TZ => fun xy => Z.land (fst xy) (snd xy) + | Lor TZ => fun xy => Z.lor (fst xy) (snd xy) + | Neg TZ int_width => fun x => ModularBaseSystemListZOperations.neg int_width x + | Cmovne TZ => fun xyzw => let '(x, y, z, w) := eta4 xyzw in cmovne x y z w + | Cmovle TZ => fun xyzw => let '(x, y, z, w) := eta4 xyzw in cmovl x y z w + | Cast _ _ => cast_const end%Z. diff --git a/src/Reflection/Z/Syntax/Equality.v b/src/Reflection/Z/Syntax/Equality.v index 3043deae1..ff3ed9b67 100644 --- a/src/Reflection/Z/Syntax/Equality.v +++ b/src/Reflection/Z/Syntax/Equality.v @@ -1,10 +1,15 @@ Require Import Coq.ZArith.ZArith. Require Import Crypto.Reflection.Syntax. +Require Import Crypto.Reflection.TypeInversion. Require Import Crypto.Reflection.Equality. Require Import Crypto.Reflection.Z.Syntax. Require Import Crypto.Util.Decidable. Require Import Crypto.Util.PartiallyReifiedProp. Require Import Crypto.Util.HProp. +Require Import Crypto.Util.Tactics.BreakMatch. +Require Import Crypto.Util.Tactics.DestructHead. +Require Import Crypto.Util.FixedWordSizesEquality. +Require Import Crypto.Util.NatUtil. Global Instance dec_eq_base_type : DecidableRel (@eq base_type) := base_type_eq_dec. @@ -13,46 +18,69 @@ Global Instance dec_eq_type : DecidableRel (@eq (type base_type)) := _. Definition base_type_eq_semidec_transparent (t1 t2 : base_type) : option (t1 = t2) - := Some (match t1, t2 return t1 = t2 with - | TZ, TZ => eq_refl - end). + := match base_type_eq_dec t1 t2 with + | left pf => Some pf + | right _ => None + end. Lemma base_type_eq_semidec_is_dec t1 t2 : base_type_eq_semidec_transparent t1 t2 = None -> t1 <> t2. Proof. - unfold base_type_eq_semidec_transparent; congruence. + unfold base_type_eq_semidec_transparent; break_match; congruence. Qed. -Definition op_beq_hetero {t1 tR t1' tR'} (f : op t1 tR) (g : op t1' tR') : reified_Prop +Definition op_beq_hetero {t1 tR t1' tR'} (f : op t1 tR) (g : op t1' tR') : bool := match f, g return bool with - | OpConst v, OpConst v' => Z.eqb v v' - | OpConst _, _ => false - | Add, Add => true - | Add, _ => false - | Sub, Sub => true - | Sub, _ => false - | Mul, Mul => true - | Mul, _ => false - | Shl, Shl => true - | Shl, _ => false - | Shr, Shr => true - | Shr, _ => false - | Land, Land => true - | Land, _ => false - | Lor, Lor => true - | Lor, _ => false - | Neg n, Neg m => Z.eqb n m - | Neg _, _ => false - | Cmovne, Cmovne => true - | Cmovne, _ => false - | Cmovle, Cmovle => true - | Cmovle, _ => false - end. + | OpConst TZ v, OpConst TZ v' => Z.eqb v v' + | OpConst _ _, _ => false + | Add T1, Add T2 + | Sub T1, Sub T2 + | Mul T1, Mul T2 + | Shl T1, Shl T2 + | Shr T1, Shr T2 + | Land T1, Land T2 + | Lor T1, Lor T2 + | Cmovne T1, Cmovne T2 + | Cmovle T1, Cmovle T2 + => base_type_beq T1 T2 + | Neg T1 n, Neg T2 m + => base_type_beq T1 T2 && Z.eqb n m + | Cast T1 T2, Cast T1' T2' + => base_type_beq T1 T1' && base_type_beq T2 T2' + | Add _, _ => false + | Sub _, _ => false + | Mul _, _ => false + | Shl _, _ => false + | Shr _, _ => false + | Land _, _ => false + | Lor _, _ => false + | Neg _ _, _ => false + | Cmovne _, _ => false + | Cmovle _, _ => false + | Cast _ _, _ => false + end%bool. -Definition op_beq t1 tR (f g : op t1 tR) : reified_Prop +Definition op_beq t1 tR (f g : op t1 tR) : bool := Eval cbv [op_beq_hetero] in op_beq_hetero f g. Definition op_beq_hetero_type_eq {t1 tR t1' tR'} f g : to_prop (@op_beq_hetero t1 tR t1' tR' f g) -> t1 = t1' /\ tR = tR'. Proof. - destruct f, g; simpl; try solve [ repeat constructor | intros [] ]. + destruct f, g; + repeat match goal with + | _ => progress unfold op_beq_hetero in * + | _ => simpl; intro; exfalso; assumption + | _ => solve [ repeat constructor ] + | _ => progress destruct_head base_type + | [ |- context[reified_Prop_of_bool ?b] ] + => let H := fresh in destruct (Sumbool.sumbool_of_bool b) as [H|H]; rewrite H + | [ H : nat_beq _ _ = true |- _ ] => apply internal_nat_dec_bl in H; subst + | [ H : wordT_beq_hetero _ _ = true |- _ ] => apply wordT_beq_bl in H; subst + | [ H : wordT_beq_hetero _ _ = true |- _ ] => apply wordT_beq_hetero_bl in H; destruct H; subst + | [ H : andb ?x ?y = true |- _ ] + => assert (x = true /\ y = true) by (destruct x, y; simpl in *; repeat constructor; exfalso; clear -H; abstract congruence); + clear H + | [ H : and _ _ |- _ ] => destruct H + | [ H : false = true |- _ ] => exfalso; clear -H; abstract congruence + | [ H : true = false |- _ ] => exfalso; clear -H; abstract congruence + end. Defined. Definition op_beq_hetero_type_eqs {t1 tR t1' tR'} f g : to_prop (@op_beq_hetero t1 tR t1' tR' f g) -> t1 = t1' @@ -68,22 +96,29 @@ Definition op_beq_hetero_eq {t1 tR t1' tR'} f g _ (op_beq_hetero_type_eqs f g pf) = g. Proof. - destruct f, g; simpl; try solve [ reflexivity | intros [] ]; - unfold op_beq_hetero; simpl; - repeat match goal with - | [ |- context[to_prop (reified_Prop_of_bool ?x)] ] - => destruct (Sumbool.sumbool_of_bool x) as [P|P] - | [ H : NatUtil.nat_beq _ _ = true |- _ ] - => apply NatUtil.internal_nat_dec_bl in H - | [ H : Z.eqb _ _ = true |- _ ] - => apply Z.eqb_eq in H - | _ => progress subst - | _ => reflexivity - | [ H : ?x = false |- context[reified_Prop_of_bool ?x] ] - => rewrite H - | _ => progress simpl @to_prop - | _ => tauto - end. + destruct f, g; + repeat match goal with + | _ => solve [ intros [] ] + | _ => reflexivity + | [ H : False |- _ ] => exfalso; assumption + | _ => intro + | [ |- context[op_beq_hetero_type_eqd ?f ?g ?pf] ] + => generalize (op_beq_hetero_type_eqd f g pf), (op_beq_hetero_type_eqs f g pf) + | _ => intro + | _ => progress eliminate_hprop_eq + | _ => progress inversion_flat_type + | _ => progress unfold op_beq_hetero in * + | _ => progress simpl in * + | [ H : context[andb ?x ?y] |- _ ] + => destruct x eqn:?, y eqn:?; simpl in H + | [ H : Z.eqb _ _ = true |- _ ] => apply Z.eqb_eq in H + | [ H : to_prop (reified_Prop_of_bool ?b) |- _ ] => destruct b eqn:?; compute in H + | _ => progress subst + | _ => progress break_match_hyps + | [ H : wordT_beq_hetero _ _ = true |- _ ] => apply wordT_beq_bl in H; subst + | [ H : wordT_beq_hetero _ _ = true |- _ ] => apply wordT_beq_hetero_bl in H; destruct H; subst + | _ => congruence + end. Qed. Lemma op_beq_bl : forall t1 tR x y, to_prop (op_beq t1 tR x y) -> x = y. diff --git a/src/Reflection/Z/Syntax/Util.v b/src/Reflection/Z/Syntax/Util.v index 42569daf8..1d591658f 100644 --- a/src/Reflection/Z/Syntax/Util.v +++ b/src/Reflection/Z/Syntax/Util.v @@ -1,4 +1,5 @@ Require Import Crypto.Reflection.Syntax. +Require Import Crypto.Reflection.Wf. Require Import Crypto.Reflection.TypeUtil. Require Import Crypto.Reflection.TypeInversion. Require Import Crypto.Reflection.Z.Syntax. @@ -9,17 +10,85 @@ 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. + := OpConst. Definition is_const s d (v : op s d) : bool - := match v with OpConst _ => true | _ => false end. + := match v with OpConst _ _ => true | _ => false end. Arguments is_const [s d] v. Definition is_cast s d (v : op s d) : bool - := false. + := match v with Cast _ _ => true | _ => false end. Arguments is_cast [s d] v. Definition base_type_leb (v1 v2 : base_type) : bool - := true. + := match v1, v2 with + | _, TZ => true + end. Definition base_type_min := base_type_min base_type_leb. Global Arguments base_type_min !_ !_ / . Global Arguments TypeUtil.base_type_min _ _ _ / . + +Definition Castb {var} A A' (v : exprf base_type op (var:=var) (Tbase A)) + : exprf base_type op (var:=var) (Tbase A') + := Op (Cast A A') v. + +Local Notation Se opv := (Some (existT _ (_, _) opv)) (only parsing). + +Definition genericize_op src dst (opc : op src dst) (t_in t_out : base_type) + : option { src'dst' : _ & op (fst src'dst') (snd src'dst') } + := match opc with + | OpConst T z => Se (OpConst z) + | Add T => Se (Add t_out) + | Sub T => Se (Sub t_in) + | Mul T => Se (Mul t_out) + | Shl T => Se (Shl t_out) + | Shr T => Se (Shr t_in) + | Land T => Se (Land t_out) + | Lor T => Se (Lor t_out) + | Neg T int_width => Se (Neg t_out int_width) + | Cmovne T => Se (Cmovne t_out) + | Cmovle T => Se (Cmovle t_out) + | Cast T1 T2 => None + end. + +Lemma cast_const_id {t} v + : @cast_const t t v = v. +Proof. + destruct t; simpl; trivial. +Qed. + +Lemma cast_const_idempotent {a b c} v + : base_type_min b (base_type_min a c) = base_type_min a c + -> @cast_const b c (@cast_const a b v) = @cast_const a c v. +Proof. + repeat first [ reflexivity + | congruence + | progress destruct_head' base_type + | progress simpl + | progress break_match + | progress subst + | intro + | match goal with + | [ H : ?leb _ _ = true |- _ ] => apply Compare_dec.leb_complete in H + | [ H : ?leb _ _ = false |- _ ] => apply Compare_dec.leb_iff_conv in H + end + | rewrite ZToWord_wordToZ_ZToWord by omega * + | rewrite wordToZ_ZToWord_wordToZ by omega * ]. +Qed. + +Lemma is_cast_correct s d opc + : forall e, + @is_cast (Tbase s) (Tbase d) opc = true + -> Syntax.interp_op _ _ opc (interpf Syntax.interp_op e) + = interpf Syntax.interp_op (Castb s d e). +Proof. + preinvert_one_type opc; intros ? opc. + pose (fun x y => op y x) as op'. + change op with (fun x y => op' y x) in opc; cbv beta in opc. + preinvert_one_type opc; intros ? opc; subst op'; cbv beta in *. + destruct opc; try exact I; simpl; try congruence. +Qed. + +Lemma wff_Castb {var1 var2 G A A'} {e1 e2 : exprf base_type op (Tbase A)} + (Hwf : wff (var1:=var1) (var2:=var2) G e1 e2) + : wff G (Castb A A' e1) (Castb A A' e2). +Proof. constructor; assumption. Qed. |