erutuf

Require Import List.
Import ListNotations.

Inductive State := Q1 | Q2.
Inductive Alphabet := A | B.

Inductive trans : State -> Alphabet -> State -> Prop :=
| tr1A : trans Q1 A Q2
| tr1B : trans Q1 B Q1
| tr2A : trans Q2 A Q1

erutuf

Add LoadPath "/Users/erutuf/Documents/mit/fiat/src" as Fiat.
Require Import Fiat.Common Fiat.Computation
  Fiat.ADTRefinement Fiat.ADTNotation Fiat.ADTRefinement.BuildADTRefinements.
Require Import List Omega.

Set Implicit Arguments.
Set Regular Subst Tactic.
Import ListNotations.

Inductive removed A : nat -> list A -> list A -> Prop :=

erutuf

(* sample code of automatic differentiation in Coq *)

Require Import QArith.
Open Scope Q_scope.

Definition QFunc := Q -> Q.

Parameter der_rel : QFunc -> QFunc -> Prop.

Axiom add_der : forall f g f' g', der_rel f f' -> der_rel g g' ->

erutuf

(* sample code of automatic differentiation in Coq *)

Require Import QArith.
Open Scope Q_scope.

Definition QFunc := Q -> Q.

Parameter der_rel : QFunc -> QFunc -> Prop.

Axiom add_der : forall f g f' g', der_rel f f' -> der_rel g g' ->

erutuf

Risa/Asir で D 加群の積分を計算

Risa/Asir

オープンソースの数式処理システム

http://www.math.kobe-u.ac.jp/Asir/asir-ja.html

ここからダウンロード&インストール

erutuf

\ProvidesPackage{beamerthemeErutuf}
\mode<presentation>

%% font size
\setbeamerfont{title}{parent=structure,size=\Large}
\setbeamerfont{section in head/foot}{size=\tiny,series=\bfseries}
\setbeamerfont{frametitle}{parent=structure,size=\Large,series=\bfseries}
\setbeamerfont{framesubtitle}{parent=frametitle,size=\large}
\setbeamerfont{itemize/enumerate body}{size=\normalsize}
\setbeamerfont{itemize/enumerate subbody}{size=\small}

erutuf

module NeuralNetwork where

import Data.List
import System.Random
import Control.Monad
import Numeric.LinearAlgebra

learnCnst = 0.01

addThres v = vector $ toList v ++ [1.0]

erutuf

module NeuralNetwork where

import Data.List
import System.Random
import Numeric.LinearAlgebra

learnCnst = 0.1

sigmoid x = 1.0 / (1.0 + exp (-x))

erutuf

Require Import List.

Variable A B : Type.

Theorem fold_symmetric2 : forall (f : A -> B -> A) (g : B -> A -> A),
  (forall x y, f x y = g y x) ->
  forall x l, fold_left f l x = fold_right g x (rev l).
Proof with simpl in *; intuition.
intros f g H x l. revert x.
induction l...

erutuf

Require Import ssreflect.

Lemma exo5 : forall A B C : Prop, A /\ B <-> B /\ A.
Proof.
move=> A B P.
split.
  case.
  move=> a b.
  split.
    exact b.