more results of terms having head normal forms (has_hnf)

[binghe]

Hi,

This is a stage work proving more results of terms having head normal forms (has_hnf), independent with solvable terms. The end of the chain of proved theorems is the following theorems with [simp] (Proposition 8.3.13 (i) of [1, p.174]):

[has_hnf_iff_LAM] (standardisationTheory)
    ⊢ ∀x M. has_hnf (LAM x M) ⇔ has_hnf M

Now I have to use chap3Theory, i.e. using theorems about (beta) reductions (beta and grandbeta) to prove results about beta conversions (lameq). The following important lemmas are proved:

lameq_CR (chap3Theory)
    ⊢ ∀M N. M == N ⇒ ∃Z. M -β->* Z ∧ N -β->* Z

grandbeta_imp_betastar (chap3Theory)
    ⊢ ∀M N. M =β=> N ⇒ M -β->* N

grandbeta_imp_lameq (chap3Theory)
    ⊢ ∀M N. M =β=> N ⇒ M == N

abs_betastar (chap3Theory, statements modified in 2nd commit)
    ⊢ ∀x M Z. LAM x M -β->* Z ⇒ ∃N'. Z = LAM x N' ∧ M -β->* N'

P.S. With the above theorem "has_hnf_iff_LAM" and the following theorem (slightly renamed) added by previous PR #1148:

solvable_iff_LAM (solvableTheory)
    ⊢ ∀x M. solvable (LAM x M) ⇔ solvable M

we are now ready to show |- solvable M <=> has_hnf M (a term is solvable iff has head normal forms) by first reducing all involved terms to closed terms (by closing the terms with LAMs of free variables.), i.e. |- closed M ==> solvable M <=> has_hnf M.

[1] Barendregt, H.P.: The Lambda Calculus, Its Syntax and Semantics. College Publications, London (1984).

[mn200]

This could be an iff.

[mn200]

If you lift the Ns <> [] assumption out, I believe the statement could be an iff:

Ns <> [] ==> (hnf (M @* Ns) <=> hnf M /\ ~is_abs M)

[mn200]

If you use the labelling option in the Inductive definition of lameq you should be able to get these for free:

...
[~SYM:]
(!M N. M == N ==> N == M) /\
[~TRANS:]
(!M N P. M == N /\ N == P ==> M == P) /\ ...

You will need to replace the call to xHol_reln with Inductive lameq:

[binghe]

Thanks for your code review @mn200, I have made all the related changes (my first time using the modern syntax of Inductive with tags)

[binghe]

If you could take a look at hnf_cases :

    !M. hnf M ==> ?vs args y. M = LAMl vs (VAR y @* args)

I believe this theorem may be also improved as an iff: if M = LAMl vs (VAR y @* args) holds, then there should be no way to do one more head reduction as VAR y plus HD args (if exists) is not a valid head redex. Is this true? (even so, the new proof has to be delayed to next PR as I don't know how to manipulate head reduction process yet...)

[mn200]

Thanks for all this!

I agree that your implication looks to definitely be an iff. Will look at it.

[mn200]

See b1932f5