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?

`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.

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

What would be the difference if I used

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

End Sig.

?

`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

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

yes, the name hints at it, but everything that has type `{...}+{...}`

or just `{...}`

lives in `Set`

/`Type`

(not `Prop`

)

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

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