diff options
| author |  Jason Gross <jgross@mit.edu> | 2017-06-15 18:17:57 -0400 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2017-06-15 18:17:57 -0400 |
| commit | 4c29a88db8c65e2e5450a662eb793fcac62ddb5d (patch) | |
| tree | 955de3e1361384ec57cbbccd8a1dadabce5e909d | |
| parent | 63d4185fd06c3ead20c69e80f2a0d856d51ebc75 (diff) | |
Show the bounds going wrong in karatsuba
| -rw-r--r-- | src/Specific/IntegrationTestKaratsubaMul.v | 20 |
1 files changed, 10 insertions, 10 deletions
diff --git a/src/Specific/IntegrationTestKaratsubaMul.v b/src/Specific/IntegrationTestKaratsubaMul.v index 08cd21936..444c0746b 100644 --- a/src/Specific/IntegrationTestKaratsubaMul.v +++ b/src/Specific/IntegrationTestKaratsubaMul.v @@ -63,16 +63,6 @@ Section BoundedField25p5. apply (fun f => proj2_sig_map (fun THIS_NAME_MUST_NOT_BE_UNDERSCORE_TO_WORK_AROUND_CONSTR_MATCHING_ANAOMLIES___BUT_NOTE_THAT_IF_THIS_NAME_IS_LOWERCASE_A___THEN_REIFICATION_STACK_OVERFLOWS___AND_I_HAVE_NO_IDEA_WHATS_GOING_ON p => f_equal f p)). (* jgross start here! *) (*Set Ltac Profiling.*) - (*Open Scope zrange_scope. - assert (Interpretation.Bounds.is_tighter_thanb - (T:=Syntax.tuple (Syntax.Tbase Syntax.TZ) 8) - (r[0 ~> 72057594037927935]%zrange, r[0 ~> 72057594037927935]%zrange, r[0 ~> 72057594037927935]%zrange, - r[0 ~> 102363547501837588311535505879802992345435751778060049012811372691468]%zrange, r[0 ~> 72057594037927935]%zrange, - r[0 ~> 19714502134749424271321677013450763]%zrange, r[0 ~> 72057594037927935]%zrange, r[0 ~> 72057594037927935]%zrange) - (r[0 ~> 81064793292668928]%zrange, r[0 ~> 81064793292668928]%zrange, r[0 ~> 81064793292668928]%zrange, - r[0 ~> 81064793292668928]%zrange, r[0 ~> 81064793292668928]%zrange, r[0 ~> 81064793292668928]%zrange, - r[0 ~> 81064793292668928]%zrange, r[0 ~> 81064793292668928]%zrange) = true). - cbv [Interpretation.Bounds.is_tighter_thanb Relations.interp_flat_type_relb_pointwise Relations.interp_flat_type_rel_pointwise_gen_Prop Syntax.tuple Syntax.tuple' fst snd].*) Ltac ReflectiveTactics.solve_side_conditions ::= idtac. Time refine_reflectively. Import ReflectiveTactics. @@ -97,6 +87,16 @@ Section BoundedField25p5. Unshelve. all:shelve_unifiable. cbv [Interpretation.Bounds.is_tighter_thanb Relations.interp_flat_type_relb_pointwise Relations.interp_flat_type_rel_pointwise_gen_Prop Syntax.tuple Syntax.tuple' fst snd codomain bounds Interpretation.Bounds.is_tighter_thanb']. + Show. + (* + assert (((r[0 ~> 72057594037927935] <=? r[0 ~> 81064793292668928])%zrange && + (r[0 ~> 72057594037927935] <=? r[0 ~> 81064793292668928])%zrange && + (r[0 ~> 72057594037927935] <=? r[0 ~> 81064793292668928])%zrange && + (r[0 ~> 1166432303488958480] <=? r[0 ~> 81064793292668928])%zrange && + (r[0 ~> 72057594037927935] <=? r[0 ~> 81064793292668928])%zrange && + (r[0 ~> 72057594037927936] <=? r[0 ~> 81064793292668928])%zrange && + (r[0 ~> 72057594037927935] <=? r[0 ~> 81064793292668928])%zrange && + (r[0 ~> 72057594037927935] <=? r[0 ~> 81064793292668928])%zrange)%bool = true). *) (*Show Ltac Profile.*) Time Admitted. |