Callan McGill (Feb 17 2022 at 03:05): 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.
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".
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: Apr 16 2024 at 18:02 UTC