Stream: Coq users

Topic: Redefing a function using the same name


view this post on Zulip Thomas Lamiaux (May 16 2024 at 17:33):

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.

view this post on Zulip Gaëtan Gilbert (May 16 2024 at 17:41):

there is no shadowing for globals

view this post on Zulip Pierre Courtieu (May 16 2024 at 17:53):

you can put each def in a separate module.

view this post on Zulip Thomas Lamiaux (May 16 2024 at 18:28):

Isn't there a tactic or a command to reset the head of the global goal ?

view this post on Zulip Thomas Lamiaux (May 16 2024 at 18:28):

Opening and closing sections wouldn't be very suited

view this post on Zulip Gaëtan Gilbert (May 16 2024 at 20:13):

what's the "global goal"?

view this post on Zulip Thomas Lamiaux (May 16 2024 at 22:33):

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

view this post on Zulip Théo Winterhalter (May 16 2024 at 23:55):

Related discussion: https://github.com/coq-community/vscoq/issues/687

view this post on Zulip Pierre Courtieu (May 18 2024 at 14:50):

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.

view this post on Zulip Karl Palmskog (May 18 2024 at 20:06):

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")

view this post on Zulip Karl Palmskog (May 18 2024 at 20:07):

in fact, when they disabled shadowing they found a "bug" (missing theorem) in one of the bundled theories

view this post on Zulip Thomas Lamiaux (May 18 2024 at 21:50):

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.

view this post on Zulip Emilio Jesús Gallego Arias (May 19 2024 at 09:58):

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.

view this post on Zulip Thomas Lamiaux (May 19 2024 at 14:32):

@Emilio Jesús Gallego Arias From me, it is mostly about pedagogies c.f. https://github.com/Zimmi48/platform-docs

view this post on Zulip Thomas Lamiaux (May 19 2024 at 18:09):

You say there is "there is no shadowing for globals" but about the behaviour described in this tutorial ?

view this post on Zulip Thomas Lamiaux (May 19 2024 at 18:10):

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

view this post on Zulip Théo Winterhalter (May 19 2024 at 18:11):

Shadowing is not completely correct here. You can sometimes use short names, but they are always resolved to fully qualified names (with the modules).

view this post on Zulip Pierre Rousselin (May 20 2024 at 07:13):

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?

view this post on Zulip Théo Winterhalter (May 20 2024 at 14:48):

I don't know except explaining that resolution is doing some magic to make names shorter?

view this post on Zulip Théo Winterhalter (May 20 2024 at 14:49):

Showing Locate can help.

view this post on Zulip Pierre Courtieu (May 20 2024 at 16:25):

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: Jun 13 2024 at 19:02 UTC