Merge pull request #434 from mattam82/fix-nested-where-principles

Fix nested where principles

examples/_CoqProject

@@ -21,3 +21,4 @@ wfrec.v
 AlmostFull.v
 POPLMark1a.v
 bove_capretta.v
+cartesian.v

examples/cartesian.v

@@ -0,0 +1,51 @@
+(* From an example by Olivier Danvy. *)
+From Equations Require Import Equations.
+From Coq Require Import List.
+
+Set Equations Transparent.
+Import ListNotations.
+
+Section cart.
+   Context {A B : Type}.
+   (* No need to have the eliminator generalize over the A, B parameters *)
+
+   Equations cartesian (v1s_given : list A) (v2s_given : list B) : list (A * B) :=
+   cartesian v1s_given v2s_given := traverse_1 v1s_given
+      where traverse_1 (l : list A) : list (A * B) :=
+      { | [] := []
+         | (v1 :: v1s') := traverse_2 v2s_given 
+            where traverse_2 (l : list B) : list (A * B) by struct l :=
+            | [] := traverse_1 v1s'
+            | (v2 :: v2s') := (v1, v2) :: traverse_2 v2s' }.
+End cart.
+
+Lemma cartesian_spec {A B} (l : list A) (l' : list B) p : 
+   In p (cartesian l l') <-> In (fst p) l /\ In (snd p) l'.
+Proof.
+  revert p. pattern l, l', (cartesian l l').
+  (* The bulk of the proof is here: the two invariants needed on the 
+     two traversals. *)
+  unshelve eapply (cartesian_elim _ 
+   (fun _ l' l r => forall p, In p r <-> In (fst p) l /\ In (snd p) l')
+   (fun _ v2s_given v1 v1s' v2s' r => forall p, In p r <-> (v1 = fst p /\ In (snd p) v2s') \/
+      (In (fst p) v1s' /\ In (snd p) v2s_given))); auto.
+  all:cbn; intros; rewrite ?H; intuition auto; cbn.
+  - noconf H1. intuition auto.
+  - noconf H1. noconf H0. intuition auto.
+Qed.
+
+(* Extraction cartesian. *)
+(*
+(** val cartesian : 'a1 list -> 'a2 list -> ('a1, 'a2) prod list **)
+
+let rec cartesian v1s_given v2s_given =
+  match v1s_given with
+  | Nil -> Nil
+  | Cons (y, l) ->
+	let rec traverse_2 = function
+    | Nil -> cartesian l v2s_given
+    | Cons (y0, l1) -> Cons ((Pair (y, y0)), (traverse_2 l1))
+    in traverse_2 v2s_given
+*)
+Eval compute in cartesian [1; 2] [3; 4].
+

src/g_equations.mlg

@@ -376,13 +376,29 @@ GRAMMAR EXTEND Gram
         in aux l }
     ] ]
   ;
+
+  letconstr:
+    [ [ (*"let"; id=lident; bl = binders; ty = OPT [ ":"; c = Constr.lconstr -> { c } ] ; ":=";
+      c1 = term LEVEL "200"; "in"; c2 = letconstr ->
+      { let ty,c1 = match ty, c1 with
+        | None, { CAst.v = Constrexpr.CCast(c, Glob_term.CastConv t) } -> Some t, c (* Tolerance, see G_vernac.def_body *)
+        | _, _ -> ty, c1 in
+        let (c, (w, wn)) = c2 in
+        let eqn : pre_equation = SignPats 
+          (CAst.make ~loc (Constrexpr.CRef (Libnames.qualid_of_ident ~loc:(fst id) (snd id), None))), 
+          Some (Program (ConstrExpr c1, ([], []))) in
+        let w' : pre_equation where_clause = ((id, None, None, bl, ty, None), [eqn]) in
+        (c, (w' :: w, wn)) } *)
+       c = Constr.lconstr; w = local_wheres -> { (ConstrExpr c, w) }
+  ] ]
+  ;
   rhs:
     [ [ ":=!"; id = identloc -> { Some (Empty id) }
 
-     | [":=" -> { () } |"=>" -> { () } ]; c = Constr.lconstr; w = local_wheres ->
-        { Some (Program (ConstrExpr c, w)) }
+     | [":=" -> { () } |"=>" -> { () } ]; c = letconstr ->
+        { let (ce, w) = c in Some (Program (ce, w)) }
 
-      | ["with" -> { () } ]; refs = refine; [":=" -> { () } |"=>" -> { () } ];
+     | ["with" -> { () } ]; refs = refine; [":=" -> { () } |"=>" -> { () } ];
         e = sub_equations -> { Some (Refine (refs, e)) }
      | -> { None }
     ] ]

src/principles.ml

@@ -618,21 +618,28 @@ let map_proto evd recarg f ty =
   | None -> f
 
 type rec_subst = (Names.Id.t * (int option * EConstr.constr)) list
+let _prsubst env evd s = Pp.(prlist_with_sep spc (fun (id, (recarg, f)) ->
+  str (Id.to_string id) ++ str" -> " ++ Printer.pr_econstr_env env evd f) s)
 
-let cut_problem evd s ctx =
+let cut_problem env evd s ctx =
   (* From Γ, x := t, D |- id_subst (G, x, D) : G, x : _, D
      to oΓ, D[t] |- id_subst (G, D) | G[
      ps, prec, ps' : Δ, rec, Δ',
      and s : prec -> Γ |- t : rec
      build
      Γ |- ps, ps' : Δ, Δ'[prec/rec] *)
+  (* Feedback.msg_debug Pp.(str"cut_problem on " ++ pr_context env evd ctx);
+  Feedback.msg_debug Pp.(str"with substitution " ++ prsubst env evd s); *)
   let rec fn s (ctxl, pats, ctxr as ctxm) =
     match s with
     | [] -> ctxm
     | (id, (recarg, term)) :: s ->
       try
         let rel, _, ty = Termops.lookup_rel_id id ctxr in
         let fK = map_proto evd recarg term (lift rel ty) in
+        (* Feedback.msg_debug Pp.(str"subst_in_ctx " ++ int rel ++ str" by " ++ 
+          Printer.pr_econstr_env (push_rel_context ctxr env) evd fK ++ str " in " ++
+          pr_context env evd ctxr); *)
         let ctxr' = subst_in_ctx rel fK ctxr in
         let left, right = CList.chop (pred rel) pats in
         let right' = List.tl right in
@@ -645,13 +652,13 @@ let subst_rec env evd cutprob s (ctx, p, _ as lhs) =
   let subst =
     List.fold_left (fun (ctx, pats, ctx' as lhs') (id, (recarg, b)) ->
     try let rel, _, ty = Termops.lookup_rel_id id ctx in
-       (* Feedback.msg_debug Pp.(str"lhs': " ++ pr_context_map env evd lhs');       *)
-        let fK = map_proto evd recarg (mapping_constr evd lhs b) (lift rel ty) in
+        (* Feedback.msg_debug Pp.(str"lhs': " ++ pr_context_map env evd lhs'); *)
+        let fK = map_proto evd recarg (mapping_constr evd lhs' (mapping_constr evd lhs b)) (lift rel ty) in
         (* Feedback.msg_debug Pp.(str"fk: " ++ Printer.pr_econstr_env (push_rel_context ctx env) evd fK); *)
         let substf = single_subst env evd rel (PInac fK) ctx in
         (* ctx[n := f] |- _ : ctx *)
         let substctx = compose_subst env ~sigma:evd substf lhs' in
-        (* Feedback.msg_debug Pp.(str"substituted context: " ++ pr_context_map env evd substctx);  *)
+        (* Feedback.msg_debug Pp.(str"substituted context: " ++ pr_context_map env evd substctx); *)
         substctx
     with Not_found (* lookup *) -> lhs') (id_subst ctx) s
   in
@@ -743,13 +750,10 @@ let push_decls_map env evd (ctx : context_map) cut (g : rel_context) =
   let map, _ = List.fold_right (fun decl acc -> push_mapping_context env evd decl acc) g (ctx, cut) in
   check_ctx_map env evd map
 
-let _prsubst env evd s = Pp.(prlist_with_sep spc (fun (id, (recarg, f)) ->
-     str (Id.to_string id) ++ str" -> " ++ Printer.pr_econstr_env env !evd f) s)
-
 let subst_rec_programs env evd ps =
   let where_map = ref PathMap.empty in
   let evd = ref evd in
-  let cut_problem s ctx' = cut_problem !evd s ctx' in
+  let cut_problem s ctx' = cut_problem env !evd s ctx' in
   let subst_rec cutprob s lhs = subst_rec env !evd cutprob s lhs in
   let rec subst_programs path s ctxlen progs oterms =
     let fixsubst =
@@ -769,19 +773,20 @@ let subst_rec_programs env evd ps =
     let lifts = List.map (fun (id, (recarg, b)) ->
         (id, (recarg, lift (List.length fixsubst) b))) s in
     let s' = fixsubst @ lifts in
-    (* Feedback.msg_debug Pp.(str"In subst_programs, pr_substs" ++ prsubst env evd s'); *)
+    (* Feedback.msg_debug Pp.(str"In subst_programs, s' = " ++ prsubst env !evd s'); *)
     let one_program p oterm =
+      (* Feedback.msg_debug Pp.(str"In subst_program, substituting in " ++ Id.print p.program_info.program_id); *)
       let rec_prob, rec_arity =
         match p.program_rec with
         | Some { rec_prob; rec_arity } -> rec_prob, rec_arity
         | None -> p.program_prob, p.program_info.program_arity
       in
       let prog_info = p.program_info in
       let cutprob_sign = cut_problem s prog_info.program_sign in
-      (* Feedback.msg_debug Pp.(str"In subst_programs: " ++ pr_context env !evd prog_info.program_sign);
-       * Feedback.msg_debug Pp.(str"In subst_programs: cutprob_sign " ++ pr_context_map env !evd cutprob_sign); *)
+      (* Feedback.msg_debug Pp.(str"In subst_programs: " ++ pr_context env !evd prog_info.program_sign); *)
+      (* Feedback.msg_debug Pp.(str"In subst_programs: cutprob_sign " ++ pr_context_map env !evd cutprob_sign); *)
       let cutprob_subst, _ = subst_rec cutprob_sign s (id_subst prog_info.program_sign) in
-      (* Feedback.msg_debug Pp.(str"In subst_programs: subst_rec failed " ++ pr_context env !evd prog_info.program_sign); *)
+      (* Feedback.msg_debug Pp.(str"In subst_programs: cutprob_subst " ++ pr_context_map env !evd cutprob_subst); *)
       let program_info' =
         { prog_info with
           program_rec = None;
@@ -791,6 +796,7 @@ let subst_rec_programs env evd ps =
       let program' = { p with program_info = program_info' } in
       let path' = p.program_info.program_id :: path in
       (* Feedback.msg_debug Pp.(str"In subst_programs, cut_problem s'" ++ pr_context env !evd (pi1 rec_prob)); *)
+      (* Feedback.msg_debug Pp.(str"In subst_programs, s'" ++ prsubst env !evd s'); *)
       let rec_cutprob = cut_problem s' (pi1 rec_prob) in
       let splitting' =
           aux rec_cutprob s' program' oterm path' p.program_splitting
@@ -815,20 +821,22 @@ let subst_rec_programs env evd ps =
                         where_type} as w) (subst_wheres, wheres) =
         (* subst_wheres lives in lhs', i.e. has prototypes substituted already *)
         let wcontext = where_context subst_wheres in
-        let cutprob' = cut_problem s (pi3 subst) in
-        (* Feedback.msg_debug Pp.(str"where_context in subst rec : " ++ pr_context env !evd wcontext);
-         * Feedback.msg_debug Pp.(str"lifting subst : " ++ pr_context_map env !evd subst);
+        let wp = where_program in
+        (* Feedback.msg_debug Pp.(str"In aux compute, cut_problem for " ++ Id.print wp.program_info.program_id 
+          ++ prsubst env !evd lhss); *)
+        let cutprob' = cut_problem lhss (pi3 subst) in
+         (* Feedback.msg_debug Pp.(str"lifting subst : " ++ pr_context_map env !evd subst);
          * Feedback.msg_debug Pp.(str"cutprob : " ++ pr_context_map env !evd cutprob'); *)
         let wsubst0 = push_decls_map env !evd subst cutprob' wcontext in
         (* Feedback.msg_debug Pp.(str"new substitution in subst rec : " ++ pr_context_map env !evd wsubst0); *)
         let ctxlen = List.length wcontext + List.length ctx in
-        let wp = where_program in
         let where_type = mapping_constr !evd wsubst0 where_type in
         (* The substituted prototypes must be lifted w.r.t. the new variables bound in this where and
            preceding ones. *)
+        (* Feedback.msg_debug Pp.(str"lifting substitution by " ++ int (List.length (pi1 wp.program_prob) - List.length ctx)); *)
         let s = List.map (fun (id, (recarg, b)) ->
-            (id, (recarg, lift ((* List.length subst_wheres + *)
-                                List.length (pi1 wp.program_prob) - List.length ctx) b))) lhss in
+            (id, (recarg, lift (List.length wp.program_info.program_sign - List.length ctx) b))) lhss in
+        (* let _ = Feedback.msg_debug Pp.(str"new substitution " ++  prsubst env !evd s) in *)
         let wp' =
           match subst_programs path s ctxlen [wp] [where_term w] with
           | [wp'] -> wp'

src/principles.mli

@@ -85,7 +85,7 @@ val unfold_constr : Evd.evar_map -> constr -> Proofview.V82.tac
 
 type rec_subst = (Names.Id.t * (int option * EConstr.constr)) list
 
-val cut_problem :
+val cut_problem : Environ.env ->
   Evd.evar_map -> rec_subst ->
   Equations_common.rel_declaration list ->
   Equations_common.rel_declaration list * Context_map.pat list *

src/splitting.ml

@@ -642,6 +642,11 @@ let term_of_tree env0 isevar sort tree =
       let term = EConstr.it_mkLambda_or_LetIn term ctx in
       let typ = it_mkProd_or_subst env evm ty ctx in
       let term = Evarutil.nf_evar !evd term in
+      if !Equations_common.debug then
+        Feedback.msg_debug (str"type checking case" ++ 
+          Printer.pr_econstr_env env !evd term ++ spc () ++
+          str"of type" ++ spc () ++
+          Printer.pr_econstr_env env !evd typ);
       evd := Typing.check env !evd term typ;
       !evd, term, typ
   in
@@ -697,18 +702,37 @@ let make_program env evd p prob s rec_info =
            [| beta_appvect !evd fn (extended_rel_vect 0 (pi1 lhs)) |] in
        Single (p, prob, rec_info, s, it_mkLambda_or_LetIn term (pi1 lhs))
      | StructRec sr ->
+      if !Equations_common.debug then
+        Feedback.msg_debug (str"term_of_tree for" ++ pr_splitting env !evd s);
        let term, ty = term_of_tree env evd sort s in
        let args = extended_rel_vect 0 r.rec_lets in
+       let args_lets = rel_vect 0 (List.length r.rec_lets) in
+       if !Equations_common.debug then
+        Feedback.msg_debug (str"returned:" ++ Printer.pr_econstr_env env !evd term);
        let term = beta_appvect !evd term args in
+       if !Equations_common.debug then
+        Feedback.msg_debug (str"after beta:" ++ Printer.pr_econstr_env (push_rel_context r.rec_lets env) !evd term);
        let before, after =
          CList.chop r.rec_args r.rec_sign
        in
        let fixdecls, after =
          CList.chop sr.struct_rec_protos after in
-       let subst = List.append (List.map (fun _ -> mkProp) fixdecls) (List.rev (Array.to_list args)) in
+       let subst = List.append (List.map (fun _ -> mkProp) fixdecls) (List.rev (Array.to_list args_lets)) in
        let program_sign = subst_rel_context 0 subst before in
-       let program_arity = substnl subst r.rec_args r.rec_arity in
+       if !Equations_common.debug then
+        Feedback.msg_debug (str"rec_sign:" ++ pr_context env !evd r.rec_sign);
+       if !Equations_common.debug then
+        Feedback.msg_debug (str"program arity:" ++ Printer.pr_econstr_env env !evd r.rec_arity);
+      if !Equations_common.debug then
+        Feedback.msg_debug (str"rec_lets:" ++ pr_context env !evd r.rec_lets);
+      if !Equations_common.debug then
+        Feedback.msg_debug (str"rec_args:" ++ int r.rec_args);
+      let program_arity = substnl subst r.rec_args r.rec_arity in
        let p' = { p with program_sign; program_arity } in
+       if !Equations_common.debug then
+        Feedback.msg_debug (str"program_sign:"  ++ pr_context (push_rel_context after env) !evd program_sign);
+      if !Equations_common.debug then
+        Feedback.msg_debug (str"program arity:" ++ Printer.pr_econstr_env env !evd program_arity);
        let p' =
          match p.program_rec with
          | Some (Structural ann) ->

test-suite/fin.v

@@ -80,7 +80,7 @@ Set Program Mode.
 
 Equations? fin_to_nat_bound {n : nat} (i : fin n) : {m : nat | m < n} :=
 fin_to_nat_bound fz := 0;
-fin_to_nat_bound (fs j) := let (m, p) := fin_to_nat_bound j in (S m).
+fin_to_nat_bound (fs j) with fin_to_nat_bound j := { | (exist _ m p) := (S m) }.
 Proof.
   - apply Le.le_n_S; apply Le.le_0_n.
   - apply Lt.lt_n_S; assumption.