Continued developments up to Separability Lemma [Barendregt 1984, p.254]

[binghe]

Hi,

This PR continues the formal developments under examples/lambda, up to the concept of Böhm transformations and then the following (two) Separability Lemmas (to be used by the target completeness theorem):

Boehm_transform_def
⊢ ∀pi. Boehm_transform pi ⇔ EVERY solving_transform pi

solving_transform_def
⊢ ∀f. solving_transform f ⇔ (∃x. f = (λp. p @@ VAR x)) ∨ ∃x N. f = [N/x]

separability_lemma1 [boehmTheory]
⊢ ∀M N.
    solvable M ∧ solvable N ∧ ¬equivalent M N ⇒
    ∀P Q. ∃pi. Boehm_transform pi ∧ apply pi M == P ∧ apply pi N == Q

separability_lemma2 [boehmTheory]
⊢ ∀M N.
    solvable M ∧ ¬equivalent M N ⇒
    ∀P. ∃pi. Boehm_transform pi ∧ apply pi M == P ∧ unsolvable (apply pi N)

The main work is added as a new theory file under examples/lambda/barendregt which does not depend on pure_dBTheory (in .../other-models), as now it seems possible that the entire work can be done without using de Brujin encoding of lambda terms.

The present stage work shows that the rather long definition of the above "equivalence" (its dB version is slightly shorter) can be handled in practice:

The concept "equivalent" has a big definition body:

equivalent_def
⊢ ∀M N.
    equivalent M N ⇔
    if solvable M ∧ solvable N then
      (let
         M0 = principle_hnf M;
         N0 = principle_hnf N;
         n = LAMl_size M0;
         n' = LAMl_size N0;
         vs = FRESH_list (MAX n n') (FV M0 ∪ FV N0);
         vsM = TAKE n vs;
         vsN = TAKE n' vs;
         M1 = principle_hnf (M0 ·· MAP VAR vsM);
         N1 = principle_hnf (N0 ·· MAP VAR vsN);
         y = hnf_head M1;
         y' = hnf_head N1;
         m = LENGTH (hnf_children M1);
         m' = LENGTH (hnf_children N1)
       in
         y = y' ∧ n + m' = n' + m)
    else unsolvable M ∧ unsolvable N

This is mainly due to the following new variant of hnf_cases sharing the binding variable list among different hnfs:

hnf_cases_shared
⊢ ∀vs M.
    ALL_DISTINCT vs ∧ LAMl_size M ≤ LENGTH vs ∧ DISJOINT (set vs) (FV M) ⇒
    (hnf M ⇔ ∃y args. M = LAMl (TAKE (LAMl_size M) vs) (VAR y ·· args))

where LAMl_size returns the levels of toplevel abstracts for any term:

LAMl_size_def
⊢ ((∀s. LAMl_size (VAR s) = 0) ∧ (∀t2 t1. LAMl_size (t1 @@ t2) = 0) ∧
   ∀t v. LAMl_size (LAM v t) = 1 + LAMl_size t) ∧
  ∀pi t. LAMl_size (pi·t) = LAMl_size t

There are many other small additions here and there, hard to describe them all. In particular, the following FRESH_list has been promoted from standarisationTheory to termTheory as a function. Now it plays an important role in setting up a shared binding variable list for all hnfs involved in the same proof: (NOTE: it can be further moved to basic_swapTheory but I think termTheory is already early enough).

FRESH_list_def
⊢ ∀n s.
    FINITE s ⇒
    ALL_DISTINCT (FRESH_list n s) ∧ DISJOINT (set (FRESH_list n s)) s ∧
    LENGTH (FRESH_list n s) = n

Besides, in relationTheory now we have RINSERT R x y for inserting one more pair of elements (x,y) into an existing relation R.

--Chun

[binghe]

In chap2Theory where you left a note for has_benf, I have confirmed (by proving the completeness theorem with cheated lemmas) that the definition was indeed wrong and should have lameta instead == as the following:

has_benf_def
⊢ ∀t. has_benf t ⇔ ∃t'. lameta t t' ∧ benf t'