You do not have permission to delete messages in this group
Report message as abuse
Sign in to report message as abuse
Show original message
Either email addresses are anonymous for this group or you need the view member email addresses permission to view the original message
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
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.
(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 )