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
ryuta-ito
/ finite_ordinal.v
Last active
November 3, 2018 02:22
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| 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
/ coq_notation.md
Last active
November 10, 2018 06:49
ryuta-ito
/ kernel_is_group.v
Created
October 27, 2018 11:11
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| 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
/ map_rel_example.v
Created
October 20, 2018 00:59
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| 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
/ bijection_iff_has_inverse.v
Created
October 8, 2018 13:09
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| 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
/ group_defined_structure.v
Created
September 26, 2018 13:47
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| 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
/ symmetric_group.v
Last active
September 23, 2018 07:32
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| 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
/ simple_set_example.v
Last active
September 23, 2018 00:41
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| 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. |
ryuta-ito
/ inverse_map_uniq.v
Last active
September 19, 2018 13:28
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Definition obj := Type. | |
| Inductive map : Type := | |
| | Id : obj -> map | |
| | Diff : obj -> obj -> map | |
| | Comp : map -> map -> map. | |
| Inductive hom : map -> obj -> obj -> Prop := | |
| | HomId : forall f a, | |
| f = Id a -> hom f a a |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| -- P(x, y) <=> x < y | |
| -- f(x, y) = (μz < y)[P(x, z)] | |
| p x y = x < y | |
| f x 0 = 0 | |
| f x y = h x (y-1) (f x (y-1)) | |
| h x y g | g < y = f x y | |
| | g == y && p x y = y | |
| | otherwise = y + 1 |