]> matita.cs.unibo.it Git - helm.git/blob - matita/matita/contribs/lambdadelta/apps_2/examples/ex_cnv_eta.ma
update in delayed-updating
[helm.git] / 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.