mathink

Set Implicit Arguments.
Unset Strict Implicit.

Class Setoid :=
  {
    carrier: Type;
    equal: carrier -> carrier -> Prop
  }.
Coercion carrier: Setoid >-> Sortclass.
Notation "x == y" := (equal x y) (at level 90, no associativity).

mathink

Set Implicit Arguments.
Unset Strict Implicit.

Class Setoid :=
  {
    carrier: Type;
    equal: carrier -> carrier -> Prop
  }.
Coercion carrier: Setoid >-> Sortclass.
Notation "x == y" := (equal x y) (at level 90, no associativity).

mathink

Require Import Program Arith.

(** * リストモジュールの拡張 *)
Module List.
  Require Export List.
 
  Fixpoint _index_of_loop {A:Type} (eq_dec : forall (x y:A),{x=y}+{x<>y}) a xs i :=
    match xs with
    | nil => None
    | x::xs => if eq_dec x a then Some i else _index_of_loop eq_dec a xs (S i)

mathink

(** 
 * Do do notation with Notation
 Haskell の do 記法はモナディックな計算を [<-] を使って命令的に記述するためのもの。
 つまり、 do 内部の記述は解釈の仕方が外部と異なる。

 ここでは、 Coq の Arguments コマンドや Notation コマンドを用いて同様のコンセプトを実現する。
 すなわち、Coq に於ける Monad の do 記法を実装する。
 **)

Set Implicit Arguments.

mathink

Set Implicit Arguments.
Set Universe Polymorphism.

Fail Inductive JMeq (A:Type)(x:A): forall B: Type, B -> Prop :=
| JMeq_refl: JMeq x x.
(* JMeq is defined *)
(* The command has indeed failed with message: *)
(* Incorrect elimination of "j" in the inductive type "JMeq": *)
(* ill-formed elimination predicate. *)

mathink

Set Implicit Arguments.
Unset Strict Implicit.

Inductive m (X: Type)(F: Type -> Type)(P: forall X, F X -> Prop) :=
| cTT: forall (x: F X),  P X x  -> m X P.

Record Wrap (X: Type) := wrap { get: X }.
  
Inductive T1 :=
| cT1: m T1 (fun X (w: Wrap X) => w = w) -> T1.

mathink

Set Implicit Arguments.
Unset Strict Implicit.

Record Wrap (X: Type) := wrap { get: X }.
  
Inductive TT (X: Type)(F: Type -> Type)(P: forall X, F X -> Prop) :=
| cTT: forall (x: F X),  P X x  -> TT X P.

Inductive T :=
| cT: TT T (fun X (w: Wrap X) => w = w) -> T.

mathink

Set Implicit Arguments.
Unset Strict Implicit.
 
Generalizable All Variables.
 
Require Export Basics Tactics Coq.Setoids.Setoid Morphisms.
 
Structure Setoid :=
  {
    carrier:> Type;

mathink

Set Implicit Arguments.
Set Contextual Implicit.

Definition compose {X Y Z: Type}(f: X -> Y)(g: Y -> Z)(x: X): Z := g (f x).
Notation "g \o f" := (compose f g) (at level 60, right associativity).

Inductive list (X: Type): Type := nil | cons (h: X)(t: list X).
Notation "[]" := nil.
Notation "[ x ]" := (cons x nil).
Notation "[ x ; .. ; y ]" := (cons x .. (cons y nil) .. ).

mathink

(* Categorical Abstract Machine *)
Set Implicit Arguments.
Unset Strict Implicit.
Set Contextual Implicit.
Require Import Arith.
Require Import List.
Import ListNotations.

(** * Monad *)
Class Monad :=