search

harp-project / AML-Formalization

GNU Lesser General Public License v2.1
10 stars 5 forks source link

Generic OPML models #413

Closed h0nzZik closed 12 months ago

h0nzZik commented 12 months ago

As per the discussion we had this morning and also https://github.com/harp-project/AML-Formalization/issues/383, I created some infrastructure for defining OPML models from components. I am quite satisfied with the Component record, which also contains a generic way of constructing and destructing elements that came from the particular component. There is also the example bool_component, There are also some very basic combinators for creating a new component: some for a "constant" component like Bools or Nats, and some for a combination of two components into one. However, here is something suspicious in the proof of the lemma paircomb_ucf_UnifiedCarrierFunctor_monotone, where it is enough if one component is monotone in order to prove that the generated component is monotone. Perhaps something is wrong with our definition of monotonicity?

h0nzZik commented 12 months ago

Now I am thinking that monotonicity should be more like (a -> b) -> (f a -> fb); what I have is extensivity.