RIS.stacks: an algebra of stacks.

Set Implicit Arguments.

Require Export tools atoms bijection.

Section s.
Context {atom : Set}{𝐀 : Atom atom}.

Definitions

The main data structure in this module is stacks. These are lists of pairs of names.

Definition stack {A : Atom atom}:= list (atom × atom).

A stack is accepting exactly when its two projections coincide.

Notation " s ✓ " := (prj1 s = prj2 (s : stack)) (at level 30).

The predicate absent s a b holds when a does not appear in the first component of a pair in s, and b does not appear in second components.

Definition absent (s : stack) a b :=
¬ a ∈ prj1 s ∧ ¬ b ∈ prj2 s.

The boolean predicate absentb is meant to reflects absent.

Definition absentb (s:stack) a b := negb (inb a (prj1 s) || inb b (prj2 s)).

a and b are paired in s if either:

a and b are equal and a is not mentioned anywhere in s;
s can be decomposed as s1++(a,b)::s2, such that absent s1 a b.

Definition paired s a b :=
(b =a ∧ absent s a a )
∨ (∃ s1 s2, s = s1 ++(a ,b )::s2 ∧ absent s1 a b ).

Notation " s ⊨ a ↦ b " := (paired s a b) (at level 80).

The boolean predicate pairedb is meant to reflects paired.

Fixpoint pairedb (s:stack) a b :=
  match s with
  | [] ⇒ a =?=b
  | (c,d)::s ⇒
    (c,d)=?=(a ,b )
    || (negb(c=?=a) && (negb(d=?= b) && pairedb s a b ))
  end.

Simple properties

Accepting

A stack is accepting if it only contains reflexive pairs.

Lemma Accepting_refl s : s ✓ ↔ (∀ a b, (a ,b ) ∈ s → a =b ).

l⊗l is always accepting, and so is the empty stack.

Remark Accepting_combine l : (l ⊗l ) ✓.

Remark Accepting_nil : (@nil (atom ×atom)) ✓.

Remark Accepting_cons p s : (p ::s ) ✓ ↔ s ✓ ∧ fst p = snd p.

Remark Accepting_cons_refl a s : ((a ,a )::s ) ✓ ↔ s ✓.

Remark Accepting_app s s' : (s ++s') ✓ ↔ s ✓ ∧ s' ✓.

If s is accepting, so is s ⊖ (a,b).

Remark Accepting_rmfst s a b : s ✓ → (s ⊖ (a ,b )) ✓.

absent

absent s a b holds if and only if for any pair in s the first component differs from a and the second differs from b.

Lemma absent_alt_def s a b : absent s a b ↔ ∀ x y, (x ,y ) ∈ s → x ≠ a ∧ y ≠ b.

Remark absent_app s1 s2 a b :
  absent (s1 ++s2) a b ↔ absent s1 a b ∧ absent s2 a b.

Remark absent_cons s a b c d :
  absent ((a ,b )::s) c d ↔ a ≠c ∧ b ≠d ∧ absent s c d.

Remark absent_flip s a b :
  absent s a b ↔ absent (s `) b a.

Remark absent_mix s1 s2 a b c :
  absent s1 a b → absent s2 b c → absent (s1 ⋈ s2) a c.

The absent predicate commutes with the action of permutations.

Lemma absent_perm p s a b : absent (p ∙s) a b ↔ absent s (p ∗∙a) (p ∗∙b).

absentb reflects absent.

Lemma absentb_correct a b s : absent s a b ↔ absentb s a b = true.

Remark absentb_false a b s : ¬ absent s a b ↔ absentb s a b = false.

Remark absentb_cons s a b c d :
absentb ((a ,b )::s) c d = negb (a =?=c) && negb (b =?=d) && absentb s c d.

Remark absentb_app s1 s2 a b :
absentb (s1 ++s2) a b = absentb s1 a b && absentb s2 a b.

If s and s' are equivalent (contain the same pairs), then a,b is absent from s if and only if it is absent from s'.

Global Instance absent_equivalent :
Proper ((@equivalent (atom ×atom)) ==> eq ==> eq ==> iff) absent.

Global Instance absentb_equivalent :
Proper ((@equivalent (atom ×atom)) ==> eq ==> eq ==> eq) absentb.

We can simplify rmfst.

Lemma rmfst_absent s a b : absent s a b → s ⊖ (a ,b ) = s.

Lemma rmfst_present s s' a b : absent s a b → (s ++(a ,b )::s') ⊖ (a ,b ) = s ++s'.

paired

For accepting stacks, a and b are paired if and only if they are equal.

Remark paired_Accepting s a b : s ✓ → (s ⊨ a ↦ b ) ↔ b = a.

Remark paired_app s s' a b :
  (s ++s' ⊨ a ↦ b ) ↔ ((s ⊨ a ↦ b ) ∧ (a ,b ) ∈ s ) ∨ (absent s a b ∧ s' ⊨ a ↦ b ).

Remark paired_flip s a b : (s ⊨ a ↦ b ) ↔ s ` ⊨ b ↦ a.

Remark paired_mix s1 s2 a b c :
  prj2 s1 = prj1 s2 → (s1 ⊨ a ↦ b ) → (s2 ⊨ b ↦ c ) →
  (s1 ⋈ s2 ⊨ a ↦ c )
  ∧ (s1 ⋈s2 )⊖(a ,c ) = (s1 ⊖(a ,b ))⋈(s2 ⊖(b ,c ))
  ∧ prj2 (s1 ⊖(a ,b )) = prj1 (s2 ⊖(b ,c )).

Remark paired_cons s a b c d :
  ((c ,d )::s ⊨ a ↦ b ) ↔ (c ,d )=(a ,b ) ∨ (c ≠a ∧ d ≠b ∧ s ⊨ a ↦ b ).

Remark rmfst_paired s a b c d :
  (a , b ) ≠ (c , d ) → (s ⊨ c ↦ d ) → s ⊖ (a , b ) ⊨ c ↦ d.

Remark paired_rmfst s a b c d :
  a ≠c → b ≠ d → (s ⊖ (a , b ) ⊨ c ↦ d ) → s ⊨ c ↦ d.

The boolean predicate pairedb reflects paired.

Lemma pairedb_spec s a b : (s ⊨a ↦b ) ↔ pairedb s a b = true.

It is worth noticing that is s pairs a with b with d, then b and d are equal. Symmetrically, if both a and b are paired with c, then they are equal.

Remark paired_inj s a b c d : (s ⊨ a ↦ b ) → (s ⊨ c ↦ d ) → a =c ↔ b =d.

The pairing predicate commutes with permutation actions.

Lemma paired_perm p s a b : (p ∙s ⊨ a ↦ b ) ↔ s ⊨ p ∗∙a ↦ p ∗∙b.

If a stack s1++s2 validates the pair a,b, then three cases are possible:

s1 validates the pair by containing it;
a,b is absent from s1, and s2 validates the pair by containing it;
a and b are equal, and both s1 and s2 validate the pair by absence.

The following technical lemma witnesses this case analysis, and provides a closed formula for s1++s2 ⊖ (a,b) in each case.

Lemma rmfst_app_dec_stacks s1 s2 a b :
  (s1 ++s2 ⊨ a ↦ b ) →
  (∃ l1 l2, s1 = l1 ++(a ,b )::l2 ∧ absent l1 a b
            ∧ (s1 ++s2 )⊖(a ,b ) = l1 ++l2 ++s2 )
  ∨ (∃ m1 m2, s2 = m1 ++(a ,b )::m2 ∧ absent (s1 ++m1) a b
              ∧ (s1 ++s2 )⊖(a ,b ) = s1 ++m1 ++m2 )
  ∨ (a =b ∧ absent (s1 ++s2) a b
     ∧ (s1 ++s2 )⊖(a ,b ) = s1 ++s2 ).

Converting a stack into a permutation

image s converts the stack s into a function from atoms to atoms:

if a does not appear in the first projection of s, image s a is a itself;
otherwise, image s a returns an atom b such that s can be decomposed as s1++(a,b)::s2, where a does not appear in the first projection of s1. Note that b may appear in the second projection of s1, therefore it is not always the case that s⊨ a ↦ image s a.

Fixpoint image (s:stack) a :=
  match s with
  | [] ⇒ a
  | (c,d)::s ⇒ if a =?=c then d else image s a
  end.

However, if there exists a b such that s⊨ a↦b, then image s a will coincide with that b.

Lemma image_spec s a b : (s ⊨ a ↦b ) → image s a = b.

var_perm l s tries to compute a permutation sending names from l to their image by s.

Definition var_perm (l:list atom) s := l >> (map (image s) l ).

Fixpoint var_perm' (l:list atom) s : option perm :=
  match s with
  | [] ⇒ Some []
  | (a,b)::s ⇒
      match var_perm' (l ∖a) s with
      | None ⇒ None
      | Some p ⇒
        if (existsb (fun c ⇒ p ∙ c =?= b) (l ∖ a))
        then None
        else
          if inb a l
          then Some ((p∙a,b)::p)
          else Some p
      end
  end.

Lemma var_perm'_Some l s p a :
  var_perm' l s = Some p → a ∈ l → s ⊨ a ↦ p ∙ a.
Lemma var_perm'_None l s :
  var_perm' l s = None → ∃ a, a ∈ l ∧ ∀ b, ¬ (s ⊨ a ↦ b ).

Lemma var_perm'_spec l s p :
  (∀ a, a ∈ l → s ⊨ a ↦ p ∙ a )
  ↔ (∃ p', var_perm' l s = Some p' ∧ (∀ a, a ∈ l → p ∙ a = p' ∙ a )).

If l is duplication-free, and if a permutation p exists such that s⊨a↦p∙a for every name a in l, then for each of these names the action of var_perm l s and that of p coincide.

Lemma var_perm_paired s l p :
NoDup l → (∀ a, a ∈l → s ⊨a ↦p ∙a ) → ∀ a, a ∈ l → var_perm l s ∙ a = p ∙a.

If s is accepting, then var_perm l s is the identity permutation.

Remark var_perm_accepting s l: s ✓ → var_perm l s ≃ [].

If s is accepting, then var_perm' l s is the identity permutation.

Remark var_perm'_accepting s l: s ✓ → ∃ p, var_perm' l s = Some p ∧ p ≃ [].

End s.

Notation " s ⊨ a ↦ b " := (paired s a b) (at level 80).
Notation " s ✓ " := (prj1 s = prj2 (s : stack)) (at level 30).