Skip to content

Account for redex which unlocks neutral terms in guard condition reduction failures #22142

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
yannl35133 wants to merge 2 commits into
base: master
Choose a base branch
from
+81 −91
Open

Account for redex which unlocks neutral terms in guard condition reduction failures #22142

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
e2b8b22
Account for redex which unlocks neutral terms in guard condition redu…
yannl35133 Jun 18, 2026
b4a9ebf
remove failing tests
yannl35133 Jun 19, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
99 changes: 69 additions & 30 deletions kernel/inductive.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -1205,7 +1205,7 @@ let restrict_spec ?evars env spec p =

(* [filter_stack_domain env spec p] restricts the size information in stack to
what is allowed to enter under a match with predicate p in environment env. *)
let filter_stack_domain stack_element_specif not_subterm ?evars env p stack =
let filter_stack_domain stack_element_specif not_subterm ?nr ?evars env p stack =
let absctx, ar = Term.decompose_lambda_decls p in
let absctxlen = Context.Rel.length absctx in
(* Optimization: if the predicate is not dependent, no restriction is needed
Expand All @@ -1226,7 +1226,7 @@ let filter_stack_domain stack_element_specif not_subterm ?evars env p stack =
let ty, args = decompose_app_list (whd_all ?evars env a) in
let elt = match kind ty with
| Ind ind ->
let spec = stack_element_specif ?evars elt in
let spec = Option.fold_right Subterm.make_internal nr (stack_element_specif ?evars elt) in
if has_constant_parameters env absctxlen (k + List.length ctx) ind args then
spec
else
Expand Down Expand Up @@ -1454,7 +1454,7 @@ let filter_fix_stack_domain ?evars nr decrarg stack nuniformparams =
let uniform, nuniformparams = if nuniformparams = 0 then false, 0 else true, nuniformparams -1 in
let a =
if uniform then a
else if Int.equal i decrarg then SArg (stack_element_specif ?evars a)
else if Int.equal i decrarg then SArg (Subterm.make_internal nr (stack_element_specif ?evars a))
(* We forget the needreduce status of the structural argument here,
since it's checked in [non_absorbed_stack]. *)
else
Expand Down Expand Up @@ -1491,6 +1491,38 @@ let rec reduce_and_contract_cofix ?evars env c =
reduce_and_contract_cofix ?evars env (mkApp (contract_cofix cofix, args))
| _ -> hd, args

type reduce_result =
| Reduce of constr * stack_element list
| HeadRel of int
| HeadStuck
| NoHead

let rec find_neutral_head env c =
match kind c with
| Rel n -> HeadRel n
| Var _ -> NoHead
| Evar _ -> HeadStuck
| Fix _ | CoFix _ -> HeadStuck
| Const (c, _) ->
if Environ.is_symbol env c then NoHead else HeadStuck
| Meta _ -> assert false
| LetIn _ -> assert false (* only whnf terms *)
| Sort _ | Prod _ | Lambda _ | Ind _ | Construct _
| Int _ | Float _ | String _ | Array _ -> assert false
(* only terms allowed in head of elimination *)
| Case (_, _, _, _, _, c, _)
| Cast (c, _, _) | Proj (_, _, c) -> find_neutral_head env c
| App (hd, args) ->
match kind_nocast hd with
| Fix ((recindxs, i), _) ->
if recindxs.(i) < Array.length args then
find_neutral_head env args.(recindxs.(i))
else
HeadStuck
| _ -> find_neutral_head env hd



(* Check if [def] is a guarded fixpoint body with decreasing arg.
given [recpos], the decreasing arguments of each mutually defined
fixpoint. *)
Expand Down Expand Up @@ -1536,8 +1568,8 @@ let check_one_fix ?evars renv recpos trees def =
in
check_rec_call_state renv NoNeedReduce stack rs (fun () ->
match lookup_rel p renv.env with
| LocalAssum _ -> None
| LocalDef (_,c,_) -> Some (lift p c, []))
| LocalAssum _ -> HeadRel p
| LocalDef (_,c,_) -> Reduce (lift p c, []))

| Case (ci, u, pms, ret, iv, c_0, br) -> (* iv ignored: it's just a cache *)
let (ci, (p,_), _iv, c_0, brs) = expand_case renv.env (ci, u, pms, ret, iv, c_0, br) in
Expand All @@ -1548,7 +1580,7 @@ let check_one_fix ?evars renv recpos trees def =
let nr = redex_level rs' in
let c_spec = Subterm.make_internal nr (lazy_subterm_specif ?evars renv [] c_0) in
let case_spec = Subterm.on_branches renv.env ci.ci_ind c_spec in
let stack' = filter_stack_domain stack_element_specif (Lazy.from_val (Subterm.internal nr)) ?evars renv.env p stack in
let stack' = filter_stack_domain stack_element_specif (Lazy.from_val (Subterm.internal nr)) ~nr ?evars renv.env p stack in
let rs' =
Array.fold_left_i (fun k rs' br' ->
let stack_br = push_stack_args (case_spec k) stack' in
Expand All @@ -1559,11 +1591,10 @@ let check_one_fix ?evars renv recpos trees def =
constructor in c_0 (we unfold definitions too) *)
let hd, args = reduce_and_contract_cofix ?evars renv.env c_0 in
match kind hd with
| Construct cstr -> Some (apply_branch cstr (Array.to_list args) ci brs, [])
| Construct cstr -> Reduce (apply_branch cstr (Array.to_list args) ci brs, [])
| CoFix _ | Ind _ | Lambda _ | Prod _ | LetIn _
| Sort _ | Int _ | Float _ | String _ | Array _ -> assert false
| Rel _ | Var _ | Const _ | App _ | Case _ | Fix _
| Proj _ | Cast _ | Meta _ | Evar _ -> None)
| Sort _ | Int _ | Float _ | String _ | Array _ | Meta _ -> assert false
| _ -> find_neutral_head renv.env hd)

(* Enables to traverse Fixpoint definitions in a more intelligent
way, ie, the rule :
Expand All @@ -1584,7 +1615,7 @@ let check_one_fix ?evars renv recpos trees def =
let renv' = push_fix_renv renv recdef in
let nuniformparams = find_uniform_parameters recindxs (List.length stack) bodies in
let bodies = drop_uniform_parameters nuniformparams bodies in
let fix_stack = filter_fix_stack_domain ?evars (redex_level rs) decrArg stack nuniformparams in
let fix_stack = filter_fix_stack_domain ?evars (redex_level rs') decrArg stack nuniformparams in
let fix_stack = if List.length stack > decrArg then List.firstn (decrArg+1) fix_stack else fix_stack in
let stack_this = lift_stack nbodies fix_stack in
let stack_others = lift_stack nbodies (List.firstn nuniformparams fix_stack) in
Expand All @@ -1601,24 +1632,23 @@ let check_one_fix ?evars renv recpos trees def =
check_rec_call_state renv needreduce_fix non_absorbed_stack rs (fun () ->
(* we try hard to reduce the fix away by looking for a
constructor in [decrArg] (we unfold definitions too) *)
if List.length stack <= decrArg then None else
if List.length stack <= decrArg then HeadStuck else
match List.nth stack decrArg with
| SArg _ -> (* A match on the way *) None
| SArg _ -> (* A match on the way *) HeadStuck
| SClosure (_,_,n,recArg) ->
let c = whd_all ?evars renv.env (lift n recArg) in
let hd, _ = decompose_app_list c in
match kind hd with
| Construct _ -> Some (contract_fix fix, absorbed_stack)
| Construct _ -> Reduce (contract_fix fix, absorbed_stack)
| CoFix _ | Ind _ | Lambda _ | Prod _ | LetIn _
| Sort _ | Int _ | Float _ | String _
| Array _ -> assert false
| Rel _ | Var _ | Const _ | App _ | Case _ | Fix _
| Proj _ | Cast _ | Meta _ | Evar _ -> None)
| _ -> find_neutral_head renv.env hd)

| Const (kn,_u as cu) ->
check_rec_call_state renv NoNeedReduce stack rs (fun () ->
if evaluable_constant kn renv.env then Some (constant_value_in renv.env cu, [])
else None)
if evaluable_constant kn renv.env then Reduce (constant_value_in renv.env cu, [])
else if is_symbol renv.env kn then NoHead else HeadStuck)

| Lambda (x,a,b) ->
begin
Expand All @@ -1644,11 +1674,11 @@ let check_one_fix ?evars renv recpos trees def =
let renv' = push_fix_renv renv recdef in
Array.fold_left (fun rs body ->
let needreduce', rs = check_rec_call renv' rs body in
check_rec_call_state renv needreduce' stack rs (fun _ -> None))
check_rec_call_state renv needreduce' stack rs (fun () -> HeadStuck))
rs bodies

| Ind _ | Construct _ ->
check_rec_call_state renv NoNeedReduce stack rs (fun () -> None)
check_rec_call_state renv NoNeedReduce stack rs (fun () -> HeadStuck)

| Proj (p, _, c) ->
begin
Expand All @@ -1658,19 +1688,18 @@ let check_one_fix ?evars renv recpos trees def =
constructor in c (we unfold definitions too) *)
let hd, args = reduce_and_contract_cofix ?evars renv.env c in
match kind hd with
| Construct _ -> Some (args.(Projection.npars p + Projection.arg p), [])
| Construct _ -> Reduce (args.(Projection.npars p + Projection.arg p), [])
| CoFix _ | Ind _ | Lambda _ | Prod _ | LetIn _
| Sort _ | Int _ | Float _ | String _ | Array _ -> assert false
| Rel _ | Var _ | Const _ | App _ | Case _ | Fix _
| Proj _ | Cast _ | Meta _ | Evar _ -> None)
| _ -> find_neutral_head renv.env hd)
end

| Var id ->
check_rec_call_state renv NoNeedReduce stack rs (fun () ->
let open! Context.Named.Declaration in
match lookup_named id renv.env with
| LocalAssum _ -> None
| LocalDef (_,c,_) -> Some (c, []))
| LocalAssum _ -> NoHead
| LocalDef (_,c,_) -> Reduce (c, []))

| LetIn (x,c,t,b) ->
let needreduce_c, rs = check_rec_call renv rs c in
Expand Down Expand Up @@ -1724,24 +1753,34 @@ let check_one_fix ?evars renv recpos trees def =
end
| _ -> illformed ()

and check_rec_call_state renv needreduce_of_head stack rs expand_head =
and check_rec_call_state renv needreduce_of_head stack rs (expand_head : unit -> reduce_result) =
(* Test if either the head or the stack of a state
needs the state to be reduced before continuing checking *)
match needreduce_of_head ||| needreduce_of_stack stack with
| NoNeedReduce -> rs
| NeedReduce _ as e ->
| NeedReduce (env, err) ->
(* Expand if possible, otherwise, last chance, propagate need
for expansion, in the hope to be eventually erased *)
match expand_head () with
| None -> e :: List.tl rs
| Some (c, stack') -> check_rec_call_stack renv (stack'@stack) rs c
| Reduce (c, stack') -> check_rec_call_stack renv (stack'@stack) rs c
| HeadRel n ->
begin match subterm_var n renv with
| Vars l -> set_need_reduce env l err rs
| DeadCode -> set_need_reduce_top env err rs
| NotSubterm | Subterm (_, _, _) -> raise (FixGuardError (env, err))
end
| HeadStuck -> set_need_reduce_top env err rs
| NoHead -> raise (FixGuardError (env, err))

(* | None -> e :: List.tl rs
| Some (c, stack') -> check_rec_call_stack renv (stack'@stack) rs c *)

and check_inert_subterm_rec_call renv rs c =
(* Check rec calls of a term which does not interact with its
immediate context and which can be possibly erased at higher
level of the redex stack *)
let need_reduce, rs = check_rec_call renv rs c in
check_rec_call_state renv need_reduce [] rs (fun () -> None)
check_rec_call_state renv need_reduce [] rs (fun () -> HeadStuck)

and check_rec_call renv rs c =
(* either fails if a non guarded call occurs or tells if there is
Expand Down
12 changes: 12 additions & 0 deletions test-suite/bugs/bug_22141.v
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,12 @@
Fail Fixpoint rec a (x : nat) {struct x} :=
let _ : nat := a (rec a) in
0.

Fail Fixpoint rec a x {struct x} :=
let _ :=
match a with
| 0 => 0
| S n => rec a n
end
in
0.
61 changes: 0 additions & 61 deletions test-suite/success/Fixpoint.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -292,19 +292,6 @@ Fixpoint f n :=

End NestedRedexesWithCofix.

Module NestedApplicationsWithVariables.

Section S.
Variable h : (nat -> nat) -> nat.
Fixpoint f n :=
match n with
| 0 => 0
| S p => (fun _ => 0) (h f)
end.
End S.

End NestedApplicationsWithVariables.

Module NestedApplicationsWithParameters.

Parameter h : (nat -> nat) -> nat.
Expand All @@ -316,29 +303,6 @@ Fixpoint f n :=

End NestedApplicationsWithParameters.

Module NestedApplicationsWithLocalVariables.

Fixpoint f (h:(nat->nat)->nat) n :=
match n with
| 0 => 0
| S p => (fun _ => 0) (h (f h))
end.

End NestedApplicationsWithLocalVariables.

Module NestedApplicationsWithProjections.

Set Primitive Projections.
Record R := { field : (nat -> nat) -> nat }.

Fixpoint f x n :=
match n with
| 0 => 0
| S p => (fun _ => 0) (x.(field) (f x))
end.

End NestedApplicationsWithProjections.

Module NestedRedexesWithFix.

Fixpoint f n :=
Expand All @@ -347,35 +311,10 @@ Fixpoint f n :=
| S p => (fun _ => 0) ((fix h k (q:nat) {struct q} := k) f)
end.

(* inner fix fully applied with a match subterm *)
Fixpoint f' n :=
match n with
| 0 => 0
| S p => (fun _ => 0) ((fix h k (q:nat) {struct q} := k) f' p)
end.

(* inner fix fully applied with an arbitrary term *)
Fixpoint f'' o n :=
match n with
| 0 => 0
| S p => (fun _ => 0) ((fix h k (q:nat) {struct q} := k o) f'' o)
end.

End NestedRedexesWithFix.

Module NestedRedexesWithMatch.

Fixpoint f o n :=
match n with
| 0 => 0
| S p => (fun _ => 0) (match o with tt => f o end)
end.

Fixpoint f' o n :=
match n with
| 0 => 0
| S p => (fun _ => 0) ((match o with tt => fun x => x o end) f')
end.

End NestedRedexesWithMatch.

Expand Down
Loading