From 58d209fe36e37b6c0ee4acd702dac333388b1b88 Mon Sep 17 00:00:00 2001 From: Jasper Hugunin Date: Sat, 6 Jan 2018 16:37:06 +0900 Subject: Use let-in aware prod_applist_assum in dtauto and firstorder. Fixes #6490. `prod_applist_assum` is copied from `kernel/term.ml` to `engine/termops.ml`, and adjusted to work with econstr. This change uncovered a bug in `Hipattern.match_with_nodep_ind`, where `has_nodep_prod_after` counts both products and let-ins, but was only being passed `mib.mind_nparams`, which does not count let-ins. Replaced with (Context.Rel.length mib.mind_params_ctxt). --- engine/termops.ml | 12 ++++++++++ engine/termops.mli | 7 ++++++ plugins/firstorder/formula.ml | 3 ++- tactics/hipattern.ml | 54 +++++++++++++++++++++++-------------------- test-suite/bugs/closed/6490.v | 4 ++++ 5 files changed, 54 insertions(+), 26 deletions(-) create mode 100644 test-suite/bugs/closed/6490.v diff --git a/engine/termops.ml b/engine/termops.ml index a71bdff31e..40b3d0d8b6 100644 --- a/engine/termops.ml +++ b/engine/termops.ml @@ -1463,6 +1463,18 @@ let prod_applist sigma c l = | _ -> anomaly (Pp.str "Not enough prod's.") in app [] c l +let prod_applist_assum sigma n c l = + let open EConstr in + let rec app n subst c l = + if Int.equal n 0 then + if l == [] then Vars.substl subst c + else anomaly (Pp.str "Not enough arguments.") + else match EConstr.kind sigma c, l with + | Prod(_,_,c), arg::l -> app (n-1) (arg::subst) c l + | LetIn(_,b,_,c), _ -> app (n-1) (Vars.substl subst b::subst) c l + | _ -> anomaly (Pp.str "Not enough prod/let's.") in + app n [] c l + (* Combinators on judgments *) let on_judgment f j = { uj_val = f j.uj_val; uj_type = f j.uj_type } diff --git a/engine/termops.mli b/engine/termops.mli index c1600abe80..1f4c85054d 100644 --- a/engine/termops.mli +++ b/engine/termops.mli @@ -159,8 +159,15 @@ val eta_reduce_head : Evd.evar_map -> constr -> constr (** Flattens application lists *) val collapse_appl : Evd.evar_map -> constr -> constr +(** [prod_applist] [forall (x1:B1;...;xn:Bn), B] [a1...an] @return [B[a1...an]] *) val prod_applist : Evd.evar_map -> constr -> constr list -> constr +(** In [prod_applist_assum n c args], [c] is supposed to have the + form [∀Γ.c] with [Γ] of length [m] and possibly with let-ins; it + returns [c] with the assumptions of [Γ] instantiated by [args] and + the local definitions of [Γ] expanded. *) +val prod_applist_assum : Evd.evar_map -> int -> constr -> constr list -> constr + (** Remove recursively the casts around a term i.e. [strip_outer_cast (Cast (Cast ... (Cast c, t) ... ))] is [c]. *) val strip_outer_cast : Evd.evar_map -> constr -> constr diff --git a/plugins/firstorder/formula.ml b/plugins/firstorder/formula.ml index c55040df03..4c59996aa7 100644 --- a/plugins/firstorder/formula.ml +++ b/plugins/firstorder/formula.ml @@ -55,7 +55,8 @@ let ind_hyps env sigma nevar ind largs = let types= Inductiveops.arities_of_constructors env ind in let myhyps t = let t = EConstr.of_constr t in - let t1=Termops.prod_applist sigma t largs in + let nparam_decls = Context.Rel.length (fst (Global.lookup_inductive (fst ind))).mind_params_ctxt in + let t1=Termops.prod_applist_assum sigma nparam_decls t largs in let t2=snd (decompose_prod_n_assum sigma nevar t1) in fst (decompose_prod_assum sigma t2) in Array.map myhyps types diff --git a/tactics/hipattern.ml b/tactics/hipattern.ml index a3a3e0a9e9..11ac166801 100644 --- a/tactics/hipattern.ml +++ b/tactics/hipattern.ml @@ -111,7 +111,8 @@ let match_with_one_constructor sigma style onlybinary allow_rec t = Some (hdapp,args) else None else - let ctyp = Termops.prod_applist sigma (EConstr.of_constr mip.mind_nf_lc.(0)) args in + let ctyp = Termops.prod_applist_assum sigma (Context.Rel.length mib.mind_params_ctxt) + (EConstr.of_constr mip.mind_nf_lc.(0)) args in let cargs = List.map RelDecl.get_type (prod_assum sigma ctyp) in if not (is_lax_conjunction style) || has_nodep_prod sigma ctyp then (* Record or non strict conjunction *) @@ -364,36 +365,39 @@ let is_forall_term sigma c = op2bool (match_with_forall_term sigma c) let match_with_nodep_ind sigma t = let (hdapp,args) = decompose_app sigma t in - match EConstr.kind sigma hdapp with - | Ind (ind, _) -> - let (mib,mip) = Global.lookup_inductive ind in - if Array.length (mib.mind_packets)>1 then None else - let nodep_constr c = has_nodep_prod_after mib.mind_nparams sigma (EConstr.of_constr c) in - if Array.for_all nodep_constr mip.mind_nf_lc then - let params= - if Int.equal mip.mind_nrealargs 0 then args else - fst (List.chop mib.mind_nparams args) in - Some (hdapp,params,mip.mind_nrealargs) - else - None - | _ -> None + match EConstr.kind sigma hdapp with + | Ind (ind, _) -> + let (mib,mip) = Global.lookup_inductive ind in + if Array.length (mib.mind_packets)>1 then None else + let nodep_constr c = + has_nodep_prod_after (Context.Rel.length mib.mind_params_ctxt) sigma (EConstr.of_constr c) in + if Array.for_all nodep_constr mip.mind_nf_lc then + let params= + if Int.equal mip.mind_nrealargs 0 then args else + fst (List.chop mib.mind_nparams args) in + Some (hdapp,params,mip.mind_nrealargs) + else + None + | _ -> None let is_nodep_ind sigma t = op2bool (match_with_nodep_ind sigma t) let match_with_sigma_type sigma t = let (hdapp,args) = decompose_app sigma t in match EConstr.kind sigma hdapp with - | Ind (ind, _) -> - let (mib,mip) = Global.lookup_inductive ind in - if Int.equal (Array.length (mib.mind_packets)) 1 && - (Int.equal mip.mind_nrealargs 0) && - (Int.equal (Array.length mip.mind_consnames)1) && - has_nodep_prod_after (mib.mind_nparams+1) sigma (EConstr.of_constr mip.mind_nf_lc.(0)) then - (*allowing only 1 existential*) - Some (hdapp,args) - else - None - | _ -> None + | Ind (ind, _) -> + let (mib,mip) = Global.lookup_inductive ind in + if Int.equal (Array.length (mib.mind_packets)) 1 + && (Int.equal mip.mind_nrealargs 0) + && (Int.equal (Array.length mip.mind_consnames)1) + && has_nodep_prod_after (Context.Rel.length mib.mind_params_ctxt + 1) sigma + (EConstr.of_constr mip.mind_nf_lc.(0)) + then + (*allowing only 1 existential*) + Some (hdapp,args) + else + None + | _ -> None let is_sigma_type sigma t = op2bool (match_with_sigma_type sigma t) diff --git a/test-suite/bugs/closed/6490.v b/test-suite/bugs/closed/6490.v new file mode 100644 index 0000000000..dcf9ff29ed --- /dev/null +++ b/test-suite/bugs/closed/6490.v @@ -0,0 +1,4 @@ +Inductive Foo (A' := I) (B : Type) := foo : Foo B. + +Goal Foo True. dtauto. Qed. +Goal Foo True. firstorder. Qed. -- cgit v1.2.3 From 92bc1c642c2bf9001b86c71bb26f3e73011d02a7 Mon Sep 17 00:00:00 2001 From: Jasper Hugunin Date: Wed, 10 Jan 2018 17:13:44 +0900 Subject: Add a test that `prod_applist_assum` reduces the right number of let-ins --- engine/termops.mli | 5 ++++- test-suite/success/dtauto-let-deps.v | 24 ++++++++++++++++++++++++ 2 files changed, 28 insertions(+), 1 deletion(-) create mode 100644 test-suite/success/dtauto-let-deps.v diff --git a/engine/termops.mli b/engine/termops.mli index 1f4c85054d..a3559a693b 100644 --- a/engine/termops.mli +++ b/engine/termops.mli @@ -165,7 +165,10 @@ val prod_applist : Evd.evar_map -> constr -> constr list -> constr (** In [prod_applist_assum n c args], [c] is supposed to have the form [∀Γ.c] with [Γ] of length [m] and possibly with let-ins; it returns [c] with the assumptions of [Γ] instantiated by [args] and - the local definitions of [Γ] expanded. *) + the local definitions of [Γ] expanded. + Note that [n] counts both let-ins and prods, while the length of [args] + only counts prods. In other words, varying [n] changes how many + trailing let-ins are expanded. *) val prod_applist_assum : Evd.evar_map -> int -> constr -> constr list -> constr (** Remove recursively the casts around a term i.e. diff --git a/test-suite/success/dtauto-let-deps.v b/test-suite/success/dtauto-let-deps.v new file mode 100644 index 0000000000..094b2f8b3c --- /dev/null +++ b/test-suite/success/dtauto-let-deps.v @@ -0,0 +1,24 @@ +(* +This test is sensitive to changes in which let-ins are expanded when checking +for dependencies in constructors. +If the (x := X) is not reduced, Foo1 won't be recognized as a conjunction, +and if the (y := X) is reduced, Foo2 will be recognized as a conjunction. + +This tests the behavior of engine/termops.ml : prod_applist_assum, +which is currently specified to reduce exactly the parameters. + +If dtauto is changed to reduce lets in constructors before checking dependency, +this test will need to be changed. +*) + +Context (P Q : Type). +Inductive Foo1 (X : Type) (x := X) := foo1 : let y := X in P -> Q -> Foo1 x. +Inductive Foo2 (X : Type) (x := X) := foo2 : let y := X in P -> Q -> Foo2 y. + +Goal P -> Q -> Foo1 nat. +solve [dtauto]. +Qed. + +Goal P -> Q -> Foo2 nat. +Fail solve [dtauto]. +Abort. -- cgit v1.2.3 From 7f60ab72facdee620467c0c48c914273f70aa96f Mon Sep 17 00:00:00 2001 From: Jasper Hugunin Date: Wed, 17 Jan 2018 14:55:28 +0900 Subject: Add CHANGES entry --- CHANGES | 2 ++ 1 file changed, 2 insertions(+) diff --git a/CHANGES b/CHANGES index ead751147a..818a66e9c6 100644 --- a/CHANGES +++ b/CHANGES @@ -40,6 +40,8 @@ Tactics - Added tactic optimize_heap, analogous to the Vernacular Optimize Heap, which performs a major garbage collection and heap compaction in the OCaml run-time system. +- The tactics "dtauto", "dintuition", "firstorder" now handle inductive types + with let bindings in the parameters. Vernacular Commands -- cgit v1.2.3