The Coq mailing list

[Joshua Gancher <jrg358 AT cornell.edu>]

I was not aware of the ability to insert newlines in format clauses; I similarly have a notation for every statement in my language, so I ended up doing something very similar to what Samuel did in bedrock2. Thanks so much!

Josh

On Fri, Jun 21, 2019 at 1:20 PM Ralf Jung <jung AT mpi-sws.org> wrote:

Hi,

On 21.06.19 18:52, Samuel Gruetter wrote:
> 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

We are doing something like "one element of a list per line" in the Iris /
Separation Logic Proof Mode, you can find the Notation for that at
<https://gitlab.mpi-sws.org/iris/iris/blob/472aa3bcb129182fd6fc9aca241a38340c9ceafd/theories/proofmode/notation.v>.
Basically, you can add the newline to the notation for "cons".

We don't have line numbers, though.

Kind regards,
Ralf

>
> 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
>>
>>

--
Website: https://people.mpi-sws.org/~jung/