Hello Makarius, Thank you for your feedback.
On 11/20/2012 11:33 AM, Makarius wrote: > On Mon, 29 Oct 2012, Alexey Solovyev wrote: > >> I would like to present a new tool for formal verification of nonlinear >> inequalities in HOL Light. The tool can be downloaded at: >> http://code.google.com/p/flyspeck/downloads/list > > It is always interesting for me to see projects that try to redefine > the old ways of doing interactive proof -- I did this myself with > Isabelle/Isar in 1998/1999. > > I've looked a bit through the manual > http://flyspeck.googlecode.com/files/HOL-SSReflect%20v1.1.pdf and here > is some random feedback on it: > > * Concerning specifications it looks a lot like an imitation of Coq > "vernacular". How do hardcore HOL users like the style? After working a little bit with SSReflect/Coq, I became quite attached to its style. That was the primary reason for creating my version of SSReflect in HOL Light: I wanted to be able to create SSReflect/Coq-style proofs for the Flyspeck project. > > BTW, the use of capital keywords like Definition or Lemma was > recently > considered a historical mistake on coq-club, on the "Coq and RSI" > thread, about pain inflicted on users by Coq conventions and Emacs > keymaps coming together. > This is a good point. I'll include lowercase keywords in a new version of SSReflect/HOL Light. > * How much SSReflect is there in SSReflect/HOL Light actually? The > "small-scale reflection" aspect of the Coq version appears to be > mainly an approach to make Coq propositions work more like HOL > propositions, but you have that already. In your section about views > it sounds like there is little or nothing of it in your version of > SSReflect. So is it just a marketing aspect to retain the name? > (Even for Coq it might be just a branding issue to keep this obscure > name that everybody knows already.) > It is exactly as you are saying: SSReflect is just a brand name which I don't want to change. There is no real reflection in SSReflect/HOL Light proofs. All features of SSReflect/HOL Light are mostly syntactic plus some new tactics. > * Page 15: > move: {1}x a transforms the goal into !x1 a. a + x1 = x + 3, where > x1 is an automatically generated name. > > How does that compare to SSReflect by Gonthier? It is one of the > very > few points where SSReflect and Isar agree, to have generated names > never intrude the proof text implicitly. Does that actually > happen above for HOL Light, or is it just the text confusing me? > I'm not sure how this is done in SSReflect/Coq since I rarely used this construction in my SSReflect/Coq proofs (in SSReflect/HOL Light, I'm not using it often either). The SSReflect manual shows a similar example with a similar outcome (see http://hal.inria.fr/inria-00258384, pages 27-28). I agree that this is not a good way to interfere with the proof. Usually, this construction is immediately followed by the introduction tactical => which replaces auto-generated names with user-provided names. > * wlog: Can you give some examples? Despite some talks and papers > about > "wlog" reasoning by John Harrison, I've never quite understood how > this would work in Isabelle/Isar. Maybe I can learn something new. > First of all, I would like to say that this tactic is rarely used (or, maybe, I avoid it too much). Here is a lemma from SSReflect/Coq library ssrnat.v which uses this tactic: Lemma leq_maxr m n1 n2 : (m <= maxn n1 n2) = (m <= n1) || (m <= n2). Proof. wlog le_n21: n1 n2 / n2 <= n1. by case/orP: (leq_total n2 n1) => le_n12; last rewrite maxnC orbC; auto. rewrite /maxn ltnNge le_n21 /=; case: leqP => // lt_m_n1. by rewrite leqNgt (leq_trans _ lt_m_n1). Qed. The initial goal is ?- (m <= maxn n1 n2) = (m <= n1) || (m <= n2) (denote this goal by (G m n1 n2).) The tactic wlog le_n21: n1 n2 / n2 <= n1 creates two subgoals: 1. forall n1 n2, n2 <= n1 -> G m n1 n2 ?- G m n1 n2 2. n2 <= n1 ?- G m n1 n2 The first goal includes a new assumption where n1 and n2 are generalized. This goal is easily solved by considering two cases: n2 <= n1 or n1 <= n2. The first case is exactly the same as the assumption. In the second case, the goal is modified to (G m n2 n1) and then everything follows from the assumption. > * 'by' vs. 'done': Is this copied from Isar, or did Gonthier copy it > from Isar for SSReflect? BTW, in Isabelle/Isar 'by' does a bit more: > it solves the remaining situation "by assumption", and then > insists in > being finished. The proof structure is already known, so one can > afford implicit "trivial steps" at the end of a sub-proof. > I don't know the actual story, but I copied it directly from SSReflect/Coq. > * 'have' as subgoal: I reckon it is simular to subgoal_tac in Isabelle > or its counterpart in HOL. In Isar, I made this quite different: > having a first-class notion of proof context, 'have' is just a fresh > local goal within it, and its result a theorem with certain > assumptions, which is then re-used in the enclosing proof. This gives > you more structure and scalability than just goal-modifications in > the > old style. > 'have' is implemented via SUBGOAL_THEN in HOL Light. Your implementation of 'have' in Isar sounds interesting, but could you give examples when "local theorems" are better than just subgoals? > > Makarius Best, Alexey ------------------------------------------------------------------------------ Monitor your physical, virtual and cloud infrastructure from a single web console. Get in-depth insight into apps, servers, databases, vmware, SAP, cloud infrastructure, etc. Download 30-day Free Trial. Pricing starts from $795 for 25 servers or applications! http://p.sf.net/sfu/zoho_dev2dev_nov _______________________________________________ hol-info mailing list [email protected] https://lists.sourceforge.net/lists/listinfo/hol-info
