Design of tyepclasses

• As noted in #136, we currently have instances of tyepclasses that take in nontypeclass parameters.
• Typeclass inference in Coq can not infer these instances.
• One of the currently approaches (as noted in #136) is to restate these instances at the top of the file.
• However, in some files such as https://prosa.mpi-sws.org/branches/master/pretty/prosa.results.rs.fp.fully_preemptive.html these definitions are not restated.
• In these files, one or more lemmas that are used (along with eauto) silently ties the results of the lemma to specific definitions of the typeclass instances.
• These is bad design in my opinion. Such proofs will become hard to maintain and change.
• The code is also not readable to developers.
• We need to find a better way of handling these tyepclass instances.
• In our concrete case, I don't think it make sense to put the nontypeclass parameters inside typeclasses.
• Then we can either make it a rule to state definitions with nontypeclass parameters fed at the top of file or explore using canonical instances instead of typeclasses

changed the description

Then we can either make it a rule to state definitions with nontypeclass parameters fed at the top of file or explore using canonical instances instead of typeclasses

Could you sketch the solution for (e.g.) instance rs_jlfp_interference in file rs.fp.fully_preemptive?

Sorry I forgot to reply. Yeah I will try to make an MR soon

I remember we talked about it at one point, but just to fix it somewhere.

Can we transform all typeclasses into typeclasses-records (like in !365)?

E.g.,

 Class MaxArrivals (Task : TaskType) := max_arrivals : Task -> duration -> nat.

becomes

 Class MaxArrivals (Task : TaskType) := { max_arrivals : Task -> duration -> nat }.

And then make sched and arr_seq typeclasses as well?

This change should solve at least this part and make automation a bit smarter (since now coq can derive parameters of typeclass instances)

As noted in #136, we currently have instances of tyepclasses that take in nontypeclass parameters.

!365 needs green CI

Making sched and arr_seq type classes would be a pretty invasive change that I am not too keen to consider at this point.