The Coq mailing list

[Ralf Jung <jung AT mpi-sws.org>]

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/