1

I am currently working with Coq and I am encountering a problem that I don't know how to solve.

Let's say we are working with a given type, I'll take nat for the example, and I want to use a function f that might fail. To compensate the failure, we define f to be of type nat -> option nat.

Now I have a given hypothesis H: nat -> bool under which f doesn't fail, and I have even proved the lemma

Lemma no_error_in_f : forall (n:nat), H n = true -> exists (u:nat), f n = Some u.

I want to define a function g: nat->nat which gives the result of f on n if H n is satisfied, and just gives n otherwise. This function should be well defined, but I don't know how to define it properly. If I try something naive like Definition g (n:nat) := if H n then f n else n., there is a problem in the typing system.

Does anyone knows how to gather all the elements and tell the system that the definition is legal?

Vinz
  • 5,997
  • 1
  • 31
  • 52
tben
  • 123
  • 1
  • 6

3 Answers3

1

I give here a solution that works with the same hypotheses as the ones given in the question.

Axiom f : nat -> option nat.
Axiom H : nat -> bool.
Axiom no_error_in_f : forall n,
  H n = true -> exists u, f n = Some u.

Lemma no_error_in_f_bis : forall n,
  H n = true -> f n <> None.
Proof.
  intros. apply no_error_in_f in H0. destruct H0. rewrite H0. discriminate.
Qed.

Definition g n :=
  match H n as b return H n = b -> _ with
  | true => fun H =>
    match f n as f0 return f n = f0 -> _ with
    | Some n0 => fun _ => n0
    | None => fun H0 => match no_error_in_f_bis n H H0 with end
    end eq_refl
  | false => fun _ => n
  end eq_refl.

I use another lemma than no_error_in_f, which is more convenient to prove False. Note that the two ideas of this function (use the return construct of match, destruct a proof of False to show that a branch is not reachable) are explained here: http://adam.chlipala.net/cpdt/html/Subset.html.

eponier
  • 3,062
  • 9
  • 20
0

There are two problems in your development. One is that you cannot use no_error_in_f to define g in Coq without assuming additional axioms, because Coq does not allow to extract computational information from a proof (check here for more details). Another problem is that you can't use H in an if expression, because it returns a Prop instead of a bool (check this answer for more details).

Community
  • 1
  • 1
Arthur Azevedo De Amorim
  • 23,012
  • 3
  • 33
  • 39
  • Sorry, I made a mistake, the second error does not appear, because `H n` is of type `bool` and my lemma has as predicate `H n = true`. I will edit this. For the first problem, I thought of something like False_rec, or something like that – tben Jan 23 '16 at 22:59
0

I have found a way to do this, here is my solution if anyone is interested:

Definition g (n:nat) :nat := (match (H n) as a return a = H n -> nat with | true => (fun H_true => (match (f n) as b return b = f n -> nat with | Some u => (fun _ => u) | None => (fun H1 => False_rec _ (no_error_in_f H_true H1)) end) (eq_refl f n)) | false => n end) (eq_refl H n).

For those who would like to know what it means, False_rec take as a second argument a proof of False and certifies that the matching is not possible. the term

(match (f n) as b return b = f n -> nat with | Some u => (fun _ => u) | None => (fun H1 => False_rec _ (no_error_in_f H_true H1)) end) (eq_refl f n)) has type f n = f n-> nat and when I apply it to the proof eq_refl (f n) (which is a proof that f n = f n, so is typed f n = f n), I obtain a nat. This a trick that allows me to obtain H1 which is a proof that f n = None obtained using the reflexevity of equality and the pattern-matching, and that I am goin to use in my proof of False.

Same goes for the other match.

tben
  • 123
  • 1
  • 6
  • I understand the idea, but your solution does not typecheck as is. Could you correct it so that it works with the hypotheses given in your question ? – eponier Jan 24 '16 at 14:22