The Coq mailing list

[Samuel Gruetter <gruetter AT mit.edu>]

I'd like to have the same in bedrock2! I didn't try anything zip-with-index related yet, but we have a notation for separation logic equivalences, which prints (P1 * P2 * ... Pn <==> Q1 * Q2 * ... * Qn) as

[P1; P2; ... Pn]

=== seps iff ===

[Q1; Q2; ... Qn]

https://github.com/mit-plv/bedrock2/blob/ce3f6ee55351d89e0c5091a4e5af98b3ae778dae/bedrock2/src/Map/SeparationLogic.v#L218

which is probably similar to what you already have.

Another ingredient you'd need would be to print each element of a list on a new line. I haven't managed to do this within a notation for lists, but instead I had to insert a newline for each possible element of the list, see here:

https://github.com/mit-plv/riscv-coq/blob/ab9adb6ce5c104886a3a435d16b0cd78c7d1a64f/src/Utility/InstructionNotations.v

Please let us know if you make progress on this :)

On Sat, 2019-06-15 at 15:28 -0400, Joshua Gancher wrote:

Hi all,

I am mechanizing a program logic, and have an equivalence judgement (written as an Inductive) of the form Equiv xs xs', where xs and xs' are of the type list Cmd. 

My current way of displaying this goal looks something like [:: p1; p2; p3; p4] <~~> [:: p5; p6; p7] (using ssreflect's notation for lists.) I would like to instead display something like:

0 : p1;

1 : p2;

2 : p3;

4 : p4

<~~>

0 : p5;

1 : p6;

2 : p7.

Is there a simple programmatic way of doing this, akin to defining a pprint_equiv : forall xs xs', Equiv xs xs' -> string? I think I could also achieve this by zipping each list with an increasing sequence of nats, and doing something special with this list of pairs, but this seems overkill if there is a more natural solution.

Thanks,

Joshua