aboutsummaryrefslogtreecommitdiff
path: root/src/Reflection/Z
diff options
context:
space:
mode:
Diffstat (limited to 'src/Reflection/Z')
-rw-r--r--src/Reflection/Z/Interpretations128/Relations.v81
-rw-r--r--src/Reflection/Z/Interpretations128/RelationsCombinations.v14
-rw-r--r--src/Reflection/Z/Interpretations64/Relations.v81
-rw-r--r--src/Reflection/Z/Interpretations64/RelationsCombinations.v14
-rw-r--r--src/Reflection/Z/InterpretationsGen.v10
-rw-r--r--src/Reflection/Z/Reify.v11
-rw-r--r--src/Reflection/Z/Syntax.v9
7 files changed, 151 insertions, 69 deletions
diff --git a/src/Reflection/Z/Interpretations128/Relations.v b/src/Reflection/Z/Interpretations128/Relations.v
index 5ce0df08e..fcd7bf2d8 100644
--- a/src/Reflection/Z/Interpretations128/Relations.v
+++ b/src/Reflection/Z/Interpretations128/Relations.v
@@ -2,7 +2,8 @@ Require Import Coq.ZArith.ZArith.
Require Import Coq.micromega.Psatz.
Require Import Crypto.Reflection.Z.Syntax.
Require Import Crypto.Reflection.Syntax.
-Require Import Crypto.Reflection.Application.
+Require Import Crypto.Reflection.Relations.
+Require Import Crypto.Reflection.Tuple.
Require Import Crypto.Reflection.Z.InterpretationsGen.
Require Import Crypto.Reflection.Z.Interpretations128.
Require Import Crypto.ModularArithmetic.ModularBaseSystemListZOperationsProofs.
@@ -152,7 +153,7 @@ Lemma related_tuples_None_left
(v : interp_flat_type interp_base_type' (tuple (Tbase TZ) (S n)))
: interp_flat_type_rel_pointwise2
R
- (flat_interp_untuple' (T:=Tbase TZ) (Tuple.push_option (n:=S n) None))
+ (flat_interp_untuple (T:=Tbase TZ) (Tuple.push_option None))
v.
Proof.
induction n; simpl; intuition.
@@ -162,16 +163,17 @@ Lemma related_tuples_Some_left
n T interp_base_type'
(R : forall t, T -> interp_base_type' t -> Prop)
u
- (v : interp_flat_type interp_base_type' (tuple (Tbase TZ) (S n)))
+ (v : interp_flat_type interp_base_type' (tuple (Tbase TZ) n))
: interp_flat_type_rel_pointwise2
R
- (flat_interp_untuple' (T:=Tbase TZ) u)
+ (flat_interp_untuple (T:=Tbase TZ) u)
v
<-> interp_flat_type_rel_pointwise2
(LiftOption.lift_relation R)
- (flat_interp_untuple' (T:=Tbase TZ) (Tuple.push_option (n:=S n) (Some u)))
+ (flat_interp_untuple (T:=Tbase TZ) (Tuple.push_option (Some u)))
v.
Proof.
+ destruct n as [|n]; [ reflexivity | ].
induction n; [ reflexivity | ].
simpl in *; rewrite <- IHn; clear IHn.
reflexivity.
@@ -181,14 +183,15 @@ Lemma related_tuples_Some_left_ext
{n T interp_base_type'}
{R : forall t, T -> interp_base_type' t -> Prop}
{u v u'}
- (H : Tuple.lift_option (flat_interp_tuple (T:=Tbase TZ) (n:=S n) u) = Some u')
+ (H : Tuple.lift_option (flat_interp_tuple (T:=Tbase TZ) (n:=n) u) = Some u')
: interp_flat_type_rel_pointwise2
R
- (flat_interp_untuple' (T:=Tbase TZ) u') v
+ (flat_interp_untuple (T:=Tbase TZ) u') v
<-> interp_flat_type_rel_pointwise2
(LiftOption.lift_relation R)
u v.
Proof.
+ destruct n as [|n]; [ reflexivity | ].
induction n.
{ simpl in *; subst; reflexivity. }
{ destruct_head_hnf' prod.
@@ -200,13 +203,14 @@ Qed.
Lemma related_tuples_proj_eq_rel_untuple
{n T interp_base_type'}
{proj : forall t, T -> interp_base_type' t}
- {u : Tuple.tuple _ (S n)} {v : Tuple.tuple _ (S n)}
+ {u : Tuple.tuple _ n} {v : Tuple.tuple _ n}
: interp_flat_type_rel_pointwise2
(fun t => proj_eq_rel (proj t))
- (flat_interp_untuple' (T:=Tbase TZ) u)
- (flat_interp_untuple' (T:=Tbase TZ) v)
+ (flat_interp_untuple (T:=Tbase TZ) u)
+ (flat_interp_untuple (T:=Tbase TZ) v)
<-> (Tuple.map (proj _) u = v).
Proof.
+ destruct n as [|n]; [ destruct_head_hnf' unit; simpl; tauto | ].
induction n; [ reflexivity | ].
destruct_head_hnf' prod.
simpl @Tuple.tuple.
@@ -222,27 +226,27 @@ Lemma related_tuples_proj_eq_rel_tuple
: interp_flat_type_rel_pointwise2
(fun t => proj_eq_rel (proj t))
u v
- <-> (Tuple.map (proj _) (flat_interp_tuple (n:=S n) (T:=Tbase TZ) u)
+ <-> (Tuple.map (proj _) (flat_interp_tuple (n:=n) (T:=Tbase TZ) u)
= flat_interp_tuple (T:=Tbase TZ) v).
Proof.
- rewrite <- related_tuples_proj_eq_rel_untuple, !flat_interp_untuple'_tuple; reflexivity.
+ rewrite <- related_tuples_proj_eq_rel_untuple, !flat_interp_untuple_tuple; reflexivity.
Qed.
Local Arguments LiftOption.lift_relation2 _ _ _ _ !_ !_ / .
-Lemma related_tuples_lift_relation2_untuple'
+Lemma related_tuples_lift_relation2_untuple
n T U
(R : T -> U -> Prop)
(t : option (Tuple.tuple T (S n)))
(u : option (Tuple.tuple U (S n)))
: interp_flat_type_rel_pointwise2
(LiftOption.lift_relation2 R)
- (flat_interp_untuple' (T:=Tbase TZ) (Tuple.push_option t))
- (flat_interp_untuple' (T:=Tbase TZ) (Tuple.push_option u))
+ (flat_interp_untuple (T:=Tbase TZ) (Tuple.push_option t))
+ (flat_interp_untuple (T:=Tbase TZ) (Tuple.push_option u))
<-> LiftOption.lift_relation2
(interp_flat_type_rel_pointwise2 (fun _ => R))
TZ
- (option_map (flat_interp_untuple' (interp_base_type:=fun _ => T) (T:=Tbase TZ)) t)
- (option_map (flat_interp_untuple' (interp_base_type:=fun _ => U) (T:=Tbase TZ)) u).
+ (option_map (flat_interp_untuple (interp_base_type:=fun _ => T) (T:=Tbase TZ)) t)
+ (option_map (flat_interp_untuple (interp_base_type:=fun _ => U) (T:=Tbase TZ)) u).
Proof.
induction n.
{ destruct_head' option; reflexivity. }
@@ -255,7 +259,7 @@ Proof.
try (simpl @interp_flat_type_rel_pointwise2; tauto). }
Qed.
-Lemma related_tuples_lift_relation2_untuple'_ext
+Lemma related_tuples_lift_relation2_untuple_ext
{n T U}
{R : T -> U -> Prop}
{t u}
@@ -267,8 +271,8 @@ Lemma related_tuples_lift_relation2_untuple'_ext
<-> LiftOption.lift_relation2
(interp_flat_type_rel_pointwise2 (fun _ => R))
TZ
- (option_map (flat_interp_untuple' (interp_base_type:=fun _ => T) (T:=Tbase TZ)) (Tuple.lift_option (flat_interp_tuple (T:=Tbase TZ) t)))
- (option_map (flat_interp_untuple' (interp_base_type:=fun _ => U) (T:=Tbase TZ)) (Tuple.lift_option (flat_interp_tuple (T:=Tbase TZ) u))).
+ (option_map (flat_interp_untuple (interp_base_type:=fun _ => T) (T:=Tbase TZ)) (Tuple.lift_option (flat_interp_tuple (T:=Tbase TZ) t)))
+ (option_map (flat_interp_untuple (interp_base_type:=fun _ => U) (T:=Tbase TZ)) (Tuple.lift_option (flat_interp_tuple (T:=Tbase TZ) u))).
Proof.
induction n.
{ destruct_head_hnf' option; reflexivity. }
@@ -293,22 +297,22 @@ Proof.
| progress break_match ] ]. }
Qed.
-Lemma lift_option_flat_interp_tuple'
+Lemma lift_option_flat_interp_tuple
{n T x y}
- : (Tuple.lift_option (n:=S n) (A:=T) (flat_interp_tuple' (interp_base_type:=LiftOption.interp_base_type' _) (T:=Tbase TZ) x) = Some y)
- <-> (x = flat_interp_untuple' (T:=Tbase TZ) (n:=n) (Tuple.push_option (n:=S n) (Some y))).
+ : (Tuple.lift_option (n:=S n) (A:=T) (flat_interp_tuple (interp_base_type:=LiftOption.interp_base_type' _) (T:=Tbase TZ) x) = Some y)
+ <-> (x = flat_interp_untuple (T:=Tbase TZ) (n:=S n) (Tuple.push_option (n:=S n) (Some y))).
Proof.
rewrite Tuple.push_lift_option; generalize (Tuple.push_option (Some y)); intro.
split; intro; subst;
- rewrite ?flat_interp_tuple'_untuple', ?flat_interp_untuple'_tuple';
+ rewrite ?flat_interp_tuple_untuple, ?flat_interp_untuple_tuple;
reflexivity.
Qed.
Lemma lift_option_None_interp_flat_type_rel_pointwise2_1
T U n R x y
(H : interp_flat_type_rel_pointwise2 (LiftOption.lift_relation2 R) x y)
- (HNone : Tuple.lift_option (A:=T) (n:=S n) (flat_interp_tuple' (T:=Tbase TZ) (n:=n) x) = None)
- : Tuple.lift_option (A:=U) (n:=S n) (flat_interp_tuple' (T:=Tbase TZ) (n:=n) y) = None.
+ (HNone : Tuple.lift_option (A:=T) (n:=S n) (flat_interp_tuple (T:=Tbase TZ) (n:=S n) x) = None)
+ : Tuple.lift_option (A:=U) (n:=S n) (flat_interp_tuple (T:=Tbase TZ) (n:=S n) y) = None.
Proof.
induction n; [ | specialize (IHn (fst x) (fst y) (proj1 H)) ];
repeat first [ progress destruct_head_hnf' False
@@ -328,12 +332,18 @@ Local Arguments LiftOption.lift_relation _ _ _ _ !_ _ / .
Local Arguments LiftOption.of' _ _ !_ / .
Local Arguments BoundedWordW.BoundedWordToBounds !_ / .
+Local Ltac unfold_related_const :=
+ intros; hnf; simpl;
+ unfold related_wordW, LiftOption.lift_relation, LiftOption.of', BoundedWordW.wordWToBoundedWord, BoundedWordW.SmartBuildBoundedWord, BoundedWordW.of_Z, BoundedWordW.of_wordW, BoundedWordW.wordWToBoundedWord;
+ simpl.
+
Lemma related_wordW_op : related_op related_wordW (@BoundedWordW.interp_op) (@WordW.interp_op).
Proof.
(let op := fresh in intros ?? op; destruct op; simpl);
try first [ apply related_wordW_t_map1
| apply related_wordW_t_map2
- | apply related_wordW_t_map4 ].
+ | apply related_wordW_t_map4
+ | unfold_related_const; break_innermost_match; reflexivity ].
Qed.
Lemma related_bounds_t_map1 opW opB pf
@@ -383,9 +393,25 @@ Local Arguments Tuple.map : simpl never.
Local Arguments Tuple.map2 : simpl never.
Local Arguments ZBounds.SmartBuildBounds _ _ / .
+
+Local Ltac related_const_op_t :=
+ unfold_related_const; break_innermost_match; try reflexivity; hnf; simpl;
+ repeat match goal with
+ | [ H : andb _ _ = true |- _ ] => apply andb_prop in H
+ | _ => progress destruct_head' and
+ | _ => progress Z.ltb_to_lt
+ | _ => rewrite WordW.wordWToZ_ZToWordW by (simpl @Z.of_nat; omega)
+ | [ H : _ |- _ ] => rewrite WordW.wordWToZ_ZToWordW in H by (simpl @Z.of_nat; omega)
+ | [ H : (Z.log2 ?x < ?y)%Z |- _ ]
+ => unique assert (x < 2^y)%Z by (apply WordW.log2_lt_pow2_alt_proj_r2l; omega)
+ | _ => reflexivity
+ | _ => omega
+ end.
+
Lemma related_bounds_op : related_op related_bounds (@BoundedWordW.interp_op) (@ZBounds.interp_op).
Proof.
let op := fresh in intros ?? op; destruct op; simpl.
+ { related_const_op_t. }
{ apply related_bounds_t_map2; intros; destruct_head' option; reflexivity. }
{ apply related_bounds_t_map2; intros; destruct_head' option; reflexivity. }
{ apply related_bounds_t_map2; intros; destruct_head' option; reflexivity. }
@@ -515,6 +541,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.
+ { related_const_op_t. }
{ apply related_Z_t_map2; related_Z_op_fin_t. }
{ apply related_Z_t_map2; related_Z_op_fin_t. }
{ apply related_Z_t_map2; related_Z_op_fin_t. }
diff --git a/src/Reflection/Z/Interpretations128/RelationsCombinations.v b/src/Reflection/Z/Interpretations128/RelationsCombinations.v
index 64c0fceb1..2de4510c7 100644
--- a/src/Reflection/Z/Interpretations128/RelationsCombinations.v
+++ b/src/Reflection/Z/Interpretations128/RelationsCombinations.v
@@ -1,6 +1,7 @@
Require Import Coq.ZArith.ZArith.
Require Import Crypto.Reflection.Z.Syntax.
Require Import Crypto.Reflection.Syntax.
+Require Import Crypto.Reflection.Relations.
Require Import Crypto.Reflection.Application.
Require Import Crypto.Reflection.Z.InterpretationsGen.
Require Import Crypto.Reflection.Z.Interpretations128.
@@ -72,7 +73,8 @@ Module Relations.
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; [ solve [ trivial | reflexivity ] | ].
+ { 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 *.
@@ -122,7 +124,8 @@ Module Relations.
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; [ solve [ trivial | reflexivity ] | ].
+ { 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 *.
@@ -181,7 +184,8 @@ Module Relations.
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; [ solve [ trivial | reflexivity ] | ].
+ { 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 *.
@@ -247,7 +251,7 @@ Module Relations.
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.
+ { 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. }
@@ -318,7 +322,7 @@ Module Relations.
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.
+ { 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. }
diff --git a/src/Reflection/Z/Interpretations64/Relations.v b/src/Reflection/Z/Interpretations64/Relations.v
index 80f3d139c..6b4279043 100644
--- a/src/Reflection/Z/Interpretations64/Relations.v
+++ b/src/Reflection/Z/Interpretations64/Relations.v
@@ -2,7 +2,8 @@ Require Import Coq.ZArith.ZArith.
Require Import Coq.micromega.Psatz.
Require Import Crypto.Reflection.Z.Syntax.
Require Import Crypto.Reflection.Syntax.
-Require Import Crypto.Reflection.Application.
+Require Import Crypto.Reflection.Relations.
+Require Import Crypto.Reflection.Tuple.
Require Import Crypto.Reflection.Z.InterpretationsGen.
Require Import Crypto.Reflection.Z.Interpretations64.
Require Import Crypto.ModularArithmetic.ModularBaseSystemListZOperationsProofs.
@@ -152,7 +153,7 @@ Lemma related_tuples_None_left
(v : interp_flat_type interp_base_type' (tuple (Tbase TZ) (S n)))
: interp_flat_type_rel_pointwise2
R
- (flat_interp_untuple' (T:=Tbase TZ) (Tuple.push_option (n:=S n) None))
+ (flat_interp_untuple (T:=Tbase TZ) (Tuple.push_option None))
v.
Proof.
induction n; simpl; intuition.
@@ -162,16 +163,17 @@ Lemma related_tuples_Some_left
n T interp_base_type'
(R : forall t, T -> interp_base_type' t -> Prop)
u
- (v : interp_flat_type interp_base_type' (tuple (Tbase TZ) (S n)))
+ (v : interp_flat_type interp_base_type' (tuple (Tbase TZ) n))
: interp_flat_type_rel_pointwise2
R
- (flat_interp_untuple' (T:=Tbase TZ) u)
+ (flat_interp_untuple (T:=Tbase TZ) u)
v
<-> interp_flat_type_rel_pointwise2
(LiftOption.lift_relation R)
- (flat_interp_untuple' (T:=Tbase TZ) (Tuple.push_option (n:=S n) (Some u)))
+ (flat_interp_untuple (T:=Tbase TZ) (Tuple.push_option (Some u)))
v.
Proof.
+ destruct n as [|n]; [ reflexivity | ].
induction n; [ reflexivity | ].
simpl in *; rewrite <- IHn; clear IHn.
reflexivity.
@@ -181,14 +183,15 @@ Lemma related_tuples_Some_left_ext
{n T interp_base_type'}
{R : forall t, T -> interp_base_type' t -> Prop}
{u v u'}
- (H : Tuple.lift_option (flat_interp_tuple (T:=Tbase TZ) (n:=S n) u) = Some u')
+ (H : Tuple.lift_option (flat_interp_tuple (T:=Tbase TZ) (n:=n) u) = Some u')
: interp_flat_type_rel_pointwise2
R
- (flat_interp_untuple' (T:=Tbase TZ) u') v
+ (flat_interp_untuple (T:=Tbase TZ) u') v
<-> interp_flat_type_rel_pointwise2
(LiftOption.lift_relation R)
u v.
Proof.
+ destruct n as [|n]; [ reflexivity | ].
induction n.
{ simpl in *; subst; reflexivity. }
{ destruct_head_hnf' prod.
@@ -200,13 +203,14 @@ Qed.
Lemma related_tuples_proj_eq_rel_untuple
{n T interp_base_type'}
{proj : forall t, T -> interp_base_type' t}
- {u : Tuple.tuple _ (S n)} {v : Tuple.tuple _ (S n)}
+ {u : Tuple.tuple _ n} {v : Tuple.tuple _ n}
: interp_flat_type_rel_pointwise2
(fun t => proj_eq_rel (proj t))
- (flat_interp_untuple' (T:=Tbase TZ) u)
- (flat_interp_untuple' (T:=Tbase TZ) v)
+ (flat_interp_untuple (T:=Tbase TZ) u)
+ (flat_interp_untuple (T:=Tbase TZ) v)
<-> (Tuple.map (proj _) u = v).
Proof.
+ destruct n as [|n]; [ destruct_head_hnf' unit; simpl; tauto | ].
induction n; [ reflexivity | ].
destruct_head_hnf' prod.
simpl @Tuple.tuple.
@@ -222,27 +226,27 @@ Lemma related_tuples_proj_eq_rel_tuple
: interp_flat_type_rel_pointwise2
(fun t => proj_eq_rel (proj t))
u v
- <-> (Tuple.map (proj _) (flat_interp_tuple (n:=S n) (T:=Tbase TZ) u)
+ <-> (Tuple.map (proj _) (flat_interp_tuple (n:=n) (T:=Tbase TZ) u)
= flat_interp_tuple (T:=Tbase TZ) v).
Proof.
- rewrite <- related_tuples_proj_eq_rel_untuple, !flat_interp_untuple'_tuple; reflexivity.
+ rewrite <- related_tuples_proj_eq_rel_untuple, !flat_interp_untuple_tuple; reflexivity.
Qed.
Local Arguments LiftOption.lift_relation2 _ _ _ _ !_ !_ / .
-Lemma related_tuples_lift_relation2_untuple'
+Lemma related_tuples_lift_relation2_untuple
n T U
(R : T -> U -> Prop)
(t : option (Tuple.tuple T (S n)))
(u : option (Tuple.tuple U (S n)))
: interp_flat_type_rel_pointwise2
(LiftOption.lift_relation2 R)
- (flat_interp_untuple' (T:=Tbase TZ) (Tuple.push_option t))
- (flat_interp_untuple' (T:=Tbase TZ) (Tuple.push_option u))
+ (flat_interp_untuple (T:=Tbase TZ) (Tuple.push_option t))
+ (flat_interp_untuple (T:=Tbase TZ) (Tuple.push_option u))
<-> LiftOption.lift_relation2
(interp_flat_type_rel_pointwise2 (fun _ => R))
TZ
- (option_map (flat_interp_untuple' (interp_base_type:=fun _ => T) (T:=Tbase TZ)) t)
- (option_map (flat_interp_untuple' (interp_base_type:=fun _ => U) (T:=Tbase TZ)) u).
+ (option_map (flat_interp_untuple (interp_base_type:=fun _ => T) (T:=Tbase TZ)) t)
+ (option_map (flat_interp_untuple (interp_base_type:=fun _ => U) (T:=Tbase TZ)) u).
Proof.
induction n.
{ destruct_head' option; reflexivity. }
@@ -255,7 +259,7 @@ Proof.
try (simpl @interp_flat_type_rel_pointwise2; tauto). }
Qed.
-Lemma related_tuples_lift_relation2_untuple'_ext
+Lemma related_tuples_lift_relation2_untuple_ext
{n T U}
{R : T -> U -> Prop}
{t u}
@@ -267,8 +271,8 @@ Lemma related_tuples_lift_relation2_untuple'_ext
<-> LiftOption.lift_relation2
(interp_flat_type_rel_pointwise2 (fun _ => R))
TZ
- (option_map (flat_interp_untuple' (interp_base_type:=fun _ => T) (T:=Tbase TZ)) (Tuple.lift_option (flat_interp_tuple (T:=Tbase TZ) t)))
- (option_map (flat_interp_untuple' (interp_base_type:=fun _ => U) (T:=Tbase TZ)) (Tuple.lift_option (flat_interp_tuple (T:=Tbase TZ) u))).
+ (option_map (flat_interp_untuple (interp_base_type:=fun _ => T) (T:=Tbase TZ)) (Tuple.lift_option (flat_interp_tuple (T:=Tbase TZ) t)))
+ (option_map (flat_interp_untuple (interp_base_type:=fun _ => U) (T:=Tbase TZ)) (Tuple.lift_option (flat_interp_tuple (T:=Tbase TZ) u))).
Proof.
induction n.
{ destruct_head_hnf' option; reflexivity. }
@@ -293,22 +297,22 @@ Proof.
| progress break_match ] ]. }
Qed.
-Lemma lift_option_flat_interp_tuple'
+Lemma lift_option_flat_interp_tuple
{n T x y}
- : (Tuple.lift_option (n:=S n) (A:=T) (flat_interp_tuple' (interp_base_type:=LiftOption.interp_base_type' _) (T:=Tbase TZ) x) = Some y)
- <-> (x = flat_interp_untuple' (T:=Tbase TZ) (n:=n) (Tuple.push_option (n:=S n) (Some y))).
+ : (Tuple.lift_option (n:=S n) (A:=T) (flat_interp_tuple (interp_base_type:=LiftOption.interp_base_type' _) (T:=Tbase TZ) x) = Some y)
+ <-> (x = flat_interp_untuple (T:=Tbase TZ) (n:=S n) (Tuple.push_option (n:=S n) (Some y))).
Proof.
rewrite Tuple.push_lift_option; generalize (Tuple.push_option (Some y)); intro.
split; intro; subst;
- rewrite ?flat_interp_tuple'_untuple', ?flat_interp_untuple'_tuple';
+ rewrite ?flat_interp_tuple_untuple, ?flat_interp_untuple_tuple;
reflexivity.
Qed.
Lemma lift_option_None_interp_flat_type_rel_pointwise2_1
T U n R x y
(H : interp_flat_type_rel_pointwise2 (LiftOption.lift_relation2 R) x y)
- (HNone : Tuple.lift_option (A:=T) (n:=S n) (flat_interp_tuple' (T:=Tbase TZ) (n:=n) x) = None)
- : Tuple.lift_option (A:=U) (n:=S n) (flat_interp_tuple' (T:=Tbase TZ) (n:=n) y) = None.
+ (HNone : Tuple.lift_option (A:=T) (n:=S n) (flat_interp_tuple (T:=Tbase TZ) (n:=S n) x) = None)
+ : Tuple.lift_option (A:=U) (n:=S n) (flat_interp_tuple (T:=Tbase TZ) (n:=S n) y) = None.
Proof.
induction n; [ | specialize (IHn (fst x) (fst y) (proj1 H)) ];
repeat first [ progress destruct_head_hnf' False
@@ -328,12 +332,18 @@ Local Arguments LiftOption.lift_relation _ _ _ _ !_ _ / .
Local Arguments LiftOption.of' _ _ !_ / .
Local Arguments BoundedWordW.BoundedWordToBounds !_ / .
+Local Ltac unfold_related_const :=
+ intros; hnf; simpl;
+ unfold related_wordW, LiftOption.lift_relation, LiftOption.of', BoundedWordW.wordWToBoundedWord, BoundedWordW.SmartBuildBoundedWord, BoundedWordW.of_Z, BoundedWordW.of_wordW, BoundedWordW.wordWToBoundedWord;
+ simpl.
+
Lemma related_wordW_op : related_op related_wordW (@BoundedWordW.interp_op) (@WordW.interp_op).
Proof.
(let op := fresh in intros ?? op; destruct op; simpl);
try first [ apply related_wordW_t_map1
| apply related_wordW_t_map2
- | apply related_wordW_t_map4 ].
+ | apply related_wordW_t_map4
+ | unfold_related_const; break_innermost_match; reflexivity ].
Qed.
Lemma related_bounds_t_map1 opW opB pf
@@ -383,9 +393,25 @@ Local Arguments Tuple.map : simpl never.
Local Arguments Tuple.map2 : simpl never.
Local Arguments ZBounds.SmartBuildBounds _ _ / .
+
+Local Ltac related_const_op_t :=
+ unfold_related_const; break_innermost_match; try reflexivity; hnf; simpl;
+ repeat match goal with
+ | [ H : andb _ _ = true |- _ ] => apply andb_prop in H
+ | _ => progress destruct_head' and
+ | _ => progress Z.ltb_to_lt
+ | _ => rewrite WordW.wordWToZ_ZToWordW by (simpl @Z.of_nat; omega)
+ | [ H : _ |- _ ] => rewrite WordW.wordWToZ_ZToWordW in H by (simpl @Z.of_nat; omega)
+ | [ H : (Z.log2 ?x < ?y)%Z |- _ ]
+ => unique assert (x < 2^y)%Z by (apply WordW.log2_lt_pow2_alt_proj_r2l; omega)
+ | _ => reflexivity
+ | _ => omega
+ end.
+
Lemma related_bounds_op : related_op related_bounds (@BoundedWordW.interp_op) (@ZBounds.interp_op).
Proof.
let op := fresh in intros ?? op; destruct op; simpl.
+ { related_const_op_t. }
{ apply related_bounds_t_map2; intros; destruct_head' option; reflexivity. }
{ apply related_bounds_t_map2; intros; destruct_head' option; reflexivity. }
{ apply related_bounds_t_map2; intros; destruct_head' option; reflexivity. }
@@ -515,6 +541,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.
+ { related_const_op_t. }
{ apply related_Z_t_map2; related_Z_op_fin_t. }
{ apply related_Z_t_map2; related_Z_op_fin_t. }
{ apply related_Z_t_map2; related_Z_op_fin_t. }
diff --git a/src/Reflection/Z/Interpretations64/RelationsCombinations.v b/src/Reflection/Z/Interpretations64/RelationsCombinations.v
index ecb65591b..8777cd7ed 100644
--- a/src/Reflection/Z/Interpretations64/RelationsCombinations.v
+++ b/src/Reflection/Z/Interpretations64/RelationsCombinations.v
@@ -1,6 +1,7 @@
Require Import Coq.ZArith.ZArith.
Require Import Crypto.Reflection.Z.Syntax.
Require Import Crypto.Reflection.Syntax.
+Require Import Crypto.Reflection.Relations.
Require Import Crypto.Reflection.Application.
Require Import Crypto.Reflection.Z.InterpretationsGen.
Require Import Crypto.Reflection.Z.Interpretations64.
@@ -72,7 +73,8 @@ Module Relations.
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; [ solve [ trivial | reflexivity ] | ].
+ { 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 *.
@@ -122,7 +124,8 @@ Module Relations.
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; [ solve [ trivial | reflexivity ] | ].
+ { 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 *.
@@ -181,7 +184,8 @@ Module Relations.
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; [ solve [ trivial | reflexivity ] | ].
+ { 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 *.
@@ -247,7 +251,7 @@ Module Relations.
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.
+ { 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. }
@@ -318,7 +322,7 @@ Module Relations.
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.
+ { 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. }
diff --git a/src/Reflection/Z/InterpretationsGen.v b/src/Reflection/Z/InterpretationsGen.v
index c24506cc1..3b403acc8 100644
--- a/src/Reflection/Z/InterpretationsGen.v
+++ b/src/Reflection/Z/InterpretationsGen.v
@@ -61,6 +61,7 @@ Module InterpretationsGen (Bit : BitSize).
base_type
interp_base_type' interp_flat_type
(fun t => match t with TZ => fun x => x end)
+ (Some tt)
(fun _ _ x y => match x, y with
| Some x', Some y' => Some (x', y')
| _, _ => None
@@ -70,6 +71,7 @@ Module InterpretationsGen (Bit : BitSize).
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
+ | Unit => fun _ => tt
| Prod A B => fun x => (@to' A (option_map (@fst _ _) x),
@to' B (option_map (@snd _ _) x))
end.
@@ -268,6 +270,7 @@ 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
@@ -415,6 +418,7 @@ Module InterpretationsGen (Bit : BitSize).
:= LiftOption.interp_base_type' bounds ty.
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
@@ -520,6 +524,11 @@ Module InterpretationsGen (Bit : BitSize).
| TZ => to_bounds'
end.
+ Definition SmartBuildBoundedWord (v : Z) : t
+ := if ((0 <=? v) && (Z.log2 v <? WordW.bit_width))%Z%bool
+ then of_Z TZ v
+ else None.
+
Definition t_map1
(opW : WordW.wordW -> WordW.wordW)
(opB : ZBounds.t -> ZBounds.t)
@@ -794,6 +803,7 @@ 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
diff --git a/src/Reflection/Z/Reify.v b/src/Reflection/Z/Reify.v
index 1b6dc3bef..111cf34d2 100644
--- a/src/Reflection/Z/Reify.v
+++ b/src/Reflection/Z/Reify.v
@@ -33,14 +33,15 @@ Ltac base_reify_type T ::=
end.
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 e in
- constr:((*Inline _*) ((*CSE _*) (InlineConst (Linearize v)))).
+ 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 :=
fun _
- => lazymatch goal with
- | [ |- Syntax.interp_type_gen_rel_pointwise _ (@Syntax.Interp ?base_type_code ?interp_base_type ?op ?interp_op ?t (InlineConst (Linearize _))) _ ]
+ => intros;
+ lazymatch goal with
+ | [ |- ?R (@Syntax.Interp ?base_type_code ?interp_base_type ?op ?interp_op ?t (InlineConst ?is_const (Linearize _))) _ ]
=> etransitivity;
- [ apply (@Interp_InlineConst base_type_code interp_base_type op interp_op t);
+ [ apply (@Interp_InlineConst base_type_code interp_base_type op interp_op is_const t);
reflect_Wf base_type_eq_semidec_is_dec op_beq_bl
| etransitivity;
[ apply (@Interp_Linearize base_type_code interp_base_type op interp_op t)
diff --git a/src/Reflection/Z/Syntax.v b/src/Reflection/Z/Syntax.v
index ea867d024..311ceb53a 100644
--- a/src/Reflection/Z/Syntax.v
+++ b/src/Reflection/Z/Syntax.v
@@ -30,6 +30,7 @@ Local Notation eta3 x := (eta (fst x), snd x).
Local Notation eta4 x := (eta3 (fst x), snd x).
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
@@ -41,8 +42,14 @@ Inductive op : flat_type base_type -> flat_type base_type -> Type :=
| Cmovne : op (tZ * tZ * tZ * tZ) tZ
| Cmovle : op (tZ * tZ * tZ * tZ) tZ.
+Definition make_const t : interp_base_type t -> op Unit (Syntax.Tbase t)
+ := match t with TZ => OpConst end.
+Definition is_const s d (v : op s d) : bool
+ := match v with OpConst _ => true | _ => false end.
+
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
@@ -67,6 +74,8 @@ Qed.
Definition op_beq_hetero {t1 tR t1' tR'} (f : op t1 tR) (g : op t1' tR') : reified_Prop
:= match f, g return bool with
+ | OpConst v, OpConst v' => Z.eqb v v'
+ | OpConst _, _ => false
| Add, Add => true
| Add, _ => false
| Sub, Sub => true
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-06 09:08:48 +0000