Coq losing information from if-statement when doing recursive function with Program

Question

I want to write this recursive variant of gcd as simply and "naturally" as possible in Coq.

Require Import Arith.
Require Import Program.

Program Fixpoint gcd (a b:nat) {measure b} :=
  if 0 <? b then gcd b (a mod b) else a.
Next Obligation.
  (* Here I need to prove that `a mod b < b` *)
  apply Nat.mod_upper_bound.

Now I need to prove that b <> 0 but I have lost the info that we are in the 0 <? b = false branch.

  a, b : nat
  gcd : nat -> forall b0 : nat, b0 < b -> nat
  ============================
  b <> 0

How do I keep the information from the if statement?

I know I could use match, but how to I write it with if?)

Program Fixpoint gcd (a b:nat) {measure b} :=
  match b with 0 => a | S b' => gcd b (a mod b) end.
Next Obligation.
  apply Nat.mod_upper_bound.
  (* Goal:  S b' <> 0 *)
  congruence.
Defined.

=== EDIT ===

I noticed that Coq (in more recent versions?) remembers the association between 0 <? b and the match patterns (true or false in this case). Or is it a feature of Program? Anyway, I thought that if essentially was expanded into this match statement, but apparently it isn't...

Program Fixpoint gcd (a b:nat) {measure b} : nat:=
  match 0<?b with
  | true => gcd b (a mod b)
  | false => a
  end.
Next Obligation.
  apply Nat.mod_upper_bound.
  (* now we have ` true = (0 <? b)` in the assumptions, and the goal `b <> 0` *)
  now destruct b.
Defined.

[This](http://stackoverflow.com/questions/42285235/writing-well-founded-programs-in-coq-using-fix-or-program-fixpoint) is a related question. — Anton Trunov, May 10 '17 at 16:50
Thank you for this interesting observation! Yes, you are right, it is a feature of `Program`. I updated my answer with a couple quotes :) — Anton Trunov, May 10 '17 at 18:04

Anton Trunov · Accepted Answer · 2017-05-10T18:00:14.357

One can use lt_dec to do that.

lt_dec
     : forall n m : nat, {n < m} + {~ n < m}

This way we can keep the proofs we need in the context, unlike when using <?, which returns a bool.

Require Import Arith.
Require Import Program.

Program Fixpoint gcd (a b:nat) {measure b} :=
  if lt_dec 0 b then gcd b (a mod b) else a.
Next Obligation.
  apply Nat.mod_upper_bound.
  now destruct H.
Defined.

Yes, it is a feature of Program. Actually the reference manual explain it in a very clear manner (see §24.1):

Generation of equalities. A match expression is always generalized by the corresponding equality. As an example, the expression:
match x with
  | 0 => t
  | S n => u
  end.
will be first rewritten to:
(match x as y return (x = y -> _) with
| 0 => fun H : x = 0 -> t
| S n => fun H : x = S n -> u
end) (eq_refl n).

Here is the reason why if is different:

To give more control over the generation of equalities, the typechecker will fall back directly to Coq’s usual typing of dependent pattern-matching if a return or in clause is specified. Likewise, the if construct is not treated specially by Program so boolean tests in the code are not automatically reflected in the obligations. One can use the dec combinator to get the correct hypotheses as in:
Coq < Program Definition id (n : nat) : { x : nat | x = n } :=
        if dec (leb n 0) then 0
        else S (pred n).

Coq losing information from if-statement when doing recursive function with Program

1 Answers1