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
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 |
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
(* | |
(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. |
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
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);} |
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 | |
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 := |
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
(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) |
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
#!/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 |
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
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. |
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 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. |
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
\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} |
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 <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); |
OlderNewer