[IL Semantics] Meta-theory in rocq

[DCupello1]

This pull request is for tracking what is done on the IL meta-theory, while also keeping track of discussions on the subject in matter.

TODO:

• Port Syntax, Env and Subst in Rocq
  • Handle capture avoidance in Rocq
• Port Numerics using regularly used number types in rocq
  • Figure out how to convert reals to rationals.
• Port Reduction in Rocq
  • Handle Iter expressions
  • Matching
• Port typing in Rocq
  • Make subtyping into coinduction?
• (More to do)

[DCupello1]

@rossberg Had a question on the reduction rules.

For a reduction rule as such:

rule Step_exp/ACC-ctxt2:
  S |- ACC e p ~> ACC e p'
  -- Step_path: S |- p ~> p'

What is Step_path supposed to do? There does seem to be an rule for Step_path. But even if there was, it seems like the Step_exp is already doing the work of Step_path in the way of the ACC rules. As an example:

rule Step_exp/ACC-ROOT:
  S |- ACC e ROOT ~> e

rule Step_exp/ACC-THE:
  S |- ACC e (THE p) ~> e'
  -- Step_exp: S |- ACC e p ~> OPT e'

rule Step_exp/ACC-IDX:
  S |- ACC e (IDX p (NAT n)) ~> e'_n
  -- Step_exp: S |- ACC e p ~> LIST e'*
  -- if n < |e'*|
  -- if e'_n = e'*[n]

The same question extends to Step_iter and Step_exppull which also has no rules, though these might actually need something unlike Step_path.

[rossberg]

Oops, yeah, seems like I forgot to add the actual rules. Perhaps because they are boring: they should simply be the contextual rules for reducing inner expressions, such as indices in Step_path. (Anything beyond that that you think should happen in Step_iter and Step_exppull?)

Maybe there would be a warning when a relation has no rules. :)

[DCupello1]

Oops, yeah, seems like I forgot to add the actual rules. Perhaps because they are boring: they should simply be the contextual rules for reducing inner expressions, such as indices in Step_path. (Anything beyond that that you think should happen in Step_iter and Step_exppull?)

Maybe there would be a warning when a relation has no rules. :)

Ah alright, yeah I don't really see anything other than contextual rules either at the moment.

At least for translating to rocq, relations with no rules doesn't really pose a problem :) but it would be nice to at least warn the user as a sanity check.

[rossberg]

Pushed a fix.

[DCupello1]

@rossberg Had a question about SubE reduction.

Take this reduction rule:

rule Step_exp/SUB-STR:
  S |- SUB (STR (at `= e)*) (VAR x_1 a_1*) (VAR x_2 a_2*) ~> STR (at' `= SUB e t_1 t_2)*
  -- Expand_typ: S |- VAR x_1 a_1* => STRUCT tf_1*
  -- Expand_typ: S |- VAR x_2 a_2* => STRUCT tf_2*
  -- (if (at' `: t_1 `- `{q_1*} pr_1*) <- tf_1*)*
  -- (if (at' `: t_2 `- `{q_2*} pr_2*) = tf_2)*

What is the relation between at and at'?

And also what are we trying to achieve with this rule? Is it that, for each field in the StrE, we are ensuring it is in the type definition of the subtype, while also existing in the supertype? Are we trying to ensure that there are the same amount of fields in both type fields?

[rossberg]

@DCupello1, this is supposed to say that for every field at' in tf_2* (the super-type) there exists a field at' in tf_1* (the sub-type). We can then reduce a coercion over structure types to pointwise coercions over the (super-type's) fields. But it looks like I screwed up gathering the e's. I suppose it should rather be

rule Step_exp/SUB-STR:
  S |- SUB (STR ef*) (VAR x_1 a_1*) (VAR x_2 a_2*) ~> STR (at `= SUB e t_1 t_2)*
  -- Expand_typ: S |- VAR x_1 a_1* => STRUCT tf_1*
  -- Expand_typ: S |- VAR x_2 a_2* => STRUCT tf_2*
  -- (if (at `= e) <- ef*)*
  -- (if (at `: t_1 `- `{q_1*} pr_1*) <- tf_1*)*
  -- (if (at `: t_2 `- `{q_2*} pr_2*) = tf_2)*

Does that make more sense?

Thanks for catching!

[DCupello1]

Yes it does make more sense, thank you!

[rossberg]

Fixed upstream.