Skip to content

Instantly share code, notes, and snippets.

View pi8027's full-sized avatar

Kazuhiko Sakaguchi pi8027

View GitHub Profile
89d185fa3e0d3620703ad4b723ef85695ce427da6235fe91d74fc22d1ffcfd5d coq-8.3pl5.tar.gz
f46ae5b6f0bea9dc299de6f3c020ee75c40581e32a1832e9a290d098a6a2424d coq-8.4.tar.gz
5d0e4553ab50677a94b4d5ca1650a90718e9362082a649ba95be4010390a0f80 coq-8.4pl1.tar.gz
fb719a38f613b01861e3b251e745a5c8ef395a26ce7029668e85ac75fcbca2d8 coq-8.4pl2.tar.gz
97583d637f981c5554007f4e99ce6420ebc737186b1d021bd71766fd891cfb38 coq-8.4pl3.tar.gz
85a728e28346dec378d5437f7c409eab20bd42aa528b5f873cb0c9827d5baaa3 mathcomp-1.5rc1.tar.gz
5d0769c1639dcccbfe57407591ddfc12dee163c46fc012b307f17aedb5ab4d1d ssreflect-1.4-coq8.3pl4.tar.gz
f044de8f75008000caf0ad61829f936384ee2d4b5fa40630352826c07b125dfb ssreflect-1.4-coq8.4.tar.gz
f85d8ced769b6c38a499681a52480f2e0b9b7a0a8f028a3d35ecd1794ae64fc2 ssreflect-1.5rc1.tar.gz
(*
(add-to-list 'coq-load-path "~/src/coq/regular/")
*)
Require Import
ssreflect ssrfun ssrbool eqtype ssrnat seq fintype div bigop prime.
Set Implicit Arguments.
Unset Strict Implicit.
Import Prenex Implicits.
char a[]="!!!!!!!!!!!!!!!Zi!sf!wc!z^![!!\"X!!!!o2*-!?+q0+-!>,q0+,!?-p0+,!?-p0+,!?-p0+,2$!--p0+,0&!--p0+,-##'!--p0+,,*!--p0*/&$#+.#.#@#4#@-,#e0+>-.$7-6,@,6R0-<+0$8.7)@)7T0/:)2$:.6(?'##7U018'4$<.6&@&6X0+>%6$>%#$#'6$@$6$#'#Q0+,++%,.,*-$/(,$,+-$,(.R0+,++%,.,*-$0',$,+-$,&0R0+,++%,.,*-$2%,$,+-$,$2R0+,++%,.,*-$4#,$,+-$>R0+,++%,.?$?$,+-$+#*#+R0+,++%,.,#4$,+,$,+-$)##,+R0+,++%,.,%2$,+,$,+-$'0+R0+,++%,.,(/$,+,$,+-$%##0+R0+,++%,--*-$,+,$,*.$#3,R0,+++%+/7,6/5##1##7Q0.)++%*27,6/5##/6T00'++%'77-5/5-6V11%++%&:7,6/5##'6x#++%$>7,7.5%6!!!!!!!!!!!!!!!l";i,j,o,m;main(){for(;a[i];i++){for(j=0;(a[i]+158)%96-j;j++)o++,putchar("@1"[m]),o%246||putchar('\n');(a[i]-33)&&(m=!m);}exit(1);}
Require Import
Coq.Relations.Relations Coq.Relations.Relation_Operators
Ssreflect.ssreflect Ssreflect.ssrfun Ssreflect.ssrbool Ssreflect.eqtype
Ssreflect.ssrnat Ssreflect.seq Omega.
Set Implicit Arguments.
Unset Strict Implicit.
Import Prenex Implicits.
Definition natE :=
(define-fun sub ((x Int) (y Int)) Int
(ite (< x y) 0 (- x y)))
(define-fun minn ((x Int) (y Int)) Int
(sub x (sub x y)))
(define-fun maxn ((x Int) (y Int)) Int
(+ x (sub y x)))
(assert (forall ((x Int) (y Int))
(implies (and (<= 0 x) (<= 0 y))
(= (minn x y) (minn y x)))))
(check-sat)
#!/bin/zsh
script=$(cat << EOT
{
:loop
p
s/0 \([^ ]*\)\([01]\) +O/ \1 +O\2/ ; t loop
s/1 \([^ ]*\)0 +O/ \1 +O1/ ; t loop
s/1 \([^ ]*\)1 +O/ \1 +I0/ ; t loop
s/0 \([^ ]*\)0 +I/ \1 +O1/ ; t loop
Goal forall (f g : nat -> nat),
(forall x, f x = f (g x)) ->
(forall x, f (g x) = f (S x)) ->
f 0 = f 100.
Proof.
intros f g H H0.
Fail congruence.
repeat rewrite <- H0, <- H.
reflexivity.
Qed.
@pi8027
pi8027 / gist:0e50404fe879d95a7bbe
Last active August 29, 2015 14:13
omega nightmare
Require Import Omega Psatz.
Open Scope Z.
Goal forall x y, x * 2 <= y -> 5 - 3 * x <= 4 * y -> 4 * y <= x + 6 -> False.
Proof.
intros x y.
Fail omega.
lia.
Qed.
@pi8027
pi8027 / gist:5c2ecfd94e1a8364dd7a
Last active August 29, 2015 14:13
全てのページの左上にコンパイルした日時を出力する
\usepackage[yyyymmdd,hhmmss]{datetime}
\usepackage[all]{background}
\usepackage{tikz}
\SetBgContents{
\begin{tikzpicture}[remember picture,overlay, color=black!60]
\draw (-1, 1) node[below right] {\LARGE{\texttt{\today~\currenttime}}};
\end{tikzpicture}
}
\SetBgPosition{current page.south west}
#include <stdio.h>
#define binary_to_gray_code(binary) ((binary)^(binary)>>1)
int fputb(unsigned int input,unsigned int digit,FILE *output)
{
if(digit){
fputb(input>>1,digit-1,output);
fputc('0'+(input&1),stdout);