coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- 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.
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.
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- [Coq-Club] Type checking in apply-with-in, Petar Maksimovic, 01/23/2014
- Re: [Coq-Club] Type checking in apply-with-in, Pierre-Marie Pédrot, 01/23/2014
- Re: [Coq-Club] Type checking in apply-with-in, Pierre-Marie Pédrot, 01/23/2014
- Re: [Coq-Club] Type checking in apply-with-in, Petar Maksimovic, 01/23/2014
- Re: [Coq-Club] Type checking in apply-with-in, Pierre-Marie Pédrot, 01/23/2014
- Re: [Coq-Club] Type checking in apply-with-in, Pierre-Marie Pédrot, 01/23/2014
Archive powered by MHonArc 2.6.18.