YOSHIHIRO Imai yoshihiro503

## coqtokyo_EqClass_sort2.v
From mathcomp Require Import all_ssreflect.
Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.

(* :> を複数持つと予期せぬことがおきることがあるぞ *)
Structure S : Type := MakeS {
  sort2 :> Type;
  sort :> Type;

## mathcompbook_edivn.v
From mathcomp Require Import all_ssreflect.

Fixpoint evivn_rec pred_d m q :=
  if m - pred_d is m'.+1 then edivn_rec pred_d m' q.+1 else (q, m).

Definition edivn m d := if d > 0 then edivn_rec d.-1 m 0 else (0, m).

Lemma edivn_recP1 q r m pred_d q0:
  (q, r) = edivn_rec pred_d m q0 ->
  r < pred_d.+1.

## 民間企業が京都大学教職員へ技術顧問として兼業依頼する方法.md

      
              1 file
            
          
              0 forks
            
          
              0 comments
            
          
              0 stars
            
          
                yoshihiro503
                / 民間企業が京都大学教職員へ技術顧問として兼業依頼する方法.md
            
            
              Last active
              February 21, 2024 03:41
            
          
    ここを見る: https://www.kyoto-u.ac.jp/ja/research/Additional-Position

  
## DMM_Coq_School_Day4.v
Require Import String List.
Import ListNotations.
Open Scope string_scope.

Definition aaa := 1+2.
Definition bbb := aaa * 5.

Definition foo x y:= 2*x + y.
Compute foo 1 2.

## kobayashi_qa.v
Require Import Arith Unicode.Utf8.

Definition f (n : nat) :=
  n - 1.

Inductive reaches_1 : nat → Prop :=
  | term_done : reaches_1 1
  | term_more (n : nat) : reaches_1 (f n) → reaches_1 n.

Check reaches_1_ind.

## coqtokyo_question_0927_without_ssreflect.v
Require Import Arith.

Lemma test_000: forall a b c : nat, a + b + c = b + c + a.
Proof.
  intros a b c. now rewrite (Nat.add_comm a b), Nat.add_shuffle0.
Qed.

Lemma test_001: forall m : nat, 2 ^ (S m) = 2 * 2 ^ m.
Proof. reflexivity. Qed.

## coqtokyo_question_0927.v
From mathcomp Require Import ssreflect ssrnat div.


Lemma test_000: forall a b c : nat, a + b + c = b + c + a.
Proof.
  move=> a b c.
  rewrite (_: b + c = c + b).
  - by apply addnCAC.
  - by apply addnC.
Qed.

## contrapositive_bool.v
Theorem contrapositive_bool : forall (p q : bool),
  (p = true -> q = true) -> (q = false -> p = false).
Proof.
  intros p q H Hq.
  destruct p. (* pで場合分け*)
  - (* pがtrueのとき *)
    rewrite H in Hq.
    + discriminate Hq.
    + reflexivity.
  - (* pがfalseのとき*)

## placticing_mathcomp.v
From mathcomp Require Import all_ssreflect.

Lemma rensyu : forall i x y,
    i != 0 -> (x - y) = 0 -> x.+1 - y <= i.
Proof.
  move=> i x y i0 /eqP xy.
  rewrite -addn1.
  rewrite leq_subLR.
  apply: leq_add.
    by [].

## verify_plebeia_merkle_proof.ml
open SCaml

let empty_bytes = Bytes "0x"
let is_empty_bytes b = (Bytes.length b = Nat 0)

let bytes_concat sep ss =
  match ss with
  | [] -> empty_bytes
  | s0 :: ss ->
    List.fold_left' (fun (acc, s) -> Bytes.concat (Bytes.concat acc sep) s) s0 ss
	From mathcomp Require Import all_ssreflect.
	Set Implicit Arguments.
	Unset Strict Implicit.
	Unset Printing Implicit Defensive.

	(* :> を複数持つと予期せぬことがおきることがあるぞ *)
	Structure S : Type := MakeS {
	sort2 :> Type;
	sort :> Type;
	From mathcomp Require Import all_ssreflect.

	Fixpoint evivn_rec pred_d m q :=
	if m - pred_d is m'.+1 then edivn_rec pred_d m' q.+1 else (q, m).

	Definition edivn m d := if d > 0 then edivn_rec d.-1 m 0 else (0, m).

	Lemma edivn_recP1 q r m pred_d q0:
	(q, r) = edivn_rec pred_d m q0 ->
	r < pred_d.+1.
	Require Import String List.
	Import ListNotations.
	Open Scope string_scope.

	Definition aaa := 1+2.
	Definition bbb := aaa * 5.

	Definition foo x y:= 2*x + y.
	Compute foo 1 2.
	Require Import Arith Unicode.Utf8.

	Definition f (n : nat) :=
	n - 1.

	Inductive reaches_1 : nat → Prop :=
	\| term_done : reaches_1 1
	\| term_more (n : nat) : reaches_1 (f n) → reaches_1 n.

	Check reaches_1_ind.
	Require Import Arith.

	Lemma test_000: forall a b c : nat, a + b + c = b + c + a.
	Proof.
	intros a b c. now rewrite (Nat.add_comm a b), Nat.add_shuffle0.
	Qed.

	Lemma test_001: forall m : nat, 2 ^ (S m) = 2 * 2 ^ m.
	Proof. reflexivity. Qed.
	From mathcomp Require Import ssreflect ssrnat div.


	Lemma test_000: forall a b c : nat, a + b + c = b + c + a.
	Proof.
	move=> a b c.
	rewrite (_: b + c = c + b).
	- by apply addnCAC.
	- by apply addnC.
	Qed.
	Theorem contrapositive_bool : forall (p q : bool),
	(p = true -> q = true) -> (q = false -> p = false).
	Proof.
	intros p q H Hq.
	destruct p. (* pで場合分け*)
	- (* pがtrueのとき *)
	rewrite H in Hq.
	+ discriminate Hq.
	+ reflexivity.
	- (* pがfalseのとき*)
	From mathcomp Require Import all_ssreflect.

	Lemma rensyu : forall i x y,
	i != 0 -> (x - y) = 0 -> x.+1 - y <= i.
	Proof.
	move=> i x y i0 /eqP xy.
	rewrite -addn1.
	rewrite leq_subLR.
	apply: leq_add.
	by [].
	open SCaml

	let empty_bytes = Bytes "0x"
	let is_empty_bytes b = (Bytes.length b = Nat 0)

	let bytes_concat sep ss =
	match ss with
	\| [] -> empty_bytes
	\| s0 :: ss ->
	List.fold_left' (fun (acc, s) -> Bytes.concat (Bytes.concat acc sep) s) s0 ss