joisino

'''
Implementation of batch normalization with chainer

http://joisino.hatenablog.com/entry/2017/07/09/210000

Copyright (c) 2017 joisino
Released under the MIT license
http://opensource.org/licenses/mit-license.php
'''

joisino

'''
Implementation of GAN with chainer

http://joisino.hatenablog.com/entry/2017/07/06/210000

Copyright (c) 2017 joisino
Released under the MIT license
http://opensource.org/licenses/mit-license.php
'''

joisino

int fib( int n ){
  if( n <= 1 ){
    return n;
  }
  return fib( n - 1 ) + fib( n - 2 );
}
int main(){
  return fib( 10 );
}

joisino

#include <bits/stdc++.h>
      
#define FOR(i,a,b) for( ll i = (a); i < (ll)(b); i++ )
#define REP(i,n) FOR(i,0,n)
#define YYS(x,arr) for(auto& x:arr)
#define ALL(x) (x).begin(),(x).end()
#define SORT(x) sort( (x).begin(),(x).end() )
#define REVERSE(x) reverse( (x).begin(),(x).end() )
#define UNIQUE(x) (x).erase( unique( ALL( (x) ) ) , (x).end() )
#define PW(x) (1LL<<(x))

joisino

Ltac split_all := repeat try split.

(* 以下は動作確認用 *)

Lemma bar :
  forall P Q R S : Prop,
    R -> Q -> P -> S -> (P /\ R) /\ (S /\ Q).
Proof.
  intros P Q R S H0 H1 H2 H3.
  split_all.

joisino

Require Import ZArith.

Section Principal_Ideal.
  Variable a : Z.

  Definition pi : Set := { x : Z | ( a | x )%Z }.

  Program Definition plus(a b : pi) : pi := (a + b)%Z.
  Next Obligation.
    apply (Z.divide_add_r a (proj1_sig a0) (proj1_sig b)).

joisino

Inductive pos : Set :=
  | S0 : pos
  | S : pos -> pos.
 
Fixpoint plus(n m:pos) : pos :=
  match n with
  | S0 => S m
  | S p => S( plus p m )
  end.
 

joisino

Require Import Omega.

Goal (221 * 293 * 389 * 397 + 17 = 14 * 119 * 127 * 151 * 313)%nat.
Proof.
  omega.
Qed.

joisino

Require Import Arith.
 
Definition Nat : Type :=
  forall A : Type, (A -> A) -> (A -> A).
 
Definition NatPlus(n m : Nat) : Nat :=
  fun (A:Type)(f:A->A)(x:A) => ((n A) f)(((m A) f) x).
 
Definition nat2Nat : nat -> Nat := nat_iter.
 

joisino

Parameter G : Set.
Parameter mult : G -> G -> G.
Notation "x * y" := (mult x y).
Parameter one : G.
Notation "1" := one.
Parameter inv : G -> G.
Notation "/ x" := (inv x).
(* Notation "x / y" := (mult x (inv y)). *) (* 使ってもよい *)

Axiom mult_assoc : forall x y z, x * (y * z) = (x * y) * z.