]> matita.cs.unibo.it Git - helm.git/blob - matita/matita/contribs/lambda/subterms/projections.ma
026a359c95b69ab9f58e4728b299b576d326472b
[helm.git] / matita / matita / contribs / lambda / subterms / projections.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 "terms/term.ma".
16 include "subterms/subterms.ma".
17
18 (* PROJECTIONS **************************************************************)
19
20 (* Note: the boolean subset of subterms *) 
21 let rec boolean b M on M ≝ match M with
22 [ VRef i   ⇒ {b}#i
23 | Abst A   ⇒ {b}𝛌.(boolean b A)
24 | Appl B A ⇒ {b}@(boolean b B).(boolean b A)
25 ].
26
27 interpretation "boolean subset (subterms)"
28    'ProjectUp b M = (boolean b M).
29
30 notation "hvbox( { term 46 b } ⇑ break term 46 M)"
31    non associative with precedence 46
32    for @{ 'ProjectUp $b $M }.
33
34 lemma boolean_inv_vref: ∀j,b0,b,M. {b}⇑ M = {b0}#j → b = b0 ∧ M = #j.
35 #j #b0 #b * normalize
36 [ #i #H destruct /2 width=1/
37 | #A #H destruct
38 | #B #A #H destruct
39 ]
40 qed-.
41
42 lemma boolean_inv_abst: ∀U,b0,b,M. {b}⇑ M = {b0}𝛌.U →
43                         ∃∃C. b = b0 & {b}⇑C = U & M = 𝛌.C.
44 #U #b0 #b * normalize
45 [ #i #H destruct
46 | #A #H destruct /2 width=3/
47 | #B #A #H destruct
48 ]
49 qed-.
50
51 lemma boolean_inv_appl: ∀W,U,b0,b,M. {b}⇑ M = {b0}@W.U →
52                         ∃∃D,C. b = b0 & {b}⇑D = W & {b}⇑C = U & M = @D.C.
53 #W #U #b0 #b * normalize
54 [ #i #H destruct
55 | #A #H destruct
56 | #B #A #H destruct /2 width=5/
57 ]
58 qed-.
59
60 (* Note: the carrier (underlying term) of a subset of subterms *)
61 let rec carrier F on F ≝ match F with
62 [ SVRef _ i   ⇒ #i
63 | SAbst _ T   ⇒ 𝛌.(carrier T)
64 | SAppl _ V T ⇒ @(carrier V).(carrier T)
65 ].
66
67 interpretation "carrier (subterms)"
68    'ProjectDown F = (carrier F).
69
70 notation "hvbox(⇓ term 46 F)"
71    non associative with precedence 46
72    for @{ 'ProjectDown $F }.
73
74 lemma carrier_inv_vref: ∀j,F. ⇓F = #j → ∃b. F = {b}#j.
75 #j * normalize
76 [ #b #i #H destruct /2 width=2/
77 | #b #T #H destruct
78 | #b #V #T #H destruct
79 ]
80 qed-.
81
82 lemma carrier_inv_abst: ∀C,F. ⇓F = 𝛌.C → ∃∃b,U. ⇓U = C & F = {b}𝛌.U.
83 #C * normalize
84 [ #b #i #H destruct
85 | #b #T #H destruct /2 width=4/
86 | #b #V #T #H destruct
87 ]
88 qed-.
89
90 lemma carrier_inv_appl: ∀D,C,F. ⇓F = @D.C →
91                         ∃∃b,W,U. ⇓W = D & ⇓U = C & F = {b}@W.U.
92 #D #C * normalize
93 [ #b #i #H destruct
94 | #b #T #H destruct
95 | #b #V #T #H destruct /2 width=6/
96 ]
97 qed-.
98
99 definition mk_boolean: bool → subterms → subterms ≝
100    λb,F. {b}⇑⇓F.
101
102 interpretation "make boolean (subterms)"
103    'ProjectSame b F = (mk_boolean b F).
104
105 notation "hvbox( { term 46 b } ⇕ break term 46 F)"
106    non associative with precedence 46
107    for @{ 'ProjectSame $b $F }.
108
109 lemma mk_boolean_inv_vref: ∀j,b0,b,F. {b}⇕ F = {b0}#j →
110                            ∃∃b1. b = b0 & F = {b1}#j.
111 #j #b0 #b #F #H
112 elim (boolean_inv_vref … H) -H #H0 #H
113 elim (carrier_inv_vref … H) -H /2 width=2/
114 qed-.
115
116 lemma mk_boolean_inv_abst: ∀U,b0,b,F. {b}⇕ F = {b0}𝛌.U →
117                            ∃∃b1,T. b = b0 & {b}⇕T = U & F = {b1}𝛌.T.
118 #U #b0 #b #F #H
119 elim (boolean_inv_abst … H) -H #C #H0 #H1 #H
120 elim (carrier_inv_abst … H) -H #b1 #U1 #H3 destruct /2 width=4/
121 qed-.
122
123 lemma mk_boolean_inv_appl: ∀W,U,b0,b,F. {b}⇕ F = {b0}@W.U →
124                            ∃∃b1,V,T. b = b0 & {b}⇕V = W & {b}⇕T = U & F = {b1}@V.T.
125 #W #U #b0 #b #F #H
126 elim (boolean_inv_appl … H) -H #D #C #H0 #H1 #H2 #H
127 elim (carrier_inv_appl … H) -H #b1 #W1 #U1 #H3 #H4 destruct /2 width=6/
128 qed-.