The Coq mailing list

[Christine Paulin <Christine.Paulin AT lri.fr>]

Let try a few explanations around  your example :

In a more general setting we could have 

Inductive P [A:Set] : Prop := Hide : A -> (P A).

You want to prove:
Lemma Hide_inj : (A:Set)(x,y:A)(Hide x)==(Hide y)->x=y.

the normal way to do that uses a function 
proj : (P A)->A 
such that (proj (Hide x))=x which cannot exists because it extract the
information x from the non-informative term (Hide x)

The alternative way is to build a non-informative relation 
R : (P A)->A ->Prop corresponding to the projection function ie
such that (R (Hide x) y) <-> x=y 
then (R (Hide y) y) is trivially true and Hide x = Hide y implies 
(R (Hide x) y) which is equivalent to x=y

This relation cannot be built in Coq because it requires an
elimination from Prop to Type which is not allowed because it may lead
to inconsistency if you add an axiom which leads to proof-irrelevance 
(P:Prop)(a,b:P)a=b
(for instance classical logic)
Indeed, in that case, if your axiom was also true then you will have 
(A:Set)(a,b:A)a=b
which is contradictory

But if you avoid any other axiom, then your axiom does not lead to an
inconsistency because 
        1- it is provable in a system where Prop=Set
        2- it is non-informative and then does not lead to an
extraction inconsistency.

More precisely, if you prove Ax |- t:P then you can extract your
program, which is correct in a system where Ax is realisable.
You have to use a different realisability than the one presented in my
thesis, where you keep the logical proof-terms in realisability
predicate, such that your axiom becomes realisable iff it is provable.

Christine.



In his message of Fri June 12, 1998, Jean-Francois Monin writes: 
> Hello,
> 
> I have a Set ordm and functions like f: ordm -> ordm, and introduce
> 
> Inductive ordp : Prop := Hide : ordm -> ordp.
> Scheme ordp_indd := Induction for ordp Sort Prop.
> 
> In this way it is possible to
> would work on some family (A x) with x:ordp and to
> build e.g. ff : (x:ordp) (A x) -> (A (f x)). 
> Case analysis on the content of x is forbidden at the Set level.
> 
> Extracting the informative contents of ff yields a function of type
> A->A, as desired. (If ff had the type (x:ordm) (A x) -> (A (f x)),
> extraction would inhabit ordm->A->A, though the first argument is not
> used.)
> 
> I agree that it is not very convenient, because counterparts of
> theorems on ordm have to be proved on ordm. As far as I remember, this
> should be settled with a new approach of extraction to be implemented.
> 
> However it should at least be feasible. At the moment I need the
> following axiom.
> 
> Axiom ax_eqP_eq :
>   (x,y:ordm) (eqP ordm (Hide x) (Hide y)) -> x=y.
> 
> Is this axiom dangerous ?
> 
> -- Jean-Francois.
-- 
  Christine Paulin-Mohring             mailto : 
Christine.Paulin AT lri.fr
  LRI, URA 410 CNRS, Bat 490, Université Paris Sud,   91405 ORSAY Cedex 
  LRI   tel : (+33) (0)1 69 15 66 35       fax : (+33) (0)1 69 15 65 86
  INRIA tel : (+33) (0)1 39 63 55 70       fax : (+33) (0)1 39 63 56 84
  Tatoo tel : 06 04 24 44 75 
   message numerique +1(pas urgent)-3(tres urgent) ou * + message vocal