Library letter

Parameter Name : Set.
Parameter τ_nm : Name list Atom.
Parameter beq_name : Name Name bool.
Axiom beq_name_spec : x y, reflect (x=y) (beq_name x y).
Axiom τ_nm_spec : a, NoDup (τ_nm a).

Definition is_perm x := p, p (snd x) = τ_nm (fst x).
Parameter get_new : list Atom Atom.
Axiom new_atom : l, ¬In (get_new l) l.

Fixpoint transfer_perm l m :=
match (l,m) with
| ([],_) |(_,[])[]
| (a::l,b::m)
let q :=(transfer_perm l m) in
let n := get_new (l++(elements q)) in
([b,n]++q++[a,n])
end.
Lemma is_perm_no_dup_length m l :
NoDup l NoDup m length l = length m
(transfer_perm l m) l = m.
Definition nodup_bool (l : list Atom):=
(forallb (fun x(count_occ Atom_eq_dec l x) =? 1) l).
Lemma nodup_bool_spec l : reflect (NoDup l) (nodup_bool l).

Definition is_perm_bool x :=
(length (snd x) =? length (τ_nm (fst x))) && (nodup_bool (snd x)).

Lemma is_perm_bool_spec x : reflect (is_perm x) (is_perm_bool x).
Lemma is_perm_bool_is_perm x :
is_perm x is_perm_bool x = true.

Definition Letter := { x | is_perm_bool x = true}.
Definition beq_letter : Letter Letter bool :=
fun n1 n2
match (proj1_sig n1,proj1_sig n2) with
|((x,l),(y,m))
if (beq_name x y)
then beq_list l m
else false
end.
Definition eq_letter (x y : Letter) := proj1_sig x = proj1_sig y.
Infix " ≃ " := eq_letter (at level 50).

Global Instance eq_letter_Equivalence : Equivalence eq_letter.
Lemma beq_letter_spec : x y, reflect (x y) (beq_letter x y).
Definition τ : Letter (list Atom) :=
fun n
match (proj1_sig n) with
| (x,l)l
end.
Tactic Notation "simpl_is_perm" "in" ident(h):=
let p := fresh "p" in
simpl_is_perm_hyp p h.
Tactic Notation "simpl_is_perm" "in" ident(h) "as" ident(p) :=
simpl_is_perm_hyp p h.
Lemma τ_spec : a, NoDup (τ a).
Lemma eq_letter_τ : Proper (eq_letter ==> Logic.eq) τ.