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 (basic_2B) vs. restricted validity (basic_1A) ************)
  21
  22 (* Note: extended validity of a closure, height of cnv_appl > 1 *)
  23 lemma cnv_extended (h) (p): ∀G,L,s. ⦃G,L.ⓛ⋆s.ⓛⓛ{p}⋆s.⋆s.ⓛ#0⦄ ⊢ ⓐ#2.#0 !*[h].
  24 #h #p #G #L #s
  25 @(cnv_appl … 2 p … (⋆s) … (⋆s))
  26 [ //
  27 | /4 width=1 by cnv_sort, cnv_zero, cnv_lref/
  28 | /4 width=1 by cnv_bind, cnv_zero/
  29 | /5 width=3 by cpm_cpms, cpm_lref, cpm_ell, lifts_sort/
  30 | /5 width=5 by cpm_cpms, cpm_bind, cpm_ell, lifts_uni, lifts_sort, lifts_bind/
  31 ]
  32 qed.
  33
  34 (* Note: restricted validity of the η-expanded closure, height of cnv_appl = 1 **)
  35 lemma vnv_restricted (h) (p): ∀G,L,s. ⦃G,L.ⓛ⋆s.ⓛⓛ{p}⋆s.⋆s.ⓛⓛ{p}⋆s.ⓐ#0.#1⦄ ⊢ ⓐ#2.#0 ![h].
  36 #h #p #G #L #s
  37 @(cnv_appl … 1 p … (⋆s) … (ⓐ#0.#2))
  38 [ /2 width=1 by ylt_inj/
  39 | /4 width=1 by cnv_sort, cnv_zero, cnv_lref/
  40 | @cnv_zero
  41   @cnv_bind //
  42   @(cnv_appl … 1 p … (⋆s) … (⋆s))
  43   [ /2 width=1 by ylt_inj/
  44   | /2 width=1 by cnv_sort, cnv_zero/
  45   | /4 width=1 by cnv_sort, cnv_zero, cnv_lref, cnv_bind/
  46   | /2 width=3 by cpms_ell, lifts_sort/
  47   | /4 width=5 by cpms_lref, cpms_ell, lifts_uni, lifts_sort, lifts_bind/
  48   ]
  49 | /4 width=3 by cpms_lref, cpms_ell, lifts_sort/
  50 | /5 width=7 by cpms_ell, lifts_bind, lifts_flat, lifts_push_lref, lifts_push_zero, lifts_sort/
  51 ]
  52 qed.