[lambda] agree_upto_lemma (enhanced)

[binghe]

Hi,

This PR follows #1348 and fixed the involved definitions and proofs. Previously, the definition of agree_upto requires literal equivalent of corresponding Böhm tree notes between two terms (ltree_el (BT' X M r) q = ltree_el (BT' X N r) q). This turns out to be wrong (not general enough). Instead, the concept of subtree_equiv (based on head_equivalent) should be used:

[agree_upto_def] (fixed)
⊢ ∀X Ms p r.
    agree_upto X Ms p r ⇔
    ∀M N q. MEM M Ms ∧ MEM N Ms ∧ q ≼ p ⇒ subtree_equiv X M N q r

[subtree_equiv_def]
⊢ ∀X M N p r.
    subtree_equiv X M N p r ⇔
    ltree_equiv (ltree_el (BT' X M r) p) (ltree_el (BT' X N r) p)

Overload ltree_equiv = “OPTREL head_equivalent”

[head_equivalent_def] (updated)
⊢ ∀a1 m1 a2 m2.
    head_equivalent (a1,m1) (a2,m2) ⇔
    case (a1,a2) of
      (NONE,NONE) => T
    | (NONE,SOME v3) => F
    | (SOME v2,NONE) => F
    | (SOME (vs1,y1),SOME (vs2,y2)) =>
      (let
         n1 = LENGTH vs1;
         n2 = LENGTH vs2
       in
         y1 = y2 ∧ n1 + THE m2 = n2 + THE m1)

In short words, previously the equivalence of corresponding tree nodes is y1 = y2 /\ n1 = n2 /\ m1 = m2, now it's relaxed to y1 = y2 ∧ n1 + m2 = n2 + m1, which essentially captures the idea of η-equivalence between λ-terms.

The proof of agree_upto_lemma (for the previously proved conclusions) becomes even more tedious, requiring some more devices on head reductions, which now involves "suffix" of lists:

[hreduce_permutator_shared]
⊢ ∀Ns n ls.
    LENGTH Ns ≤ n ∧ n < LENGTH ls ∧ ALL_DISTINCT ls ∧
    DISJOINT (set ls) (BIGUNION (IMAGE FV (set Ns))) ⇒
    ∃xs y.
      permutator n ·· Ns -h->* LAMl xs (LAM y (VAR y ·· Ns ·· MAP VAR xs)) ∧
      LENGTH xs = n − LENGTH Ns ∧ IS_SUFFIX ls (SNOC y xs)

For this reason, I have also added a few new lemmas into rich_listTheory regarding IS_SUFFIX, etc.

Now the statements of agree_upto_lemma is slightly extended to the following:

[agree_upto_lemma]
⊢ ∀X Ms p r.
    FINITE X ∧ p ≠ [] ∧ 0 < r ∧ Ms ≠ [] ∧
    BIGUNION (IMAGE FV (set Ms)) ⊆ X ∪ RANK r ∧
    EVERY (λM. subterm X M p r ≠ NONE) Ms ⇒
    ∃pi.
      Boehm_transform pi ∧ EVERY is_ready' (MAP (apply pi) Ms) ∧
      (agree_upto X Ms p r ⇒ agree_upto X (MAP (apply pi) Ms) p r) ∧
      ∀M N.
        MEM M Ms ∧ MEM N Ms ⇒
        subtree_equiv X M N p r ⇒
        subtree_equiv X (apply pi M) (apply pi N) p r

Note that the only difference between the above form and the final full form, is that the last logical implication ⇒ (between two subtree_equivs) will be an "if and only if" in the full form.

Chun

[binghe]

Strange, I forked this delivery branch from 01016dc for which CI tests passed but still encountered CI test failures...

[binghe]

I have updated [head_equivalent_def] by using SML case .. of. I look forward for updates on develop to get the CI tests fully fixed.

[mn200]

Thanks for this !