matita/matita/contribs/lambdadelta/apps_2/examples/ex_cnv_eta.ma

   1 (**************************************************************************)
   2 (*       ___                                                              *)
   3 (*      ||M||                                                             *)
   4 (*      ||A||       A project by Andrea Asperti                           *)
   5 (*      ||T||                                                             *)
   6 (*      ||I||       Developers:                                           *)
   7 (*      ||T||         The HELM team.                                      *)
   8 (*      ||A||         http://helm.cs.unibo.it                             *)
   9 (*      \   /                                                             *)
  10 (*       \ /        This file is distributed under the terms of the       *)
  11 (*        v         GNU General Public License Version 2                  *)
  12 (*                                                                        *)
  13 (**************************************************************************)
  14
  15 include "basic_2/rt_computation/cpms_drops.ma".
  16 include "basic_2/dynamic/cnv.ma".
  17
  18 (* EXAMPLES *****************************************************************)
  19
  20 (* Extended validy (λδ-2A) vs. restricted validity (λδ-1B) ******************)
  21
  22 (* Note: extended validity of a closure, height of cnv_appl > 1 *)
  23 lemma cnv_extended (h) (p) (G) (L):
  24       ∀s. ❨G,L.ⓛ⋆s.ⓛⓛ[p]⋆s.⋆s.ⓛ#0❩ ⊢ ⓐ#2.#0 ![h,𝛚].
  25 #h #p #G #L #s
  26 @(cnv_appl … 2 p … (⋆s) … (⋆s))
  27 [ //
  28 | /4 width=1 by cnv_sort, cnv_zero, cnv_lref/
  29 | /4 width=1 by cnv_bind, cnv_zero/
  30 | /5 width=3 by cpm_cpms, cpm_lref, cpm_ell, lifts_sort/
  31 | /5 width=5 by cpm_cpms, cpm_bind, cpm_ell, lifts_uni, lifts_sort, lifts_bind/
  32 ]
  33 qed.
  34
  35 (* Note: restricted validity of the η-expanded closure, height of cnv_appl = 1 **)
  36 lemma cnv_restricted (h) (p) (G) (L):
  37       ∀s. ❨G,L.ⓛ⋆s.ⓛⓛ[p]⋆s.⋆s.ⓛⓛ[p]⋆s.ⓐ#0.#1❩ ⊢ ⓐ#2.#0 ![h,𝟐].
  38 #h #p #G #L #s
  39 @(cnv_appl … 1 p … (⋆s) … (ⓐ#0.#2))
  40 [ //
  41 | /4 width=1 by cnv_sort, cnv_zero, cnv_lref/
  42 | @cnv_zero
  43   @cnv_bind //
  44   @(cnv_appl … 1 p … (⋆s) … (⋆s))
  45   [ //
  46   | /2 width=1 by cnv_sort, cnv_zero/
  47   | /4 width=1 by cnv_sort, cnv_zero, cnv_lref, cnv_bind/
  48   | /2 width=3 by cpms_ell, lifts_sort/
  49   | /4 width=5 by cpms_lref, cpms_ell, lifts_uni, lifts_sort, lifts_bind/
  50   ]
  51 | /4 width=3 by cpms_lref, cpms_ell, lifts_sort/
  52 | /5 width=7 by cpms_ell, lifts_bind, lifts_flat, lifts_push_lref, lifts_push_zero, lifts_sort/
  53 ]
  54 qed.