Hi, I'm trying to make sense of how Coq works. I've seen some rules of inference in a natural deduction system, e.g.

- conj-intro
- conj-elim-left and -right
- disj-intro-left and -right
- disj-elim
- impl-intro
- impl-elim/modus ponens
- not-intro, i.e.
`(P -> false) -> ~P`

. - not-elim (or false intro), i.e.
`~P -> P -> false`

.

Yet, instead of taking these rules as granted. I am able to prove them using Coq's built-in tactics. Thus, I wonder whether Coq's tactics are a more general form of deductive system than the natural deduction system. "More general" because these connectives are not built-in and can be defined as indprops, and therefore these tactics are applicable to inductive types in general(?).

Thanks!

One sometimes says that Coq is a MetaLanguage.

Hmm, then are Coq tactics a meta-deductive system, such that it can be used to define deductive system in the object language? :thinking:

Coq has an underlying type theory which has typing rules similar to natural deduction. Tactics can be used to build proofs in this system if you want.

Ah, I see. Deductive behaviours of Coq are governed by its typing rule. Then, the process of building up its type is the process of carrying out deduction

Gosh, can't imagine how powerful is the underlying type theory of Coq. Seems like everything is pointing back to it. Thanks!

Jiahong Lee has marked this topic as resolved.

Arguably Coq's basic tactics resemble a sequent calculus (given that tactics often talk about parts of the context and do case-splitting as a basic operation), with running a tactic script amounting to translating the sequent calculus proof into Coq's core natural deduction type theory (plus loads of elaboration). However, this view breaks down with tactics like `repeat`

, which only makes sense because tactics are untyped and stateful (they are commands that modify the proof state and build a term piecewise).

Last updated: May 18 2024 at 08:40 UTC