search

affeldt-aist / infotheo

A Coq formalization of information theory and linear error-correcting codes
GNU Lesser General Public License v2.1
64 stars 15 forks source link

Boolean prob #45

Closed t6s closed 3 years ago

t6s commented 3 years ago

Resolves #43

~(based on PR #47)~ has been merged

@t6s

affeldt-aist commented 3 years ago

Two things:

t6s commented 3 years ago
  • it looks like the main change is to use (0 <b= p <b= 1)%R has the proof field for the prob structure, is this understanding correct? (one may wonder whether the lack of lra would be painful but since it is a proof inside a structure that should be ok)

Yes.

  • before merging this PR we should move out of monae and in infotheo the pieces of code that expose the prob structure (this change has indeed exposed that we were lacking modularity here, this should be fixed beforehand)

I did not understand this aspect very well. Can you show by example what sort of changes should be made?

affeldt-aist commented 3 years ago
  • before merging this PR we should move out of monae and in infotheo the pieces of code that expose the prob structure (this change has indeed exposed that we were lacking modularity here, this should be fixed beforehand)

I did not understand this aspect very well. Can you show by example what sort of changes should be made?

https://github.com/affeldt-aist/monae/pull/39/ already exposes where we reveal the Prob.mk constructor; since only the proof field of prob has changed we could have expected the change in infotheo to be more transparent.

I was also thinking of lemmas like https://github.com/affeldt-aist/monae/blob/702b0be30a9e71b22fa84a884fd93d754c5a32c8/proba_lib.v#L298 that ought to be in infotheo in the first place.

At first sight, you seem to point at a lack of modularity.

affeldt-aist commented 3 years ago

@t6s how about we merge this now so that it does not block you?

affeldt-aist commented 3 years ago

maybe mkP is not good because it looks like a view; mk_ -> mk, mk -> build is maybe better @t6s

t6s commented 3 years ago

maybe mkP is not good because it looks like a view; mk_ -> mk, mk -> build is maybe better @t6s

I would rather eliminate all uses of mk_. I partly did it in conv_set branch and it was not a big change.

affeldt-aist commented 3 years ago

I would rather eliminate all uses of mk_. I partly did it in conv_set branch and it was not a big change.

In the interest of time, what about rolling back to mk and make an issue to treat all mk's removal later once we have more material in master to evaluate it?

t6s commented 3 years ago

I would rather eliminate all uses of mk_. I partly did it in conv_set branch and it was not a big change.

In the interest of time, what about rolling back to mk and make an issue to treat all mk's removal later once we have more material in master to evaluate it?

No problem. Shall I file another PR to remove mk_?

affeldt-aist commented 3 years ago

No problem. Shall I file another PR to remove mk_?

No hurry. For the time being, an issue will do. I'll fill one once this PR is merged.