coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- 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
- [Coq-Club] A peculiar proof script, Victor Porton
- Re: [Coq-Club] A peculiar proof script,
Alexandre Pilkiewicz
- Re: [Coq-Club] A peculiar proof script,
Victor Porton
- Re: [Coq-Club] A peculiar proof script, Vincent Siles
- Re: [Coq-Club] A peculiar proof script, Alexandre Pilkiewicz
- Re: [Coq-Club] A peculiar proof script,
Victor Porton
- Re: [Coq-Club] A peculiar proof script, Matthieu Sozeau
- Re: [Coq-Club] A peculiar proof script,
Alexandre Pilkiewicz
Archive powered by MhonArc 2.6.16.