Hi, for the Coq Platform docs project, I need to be able to redefine definitions several times.
For instance, I would like to be able to define a function map
with a syntax, then again with another without having to name it map'
. Simialrly, for proving different time a lemma.
Is there any way to do that in Coq ? I have tried a few stuffs, but I haven't succeeded.
For a minimal working example:
Require Import List.
Import ListNotations.
Fixpoint map {A B} (f : A -> B) (l : list A) : list B :=
match l with
| nil => nil
| cons a l => cons (f a) (map f l)
end.
Fixpoint map {A B} (f : A -> B) (l : list A) : list B :=
match l with
| [] => []
| a::l => (f a) :: (map f l)
end.
there is no shadowing for globals
you can put each def in a separate module.
Isn't there a tactic or a command to reset the head of the global goal ?
Opening and closing sections wouldn't be very suited
what's the "global goal"?
Sorry, I meant the environment. Can't I just reset it to a specific point or something ? The command Succeded is supposed to do something like that, does an action than reverts it, but it does not work to revert definitions
Related discussion: https://github.com/coq-community/vscoq/issues/687
You have such command in coqtop
but they don't really fit in the "document model" that IDEs use nowadays.
I would recommend something like:
Require Import List.
Import ListNotations.
Module Ex1.
Fixpoint map {A B} (f : A -> B) (l : list A) : list B :=
match l with
| nil => nil
| cons a l => cons (f a) (map f l)
end.
Eval compute in (map (fun x => x+1) [3;4;5]).
End Ex1.
Module Ex2.
Fixpoint map {A B} (f : A -> B) (l : list A) : list B :=
match l with
| [] => []
| a::l => (f a) :: (map f l)
end.
Eval compute in (map (fun x => x+1) [3;4;5]).
End Ex2.
there appears to be consensus among several ITP systems that shadowing for global names is a bad idea, the recent HOL4 release has completely disabled it: https://github.com/HOL-Theorem-Prover/HOL/releases/tag/trindemossen-1 ("incompatibilities")
in fact, when they disabled shadowing they found a "bug" (missing theorem) in one of the bundled theories
I understand. I guess it might just be a question of interface. There is a begin / end in codqoc. Maybe, we could have something similar to hide begin and end of modules in order nor to parasite reading.
We had some discussion about Reset
et al this week and we actually decided to implement them in coq-lsp
as they are quite easy to support, and together with the incremental engine, they do provide some interesting features that amount to "document partinioning", that is to say, when you do Reset bar
, the document state at this point is just before bar
, so the slide of the document between bar
and Reset bar
can be updated, and what follows after Reset bar
won't be re-checked.
But in general I agree that these features are only useful mainly as a low-level hacks during proof development.
@Emilio Jesús Gallego Arias From me, it is mostly about pedagogies c.f. https://github.com/Zimmi48/platform-docs
You say there is "there is no shadowing for globals" but about the behaviour described in this tutorial ?
Module Foo.
Definition foo := 42.
Lemma bar : 21 * 2 = foo.
Proof. reflexivity. Qed.
Lemma baz : 21 + 21 = foo.
Proof. reflexivity. Qed.
End Foo.
Import Foo.
(** When we [Import]ed our [Foo] module before, there was no possible name
clash since no constant in our context were named [foo], [bar] or [baz].
In real life Coq, however, global contexts can be huge and there will
be name clashes.
So, what happens if we define and import the following module? *)
Module OtherFoo.
Definition foo := true.
End OtherFoo.
Import OtherFoo.
(** First, Coq emits no error or warning, so this is a legit operation.
What is [foo] now? *)
Print foo.
About foo.
(** Our [OtherFoo.foo] identifier has actually [shadowed] [Foo.foo].
Shadowing is not completely correct here. You can sometimes use short names, but they are always resolved to fully qualified names (with the modules).
Théo Winterhalter said:
Shadowing is not completely correct here. You can sometimes use short names, but they are always resolved to fully qualified names (with the modules).
To make this tutorial correct, how would you name the fact that Import
may change the meaning of a short name?
I don't know except explaining that resolution is doing some magic to make names shorter?
Showing Locate
can help.
Thomas Lamiaux said:
I understand. I guess it might just be a question of interface. There is a begin / end in codqoc. Maybe, we could have something similar to hide begin and end of modules in order nor to parasite reading.
I don’t think you should hide the modules. 1) because modules without functors are very easy to understand 2) you can then proof things between ex1.map
and ex2.map
which would not be possible with Reset and like.
Last updated: Oct 13 2024 at 01:02 UTC