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: Oct 13 2024 at 01:02 UTC