The Coq mailing list

[Vadim Zaliva <vzaliva AT cmu.edu>]

Amin & Cedric,

Thank you for your suggestions. One thing I realized that I do need to stay away from equality proofs.

That laves me with two approaches:

1. Cedirc’s: "Inductive Vop (A : Type) : nat -> nat -> Type :=…" (with no equalities).

2. Amir’s: Intermediate Vop_i and Vop_o types

Without actually trying to do some more proofs using either it is hard for me to judge which one is better.

Any comments how these two compare?

Are proof complications caused by destructing (a+b) in the context where (a) alone is also used in approach #1 not likely to happen in #2?

Presently #2 looks like a very neat use of type system to express underlying nature of dependencies (from “i” to “o” or vice

versa). In this way it is very appealing to me. I wish I can hide little bit of this internal machinery (VI and VO) so I can have a more direct operator representation in expressions. Maybe I can use some syntax sugar to hide these?

I am going to experiment with both approaches for now, but if there any comments on pros and cons of these two I would love to hear them.

And thanks again for your answers!

Sincerely,
Vadim Zaliva