オープンソースの数式処理システム
http://www.math.kobe-u.ac.jp/Asir/asir-ja.html
ここからダウンロード&インストール
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 |
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 := |
(* 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' -> |
(* 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' -> |
オープンソースの数式処理システム
http://www.math.kobe-u.ac.jp/Asir/asir-ja.html
ここからダウンロード&インストール
\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} |
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] |
module NeuralNetwork where | |
import Data.List | |
import System.Random | |
import Numeric.LinearAlgebra | |
learnCnst = 0.1 | |
sigmoid x = 1.0 / (1.0 + exp (-x)) |
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... |
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. |