coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: AUGER Cedric <Cedric.Auger AT lri.fr>
- To: Andreas Abel <andreas.abel AT ifi.lmu.de>
- Cc: Vladimir Voevodsky <vladimir AT ias.edu>, Coq-Club Club <coq-club AT inria.fr>
- Subject: Re: [Coq-Club] inductive-coinductive ??
- Date: Mon, 27 Jun 2011 13:33:14 +0200
Le Mon, 27 Jun 2011 11:14:09 +0200,
Andreas Abel
<andreas.abel AT ifi.lmu.de>
a écrit :
> Hello Vladimir,
>
> does this serve your purpose?
>
> Variable A : Type.
> Variable a : A.
>
> CoInductive Stream (P : A -> Prop) : Type :=
> cons : forall
> (head : { x : A | P x } -> A)
> (tail : Stream (fun x => forall (p : P x),
> head (exist (fun x => P x) x p) = a)),
> Stream P.
>
> Definition VS := Stream (fun x => True).
>
> Cheers,
> Andreas
>
> On 27.06.11 2:30 AM, Vladimir Voevodsky wrote:
> > Is there a way to define in Coq the type which can be informally
> > described as follows:
> >
> > 1. Given parameters A : Type , a : A .
> >
> > 2. I want to define the type of (infinite) sequences f_0 ,..., f_n,
> > .... where
> >
> > 2a. f_0 : A -> A .
> >
> > 2b. f_{S n} : {| x : A ; f_n x = a |} -> A .
> >
> > Is there a way to define the type of such sequences ?
> >
>
Here are 2 variants of Andreas solution
(the first one is just defining a separate type for the contents of
a stream).
Section Refinement.
Variable A: Type.
Variable a: A.
Record item (current_restriction: A -> Prop): Type := {
current_function: forall x, current_restriction x -> A;
next_restriction := fun x => exists h, current_function x h = a
}.
CoInductive Refinement: (A->Prop) -> Type :=
Next: forall current_restriction (f: item current_restriction),
Refinement f.(next_restriction current_restriction) ->
Refinement current_restriction.
End Refinement.
Section Refinement2.
Variable A: Type.
Variable a: A.
Record item2 (current_restriction: A -> Prop): Type := {
current_function2: forall x, A+(~current_restriction x);
next_restriction2 :=
fun x => current_function2 x = inl (~current_restriction x) a
}.
CoInductive Refinement2: (A->Prop) -> Type :=
Next2: forall current_restriction (f: item2 current_restriction),
Refinement2 f.(next_restriction2 current_restriction) ->
Refinement2 current_restriction.
End Refinement2.
The second variant may not be as convenient, but using it, you won't
have to worry about the use of a proof_irrelevance axiom.
That is in the environment:
P: A -> Prop
f_n: {x|P A} -> A
x: A
Hx1: P x
Hx2: P x
b: A
Hb: f_n (ex_intro _ x Hx1) = b
c: A
Hc: f_n (ex_intro _ x Hx2) = c
===============================
b = c
is not axiom free provable.
But in the second variant,
P: A -> Prop
f_n: forall x:A, A+(~P x)
x: A
Hx1: P x
Hx2: P x
b: A
Hb: f_n x = left (~P x) b
c: A
Hc: f_n x = left (~P x) c
===============================
b = c
is axiom free provable
- [Coq-Club] inductive-coinductive ??, Vladimir Voevodsky
- Re: [Coq-Club] inductive-coinductive ??,
Andreas Abel
- Re: [Coq-Club] inductive-coinductive ??, Vladimir Voevodsky
- Re: [Coq-Club] inductive-coinductive ??, AUGER Cedric
- Re: [Coq-Club] inductive-coinductive ??, AUGER Cedric
- <Possible follow-ups>
- Re: [Coq-Club] inductive-coinductive ??, Paolo Herms
- Re: [Coq-Club] inductive-coinductive ??,
Andreas Abel
Archive powered by MhonArc 2.6.16.