The Coq mailing list

[AUGER Cédric <sedrikov AT gmail.com>]

Le Sun, 13 Apr 2014 11:32:59 +0300,
Ömer Sinan Ağacan 
<omeragacan AT gmail.com>
 a écrit :

> Hi all,
> 
> With your help to my last questions, I managed to write a function
> that produces an infinite data structure, where in every level I'm
> holding a a row of Pascal's triangle. Here's the complete program:
> 
>   Require Import Omega.
>   Require Import Coq.Vectors.Vector.
>   Require Import Coq.Vectors.VectorDef.
>   Open Scope vector_scope.
>   Require Import Bool.
>   Require Import List.
>   Require Import Arith.
>   Require Import Arith.EqNat.
>   Require Import Program.
> 
>   CoInductive triangle_t (T : Type) : nat -> Type :=
>   | triangle : forall (n : nat), Vector.t T n -> triangle_t T (S n) ->
> triangle_t T n.
> 
>   Definition nth_triangle_aux
>     : forall T steps_left stop,
>       stop >= steps_left -> triangle_t T (stop - steps_left) ->
> Vector.t T stop. refine (fix fn T (steps_left stop : nat)
>                      (pf : stop >= steps_left)
>                      (tr : triangle_t T (stop - steps_left))
>                      : Vector.t T stop :=
>       match steps_left as sl return steps_left = sl -> Vector.t T
> stop with | O => fun Z => _
>       | S n' => fun NZ => _
>       end (eq_refl steps_left)).
>     subst. rewrite <- minus_n_O in tr. inversion tr; subst. apply X.
>     apply fn with (steps_left := n').
>       rewrite NZ in pf. omega.
>       rewrite NZ in tr. inversion tr; subst.
>         assert (S (stop - S n') = stop - n'). omega.
>         rewrite H in X0. apply X0.
>   Defined.
> 
>   Definition nth_triangle {T : Type} (idx : nat) (tr : triangle_t T 0)
> : Vector.t T idx.
>     refine (nth_triangle_aux T idx idx _ _).
>     auto.
>     rewrite minus_diag. apply tr.
>   Defined.
> 
>   Fixpoint pt_aux h len (v : Vector.t nat len) : Vector.t nat (S
> len) := match v in Vector.t _ len' with
>     | Vector.nil as v' => Vector.cons nat 1 0 v'
>     | Vector.cons h' _ t' => Vector.cons nat (h + h') _ (pt_aux h' _
> t') end.
> 
>   CoFixpoint pt_aux' len (v : Vector.t nat len) : triangle_t nat
> len := match v with
>     | Vector.nil as v' => triangle nat 0 v' (pt_aux' 1 (Vector.cons
> nat 1 0 v')) | Vector.cons h' _ t' as v' =>
>         let vec := Vector.cons nat 1 _ (pt_aux h' _ t') in
>         triangle nat _ v' (pt_aux' _ vec)
>     end.
> 
>   Definition pascals_triangle : triangle_t nat 0 := pt_aux' 0
> (Vector.nil nat).
> 
> Even though I didn't run extracted OCaml code, I checked it and the
> code looked reasonable(except keeping length of vectors and using
> nats). But for some reason, if I try to run this program:
> 
>   Eval compute in (Vector.nth (nth_triangle 3 pascals_triangle)
>                               (Fin.F1)).
> 
> It takes almost a minute to end and it produces a very weird term:
> 
>   Warning: query commands should not be inserted in scripts
>        = (fix nth_fix (m : nat) (v' : Vector.t nat m) (p : Fin.t m)
> {struct v'} :
>             nat :=
>             match p in (Fin.t m') return (Vector.t nat m' -> nat) with
>             | Fin.F1 q =>
>                 fun v : Vector.t nat (S q) =>
>                 match
>                   v as v'0 in (Vector.t _ m0)
>                   return
>                     (match m0 as m1 return (Vector.t nat m1 -> Type)
> with | 0 => fun _ : Vector.t nat 0 => False -> True
>                      | S n => fun _ : Vector.t nat (S n) => nat
>                      end v'0)
>                 with
>                 | Vector.nil =>
>                     fun devil : False => match devil return True with
>                                          end
>                 | Vector.cons h _ _ => h
>                 end
> ... 650 lines of code removed ...
>        : nat
> 
> I tried using a different strategy to evaluate this term:
> 
>   Eval simpl in (Vector.nth (nth_triangle 3 pascals_triangle)
>                             (Fin.F1)).
> 
> This time it ended fast but resulting term is still equally useless:
> 
>   Warning: query commands should not be inserted in scripts
>        = Vector.nth (nth_triangle 3 pascals_triangle) Fin.F1
>        : nat
> 
> Can anyone tell me what's wrong with my code and how can I get a 'nat'
> out of simple program? Do I have to run extracted OCaml program for
> this?
> 
> Thanks.
> 
> ---
> Ömer Sinan Ağacan
> http://osa1.net

==================================================================
Below are many optimizations for your code (up to the point that it
does not use any proof script at all). The quick answer to your
question is that although you put all your terms as 'Defined', the
tactics you used relied on opaque terms (for instance, it is the case
of omega which relies on opaque arithmetical proofs).

==================================================================
Require Import Coq.Vectors.Vector.
Require Import Coq.Vectors.VectorDef.
Open Scope vector_scope.

CoInductive triangle_t (T : Type) (n : nat) : Type :=
| triangle : Vector.t T n -> triangle_t T (S n) -> triangle_t T n.

Fixpoint po (a : nat) : forall (Tn : nat -> Type), Tn a -> Tn (a + O) :=
  fun Tn =>
  match a as a return Tn a -> Tn (a + O) with
  | O => fun x => x
  | S a => fun x => po a (fun n => Tn (S n)) x
  end.

Definition ps (b : nat) : forall (a : nat) (Tn : nat -> Type),
                          Tn (S a + b) -> Tn (a + S b) :=
  fix ps a := fun Tn =>
  match a as a return Tn (S a + b) -> Tn (a + S b) with
  | O => fun x => x
  | S a => fun x => ps a (fun n => Tn (S n)) x
  end.

Definition nth_triangle_aux (T : Type)
: forall steps_done steps_left,
         triangle_t T steps_done -> Vector.t T (steps_done + steps_left)
:= fix nth_triangle_aux (steps_done steps_left : nat)
                        (tr : triangle_t T steps_done) :=
   match tr with
   | triangle v t =>
     match steps_left as sl return Vector.t T (steps_done + sl) with
     | O => po steps_done (Vector.t T) v
     | S n' => ps n' steps_done (Vector.t T)
                  (nth_triangle_aux (S steps_done) n' t)
     end
   end.

Definition nth_triangle {T : Type}
: forall idx, triangle_t T O -> Vector.t T idx
:= nth_triangle_aux T O.

Fixpoint pt_aux h len (v : Vector.t nat len) : Vector.t nat (S len) :=
  match v in Vector.t _ len' with
  | Vector.nil as v' => Vector.cons nat 1 0 v'
  | Vector.cons h' _ t' => Vector.cons nat (h + h') _ (pt_aux h' _ t')
  end.

CoFixpoint pt_aux' len (v : Vector.t nat len) : triangle_t nat len :=
  match v with
  | Vector.nil as v' => triangle nat 0 v' (pt_aux' 1 (Vector.cons nat 1 0 v'))
  | Vector.cons h' _ t' as v' =>
      let vec := Vector.cons nat 1 _ (pt_aux h' _ t') in
      triangle nat _ v' (pt_aux' _ vec)
  end.

Definition pascals_triangle : triangle_t nat 0 := pt_aux' 0 (Vector.nil nat).

Eval simpl in (Vector.nth (nth_triangle 3 pascals_triangle)
                            (Fin.F1)).