The Coq mailing list

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

Hi Nuno,

the _terminate function is an internal function defined by the Function command when the function is not structurally decreasing.

Non structurally functions should unfolded using the ..._equation lemma that should have been generated as well, here "rewrite string_of_nat_aux_equation works." works.

Best regards,
Pierre Courtieu

2013/5/23 Nuno Gaspar <nmpgaspar AT gmail.com>

Hello.

I recently found the function string_of_nat : nat -> string in [1]

Quite cool, until I decided to prove some stuff about it. For instance,

Definition digit_of_nat n := ascii_of_nat (n + 48).

Function string_of_nat_aux n acc {measure (fun x => x) n} :=
  match n with
    | 0 => acc
    | _ => string_of_nat_aux (n / 10) (String (digit_of_nat (n mod 10)) acc)
  end.
Proof.
  intros. apply Nat.div_lt; auto with arith.
Defined.

Definition string_of_nat n :=
  match n with
    | 0 => "0"%string
    | _ => string_of_nat_aux n EmptyString
  end.

Lemma string_of_nat_fact:
  forall n m, n <> m -> string_of_nat n <> string_of_nat m.
Proof.
  induction n; induction m; intros; try congruence.
  unfold string_of_nat.
  unfold string_of_nat_aux.
  wtf?

Unfolding the _aux function yields a string_of_nat_aux_terminate function that really doesn't exist in the implementation.. and I'm not quite sure how it could help me here.

Help please :-)

[1] https://github.com/glug/coq-classtests/blob/master/Classes/Show.v
--
Bart: Look at me, I'm a grad student, I'm 30 years old and I made $600 dollars last year.
Marge: Bart! Don't make fun of grad students, they just made a terrible life choice.