yoshihiro503

Require Import Arith List.
Import ListNotations.

Lemma list_Forall_map : forall (A B: Type) (P : B -> Prop) (f: A -> B) xs,
    Forall P (map f xs) <-> Forall (fun x => P (f x)) xs.
Proof.
Admitted.

yoshihiro503

Require Import Arith List.
Import ListNotations.

Fixpoint range_aux (a len: nat) : list nat :=
  match len with
  | O => []
  | S len' => a :: range_aux (S a) len'
  end.
Definition range (a b: nat) : list nat := range_aux a (b - a + 1).

yoshihiro503

Require Import Arith List.
Import ListNotations.

Definition list_reduce_left {A: Type} (f: A -> A -> A) (xs: list A) :=
  match xs with
  | [] => None
  | x :: xs =>
    Some (List.fold_left f xs x)
  end.

yoshihiro503

opamで fialyzer 環境の導入

$ opam switch fialyzer --alias-of 4.04.2
$ eval `opam config env`

obeamのインストール

yoshihiro503

Definition fact (n: nat) : nat.
  refine (Fix (lt_wf) (fun _ => nat)
              (fun n F =>
                 match n as k return n=k -> nat with
                 | O => fun _ => 1
                 | S n' => fun _ => n * F n' _
                 end (eq_refl _)
              ) n).
  rewrite e. auto with arith.
Defined.

yoshihiro503

case class Lazy[A](f: () => A) {
  private var contents : Option[A] = None
  def get() : A = {
    this.contents match {
      case None =>
        this.contents = f()
        this.contents
      case Some(x) => x
    }
  }

yoshihiro503

Require Import Program.
Open Scope list_scope.

Lemma fold_right_rev : forall (A: Type) (f: A -> A -> A) xs x0,
  (forall x y z, f x (f y z) = f (f x y) z) ->
  (forall x y, f x y = f y x) ->
  List.fold_right f x0 xs = List.fold_right f x0 (List.rev xs).

yoshihiro503

Require Import Program.
Open Scope list_scope.

Lemma fold_right_tail : forall (A B: Type) (f: A -> B -> B) xs x b0,
  List.fold_right f b0 (xs ++ [x]) = List.fold_right f (f x b0) xs.

yoshihiro503

OCamlで説明するgen_serverの使い方

Erlang/OTPを勉強し始めたので、自分が理解するためにOCamlの型でgen_serverを理解したい。間違いの指摘など大歓迎。 gen_serverを完璧に型付けすることが目的ではない。なんとなく理解できれば良いつもり。

想定する読者

• OCaml使い
• Erlang/OTPの勉強中の人
• (optional) すごいE本の14章を読んだ

yoshihiro503

// すごいE本の30.6章の「選択的な節を持つ型」 (p.538) をScalaでも
object AlternativeClausesType {
  def main() = {
    val List(_, _) = convert(('a, 'b))
    val (_, _)     = convert(List('a, 'b))
    val List(_, _) = convert(List('a, 'b)) // <- 型エラーにできる
    val (_, _)     = convert(('a, 'b))     // <- 型エラーにできる
  }
  
  def convert(xy: (Symbol, Symbol)): List[Symbol] = xy match {