Library StdNotations

Require Import Utf8.

Ltac inv H := inversion H ; try subst ; clear H.
Ltac add_eq expr val := set (temp := expr) ; generalize (refl_equal temp) ; unfold temp at 1 ; generalize temp ; intro val ; clear temp.
Ltac dup H H' := assert (H':= H).

Definition is_dec (A: Type) := ∀ (x y : A),{x=y} + {x ≠ y}.

Class EqDec (A:Type) : Type := {
  eq_dec : is_dec A
}.

Definition subst {Var} (eq : EqDec Var) (A:Type)
  (env : Var → A) (x:Var) (v:A) : Var → A :=
  fun vr ⇒
  if eq_dec vr x then v else env vr.

Notation "E [ X ↦ V ]" := (subst _ _ E X V) (at level 100).

Lemma subst_eq : ∀ (T:Type) (Eq : EqDec T) (X:Type) e (r: T) (k:X), subst Eq X e r k r = k.

Lemma subst_neq : ∀ (T:Type) (Eq : EqDec T) (X:Type) e (r r': T) (k:X), r ≠ r' → subst Eq X e r k r' = e r'.


Ltac subst_g X Y :=
  let h := fresh in destruct (eq_dec X Y) as [h | h] ;
    [ subst; try rewrite (subst_eq ) | rewrite (subst_neq ) ; auto].

Ltac subst_h X Y H :=
  let h := fresh in destruct (eq_dec X Y) as [h | h] ;
    [ subst; try rewrite (subst_eq ) in H | rewrite (subst_neq ) in H ; auto].

Class Triple (A B C D:Type) : Type := {
  cons : A → B → C → D
}.

Definition mkT {A} {B} {C} {D} (tr : Triple A B C D) (a : A) (b:B) (c:C) : D :=
  cons a b c.

Notation "[ A , B , C ]" := (mkT _ A B C) (at level 110).