[lambda] agree_upto_lemma

[binghe]

Hi,

This PR finally completes the proof of "agree up to lemma" (Lemma 10.3.11 [1. p.251]). Recall that a set (or finite list) of λ-terms are "agree up to" a path p if the Böhm tree nodes of any two terms in it are the same (i.e. same binding variables, same number of children) along the path:

[agree_upto_def]
⊢ ∀X Ms p r.
    agree_upto X Ms p r ⇔
    ∀M N.
      MEM M Ms ∧ MEM N Ms ⇒
      ∀q. q ≼ p ⇒ ltree_el (BT' X M r) q = ltree_el (BT' X N r) q

The "agree up to" lemma says, for a (non-empty) list (or finite set) of λ-terms agree up to path p , under suitable condition (the path is valid, the excluded set is big enough, etc.) there exists a Böhm transform pi such that, after applying pi the resulting terms still agree up to p. This proof is quite tedious, requiring a lot of new lemmas.

[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)

NOTE: The above theorem only covers part (1) and (2) of the textbook theorem. There's still a part (3) whose proof should be similar with (2) and I'm still working on it.

Chun

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

[mn200]

Excellent!