RIS.factors: square bindings and binding division.

Set Implicit Arguments.

Require Import tools words.

Enumerate bindings

Bindupto N returns a list containing every element of 𝖡 of size not exceeding N.

Fixpoint Bindupto n : list 𝖡 :=
  match n with
  | 0 ⇒ [ε ;(0,true ,0)]
  | S n ⇒
    flat_map (fun b : 𝖡 ⇒
                b ::(S (fst (fst b)),snd(fst b),snd b )
                 ::[(fst (fst b),snd(fst b),S (snd b))]
             )
             (Bindupto n)
  end.
Lemma Bindupto_spec n b : size b ≤ n ↔ b ∈ Bindupto n.

Factors

factors b N is a list containing pairs of bindings (α,β) such that α⋅β=b. This list is not exhaustive, as there are in general an infinite number of such pairs. The parameter N is used as a bound, to collect only a finite number of pairs. The following lemmas will outline the properties of this function.

Definition factors (b : 𝖡) N : list (𝖡 × 𝖡) :=
  (fun p ⇒ (fst p ⋅ snd p ) =?= b )
    :> pairs
    (pairs (pairs (seq 0 (S N)) [true ;false ]) (seq 0 (S N)))
    (pairs (pairs (seq 0 (size b + S N)) [true ;false ]) (seq 0 (size b + S N))).

Every pair (a1,a2) in factors b N satisfies a1⋅a2=b.

Lemma factors_prod b N a1 a2 : (a1 ,a2 ) ∈ factors b N → a1 ⋅ a2 = b.

If the size of a1 is below N and if the product a1⋅a2 equals b, then (a1,a2) belongs to factors b N.

Lemma factors_In b N a1 a2 : size a1 ≤ N → a1 ⋅ a2 = b → (a1 ,a2 ) ∈ factors b N.

For any pair (a1,a2) in factors b N, the size of a1 does not exceed 2*N.

Lemma factors_size a1 a2 b N : (a1 ,a2 ) ∈ factors b N → size a1 ≤ 2×N.

Division when one projection is 0

factors (N,t,0) k contains only pairs of the shape ((D,F,C),(N',t',0)) such that C≤N'.

Lemma factors_open_balanced β1 β2 N t k :
(β1 ,β2 ) ∈ factors (N ,t ,0) k →
∃ N' t', β2 = (N',t',0) ∧ c_binding β1 ≤ N'.

divide_by_open β yields a list containing every α such that (0,false,1)⋅β=(0,false,1)⋅α.

Definition divide_by_open β :=
  match β with
  | (0,false ,n) | (0,true ,n)| (1,false ,S n) ⇒ [(0,false ,n);(0,true ,n);(1,false ,S n)]
  | _ ⇒ [β ]
  end.

Lemma divide_by_open_spec β1 β2 : (0,false ,1) ⋅ β1 = (0,false ,1) ⋅ β2 ↔ β1 ∈ divide_by_open β2.

Square bindings

A binding α:𝖡 is called square when its creation and destruction projections are equal.

Definition square α := c_binding α = d_binding α.

This property can be checked using the is_square boolean predicate.

Definition is_square β := c_binding β =?= d_binding β.

We define the following binary operation on bindings.

Definition maxBind (α β : 𝖡) : 𝖡 :=
  if Nat.ltb (d_binding α) (d_binding β) then β
  else if Nat.ltb (d_binding β) (d_binding α) then α
       else (d_binding α ,snd(fst α)||snd(fst β),max (c_binding α) (c_binding β)).
Infix " ⊓ " := maxBind (at level 45).

On square bindings, this operation coincides with multiplication.

Lemma prod_binding_maxBind a b : square a → square b → a ⊓ b = a ⋅ b.

The structure (𝖡,⊓,ε) forms a commutative idempotent monoid.

Lemma maxBind_neutral a : a ⊓ ε = a.
Lemma maxBind_assoc a b c : a ⊓ (b ⊓ c ) = (a ⊓ b ) ⊓ c.
Lemma maxBind_comm a b : a ⊓ b = b ⊓ a.
Lemma maxBind_idem a : a ⊓ a = a.

If a and b are square, a ⊓ b is either a or b.

Lemma maxBind_square_disj a b :
square a → square b → a ⊓ b = a ∨ a ⊓ b = b.

Hence, ⊓ maps pairs of square bindings to square bindings.

Lemma maxBind_square a b :
square a → square b → square (a ⊓ b).

Since ⊓ is commutative, associative and idempotent, applying on equivalent lists yields the same result.

Lemma maxBind_lists A B : A ≈ B → fold_right maxBind ε A = fold_right maxBind ε B.

Square factors of square bindings

lower_squares, when applied to a square binding β, produces the list of square bindings α such that α⋅β=β.

Definition lower_squares (β : 𝖡) : list 𝖡 :=
  if (snd(fst β))
  then flat_map (fun m ⇒ [(m ,true ,m );(m ,false ,m )]) (seq 0 (S (snd β)))
  else β ::flat_map (fun m ⇒ [(m ,true ,m );(m ,false ,m )]) (seq 0 (snd β)).

Lemma lower_squares_spec α β :
  square β → α ∈ lower_squares β ↔ square α ∧ α ⋅ β = β.

We may write the following detailed characterisation of the elements of lower_squares β.

Lemma lower_squares_alt α β :
  square β → α ∈ lower_squares β
              ↔ square α ∧ (c_binding α < c_binding β
                               ∨ (c_binding α = c_binding β ∧ negb (snd (fst α))||snd(fst β) = true )).

If the product of two squares belongs to lower_squares γ, so does its arguments.

Lemma lower_squares_prod α β γ :
square α → square β → square γ → α ⋅ β ∈ lower_squares γ →
α ∈ lower_squares γ ∧ β ∈ lower_squares γ.

lower_squares b only contains bindings of smaller size.

Lemma lower_squares_size a b : square b → a ∈ lower_squares b → size a ≤ size b.

Technical remark:

Remark product_square_close_balanced β1 β2 β3 :
  square β1 → β1 ⋅ β2 = β3 → c_binding β3 = 0 →
  ∃ N1 N2 N3 t1 t2 t3,
    β1 = (N1 ,t1 ,N1 )
    ∧ β2 = (N2 ,t2 ,0)
    ∧ β3 = (N3 ,t3 ,0)
    ∧ N1 ≤ N2
    ∧ N2 = N3
    ∧ ((t2 = t3 ∧ (∀ β, β ∈ lower_squares β1 → β ⋅ β2 = β2 ))
        ∨ (t1 = true ∧ t2 = false ∧ t3 = true ∧ N1 = N2
            ∧ lower_squares β1 ≈ β1 :: lower_squares (N1 ,false ,N1 )
            /\(∀ β, β ∈ lower_squares (N1 ,false ,N1 ) → β ⋅ β2 = β2 ))).