Stream: Coq users

Topic: ✔ [Beginner theory] Are Coq tactics a deductive system?

Jiahong Lee (Jul 21 2022 at 05:20):

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.

1. conj-intro
2. conj-elim-left and -right
3. disj-intro-left and -right
4. disj-elim
5. impl-intro
6. impl-elim/modus ponens
7. not-intro, i.e. (P -> false) -> ~P.
8. 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!

Li-yao (Jul 21 2022 at 07:11):

One sometimes says that Coq is a MetaLanguage.

Jiahong Lee (Jul 21 2022 at 08:10):

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

Théo Winterhalter (Jul 21 2022 at 08:18):

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.

Jiahong Lee (Jul 21 2022 at 08:31):

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

Jiahong Lee (Jul 21 2022 at 08:33):

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

Notification Bot (Jul 21 2022 at 08:33):

Jiahong Lee has marked this topic as resolved.

James Wood (Jul 23 2022 at 14:04):

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: Oct 13 2024 at 01:02 UTC