Stream: Coq users

Topic: Parameter keyword in Coq modules

Gergely Buday (Aug 04 2020 at 08:58):

I am to translate the module example at

https://github.com/coq/coq/wiki/ModuleSystemTutorial

into Isabelle using locales:

Module Type Sig.
Parameter A : Type.
Parameter le : A ⇒ A ⇒ Prop.
Infix "≤" := le : order_scope.
Open Scope order_scope.
Axiom le_refl : ∀ x, x ≤ x.
Axiom le_antisym : ∀ x y, x ≤ y ⇒ y ≤ x ⇒ x = y.
Axiom le_trans : ∀ x y z, x ≤ y ⇒ y ≤ z ⇒ x ≤ z.
Axiom le_total : ∀ x y, {x ≤ y} + {y ≤ x}.
Parameter le_dec : ∀ x y, {x ≤ y} +{¬ x ≤ y}.
End Sig.

Aside the Coq example being constructive, using prop where I will use bool in Isabelle, there is a quirk with Parameter.

The first Parameters I translate as fixes into Isabelle which is usually at the beginning of a locale, they fix universally quantified variables with types.

Axioms will be assumes in Isabelle, these are the logical rules for the variables mentioned in Parameter.

But why is the last rule a Parameter? That's not a variable but a reformulation of totality, which is different from total: in a constructive setting. Why is it not an Axiom in Coq?

Karl Palmskog (Aug 04 2020 at 09:00):

`Axiom` and `Parameter` inside a module signature are not really axioms in the sense of, for example, the law of excluded middle. They just convey that if you want to create a module of the indicated type, you have to provide certain types and prove certain theorems about them.

Ali Caglayan (Aug 04 2020 at 09:02):

Didn't there used to be a difference when axiom also declared instances which it doesn't anymore?

Gergely Buday (Aug 04 2020 at 09:04):

What would be the difference if I used

Axiom le_dec : ∀ x y, {x ≤ y} +{¬ x ≤ y}.
End Sig.

?

Karl Palmskog (Aug 04 2020 at 09:06):

`Axiom` and `Parameter` are effectively synonyms, but there is a convention to use the former for things that live in `Prop`, and the latter for non-`Prop` things, like decision procedures

Gergely Buday (Aug 04 2020 at 09:09):

Karl Palmskog I guess the name le_dec refers to decision, doesn't it?

Karl Palmskog (Aug 04 2020 at 09:11):

yes, the name hints at it, but everything that has type `{...}+{...}` or just `{...}` lives in `Set`/`Type` (not `Prop`)

Gergely Buday (Aug 04 2020 at 09:16):

I do not have much expertise in Coq, where can I read about {...} and {...} + {...} ? What is this syntax?

Karl Palmskog (Aug 04 2020 at 09:19):

most intro Coq books will cover it. But for the definition, see https://coq.inria.fr/stdlib/Coq.Init.Specif.html

Last updated: Jun 14 2024 at 19:02 UTC