diff options
Diffstat (limited to 'src/Reflection/Z')
| -rw-r--r-- | src/Reflection/Z/BoundsInterpretations.v | 25 | ||||
| -rw-r--r-- | src/Reflection/Z/CNotations.v | 42 | ||||
| -rw-r--r-- | src/Reflection/Z/Interpretations128/Relations.v | 11 | ||||
| -rw-r--r-- | src/Reflection/Z/Interpretations128/RelationsCombinations.v | 375 | ||||
| -rw-r--r-- | src/Reflection/Z/Interpretations64/Relations.v | 10 | ||||
| -rw-r--r-- | src/Reflection/Z/Interpretations64/RelationsCombinations.v | 375 | ||||
| -rw-r--r-- | src/Reflection/Z/InterpretationsGen.v | 183 | ||||
| -rw-r--r-- | src/Reflection/Z/JavaNotations.v | 42 | ||||
| -rw-r--r-- | src/Reflection/Z/OpInversion.v | 4 | ||||
| -rw-r--r-- | src/Reflection/Z/Reify.v | 31 | ||||
| -rw-r--r-- | src/Reflection/Z/Syntax.v | 46 | ||||
| -rw-r--r-- | src/Reflection/Z/Syntax/Equality.v | 127 | ||||
| -rw-r--r-- | src/Reflection/Z/Syntax/Util.v | 77 |
13 files changed, 656 insertions, 692 deletions
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. |