Require Import

Section contents.

Context (operation: Set) (operation_type: operation OpType unit).

Let sign := Build_Signature unit operation operation_type.

Definition M (T: Type): Type := Term sign T (ne_list.one tt).

Section equality.

Context {A: Type} `{Setoid A}.

Fixpoint geneq {s s'} (x: Term sign A s) (y: Term sign A s'): Prop :=
match x, y with
| Var v _, Var w _ => v = w
| App _ z t t', App _ z' t'' t''' => geneq t t'' geneq t' t'''
| Op o, Op o' => o o'
| _, _ => False
end.

Lemma geneq_sym s (x: Term sign A s): s' (y: Term sign A s'), geneq x y geneq y x.

Lemma geneq_trans s (x: Term sign A s): s' (y: Term sign A s') s'' (z: Term sign A s''),
geneq x y geneq y z geneq x z.

Global Instance Me: Equiv (M A) := geneq.

Instance: Symmetric Me.

Instance: Transitive Me.

Instance: Reflexive Me.

Global Instance: Setoid (M A).
End equality.

Definition gen_bind {A B: Type} (f: A M B): {s}, Term sign A s Term sign B s
:= fix F {s} (t: Term sign A s): Term sign B s :=
match t with
| Var v tt => f v
| App o z x y => App _ _ _ z (F x) (F y)
| Op o => Op _ _ o
end.

Implicit Arguments gen_bind [[A] [B] [s]].

Instance: MonadBind M := λ _ _ z f, gen_bind f z.

Instance: `{Equiv A} `{Equiv B},
Proper ((=) ==> ((=) ==> (=)) ==> (=)) (@bind M _ A B).

Instance: MonadReturn M := λ _ x, Var sign _ x tt.

Instance: `{Equiv A}, Proper ((=) ==> (=)) (@ret M _ A).