compiling from hcode to ghilbert

[Joe Corneli]

Hi all:

Some years ago Raph and I had a few exchanges on the AsteroidMeta wiki about "hcode" and its potential relationship to Ghilbert.  At the time, hcode was more or less vaporware -- but I think it is starting to distill into something.  I now have some time to think about this more, I'm wondering whether it's reasonably possible to compile from hcode to Ghilbert.  A developing spec is here: http://metameso.org/~joe/math/hcode.pdf

I'm encouraged by noticing some recent additions to the Metamath repository that are very recognizable as the kind of thing I might want to prove.  http://de.metamath.org/mpeuni/cncfss.html is one example.

Here, below, is a sketch of a proof represented in hcode.  Could we translate this to Ghilbert?  Please keep in mind that at the moment hcode is just a representation language: it doesn't "do" anything.  I've spelled out some inferences in comments that would have to be made explicit in a more formal system and I don't know how much, if any, could be picked up from context.  I'm not attached to any such "magic".

Many of your examples look "close" -- though I don't know why you've dropped the outer parentheses on your s-exps.  Maybe hcode could be understood to be syntactic sugar over Ghilbert.  I have many addition definitions and theorems, and all-too-few proofs written down.  I'd like to be able to just sit and "transcribe" mathematical texts into a format like what follows, and much better if it actually runs somehow.

I'll start off with a simple example, if the prospects here are looking good I'll follow up with something more complicated next.

Cheers,

Joe

(defn topological-space (X T)
   (set X)
   ;; T is a set of subsets of X
   (subset T (setof Y :st (subset Y X)))
   (elt empty-set T)
   (elt X T)
   ;; closed under finite intersections
   (forall V :st (if (countable-subset V T)
                     (elt (intersection (setof v :st (elt v V)))
                          T)))
   ;; closed under unions
   (forall W :st (if (subset W T)
                     (elt (union (setof w :st (elt w W)))
                          T))))

(defthm elements-in-open-subsets-means-set-is-open
 (X T A)
  (topological-space X T)
  (subset A X)
  (forall a :in A :st (exists B :in T
                                :st (and (elt a B)
                                         (subset B A))))
  (elt A T))

(defproof
  PR:elements-in-open-subsets-means-set-is-open (X T A)
  ;; we can make use of the main assumption
  (forall a :in A
          (bind (sub B a)
                (some B :in T
                        :st (and (elt a B)
                                 (subset (sub B a) A)))))
  ;; per `topological-space' closure under unions,
  ;; the union of our chosen open sets is open
  (implies (forall W :st (if (subset W T)
                    (elt (union (setof w :st (elt w W)))
                         T)))
           (elt (union (setof (sub B a))) T)) ; [i]
  ;; the union of subsets is a subset
  (implies (subset (sub B a) A)
           (subset (union (setof (sub B a))) A))
  ;; And if each element of a set is contained in
  ;; an element of a cover, the set is contained
  ;; in the union of covering sets
  (implies (forall a :in A (exists (sub B a)
                     :st (elt a (sub B a))))
           (subset A (union (setof (sub B a)))))
  ;; So we have containment in both directions and
  ;; can conclude:
  (eq A (union (setof (sub B a)))) ; [ii]
  ;; and [i] showed that this union is in T
  ;; so this concludes the proof
)