Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] A peculiar proof script

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] A peculiar proof script


chronological Thread 
  • From: Matthieu Sozeau <matthieu.sozeau AT gmail.com>
  • To: Victor Porton <porton AT narod.ru>
  • Cc: Coq <coq-club AT inria.fr>
  • Subject: Re: [Coq-Club] A peculiar proof script
  • Date: Mon, 14 Nov 2011 17:47:09 +0100

Hi Victor,

  maybe I can help? Let's forget about classes and see what happens under the 
hood.

<<<
Require Import Setoid. 
Hypothesis P: nat->Prop.
Hypothesis Q: nat->Prop.

Axiom Eq: forall x:nat, P(x)<->Q(x).

Record C := {
 num: nat;
 cond: P num
}.

Section sect.
 Hypothesis Other: forall obj:C, Q (num obj).

 Lemma C2 : C.
 Proof. apply Build_C with 0.
   rewrite Eq. apply Other.
>>>

This fails, as you have no object of type [C] with a [num] field
set to [0] already built. You're in the process of trying to build
one though.

Hope this helps,
-- Matthieu

Le 14 nov. 2011 à 17:05, Victor Porton a écrit :

> Please help me to replace an admission with an actual proof script in this 
> .v file. (It seems particularly difficult to specialize over an object 
> variable of type C. This is the part I haven't succeeded myself without 
> your help.)
> 
> [[[[
> Hypothesis P: nat->Prop.
> Hypothesis Q: nat->Prop.
> 
> Axiom Eq: forall x:nat, P(x)<->Q(x).
> 
> Class C := {
>  num: nat;
>  cond: P num
> }.
> 
> Section sect.
>  Hypothesis Other: forall obj:C, Q num.
> 
>  Instance C2: C := { num:=0 }.
>  Proof. generalize Other. admit. Save.
> End sect.
> 
> Axiom ax: forall obj:C, Q num.
> 
> Definition C3 := C2(ax).
> ]]]]
> 
> -- 
> Victor Porton - http://portonvictor.org





Archive powered by MhonArc 2.6.16.

Top of Page