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 Import ZArith.
Open Scope Z_scope.

  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.


Follow this link

Going home
Pierre Castéran