pi8027

Require Import mathcomp.ssreflect.all_ssreflect.

Goal forall p k n, 1 < p -> p ^ k <= n < p ^ k.+1 -> trunc_log p n = k.
Proof.
move => p k n H /andP [H0 H1].
have/(trunc_log_bounds H)/andP [H2 _] : 0 < n
  by apply: (leq_trans _ H0); rewrite expn_gt0 (ltnW H).
apply/eqP; rewrite eqn_leq trunc_log_max // andbT.
move: H1; apply contraTT; rewrite -leqNgt -ltnNge => H1.
by apply: (leq_trans _ H2); rewrite leq_exp2l.

pi8027

diff --git a/automata.v b/automata.v
index e63d92e..305988a 100644
--- a/automata.v
+++ b/automata.v
@@ -1,5 +1,5 @@
 (** Authors: Christian Doczkal and Jan-Oliver Kaiser *)
-Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq choice fintype path fingraph  finfun  finset.
+Require Import mathcomp.ssreflect.all_ssreflect.
 Require Import misc regexp.
 

pi8027

\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}

pi8027

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

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

#!/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

pi8027

(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)

pi8027

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 :=

pi8027

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);}

pi8027

(*
(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.