From: Enrico Tassi Date: Fri, 25 Sep 2009 15:39:03 +0000 (+0000) Subject: ... X-Git-Tag: make_still_working~3434 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=a436718fd9b50340f5535cef223399c5813d9869;p=helm.git ... --- diff --git a/helm/software/matita/nlibrary/topology/igft.ma b/helm/software/matita/nlibrary/topology/igft.ma index 6b2b73f88..b372d94a3 100644 --- a/helm/software/matita/nlibrary/topology/igft.ma +++ b/helm/software/matita/nlibrary/topology/igft.ma @@ -322,6 +322,9 @@ interpretation "covers set temp" 'covers C U = (cover_set ?? C U). (*D +The cover relation +------------------ + We can now define the cover relation using the `◃` notation for the premise of infinity. @@ -409,6 +412,10 @@ subproof and `##]` ends the branching. D*) (*D + +The fish relation +----------------- + The definition of fish works exactly the same way as for cover, except that it is defined as a coinductive proposition. D*) @@ -433,6 +440,9 @@ interpretation "fish" 'fish a U = (fish ? U a). (*D +Introction rule for fish +------------------------ + Matita is able to generate elimination rules for inductive types, but not introduction rules for the coinductive case. @@ -540,12 +550,33 @@ in the context. Instead of explicitly mention them, we use the D*) +(*D + +Subset of covered/fished points +------------------------------- + +We now have to define the subset of `S` of points covered by `U`. +We also define a prefix notation for it. Remember that the precedence +of the prefix form of a symbol has to be lower than the precedence +of its infix form. + +*) + ndefinition coverage : ∀A:Ax.∀U:Ω^A.Ω^A ≝ λA,U.{ a | a ◃ U }. notation "◃U" non associative with precedence 55 for @{ 'coverage $U }. interpretation "coverage cover" 'coverage U = (coverage ? U). +(*D + +Here we define the equation characterizing the cover relation. +In the igft.ma file we proved that `◃U` is the minimum solution for +such equation, the interested reader should be able to reply the proof +with Matita. + +*) + ndefinition cover_equation : ∀A:Ax.∀U,X:Ω^A.CProp[0] ≝ λA,U,X. ∀a.a ∈ X ↔ (a ∈ U ∨ ∃i:𝐈 a.∀y.y ∈ 𝐂 a i → y ∈ X). @@ -569,6 +600,14 @@ ntheorem coverage_min_cover_equation : ##] nqed. +(*D + +We similarly define the subset of point fished by `F`, the +equation characterizing `⋉F` and prove that fish is +the biggest solution for such equation. + +*) + notation "⋉F" non associative with precedence 55 for @{ 'fished $F }. @@ -592,8 +631,15 @@ ntheorem fised_max_fish_equation : ∀A,F,G. fish_equation A F G → G ⊆ ⋉F. #b; ncases (H b); #H1; #_; #bG; ncases (H1 bG); #E1; #E2; nassumption; nqed. +(*D + +Part 2, the new set of axioms +----------------------------- + +*) + nrecord nAx : Type[2] ≝ { - nS:> setoid; (*Type[0];*) + nS:> setoid; nI: nS → Type[0]; nD: ∀a:nS. nI a → Type[0]; nd: ∀a:nS. ∀i:nI a. nD a i → nS