yoshihiro503

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.

yoshihiro503

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.

yoshihiro503

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.

yoshihiro503

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のとき*)

yoshihiro503

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 [].

yoshihiro503

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

yoshihiro503

(** * Draft: The evolution of a Coq programmer *)

(** ** Freshman Coq programmer *)
Fixpoint fac n :=
  match n with
  | O => 1
  | S p => n * fac p
  end.

(* begin hide *) Reset fac. (* end hide *)

yoshihiro503

Require Import Nat.

Inductive Person :=
  | CPerson : nat -> option Person -> Person.

Definition 年齢 p :=
  let 'CPerson 年齢 配偶者 := p in 年齢.

Definition 配偶者 p :=
  let 'CPerson 年齢 配偶者 := p in 配偶者.

yoshihiro503

formatting

フォーマットに準拠しているか検査

dune build @fmt

強制的にフォーマット

dune build @fmt --auto-promote

yoshihiro503

int hoge(x) {
  int y = x + 1;
  return y;
}