The Coq mailing list

[Gregory Malecha <gmalecha AT eecs.harvard.edu>]

It seems like what you want to do is abstract over the term that you want. Would something like this work:

Section Abs.

  Variable A : nat -> Prop.

  Hypothesis First : A O = True.

  Class C := { x : nat ; a : A x }.

  Instance I : C := {x := O }.

  Proof. ... Admitted.

End Abs.

This would have the effect of producing the definitions:

Class C (A : nat -> Prop) := { x : nat ; a : A x }.

Instance I (A : nat -> Prop) (First : A O = True) := { x := O }.

Proof. 

  ...

Admitted.

where C and I are parameterized by A and First. Then something like: @I A First and @I B ... would give you different versions of I for the different types A and B.

On Sun, Nov 6, 2011 at 5:44 PM, Victor Porton <porton AT narod.ru> wrote:

Let we have some dependent structure. I want several instance proofs every of which requires a DIFFERENT but equivalent condition instead of a condition specified in the dependent structure.

How to refactor these several proofs to refer to the different condition instead of the condition specified in the definition of dependent structure?

An example to be clear:

[[[[
Parameter A: nat->Prop.
Parameter B: nat->Prop.

Axiom First: B O = True.

Axiom Second: B O <-> A O.

Class C := {
 x: nat;
 a: A x
}.

Instance I: C := { x:=O }.
Proof.
Admitted.
]]]]

Here I want to base the proof of I on the axiom First (that is on the condition B instead of the condition A which appears in the definition of the structure).

You may imagine that I want to prove it for several instances (in the script above we have only one instance I, for an example).

--
Victor Porton - http://portonvictor.org

--
gregory malecha

http://www.people.fas.harvard.edu/~gmalecha/