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

"intros []" fails, but "intros x; destruct x" works #7972

Open anton-trunov opened 6 years ago

anton-trunov commented 6 years ago

Version

8.8.0

Operating system

macOS 10.13.5

Description of the problem

The following snippet

Inductive foo : Set -> Type := Foo : foo unit.

Lemma bar U (pf : unit = U) : forall (x : foo U), x = eq_rect unit foo Foo U pf.
Proof.
  intros x; destruct x.  (* works *)
  Restart.
  Fail intros [].
Abort.

produces this error message:

Abstracting over the terms "U" and "x" leads to a term fun (U0 : Set) (x0 : foo U0) => x0 = eq_rect unit foo Foo U0 pf which is ill-typed. Reason is: Illegal application: The term "eq_rect" of type "forall (A : Type) (x : A) (P : A -> Type), P x -> forall y : A, x = y -> P y" cannot be applied to the terms "Set" : "Type" "unit" : "Set" "foo" : "Set -> Prop" "Foo" : "foo unit" "U0" : "Set" "pf" : "unit = U" The 6th term has type "unit = U" which should be coercible to "unit = U0".

herbelin commented 6 years ago

Well, the reference manual seems to say that intros [] works like destruct but internally this is wrong (i.e., internally, no generalization is done by [] over the indices like destruct would do). So, the implementation should probably rather indeed follow the reference manual.

Thanks a lot for the example.