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 *)