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