coqlogical-foundations

How to set implicit parameters for constructor

Playing with nostutter excersizes I found another odd behaviour. Here is the code:

Inductive nostutter {X:Type} : list X -> Prop :=
| ns_nil : nostutter []
| ns_one : forall (x : X), nostutter [x]
| ns_cons: forall (x : X) (h : X) (t : list X), nostutter (h::t) -> x <> h -> nostutter (x::h::t).

Example test_nostutter_manual: not (nostutter [3;1;1;4]).
Proof.
  intro.
  inversion_clear H.
  inversion_clear H0.
  unfold not in H2.
  (* We are here *)
  specialize (H2 eq_refl).
  apply H2.
Qed.

Status after unfold is this:

1 subgoal (ID 229)

H1 : 3 <> 1
H : nostutter [1; 4]
H2 : 1 = 1 -> False
============================
False

When I run specialize (H2 eq_refl). inside IndProp.v that loads other Logical foundations files, it works. Somehow it understands that it needs to put "1" as a parameter. Header of IndProp.v is this:

Set Warnings "-notation-overridden,-parsing".
From LF Require Export Logic.
Require Import String.
Require Coq.omega.Omega.

When I move the code into another file "nostutter.v", this same code gives an expected error:

The term "eq_refl" has type "RelationClasses.Reflexive Logic.eq" while it is expected to have type "1 = 1".

Header of nostutter.v:

Set Warnings "-notation-overridden,-parsing".
Require Import List.
Import ListNotations.
Require Import PeanoNat.
Import Nat.
Local Open Scope nat_scope.

I have to explicitly add a parameter to eq_refl: specialize (H2 (eq_refl 1)).

I think it's not related specifically to specialize. What is it? How to fix?

Solution

  • The problem is importing PeanoNat.Nat.

    When you import PeanoNat, the module type Nat comes into scope, so importing Nat brings in PeanoNat.Nat. If you meant to import Coq.Init.Nat, you'll either have to import it before importing PeanoNat, or import it with Import Init.Nat..

    Why does importing PeanoNat.Nat cause trouble in this case?

    Arith/PeanoNat.v (static link) contains the module1 Nat. Inside that module, we find2 the unusual looking line

    Include NBasicProp <+ UsualMinMaxLogicalProperties <+ UsualMinMaxDecProperties.

    All this means is that each of NBasicProp, UsualMinMaxLogicalProperties and UsualMinMaxDecProperties are included, which in turn means that everything defined in those modules is included in the current module. Separating this line out into three Include commands, we can figure out which one is redefining eq_refl. It turns out to be NBasicProp, which is found in this file (static link). We're not quite there yet: the redefinition of eq_refl isn't here. However, we see the definition of NBasicProp in terms of NMaxMinProp.

    This leads us to NMaxMin.v, which in turn leads us to NSub.v, which leads us to NMulOrder.v, which leads us to NAddOrder.v, which leads us to NOrder.v, which leads us to NAdd.v, which leads us to NBase.v, ...

    I'll cut to the chase here. Eventually we end up in Structures/Equality.v (static link) with the module BackportEq which finally gives us our redefinition of eq_refl.

    Module BackportEq (E:Eq)(F:IsEq E) <: IsEqOrig E.
 Definition eq_refl := @Equivalence_Reflexive _ _ F.eq_equiv.
 Definition eq_sym := @Equivalence_Symmetric _ _ F.eq_equiv.
 Definition eq_trans := @Equivalence_Transitive _ _ F.eq_equiv.
End BackportEq.

    The way this is defined, eq_refl (without any arguments) has type Reflexive eq, where Reflexive is the class

    Class Reflexive (R : relation A) :=
  reflexivity : forall x : A, R x x.

    (found in Classes/RelationClasses.v)

    So that means that we'll always need to supply an extra argument to get something of type x = x. There are no implicit arguments defined here.

    Why is importing modules like PeanoNat.Nat generally a bad idea?

    If the wild goose chase above wasn't convincing enough, let me just say that modules like this one, which extend and import other modules and module types, are often not meant to be imported. They often have short names (like N, Z or Nat) so any theorem you want to use from them is easily accessible without having to type out a long name. They usually have a long chain of imports and thus contain a vast number of items. If you import them, now that vast number of items is polluting your global namespace. As you saw with eq_refl, that can cause unexpected behavior with what you thought was a familiar constant.

    1. Most of the modules encountered in this adventure are of the "module type/functor" variety. Suffice to say, they're difficult to understand fully, but a short guide can be found here.

    2. My sleuthing was done by opening files in CoqIDE and running the command Locate eq_refl. (or better yet, ctrl+shift+L) after anything that might import from elsewhere. Locate can also tell you where a constant was imported from. I wish there were an easier way to see the path of imports in module types, but I don't think so. You could guess that we'd end up in Coq.Classes.RelationClasses based on the type of the overwritten eq_refl, but that isn't as precise.