Skip to content

Instantly share code, notes, and snippets.

View ryuta-ito's full-sized avatar

Ryuta Ito ryuta-ito

1 follower · 1 following
View GitHub Profile
@ryuta-ito
ryuta-ito / ssreflect_terminology.md
Last active November 6, 2018 12:19
  • collective predicate x \in P
  • applicative predicate P x
@ryuta-ito
ryuta-ito / finite_ordinal.v
Last active November 3, 2018 02:22
Set Printing Coercions.
Require Import Omega.
Inductive hoge (n:nat) : Type :=
| fuga (m:nat) : m < n -> hoge n.
Coercion nat_of_hoge {n:nat} (h : hoge n) :=
match h with
| fuga _ n _ => n
end.
@ryuta-ito
ryuta-ito / ssreflect_example.md
Last active November 11, 2018 00:27 
Set Printing Coercions.

utils

let pattern match

Inductive hoge :=
| fuga : forall (n:nat), hoge.

Eval simpl in let: fuga n := fuga 10 in n.
@ryuta-ito
ryuta-ito / coq_notation.md
Last active November 10, 2018 06:49

sigma type

Require Import Omega.

Print sig. (* Σx:A B(x) *)
(* Inductive sig (A : Type) (P : A -> Prop) : Type := *)
(* exist : forall x : A, P x -> {x : A | P x}         *)
(* For sig: Argument A is implicit                    *)
(* For exist: Argument A is implicit                  *)
@ryuta-ito
ryuta-ito / kernel_is_group.v
Created October 27, 2018 11:11
Definition set (M : Type) := M -> Prop.
Definition belongs {M : Type} (x : M) (P : set M) : Prop := P x.
Arguments belongs {M} x P /.
Definition map {M M' : Type} f (A : set M) (B : set M') :=
forall x, belongs x A -> belongs (f x) B.
Arguments map {M M'} f A B /.
Class group (M : Type) := {
cset : set M;
@ryuta-ito
ryuta-ito / map_rel_example.v
Created October 20, 2018 00:59
Definition gen_rel (X Y : Type) := X -> Y -> Prop.
Definition map_rel {X Y : Type} (R : gen_rel X Y) :=
forall x x', x = x' -> forall y y', R x y -> R x' y' -> y = y'.
Arguments map_rel {X Y} R/.
Definition map_rel' {X Y : Type} (R : gen_rel X Y) :=
forall x, exists! y, R x y.
Arguments map_rel' {X Y} R/.
@ryuta-ito
ryuta-ito / bijection_iff_has_inverse.v
Created October 8, 2018 13:09
Definition relation (X Y : Type) := X -> Y -> Prop.
Structure map X Y := {
R : relation X Y;
map_law : forall x, exists! y, R x y
}.
Definition is_map {X Y : Type} (R : relation X Y) :=
forall x, exists! y, R x y.
@ryuta-ito
ryuta-ito / group_defined_structure.v
Created September 26, 2018 13:47
Structure group M := {
id : M;
bin : M -> M -> M;
inverse : M -> M;
assoc : forall x y z, bin x (bin y z) = bin (bin x y) z;
idR : forall g, bin g id = g;
idL : forall g, bin id g = g;
invR : forall g, bin g (inverse g) = id;
invL : forall g, bin (inverse g) g = id
}.
@ryuta-ito
ryuta-ito / symmetric_group.v
Last active September 23, 2018 07:32
Definition set (M : Type) := M -> Prop.
Definition belongs {M : Type} (x : M) (P : set M) : Prop := P x.
Definition subset {M : Type} (S T : set M) :=
forall s, belongs s S -> belongs s T.
Definition id {M : Type} (S : set M) (id : M) (bin : M -> M -> M) :=
forall s, belongs s S -> bin s id = s /\ bin id s = s.
Definition identity {M : Type} (S : set M) (bin : M -> M -> M) :=
exists e, id S e bin.
@ryuta-ito
ryuta-ito / simple_set_example.v
Last active September 23, 2018 00:41
Definition set (M : Type) := M -> Prop.
Definition belongs {M : Type} (x : M) (P : set M) : Prop := P x.
Definition subset {M : Type} (S T : set M) :=
forall s, belongs s S -> belongs s T.
Definition id {M : Type} (S : set M) (id : M) (bin : M -> M -> M) :=
forall s, belongs s S -> bin s id = s /\ bin id s = s.
Axiom id_belongs : forall {M : Type} (S : set M) (id_ : M) bin,
id S id_ bin -> belongs id_ S.