yoshihiro503

Coqのコードをopamに登録する方法

move to : https://qiita.com/yoshihiro503/items/822376f92a003fa99b71

yoshihiro503

mathcomp analysisのtopology.vにおいて，

...
Module PropInFilter : PropInFilterSig.
  Definition t := prop_in_filter_proj.
  ...
End PropInFilter.
Notation prop_of := PropInFilter.t.
...

yoshihiro503

From mathcomp Require Import all_ssreflect.
Require Import JMeq.

Inductive sizseq (T:Type) : nat -> Type :=
| SizNil : sizseq T 0
| SizCons n : T -> sizseq T n -> sizseq T n.+1.


Lemma sizseq0nil_aux (T:Type) n : forall xs : sizseq T n, n = 0 -> JMeq xs (SizNil T).
Proof.

yoshihiro503

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

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

yoshihiro503

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.

yoshihiro503

ここを見る: https://www.kyoto-u.ac.jp/ja/research/Additional-Position

yoshihiro503

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.

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.