Stream: Coq users

Topic: ✔ Using short names of theorems in a Module (eg PeanoNat....

Pierre Rousselin (Oct 04 2022 at 04:46):

Is there a way to use short names for theorems proved in a module ? I am thinking of theorems in Coq.Arith.PeanoNat.Nat.

Require Import PeanoNat
Fail Definition plop := mul_comm.
Definition hop := Nat.mul_comm.

Guillaume Melquiond (Oct 04 2022 at 05:04):

Just Import Nat.

Pierre Rousselin (Oct 04 2022 at 05:31):

This doesn't work :

Require Import PeanoNat.
Require Import Nat.
Fail Definition plop := mul_comm.

Guillaume Melquiond (Oct 04 2022 at 05:37):

You are confusing Require and Import. Require loads a file, while Import puts the content of a module into scope. So, when you write Require Import Nat, you are telling Coq to load a file named Nat.vo and then to put its content into scope. What I was telling you was to do Require Import PeanoNat. Import Nat., that is, load the PeanoNat.vo file and then import the Nat module that is part of that file.

Guillaume Melquiond (Oct 04 2022 at 05:38):

(And in case that was not clear, Require Import X is just syntactic sugar for Require X. Import X.)

Pierre Rousselin (Oct 04 2022 at 05:50):

Thank you ! Indeed, I had not understood this. This is clear now.

Last updated: Oct 04 2023 at 18:01 UTC