yoshihiro503

(**
 * 自然数の二進表現
 * 例: (10010) は O I O O I Z
 * 一つの数の表現が一意でないことに注意
 *)
Inductive bin_numb :=
  | I : bin_numb -> bin_numb
  | O : bin_numb -> bin_numb
  | Z : bin_numb.

yoshihiro503

val tup22 = (1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1)

val ((a,b,c,d,e,f,g,h,i,j,k,l,m,n,o,p,q,r,s,t,u,v), w) = (tup22, "hoge")

yoshihiro503

import scala.reflect.ClassTag

class EqualsWithOnlySameType[A <: EqualsWithOnlySameType[A] : ClassTag) {
  override def equals(other: Any): Boolean = {
    other match {
      case (otherA: A) => super.equals(otherA)
      case _ => throw new RuntimeException(s"異なる型同士の比較を禁止しています: $this.equals($other)")
    }
  }
}

yoshihiro503

Fixpoint true_upto_n__true_everywhere
(* FILL IN HERE *)

Example true_upto_n_example :
    (true_upto_n__true_everywhere 3 (fun n => even n))
  = (even 3 -> even 2 -> even 1 -> forall m : nat, even m).
Proof. reflexivity.  Qed.

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 {

yoshihiro503

OCamlで説明するgen_serverの使い方

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

想定する読者

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

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

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

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

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.