The Coq mailing list

[Tej Chajed <tchajed AT mit.edu>]

One alternative is to use the list itself to get a default instance of A:

• destruct l into either nil or a :: l'
• Prove your theorem without using the lemma for l = nil; if this isn't possible, then you probably really do need an (a: A) to make the theorem true
• In the other destruct case, you can apply your lemma with (a := a) and (l := a :: l')

-Tej

On Mon, Jul 13, 2015 at 4:09 AM Soegtrop, Michael <michael.soegtrop AT intel.com> wrote:

Dear George,

 

I would think there is no way to do this. Your lemma “forall (a: A) (l: list A), <conclusion>” says “if you have an A and a list of A, I give you the conclusion”. No A, no conclusion.

 

Coq has no way to conjure instances of arbitrary types out of thin air. Type includes Prop, so if you could create instances of arbitrary types, you could create proofs of arbitrary propositions. It is obvious that Coq cannot allow such a mechanism.

 

One solution is to restrict your type to something where you know an instance exists. You can use the type class mechanism to express this as follows:

 

Class HasInst (A : Type) :=

{

  inst : A

}.

 

Instance nat_HasInst : HasInst nat := { inst := 0 }.

Instance bool_HasInst : HasInst bool := { inst := false }.

 

Lemma HasInst_HasInst: forall {A : Type} (a : HasInst A), A.

Proof.

  intros A HIA.

  apply inst.

Qed.

 

The type class HasInst describes a type for which you know that there is some default instance. For all types for which you want to use your lemma, you need to provide this instance as shown above for bool and nat. The Lemma shows that indeed each “HasInst A” has an instance of A.

 

Putting A into {} makes it an implicit argument. Since it can be concluded from HasInst A what A is, it is not required to specify A.

 

Best regards,

 

Michael

 

From: coq-club-request AT inria.fr [mailto:coq-club-request AT inria.fr] On Behalf Of George Van Treeck
Sent: Saturday, July 11, 2015 6:38 PM
To: Coq Club
Subject: [Coq-Club] More elegant work-around for A as goal

 

I have a "Variable A : Type." and a lemma that uses "forall (a: A) (l: list A),...". When I apply that lemma it to another lemma, which only uses "forall (l: list A),...", then Coq leaves a final goal of "A" that I can't clear.

 

I can work around this problem by adding the variable, "(a:A)", to use assumption to clear the "A" goal. But, it's an ugly hack because the variable, a, isn't actually used in the lemma. Is there a more elegant way to clear the goal "A"? I'm using Coq versioin 8.4p16.

 

-George

Intel Deutschland GmbH
Registered Address: Am Campeon 10-12, 85579 Neubiberg, Germany
Tel: +49 89 99 8853-0, www.intel.de
Managing Directors: Christin Eisenschmid, Prof. Dr. Hermann Eul
Chairperson of the Supervisory Board: Tiffany Doon Silva
Registered Office: Munich
Commercial Register: Amtsgericht Muenchen HRB 186928