Claudio's question

[Artur Kornilowicz <arturk@math.uwb.edu.pl>]

Hi Claudio,

I do not know Coq, so I better explain the situation in Mizar.

The Iterative Equality in Mizar is a construction of the form

                tau_0 = tau_1 by rho_1           (*)
                     .= tau_2 by rho_2
                     .................
                     .= tau_k by rho_k;

where tau's are terms, and rho's are justifications (similar construction
is in (Mizar Mode in) HOL, even more general). The result of (*) is

                          tau_0 = tau_k;

rho_1 justifies the proposition tau_0 = tau_1 and
rho_(i+1) justifies the proposition tau_i = tau_(i+1).

RELITERS finds out if two steps can be done as a single step, i.e. if

                          tau_i = tau_(i+2)

can be justified by rho_i, rho_(i+1).

Then the error (#746) is reported. It means that the line

                       .= tau_(i+1) by rho_(i+1)

may be removed; after moving rho_(i+1) to the justification of the next
step.

I hope that this clarifies the matter.

Greetings
Artur Kornilowicz


On Fri, 19 Jan 2001, Claudio Sacerdoti Coen wrote:

>  Hello Artur,
>
>  I am a graduate student of the University of Bologna, member
>  of HELM project and currently on leaving at INRIA. One of my
>  interests is enhanching proofs
>  (i.e. lambda-terms) you get with the Coq proof-assistants.
>  One usual source of bad proofs are overkilling equalities, so
>  Hugo Herbelin pointed me to you and RELITERS.
>
>  I know that Mizar and Curry-Howard based proof-assistants are
>  somehow difficult to comfront, but can you briefly explain
>  me what is a ``superfluous step in iterative equalities'' in
>  Mizar? (In Coq it involves beta-delta-iota-let convertibility,
>  so it could be quite different)
>
>  			Thanks in advance,
> 			    C.S.C.
>
> --
> ----------------------------------------------------------------
> Real name: Claudio Sacerdoti Coen
> Graduate Computer Science Student at University of Bologna
> Now at INRIA (Sophia-Antipolis, France)
> E-mail: sacerdot@cs.unibo.it
> ----------------------------------------------------------------