[Date Prev][Date Next] [Chronological] [Thread] [Top]

Re: [mizar] Private DB

Hi Freek,

On Tue, 26 Sep 2006, Freek Wiedijk wrote:


Hi Adam,

Thanks for the very nice explanation of what happens to MML
when you sort things according to mml.lar!


Apparently, there are more than a hundred files that pose
problems, but it seems that in most cases they can be fixed
rather easily by using a different redefinition for expansion.


Sorry, but I don't understand this.  Can you give an example?
What I ment was that one may try to resolve some conflicts by 'qualifying' expressions to proper redefinitions. E.g. the first article (in mml.lar processing order) with errors is PARTFUN1, where the fix could look like that: 

:: definition let X,Y,V,Z;
::   let f be PartFunc of X,Y; let g be PartFunc of V,Z;
::  redefine func g*f -> PartFunc of X,Z;
::   coherence
::    proof
::     dom f c= X & dom(g*f) c= dom f & rng g c= Z & rng(g*f) c= rng g
::       by Lm3,RELAT_1:44,45;
:: ::>    *4,4
::     then dom(g*f) c= X & rng(g*f) c= Z by XBOOLE_1:1;
::     hence g*f is PartFunc of X,Z by Lm3;
:: ::>       *51
::    end;
:: end;

definition let X,Y,V,Z;
  let f be PartFunc of X,Y; let g be PartFunc of V,Z;
 redefine func g*f -> PartFunc of X,Z;
  coherence
   proof
    dom f c= X & dom(g*f) c= dom g & rng g c= Z & rng(g*f) c= rng f
      by Lm3,RELAT_1:44,45;
    then dom(f*g) c= X & rng(f*g) c= Z by XBOOLE_1:1;
    hence f*g is PartFunc of X,Z by Lm3;
   end;
end;
Here, the situation is a bit more cryptic (compare 'redefine func g*f' and 'hence f*g') because of the fact that redefinitins are applied to original constructors (here Relation) while the statement uses the Function notation!
Another thing is that I should have rather put the results of verifying the database with sorted notations _and_ at the same time building the new database, so that the exported articles reflect these changes - what I showed previously was just simple verifier run over all articles without taking care of any resulting consequences.
Still, many errors seem to be the result of NAT_1/INT_1 order change. I guess in these cases, the order should be reversed by 'encapsulating' a prototype of Integers in a way similar to Reals. Otherwise, when we want to use attributes like 'natural' and 'integer' as much as possible, the functors like 'GCD' are very much conflict-prone. 

Best,

Adam