[opentheory-users] Theorems about sums
Rob Arthan
rda at lemma-one.com
Mon Mar 31 16:01:26 UTC 2014
Joe,
On 27 Mar 2014, at 18:04, Joe Leslie-Hurd <joe at gilith.com> wrote:
> Hi Rob,
>
> Many thanks for that. I have now defined a set fold operation like the one in the repo and I can import the whole base package conservatively without any devious tricks in one go using the article file that your perl magic generates.
>
> That is excellent news.
>
> I have just one outstanding concern: there are no theorems in the sum package and only one in the real package (and the only operators it uses are <= and sup. There don’t seem to be any uses of real or sum in the other packages in the repo, so I haven’t really been able to test that I have got the mappings right for these packages. Any suggestions would be welcome.
>
> Hmm... do you have any suggestions for theorems about sum types that I could prove in a sum-thm package to help here? Does ProofPower contain any such theorems?
>
I didn’t have any to hand. The following are analogous to some of the theorems you have about pairs.
⊢ ∀ p⦁ (∀ x⦁ p x) ⇔ (∀ a⦁ p (InL a)) ∧ (∀ b⦁ p (InR b))
⊢ ∀ p⦁ (∀ a⦁ p a) ⇔ (∀ x⦁ p (OutL x))
⊢ ∀ p⦁ (∀ b⦁ p b) ⇔ (∀ x⦁ p (OutR x))
I can send you an article that proves these if you like (but the proofs are so easy, it is probably more trouble than it is worth).
I will have a think about how you might populate real-thm.
Regards,
Rob.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.gilith.com/opentheory/mailing-list/attachments/20140331/2e44a991/attachment.html>
More information about the opentheory-users
mailing list