The Coq mailing list

[Petar Maksimovic <petar.maksimovic AT gmail.com>]

Good morning/afternoon/evening everyone,

I have a question about Coq handles type checking of apply-with-in. If we take a simple script:

Require Import List.

Definition is_empty (l : list nat) :=
match l with
 | nil => True
 | _ => False
end.

Lemma foo : forall (A : list nat),
  ~ is_empty nil -> is_empty A.
Proof. simpl. intuition. Qed.

Goal (~ is_empty nil -> True).
  intros H.
  apply foo with (A := False) in H. (***)
  auto.
Qed.

we can notice that, apparently, I am allowed to instantiate A with anything at point (***) in the proof, and this behaviour seems somewhat unexpected to me. Of course, the Qed doesn't allow the proof to be finalized in the end, and if I wanted to, I couldn't really do anything meaningful with H.

Is this a bug, a feature, something else?

As for the context, I stumbled upon this accidentally, as part of a bigger development, by mistyping the argument of 'with', and was later stuck for a while trying to understand why I couldn't proceed further. The example here is a minimal illustrative example.

Thank you,

Petar