# Library StdNotations

A few standard notations and tactics
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} + {xy}.

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

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

We note f[xv] the function identical to f everywhere except for x for which it returns v
Notation "E [ X ↦ V ]" := (subst _ _ E X V) (at level 100).

Associated tactics

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), rr'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].

A generic notation for triples
Class Triple (A B C D:Type) : Type := {
cons : ABCD
}.

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).