search

math-comp / algebra-tactics

Ring, field, lra, nra, and psatz tactics for Mathematical Components
33 stars 2 forks source link

A performance issue with morphism detection #27

Closed pi8027 closed 2 years ago

pi8027 commented 3 years ago 
Goal forall (F : numFieldType),
let x : F := 2%:~R in
x * x * x * x * x * x * x * x * x * x * x * x * x * x * x * x * x * x * x * x *
x * x * x * x * x * x * x * x * x * x * x * x * x * x * x * x * x * x * x * x *
x * x * x * x * x * x * x * x * x * x * x * x * x * x * x * x * x * x * x * x *
x * x * x * x * x * x * x * x * x * x * x * x * x * x * x * x * x * x * x * x *
x * x * x * x * x * x * x * x * x * x * x * x * x * x * x * x * x * x * x * x *
x * x * x * x * x * x * x * x * x * x * x * x * x * x * x * x * x * x * x * x *
x * x * x * x * x * x * x * x * x * x * x * x * x * x * x * x * x * x * x * x *
x * x * x * x * x * x * x * x * x * x * x * x * x * x * x * x * x * x * x * x *
x * x * x * x * x * x * x * x * x * x * x * x * x * x * x * x * x * x * x * x *
x * x * x * x * x * x * x * x * x * x * x * x * x * x * x * x * x * x * x * x =
4%:~R ^+ 100.
Proof.
move=> F /=.
Time by field.
(*
Reification: 0.019452 sec.
Reflection: 0.197635 sec.
Finished transaction in 0.246 secs (0.246u,0.s) (successful)
*)
Qed.

Goal forall (F : numFieldType),
let x : F := ratr 2%:~R in (* ratr is a ring morphism *)
x * x * x * x * x * x * x * x * x * x * x * x * x * x * x * x * x * x * x * x *
x * x * x * x * x * x * x * x * x * x * x * x * x * x * x * x * x * x * x * x *
x * x * x * x * x * x * x * x * x * x * x * x * x * x * x * x * x * x * x * x *
x * x * x * x * x * x * x * x * x * x * x * x * x * x * x * x * x * x * x * x *
x * x * x * x * x * x * x * x * x * x * x * x * x * x * x * x * x * x * x * x *
x * x * x * x * x * x * x * x * x * x * x * x * x * x * x * x * x * x * x * x *
x * x * x * x * x * x * x * x * x * x * x * x * x * x * x * x * x * x * x * x *
x * x * x * x * x * x * x * x * x * x * x * x * x * x * x * x * x * x * x * x *
x * x * x * x * x * x * x * x * x * x * x * x * x * x * x * x * x * x * x * x *
x * x * x * x * x * x * x * x * x * x * x * x * x * x * x * x * x * x * x * x =
4%:~R ^+ 100.
Proof.
move=> F /=.
Time by field.
(*
Reification: 0.221024 sec.
Reflection: 0.251970 sec.
Finished transaction in 0.544 secs (0.544u,0.s) (successful)
*)
Qed.
pi8027 commented 3 years ago

~In the latter case, it rather seems to fail to recognize that ratr is a ring morphism :/~ Indeed, F should be a numFieldType.

Goal forall (F : fieldType), ratr 2%:~R = 2%:~R :> F.
Proof.
move=> F.
Fail field. (* Not a valid ring equation. *)
pi8027 commented 3 years ago

I happened to see another performance issue in the example above, which has been fixed in #29. The performance issue of morphism detection is not easy to fix. I attempted to do that by implementing a restricted version of canonical structure inference in Elpi and it does not improve anything.

pi8027 commented 2 years ago

I confirm that this performance issue has disappeared.