The Coq mailing list

[Jean-Francois Monin <JeanFrancois.Monin AT cnet.francetelecom.fr>]

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.