sphinx-proof

sphinx-proof copied to clipboard

If we want to support commonality with sphinxcontrib-proof we may want to add the common types:

proof_theorem_types = {
   "algorithm": "Algorithm",
   "conjecture": "Conjecture",
   "corollary": "Corollary",
   "definition": "Definition",
   "example": "Example",
   "lemma": "Lemma",
   "observation": "Observation",
   "proof": "Proof",
   "property": "Property",
   "theorem": "Theorem",
}

https://sphinxcontrib-proof.readthedocs.io/en/latest/usage/#common-options

@jstac is using proof:example in his new lecture set.

The types which we have in the package at present is:

["proof", "theorems", "axioms","lemmas","definitions","Criterion","Remarks","Conjectures", "Corollaries" ,"Algorithms", "Exercise"]

thanks @AakashGfude it would be helpful to perhaps list the ones that are not implemented. It looks like property and example from sphinxcontrib-proof are not implemented.

exercise, axiom, remarks, criterion are new.

In that case I wonder why {proof:example} isn't working in John's project then.

```{proof:example} Exponential curves are UC semigroups
:label: ecuc

If $U_t = e^{tA}$ for $t \in \RR_+$ and $A \in \linop$, then $(U_t)$
is a uniformly continuous semigroup on $\BB$.
```

is causing:

ctmc_lectures/generators.md:230: WARNING: Unknown directive type "proof:example".

@mmcky example is also not implemented I think. nor is observation. And Exercise, axiom is also additional it seems.

thanks @AakashGfude was reading exercise too quickly :-)

exercise was used in @boazbk's TCS textbook. Unfortunately, I can't remember where I saw the axiom example.

I'll add the following directives:

• [x] example
• [x] property
• [x] observation
• [x] proposition

Thanks guys! @najuzilu , you've done really nice work here! Could you please add "proposition" as well, and make it the same as "theorem"?

As of now, we're supporting the following directives (total 15):

• proof
• theorem
• axiom
• lemma
• definition
• criterion
• remark
• conjecture
• corollary
• algorithm
• exercise
• example
• property
• observation
• proposition

solution directive is in the workings bringing the total to 16 directives.

With all these additions, I wonder if we should open a discussion to rename the proof domain. While moving them to new extensions would be one solution, the reason I have kept them all within one domain is that the numbering for each directive builds on the other directive (similar to how LaTeX numbers these types of directives). For example, figure and table directives are independent of each other so their numbering depends on previous respective directives. This is not the case for the directives in this extension.

What do others think?