From: Enrico Tassi Date: Sun, 13 Sep 2009 21:02:15 +0000 (+0000) Subject: a nice bug in meta handling is not visible... brr... X-Git-Tag: make_still_working~3470 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=1434d54f86fcce0296bcda49086ce7f7040aa53d;p=helm.git a nice bug in meta handling is not visible... brr... --- diff --git a/helm/software/matita/nlibrary/topology/igft.ma b/helm/software/matita/nlibrary/topology/igft.ma index 9bff8502f..b3f2c2d6b 100644 --- a/helm/software/matita/nlibrary/topology/igft.ma +++ b/helm/software/matita/nlibrary/topology/igft.ma @@ -6,6 +6,12 @@ nrecord axiom_set : Type[1] ≝ { C: ∀a:S. I a → Ω ^ S }. +notation "𝐈 term 90 a" non associative with precedence 70 for @{ 'I $a }. +notation "𝐂 term 90 a term 90 i" non associative with precedence 70 for @{ 'C $a $i }. + +interpretation "I" 'I a = (I ? a). +interpretation "C" 'C a i = (C ? a i). + ndefinition cover_set ≝ λc:∀A:axiom_set.Ω^A → A → CProp[0].λA,C,U. ∀y.y ∈ C → c A U y. @@ -17,7 +23,7 @@ interpretation "covers set temp" 'covers C U = (cover_set ?? C U). ninductive cover (A : axiom_set) (U : Ω^A) : A → CProp[0] ≝ | creflexivity : ∀a:A. a ∈ U → cover ? U a -| cinfinity : ∀a:A. ∀i:I ? a. (C ? a i ◃ U) → cover ? U a. +| cinfinity : ∀a:A. ∀i:?. ((C ? a i) ◃ U) → cover ? U a. napply cover; nqed. @@ -35,7 +41,7 @@ for @{ 'fish $a $b }. interpretation "fish set temp" 'fish A U = (fish_set ?? U A). ncoinductive fish (A : axiom_set) (F : Ω^A) : A → CProp[0] ≝ -| cfish : ∀a. a ∈ F → (∀i:I ? a.C A a i ⋉ F) → fish A F a. +| cfish : ∀a. a ∈ F → (∀i:𝐈 a.C A a i ⋉ F) → fish A F a. napply fish; nqed. @@ -44,7 +50,7 @@ interpretation "fish" 'fish a U = (fish ? U a). nlet corec fish_rec (A:axiom_set) (U: Ω^A) (P: Ω^A) (H1: P ⊆ U) - (H2: ∀a:A. a ∈ P → ∀j: I ? a. C ? a j ≬ P): + (H2: ∀a:A. a ∈ P → ∀j: 𝐈 a. C ? a j ≬ P): ∀a:A. ∀p: a ∈ P. a ⋉ U ≝ ?. #a; #p; napply cfish; ##[ napply H1; napply p; @@ -61,7 +67,7 @@ ndefinition coverage : ∀A:axiom_set.∀U:Ω^A.Ω^A ≝ λA,U.{ a | a ◃ U }. interpretation "coverage cover" 'coverage U = (coverage ? U). ndefinition cover_equation : ∀A:axiom_set.∀U,X:Ω^A.CProp[0] ≝ λA,U,X. - ∀a.a ∈ X ↔ (a ∈ U ∨ ∃i:I ? a.∀y.y ∈ C ? a i → y ∈ X). + ∀a.a ∈ X ↔ (a ∈ U ∨ ∃i:𝐈 a.∀y.y ∈ 𝐂 a i → y ∈ X). ntheorem coverage_cover_equation : ∀A,U. cover_equation A U (◃U). #A; #U; #a; @; #H; @@ -90,7 +96,7 @@ ndefinition fished : ∀A:axiom_set.∀F:Ω^A.Ω^A ≝ λA,F.{ a | a ⋉ F }. interpretation "fished fish" 'fished F = (fished ? F). ndefinition fish_equation : ∀A:axiom_set.∀F,X:Ω^A.CProp[0] ≝ λA,F,X. - ∀a. a ∈ X ↔ a ∈ F ∧ ∀i:I ? a.∃y.y ∈ C ? a i ∧ y ∈ X. + ∀a. a ∈ X ↔ a ∈ F ∧ ∀i:𝐈 a.∃y.y ∈ 𝐂 a i ∧ y ∈ X. ntheorem fised_fish_equation : ∀A,F. fish_equation A F (⋉F). #A; #F; #a; @; (* bug, fare case sotto diverso da farlo sopra *) #H; ncases H; @@ -100,84 +106,8 @@ ntheorem fised_fish_equation : ∀A,F. fish_equation A F (⋉F). ##] nqed. -ntheorem fised_min_fish_equation : ∀A,F,G. fish_equation A F G → G ⊆ ⋉F. +ntheorem fised_max_fish_equation : ∀A,F,G. fish_equation A F G → G ⊆ ⋉F. #A; #F; #G; #H; #a; #aG; napply (fish_rec … aG); #b; ncases (H b); #H1; #_; #bG; ncases (H1 bG); #E1; #E2; nassumption; nqed. -STOP - -(* -alias symbol "covers" (instance 0) = "covers". -alias symbol "covers" (instance 2) = "covers". -alias symbol "covers" (instance 1) = "covers set". -ntheorem covers_elim2: - ∀A: axiom_set. ∀U:Ω^A.∀P: A → CProp[0]. - (∀a:A. a ∈ U → P a) → - (∀a:A.∀V:Ω^A. a ◃ V → V ◃ U → (∀y. y ∈ V → P y) → P a) → - ∀a:A. a ◃ U → P a. -#A; #U; #P; #H1; #H2; #a; #aU; nelim aU; -##[ #b; #H; napply H1; napply H; -##| #b; #i; #CaiU; #H; napply H2; - ##[ napply (C ? b i); - ##| napply cinfinity; ##[ napply i ] nwhd; #y; #H3; napply creflexivity; ##] - nassumption; -##] -nqed. -*) - -alias symbol "fish" (instance 1) = "fish set". -alias symbol "covers" = "covers". -ntheorem compatibility: ∀A:axiom_set.∀a:A.∀U,V. a ⋉ V → a ◃ U → U ⋉ V. -#A; #a; #U; #V; #aV; #aU; ngeneralize in match aV; (* clear aV *) -nelim aU; -##[ #b; #bU; #bV; @; ##[ napply b] @; nassumption; -##| #b; #i; #CaiU; #H; #bV; ncases bV in i CaiU H; - #c; #cV; #CciV; #i; #CciU; #H; ncases (CciV i); #x; *; #xCci; #xV; - napply H; nassumption; -##] -nqed. - - - - -STOP - -definition leq ≝ λA:axiom_set.λa,b:A. a ◃ {y|b=y}. - -interpretation "covered by one" 'leq a b = (leq ? a b). - -theorem leq_refl: ∀A:axiom_set.∀a:A. a ≤ a. - intros; - apply refl; - normalize; - reflexivity. -qed. - -theorem leq_trans: ∀A:axiom_set.∀a,b,c:A. a ≤ b → b ≤ c → a ≤ c. - intros; - unfold in H H1 ⊢ %; - apply (transitivity ???? H); - constructor 1; - intros; - normalize in H2; - rewrite < H2; - assumption. -qed. - -definition uparrow ≝ λA:axiom_set.λa:A.mk_powerset ? (λb:A. a ≤ b). - -interpretation "uparrow" 'uparrow a = (uparrow ? a). - -definition downarrow ≝ λA:axiom_set.λU:Ω \sup A.mk_powerset ? (λa:A. (↑a) ≬ U). - -interpretation "downarrow" 'downarrow a = (downarrow ? a). - -definition fintersects ≝ λA:axiom_set.λU,V:Ω \sup A.↓U ∩ ↓V. - -interpretation "fintersects" 'fintersects U V = (fintersects ? U V). - -record convergent_generated_topology : Type ≝ - { AA:> axiom_set; - convergence: ∀a:AA.∀U,V:Ω \sup AA. a ◃ U → a ◃ V → a ◃ (U ↓ V) - }.