WIP: Type-level Quantifiers

Closes #4 (closed)

added 27 commits

• ce488288...8f62d513 - 24 commits from branch master
• 59c42dce - Merged quantification over types and session types in types
• 94f93b00 - WIP Quantifiers over types and session types in session types
• 9bd6b777 - Removed merge conflict artifact

Compare with previous version

added 1 commit

• 94b64617 - Bumped unification of send/receive

Compare with previous version

added 6 commits

• 176ff8bb - 1 commit from branch master
• 434eff26 - Merged quantification over types and session types in types
• 6b126a60 - WIP Quantifiers over types and session types in session types
• a19b80d5 - Removed merge conflict artifact
• 6bac37c7 - Bumped unification of send/receive
• 48cfcccc - Added proper instance of quantifier versions of message

Compare with previous version

added 11 commits

• 48cfcccc...25f6a014 - 6 commits from branch master
• 9a39d86e - Merged quantification over types and session types in types
• 36cff754 - WIP Quantifiers over types and session types in session types
• a48c2717 - Removed merge conflict artifact
• 2805f79c - Bumped unification of send/receive
• a72780c4 - Added proper instance of quantifier versions of message

Compare with previous version

added 6 commits

• c801fc33 - 1 commit from branch master
• e5e97e25 - Merged quantification over types and session types in types
• fe088bd9 - WIP Quantifiers over types and session types in session types
• beb1a7d1 - Removed merge conflict artifact
• 5952cdc7 - Bumped unification of send/receive
• be39c04a - Added proper instance of quantifier versions of message

Compare with previous version

@jihgfee You wanted feedback on this, but it seems a notation fails. Is that the problem?

The tactics fail because the "coercion" from tytele_app _ to its value does not happen. Specifically this problem occurs at line 215.

Line 227 fails, but I am unsure if it is the same reason behind it.

I get the following error:

COQC theories/logrel/types.v
File "./theories/logrel/types.v", line 656, characters 41-42:
Error:
Syntax error: ',' 'TY' expected after [constr:open_binders] (in [constr:operconstr]).

The code is only expected to compile up until session_types.v (where the problem is shown via examples). types.v has not yet been ported

Can you give some more precise description of what's working and what's not. It's really hard for me to make sense of the problem of this MR, since it's just a bulk of code without instructions.

We discussed the next attempt at quantifiers as being overloading the notation of lty/lsty to be interp_kind lty_kind/lsty_kind. I did this.

The result of having done that is that the coercion works correctly when creating instances of lty/lsty, but that it fails when using the existing lemmas send_spec/recv_spec, as illustrated by the included examples at the end of session_types.v

The problem seems that it doesn't properly guess the evars. e.g. using wp_send on line 213 yields the goal:

  "HA" : A v
  --------------------------------------∗
  tytele_app A ?Goal v

This is resolved immediately with by instantiate (1:=TyTargO)., but it should happen automatically.

As for wp_recv it simply doesn't work at all.

But wait, this problem has nothing to do with kinded quantifiers, but it has to do with the use of telescopes. Maybe we should do these two things in sequence. So, first kinded quantifiers for types, and then add the whole telescope stuff to also have kinded quantifiers at the level of protocols.

closed