CODEWITHSUNDEEP
coqssreflect
András Kovács
András Kovács

Reputation: 30103

No implicits in dependent "match" pattern with ssreflect

It seems to me that with ssreflect, implicit constructor fields turn into explicit fields when we do dependent pattern matching, and setting various implicit options doesn't affect this behavior.

The following code is fine with Coq 8.6:

Require Import Coq.Unicode.Utf8.
Set Implicit Arguments.
Set Contextual Implicit.

Inductive Vec (A : Type) : nat → Type :=
  nil  : Vec A 0
| cons : ∀ {n}, A → Vec A n → Vec A (S n).

Fixpoint append {A n m}(xs : Vec A n)(ys : Vec A m) : Vec A (n + m) :=
  match xs with
    nil => ys
  | cons x xs => cons x (append xs ys)
  end.

It stops working when I import ssreflect, because it demands an extra field for the cons pattern in append:

From mathcomp Require ssreflect.

Fixpoint append {A n m}(xs : Vec A n)(ys : Vec A m) : Vec A (n + m) :=
  match xs with
    nil => ys
  | cons _ x xs => cons x (append xs ys)
  end.

What's the reason for this, and is there a way to still have the implicits in pattern matching?

Upvotes: 3

Views: 99

Answers (1)

ejgallego
ejgallego

Reputation: 6852

There was a change in pattern behavior between Coq 8.5 and Coq 8.6 that basically broke every Coq script in existence, for 8.6 will take into account implicit arguments in patterns as you have noticed.

Instead of rewriting all of their library for the 8.6 specific feature, which would have prevented compatibility with 8.5, ssreflect opted to revert back to 8.5 behavior by setting the Asymmetric Patterns option when you load the plugin.

You can go back to the default 8.6 behavior doing

Global Unset Asymmetric Patterns.

in your script after you import ssreflect.

Upvotes: 6

Related Questions