## Stream: Coq users

### Topic: Confusion over hand-rolled Fin

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

#### 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?

#### Paolo Giarrusso (Feb 17 2022 at 06:59):

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

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

#### 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

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

#### Ali Caglayan (Feb 17 2022 at 20:10):

Which editor are you using?

#### Callan McGill (Feb 17 2022 at 20:10):

I am using PG in emacs

#### Ali Caglayan (Feb 17 2022 at 20:10):

Are you working in your own project?

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

#### Ali Caglayan (Feb 17 2022 at 20:11):

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

#### Ali Caglayan (Feb 17 2022 at 20:12):

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

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

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

#### Gaëtan Gilbert (Feb 17 2022 at 20:15):

how would Section help there?

#### Callan McGill (Feb 17 2022 at 20:15):

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

#### 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

#### Ali Caglayan (Feb 17 2022 at 20:16):

Some will be qualified by the module they live in

#### 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

#### Ali Caglayan (Feb 17 2022 at 20:16):

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

#### 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

#### Callan McGill (Feb 17 2022 at 20:17):

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

Last updated: Sep 09 2024 at 06:02 UTC