Delivery-Date: 
Sender: info-hol-request@ted.cs.uidaho.edu
Errors-To: info-hol-request@ted.cs.uidaho.edu
Precedence: bulk
To: info-hol@ted.cs.uidaho.edu
Subject: Re: Parnas: "some theorems we should prove"
In-Reply-To: Your message of "Thu, 17 Jun 93 18:05:12 EDT." <9306172205.AA03411@circe.mitre.org>
Date: Fri, 18 Jun 93 01:02:14 +0100
From: John Harrison <John.Harrison@cl.cam.ac.uk>
Message-Id: <"swan.cl.cam.:266830:930618000222"@cl.cam.ac.uk>


Well, just for the sake of it, I tried doing the "Parnas theorems" in HOL.

Generally the semantics of partial functions which is implicit in the Parnas
paper do not mesh with HOL's mathematical infrastructure (Josh is right that
IMPS is a much better fit).

Insofar as the theorems can be meaningfully translated into HOL, they are
pretty trivial to prove. However I gather David Parnas is interested in
complete automation. It is not hard to program HOL to prove theorems of some
"genre" without user intervention, so how far the process could be automated
depends on the degree of regularity of the whole batch of theorems.

Please note that the following represents only about an hour's work, including
reading the paper, and I may well have failed to grasp the point of some of the
theorems.

Proof script follows.

John.


new_theory `PARNAS`;;

load_library `reals`;;

set_interface_map real_interface_map;;

load_library `pred_sets`;;

load_library `reduce`;;

%
  The first two theorems are trivial properties of real arithmetic. The HOL
  arithmetic decision procedure has not yet been extended to the reals (it
  only works for the naturals) so I have to do a bit of hands-on proof.

  A merit of HOL's programmability is that one can always fall back on this
  sort of approach, even though it is often rather tedious.

  The ampersand is the injection N -> R (there is no transparent subtyping).
%

let THM2 = prove_thm(`THM2`,
  "!x. x < &0 \/ (x = &0) \/ x > &0",
  GEN_TAC THEN REWRITE_TAC[real_gt] THEN
  STRIP_ASSUME_TAC(SPECL ["&0"; "x:real"] REAL_LT_TOTAL) THEN
  ASM_REWRITE_TAC[]);;

let THM3 = prove_thm(`THM3`,
  "!x. ~((x < &0 /\ (x = &0)) \/
         (x < &0 /\ x > &0) \/
         (x > &0 /\ (x = &0)))",
  GEN_TAC THEN REWRITE_TAC[real_gt] THEN
  ASM_CASES_TAC "x = &0" THEN
  ASM_REWRITE_TAC[REAL_LT_REFL; REAL_LT_ANTISYM]);;


%
  The next two theorems are rather hard to translate meaningfully into HOL
  because its basic functions are all total. (One could of course define one's
  own theory of functions-as-sets.) The general consensus is that
  the simplicity of this approach compensates for its incompatibility with
  mathematical practice. The only system I know which handles partial functions
  properly is IMPS; some systems use total functions defined on a subtype,
  but this is not a complete answer. I define the domain of |sqrt| to be
  the set of reals where its behaviour is as expected.
%

let THM4 = prove_thm(`THM4`,
  "x < &0 ==> --x IN {u | sqrt(u) pow 2 = u}",
  CONV_TAC(ONCE_DEPTH_CONV SET_SPEC_CONV) THEN
  REWRITE_TAC[SQRT_POW2; GSYM REAL_NEG_GT0; REAL_LT_IMP_LE]);;

let THM5 = prove_thm(`THM5`,
  "x > &0 ==> x IN {u | sqrt(u) pow 2 = u}",
  CONV_TAC(ONCE_DEPTH_CONV SET_SPEC_CONV) THEN
  REWRITE_TAC[real_gt; SQRT_POW2; REAL_LT_IMP_LE]);;

%
  Again I use total functions; as stated one of the quantifiers is
  restricted to 1..N anyway, but I need to restrict the other in THM8.
  THM7 is actually true without the restriction. The distinction between
  inequality and not-equality likewise has no analogue in HOL.
  I've assumed the array is of reals; that makes little difference to
  the proof.

  Rather than actually define "NONEMPTY" I just say "~(x = {})"; this
  could easily be changed.
%

set_interface_map [];;

hide_constant `B`;;

let THM7 = prove_thm(`THM6`,
  "(?i. B(i):real = x) \/ (!i. 1 <= i /\ i <= N ==> ~(B(i) = x))",
  ASM_CASES_TAC "?i:num. B(i):real = x" THEN ASM_REWRITE_TAC[] THEN
  RULE_ASSUM_TAC(CONV_RULE NOT_EXISTS_CONV) THEN
  ASM_REWRITE_TAC[]);;

let THM8 = prove_thm(`THM8`,
  "~((?i. 1 <= i /\ i <= N /\ (B(i):real = x)) /\
     (!i. 1 <= i /\ i <= N ==> ~(B(i) = x)))",
  REWRITE_TAC[DE_MORGAN_THM] THEN
  CONV_TAC(ONCE_DEPTH_CONV NOT_FORALL_CONV) THEN
  ONCE_REWRITE_TAC[DISJ_SYM] THEN
  REWRITE_TAC[NOT_IMP; CONJ_ASSOC; EXCLUDED_MIDDLE]);;

let THM11 = prove_thm(`THM11`,
  "(?i. (B:num->real)(i) = x) ==> ~({j' | B(j') = x} = {})",
  STRIP_TAC THEN ONCE_REWRITE_TAC[EXTENSION] THEN
  CONV_TAC(ONCE_DEPTH_CONV SET_SPEC_CONV) THEN
  CONV_TAC NOT_FORALL_CONV THEN EXISTS_TAC "i:num" THEN
  ASM_REWRITE_TAC[NOT_IN_EMPTY]);;

%
  This theorem is structurally identical to THM11
  Note the 0 <= i is superfluous as I use "num"; it
  would be needed if I used "int"
%

let THM13 = prove_thm(`THM13`,
  "(?l. !i. 0 <= i /\ i <= n DIV 2 ==>
                (A(l + i):real = A((l + n - 1) - i))) ==>
     ~( {l'| !i. 0 <= i /\ i <= n DIV 2 ==> (A(l' + i) = A((l' + n - 1) - i))}
        = {} )",
  STRIP_TAC THEN ONCE_REWRITE_TAC[EXTENSION] THEN
  CONV_TAC(ONCE_DEPTH_CONV SET_SPEC_CONV) THEN
  CONV_TAC NOT_FORALL_CONV THEN EXISTS_TAC "l:num" THEN
  ASM_REWRITE_TAC[NOT_IN_EMPTY]);;

%
  The last theorem is pretty routine too. Note that DIV automatically
  truncates towards 0 (I assume n is meant to be an integer) so the
  use of |floor| is implicit.

  I can't see what N > 0 has to do with anything, so I am probably
  missing the point of the theorem. Is it something to do with the
  "definedness" of the array index?
%

let THM15 = prov  "N > 0 ==> ~( {n| ?l. !i. 0 <= i /\ i < (n DIV 2) ==>
                            (A(l + i) :real = A((l + n - 1) - i)) } = {} )",
  DISCH_TAC THEN ONCE_REWRITE_TAC[EXTENSION] THEN
  CONV_TAC(ONCE_DEPTH_CONV SET_SPEC_CONV) THEN
  DISCH_THEN(MP_TAC o SPEC "1") THEN REDUCE_TAC THEN
  REWRITE_TAC[NOT_LESS_0; NOT_IN_EMPTY]);;

close_theory();;