[lambda] The "congruence" of subterm properties w.r.t different excluded lists

[binghe]

Hi,

given a solvable term, the concept of "subterm", along a path of numbers, is the specified (by the path) children term of the principle hnf converted from the original term, so on until the last path element:

subterm_def
⊢ (∀X M. subterm X M [] = SOME (X,M)) ∧
  ∀X M x xs.
    subterm X M (x::xs) =
    if solvable M then
      (let
         M0 = principle_hnf M;
         n = LAMl_size M0;
         m = hnf_children_size M0;
         vs = FRESH_list n (X ∪ FV M0);
         M1 = principle_hnf (M0 ·· MAP VAR vs);
         Ms = hnf_children M1
       in
         if x < m then subterm (X ∪ set vs) (EL x Ms) xs else NONE)
    else NONE

Due to alpha-conversion, the returned subterm may contain some fresh variables generated according to an "excluded list" given as input parameter. The definition guarantees (see the part vs = FRESH_list n (X ∪ FV M0)) that whatever X (the excluded list) will give the "correct" result, in the sense that the principle hnf of M0 ·· MAP VAR vs is indeed the inner body of M0 without variable captures (because vs is fresh, disjoint with FV M0).

In general, FRESH_list (or NEW_TAC) is like a blackbox: nothing can be said between FRESH_list n X and FRESH_list n Y except for their size of lists are the same. Therefore, in many related proofs, properties about subterm X M p cannot be directly used if subterm Y M p is to be discussed, even X and Y themselves have some relationships.

Here I proved a hard result saying that, for any X and Y, the actual term returned by subterm X M p and subterm Y M p differ only by a "term permutation" (tpm), or they are both NONE (either both unsolvable or the path itself is invalid, accessing out bound of the hnf children lists):

subterm_tpm_cong
⊢ ∀p X Y M.
    FINITE X ∧ FINITE Y ⇒
    (subterm X M p = NONE ⇔ subterm Y M p = NONE) ∧
    (subterm X M p ≠ NONE ⇒ ∃pi. tpm pi (subterm' X M p) = subterm' Y M p)

Actually the above theorem cannot be directly proved, without first generalizing to the following lemma involving tpm:

subterm_tpm_lemma
⊢ ∀p X Y M pi.
    FINITE X ∧ FINITE Y ⇒
    (subterm X M p = NONE ⇒ subterm Y (tpm pi M) p = NONE) ∧
    (subterm X M p ≠ NONE ⇒
     ∃pi'. tpm pi' (subterm' X M p) = subterm' Y (tpm pi M) p)

Here, it's interesting to see (if taking both X and Y as X) that subterm' X (tpm pi M) p is not tpm pi (subterm' X p) but with another different permutation list. This is because, although all free variables in M are permuted by pi, the fresh binding list is completely different, and therefore subterm' X (tpm pi M) p actually contains two permutations: one is the pi from tpm pi M, the other is ZIP (vs,vs') where vs and vs' are the two internal fresh lists generated for M and tpm pi M. To prove the above lemma, a lot of new small theorems about tpm of existing concepts are added.

Once the above results are obtained, all functions built upon this concept of "subterms" but only returning some numbers, can be proved to be independent with the input excluded list, e.g. the number of hnf children:

subterm_hnf_children_size_cong
⊢ ∀X Y M p.
    FINITE X ∧ FINITE Y ∧ subterm X M p ≠ NONE ∧ solvable (subterm' X M p) ⇒
    hnf_children_size (principle_hnf (subterm' X M p)) =
    hnf_children_size (principle_hnf (subterm' Y M p))

Another more interesting application is the following concept of "subterm (tree) width", i.e. the maximal number of hnf children along the given path p:

subterm_width_def
⊢ ∀M p.
    subterm_width M p =
    (let
       Ms = {subterm' ∅ M p' | p' ≼ FRONT p}
     in
       MAX_SET (IMAGE (hnf_children_size ∘ principle_hnf) Ms))

Note that, when defining subterm_width, the empty set {} has been used to with subterm. But then we can prove that this width is independent with this excluded list (actually a set, same for all above places), i.e. this number is the same for all possible X used in place of subterm X ...:

subterm_width_thm
⊢ ∀X M p p'.
    FINITE X ∧ p ≠ [] ∧ p ∈ ltree_paths (BTe X M) ∧ subterm X M p ≠ NONE ∧
    p' ≼ FRONT p ⇒
    hnf_children_size (principle_hnf (subterm' X M p')) ≤ subterm_width M p

P. S. There are other related minor additions in core theories (rich_list and ltree) in this PR.

Chun

[mn200]

Awesome; thanks!