Search code examples
coq

How to mix sections with hints in Coq?

I am writing something heavily involving typeclasses and I would like to utilize hints to ease proving local lemmas as well as exported theorems.

For instance, consider

Class MyClass (A : Type) :=
  connect : A -> A -> Prop.

Fixpoint chain [A] [C : MyClass A] (l : list A) {struct l} : Prop :=
  match l with
  | [] | [_] => True
  | a0 :: (a1 :: _ as rest) => connect a0 a1 /\ chain rest
  end.

Lemma chain_seq : forall {A} `{C : MyClass A} l1 l2,
    chain l1 -> chain l2 -> chain (l1 ++ l2).
Admitted.

Lemma chain_seq_seq : forall {A} `{C : MyClass A} l1 l2 l3,
    chain l1 -> chain l2 -> chain l3 -> chain (l1 ++ l2 ++ l3).
Admitted.

(* and so on... *)

It's quite annoying to specify that {A} {C : MyClass A} in every single lemma or definition (imagine having more parameters and more classes). Thankfully, we have the Section construction to help:

Section ChainFacts.
  Variable A : Type.
  Context `{C : MyClass A}.

  Lemma chain_seq : forall l1 l2,
      chain l1 -> chain l2 -> chain (l1 ++ l2).
  Admitted.

  Lemma chain_seq_seq : forall l1 l2 l3,
      chain l1 -> chain l2 -> chain l3 -> chain (l1 ++ l2 ++ l3).
  Admitted.

Way better. Now I add a hint for the first theorem and use it to show the second one:

Section ChainFacts.
  Variable A : Type.
  Context `{C : MyClass A}.

  Lemma chain_seq : forall l1 l2,
      chain l1 -> chain l2 -> chain (l1 ++ l2).
  Admitted.
  Hint Resolve chain_seq.

  Lemma chain_seq_seq : forall l1 l2 l3,
      chain l1 -> chain l2 -> chain l3 -> chain (l1 ++ l2 ++ l3).
    intros. auto.
  Qed.
End ChainFacts.

That works. However, it does not after I exit the section:

End ChainFacts.

#[export] Instance nat_connect : (MyClass nat) := eq.

Lemma chain_seq_seq_out : forall  [l1 l2 l3 : list nat],
    chain l1 -> chain l2 -> chain l3 -> chain (l1 ++ l2 ++ l3).
  intros. now auto.
  (* Tactic failure: Cannot solve this goal. *)

That is because hints are always section-local, which I frankly speaking do not like. I really want to be able to use hints right after each lemma definition, but I also want to export them to be used externally. Currently I see two exits from this situation:

  • Not use sections (and suffer the pain of writing all class-related stuff every single time)
  • Maintain a copy of all hint declarations right after closing the section. Bonus fun points: do it for each time a section is nested.

Is there anything else I can do?

Solution

  • https://coq.inria.fr/doc/V8.19.0/refman/proofs/automatic-tactics/auto.html#creating-hints

    Inside sections, some commands only support the local attribute. These are Hint Immediate, Hint Resolve, Hint Constructors, Hint Unfold, Hint Extern and Hint Rewrite. local is the default for all hint commands inside sections.

    Seems like you may have to repeat all the Hint Resolve lines directly after the End Section. :(