Show newer

Is it possible to define a mutual inductive type and coinductive type in Coq? I can do this in Agda by putting the declarations at the top but Coq only seems to have with

re: G proof 

It's like a little logic puzzle and I got sniped

Show thread

re: G proof 

If you interpret r, s, t, u as sets (might as well), then ⊳ is some sort of pointwise order (every element of r is greater than every element of s), and ⊏ (not <, oops) is the subset relation
Axiom 4 says that if r is pointwise greater than s and u is a subset of s, then r is pointwise greater than u, which makes sense
Axiom 5 says that there is a set r s.t. if there is a set pointwise smaller than z, then z is a subset of r
Personally I think ax5 isn't independent of ax1 and ax4
I bet Axiom 5 could be proven from the other axioms
I bet I can find a shorter proof

Show thread

G proof 

Looks like there's two relations, _ ⊳ _ and _ < _
The first is meant to be some sort of order and the second one is some sort of subtyping relation

Definitions:

  • S r ≡ r ⊳ r
  • C r ≡ ∃s. r ⊳ s
  • O r ≡ ∀s. r ⊳ s

Axioms:

  • ax1: ∀r. ∃v. v ⊳ r
  • ax2: ∀r. ∀s. ∀t. (r ⊳ s) → (s ⊳ t) → (r ⊳ t)
  • ax3: ∀r. ∀s. (r ⊳ s) → (s ⊳ r) → r = s
  • ax4: ∀r. ∀s. (r ⊳ s) → (u < s) → r ⊳ u
  • ax5: ∃r. ∀z. C z → z < r, i.e. ∃r. ∀z. ∃s. z ⊳ s → z < r

Let's see... ax1 says that there always exists a greater element, ax2 is transitivity, ax3 is antisymmetry, and ax4 and ax5... well I can't tell what < is meant to be
In any case the G theorem just says that there's a unique maximal element that's reflexive under ⊳

Anyway, and is and, or is or, nor is nor, so is implication, for is inverse implication, and yet is like the inverse of but

Show thread

They're all coordinating conjunctions but it doesn't seem like for or so could be used to coordinate anything but independent clauses, i.e. not noun phrases

Show thread

In school we learned about FANBOYS:
For
And
Nor
But
Or
Yet
So

Show thread

"and" is a conjunction. "or" is a conjunction. what about "but"

In contrast, a well-founded data type like [Integer] lives entirely in the moment.

McBride writes the funniest sentences

genitals, Coq 

Okay people like this

But maybe you should ask yourself why you see what-you-don't-want-to-see in something that has never been related to what-you-don't-want-to-see...
(If the shape of the Coq logo makes you think to what-you-don't-want-to-see, maybe it's time to go to the doctor...?)

People like this annoy me so much

Show thread

"It type checks but I have no idea what it means" is my slogan right now

genitals, Coq 

They're doing the "yeah I agree" reply-all email chain on the Coq mailing list about Coq sounding like "cock" and the logo looking like a beige cock

(inspecting gender) Wow..... this is a shit type system...

There's no good way of pronouncing Coq anyway
Say it in English and it sounds like cock
Say it in French and it sounds like cuck

Show older
types.pl

A Mastodon instance for users who like the study of programming languages, formal semantics, types, or linguistics.