The Logic of Rocq

Curry-Howard Correspondence

• Propositions as Types correspondence

• Formulas correspond to types

• Proofs correspond to terms

• Formula true iff type inhabited

• Discovered by Haskell Curry and William Howard

Rocq Has-Type Relation

• t : τ means term t has type τ

• Rocq's kernel checks this relation

• All terms are typed

• Types are terms

Simple Typing Rules

• lam: x:S ⊢ e:T implies ⊢ (λ(x:S).e) : (S → T)
• app: ⊢ e1:S→T and ⊢ e2:S implies ⊢ (e1 e2) : T
• Minimal core of type system

Dependent Function Types

• lam: x:S ⊢ e:T[x] implies ⊢ (λ(x:S).e) : (∀(x:S), T[x])
• app: e1:∀(x:S),T[x] and e2:S implies (e1 e2):T[e2]
• Types can depend on terms

Implication as Function Type

• P ⇒ Q corresponds to function type P → Q
• Proof transforms proof of P to proof of Q
• Modus ponens corresponds to function application

Conjunction as Product Type

• P ∧ Q corresponds to product type (P,Q)
• Proof is pair (p,q)
• Projections correspond to conjunction elimination

Disjunction as Sum Type

• P ∨ Q corresponds to sum type P + Q (Either)
• Constructors inl and inr for disjunction introduction
• Case analysis corresponds to disjunction elimination

Truth as Unit Type

• ⊤ corresponds to unit type with single constructor
• Always inhabited
• Represents trivially true proposition

Falsity as Empty Type

• ⊥ corresponds to empty type with no constructors
• No proof exists
• Uninhabited type represents contradiction

Law of Excluded Middle in Rocq

• Rocq does not assume P ∨ ¬P by default
• Constructive logic
• Axiom for decidable propositions

Constructive Logic

• Proofs must be constructive
• Existence proved by explicit construction
• Rocq implements intuitionistic logic

Logic vs Types in Rocq

• Rocq doesn't need separate logic
• Type system provides logical reasoning
• Propositions are types, proofs are terms