erutuf

module Joshiryoku where

infix 1 >_< ^_^ ・_・
infix 2 （_） [_]
infix 3 o_o ∩_∩ ☜_☞

data Mouse : Set where
    O : Mouse
    - : Mouse
    ω : Mouse

erutuf

open List;;

let rec seq n m = if n > m then [] else n :: seq (n + 1) m;;

let rec safe x n = function
    | [] -> true
    | y::ys -> x <> y && x <> y + n && x <> y - n && safe x (n + 1) ys;;

let concmap f xs = concat (map f xs)

erutuf

Require Import List.
Require Import Bool.
Require Import Bool.Sumbool.

Ltac find_if :=
  match goal with
  | H:context[if ?X then _ else _] |- _ => destruct X as ()_eqn
  | |- context[if ?X then _ else _] => destruct X as ()_eqn
  end.

erutuf

Inductive even : nat -> Prop :=
| even_O : even 0
| even_S : forall n, odd n -> even (S n)
with odd : nat -> Prop :=
| odd_S : forall n, even n -> odd (S n).

Scheme even_mut := Induction for even Sort Prop
  with odd_mut := Induction for odd Sort Prop.

Theorem daigakuseinosuugakuryoku : forall n m, 

erutuf

Require Import Program.Basics.
Require Import Arith.Le.
Require Import Omega.
Require Import Classes.Equivalence.
Require Import Classes.SetoidClass.

Set Implicit Arguments.
Unset Strict Implicit.

erutuf

Require Import Arith.
Require Import List.

Open Scope list_scope.

Import ListNotations.

Variable String : Type.

Axiom string_eq_dec : forall s1 s2 : String, {s1 = s2} + {s1 <> s2}.

erutuf

Require Import List.

Open Scope list_scope.

Import ListNotations.

Variable String : Type.

Axiom string_eq_dec : forall s1 s2 : String, {s1 = s2} + {s1 <> s2}.

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.

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

module NeuralNetwork where

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

learnCnst = 0.1

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