]> matita.cs.unibo.it Git - helm.git/blob - helm/software/matita/nlibrary/topology/igft-setoid.ma
Use the inversion!
[helm.git] / helm / software / matita / nlibrary / topology / igft-setoid.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 "sets/sets.ma".
16
17 nrecord category : Type[2] ≝
18  { objs:> Type[1];
19    arrows: objs → objs → setoid;
20    id: ∀o:objs. arrows o o;
21    comp: ∀o1,o2,o3. unary_morphism (arrows o1 o2) (unary_morph_setoid (arrows o2 o3) (arrows o1 o3));
22    comp_assoc: ∀o1,o2,o3,o4. ∀a12,a23,a34.
23     comp o1 o3 o4 (comp o1 o2 o3 a12 a23) a34 = comp o1 o2 o4 a12 (comp o2 o3 o4 a23 a34);
24    id_neutral_left: ∀o1,o2. ∀a: arrows o1 o2. comp ??? (id o1) a = a;
25    id_neutral_right: ∀o1,o2. ∀a: arrows o1 o2. comp ??? a (id o2) = a
26  }.
27
28 notation "hvbox(A break ⇒ B)" right associative with precedence 50 for @{ 'arrows $A $B }.
29 interpretation "arrows" 'arrows A B = (unary_morphism A B).
30
31 notation > "𝐈𝐝 term 90 A" non associative with precedence 90 for @{ 'id $A }.
32 notation < "mpadded width -90% (𝐈) 𝐝 \sub term 90 A" non associative with precedence 90 for @{ 'id $A }.
33
34 interpretation "id" 'id A = (id ? A).
35
36 ndefinition SETOID : category.
37 @; 
38 ##[ napply setoid;
39 ##| napply unary_morph_setoid;
40 ##| #o; @ (λx.x); //
41 ##| #o1; #o2; #o3; napply mk_binary_morphism [ #f; #g; @(λx.g (f x)) ]
42     nnormalize; /3/
43 ##| nnormalize; /4/
44 ##|##6,7: nnormalize; /2/ ]
45 nqed.
46
47 unification hint 0 ≔ ;
48    R ≟ (mk_category setoid unary_morph_setoid (id SETOID) (comp SETOID)
49           (comp_assoc SETOID) (id_neutral_left SETOID)
50           (id_neutral_right SETOID))
51  (* -------------------------------------------------------------------- *) ⊢
52                               objs R ≡ setoid.
53                               
54  unification hint 0 ≔ x,y ;
55    R ≟ (mk_category setoid unary_morph_setoid (id SETOID) (comp SETOID)
56           (comp_assoc SETOID) (id_neutral_left SETOID)
57           (id_neutral_right SETOID))
58  (* -------------------------------------------------------------------- *) ⊢
59                   arrows R x y ≡ unary_morph_setoid x y. 
60                   
61 unification hint 0 ≔ A,B ;               
62                   T ≟ (unary_morph_setoid A B)
63            (* ----------------------------------- *) ⊢              
64                   unary_morphism A B ≡ carr T. 
65                 
66                 
67 ndefinition TYPE : setoid1.
68 @ setoid; @; 
69 ##[ #T1; #T2; 
70     alias symbol "eq" = "setoid eq".
71     napply (∃f:T1 ⇒ T2.∃g:T2 ⇒ T1. (∀x.f (g x) = x) ∧ (∀y.g (f y) = y));
72 ##| #A; @ (𝐈𝐝 A); @ (𝐈𝐝 A); @; #x; napply #;
73 ##| #A; #B; *; #f; *; #g; *; #Hfg; #Hgf; @g; @f; @; nassumption; 
74 ##| #A; #B; #C; *; #f; *; #f'; *; #Hf; #Hf'; *; #g; *; #g'; *; #Hg; #Hg'; 
75     @; ##[ @(λx.g (f x)); #a; #b; #H; napply (.= (††H)); napply #;
76        ##| @; ##[ @(λx.f'(g' x)); #a; #b; #H; napply (.= (††H)); napply #; ##]
77     @; #x;
78     ##[ napply (.= (†(Hf …))); napply Hg;
79     ##| napply (.= (†(Hg' …))); napply Hf'; ##] ##] 
80 nqed.
81
82 unification hint 0 ≔ ;
83           R ≟ (mk_setoid1 setoid (eq1 TYPE))
84   (* -------------------------------------------- *) ⊢
85                  carr1 R ≡ setoid.
86    
87 nrecord unary_morphism01 (A : setoid) (B: setoid1) : Type[1] ≝
88  { fun01:1> A → B;
89    prop01: ∀a,a'. eq ? a a' → eq1 ? (fun01 a) (fun01 a')
90  }.
91  
92 interpretation "prop01" 'prop1 c  = (prop01 ????? c).
93
94 nrecord nAx : Type[1] ≝ { 
95   nS:> setoid; 
96   nI: unary_morphism01 nS TYPE;
97   nD: ∀a:nS. unary_morphism01 (nI a) TYPE;
98   nd: ∀a:nS. ∀i:nI a. unary_morphism (nD a i) nS
99 }.
100
101 notation "𝐃 \sub ( ❨a,\emsp i❩ )" non associative with precedence 70 for @{ 'D $a $i }.
102 notation "𝐝 \sub ( ❨a,\emsp i,\emsp j❩ )" non associative with precedence 70 for @{ 'd $a $i $j}.
103 notation "𝐈  \sub( ❨a❩ )" non associative with precedence 70 for @{ 'I $a }.
104
105 notation > "𝐈 term 90 a" non associative with precedence 70 for @{ 'I $a }.
106 notation > "𝐃 term 90 a term 90 i" non associative with precedence 70 for @{ 'D $a $i }.
107 notation > "𝐝 term 90 a term 90 i term 90 j" non associative with precedence 70 for @{ 'd $a $i $j}.
108
109 interpretation "D" 'D a i = (nD ? a i).
110 interpretation "d" 'd a i j = (nd ? a i j).
111 interpretation "new I" 'I a = (nI ? a).
112
113 ndefinition image ≝ λA:nAx.λa:A.λi. { x | ∃j:𝐃 a i. x = 𝐝 a i j }.
114 (*
115 nlemma elim_eq_TYPE : ∀A,B:setoid.∀P:CProp[1]. A=B → ((B ⇒ A) → P) → P.
116 #A; #B; #P; *; #f; *; #g; #_; #IH; napply IH; napply g;
117 nqed.
118
119 ninductive squash (A : Type[1]) : CProp[1] ≝
120   | hide : A → squash A.     
121
122 nrecord unary_morphism_dep (A : setoid) (T:unary_morphism01 A TYPE) : Type[1] ≝ {
123   fun_dep  : ∀a:A.(T a);
124   prop_dep : ∀a,b:A. ∀H:a = b. 
125     ? (prop01 … T … H) }.
126 ##[##3: *; 
127     
128      (λf.hide ? (eq_rel ? (eq (T a)) (fun_dep a) (f (fun_dep b))))  
129 }.
130 ##[##2: nletin lhs ≝ (fun_dep a:?); nletin rhs ≝ (fun_dep b:?);
131         nletin patched_rhs ≝ (f rhs : ?);
132         nlapply (lhs = patched_rhs);
133         *)
134
135 (*
136 nlemma foo: ∀A:setoid.∀T:unary_morphism01 A TYPE.∀P:∀x:A.∀a:T x.CProp[0].
137     ∀x,y:A.x=y → (∃a:T x.P ? a) = (∃a:T y.P ? a).
138 #A; #T; #P; #x; #y; #H; ncases (prop01 … T … H); #f; *; #g; *; #Hf; #Hg;
139 @; *; #e; #He;
140 ##[ @(f e);   
141 *)
142
143 ndefinition image_is_ext : ∀A:nAx.∀a:A.∀i:𝐈 a.𝛀^A.
144 #A; #a; #i; @ (image … i); #x; #y; #H; @;
145 ##[ *; #d; #Ex; @ d; napply (.= H^-1); nassumption;
146 ##| *; #d; #Ex; @ d; napply (.= H); nassumption; ##]
147 nqed.
148
149 unification hint 0 ≔ A,a,i ;
150        R ≟ (mk_ext_powerclass ? (image A a i) (ext_prop ? (image_is_ext A a i)))
151  (* --------------------------------------------------------------- *) ⊢
152       ext_carr A R ≡ (image A a i).
153
154 notation > "𝐈𝐦  [𝐝 term 90 a term 90 i]" non associative with precedence 70 for @{ 'Im $a $i }.
155 notation < "mpadded width -90% (𝐈) 𝐦  [𝐝 \sub ( ❨a,\emsp i❩ )]" non associative with precedence 70 for @{ 'Im $a $i }.
156
157 interpretation "image" 'Im a i = (image ? a i).
158
159 ninductive Ord (A : nAx) : Type[0] ≝ 
160  | oO : Ord A
161  | oS : Ord A → Ord A
162  | oL : ∀a:A.∀i.∀f:𝐃 a i → Ord A. Ord A.
163
164 notation "0" non associative with precedence 90 for @{ 'oO }.
165 notation "Λ term 90 f" non associative with precedence 50 for @{ 'oL $f }.
166 notation "x+1" non associative with precedence 50 for @{'oS $x }.
167
168 interpretation "ordinals Zero" 'oO = (oO ?).
169 interpretation "ordinals Lambda" 'oL f = (oL ? ? ? f).
170 interpretation "ordinals Succ" 'oS x = (oS ? x).
171
172 (* manca russell *)
173 nlet rec famU (A : nAx) (U : 𝛀^A) (x : Ord A) on x : 𝛀^A ≝ 
174   match x with
175   [ oO ⇒ mk_ext_powerclass A U ?
176   | oS y ⇒ let Un ≝ famU A U y in mk_ext_powerclass A (Un ∪ { x | ∃i.𝐈𝐦[𝐝 x i] ⊆ Un}) ? 
177   | oL a i f ⇒ mk_ext_powerclass A { x | ∃j.x ∈ famU A U (f j) } ? ].
178 ##[ #x; #y; #H; alias symbol "trans" = "trans1".
179     alias symbol "prop2" = "prop21".
180     napply (.= (H‡#)); napply #;
181 ##| #x; #y; #H; @; *;
182     ##[##1,3: #E; @1; ##[ napply (. (ext_prop A Un … H^-1)); ##| napply (. (ext_prop A Un … H)); ##]
183               nassumption;
184     ##|##*: *; #i; #H1; @2; 
185             ##[ nlapply (†H); ##[ napply (nI A); ##| ##skip ##]
186                 #W; ncases W; #f; *; #g; *; #Hf; #Hg;
187                 @ (f i); #a; #Ha; napply H1;
188                 ncut (𝐈𝐦[𝐝 y (f i)] = 𝐈𝐦[𝐝 x i]); 
189                 
190                 ##[##2: #E; napply (. (#‡E^-1)); napply Ha; ##]
191                         
192                 @; #w; #Hw; nwhd;
193                 ncut (𝐈𝐦[𝐝 y (f i)] = 𝐈𝐦[𝐝 x i]);                    
194                   
195 (*    
196   
197 notation < "term 90 U \sub (term 90 x)" non associative with precedence 50 for @{ 'famU $U $x }.
198 notation > "U ⎽ term 90 x" non associative with precedence 50 for @{ 'famU $U $x }.
199
200 interpretation "famU" 'famU U x = (famU ? U x).
201
202 (*D
203
204 We attach as the input notation for U_x the similar `U⎽x` where underscore,
205 that is a character valid for identifier names, has been replaced by `⎽` that is
206 not. The symbol `⎽` can act as a separator, and can be typed as an alternative
207 for `_` (i.e. pressing ALT-L after `_`). 
208
209 The notion ◃(U) has to be defined as the subset of of y 
210 belonging to U_x for some x. Moreover, we have to define the notion
211 of cover between sets again, since the one defined at the beginning
212 of the tutorial works only for the old axiom set definition.
213
214 D*)
215   
216 ndefinition ord_coverage : ∀A:nAx.∀U:Ω^A.Ω^A ≝ λA,U.{ y | ∃x:Ord A. y ∈ famU ? U x }.
217
218 ndefinition ord_cover_set ≝ λc:∀A:nAx.Ω^A → Ω^A.λA,C,U.
219   ∀y.y ∈ C → y ∈ c A U.
220
221 interpretation "coverage new cover" 'coverage U = (ord_coverage ? U).
222 interpretation "new covers set" 'covers a U = (ord_cover_set ord_coverage ? a U).
223 interpretation "new covers" 'covers a U = (mem ? (ord_coverage ? U) a).
224
225 (*D
226
227 Before proving that this cover relation validates the reflexivity and infinity
228 rules, we prove this little technical lemma that is used in the proof for the 
229 infinity rule.
230
231 D*)
232
233 nlemma ord_subset:
234   ∀A:nAx.∀a:A.∀i,f,U.∀j:𝐃 a i.U⎽(f j) ⊆ U⎽(Λ f).
235 #A; #a; #i; #f; #U; #j; #b; #bUf; @ j; nassumption;
236 nqed.
237
238 (*D
239
240 The proof of infinity uses the following form of the Axiom of choice,
241 that cannot be prove inside Matita, since the existential quantifier
242 lives in the sort of predicative propositions while the sigma in the conclusion
243 lives in the sort of data types, and thus the former cannot be eliminated
244 to provide the second.
245
246 D*)
247
248 naxiom AC : ∀A,a,i,U.
249   (∀j:𝐃 a i.∃x:Ord A.𝐝 a i j ∈ U⎽x) → (Σf.∀j:𝐃 a i.𝐝 a i j ∈ U⎽(f j)).
250
251 (*D
252
253 In the proof of infinity, we have to rewrite under the ∈ predicate.
254 It is clearly possible to show that U_x is an extensional set:
255
256 > a=b → a ∈ U_x → b ∈ U_x
257
258 Anyway this proof in non trivial induction over x, that requires 𝐈 and 𝐃 to be
259 declared as morphisms. This poses to problem, but goes out of the scope of the 
260 tutorial and we thus assume it.
261
262 D*)
263
264 naxiom setoidification :
265   ∀A:nAx.∀a,b:A.∀x.∀U.a=b → b ∈ U⎽x → a ∈ U⎽x.
266
267 (*D
268
269 The reflexivity proof is trivial, it is enough to provide the ordinal 0
270 as a witness, then ◃(U) reduces to U by definition, hence the conclusion.
271
272 D*)
273 ntheorem new_coverage_reflexive:
274   ∀A:nAx.∀U:Ω^A.∀a. a ∈ U → a ◃ U.
275 #A; #U; #a; #H; @ (0); napply H;
276 nqed.
277
278 (*D
279
280 We now proceed with the proof of the infinity rule.
281
282 D*)
283
284 alias symbol "covers" = "new covers set".
285 alias symbol "covers" = "new covers".
286 alias symbol "covers" = "new covers set".
287 alias symbol "covers" = "new covers".
288 alias symbol "covers" = "new covers set".
289 alias symbol "covers" = "new covers".
290 ntheorem new_coverage_infinity:
291   ∀A:nAx.∀U:Ω^A.∀a:A. (∃i:𝐈 a. 𝐈𝐦[𝐝 a i] ◃ U) → a ◃ U.
292 #A; #U; #a;                                   (** screenshot "n-cov-inf-1". *)  
293 *; #i; #H; nnormalize in H;                   (** screenshot "n-cov-inf-2". *)
294 ncut (∀y:𝐃 a i.∃x:Ord A.𝐝 a i y ∈ U⎽x); ##[    (** screenshot "n-cov-inf-3". *)
295   #z; napply H; @ z; napply #; ##] #H';       (** screenshot "n-cov-inf-4". *)
296 ncases (AC … H'); #f; #Hf;                    (** screenshot "n-cov-inf-5". *)
297 ncut (∀j.𝐝 a i j ∈ U⎽(Λ f));
298   ##[ #j; napply (ord_subset … f … (Hf j));##] #Hf';(** screenshot "n-cov-inf-6". *)
299 @ (Λ f+1);                                    (** screenshot "n-cov-inf-7". *)
300 @2;                                           (** screenshot "n-cov-inf-8". *) 
301 @i; #x; *; #d; #Hd;                           (** screenshot "n-cov-inf-9". *)  
302 napply (setoidification … Hd); napply Hf';
303 nqed.
304
305 (*D
306 D[n-cov-inf-1]
307 We eliminate the existential, obtaining an `i` and a proof that the 
308 image of d(a,i) is covered by U. The `nnormalize` tactic computes the normal
309 form of `H`, thus expands the definition of cover between sets.
310
311 D[n-cov-inf-2]
312 The paper proof considers `H` implicitly substitutes the equation assumed
313 by `H` in its conclusion. In Matita this step is not completely trivia.
314 We thus assert (`ncut`) the nicer form of `H`.
315
316 D[n-cov-inf-3]
317 After introducing `z`, `H` can be applied (choosing `𝐝 a i z` as `y`). 
318 What is the left to prove is that `∃j: 𝐃 a j. 𝐝 a i z = 𝐝 a i j`, that 
319 becomes trivial is `j` is chosen to be `z`. In the command `napply #`,
320 the `#` is a standard notation for the reflexivity property of the equality. 
321
322 D[n-cov-inf-4]
323 Under `H'` the axiom of choice `AC` can be eliminated, obtaining the `f` and 
324 its property.
325
326 D[n-cov-inf-5]
327 The paper proof does now a forward reasoning step, deriving (by the ord_subset 
328 lemma we proved above) `Hf'` i.e. 𝐝 a i j ∈ U⎽(Λf).
329
330 D[n-cov-inf-6]
331 To prove that `a◃U` we have to exhibit the ordinal x such that `a ∈ U⎽x`.
332
333 D[n-cov-inf-7]
334 The definition of `U⎽(…+1)` expands to the union of two sets, and proving
335 that `a ∈ X ∪ Y` is defined as proving that `a` is in `X` or `Y`. Applying
336 the second constructor `@2;` of the disjunction, we are left to prove that `a` 
337 belongs to the right hand side.
338
339 D[n-cov-inf-8]
340 We thus provide `i`, introduce the element being in the image and we are
341 left to prove that it belongs to `U_(Λf)`. In the meanwhile, since belonging 
342 to the image means that there exists an object in the domain… we eliminate the
343 existential, obtaining `d` (of type `𝐃 a i`) and the equation defining `x`.  
344
345 D[n-cov-inf-9]
346 We just need to use the equational definition of `x` to obtain a conclusion
347 that can be proved with `Hf'`. We assumed that `U_x` is extensional for
348 every `x`, thus we are allowed to use `Hd` and close the proof.
349
350 D*)
351
352 (*D
353
354 The next proof is that ◃(U) is mininal. The hardest part of the proof
355 it to prepare the goal for the induction. The desiderata is to prove
356 `U⎽o ⊆ V` by induction on `o`, but the conclusion of the lemma is,
357 unfolding all definitions:
358
359 > ∀x. x ∈ { y | ∃o:Ord A.y ∈ U⎽o } → x ∈ V
360
361 D*)
362
363 nlemma new_coverage_min :  
364   ∀A:nAx.∀U:Ω^A.∀V.U ⊆ V → (∀a:A.∀i.𝐈𝐦[𝐝 a i] ⊆ V → a ∈ V) → ◃U ⊆ V.
365 #A; #U; #V; #HUV; #Im;#b;                       (** screenshot "n-cov-min-2". *)
366 *; #o;                                          (** screenshot "n-cov-min-3". *)
367 ngeneralize in match b; nchange with (U⎽o ⊆ V); (** screenshot "n-cov-min-4". *)
368 nelim o;                                        (** screenshot "n-cov-min-5". *) 
369 ##[ #b; #bU0; napply HUV; napply bU0;
370 ##| #p; #IH; napply subseteq_union_l; ##[ nassumption; ##]
371     #x; *; #i; #H; napply (Im ? i); napply (subseteq_trans … IH); napply H;
372 ##| #a; #i; #f; #IH; #x; *; #d; napply IH; ##]
373 nqed.
374
375 (*D
376 D[n-cov-min-2]
377 After all the introductions, event the element hidden in the ⊆ definition,
378 we have to eliminate the existential quantifier, obtaining the ordinal `o`
379
380 D[n-cov-min-3]
381 What is left is almost right, but the element `b` is already in the
382 context. We thus generalize every occurrence of `b` in 
383 the current goal, obtaining `∀c.c ∈ U⎽o → c ∈ V` that is `U⎽o ⊆ V`.
384
385 D[n-cov-min-4]
386 We then proceed by induction on `o` obtaining the following goals
387
388 D[n-cov-min-5]
389 All of them can be proved using simple set theoretic arguments,
390 the induction hypothesis and the assumption `Im`.
391
392 D*)
393
394
395 (*D
396
397 bla bla
398
399 D*)
400
401 nlet rec famF (A: nAx) (F : Ω^A) (x : Ord A) on x : Ω^A ≝ 
402   match x with
403   [ oO ⇒ F
404   | oS o ⇒ let Fo ≝ famF A F o in Fo ∩ { x | ∀i:𝐈 x.∃j:𝐃 x i.𝐝 x i j ∈ Fo } 
405   | oL a i f ⇒ { x | ∀j:𝐃 a i.x ∈ famF A F (f j) }
406   ].
407
408 interpretation "famF" 'famU U x = (famF ? U x).
409
410 ndefinition ord_fished : ∀A:nAx.∀F:Ω^A.Ω^A ≝ λA,F.{ y | ∀x:Ord A. y ∈ F⎽x }.
411
412 interpretation "fished new fish" 'fished U = (ord_fished ? U).
413 interpretation "new fish" 'fish a U = (mem ? (ord_fished ? U) a).
414
415 (*D
416
417 The proof of compatibility uses this little result, that we 
418 factored out. 
419
420 D*)
421 nlemma co_ord_subset:
422  ∀A:nAx.∀F:Ω^A.∀a,i.∀f:𝐃 a i → Ord A.∀j. F⎽(Λ f) ⊆ F⎽(f j).
423 #A; #F; #a; #i; #f; #j; #x; #H; napply H;
424 nqed.
425
426 (*D
427
428 We assume the dual of the axiom of choice, as in the paper proof.
429
430 D*)
431 naxiom AC_dual : 
432   ∀A:nAx.∀a:A.∀i,F. (∀f:𝐃 a i → Ord A.∃x:𝐃 a i.𝐝 a i x ∈ F⎽(f x)) → ∃j:𝐃 a i.∀x:Ord A.𝐝 a i j ∈ F⎽x.
433
434 (*D
435
436 Proving the anti-reflexivity property is simce, since the
437 assumption `a ⋉ F` states that for every ordinal `x` (and thus also 0)
438 `a ∈ F⎽x`. If `x` is choosen to be `0`, we obtain the thesis.
439
440 D*)
441 ntheorem new_fish_antirefl:
442  ∀A:nAx.∀F:Ω^A.∀a. a ⋉ F → a ∈ F.
443 #A; #F; #a; #H; nlapply (H 0); #aFo; napply aFo;
444 nqed.
445
446 (*D
447
448 bar
449
450 D*)
451 ntheorem new_fish_compatible: 
452  ∀A:nAx.∀F:Ω^A.∀a. a ⋉ F → ∀i:𝐈 a.∃j:𝐃 a i.𝐝 a i j ⋉ F.
453 #A; #F; #a; #aF; #i; nnormalize;               (** screenshot "n-f-compat-1". *)
454 napply AC_dual; #f;                            (** screenshot "n-f-compat-2". *)
455 nlapply (aF (Λf+1)); #aLf;                     (** screenshot "n-f-compat-3". *)
456 nchange in aLf with 
457   (a ∈ F⎽(Λ f) ∧ ∀i:𝐈 a.∃j:𝐃 a i.𝐝 a i j ∈ F⎽(Λ f)); (** screenshot "n-f-compat-4". *)
458 ncut (∃j:𝐃 a i.𝐝 a i j ∈ F⎽(f j));##[
459   ncases aLf; #_; #H; nlapply (H i);               (** screenshot "n-f-compat-5". *) 
460   *; #j; #Hj; @j; napply Hj;##] #aLf';             (** screenshot "n-f-compat-6". *)
461 napply aLf';
462 nqed.
463
464 (*D
465 D[n-f-compat-1]
466 D[n-f-compat-2]
467 D[n-f-compat-3]
468 D[n-f-compat-4]
469 D[n-f-compat-5]
470 D[n-f-compat-6]
471
472 D*)
473
474 (*D
475
476 The proof that `⋉(F)` is maximal is exactly the dual one of the
477 minimality of `◃(U)`. Thus the main problem is to obtain `G ⊆ F⎽o`
478 before doing the induction over `o`.
479
480 D*)
481 ntheorem max_new_fished: 
482   ∀A:nAx.∀G:ext_powerclass_setoid A.∀F:Ω^A.G ⊆ F → (∀a.a ∈ G → ∀i.𝐈𝐦[𝐝 a i] ≬ G) → G ⊆ ⋉F.
483 #A; #G; #F; #GF; #H; #b; #HbG; #o; 
484 ngeneralize in match HbG; ngeneralize in match b;
485 nchange with (G ⊆ F⎽o);
486 nelim o;
487 ##[ napply GF;
488 ##| #p; #IH; napply (subseteq_intersection_r … IH);
489     #x; #Hx; #i; ncases (H … Hx i); #c; *; *; #d; #Ed; #cG;
490     @d; napply IH;
491     alias symbol "prop2" = "prop21".
492 napply (. Ed^-1‡#); napply cG;    
493 ##| #a; #i; #f; #Hf; nchange with (G ⊆ { y | ∀x. y ∈ F⎽(f x) }); 
494     #b; #Hb; #d; napply (Hf d); napply Hb;
495 ##]
496 nqed.
497
498
499 (*D
500 <div id="appendix" class="anchor"></div>
501 Appendix: tactics explanation
502 -----------------------------
503
504 In this appendix we try to give a description of tactics
505 in terms of sequent calculus rules annotated with proofs.
506 The `:` separator has to be read as _is a proof of_, in the spirit
507 of the Curry-Howard isomorphism.
508
509                   Γ ⊢  f  :  A1 → … → An → B    Γ ⊢ ?1 : A1 … ?n  :  An 
510     napply f;    ⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼
511                            Γ ⊢ (f ?1 … ?n )  :  B
512  
513                    Γ ⊢  ?  :  F → B       Γ ⊢ f  :  F 
514     nlapply f;    ⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼
515                              Γ ⊢ (? f)  :  B
516
517
518                  Γ; x : T  ⊢ ?  :  P(x) 
519     #x;      ⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼
520                 Γ ⊢ λx:T.?  :  ∀x:T.P(x)
521
522                        
523                        Γ ⊢ ?_i  :  args_i → P(k_i args_i)          
524     ncases x;   ⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼
525                 Γ ⊢ match x with [ k1 args1 ⇒ ?_1 | … | kn argsn ⇒ ?_n ]  :  P(x)                    
526
527
528                       Γ ⊢ ?i  :  ∀t. P(t) → P(k_i … t …)          
529     nelim x;   ⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼
530                    Γ ⊢ (T_rect_CProp0 ?_1 … ?_n)  :  P(x)                    
531
532 Where `T_rect_CProp0` is the induction principle for the 
533 inductive type `T`.
534
535                           Γ ⊢ ?  :  Q     Q ≡ P          
536     nchange with Q;   ⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼
537                           Γ ⊢ ?  :  P                    
538
539 Where the equivalence relation between types `≡` keeps into account
540 β-reduction, δ-reduction (definition unfolding), ζ-reduction (local
541 definition unfolding), ι-reduction (pattern matching simplification),
542 μ-reduction (recursive function computation) and ν-reduction (co-fixpoint
543 computation).
544
545
546                                Γ; H : Q; Δ ⊢ ?  :  G     Q ≡ P          
547     nchange in H with Q; ⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼
548                                Γ; H : P; Δ ⊢ ?  :  G                    
549
550
551
552                     Γ ⊢ ?_2  :  T → G    Γ ⊢ ?_1  :  T
553     ncut T;   ⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼
554                                Γ ⊢ (?_2 ?_1)  :  G                    
555
556
557                                 Γ ⊢ ?  :  ∀x.P(x)
558     ngeneralize in match t; ⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼
559                                 Γ ⊢ (? t)  :  P(t)
560                                 
561 D*)
562
563
564 (*D
565
566 [1]: http://upsilon.cc/~zack/research/publications/notation.pdf 
567
568 D*)
569 *)