Stream: Coq users

Topic: Confusion over hand-rolled Fin


view this post on Zulip Callan McGill (Feb 17 2022 at 03:05):

I have this code (using the HoTT library if that makes a difference):

 Section Fin.

    Definition Fin : forall (n : nat), Type.
    Proof.
      refine (nat_rec _ _ _).
      * exact Empty.
      * intros n' fin_n'. exact (sum fin_n' Unit).
    Defined.

    Definition ex : Fin 3.
    Proof.
      exact (inr tt).

When I try this I get an error about how tt is not a type. Could someone explain what I am doing wrong?

Note: I know it would be better to defined this as an inductive type, I am only doing this for the sake of an exercise.

view this post on Zulip Paolo Giarrusso (Feb 17 2022 at 06:58):

that depends on the actual types of a few constructs in your context, but inr does take 2 type arguments — they’re usually implicit, but maybe not here? About inr. will say. Can you post its result, and the error message from this code?

view this post on Zulip Paolo Giarrusso (Feb 17 2022 at 06:59):

I’m also curious about the output of Print sum. and Print Unit.

view this post on Zulip Callan McGill (Feb 17 2022 at 20:04):

Here is Print sum.:

Inductive sum@{u u0} (A B : Type) : Type :=  inl : A -> (A + B)%type | inr : B -> (A + B)%type

Arguments sum (_ _)%type_scope
Arguments Datatypes.inl {A B}%type_scope _, [_] _ _
Arguments Datatypes.inr {A B}%type_scope _, _ [_] _

Here is Print unit:

Inductive Unit@{} : Type0 :=  tt : Unit

I tried to update based on this info to:

    Definition one : Fin 2.
    Proof.
      About inr.
      exact (@inr Unit (Fin 1) tt).

This tells me the following:

Error:
The term "@inr Unit (Fin 1) tt" has type "Sum (Fin 1) Unit" while it is expected to have type
 "Fin 2".

view this post on Zulip Callan McGill (Feb 17 2022 at 20:07):

Ah, I think I figured out my stupidity, I had re-defined Sum somewhere not in a section

view this post on Zulip Ali Caglayan (Feb 17 2022 at 20:09):

@Callan McGill Are you working on your own development? Use the Locate command to find which sum is being talked about. Note that sum is from the Coq stdlib and Sum is the HoTT one, which is being used in Fin.

view this post on Zulip Ali Caglayan (Feb 17 2022 at 20:10):

Which editor are you using?

view this post on Zulip Callan McGill (Feb 17 2022 at 20:10):

I am using PG in emacs

view this post on Zulip Ali Caglayan (Feb 17 2022 at 20:10):

Are you working in your own project?

view this post on Zulip Ali Caglayan (Feb 17 2022 at 20:11):

You should ideally pass -noinit to coq so that you don't accidentally confuse yourself with the Coq stdlib.

view this post on Zulip Ali Caglayan (Feb 17 2022 at 20:11):

This can be done by having a _CoqProject in your project folder that PG can find

view this post on Zulip Ali Caglayan (Feb 17 2022 at 20:12):

And put these arguments in the _CoqProject as detailed here: https://github.com/HoTT/HoTT#usage

view this post on Zulip Ali Caglayan (Feb 17 2022 at 20:14):

and in HoTT if you want basic stuff, and lemmas about types just do From HoTT Require Import Basics Types. at the top.

view this post on Zulip Callan McGill (Feb 17 2022 at 20:14):

Thanks, the situation is actually worse in that I have -noinit but I stupidly defined my own version of Sum for a particular exercise I was doing :/ It'll teach me for not using Section

view this post on Zulip Gaëtan Gilbert (Feb 17 2022 at 20:15):

how would Section help there?

view this post on Zulip Callan McGill (Feb 17 2022 at 20:15):

I thought if I end the section then it would not be in scope later?

view this post on Zulip Ali Caglayan (Feb 17 2022 at 20:15):

It's fine to define your own Sum, if you use Locate Sum it will show you the full names of all things named Sum

view this post on Zulip Ali Caglayan (Feb 17 2022 at 20:16):

Some will be qualified by the module they live in

view this post on Zulip Callan McGill (Feb 17 2022 at 20:16):

Also, interestingly the original definition still doesn't actually compute how I expect and so I had to use an explicit Fixpoint definition

view this post on Zulip Ali Caglayan (Feb 17 2022 at 20:16):

The HoTT one for example will probably be called HoTT.Basics.Datatypes.Sum

view this post on Zulip Gaëtan Gilbert (Feb 17 2022 at 20:16):

Callan McGill said:

I thought if I end the section then it would not be in scope later?

only for Variables/Context/Hypotheses
not definitions and inductives
you may want Module instead of Section

view this post on Zulip Callan McGill (Feb 17 2022 at 20:17):

Ah good to know, thanks for the information, I am still a beginner


Last updated: Jan 29 2023 at 06:02 UTC