Skip to Content.
Sympa Menu

coq-club - [Coq-Club] Type checking in apply-with-in

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Type checking in apply-with-in


Chronological Thread 
  • From: Petar Maksimovic <petar.maksimovic AT gmail.com>
  • To: coq-club AT inria.fr
  • Subject: [Coq-Club] Type checking in apply-with-in
  • Date: Thu, 23 Jan 2014 14:53:49 +0100

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



Archive powered by MHonArc 2.6.18.

Top of Page