This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
''' | |
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 | |
''' |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
''' | |
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 | |
''' |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
int fib( int n ){ | |
if( n <= 1 ){ | |
return n; | |
} | |
return fib( n - 1 ) + fib( n - 2 ); | |
} | |
int main(){ | |
return fib( 10 ); | |
} |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
#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)) |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
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. |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
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)). |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
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. | |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Require Import Omega. | |
Goal (221 * 293 * 389 * 397 + 17 = 14 * 119 * 127 * 151 * 313)%nat. | |
Proof. | |
omega. | |
Qed. |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
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. | |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
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. |