Witness Extraction

Define a function sig_extract having the following type :

forall (A:Type) (P:A -> Prop), sig P -> A

such that the following theorem holds :

Theorem sig_extract_ok {A: Type}{P:A -> Prop}:
 forall (y:sig P), P (sig_extract A P y).

Prove this theorem in Coq.

Apply your construction to the following problem :
Considering the following declaration :

Require Import ZArith.
Open Scope Z_scope.

Parameter
  div_pair :
    forall a b:Z,
      0 < b ->
      {p : Z * Z | a = fst p * b + snd p  /\ 0 <= snd p < b}.

Use sig_extract to build a function of type

forall a b:Z, 0 < b -> Z*Z.

Your function must satisfy the specification of euclidean division.

Solution

Follow this link