Witness Extraction

Define a function sig_extract having the following type :

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

such that the following theorem holds :

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

Prove this theorem in Coq.

Apply your construction to the following problem :
Let us consider the following declaration :

Require 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

Going home

Pierre Castéran