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