Skip to Content.
Sympa Menu

coq-club - Re: witness of existential

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: witness of existential


chronological Thread 
  • From: Benjamin Werner <werner>
  • To: denney AT irisa.fr (Ewen Denney)
  • Subject: Re: witness of existential
  • Date: Wed, 18 Aug 1999 16:07:17 +0200 (MET DST)


Yes. One tedious thing with having the computational/logical
distinction carried by the typing is that it leads to numerous
versions of each connector/quantifier.

For instance one might want an "or" between two sets, which is
extracted to booleans: one keeps the left/right information but
discards the respective proof that we are in the corresponding branch.

There are a few of this connectors and quantifiers which are provided
in the library (together with some syntactic sugar) but in some cases
you will have to define your ad hoc quantifier yourself.

In the present case this seems the best solution:
> 
> I want to write something like
> 
> exists R . Defn (R) /\ {t: T1 -> T2 | (x:T1) R x (tx)}

An existential is an inductive definition with one constructor. Here
it would be something like:

Inductive myEx [Defn : (T1 -> T2 -> Prop)->Prop ] : Set :=
 myExi : (t:T1->T2)(R:T1->T2->Prop)(Defn R)->
              ((x:T1)(R x (t x)))->
                  (nyEx Defn).

You then get myEX :  ((T1 -> T2 -> Prop)->Prop) -> Set

and (myEx Defn) is the set/proposition you want. And it gets extracted
to T1->T2 (that is only the t remains of a proof of (myEx Defn) after
extraction).

You use the Elim the usual way. Exists has to be replaced by 
"Apply myExi with t:= ... R:= ... .".



The situation might change if we finaly use another way to mark
computational content. This way of handling things still seems
bearable to me, though.



Cheers,



Benjamin







Archive powered by MhonArc 2.6.16.

Top of Page