diff options
| author |  Jason Gross <jgross@mit.edu> | 2017-01-11 21:02:50 -0500 |
|---|---|---|
| committer |  Jason Gross <jasongross9@gmail.com> | 2017-03-01 11:45:47 -0500 |
| commit | 6b3048c37ad348dc88ecc03ef892ecfb121bfa7f (patch) | |
| tree | 351e5438c5664ab0caf08b9d5054f296ff4aa2ee /src/Reflection/Z/Interpretations128/Relations.v | |
| parent | 80dc66a34fbf031bfac1214ccbb3bb1dcdef3d39 (diff) | |
Switch to fully uncurried form for reflection
This will eventually make a number of proofs easier.
Unfortunately, the correctness lemmas for AddCoordinates and LadderStep
no longer work (because of different arities), and there's a proof in
Experiments/Ed25519 that I've admitted.
The correctness lemmas will be easy to re-add when we have a more
general version that handle arbitrary type shapes.
Diffstat (limited to 'src/Reflection/Z/Interpretations128/Relations.v')
| -rw-r--r-- | src/Reflection/Z/Interpretations128/Relations.v | 11 |
1 files changed, 7 insertions, 4 deletions
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. |