2
$\begingroup$

How can I use the Lemma div_0_l from the standard library? Somehow I cannot instantiate the module that is defined as

Module Type NDivProp (Import N : NAxiomsSig')(Import NP : NSubProp N).
Improve this question
$\endgroup$
4
  • 2
    $\begingroup$ Have you tried Require Import Arith. and then used that lemma by Nat.div_0_l? $\endgroup$
    – Hiroki Chen
    Commented Apr 7 at 17:12
  • 1
    $\begingroup$ Thank you, that solves my problem. I should have searched in Coq via Search or SearchPattern command instead $\endgroup$
    – The Circle
    Commented Apr 7 at 17:35
  • 2
    $\begingroup$ @HirokiChen: if you're so kind, please post your comment as an anwser, with a small working example demonstrating the solution. Thanks! $\endgroup$
    – Andrej Bauer
    Commented Apr 12 at 12:52
  • $\begingroup$ @AndrejBauer Sure :) $\endgroup$
    – Hiroki Chen
    Commented Apr 12 at 16:04

1 Answer 1

Reset to default
2
$\begingroup$

TL;DR

To use the lemma div_0_l, you should import the Arith library as follows.

Require Import Arith.
Search (0 / ?a = 0).
----
Nat.div_0_l: forall a : nat, a <> 0 -> 0 / a = 0

More about the Module Type

The reason why you cannot instantiate the module defined as

Module Type NDivProp (Import N : NAxiomsSig')(Import NP : NSubProp N).

is that the entire file is wrapped in a so-called Module Type. All the lemmas and other stuffs in this file can be used only if you pass two arguments to this module functor.

Putting it all together, NDivProp is a module type that depends on two other modules: one that adheres to NAxiomsSig' and another that conforms to NSubProp, which itself depends on the first module.

If you are interested you can look up the Coq's library:

(* Declared in Coq.Numbers.Natural.Abstract.NAxioms. *)
Module Type NAxiomsSig := NAxiomsMiniSig <+ OrderFunctions
  <+ NZParity.NZParity <+ NZPow.NZPow <+ NZSqrt.NZSqrt <+ NZLog.NZLog2
  <+ NZGcd.NZGcd <+ NZDiv.NZDiv <+ NZBits.NZBits <+ NZSquare.

and then PeanoNat says that Nat module implements these modules:

Module Nat
  <: NAxiomsSig
  <: UsualDecidableTypeFull
  <: OrderedTypeFull
  <: TotalOrder.

The module type design, to some extent, resembles the notion of class in OOP languages, you can defined interfaces and some concrete object that implements these interfaces but you cannot directly use interfaces since they do not have an instance.

Improve this answer
$\endgroup$

Not the answer you're looking for? Browse other questions tagged or ask your own question.