search

coq / coq

Coq is a formal proof management system. It provides a formal language to write mathematical definitions, executable algorithms and theorems together with an environment for semi-interactive development of machine-checked proofs.
https://coq.inria.fr/
GNU Lesser General Public License v2.1
4.84k stars 647 forks source link

Problem with the beautifier #8640

Open francoisthire opened 6 years ago

francoisthire commented 6 years ago

Version

The Coq Proof Assistant, version 8.8.1 (September 2018) compiled on Sep 24 2018 15:30:31 with OCaml 4.04.2

Operating system

Ubuntu 16.04.5 LTS

Description of the problem

On the following code (that is well-typed)

Module logic.

    Parameter eq : forall (A:Type), (A) -> (A) -> Prop.

    Axiom eq_ind : forall A, forall (x:A), forall (P:(A) -> Prop), P x -> forall (y:A), eq A x y -> P y.
End logic.

Running the command coqc -beautify gives me

Module logic.

    Parameter (eq : forall A : Type, A -> A -> Prop).

    Axiom
  (eq_ind :
     forall A (x : A) (P : A -> Prop), P x -> forall y : A, (A = x) y -> P y).
End logic.

That is clearly not well-typed. The problem is in the type of eq_ind where the constant eq is replaced by the inductive equality used in the standard library while it should not.

vbgl commented 6 years ago

Good catch.

May I ask, out of curiosity, in which context are you using the beautifier ?

There are two issues here: first eq gets an extra (anonymous) argument; second the notation for equality is reused.

francoisthire commented 6 years ago

May I ask, out of curiosity, in which context are you using the beautifier ?

These files are generated from the Logipedia project: http://logipedia.science . The printer we use for this project is very basic and I wanted to use the beautifier to enhance the output.