The Coq mailing list

[David Pichardie <David.Pichardie AT inria.fr>]

Dear Nuno,

Did you try with a more general induction hypothesis ?

Lemma string_of_nat_fact:

  forall n acc1, forall m acc2, n <> m -> acc1 = "" -> acc2 = "" ->

                        string_of_nat_aux n acc1 <> string_of_nat_aux m acc2.

Proof.

  intros n acc1.

  functional induction string_of_nat_aux n acc1.

  ... 

Now the induction hypothesis is stronger.

Hope this helps,

David.

Le 24 mai 2013 à 13:17, Nuno Gaspar <nmpgaspar AT gmail.com> a écrit :

Thank you Pierre.

I tried to play with it a bit, but no luck; the problem is that the recursive call is made on n/10 ..

It seems I can progress more by using functional induction.. alas, I inevitably get useless induction hypothesis and thus... stuck.

Any ideas on how to solve this?

A version with imports follows ;)

Require Import Coq.Strings.Ascii.
Require Import Coq.Strings.String.
Require Import NPeano.
Require Import Recdef.
Open Scope string_scope.

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_aux_0:
  forall x, string_of_nat_aux 0 x = x.
Proof.
  intros. reflexivity.
Qed.

Lemma string_of_nat_aux_empty_fact:
  forall x y, y <> "" -> "" <> string_of_nat_aux x y.
Proof.
  intros.
  functional induction string_of_nat_aux x y. auto.
  apply IHs. clear IHs.
  simpl.
  destruct ((divmod n 9 0 9)); simpl.
  destruct n1; compute; intro; congruence.
Qed.


Lemma string_of_nat_fact:
  forall n m acc1 acc2, n <> m -> acc1 = "" -> acc2 = "" ->
                        string_of_nat_aux n acc1 <> string_of_nat_aux m acc2.
Proof.
  intros.
  functional induction string_of_nat_aux n acc1.
  (*Case "1/2".*)
  functional induction string_of_nat_aux m acc2; try congruence. Focus.
  destruct ((n / 10)).
    (*SCase "1/2".*)
      rewrite string_of_nat_aux_0.
      simpl.
      destruct (divmod n 9 0 9).
      simpl.
      destruct n1; compute; intro; congruence.
    (*SCase "2/2".*)
      simpl.
      destruct (divmod n 9 0 9). simpl.
      destruct n2;
        apply string_of_nat_aux_empty_fact;
        compute; intro; congruence.
  (*Case "2/2".*)
    functional induction string_of_nat_aux m acc2.
    (*SCase "1/2"*)
      simpl. clear.
      intuition.
      destruct (divmod _x 9 0 9).
      simpl in *.
      destruct n0;
        symmetry in H;
        apply string_of_nat_aux_empty_fact in H;
        auto; discriminate.
    (*SCase "2/2".*)
      IH are useless..

2013/5/23 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.

--
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.