Understanding the intros keyword work in Coq

Link:

https://stackoverflow.com/q/70482977

Question

forall P Q : Prop, P /\ ~ P -> Q


forall P Q : Prop, P /\ ~ P -> Q

  
P, Q: Prop
P_and_not_P: P /\ ~ P
Q

  
P, Q: Prop
P_holds: P
not_P: ~ P
Q

I'm trying to reaaaally understand the intros keyword. Let's say that we want to prove P /\ ~P -> Q. Ok, somehow intros P Q introduce P and Q. But what does it mean? Does it recognize the P and Q from the thing to be proven? What about P_and_not_P? What is it? Why for P and Q it uses the same name, but for P_and_not_P is defining a name?

UPDATE:

It looks like it's matching term by term:

forall P Q : Prop, (P -> Q) -> ~ Q -> ~ P


forall P Q : Prop, (P -> Q) -> ~ Q -> ~ P

  
P: Prop
forall Q : Prop, (P -> Q) -> ~ Q -> ~ P
 
P, Q: Prop
(P -> Q) -> ~ Q -> ~ P
 
P, Q: Prop
P_implies_Q: P -> Q
~ Q -> ~ P
 
P, Q: Prop
P_implies_Q: P -> Q
not_q: ~ Q
~ P
 
P, Q: Prop
P_implies_Q: P -> Q
not_q: ~ Q
not_p: P
False

gives

1 subgoal

  P, Q : Prop
  P_implies_Q : P -> Q
  not_q : ~ Q
  not_p : P
  ============================
  False

Answer

What intro A (equivalent to intros A) does: if you have a goal of the form forall (P : _), ..., it renames P to A, removes the forall from the beginning of the goal and puts an assumption A into the goal.

  (* Starting goal *)

1 subgoal

  ============================
  forall P Q : Prop, P /\ ~ P -> Q
  (* Goal after [intros A] *)

1 subgoal

  A : Prop
  ============================
  forall Q : Prop, A /\ ~ A -> Q

If you do intros P Q, by picking the names already in the goal, no renaming is necessary so there is no change in names.

The other cases of intros you mention are special cases of that one behavior.

Implications in Coq are quantifications where the assumption is not named: P /\ ~ P -> Q is equivalent to forall (H : P /\ ~P), Q, noting that H is not used in the body Q. Hence, when you do intros P_and_not_P, you are renaming H, which is not used so you don't see a change in the goal. You can disable pretty printing to see that.

Unset Printing Notations.
  (* Starting goal; a name that is not used becomes "_" *)

1 subgoal

  ============================
  forall (P Q : Prop) (_ : and P (not P)), Q
  (* After [intros P Q R] *)

1 subgoal

  P, Q : Prop
  R : and P (not P)
  ============================
  Q

The negation of P, denoted ~P, is defined as P -> False in Coq (this is typical in intuitionistic logic, other logics might differ). You can see that in action with the tactic unfold not

  (* Starting goal *)

1 subgoal

  ============================
  forall P Q : Prop, (P -> Q) -> ~ Q -> ~ P
  (* After [unfold not] *)

1 subgoal

  ============================
  forall P Q : Prop,
  (P -> Q) -> (Q -> False) -> P -> False
  (* After [intros P Q R S T] *)

1 subgoal

  P, Q : Prop
  R : P -> Q
  S : Q -> False
  T : P
  ============================
  False