The Coq mailing list

[Pierre Courtieu <pierre.courtieu AT gmail.com>]

Hi, there are basically to ways of defining partial functions in coq.

The first is with monad None/Some as in Isabelle.

The second is by using dependent types to have a complete function on
a "subset" of the carrier type.

Defining recursive functions on dependent types is generally not
considered easy,
and reasoning about them even less easy. It  is however elegant:


Require Import Arith.
Require Import Program.
Require Import Omega.
Parameter y:nat.

(* First define a measure for proving termination*)

Definition minus ij := snd ij - fst ij.

(* Then define a function on a subset of nat*nat using the existential type.
The proof obligations are either for termination or for completing the
dependent type of recursive calls. *)

Program Fixpoint diff (ij:nat*nat | fst ij <= snd ij) {measure (minus
ij)}:nat :=
   match beq_nat (fst ij) (snd ij) with
       true => 0
     | false => diff(fst ij+1,snd ij) + 1
   end.
Next Obligation.
  simpl in *.
  symmetry in Heq_anonymous.
  apply beq_nat_false in Heq_anonymous.
  omega.
Defined.
Next Obligation.
  simpl in *.
  unfold minus;simpl.
  symmetry in Heq_anonymous.
  apply beq_nat_false in Heq_anonymous.
  omega.
Defined.

Lemma foo: fst (1,3) <= snd (1,3).
Proof.
  simpl.
  repeat constructor.
Defined.

Eval compute in diff (exist _ (1,3) foo).

(* We cannot express the lemma exactly as you did because we cannot
apply diff to (i,j) without a proof that i<=j, it becomes: *)
Lemma L: forall i j, (exists (H:i<=j), diff (exist _ (i,j) H) = i - j)
                     \/ (exists (H:j<=i), diff (exist _ (j,i) H) = j - i).

(* and I have no time to prove it. Not trivial. *)


Best regards,
Pierre


2014-09-25 17:31 GMT+02:00 Iain Whiteside 
<Iain.Whiteside AT newcastle.ac.uk>:
> Dear all,
>
> I am investigating the ways in which different theorem provers handle 
> undefinedness. In Isabelle, for example, 5/0 is represented as some number, 
> but we cannot reason about it; alternatively, partial functions can be 
> encoded in a monad (None | Some x).
>
> I’d be interested to hear what is the (if any) canonical way of 
> representing partiality in Coq and pCiC? For example, how could a recursive 
> difference function like below (deliberately partial) be represented?
>
> diff (i,j) = if i = y then 0 else diff(i+1,j) + 1
>
> additionally, could a theorem such as
>
> forall i j. diff(i,j) = i - j \/ diff(j,i) = j - i
>
> Many thanks in advance,
>
> Iain