]> matita.cs.unibo.it Git - helm.git/blob - matita/matita/lib/pts_dummy/subterms.ma
Many changes
[helm.git] / matita / matita / lib / pts_dummy / subterms.ma
1 (*
2     ||M||  This file is part of HELM, an Hypertextual, Electronic        
3     ||A||  Library of Mathematics, developed at the Computer Science     
4     ||T||  Department of the University of Bologna, Italy.                     
5     ||I||                                                                 
6     ||T||  
7     ||A||  This file is distributed under the terms of the 
8     \   /  GNU General Public License Version 2        
9      \ /      
10       V_______________________________________________________________ *)
11
12 include "pts_dummy/subst.ma".
13 (*
14 inductive subterm : T → T → Prop ≝
15   | appl : ∀M,N. subterm M (App M N)
16   | appr : ∀M,N. subterm N (App M N)
17   | lambdal : ∀M,N. subterm M (Lambda M N)
18   | lambdar : ∀M,N. subterm N (Lambda M N)
19   | prodl : ∀M,N. subterm M (Prod M N)
20   | prodr : ∀M,N. subterm N (Prod M N)
21   | sub_b : ∀M. subterm M (D M)
22   | sub_trans : ∀M,N,P. subterm M N → subterm N P → subterm M P.
23
24 inverter subterm_myinv for subterm (?%).
25
26 lemma subapp: ∀S,M,N. subterm S (App M N) →
27  S = M ∨ S = N ∨ subterm S M ∨ subterm S N. 
28 #S #M #N #subH (@(subterm_myinv … subH))
29   [#M1 #N1 #eqapp destruct /4/
30   |#M1 #N1 #eqapp destruct /4/
31   |3,4,5,6: #M1 #N1 #eqapp destruct
32   |#M1 #eqapp destruct
33   |#M1 #N1 #P #sub1 #sub2 #H1 #H2 #eqapp
34    (cases (H2 eqapp))
35     [* [* /3/ | #subN1 %1 %2 /2/ ] 
36     |#subN1 %2 /2/
37     ]
38   ]
39 qed.
40  
41 lemma sublam: ∀S,M,N. subterm S (Lambda M N) →
42  S = M ∨ S = N ∨ subterm S M ∨ subterm S N. 
43 #S #M #N #subH (@(subterm_myinv … subH))
44   [1,2,5,6: #M1 #N1 #eqH destruct
45   |3,4:#M1 #N1 #eqH destruct /4/
46   |#M1 #eqH destruct
47   |#M1 #N1 #P #sub1 #sub2 #H1 #H2 #eqH
48    (cases (H2 eqH))
49     [* [* /3/ | #subN1 %1 %2 /2/ ] 
50     |#subN1 %2 /2/
51     ]
52   ]
53 qed.  
54
55 lemma subprod: ∀S,M,N. subterm S (Prod M N) →
56  S = M ∨ S = N ∨ subterm S M ∨ subterm S N. 
57 #S #M #N #subH (@(subterm_myinv … subH))
58   [1,2,3,4: #M1 #N1 #eqH destruct
59   |5,6:#M1 #N1 #eqH destruct /4/
60   |#M1 #eqH destruct
61   |#M1 #N1 #P #sub1 #sub2 #H1 #H2 #eqH
62    (cases (H2 eqH))
63     [* [* /3/ | #subN1 %1 %2 /2/ ] 
64     |#subN1 %2 /2/
65     ]
66   ]
67 qed.
68
69 lemma subd: ∀S,M. subterm S (D M) →
70  S = M ∨ subterm S M. 
71 #S #M #subH (@(subterm_myinv … subH))
72   [1,2,3,4,5,6: #M1 #N1 #eqH destruct
73   |#M1 #eqH destruct /2/
74   |#M1 #N1 #P #sub1 #sub2 #_ #H #eqH
75    (cases (H eqH)) /2/
76     #subN1 %2 /2/
77   ]
78 qed.    
79
80 lemma subsort: ∀S,n. ¬ subterm S (Sort n).
81 #S #n % #subH (@(subterm_myinv … subH))
82   [1,2,3,4,5,6: #M1 #N1 #eqH destruct
83   |#M1 #eqa destruct
84   |/2/
85   ]
86 qed.
87
88 lemma subrel: ∀S,n. ¬ subterm S (Rel n).
89 #S #n % #subH (@(subterm_myinv … subH))
90   [1,2,3,4,5,6: #M1 #N1 #eqH destruct
91   |#M1 #eqa destruct
92   |/2/
93   ]
94 qed.
95
96 theorem Telim: ∀P: T → Prop. (∀M. (∀N. subterm N M → P N) → P M) →
97  ∀M. P M.
98 #P #H #M (cut (P M ∧ (∀N. subterm N M → P N)))
99   [2: * //]
100 (elim M)
101   [#n %
102     [@H #N1 #subN1 @False_ind /2/
103     |#N #subN1 @False_ind /2/
104     ]
105   |#n %
106     [@H #N1 #subN1 @False_ind /2/
107     |#N #subN1 @False_ind /2/
108     ]
109   |#M1 #M2 * #PM1 #Hind1 * #PM2 #Hind2 
110    (cut (∀N.subterm N (App M1 M2) → P N))
111     [#N1 #subN1 (cases (subapp … subN1))
112       [* [* // | @Hind1 ] | @Hind2 ]]
113     #Hcut % /3/
114   |#M1 #M2 * #PM1 #Hind1 * #PM2 #Hind2 
115    (cut (∀N.subterm N (Lambda M1 M2) → P N))
116     [#N1 #subN1 (cases (sublam … subN1))
117       [* [* // | @Hind1 ] | @Hind2 ]]
118    #Hcut % /3/
119   |#M1 #M2 * #PM1 #Hind1 * #PM2 #Hind2 
120    (cut (∀N.subterm N (Prod M1 M2) → P N))
121     [#N1 #subN1 (cases (subprod … subN1))
122       [* [* // | @Hind1 ] | @Hind2 ]]
123    #Hcut % /3/   
124   |#M1 * #PM1 #Hind1
125    (cut (∀N.subterm N (D M1) → P N))
126     [#N1 #subN1 (cases (subd … subN1)) /2/]
127    #Hcut % /3/  
128   ]  
129 qed.
130
131 let rec size M ≝
132 match M with
133   [Sort N ⇒ 1
134   |Rel N ⇒ 1
135   |App P Q ⇒ size P + size Q + 1
136   |Lambda P Q ⇒ size P + size Q + 1
137   |Prod P Q ⇒ size P + size Q + 1
138   |D P ⇒ size P + 1
139   ]
140 .
141
142 (* axiom pos_size: ∀M. 1 ≤ size M. *)
143
144 theorem Telim_size: ∀P: T → Prop. 
145  (∀M. (∀N. size N < size M → P N) → P M) → ∀M. P M.
146 #P #H #M (cut (∀p,N. size N = p → P N))
147   [2: /2/]
148 #p @(nat_elim1 p) #m #H1 #N #sizeN @H #N0 #Hlt @(H1 (size N0)) //
149 qed.
150
151 (* size of subterms *)
152
153 lemma size_subterm : ∀N,M. subterm N M → size N < size M.
154 #N #M #subH (elim subH) normalize //
155 #M1 #N1 #P #sub1 #sub2 #size1 #size2 @(transitive_lt … size1 size2)
156 qed.
157 *)