defining with tactics problem demonstration

gistfile1.coq

Require Import Omega.
Require Import Coq.Vectors.Vector.
Require Import Coq.Vectors.VectorDef.
Open Scope vector_scope.
Require Import List.
Require Import Arith.

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 sum_pairs (len : nat) (v : Vector.t nat len) : Vector.t nat (pred len).
  induction v as [|elem1 length1 tail1].
  + apply Vector.nil.
  + simpl in *. destruct tail1 as [|elem2 length2 tail2].
    - apply Vector.nil.
    - apply Vector.cons. apply (elem1 + elem2). apply IHtail1.
Defined.

Definition snoc : forall {len : nat} {A : Type}, Vector.t A len -> A -> Vector.t A (S len).
  intros len A v. induction v as [|elem length tail]; intro new.
  + apply Vector.cons. apply new. apply Vector.nil.
  + apply Vector.cons. apply elem. apply IHtail. apply new.
Defined.

Definition next : forall {len : nat}, Vector.t nat len -> Vector.t nat (S len).
  intros len prev. apply sum_pairs in prev. destruct len.
  + apply Vector.cons. apply 1. apply Vector.nil.
  + simpl in prev. apply snoc. apply Vector.cons. apply 1. apply prev. apply 1.
Defined.

CoFixpoint pascal_aux : forall n, Vector.t nat n -> triangle_t nat n.
  intros n vec. constructor.
  + apply vec.
  + apply pascal_aux. apply next. apply vec.
Defined.

Definition pascal : triangle_t nat 0.
  apply pascal_aux. apply Vector.nil.
Defined.

Fixpoint pascal_row_aux (step : nat) : forall n, triangle_t nat n -> Vector.t nat (step + n).
  induction step; intros n tr.
  + simpl. inversion tr as [? vec ?]. apply vec.
  + assert (S step + n = step + S n) by omega. rewrite H. apply IHstep.
    inversion tr as [? ? tail]. apply tail.
Defined.

Definition pascal_nth (row col : nat) : col <= row -> nat.
  remember (pascal_row_aux (S row) 0 pascal) as column. intro pf.
  apply @nth_order with (p := col) (n := S row).
  assert (S row + 0 = S row) by omega. rewrite <- H. apply column.
  omega.
Defined.

Lemma pascal_min_row : forall row,
  pascal_nth row 0 (le_0_n row) = 1.
Proof.
  induction row.
  simpl. (* stuck *)
Abort.

gistfile2.ml

open Datatypes
open Peano
open Vector
open VectorDef

type 't triangle_t = 't __triangle_t Lazy.t
and 't __triangle_t =
| Coq_triangle of nat * 't Vector.t * 't triangle_t

(** val sum_pairs : nat -> nat Vector.t -> nat Vector.t **)

let rec sum_pairs n = function
| Vector.Coq_nil -> Vector.Coq_nil
| Vector.Coq_cons (h, n0, t1) ->
  (match t1 with
   | Vector.Coq_nil -> Vector.Coq_nil
   | Vector.Coq_cons (elem2, length2, tail2) ->
     Vector.Coq_cons ((plus h elem2), length2, (sum_pairs n0 t1)))

(** val snoc : nat -> 'a1 Vector.t -> 'a1 -> 'a1 Vector.t **)

let rec snoc n t0 new0 =
  match t0 with
  | Vector.Coq_nil -> Vector.Coq_cons (new0, O, Vector.Coq_nil)
  | Vector.Coq_cons (h, n0, t1) ->
    Vector.Coq_cons (h, (S n0), (snoc n0 t1 new0))

(** val next : nat -> nat Vector.t -> nat Vector.t **)

let next len prev =
  let prev0 = sum_pairs len prev in
  (match len with
   | O -> Vector.Coq_cons ((S O), O, Vector.Coq_nil)
   | S len0 -> snoc (S len0) (Vector.Coq_cons ((S O), len0, prev0)) (S O))

(** val pascal_aux : nat -> nat Vector.t -> nat triangle_t **)

let rec pascal_aux n vec =
  lazy (Coq_triangle (n, vec, (pascal_aux (S n) (next n vec))))

(** val pascal : nat triangle_t **)

let pascal =
  pascal_aux O Vector.Coq_nil

(** val pascal_row_aux : nat -> nat -> nat triangle_t -> nat Vector.t **)

let rec pascal_row_aux step =
  let rec f n n0 tr =
    match n with
    | O -> let Coq_triangle (n1, vec, h) = Lazy.force tr in vec
    | S n1 ->
      f n1 (S n0) (let Coq_triangle (n2, h0, tail) = Lazy.force tr in tail)
  in f step

(** val pascal_nth : nat -> nat -> nat **)

let pascal_nth row col =
  let column = pascal_row_aux (S row) O pascal in
  nth_order (S row) (Obj.magic column) col