CODEWITHSUNDEEP
coqcoq-tacticltac
Carl Patenaude Poulin
Carl Patenaude Poulin

Reputation: 6589

Ltac pattern matching: why does `forall x, ?P x` not match `forall x, x`?

Ltac checkForall H :=
  let T := type of H in
  match T with
  | forall x, ?P x =>
    idtac
  | _ =>
    fail 1 "not a forall"
  end.

Example test : (forall x, x) -> True.
Proof.
  intros H.
  Fail checkForall H. (* not a forall *)
Abort.

I would naively expect checkForall H to succeed, but it doesn't.

In his book Certified Programming with Dependent Types, Adam Chlipala discusses a limitation of pattern matching on dependent types:

The problem is that unification variables may not contain locally bound variables.

Is this the reason for the behaviour I'm seeing here?

Upvotes: 3

Views: 486

Answers (2)

Arthur Azevedo De Amorim
Arthur Azevedo De Amorim

Reputation: 23592

As larsr explained, the pattern ?P x can only match a term that is syntactically an application, which does not cover the case you are considering. However, Ltac does provide features for the match you are looking for. As the user manual says:

There is also a special notation for second-order pattern-matching problems: in an applicative pattern of the form @?id id1 …idn, the variable id matches any complex expression with (possible) dependencies in the variables id1 …idn and returns a functional term of the form fun id1 …idn => term.

Thus, we can write the following proof script:

Goal (forall x : Prop, x) -> False.
intros H.
match goal with
| H : forall x : Prop, @?P x |- _ => idtac P
end.

which prints (fun x : Prop => x).

Upvotes: 8

larsr
larsr

Reputation: 5811

The type of H is forall x, x, not forall x, P x.

Ltac checkForall H :=
  let T := type of H in
  match T with
  | forall x, ?P x =>
    idtac
  | forall x, x =>
    idtac "this matches"
  | _ =>
    fail 1 "not a forall"
  end.

Example test : (forall x, x) -> True.
Proof.
  intros H.
  checkForall H. (* not a forall *)

Abort.

or to match your checkForall

Example test {T} (f:T->Prop)  : (forall x, f x) -> True.
Proof.
  intros H.
  checkForall H.

Upvotes: 2

Related Questions