[lambda] full version of subtree_equiv_lemma (agree_upto_lemma)

[binghe]

Hi,

This PR follows #1354 and finally formalized the full proof of the "agree upto lemma" (Lemma 10.3.11 of [1. p.251]). But now I have modified the theorem statements into a more primitive form without directly using agree_upto, thus the theorem has been renamed to subtree_equiv_lemma (this single proof now has 3650+ lines):

[subterm_equiv_lemma] (boehmTheory)
⊢ ∀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) ∧
      (∀M. MEM M Ms ⇒ p ∈ ltree_paths (BT' X (apply pi M) r)) ∧
      (∀M N q.
         MEM M Ms ∧ MEM N Ms ∧ q ≼ p ∧ subtree_equiv X M N q r ⇒
         subtree_equiv X (apply pi M) (apply pi N) q r) ∧
      ∀M N.
        MEM M Ms ∧ MEM N Ms ∧ subtree_equiv X (apply pi M) (apply pi N) p r ⇒
        subtree_equiv' X M N p r

As the size of boehmScript.sml has reached more than 9k lines and the theory building took about two minutes in my laptop. To prevent repeatedly building existing long proofs, now I have started a new file completeScript.sml (perhaps a better name should be used) and moved all previous code after the big proof to the new file, where you find the previous agree_upto_lemma:

[agree_upto_lemma] (completeTheory)
⊢ ∀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 (apply pi M) (apply pi N) p r ⇒
        subtree_equiv' X M N p r

Note that there's subtree_equiv' vs subtree_equiv' in the statements. The key difference is at the underlying head_equivalent vs head_equivalent':

[head_equivalent'_def]
⊢ ∀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,v8),SOME (vs2,v6)) =>
      LENGTH vs1 + THE m2 = LENGTH vs2 + THE m1

[head_equivalent_def]
⊢ ∀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)) =>
      y1 = y2 ∧ LENGTH vs1 + THE m2 = LENGTH vs2 + THE m1

The variant head_equivalent' (and thus also subtree_equiv') does not consider y1 = y2. I found this modification is necessary to obtain the full proof of the big lemma, otherwise I can show that it's unprovable. So far I don't know if the final completeness theorem will be affected by this finding.

--Chun

[1] Barendregt, H.P.: The lambda calculus, its syntax and semantics.
College Publications, London (1984).

[mn200]

Instead of complete (runs the risk of clashing with lots of different names), how about lametaComplete (or lameta_complete, or ...)?

[binghe]

Instead of complete (runs the risk of clashing with lots of different names), how about lametaComplete (or lameta_complete, or ...)?

The theories under examples/lambda do not have the convention of using mixed case theory names. I will rename it to lameta_complete. Thanks.

[mn200]

Brilliant; many thanks!