helm/software/matita/nlibrary/topology/igft-setoid.ma

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