The Coq mailing list

[Daniel Schepler <dschepler AT gmail.com>]

On Saturday, April 05, 2014 09:35:40 PM Ömer Sinan Ağacan wrote:
> 2014-04-05 21:31 GMT+03:00 Robbert Krebbers 
<mailinglists AT robbertkrebbers.nl>:
> > That is because you are using natural numbers in unary representation.
> > 
> > Already something like:
> >   Check 362880.
> > 
> > results in
> > 
> >   Warning: Stack overflow or segmentation fault happens
> >   when working with large numbers in nat (observed
> >   threshold may vary from 5000 to 70000 depending on
> >   your system limits and on the command executed).
> >   
> >   Stack overflow.
> > 
> > Better use a more efficient representation for natural numbers like N (an
> > inductive representation as bit sequences) or bigN (arbitrary precision
> > machine integers).
> 
> Ah, that makes sense, thanks Robbert!
> 
> Any ideas about rest of my questions?

If you use the Program facility, and use eq_nat_dec instead of beq_nat to get 
some proof content out of the result, then that takes care of the immediate 
issue.  But then you run into the issue that Coq can't detect a decreasing 
argument of the fixpoint (and indeed, if idx > stop then the fixpoint won't 
terminate).  So my solution is to add an argument whose type is an inductive 
Prop, constructed specifically so that it "decreases" on each step:

Require Import Program.

Inductive alt_ge (n : nat) : nat -> Prop :=
| alt_ge_n : alt_ge n n
| alt_ge_step : forall m:nat, alt_ge n (S m) -> alt_ge n m.

Lemma alt_ge_conv : forall {n m:nat}, alt_ge n m -> n <> m ->
  alt_ge n (S m).
Proof.
destruct 1; trivial.
intro H; contradiction H; trivial.
Defined.

(* or:
Definition alt_ge_conv {n m:nat} (Hge : alt_ge n m) :
  n <> m -> alt_ge n (S m) :=
match Hge in (alt_ge _ m) return (n <> m -> alt_ge n (S m)) with
| alt_ge_n => fun Hneq : n <> n => False_ind _ (Hneq eq_refl)
| alt_ge_step m H => fun _ => H
end.

which is why alt_ge_conv Hge is considered "smaller" than Hge
*)

Program Fixpoint nth_triangle_aux {T : Type} (idx stop : nat)
  (tr : triangle_t T idx) (Hge : alt_ge stop idx) {struct Hge} :
  Vector.t T stop :=
if eq_nat_dec idx stop then
  match tr with triangle _ _ v _ => v end
else
  match tr with triangle _ _ _ tr' =>
    nth_triangle_aux (S idx) stop tr' (alt_ge_conv _ _)
  end.

Lemma alt_ge_trans : forall n m p:nat, alt_ge n m -> alt_ge m p ->
  alt_ge n p.
Proof.
induction 2; auto using alt_ge.
Defined.

Lemma alt_ge_n_O : forall n:nat, alt_ge n 0.
Proof.
induction n; eauto using alt_ge_trans, alt_ge.
Defined.

Definition nth_triangle {T : Type} (idx : nat)
  (tr : triangle_t T 0) : Vector.t T idx :=
nth_triangle_aux 0 idx tr (alt_ge_n_O _).

Recursive Extraction nth_triangle.
-- 
Daniel Schepler