Merge PR coq#18106: Fixes coq#5481: support for unification of univer…

…se variables in congruence and f_equal

Reviewed-by: ppedrot
Ack-by: SkySkimmer
Co-authored-by: ppedrot <[email protected]>

doc/changelog/04-tactics/18106-master+fix5481-congruence-polyuniv.rst

@@ -0,0 +1,7 @@
+- **Fixed:**
+  support for reasoning up to polymorphic universe variables in
+  :tacn:`congruence` and :tacn:`f_equal`
+  (`#18106 <https://github.com/coq/coq/pull/18106>`_,
+  fixes `#5481 <https://github.com/coq/coq/issues/5481>`_
+  and `#9979 <https://github.com/coq/coq/issues/9979>`_,
+  by Hugo Herbelin).

plugins/cc/ccalgo.ml

@@ -124,7 +124,7 @@ let family_eq f1 f2 = match f1, f2 with
 
 
 type 'a term =
-    Symb of constr
+    Symb of constr * (* Hash: *) int
   | Product of Sorts.t * Sorts.t
   | Eps of Id.t
   | Appli of 'a * 'a
@@ -156,7 +156,7 @@ struct
 
   let rec term_equal t1 t2 =
     match t1, t2 with
-      | Symb c1, Symb c2 -> eq_constr_nounivs c1 c2
+      | Symb (c1,_), Symb (c2,_) -> eq_constr_nounivs c1 c2
       | Product (s1, t1), Product (s2, t2) -> family_eq s1 s2 && family_eq t1 t2
       | Eps i1, Eps i2 -> Id.equal i1 i2
       | Appli (t1', u1'), Appli (t2', u2') -> term_equal t1'.term t2'.term && term_equal u1'.term u2'.term
@@ -171,7 +171,7 @@ struct
 
   let hash_term t =
     match t with
-    | Symb c -> combine 1 (Constr.hash c)
+    | Symb (_,hash_c) -> combine 1 hash_c
     | Product (s1, s2) -> combine3 2 (Sorts.hash s1) (Sorts.hash s2)
     | Eps i -> combine 3 (Id.hash i)
     | Appli (t1', t2') -> combine3 4 (t1'.hash) (t2'.hash)
@@ -190,7 +190,7 @@ struct
              mkLambda(make_annot _B_ Sorts.Relevant,mkSort(s2),_body_))
 
   let rec constr_of_term = function
-      Symb s -> s
+      Symb (s,_) -> s
     | Product(s1,s2) -> cc_product s1 s2
     | Eps id -> mkVar id
     | Constructor cinfo -> mkConstructU cinfo.ci_constr
@@ -207,7 +207,15 @@ struct
     constr = lazy (constr_of_term t);
     hash = hash_term t }
 
-  let mkSymb s = make (Symb s)
+  let rec drop_univ c =
+    match kind c with
+    | Const (c,_u) -> mkConstU (c,Univ.Instance.empty)
+    | Ind (c,_u) -> mkIndU (c,Univ.Instance.empty)
+    | Construct (c,_u) -> mkConstructU (c,Univ.Instance.empty)
+    | Sort (Type _u) -> mkSort (type1)
+    | _ -> Constr.map drop_univ c
+
+  let mkSymb s = make (Symb (s, Constr.hash (drop_univ s)))
 
   let mkProduct (s1, s2) = make (Product (s1, s2))
 

plugins/cc/ccproof.ml

@@ -152,6 +152,3 @@ let build_proof env sigma uf=
   function
   | `Prove (i,j) -> equal_proof env sigma uf i j
   | `Discr (i,ci,j,cj)-> ind_proof env sigma uf i ci j cj
-
-
-

plugins/cc/cctac.ml

@@ -440,7 +440,7 @@ let cc_tactic depth additional_terms b =
     match sol with
       None -> Tacticals.tclFAIL (str (if b then "simple congruence failed" else "congruence failed"))
     | Some reason ->
-      debug_congruence (fun () -> Pp.str "Goal solved, generating proof ...");
+      Proofview.tclORELSE (debug_congruence (fun () -> Pp.str "Goal solved, generating proof ...");
       match reason with
         Discrimination (i,ipac,j,jpac) ->
         let p=build_proof (Tacmach.pf_env gl) sigma uf (`Discr (i,ipac,j,jpac)) in
@@ -483,7 +483,14 @@ let cc_tactic depth additional_terms b =
         | HeqG id ->
           convert_to_goal_tac id ta tb p
         | HeqnH (ida,idb) ->
-          convert_to_hyp_tac ida ta idb tb p
+          convert_to_hyp_tac ida ta idb tb p)
+      begin function (e, info) -> match e with
+        | Tactics.NotConvertible ->
+          Tacticals.tclFAIL
+            (str (if b then "simple congruence failed" else "congruence failed") ++
+             str " (cannot build a well-typed proof)")
+        | e -> Proofview.tclZERO ~info e
+      end
   end
 
 let id t = mkLambda (make_annot Anonymous Sorts.Relevant, t, mkRel 1)

tactics/tactics.ml

@@ -331,13 +331,11 @@ let convert_gen pb x y =
   Proofview.Goal.enter begin fun gl ->
     match Tacmach.pf_apply (Reductionops.infer_conv ~pb) gl x y with
     | Some sigma -> Proofview.Unsafe.tclEVARS sigma
-    | None ->
-      let info = Exninfo.reify () in
-      Tacticals.tclFAIL ~info (str "Not convertible")
+    | None -> error NotConvertible
     | exception e when CErrors.noncritical e ->
       let _, info = Exninfo.capture e in
       (* FIXME: Sometimes an anomaly is raised from conversion *)
-      Tacticals.tclFAIL ~info (str "Not convertible")
+      error ?loc:(Loc.get_loc info) NotConvertible
 end
 
 let convert x y = convert_gen Conversion.CONV x y

tactics/tactics.mli

@@ -31,6 +31,8 @@ val is_quantified_hypothesis : Id.t -> Proofview.Goal.t -> bool
 
 (** {6 Primitive tactics. } *)
 
+exception NotConvertible
+
 val introduction    : Id.t -> unit Proofview.tactic
 val convert_concl   : cast:bool -> check:bool -> types -> cast_kind -> unit Proofview.tactic
 val convert_hyp     : check:bool -> reorder:bool -> named_declaration -> unit Proofview.tactic

test-suite/bugs/bug_5481.v

@@ -0,0 +1,46 @@
+(* Bug #5481 *)
+
+Set Universe Polymorphism.
+
+Parameter P : Type -> Type -> Prop.
+Parameter A : Type.
+Lemma foo (B : Type) (H : P A B) : P A B.
+Proof.
+  congruence.
+Qed.
+
+(* An example with types hidden behind "match" *)
+
+Parameter b : unit.
+Lemma foo2 (B : Type) (H : (let () := b in P) A B) : (let () := b in P) A B.
+Proof.
+  congruence.
+Qed.
+
+(* Bug #9979, with f_equal *)
+
+Record Map(K V: Type) := {
+  rep: Type;
+  put: rep -> K -> V -> rep;
+}.
+
+Section Test.
+  Universes u1 u2 u3 u4 u5 u6.
+
+  Goal forall K V (M: Map K V) (k: K) (v: V) (m: rep K V M),
+      put@{u1 u2 u3} K V M m k v = put@{u4 u5 u6} K V M m k v.
+  Proof.
+    intros.
+    f_equal.
+  Qed.
+
+End Test.
+
+(* An example with unification of monomorphic universe levels *)
+
+Unset Universe Polymorphism.
+
+Lemma foo3 (B : Type) : Type.
+Proof.
+  congruence.
+Qed.

test-suite/output/unifconstraints.out

@@ -68,3 +68,6 @@ h : P x
 Unable to unify "P x" with "?P x"
 (unable to find a well-typed instantiation for "?P": cannot ensure that
 "nat -> Type" is a subtype of "nat -> Prop").
+File "./output/unifconstraints.v", line 37, characters 5-15:
+The command has indeed failed with message:
+Tactic failure: congruence failed (cannot build a well-typed proof).

test-suite/output/unifconstraints.v

@@ -27,3 +27,13 @@ Unset Printing Existential Instances.
    improve though and succeed) *)
 
 Fail Check fun (P : _ -> Type) (x:nat) (h:P x) => exist _ x (h : P x).
+
+(* A test about universe level unification in congruence *)
+
+Set Universe Polymorphism.
+Section S.
+Polymorphic Universes i j.
+Goal Type@{i} -> (Type@{j} : Type@{i}).
+Fail congruence.
+Abort.
+End S.