Merge PR #10758: Fix #10757: Program Fixpoint uses "exists" for telescopes

Reviewed-by: mattam82

4 files changed, 99 insertions, 13 deletions

diff --git a/doc/changelog/02-specification-language/10758-fix-10757.rst b/doc/changelog/02-specification-language/10758-fix-10757.rst
new file mode 100644
index 0000000000..4cce26aedc
--- /dev/null
+++ b/doc/changelog/02-specification-language/10758-fix-10757.rst
@@ -0,0 +1,5 @@
+- ``Program Fixpoint`` now uses ``ex`` and ``sig`` to make telescopes
+  involving ``Prop`` types (`#10758
+  <https://github.com/coq/coq/pull/10758>`_, by Gaëtan Gilbert, fixing
+  `#10757 <https://github.com/coq/coq/issues/10757>`_ reported by
+  Xavier Leroy).
diff --git a/test-suite/bugs/closed/bug_10757.v b/test-suite/bugs/closed/bug_10757.v
new file mode 100644
index 0000000000..a531f6e563
--- /dev/null
+++ b/test-suite/bugs/closed/bug_10757.v
@@ -0,0 +1,38 @@
+Require Import Program Extraction ExtrOcamlBasic.
+Print sig.
+Section FIXPOINT.
+
+Variable A: Type.
+
+Variable eq: A -> A -> Prop.
+Variable beq: A -> A -> bool.
+Hypothesis beq_eq: forall x y, beq x y = true -> eq x y.
+Hypothesis beq_neq: forall x y, beq x y = false -> ~eq x y.
+
+Variable le: A -> A -> Prop.
+Hypothesis le_trans: forall x y z, le x y -> le y z -> le x z.
+
+Definition gt (x y: A) := le y x /\ ~eq y x.
+Hypothesis gt_wf: well_founded gt.
+
+Variable F: A -> A.
+Hypothesis F_mon: forall x y, le x y -> le (F x) (F y).
+
+Program Fixpoint iterate
+    (x: A) (PRE: le x (F x)) (SMALL: forall z, le (F z) z -> le x z)
+    {wf gt x}
+    : {y : A | eq y (F y) /\ forall z, le (F z) z -> le y z } :=
+  let x' := F x in
+  match beq x x' with
+  | true  => x
+  | false => iterate x' _ _
+  end.
+Next Obligation.
+  split.
+- auto.
+- apply beq_neq. auto.
+Qed.
+
+End FIXPOINT.
+
+Recursive Extraction iterate.
diff --git a/theories/Init/Logic.v b/theories/Init/Logic.v
index 09a32e9483..4d84d61f9f 100644
--- a/theories/Init/Logic.v
+++ b/theories/Init/Logic.v
@@ -274,6 +274,22 @@ Inductive ex (A:Type) (P:A -> Prop) : Prop :=
   ex_intro : forall x:A, P x -> ex (A:=A) P.
 
 Register ex as core.ex.type.
+Register ex_intro as core.ex.intro.
+
+Section Projections.
+
+  Variables (A:Prop) (P:A->Prop).
+
+  Definition ex_proj1 (x:ex P) : A :=
+    match x with ex_intro _ a _ => a end.
+
+  Definition ex_proj2 (x:ex P) : P (ex_proj1 x) :=
+    match x with ex_intro _ _ b => b end.
+
+  Register ex_proj1 as core.ex.proj1.
+  Register ex_proj2 as core.ex.proj2.
+
+End Projections.
 
 Inductive ex2 (A:Type) (P Q:A -> Prop) : Prop :=
   ex_intro2 : forall x:A, P x -> Q x -> ex2 (A:=A) P Q.
diff --git a/vernac/comProgramFixpoint.ml b/vernac/comProgramFixpoint.ml
index 3497e6369f..0e17f2b274 100644
--- a/vernac/comProgramFixpoint.ml
+++ b/vernac/comProgramFixpoint.ml
@@ -44,41 +44,68 @@ let mkSubset sigma name typ prop =
 let make_qref s = qualid_of_string s
 let lt_ref = make_qref "Init.Peano.lt"
 
+type family = SPropF | PropF | TypeF
+let family_of_sort_family = let open Sorts in function
+    | InSProp -> SPropF
+    | InProp -> PropF
+    | InSet | InType -> TypeF
+
+let get_sigmatypes sigma ~sort ~predsort =
+  let open EConstr in
+  let which, sigsort = match predsort, sort with
+    | SPropF, _ | _, SPropF ->
+      user_err Pp.(str "SProp arguments not supported by Program Fixpoint yet.")
+    | PropF, PropF -> "ex", PropF
+    | PropF, TypeF -> "sig", TypeF
+    | TypeF, (PropF|TypeF) -> "sigT", TypeF
+  in
+  let sigma, ty = Evarutil.new_global sigma (lib_ref ("core."^which^".type")) in
+  let uinstance = snd (destRef sigma ty) in
+  let intro = mkRef (lib_ref ("core."^which^".intro"), uinstance) in
+  let p1 = mkRef (lib_ref ("core."^which^".proj1"), uinstance) in
+  let p2 = mkRef (lib_ref ("core."^which^".proj2"), uinstance) in
+  sigma, ty, intro, p1, p2, sigsort
+
 let rec telescope sigma l =
   let open EConstr in
   let open Vars in
   match l with
   | [] -> assert false
-  | [LocalAssum (n, t)] ->
+  | [LocalAssum (n, t), _] ->
     sigma, t, [LocalDef (n, mkRel 1, t)], mkRel 1
-  | LocalAssum (n, t) :: tl ->
-      let sigma, ty, tys, (k, constr) =
+  | (LocalAssum (n, t), tsort) :: tl ->
+      let sigma, ty, _tysort, tys, (k, constr) =
         List.fold_left
-          (fun (sigma, ty, tys, (k, constr)) decl ->
+          (fun (sigma, ty, tysort, tys, (k, constr)) (decl,sort) ->
             let t = RelDecl.get_type decl in
             let pred = mkLambda (RelDecl.get_annot decl, t, ty) in
-            let sigma, ty = Evarutil.new_global sigma (lib_ref "core.sigT.type") in
-            let sigma, intro = Evarutil.new_global sigma (lib_ref "core.sigT.intro") in
+            let sigma, ty, intro, p1, p2, sigsort = get_sigmatypes sigma ~predsort:tysort ~sort in
             let sigty = mkApp (ty, [|t; pred|]) in
             let intro = mkApp (intro, [|lift k t; lift k pred; mkRel k; constr|]) in
-              (sigma, sigty, pred :: tys, (succ k, intro)))
-          (sigma, t, [], (2, mkRel 1)) tl
+              (sigma, sigty, sigsort, (pred, p1, p2) :: tys, (succ k, intro)))
+          (sigma, t, tsort, [], (2, mkRel 1)) tl
       in
       let sigma, last, subst = List.fold_right2
-        (fun pred decl (sigma, prev, subst) ->
+        (fun (pred,p1,p2) (decl,_) (sigma, prev, subst) ->
           let t = RelDecl.get_type decl in
-          let sigma, p1 = Evarutil.new_global sigma (lib_ref "core.sigT.proj1") in
-          let sigma, p2 = Evarutil.new_global sigma (lib_ref "core.sigT.proj2") in
           let proj1 = applist (p1, [t; pred; prev]) in
           let proj2 = applist (p2, [t; pred; prev]) in
             (sigma, lift 1 proj2, LocalDef (get_annot decl, proj1, t) :: subst))
         (List.rev tys) tl (sigma, mkRel 1, [])
       in sigma, ty, (LocalDef (n, last, t) :: subst), constr
 
-  | LocalDef (n, b, t) :: tl ->
+  | (LocalDef (n, b, t), _) :: tl ->
     let sigma, ty, subst, term = telescope sigma tl in
     sigma, ty, (LocalDef (n, b, t) :: subst), lift 1 term
 
+let telescope env sigma l =
+  let l, _ = List.fold_right_map (fun d env ->
+      let s = Retyping.get_sort_family_of env sigma (RelDecl.get_type d) in
+      let env = EConstr.push_rel d env in
+      (d, family_of_sort_family s), env) l env
+  in
+  telescope sigma l
+
 let nf_evar_context sigma ctx =
   List.map (map_constr (fun c -> Evarutil.nf_evar sigma c)) ctx
 
@@ -94,7 +121,7 @@ let build_wellfounded (recname,pl,bl,arityc,body) poly r measure notation =
   let top_env = push_rel_context binders_rel env in
   let sigma, top_arity = interp_type_evars ~program_mode:true top_env sigma arityc in
   let full_arity = it_mkProd_or_LetIn top_arity binders_rel in
-  let sigma, argtyp, letbinders, make = telescope sigma binders_rel in
+  let sigma, argtyp, letbinders, make = telescope env sigma binders_rel in
   let argname = Id.of_string "recarg" in
   let arg = LocalAssum (make_annot (Name argname) Sorts.Relevant, argtyp) in
   let binders = letbinders @ [arg] in