UniMath / agda-unimath

The agda-unimath library
https://unimath.github.io/agda-unimath/
MIT License
219 stars 71 forks source link

Are allotropes of carbon hydrocarbons? #232

Open ghost opened 2 years ago

ghost commented 2 years ago

There are certain molecules called allotropes of carbon which consist entirely of carbon atoms. Examples include carbon nanotubes and fullerines. https://en.wikipedia.org/wiki/Allotropes_of_carbon https://en.wikipedia.org/wiki/Carbon_nanotube https://en.wikipedia.org/wiki/Fullerene With the current definition of hydrocarbon, these molecules are hydrocarbons with zero hydrogen atoms.

But I'm not sure if the chemistry community would call allotropes of carbon 'hydrocarbons', common usage seems to imply that there is at least one hydrogen atom in a hydrocarbon.

EgbertRijke commented 2 years ago

I agree with you, hydrocarbons should probably have at least one hydrogen atom! Thank you again for your contribution!

plt-amy commented 2 years ago

I believe this is already impossible. If we look at this confusing-perspective diagram of Cā‚†ā‚€ fullerene (from PubChem, but I'll take full blame for the hand-drawn highlighting), we see that the highlighted carbon has 4 incident edges.

image

But this isn't allowed:

(c c' : vertex-Undirected-Graph-š”½ G) ā†’ leq-ā„•
  (number-of-elements-is-finite (is-finite-type-š”½ (pr2 G (standard-unordered-pair c c'))))
  3)

Translating, in the type of hydrocarbons, each carbon (vertex in the underlying graph) can have at most three carbon-carbon bonds. This excludes every allotrope: they all have every carbon making 4 carbon-carbon bonds!

EgbertRijke commented 2 years ago

The condition you mention here only excludes quadruple bonds between two carbon atoms in the molecule.

ghost commented 2 years ago

According to Egbert Rijke in https://github.com/UniMath/agda-unimath/issues/234#issuecomment-1176187175 requiring the molecule to have at least one hydrogen atom implies that there are no quadruple bonds between two carbon atoms in the molecule, because the graph is connected.