satos---jp

## coq_practice_31.v
(* Section の練習 *)

Section Poslist.
  (* このセクションの中では、Aが共通の変数として使える。 *)
  Variable A : Type.
  (* 非空なリスト *)
  Inductive poslist : Type :=
     nil : A -> poslist | cons : A -> poslist -> poslist.


## coq_practice_32.v
Require Import Arith.

Module Type SemiGroup.
  Parameter G : Type.
  Parameter mult : G -> G -> G.
  Axiom mult_assoc :
    forall x y z : G, mult x (mult y z) = mult (mult x y) z.
End SemiGroup.
Print SemiGroup.
Module NatMult_SemiGroup <: SemiGroup.

## coq_practice_28.v
Require Import Reals.
Require Import Fourier.

Theorem PI_RGT_3_05 : (PI > 3 + 5/100)%R.
Proof.
  assert (((sum_f_R0 (tg_alt PI_tg) (S (2 * 5)))%R <= (PI / 4)%R <=
    (sum_f_R0 (tg_alt PI_tg) (2 * 5))%R)%R).
  apply PI_ineq.
  simpl H.
  destruct H.

## coq_practice_33.v
Require Import Arith.

Module Type Monoid.
  Parameter G : Type.
  Parameter mult : G -> G -> G.
  Parameter E : G.
  Axiom mult_assoc :
    forall x y z : G, mult x (mult y z) = mult (mult x y) z.
  Axiom identity_element1 :
    forall x : G, mult x E = mult E x.

## coq_practice_36.v
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.
    unfold proj1_sig.

## coq_practice_37.v
Require Import SetoidClass.
Require Import Arith.

Record int := {
  Ifst : nat;
  Isnd : nat
}.

Program Instance ISetoid : Setoid int := {|
  equiv x y := Ifst x + Isnd y = Ifst y + Isnd x

## Ａ言語コンペ_オートマトン
RrIdPAVa+r1:IdAVb+r1:IdAiIsAp1RrLi?=Tr1iSa\ApVap::ApVbp::Op

## Ａ言語コンペ＿クワイン
ApSApSOT0,3pOpO+Mc92T3,20p\OT0,3pOpO+Mc92T3,20p

## GoogleのDoodleのTuringMachineのやつ
Dim k As Integer
Dim x As Byte
Dim y As Byte
Dim yoko As Byte
Dim gyou As Byte


Sub tyuring()
x = 1

## MMA CTF 1st 2015で、I言語のquineを製作するために書いたやつ(excelのvba)
Dim A(1000) As Integer
Dim top, pc, isend

Dim s As String

Dim out As String


Sub initi()
	(* Section の練習 *)

	Section Poslist.
	(* このセクションの中では、Aが共通の変数として使える。 *)
	Variable A : Type.
	(* 非空なリスト *)
	Inductive poslist : Type :=
	nil : A -> poslist \| cons : A -> poslist -> poslist.
	Require Import Arith.

	Module Type SemiGroup.
	Parameter G : Type.
	Parameter mult : G -> G -> G.
	Axiom mult_assoc :
	forall x y z : G, mult x (mult y z) = mult (mult x y) z.
	End SemiGroup.
	Print SemiGroup.
	Module NatMult_SemiGroup <: SemiGroup.
	Require Import Reals.
	Require Import Fourier.

	Theorem PI_RGT_3_05 : (PI > 3 + 5/100)%R.
	Proof.
	assert (((sum_f_R0 (tg_alt PI_tg) (S (2 * 5)))%R <= (PI / 4)%R <=
	(sum_f_R0 (tg_alt PI_tg) (2 * 5))%R)%R).
	apply PI_ineq.
	simpl H.
	destruct H.
	Require Import Arith.

	Module Type Monoid.
	Parameter G : Type.
	Parameter mult : G -> G -> G.
	Parameter E : G.
	Axiom mult_assoc :
	forall x y z : G, mult x (mult y z) = mult (mult x y) z.
	Axiom identity_element1 :
	forall x : G, mult x E = mult E x.
	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.
	unfold proj1_sig.
	Require Import SetoidClass.
	Require Import Arith.

	Record int := {
	Ifst : nat;
	Isnd : nat
	}.

	Program Instance ISetoid : Setoid int := {\|
	equiv x y := Ifst x + Isnd y = Ifst y + Isnd x
	Dim k As Integer
	Dim x As Byte
	Dim y As Byte
	Dim yoko As Byte
	Dim gyou As Byte



	Sub tyuring()
	x = 1
	Dim A(1000) As Integer
	Dim top, pc, isend

	Dim s As String

	Dim out As String



	Sub initi()