Merge PR #10205: Make discriminate tactic compatible with HoTT

Reviewed-by: Zimmi48
Reviewed-by: mattam82
Reviewed-by: ppedrot

7 files changed, 139 insertions, 34 deletions

diff --git a/doc/changelog/04-tactics/10205-discriminate-HoTT.rst b/doc/changelog/04-tactics/10205-discriminate-HoTT.rst
new file mode 100644
index 0000000000..bb2d2a092e
--- /dev/null
+++ b/doc/changelog/04-tactics/10205-discriminate-HoTT.rst
@@ -0,0 +1,6 @@
+- Make the :tacn:`discriminate` tactic work together with
+  :flag:`Universe Polymorphism` and equality in :g:`Type`. This,
+  in particular, makes :tacn:`discriminate` compatible with the HoTT
+  library https://github.com/HoTT/HoTT.
+  (`#10205 <https://github.com/coq/coq/pull/10205>`_,
+  by Andreas Lynge, review by Pierre-Marie Pédrot and Matthieu Sozeau)
diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml
index 7b286e69dc..e0a31e7dba 100644
--- a/plugins/ltac/rewrite.ml
+++ b/plugins/ltac/rewrite.ml
@@ -946,9 +946,9 @@ let fold_match ?(force=false) env sigma c =
 	  if dep then case_dep_scheme_kind_from_prop
 	  else case_scheme_kind_from_prop
 	else (
-	  if dep
-	  then case_dep_scheme_kind_from_type_in_prop
-	  else case_scheme_kind_from_type)
+          if dep
+          then case_dep_scheme_kind_from_type_in_prop
+          else case_scheme_kind_from_type)
       else ((* sortc <> InProp by typing *)
 	if dep
 	then case_dep_scheme_kind_from_type
diff --git a/plugins/ssr/ssrequality.ml b/plugins/ssr/ssrequality.ml
index dbb0f25abf..91905d277c 100644
--- a/plugins/ssr/ssrequality.ml
+++ b/plugins/ssr/ssrequality.ml
@@ -336,14 +336,14 @@ let pirrel_rewrite ?(under=false) ?(map_redex=id_map_redex) pred rdx rdx_ty new_
   let sigma, p = (* The resulting goal *)
     Evarutil.new_evar env sigma (beta (EConstr.Vars.subst1 new_rdx pred)) in
   let pred = EConstr.mkNamedLambda (make_annot pattern_id Sorts.Relevant) rdx_ty pred in
-  let elim, gl = 
+  let elim, gl =
     let ((kn, i) as ind, _), unfolded_c_ty = pf_reduce_to_quantified_ind gl c_ty in
     let sort = elimination_sort_of_goal gl in
     let elim, gl = pf_fresh_global (Indrec.lookup_eliminator env ind sort) gl in
     if dir = R2L then elim, gl else (* taken from Coq's rewrite *)
     let elim, _ = destConst elim in
     let mp,l = Constant.repr2 (Constant.make1 (Constant.canonical elim)) in
-    let l' = Label.of_id (Nameops.add_suffix (Label.to_id l) "_r")  in 
+    let l' = Label.of_id (Nameops.add_suffix (Label.to_id l) "_r")  in
     let c1' = Global.constant_of_delta_kn (Constant.canonical (Constant.make2 mp l')) in
     mkConst c1', gl in
   let elim = EConstr.of_constr elim in
diff --git a/tactics/elimschemes.ml b/tactics/elimschemes.ml
index 1170c1acd0..8ead050262 100644
--- a/tactics/elimschemes.ml
+++ b/tactics/elimschemes.ml
@@ -59,7 +59,7 @@ let build_induction_scheme_in_type dep sort ind =
   let sigma, pind = Evd.fresh_inductive_instance env sigma ind in
   let sigma, c = build_induction_scheme env sigma pind dep sort in
     c, Evd.evar_universe_context sigma
- 
+
 let rect_scheme_kind_from_type =
   declare_individual_scheme_object "_rect_nodep"
     (fun _ x -> build_induction_scheme_in_type false InType x, Safe_typing.empty_private_constants)
@@ -108,6 +108,16 @@ let sind_scheme_kind_from_prop =
   declare_individual_scheme_object "_sind" ~aux:"_sind_from_prop"
   (fun _ x -> build_induction_scheme_in_type false InSProp x, Safe_typing.empty_private_constants)
 
+let nondep_elim_scheme from_kind to_kind =
+  match from_kind, to_kind with
+  | InProp, InProp  -> ind_scheme_kind_from_prop
+  | InProp, InSProp -> sind_scheme_kind_from_prop
+  | InProp, InSet   -> rec_scheme_kind_from_prop
+  | InProp, InType  -> rect_scheme_kind_from_prop
+  | _     , InProp  -> ind_scheme_kind_from_type
+  | _     , InSProp -> sind_scheme_kind_from_type
+  | _     , InSet   -> rec_scheme_kind_from_type
+  | _     , InType  -> rect_scheme_kind_from_type
 
 (* Case analysis *)
 
diff --git a/tactics/elimschemes.mli b/tactics/elimschemes.mli
index 4472792449..f60e6c137a 100644
--- a/tactics/elimschemes.mli
+++ b/tactics/elimschemes.mli
@@ -33,6 +33,7 @@ val sind_dep_scheme_kind_from_type : individual scheme_kind
 val rec_scheme_kind_from_type : individual scheme_kind
 val rec_dep_scheme_kind_from_type : individual scheme_kind
 
+val nondep_elim_scheme : Sorts.family -> Sorts.family -> individual scheme_kind
 
 (** Case analysis schemes *)
 
diff --git a/tactics/equality.ml b/tactics/equality.ml
index 51eee2a053..ec0876110b 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -352,35 +352,35 @@ let find_elim hdcncl lft2rgt dep cls ot =
       (is_global_exists "core.JMeq.type" hdcncl
        && jmeq_same_dom env sigma ot)) && not dep
   then
-    let c = 
+    let c =
       match EConstr.kind sigma hdcncl with 
-      | Ind (ind_sp,u) -> 
-	let pr1 = 
+      | Ind (ind_sp,u) ->
+        let pr1 =
           lookup_eliminator env ind_sp (elimination_sort_of_clause cls gl)
-	in
+        in
         begin match lft2rgt, cls with
         | Some true, None
         | Some false, Some _ ->
-	  let c1 = destConstRef pr1 in 
+          let c1 = destConstRef pr1 in
           let mp,l = Constant.repr2 (Constant.make1 (Constant.canonical c1)) in
-	  let l' = Label.of_id (add_suffix (Label.to_id l) "_r")  in 
+          let l' = Label.of_id (add_suffix (Label.to_id l) "_r")  in
           let c1' = Global.constant_of_delta_kn (KerName.make mp l') in
-	  begin 
-	    try 
-	      let _ = Global.lookup_constant c1' in
-		c1'
-	    with Not_found -> 
+          begin
+            try
+              let _ = Global.lookup_constant c1' in
+                c1'
+            with Not_found ->
 	      user_err ~hdr:"Equality.find_elim"
                 (str "Cannot find rewrite principle " ++ Label.print l' ++ str ".")
 	  end
-	| _ -> destConstRef pr1
+        | _ -> destConstRef pr1
         end
       | _ -> 
 	  (* cannot occur since we checked that we are in presence of 
 	     Logic.eq or Jmeq just before *)
 	assert false
     in
-        pf_constr_of_global (ConstRef c) 
+        pf_constr_of_global (ConstRef c)
   else
   let scheme_name = match dep, lft2rgt, inccl with
     (* Non dependent case *)
@@ -946,12 +946,12 @@ let build_coq_I () = pf_constr_of_global (lib_ref "core.True.I")
 let rec build_discriminator env sigma true_0 false_0 dirn c = function
   | [] ->
       let ind = get_type_of env sigma c in
-      build_selector env sigma dirn c ind true_0 false_0
+      build_selector env sigma dirn c ind true_0 (fst false_0)
   | ((sp,cnum),argnum)::l ->
       let (cnum_nlams,cnum_env,kont) = descend_then env sigma c cnum in
       let newc = mkRel(cnum_nlams-argnum) in
       let subval = build_discriminator cnum_env sigma true_0 false_0 dirn newc l in
-      kont sigma subval (false_0,mkProp)
+      kont sigma subval false_0
 
 (* Note: discrimination could be more clever: if some elimination is
    not allowed because of a large impredicative constructor in the
@@ -983,25 +983,22 @@ let gen_absurdity id =
           absurd_term=False
 *)
 
-let ind_scheme_of_eq lbeq =
+let ind_scheme_of_eq lbeq to_kind =
   let (mib,mip) = Global.lookup_inductive (destIndRef lbeq.eq) in
-  let kind = inductive_sort_family mip in
+  let from_kind = inductive_sort_family mip in
   (* use ind rather than case by compatibility *)
-  let kind =
-    if kind == InProp then Elimschemes.ind_scheme_kind_from_prop
-    else Elimschemes.ind_scheme_kind_from_type in
+  let kind = Elimschemes.nondep_elim_scheme from_kind to_kind in
   let c, eff = find_scheme kind (destIndRef lbeq.eq) in
     ConstRef c, eff
 
 
-let discrimination_pf e (t,t1,t2) discriminator lbeq =
+let discrimination_pf e (t,t1,t2) discriminator lbeq to_kind =
   build_coq_I () >>= fun i ->
-  build_coq_False () >>= fun absurd_term ->
-  let eq_elim, eff       = ind_scheme_of_eq lbeq in
+  let eq_elim, eff = ind_scheme_of_eq lbeq to_kind in
   Proofview.tclEFFECTS eff <*>
     pf_constr_of_global eq_elim >>= fun eq_elim ->
     Proofview.tclUNIT
-       (applist (eq_elim, [t;t1;mkNamedLambda (make_annot e Sorts.Relevant) t discriminator;i;t2]), absurd_term)
+       (applist (eq_elim, [t;t1;mkNamedLambda (make_annot e Sorts.Relevant) t discriminator;i;t2]))
 
 
 let eq_baseid = Id.of_string "e"
@@ -1018,21 +1015,23 @@ let apply_on_clause (f,t) clause =
 let discr_positions env sigma (lbeq,eqn,(t,t1,t2)) eq_clause cpath dirn =
   build_coq_True () >>= fun true_0 ->
   build_coq_False () >>= fun false_0 ->
+  let false_ty = Retyping.get_type_of env sigma false_0 in
+  let false_kind = Retyping.get_sort_family_of env sigma false_0 in
   let e = next_ident_away eq_baseid (vars_of_env env) in
   let e_env = push_named (Context.Named.Declaration.LocalAssum (make_annot e Sorts.Relevant,t)) env in
   let discriminator =
     try
       Proofview.tclUNIT
-        (build_discriminator e_env sigma true_0 false_0 dirn (mkVar e) cpath)
+        (build_discriminator e_env sigma true_0 (false_0,false_ty) dirn (mkVar e) cpath)
     with
       UserError _ as ex -> Proofview.tclZERO ex
   in
     discriminator >>= fun discriminator ->
-    discrimination_pf e (t,t1,t2) discriminator lbeq >>= fun (pf, absurd_term) ->
-    let pf_ty = mkArrow eqn Sorts.Relevant absurd_term in
+    discrimination_pf e (t,t1,t2) discriminator lbeq false_kind >>= fun pf ->
+    let pf_ty = mkArrow eqn Sorts.Relevant false_0 in
     let absurd_clause = apply_on_clause (pf,pf_ty) eq_clause in
     let pf = Clenvtac.clenv_value_cast_meta absurd_clause in
-    tclTHENS (assert_after Anonymous absurd_term)
+    tclTHENS (assert_after Anonymous false_0)
       [onLastHypId gen_absurdity; (Proofview.V82.tactic (Refiner.refiner ~check:true EConstr.Unsafe.(to_constr pf)))]
 
 let discrEq (lbeq,_,(t,t1,t2) as u) eq_clause =
diff --git a/test-suite/success/Discriminate_HoTT.v b/test-suite/success/Discriminate_HoTT.v
new file mode 100644
index 0000000000..2a5e083d56
--- /dev/null
+++ b/test-suite/success/Discriminate_HoTT.v
@@ -0,0 +1,89 @@
+(* -*- mode: coq; coq-prog-args: ("-noinit" "-indices-matter") -*- *)
+
+(* This file tests the discriminate tactic compatibility with HoTT.
+   The first part of the file will setup a mini HoTT environment.
+   Afterwards a number of tests are performed. The tests are basically
+   copied from the Discriminate.v test file. *)
+
+Unset Elimination Schemes.
+
+Set Universe Polymorphism.
+
+Declare ML Module "ltac_plugin".
+
+Global Set Default Proof Mode "Classic".
+
+Notation "x -> y" := (forall (_:x), y) (at level 99, right associativity, y at level 200).
+
+Cumulative Variant paths {A} (a:A) : A -> Type
+  := idpath : paths a a.
+
+Arguments idpath {A a} , [A] a.
+
+Scheme paths_ind := Induction for paths Sort Type.
+Arguments paths_ind [A] a P f y p.
+
+Notation "x = y :> A" := (@paths A x y) (at level 70, y at next level, no associativity).
+Notation "x = y" := (x = y :>_) (at level 70, no associativity).
+
+Register paths as core.identity.type.
+Register idpath as core.identity.refl.
+Register paths_ind as core.identity.ind.
+
+Definition inverse {A : Type} {x y : A} (p : x = y) : y = x
+  := match p with idpath => idpath end.
+Arguments inverse {A x y} p : simpl nomatch.
+Register inverse as core.identity.sym.
+
+Definition concat {A : Type} {x y z : A} (p : x = y) (q : y = z) : x = z :=
+  match p, q with idpath, idpath => idpath end.
+Arguments concat {A x y z} p q : simpl nomatch.
+Register concat as core.identity.trans.
+
+Definition ap {A B:Type} (f:A -> B) {x y:A} (p:x = y) : f x = f y
+  := match p with idpath => idpath end.
+Arguments ap {A B} f {x y} p.
+Register ap as core.identity.congr.
+
+Variant Empty : Type :=.
+
+Register Empty as core.False.type.
+
+Variant Unit : Type := tt.
+
+Register Unit as core.True.type.
+Register tt as core.True.I.
+
+Variant Bool : Type := true | false.
+
+Inductive nat : Type := O | S (n:nat).
+
+(*********** Test discriminate tactic below. ***************)
+
+Goal O = S O -> Empty.
+ discriminate 1.
+Qed.
+
+Goal forall H : O = S O, H = H.
+ discriminate H.
+Qed.
+
+Goal O = S O -> Unit.
+intros. discriminate H. Qed.
+Goal O = S O -> Unit.
+intros. Ltac g x := discriminate x. g H. Qed.
+
+Goal (forall x y : nat, x = y -> x = S y) -> Unit.
+intros.
+try discriminate (H O) || exact tt.
+Qed.
+
+Goal (forall x y : nat, x = y -> x = S y) -> Unit.
+intros. ediscriminate (H O). instantiate (1:=O). Abort.
+
+(* Check discriminate on types with local definitions *)
+
+Inductive A := B (T := Unit) (x y : Bool) (z := x).
+Goal forall x y, B x true = B y false -> Empty.
+discriminate.
+Qed.