Reworked "strange_cases" by the newly added "term_laml_cases"

[binghe]

Recently a new lemma term_laml_cases has been added into chap2Theory:

[term_laml_cases]
⊢ ∀X. FINITE X ⇒
      ∀t. (∃s. t = VAR s) ∨ (∃M1 M2. t = M1 @@ M2) ∨
          ∃v vs Body.
            t = LAM v (LAMl vs Body) ∧ ¬is_abs Body ∧ v ∉ X ∧ ¬MEM v vs ∧
            ALL_DISTINCT vs ∧ DISJOINT (set vs) X

It's quite general, but the existing strange_cases is still useful in many places as the case splits are different with the above one:

[strange_cases] (old version)
⊢ ∀M. (∃vs M'. M = LAMl vs M' ∧ size M' = 1) ∨
      ∃vs args t.
        M = LAMl vs (t ·· args) ∧ args ≠ [] ∧ ¬is_comb t

Previously I have used this strange_cases to prove hnf_cases, but then I had to completely rework hnf_cases because it needs to assert ALL_DISTINCT vs which is not provided by strange_cases.

In this tiny PR, I reworked the proof of strange_cases (with ALL_DISTINCT vs added in all cases) by using the new term_laml_cases:

[strange_cases] (new version)
⊢ ∀M. (∃vs M'. M = LAMl vs M' ∧ size M' = 1 ∧ ALL_DISTINCT vs) ∨
      ∃vs args t.
        M = LAMl vs (t ·· args) ∧ args ≠ [] ∧ ¬is_comb t ∧ ALL_DISTINCT vs

and then the old shorter proof of hnf_cases can be recovered. The overall proof size is slightly decreased, which is good in general.

Chun

[mn200]

Incidentally, I noticed you turned IMP_RES_TAC oldthm into metis_tac[newthm] having made newthm an iff-version of oldthm. But you could equally get back the oldthm by using iffLR, which would allow IMP_RES_TAC $ iffLR newthm as your tactic.

[binghe]

Incidentally, I noticed you turned IMP_RES_TAC oldthm into metis_tac[newthm] having made newthm an iff-version of oldthm. But you could equally get back the oldthm by using iffLR, which would allow IMP_RES_TAC $ iffLR newthm as your tactic.

Thanks, I never knew iffLR before... Will try to remember this and use it next time.

[binghe]

It turns out that two theorems I added recently into listTheory were already provided in rich_listTheory, namely LENGTH_FRONT and ZIP_SNOC. I will delete them (and open rich_listTheory instead) as part of next PR.

Previously I wrongly thought rich_listTheory only provides new theorems related to new list-related definitions but actually it just tries to enrich listTheory.

[mn200]

As well as iffLR, there's iffRL and cj. All have the advantage of "attacking" the hearts of universally quantified implications. If your theorem is

  |- !vs... p /\ q ==> !us. r ==> s ==>  (lhs <=> rhs)

then iffRL on this will return

  |- !vs... p /\ q ==> !us. r ==> s ==> (rhs ==> lhs)

Similarly, cj i will extract the i-th conjunct (counting from 1(!)) of a conjunction sitting in the same position as lhs <=> rhs above.

[mn200]

rich_list is gross; but listTheory is already bigger than I'd like it to be. It's hard to know quite what to do about this.