*To*: "isabelle-users at cl.cam.ac.uk" <isabelle-users at cl.cam.ac.uk>, HOL-info list <hol-info at lists.sourceforge.net>, metamath at googlegroups.com*Subject*: [isabelle] Concept of a small logical kernel, preserving logical dependencies, axiomatic type classes vs. type abstraction, Isabelle documentation â Re: Verify the legitimacy of a proof?*From*: Ken Kubota <mail at kenkubota.de>*Date*: Sun, 9 Jul 2017 18:04:22 +0200*Cc*: "Prof. Lawrence C. Paulson" <lp15 at cam.ac.uk>, "Dr. Markus Wenzel" <makarius at sketis.net>*In-reply-to*: <BD9ECBCD-B093-4F5F-91E1-8BF6714337B3@cam.ac.uk>*References*: <CADYF24fBE5-wFje-T9-z2c9Um4ZGf1y+ukaSiDi3EPa9uRBEaw@mail.gmail.com> <5b1c5907-c172-0e3d-6163-c70e0bc884c7@sketis.net> <CADYF24c9L7mdmpNspoSEinHGU-V-_w1axhYvsHqO4_cMnRhxnw@mail.gmail.com> <BD9ECBCD-B093-4F5F-91E1-8BF6714337B3@cam.ac.uk>

In this discussion on the Isabelle mailing list, I am missing the question of the correctness of the small logical kernel that should guarantee the correctness of the whole system. Currently, the arguments presented so far seem to open up a false alternative between logically correct (reliable) but small theorem provers (e.g., HOL Zero), and large and practical but less reliable provers (e.g., Isabelle/HOL): > The other big provers (e.g. Coq) are similar in this respect. [â] > HOL-Zero is a notable exception in targeting a market of potentially > malicious (ab-)users, but it is not a "big prover". According to this idea, any reliable prover/checker must be small, and any practical (and hence, large) prover isn't reliable. But the concept of a small logical kernel that guarantees the correctness of the whole system states exactly the opposite, i.e., no matter how large and practical the software is, it remains reliable. This concept is given up in arguments like > We do not have to work on the basis that "X has been proved, therefore X is true", but rather "We have been given a proof of X; Is it credible?" which even seems to rhetorically downplay a desirable must-have (correctness) as an annoying impediment to get rid of ("do not have to work on the basis"). In particular, transferring the responsibility for providing reliability (correctness) from (verifying) the small logical kernel to either examining specific parts of the formalized proof or estimating the credibility of the supplying person is questionable, as even the best mathematicians from time to time fail at complex proofs: > Then we can look at any part of this proof where we have doubts. [â] > The effort we choose to invest in this would depend on how important X is and how much we distrust the person who supplied the proof. I do not see any alternative to providing a correct small logical kernel. Preserving logical dependencies is part of (has to be guaranteed by) the logical kernel. For this reason, I consider the following phenomenon as highly problematic (and even as a failure of the logical kernel): >> found this originally, but you can hide the âtaintâ of a theorem by >> going through a type class instantiation: If a conditional can be stripped off so easily, it might be possible to obtain from different conditionals two contradictory theorems, and hence, an inconsistency. In a related discussion about this question on the Metamath mailing list I argued in favor of introducing all non-logical axioms as conditionals (hence, Q0 and R0 have only five axioms) in order to make the dependency explicit: > Third, the dependency is made explicit. If "the software tracks > axiom usage, as Metamath does", the task of tracking dependencies > is moved from the logic to the software, which I already, in another > context, criticized at KunÄar/Popescu's approach (which is > nevertheless legitimate as an auxiliary approach). > [â] Andrews' exercise X5308 [â] stated and > formalized on pp. 151 ff. of > http://www.owlofminerva.net/files/formulae.pdf > is taken as an example where the dependency of the theorem > is make explicit, assuming the form > AC => theorem > since the (non-logical) Axiom of Choice was > introduced as a conditional, not as an axiom. https://groups.google.com/d/msg/metamath/WwKPkCGoZkg/VSAVebXPCQAJ Norman Megill presented a similar example: > It is certainly possible to prefix every theorem with "ZFC ->" https://groups.google.com/d/msg/metamath/WwKPkCGoZkg/nvmXHUffCQAJ I agree with Norman Megill that in certain practical contexts constantly displaying the same conditional prefix may be redundant, but this is a question of the user interface (which could, for example, replace the default prefix â e.g., "ZFC ->" â by a star "*"), but not a matter relevant for the logical kernel, where this dependency should be made explicit. As mentioned earlier, the Isabelle concept of axiomatic type classes as described and discussed in https://www4.in.tum.de/~wenzelm/papers/axclass-TPHOLs97.pdf and introduced in > Prover-powered type classes were introduced by Nipkow and Snelting [28] in Isabelle/HOL > and by Sozeau and Oury [32] in Coqâthey additionally feature verifiability > of the type-class conditions upon instantiation: a type T is accepted as a member > of the semigroup class only if associativity can be proved for its + operation. http://www21.in.tum.de/~kuncar/documents/kuncar-popescu-itp2015.pdf (p. 3) is considered as a preliminary solution by me, since the same fact can be expressed very naturally with the means of type abstraction (as suggested by Mike Gordon, see first quote at http://owlofminerva.net/kubota/software-implementation-of-the-mathematical-logic-r0-available-for-download/ ) and as argued and demonstrated at pp. 12, 362, 420 of http://www.owlofminerva.net/files/formulae.pdf Here, the fact that (o,XOR) is a group, formalized as Grp o XOR (p. 420) can be stated only after proving the three group axioms for (o,XOR), and only after that, a general proof on groups (Uniqueness of the Group Identity Element, pp. 362 ff.) can be instantiated (transferred) to the specific XOR group without having to carry out the proof again (Uniqueness of the Group Identity Element of the XOR Group, pp. 420 ff.). Coq is not suited for a comparison. It is very expressive (e.g., it has dependent types), but there is profound criticism raised by Freek Wiedijk and John Harrison (and Josef Urban), see section 3 of http://doi.org/10.4444/100.111 and for an example the rule on top of p. 54 at http://www.cl.cam.ac.uk/~jrh13/papers/joerg.pdf which is very far from a natural expression of formal logic and mathematics. The Isabelle documentation is discussed quite often. > Extensive documentation is available. http://www.cl.cam.ac.uk/~lp15/papers/Formath/Goedel-ar.pdf (p. 3) > The problem remains open: How can true expertise about how Isabelle > really works be reconstructed? We've seen a slow and steady decline in > the past 10 years, and myself writing hundreds of pages of documentation > helped only very little. It is always claimed that the Isabelle documentation is ample, but unfortunately, it is not logically structured, which makes the extent of the documentation rather a disadvantage than an advantage. For comparison, the HOL/HOL4 documentation provides a precise and quick introduction, which allowed me to fully comprehend the logic, install the software and carry out proofs very quickly. It has, as one would expect, a separate logic part (Part III: The HOL Logic [Gordon and Melham, 1993, pp. 191â232]), available online at http://freefr.dl.sourceforge.net/project/hol/hol/kananaskis-11/kananaskis-11-logic.pdf and a very good guidebook which allows one to inspect the details of the system: https://hol-theorem-prover.org/guidebook/ I already made suggestions for improvements earlier: > Although of course Isabelle/HOL is a very good piece of software, this precision is currently missing in my opinion. > The extension from classical HOL to Gordon's HOL can be found in section 11.7 (p. 261), as well as the > (single) extension from Gordon's HOL to Isabelle/HOL ("Isabelle/HOL goes beyond Gordon-style HOL > by admitting overloaded constant definitions") within a document of 13 chapters and 330 pages, > which makes it practically impossible to identify and locate important features and extensions of the core logic > within a reasonable amount of time: > http://www.cl.cam.ac.uk/research/hvg/Isabelle/dist/Isabelle2016/doc/isar-ref.pdf https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2016-October/msg00050.html Essential information on the logic is hidden somewhere between many technical details, and at the first glance I can't even see a reason for why the extension of the HOL logic is described in the Isar reference, and not in the Isabelle/HOL reference. With the HOL/HOL4 documentation, I was able to understand the logic and study the details of the proof technology within 24 hours (see example files attached), but with the Isabelle/HOL documentation, even after many months the details are obscure. Moreover, the concept of a small logical kernel should be reflected in the documentation by a separate logic part, as in the HOL/HOL4 documentation. The Isabelle/HOL documentation currently doesn't conform to this clear standard established by the original HOL system. The emails quoted are attached below. The full discussion is available at https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2017-July/date.html ____________________________________________________ Ken Kubota http://doi.org/10.4444/100 > Am 08.07.2017 um 20:59 schrieb Lawrence Paulson <lp15 at cam.ac.uk>: > > To protect against malicious intentions would turn Isabelle into a form of security software. But the guarantees we get from the latter are quite different from what we get from a formal proof. Ultimately security claims depend upon trusting a lot of complicated mechanisms, such as certificate authorities and cryptosystems. We are not a lot better off than when a model checker comes back with nothing. > > However, we work with formal proofs, which can be examined, even interactively. We do not have to work on the basis that "X has been proved, therefore X is true", but rather "We have been given a proof of X; Is it credible?" Then we can look at any part of this proof where we have doubts. A devious user has many ways to try to fool us, but it's not so easy if he has to supply the full source code and we insist on legibility throughout. The effort we choose to invest in this would depend on how important X is and how much we distrust the person who supplied the proof. > > Larry Paulson > >> On 8 Jul 2017, at 18:12, scott constable <sdconsta at syr.edu> wrote: >> >> Isabelle does not protect against malicious intentions. It would require >> a quite different system to do that, one that you won't like to use. >> >> The other big provers (e.g. Coq) are similar in this respect. > Am 08.07.2017 um 12:46 schrieb Makarius <makarius at sketis.net>: > > On 07/07/17 18:37, scott constable wrote: >> >> possibly written by other persons with malicious intentions. > > Isabelle does not protect against malicious intentions. It would require > a quite different system to do that, one that you won't like to use. > > The other big provers (e.g. Coq) are similar in this respect. > > HOL-Zero is a notable exception in targeting a market of potentially > malicious (ab-)users, but it is not a "big prover". > > > Makarius > On 08/07/17 13:01, Manuel Eberl wrote: >> Unfortunately, it is very easy to circumvent this. I don't recall who >> found this originally, but you can hide the âtaintâ of a theorem by >> going through a type class instantiation: > > "Found this originally" sounds very funny to me. > > Of course, the problem of oracles vs. type classes instantiations is as > old as oracles and type class instantiations in Isabelle. It is rather > well-known for insiders. > > > So we are back to the new meta-problem from recent years: even power > users don't know anymore what Isabelle is and what it does, and > especially what it does not. > > > Makarius > Am 08.07.2017 um 16:03 schrieb Makarius <makarius at sketis.net>: > > On 08/07/17 15:33, Tobias Nipkow wrote: > > [â] > >> It is usually due to a fanciful interpretation of the documentation. The >> latter says that "The system always records oracle invocations within >> derivations of theorems by a unique tag." but does not claim that these >> tags are also always inherited in the way one is all too likely to >> assume. > > The problem remains open: How can true expertise about how Isabelle > really works be reconstructed? We've seen a slow and steady decline in > the past 10 years, and myself writing hundreds of pages of documentation > helped only very little. > > > Makarius ____________________________________________________ Makefile ____________________________________________________ SRCS = types.sml OBJS = TGTS = $(SRCS:.sml=.out) CC = $(HOME)/HOL/bin/hol .PHONY: all clean view full edit all: $(TGTS) clean: rm -f $(OBJS) $(TGTS) view: all open -t $(TGTS) full: clean all view edit: open -a xcode Makefile $(SRCS) %.out: %.sml $(CC) < $< > $@ ____________________________________________________ types.sml ____________________________________________________ (* TO DO List HOL terms vs. types (different syntactical category) LCF: rules of inference (type thm) terms as trees? * type operators: fun, pair, list * pairs * 3 extensions *) (* prove that a figure - a number from 0 to 9 - exists *) app load ["Q"]; open arithmeticTheory; val figure_def = Define `figure a = a < 10`; g `?x. figure x`; e (RW_TAC arith_ss [figure_def]); val FIGURE_EXISTS = top_thm(); drop(); (* create type "figure" (tyfi) and an object (a variable) of that type *) val figure_axiom = new_type_definition ("tyfi", FIGURE_EXISTS); (* show new type *) types "-"; val figure_object = ``a:tyfi = a``; (* show type of object *) set_trace "types" 1; figure_object; (* show type of object *) set_trace "types" 2; figure_object; set_trace "types" 0; (* But figure 3 doesn't have type "tyfi", which would be desirable, and the following fails: ``3:tyfi``; The reason is, that in HOL terms can only have a single type. (Types are disjoint.) *); type_of ``3``; (* show universal quantifier *) dest_comb ``!x.x``; (* show type of universal quantifier *) type_of ``$!``; (* find theory of universal quantifier *) dest_thy_const ``$!``; (* show some information about the theory "bool" *) thy "bool"; axioms "bool"; definitions "bool"; theorems "bool"; constants "bool"; types "bool"; ancestry "bool"; (* show some information about the theory "min" *) types "min"; constants "min"; (* interactively we could do: help "arithmeticTheory"; *) (* find definition in database *) DB.find "FORALL_DEF"; DB.match ["arithmetic"] ``SUC n * x``; (* type definition example from kananaskis-10-reference.pdf, p. 630 *) app load ["PairedLambda", "Q"]; open PairedLambda pairTheory; val tyax = new_type_definition ("three", Q.prove(`?p. (\(x,y). ~(x /\ y)) p`, Q.EXISTS_TAC `(F,F)` THEN GEN_BETA_TAC THEN REWRITE_TAC [])); open arithmeticTheory; val divides_def = Define `divides a b = ?x. b = a * x`; set_fixity "divides" (Infix(NONASSOC, 450)); val prime_def = Define `prime p = ~(p=1) /\ !x. x divides p ==> (x=1) \/ (x=p)`; g `!x. x divides 0`; e (RW_TAC arith_ss [divides_def]); e (EXISTS_TAC ``0``); e (RW_TAC arith_ss []); restart(); e (RW_TAC arith_ss [divides_def] THEN EXISTS_TAC ``0`` THEN RW_TAC arith_ss []); ____________________________________________________

**References**:**[isabelle] Verify the legitimacy of a proof?***From:*scott constable

**Re: [isabelle] Verify the legitimacy of a proof?***From:*Makarius

**Re: [isabelle] Verify the legitimacy of a proof?***From:*scott constable

**Re: [isabelle] Verify the legitimacy of a proof?***From:*Lawrence Paulson

- Previous by Date: Re: [isabelle] primrec of datatype containing fset
- Next by Date: Re: [isabelle] Extended non-negative reals summing to infinity
- Previous by Thread: Re: [isabelle] Verify the legitimacy of a proof?
- Next by Thread: Re: [isabelle] Verify the legitimacy of a proof?
- Cl-isabelle-users July 2017 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list