Coq2SMLの進捗

test.sml

(** val fold_left : ('a1 -> 'a2 -> 'a1) -> 'a2 list -> 'a1 -> 'a1 **)

fun fold_left f l a0 =
  case l of
    [] => a0
  | b::t => fold_left f t (f a0 b)

(** val fold_right : ('a2 -> 'a1 -> 'a1) -> 'a1 -> 'a2 list -> 'a1 **)

fun fold_right f a0 l =
  case l of
    [] => a0
  | b::t => f b (fold_right f a0 t)

datatype 'a tree =
  Leaf of 'a
| Node of 'a tree * 'a tree

(** val dfs : 'a1 tree -> 'a1 list **)

fun dfs t =
  case t of
    Leaf x => x::[]
  | Node (l, r) => (fn x => fn y => x @ y) (dfs l) (dfs r)

(** val dfs_aux : 'a1 list -> 'a1 tree -> 'a1 list **)

fun dfs_aux acc t =
  case t of
    Leaf x => x::acc
  | Node (l, r) => dfs_aux (dfs_aux acc r) l

(** val dfs' : 'a1 tree -> 'a1 list **)

val dfs' =
  dfs_aux []

(** val dec : int list -> int **)

fun dec l =
  fold_left (fn a => fn b =>
    (fn x => fn y => x + y)
      ((fn x => fn y => x * y) ((fn n => n + 1) ((fn n => n + 1)
        ((fn n => n + 1) ((fn n => n + 1) ((fn n => n + 1) ((fn n => n + 1)
        ((fn n => n + 1) ((fn n => n + 1) ((fn n => n + 1) ((fn n => n + 1)
        0)))))))))) a) b) l 0

(** val rev_hex : int list -> int **)

val rev_hex =
  fold_right (fn a => fn b =>
    (fn x => fn y => x + y) a
      ((fn x => fn y => x * y) ((fn n => n + 1) ((fn n => n + 1)
        ((fn n => n + 1) ((fn n => n + 1) ((fn n => n + 1) ((fn n => n + 1)
        ((fn n => n + 1) ((fn n => n + 1) ((fn n => n + 1) ((fn n => n + 1)
        ((fn n => n + 1) ((fn n => n + 1) ((fn n => n + 1) ((fn n => n + 1)
        ((fn n => n + 1) ((fn n => n + 1) 0)))))))))))))))) b)) 0

test.v

Require Import List.

Inductive tree (A : Type) : Type :=
  | leaf : A -> tree A
  | node : tree A -> tree A -> tree A.

Fixpoint dfs {A} (t : tree A) :=
  match t with
  | leaf x => x :: nil
  | node l r => dfs l ++ dfs r
  end.

Fixpoint dfs_aux {A} (acc : list A) (t : tree A) :=
  match t with
  | leaf x => x :: acc
  | node l r => dfs_aux (dfs_aux acc r) l
  end.
Definition dfs' {A} : tree A -> list A := dfs_aux nil.

Lemma dfs_aux_fact : forall (A : Type) (l : list A) (t : tree A),
  dfs_aux l t = dfs_aux nil t ++ l.
Proof.
  intros A l t.
  generalize dependent l.
  induction t; intros l.
    reflexivity.

    simpl.
    rewrite -> IHt1.
    rewrite -> IHt2.
    rewrite app_assoc.
    congruence.
Qed.

Theorem dfs'_valid : forall (A : Type) (t : tree A), dfs' t = dfs t.
Proof.
  unfold dfs'.
  intros A t.
  induction t.
    reflexivity.

    simpl.
    rewrite -> dfs_aux_fact.
    congruence.
Qed.

Definition dec l := fold_left (fun a b => 10 * a + b) l 0.
Definition rev_hex := fold_right (fun a b => a + 16 * b) 0.

Extraction Language Sml.
Extraction tree.
Extract Inductive list => "list" ["[]" "(::)"].
Extract Inlined Constant app => "(fn x => fn y => x @ y)". 
Extract Inductive nat => int ["0" "(fn n => n + 1)"]
  "(fun fO fS n -> if n = 0 then fO () else fS (n-1))".
Extract Inlined Constant plus => "(fn x => fn y => x + y)".
Extract Inlined Constant mult => "(fn x => fn y => x * y)".
Extraction "test.sml" dfs dfs' dec rev_hex.