Apply: versus apply

Using Coq
1

I am really, really confused by the difference between the normal apply tactic and the ssreflect apply: tactic.

Here’s a script, the beginning of a toy formalization of Go/Weiqi/Baduk rules. In the last proof, in the intermediate sub-lemma H2, if I replace apply with apply: , I get an error. Why?

(* Support ssreflect tactic language and finitary modules. *)
Set Warnings "-notation-overridden".
From mathcomp Require Import ssreflect ssrfun ssrbool.
Set Warnings "+notation-overridden".

Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.

(* Support unicode symbols. *)
Require Import Utf8.

(* Support for classical logic. *)
Require Import FunctionalExtensionality.
Require Import ClassicalEpsilon.
Require Import PropExtensionality.

Require Import Coq.Relations.Relation_Definitions.
Require Import Coq.Classes.SetoidClass.

Section Board.

  Local Parameter N : nat.

  Definition in_bounds (p: nat * nat): Prop := fst p < N ∧ snd p < N.

  Definition point : Set := { p: nat * nat & in_bounds p }.

  Definition ex_in_bounds := @existT (nat * nat) in_bounds.

  Definition horizontal (p: point): nat :=
    let: existT (i, _) _ := p in i.

  Definition vertical (p: point): nat :=
    let: existT (_, j) _ := p in j.

  Definition same_horizontal (p1 p2: point): Prop :=
    horizontal p1 = horizontal p2.

  Definition same_vertical (p1 p2: point): Prop :=
    vertical p1 = vertical p2.

  (** The ssreflect rewrite and congr tactics have trouble with this pattern.
      I have already run into this in my toy group theory module.
      That's why I use subst here. *)
  Proposition point_extensionality (p1 p2: point):
  same_horizontal p1 p2 → same_vertical p1 p2 → p1 = p2.
  Proof.
    case: p1 => x1 ?. case: p2 => x2 ?.
    rewrite /same_horizontal /same_vertical /horizontal /vertical => H V.
    have ?: x1 = x2 by apply (injective_projections x1 x2 H V).
    by subst; congr existT; apply proof_irrelevance.
  Qed.

  Definition just_left (p1 p2: point): Prop :=
    same_vertical p1 p2 ∧
    horizontal p2 + 1 = horizontal p1.

  Definition just_right (p1 p2: point): Prop :=
    same_vertical p1 p2 ∧
    horizontal p1 + 1 = horizontal p2.

  Definition just_up (p1 p2: point): Prop :=
    same_horizontal p1 p2 ∧
    vertical p1 + 1 = vertical p2.

  Definition just_down (p1 p2: point): Prop :=
    same_horizontal p1 p2 ∧
    vertical p2 + 1 = vertical p1.

  Fact same_horizontal_sym (p1 p2: point) :
  same_horizontal p1 p2 ↔ same_horizontal p2 p1.
  Proof.
    by auto.
  Qed.

  Fact same_vertical_sym (p1 p2: point) :
  same_vertical p1 p2 ↔ same_vertical p2 p1.
  Proof.
    by auto.
  Qed.

  Fact just_left_just_right_sym (p1 p2: point) :
  just_left p1 p2 ↔ just_right p2 p1.
  Proof.
    by rewrite /just_right /just_left same_vertical_sym.
  Qed.

  Fact just_up_just_down_sym (p1 p2: point) :
  just_up p1 p2 ↔ just_down p2 p1.
  Proof.
    by rewrite /just_down /just_up same_horizontal_sym.
  Qed.

  Inductive adjacent (p1 p2: point): Prop :=
  | Aup : just_up p1 p2 → adjacent p1 p2
  | Adown : just_down p1 p2 → adjacent p1 p2
  | Aright : just_right p1 p2 → adjacent p1 p2
  | Aleft : just_left p1 p2 → adjacent p1 p2
  .

  Lemma half_adjacent_sym (p1 p2: point) :
  adjacent p1 p2 → adjacent p2 p1.
  Proof.
    case.
    - by rewrite just_up_just_down_sym; apply Adown.
    - by rewrite -just_up_just_down_sym; apply Aup.
    - by rewrite -just_left_just_right_sym; apply Aleft.
    - by rewrite just_left_just_right_sym; apply Aright.
  Qed.

  Corollary adjacent_sym (p1 p2: point) :
  adjacent p1 p2 ↔ adjacent p2 p1.
  Proof.
    by split; apply half_adjacent_sym.
  Qed.

  Inductive color := Black | White.

  Inductive point_state :=
  | Occupied of color
  | Empty
  .

  Fact ps_case ps:
  ps = Empty ∨ ps = Occupied White ∨ ps = Occupied Black.
  Proof.
    case: ps => [color_case|]; first case: color_case; auto.
  Qed.

  Definition board: Set := point → point_state.

  Implicit Type b: board.
  Implicit Type ps: point_state.

  Inductive connected b ps (p q: point) : Prop :=
  | Cid : p = q → b p = ps → connected b ps p q
  | Cadj p':
    connected b ps p p' →
    b q = ps →
    adjacent p' q →
    connected b ps p q
  .

  Lemma connected_same_state b ps (p q: point):
  connected b ps p q → b p = ps ∧ b q = ps.
  Proof.
    elim => [> ? base|> _ step_p_state step_q_state]. 
    - by split; last (rewrite -base; congr b).
    - by split; [ apply step_p_state | apply step_q_state ].
  Qed.

  Lemma connected_refl b ps (p: point):
  b p = ps → connected b ps p p.
  Proof.
    by apply Cid.
  Qed.

  Lemma connected_trans b ps (p q r: point):
  connected b ps p q → connected b ps q r → connected b ps p r.
  Proof.
    move => connected_p_q. elim => [> base|? ? ? step_connected];
    by [rewrite base in connected_p_q | apply: Cadj step_connected].
  Qed.

  Lemma connected_sym b ps (p q: point):
  connected b ps p q → connected b ps q p.
  Proof.
    elim =>
    [ > base_id
    | p2 p'
      step_connected_fw
      step_connected_bw
      step_p_state
      step_adjacent
    ].
    - by rewrite -base_id; apply: connected_refl.
    - have {step_adjacent}
        H1: adjacent p2 p'
        by apply: half_adjacent_sym step_adjacent.
      have {step_connected_fw}
        H2: b p' = ps
        by apply (connected_same_state step_connected_fw).
      have {step_p_state}
        H3: connected b ps p2 p2
        by apply: connected_refl step_p_state.
      have {H3 H2 H1}
        H4: connected b ps p2 p'
        by apply: Cadj H3 H2 H1.
      by apply: connected_trans H4 step_connected_bw.
  Qed.
2

In this case, it is the apply from traditional Coq that does something clever, one step beyond the behavior that is easily explainable. The apply: tactic does not perform this clever trick and this the reason of failure.

The statement you want to prove is “b p = ps” . The head symbol of this statement is an equality eq. The lemma connected_same_state proves a conjunction, so the head symbol of the conclusion of this lemma is an and . According to the documentation Tactics — Coq 8.15.2 documentation, the apply tactic should peform unification between a formula that starts with eq and a formula that starts with and. This unification actually fails. In a way, this explains why apply: ... fails.

The apply tactic on the other hand, tries to recover from the failure by applying a behavior that requires a little more explanation: when the head lemma is a conjunction, each of the conjuncts is tried in turn as if it was itself the conclusion of the lemma. So we end up tryping to unify b p = ps (with b p ps universally quantified in the lemma statement) and b p' = ps (with b p’ and ps actually fixed by the instantiation of the lemma’s premise on step_connected_fw). This unification succeeds.

This clever behavior is actually documented in the Coq documentation, in a note that appears after the example. This clever behavior is implemented in the apply tactic of traditional Coq and not in the apply: tactic of ssreflect.

1 Like
3

So I suppose to make it resistant to that difference, I should apply a projection of connected_same_state, right?

4

yes

by apply: (proj2 (connected_same_state step_connected_fw)).

works in my copy of your script.

5

Hi, to add one of the usual answers to this question: make pressure on the Coq development team so that it clarifies the whole picture about tactics (e.g. in the current circonstance, that the behavior of going under conjunctions is made configurable both for apply and apply:, or, more generally, that apply and apply: differ only by a set of flags).