Merge pull request #800 from JasonGross/8.5pl1

Port HoTT to Coq 8.5pl1

INSTALL.md

@@ -4,7 +4,7 @@ However, the latter cannot be used by people using git to contribute to the libr
 Opam support on windows is experimental.
 [1]: https://github.com/HoTT/HoTT/issues/694
 
-We are compatible with [Coq8.5 beta](https://coq.inria.fr/coq-85), so binary packages can be used. Paths still need to be set manually.
+We are compatible with [Coq 8.5pl1](https://coq.inria.fr/distrib/V8.5pl1/files/), so binary packages can be used. Paths still need to be set manually.
 
 
 # QUICK INSTALLATION INSTRUCTIONS
@@ -39,7 +39,7 @@ minimal fuss, you should try your luck by following these instructions:
 
          dos2unix hoq*
          /usr/bin/find . -name '*.sh' | xargs dos2unix
-        
+
      If you wish to build CoqIDE/hoqide on Windows, we wish you good luck.
 2. Get the HoTT library (skip this step if you already have it):
 
@@ -54,7 +54,7 @@ minimal fuss, you should try your luck by following these instructions:
         make
 
    It may take a while to compile the custom Coq. To speed this up, use `make -jn`, where n is the number of cores you have on your machine.
-   On linux this can be found with `nproc` or `lscpu`. 
+   On linux this can be found with `nproc` or `lscpu`.
    On OSX Apple menu -> About this Mac -> System Report, then look for "number of cores"
 
    If you are using Debian/Ubuntu, and don't mind having HoTT/coq
@@ -288,4 +288,4 @@ option is to type 'M-x customize-variable', then
 'proof-prog-name-ask', to click on the 'Toogle' button in front of
 Proof Prog Name Ask and to save this for future sessions. This will
 prompt PG to ask you for the name of the coq toplevel to be used each
-time you start evaluating a file.
+time you start evaluating a file.

Makefile.am

@@ -185,7 +185,7 @@ checkproofs:
 
 $(STD_VOFILES) : %.vo : %.v coq-HoTT
 	$(VECHO) COQTOP $*
-	$(Q) $(TIMER) etc/pipe_out.sh "$*.timing" "$(COQTOP)" -time -indices-matter -boot -nois -no-native-compiler -coqlib "$(SRCCOQLIB)" -R "$(SRCCOQLIB)/theories" Coq -compile "$*"
+	$(Q) $(TIMER) etc/pipe_out.sh "$*.timing" "$(COQTOP)" -time -indices-matter -boot -nois -coqlib "$(SRCCOQLIB)" -R "$(SRCCOQLIB)/theories" Coq -compile "$*"
 
 
 # The HoTT library as a single target

contrib/HoTTBookExercises.v

@@ -434,10 +434,10 @@ Proof.
     elim (lem hprop _).
     + intro p.
       apply path_hprop; simpl. (* path_prop is silent *)
-      exact ((if_hprop_then_equiv_Unit hprop p)^-1).
+      exact ((if_hprop_then_equiv_Unit hprop p)^-1)%equiv.
     + intro np.
       apply path_hprop; simpl. (* path_prop is silent *)
-      exact ((if_not_hprop_then_equiv_Empty hprop np)^-1).
+      exact ((if_not_hprop_then_equiv_Empty hprop np)^-1)%equiv.
 Defined.
 
 (* ================================================== ex:lem-impred *)

coq/theories/.dir-locals.el

@@ -1,4 +1,4 @@
 ((coq-mode . ((eval . (let ((default-directory (locate-dominating-file
                                                 buffer-file-name ".dir-locals.el")))
                         (make-local-variable 'coq-prog-args)
-                        (setq coq-prog-args `("-no-native-compiler" "-indices-matter" "-boot" "-nois" "-coqlib" ,(expand-file-name "..") "-R" ,(expand-file-name ".") "Coq" "-emacs")))))))
+                        (setq coq-prog-args `("-indices-matter" "-boot" "-nois" "-coqlib" ,(expand-file-name "..") "-R" ,(expand-file-name ".") "Coq" "-emacs")))))))

etc/ci/install_coq.sh

@@ -37,8 +37,8 @@ if [ ! -z "$FORCE_COQ_VERSION" ]
 then
     git checkout "$FORCE_COQ_VERSION" || exit $?
 fi
-echo '$ ./configure -no-native-compiler '"$@"
-./configure -no-native-compiler "$@"
+echo '$ ./configure '"$@"
+./configure "$@"
 echo '$ make coqlight'
 make coqlight
 echo '$ sudo make install-coqlight install-devfiles'

etc/dpdgraph-0.4alpha/graphdepend.ml4

@@ -45,7 +45,7 @@ let is_prop gref = match gref with
         if Term.is_Prop cnst_type then true
         else begin
           try
-            let s = Typing.type_of env Evd.empty cnst_type
+            let s = Typing.unsafe_type_of env Evd.empty cnst_type
             in Term.is_Prop s
           with _ -> false
         end

etc/dpdgraph-0.4alpha/hoqthmdep

@@ -41,4 +41,4 @@ fi
 # or using more evil (but portable) 'eval', do
 # $ eval 'exec "$COQTOP" '"$COQ_ARGS"' "$@"'
 # Instead, we duplicate code, because it's simpler.
-exec "$mythmdepdir/coqthmdep" -no-native-compiler -coqlib "$COQLIB" -R "$HOTTLIB" HoTT -Q "$HOTTCONTRIB" "" -indices-matter "$@"
+exec "$mythmdepdir/coqthmdep" -coqlib "$COQLIB" -R "$HOTTLIB" HoTT -Q "$HOTTCONTRIB" "" -indices-matter "$@"

hoq-config.in

@@ -49,4 +49,4 @@ else
   export HOTTLIB="@hottdir@/theories"
   export HOTTCONTRIB="@hottdir@/contrib"
 fi
-#export COQ_ARGS=(-no-native-compiler -coqlib "$COQLIB" -R "$HOTTLIB" HoTT -Q "$HOTTCONTRIB" "" -indices-matter)
+#export COQ_ARGS=(-coqlib "$COQLIB" -R "$HOTTLIB" HoTT -Q "$HOTTCONTRIB" "" -indices-matter)

hoqc

@@ -46,4 +46,4 @@ fi
 # or using more evil (but portable) 'eval', do
 # $ eval 'exec "$COQC" '"$COQ_ARGS"' "$@"'
 # Instead, we duplicate code, because it's simpler.
-exec "$COQC" -no-native-compiler -coqlib "$COQLIB" -R "$HOTTLIB" HoTT -Q "$HOTTCONTRIB" "" -indices-matter "$@"
+exec "$COQC" -coqlib "$COQLIB" -R "$HOTTLIB" HoTT -Q "$HOTTCONTRIB" "" -indices-matter "$@"

hoqdep

@@ -46,4 +46,4 @@ fi
 # or using more evil (but portable) 'eval', do
 # $ eval 'exec "$COQDEP" '"$COQ_ARGS"' "$@"'
 # Instead, we duplicate code, because it's simpler.
-exec "$COQDEP" -no-native-compiler -coqlib "$COQLIB" -R "$HOTTLIB" HoTT -Q "$HOTTCONTRIB" "" -indices-matter "$@"
+exec "$COQDEP" -coqlib "$COQLIB" -R "$HOTTLIB" HoTT -Q "$HOTTCONTRIB" "" -indices-matter "$@"

hoqide

@@ -46,4 +46,4 @@ fi
 # or using more evil (but portable) 'eval', do
 # $ eval 'exec "$COQIDE" '"$COQ_ARGS"' "$@"'
 # Instead, we duplicate code, because it's simpler.
-exec "$COQIDE" -no-native-compiler -coqlib "$COQLIB" -R "$HOTTLIB" HoTT -Q "$HOTTCONTRIB" "" -indices-matter "$@"
+exec "$COQIDE" -coqlib "$COQLIB" -R "$HOTTLIB" HoTT -Q "$HOTTCONTRIB" "" -indices-matter "$@"

hoqtop

@@ -46,4 +46,4 @@ fi
 # or using more evil (but portable) 'eval', do
 # $ eval 'exec "$COQTOP" '"$COQ_ARGS"' "$@"'
 # Instead, we duplicate code, because it's simpler.
-exec "$COQTOP" -no-native-compiler -coqlib "$COQLIB" -R "$HOTTLIB" HoTT -Q "$HOTTCONTRIB" "" -indices-matter "$@"
+exec "$COQTOP" -coqlib "$COQLIB" -R "$HOTTLIB" HoTT -Q "$HOTTCONTRIB" "" -indices-matter "$@"

hoqtop.byte

@@ -46,4 +46,4 @@ fi
 # or using more evil (but portable) 'eval', do
 # $ eval 'exec "$COQTOP.byte" '"$COQ_ARGS"' "$@"'
 # Instead, we duplicate code, because it's simpler.
-exec "$COQTOP.byte" -no-native-compiler -coqlib "$COQLIB" -R "$HOTTLIB" HoTT -Q "$HOTTCONTRIB" "" -indices-matter "$@"
+exec "$COQTOP.byte" -coqlib "$COQLIB" -R "$HOTTLIB" HoTT -Q "$HOTTCONTRIB" "" -indices-matter "$@"

theories/Algebra/ooGroup.v

@@ -7,6 +7,9 @@ Import TrM.
 
 Local Open Scope path_scope.
 
+(** Keyed unification makes [rewrite !loops_functor_group] take a really long time.  See https://coq.inria.fr/bugs/show_bug.cgi?id=4544 for more discussion. *)
+Local Unset Keyed Unification.
+
 (** * oo-Groups *)
 
 (** We want a workable definition of "oo-group" (what a classical homotopy theorist would call a "grouplike Aoo-space"). The classical definitions using operads or Segal spaces involve infinitely much data, which we don't know how to handle in HoTT. But instead, we can invoke the theorem (which is a theorem in classical homotopy theory, and also in any oo-topos) that every oo-group is the loop space of some pointed connected object, and use it instead as a definition: we define an oo-group to be a pointed connected type (its classifying space or delooping). Then we make subsidiary definitions to allow us to treat such an object in the way we would expect, e.g. an oo-group homomorphism is a pointed map between classifying spaces. *)
@@ -76,7 +79,7 @@ Definition group_loops_functor
            {X Y : pType} (f : pMap X Y)
 : ooGroupHom (group_loops X) (group_loops Y).
 Proof.
-  refine (Build_pMap _ _ _ _); simpl.
+  simple refine (Build_pMap _ _ _ _); simpl.
   - intros [x p].
     exists (f x).
     strip_truncations; apply tr.
@@ -265,7 +268,7 @@ Section Subgroups.
   Definition equiv_coset_subgroup (g : G)
   : { g' : G & in_coset g g'} <~> H.
   Proof.
-    refine (equiv_adjointify _ _ _ _).
+    simple refine (equiv_adjointify _ _ _ _).
     - intros [? [h ?]]; exact h.
     - intros h; exists (incl h^ @ g); exists h; simpl.
       abstract (rewrite inv_pp, grouphom_V, inv_V, concat_p_Vp; reflexivity).

theories/Basics/Overture.v

@@ -16,6 +16,9 @@ Global Set Keyed Unification.
 (** This command makes it so that when defining an [Instance], if you give a term explicitly with [:=], then Coq must be able to fill in all the holes in that term.  This is the same as the behavior of [Definition].  (Without this command, if Coq is unable to fill in all the holes in a term given to an [Instance], it silently drops into interactive proof mode.  This is a source of hard-to-find bugs, and you can always obtain equivalent behavior by beginning an interactive proof with [refine].) *)
 Global Unset Refine Instance Mode.
 
+(** This command makes it so that you don't have to declare universes explicitly when mentioning them in the type.  (Without this command, if you want to say [Definition foo := Type@{i}.], you must instead say [Definition foo@{i} := Type@{i}.]. *)
+Global Unset Strict Universe Declaration.
+
 Definition relation (A : Type) := A -> A -> Type.
 
 Class Reflexive {A} (R : relation A) :=
@@ -72,27 +75,27 @@ Ltac transitivity x := etransitivity x.
 Notation Type0 := Set.
 
 (** Define [Type₁] (really, [Type_i] for any [i > 0]) so that we can enforce having universes that are not [Set].  In trunk, universes will not be unified with [Set] in most places, so we want to never use [Set] at all. *)
-Definition Type1 := Eval hnf in let gt := (Set : Type@{i}) in Type@{i}.
+Definition Type1@{i} := Eval hnf in let gt := (Set : Type@{i}) in Type@{i}.
 Arguments Type1 / .
 Identity Coercion unfold_Type1 : Type1 >-> Sortclass.
 
 (** We also define "the next couple of universes", which are actually an arbitrary universe with another one or two strictly below it.  Note when giving universe annotations to these that their universe parameters appear in order of *decreasing* size. *)
-Definition Type2 := Eval hnf in let gt := (Type1 : Type@{i}) in Type@{i}.
+Definition Type2@{i j} := Eval hnf in let gt := (Type1@{j} : Type@{i}) in Type@{i}.
 Arguments Type2 / .
 Identity Coercion unfold_Type2 : Type2 >-> Sortclass.
 
-Definition Type3 := Eval hnf in let gt := (Type2 : Type@{i}) in Type@{i}.
+Definition Type3@{i j k} := Eval hnf in let gt := (Type2@{j k} : Type@{i}) in Type@{i}.
 Arguments Type3 / .
 Identity Coercion unfold_Type3 : Type3 >-> Sortclass.
 
 (** Along the same lines, here is a universe with an extra universe parameter that's less than or equal to it in size.  The [gt] isn't necessary to force the larger universe to be bigger than [Set] (since we refer to the smaller universe by [Type1] which is already bigger than [Set]), but we include it anyway to make the universe parameters occur again in (now non-strictly) decreasing order. *)
-Definition Type2le := Eval hnf in let gt := (Set : Type@{i}) in
-                                  let ge := ((fun x => x) : Type1 -> Type@{i}) in Type@{i}.
+Definition Type2le@{i j} := Eval hnf in let gt := (Set : Type@{i}) in
+                                        let ge := ((fun x => x) : Type1@{j} -> Type@{i}) in Type@{i}.
 Arguments Type2le / .
 Identity Coercion unfold_Type2le : Type2le >-> Sortclass.
 
-Definition Type3le := Eval hnf in let gt := (Set : Type@{i}) in
-                                  let ge := ((fun x => x) : Type2le@{j k} -> Type@{i}) in Type@{i}.
+Definition Type3le@{i j k} := Eval hnf in let gt := (Set : Type@{i}) in
+                                          let ge := ((fun x => x) : Type2le@{j k} -> Type@{i}) in Type@{i}.
 Arguments Type3le / .
 Identity Coercion unfold_Type3le : Type3le >-> Sortclass.
 
@@ -787,7 +790,7 @@ Ltac revert_opaque x :=
 (** [transparent assert (H : T)] is like [assert (H : T)], but leaves the body transparent. *)
 (** Since binders don't respect [fresh], we use a name unlikely to be reused. *)
 Tactic Notation "transparent" "assert" "(" ident(name) ":" constr(type) ")" :=
-  refine (let __transparent_assert_hypothesis := (_ : type) in _);
+  simple refine (let __transparent_assert_hypothesis := (_ : type) in _);
   [
   | ((* We cannot use the name [__transparent_assert_hypothesis], due to some infelicities in the naming of bound variables.  So instead we pull the bottommost hypothesis. *)
     let H := match goal with H := _ |- _ => constr:(H) end in

theories/Basics/UniverseLevel.v

@@ -5,7 +5,7 @@ Require Import Basics.Overture Basics.PathGroupoids.
 (** We provide casting definitions for raising universe levels. *)
 
 (** Because we have cumulativity (that [T : U@{i}] gives us [T : U@{j}] when [i < j]), we may define [Lift : U@{i} → U@{j}] to be the identity function with a fancy type; the type says that [i < j]. *)
-Definition Lift (A : Type@{i}) : Type@{j}
+Definition Lift@{i j} (A : Type@{i}) : Type@{j}
   := Eval hnf in let enforce_lt := Type@{i} : Type@{j} in A.
 
 Definition lift {A} : A -> Lift A := fun x => x.
@@ -66,44 +66,46 @@ Definition lower_equiv {A B} (e : Equiv (Lift A) (Lift B)) : Equiv A B
 
 (** This version doesn't force strict containment, i.e. it allows the two universes to possibly be the same.  No fancy type is necessary here other than the universe annotations, because of cumulativity. *)
 
-Definition Lift' (A : Type@{i}) : Type@{j} := A.
+Definition Lift'@{i j} (A : Type@{i}) : Type@{j} := A.
 
 (** However, if we don't give the universes as explicit arguments here, then Coq collapses them. *)
-Definition lift' {A : Type@{i}} : A -> Lift'@{i j} A := fun x => x.
+Definition lift'@{i j} {A : Type@{i}} : A -> Lift'@{i j} A := fun x => x.
 
-Definition lower' {A : Type@{i}} : Lift'@{i j} A -> A := fun x => x.
+Definition lower'@{i j} {A : Type@{i}} : Lift'@{i j} A -> A := fun x => x.
 
-Definition lift'2 {A : Type@{i}} {B : A -> Type@{i'}} (f : forall x : A, B x)
+Definition lift'2@{i i' j j'} {A : Type@{i}} {B : A -> Type@{i'}} (f : forall x : A, B x)
 : forall x : Lift'@{i j} A, Lift'@{i' j'} (B (lower' x))
   := f.
 
-Definition lower'2 {A : Type@{i}} {B : A -> Type@{i'}}
+Definition lower'2@{i i' j j'} {A : Type@{i}} {B : A -> Type@{i'}}
            (f : forall x : Lift'@{i j} A, Lift'@{i' j'} (B (lower' x)))
 : forall x : A, B x
   := f.
 
 (** We make [lift] and [lower] opaque so that typeclass resolution doesn't pick up [isequiv_lift] as an instance of [IsEquiv idmap] and wreck havok. *)
 Typeclasses Opaque lift' lower' lift'2 lower'2.
 
-Global Instance isequiv_lift' T : IsEquiv (@lift'@{i j} T)
+Definition isequiv_lift'@{i j} (T : Type@{i}) : IsEquiv (@lift'@{i j} T)
   := @BuildIsEquiv
        _ _
        (@lift' T)
        (@lower' T)
        (fun _ => idpath)
        (fun _ => idpath)
        (fun _ => idpath).
+Global Existing Instance isequiv_lift'. (* work around https://coq.inria.fr/bugs/show_bug.cgi?id=4411 *)
 
-Global Instance isequiv_lift'2 A B : IsEquiv (@lift'2@{i i' j j'} A B)
+Definition isequiv_lift'2@{e0 e1 i i' j j'} (A : Type@{i}) (B : A -> Type@{j}) : IsEquiv@{e0 e1} (@lift'2@{i i' j j'} A B)
   := @BuildIsEquiv
        _ _
        (@lift'2 A B)
        (@lower'2 A B)
        (fun _ => idpath)
        (fun _ => idpath)
        (fun _ => idpath).
+Global Existing Instance isequiv_lift'2. (* work around https://coq.inria.fr/bugs/show_bug.cgi?id=4411 *)
 
-Global Instance lift'_isequiv {A B} (f : A -> B) {H : IsEquiv f} : @IsEquiv (Lift'@{i j} A) (Lift'@{i' j'} B) (lift'2 f)
+Definition lift'_isequiv@{a b i j i' j'}  {A : Type@{a}} {B : Type@{b}} (f : A -> B) {H : IsEquiv f} : @IsEquiv (Lift'@{i j} A) (Lift'@{i' j'} B) (lift'2 f)
   := @BuildIsEquiv
        (Lift' A) (Lift' B)
        (lift'2 f)
@@ -113,8 +115,9 @@ Global Instance lift'_isequiv {A B} (f : A -> B) {H : IsEquiv f} : @IsEquiv (Lif
        (fun x => ((ap (ap lift') (eisadj f (lower' x)))
                     @ (ap_compose f lift' _)^)
                    @ (@ap_compose A (Lift' A) (Lift' B) lift' (lift'2 f) _ _ _)).
+Global Existing Instance lift'_isequiv. (* work around https://coq.inria.fr/bugs/show_bug.cgi?id=4411 *)
 
-Global Instance lower'_isequiv {A B} (f : Lift'@{i j} A -> Lift'@{i' j'} B) {H : IsEquiv f} : @IsEquiv A B (lower'2 f)
+Definition lower'_isequiv@{i j i' j'} {A : Type@{i}} {B : Type@{j}} (f : Lift'@{i j} A -> Lift'@{i' j'} B) {H : IsEquiv f} : @IsEquiv A B (lower'2 f)
   := @BuildIsEquiv
        _ _
        (lower'2 f)
@@ -124,8 +127,9 @@ Global Instance lower'_isequiv {A B} (f : Lift'@{i j} A -> Lift'@{i' j'} B) {H :
        (fun x => ((ap (ap lower') (eisadj f (lift' x)))
                     @ (ap_compose f lower' _)^)
                    @ (@ap_compose (Lift' A) A B lower' (lower'2 f) _ _ _)).
+Global Existing Instance lower'_isequiv. (* work around https://coq.inria.fr/bugs/show_bug.cgi?id=4411 *)
 
-Definition lower'_equiv {A B} (e : Equiv (Lift'@{i j} A) (Lift'@{i' j'} B)) : Equiv A B
+Definition lower'_equiv@{i j i' j'} {A : Type@{i}} {B : Type@{j}} (e : Equiv (Lift'@{i j} A) (Lift'@{i' j'} B)) : Equiv A B
   := @BuildEquiv A B (lower'2 e) _.
 
 (*Fail Check Lift nat : Type0.

theories/Comodalities/CoreflectiveSubuniverse.v

@@ -36,14 +36,14 @@ Section CoreflectiveSubuniverse.
   Proof.
     refine ((fun (g : Y -> F X) => fromF F X o g)^-1 f).
     by apply isequiv_fromF_postcompose.
-  Defined.    
+  Defined.
 
   Definition F_corec_beta {Y X} (YF : inF F Y) (f : Y -> X)
   : fromF F X o F_corec YF f == f.
   Proof.
     apply ap10, (eisretr (fun g => fromF F X o g)).
   Defined.
-  
+
   Definition F_coindpaths {Y X} `(inF F Y) (g h : Y -> F X)
              (p : fromF F X o g == fromF F X o h)
   : g == h.
@@ -85,7 +85,7 @@ Section CoreflectiveSubuniverse.
     - intros ?. apply F_corec; try assumption.
       exact (fun _ => tt).
     - intros f.
-      refine (inF_fromF_sect X _ _).
+      simple refine (inF_fromF_sect X _ _).
       + intros x.
         exact (F_functor (unit_name x) (f x)).
       + intros x; unfold F_functor.
@@ -101,7 +101,7 @@ Section CoOpen.
 
   Definition coOp : CoreflectiveSubuniverse.
   Proof.
-    refine (Build_CoreflectiveSubuniverse
+    simple refine (Build_CoreflectiveSubuniverse
               (fun X => BuildhProp (X -> U))
               (fun X => X * U)
               (fun X => @snd X U)

theories/Constant.v

@@ -112,7 +112,7 @@ Definition cconst_wconst_hset `{Funext} {X Y : Type} (f : X -> Y)
 Proof.
   assert (Ys' : merely X -> IsHSet Y).
   { apply Trunc_rec. intros x; exact (Ys x). }
-  refine (cconst_factors_hprop f (image -1 f) _ _ _).
+  simple refine (cconst_factors_hprop f (image -1 f) _ _ _).
   - apply hprop_allpath; intros [y1 p1] [y2 p2].
     apply path_sigma_hprop; simpl.
     pose proof (Ys' (Trunc_functor -1 pr1 p1)).
@@ -143,7 +143,7 @@ Definition equiv_merely_rec_hset `{Funext} (X Y : Type)
 Proof.
   assert (Ys' : merely X -> IsHSet Y).
   { apply Trunc_rec. intros x; exact (Ys x). }
-  refine (equiv_adjointify
+  simple refine (equiv_adjointify
             (fun fc => @merely_rec_hset _ _ _ fc.1 _ fc.2)
             (fun g => (g o tr ; _)) _ _); try exact _.
   - intros x y; apply (ap g), path_ishprop.

theories/EquivalenceVarieties.v

@@ -357,7 +357,7 @@ Section relational.
       exists (e^-1 b; eisretr e b).
       intros [a H].
       destruct H.
-      refine (path_sigma _ _ _ _ _).
+      simple refine (path_sigma _ _ _ _ _).
       { simpl; apply eissect. }
       { simpl.
         abstract (rewrite eisadj; destruct (eissect e a); reflexivity). } }