Library FreeSpec.Core.Init
Definition when {m : Type → Type} `{Monad m} (cond : bool) `(p : m a) : m unit :=
if cond then (p;; pure tt) else pure tt.
From Coq Require Export Eqdep.
Ltac ssubst :=
lazymatch goal with
| [ H : existT _ _ _ = existT _ _ _ |- _ ]
⇒ apply Eqdep.EqdepTheory.inj_pair2 in H; ssubst
| [ |- _] ⇒ subst
end.
Declare Scope freespec_scope.
Delimit Scope freespec_scope with freespec.
Reserved Infix "===" (at level 70, no associativity).
Notation "m '~>' n" :=
(∀ (α : Type), m α → n α)
(at level 80, no associativity)
: type_scope.
Definition function_eq {a b} (r : b → b → Prop) (f g : a → b) : Prop :=
∀ (x : a), r (f x) (g x).
#[program]
Instance function_eq_Equivalence `(Equivalence b r)
: @Equivalence (a → b) (function_eq r).
Next Obligation.
now intros f x.
Qed.
Next Obligation.
intros f g equ x.
symmetry.
apply equ.
Qed.
Next Obligation.
intros f g h equ1 equ2 x.
transitivity (g x); [ apply equ1 | apply equ2 ].
Qed.
#[global]
Create HintDb freespec.