From 2384f06bfb5c2200d7f03431ea03b9b1b4412ec6 Mon Sep 17 00:00:00 2001 From: Quentin Vermande Date: Thu, 7 Nov 2024 10:25:46 +0100 Subject: [PATCH 1/5] rm problematic variables under evars for evar instantiation + shelve new variable when instantiating old shelved variable with the new one in `evarsolve/instantiate_evar` --- .../user-overlays/19822-Tragicus-evd-inst.sh | 1 + pretyping/evarsolve.ml | 18 ++++++++++++++++++ test-suite/bugs/bug_3209.v | 6 ++++-- 3 files changed, 23 insertions(+), 2 deletions(-) create mode 100644 dev/ci/user-overlays/19822-Tragicus-evd-inst.sh diff --git a/dev/ci/user-overlays/19822-Tragicus-evd-inst.sh b/dev/ci/user-overlays/19822-Tragicus-evd-inst.sh new file mode 100644 index 000000000000..947658052a54 --- /dev/null +++ b/dev/ci/user-overlays/19822-Tragicus-evd-inst.sh @@ -0,0 +1 @@ +overlay hott https://github.com/Tragicus/Coq-HoTT rocq19822 19822 diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml index 24f4c3a9e9b2..85d73cf07acd 100644 --- a/pretyping/evarsolve.ml +++ b/pretyping/evarsolve.ml @@ -1586,6 +1586,10 @@ let instantiate_evar unify flags env evd evk body = let allowed_evars = AllowedEvars.remove evk flags.allowed_evars in let flags = { flags with allowed_evars } in let evd' = check_evar_instance unify flags env evd evk body in + let evd' = try + let evk' = fst (EConstr.destEvar evd' (fst (EConstr.decompose_app evd' body))) in + if List.mem evk (Evd.shelf evd') then Evd.shelve evd' [evk'] else evd' + with DestKO -> evd' in Evd.define evk body evd' (* We try to instantiate the evar assuming the body won't depend @@ -1760,6 +1764,20 @@ let rec invert_definition unify flags choose imitate_defs map_constr_with_full_binders env' !evdref (fun d (env,k) -> push_rel d env, k+1) imitate envk t with _ -> progress := p; imitate envk (whd_beta env' !evdref t)) + | App (f, args) when EConstr.isEvar !evdref f -> + progress := true; + (* Tries to imitate the arguments. If this fails, i is Some i' with i' the index of the last argument we fail to imitate *) + let i, args' = Array.fold_left_map_i (fun i k a -> + try let a' = imitate envk a in (k, a') + with ex -> (Some i, a)) None args in + (match i with + | None -> + let f' = imitate envk f in + if f' == f && Array.for_all2 (==) args args' then t else EConstr.mkApp (f', args') + | Some i -> + let args, args' = Array.chop (i+1) args in + let evd, e = Evardefine.evar_absorb_arguments env !evdref (EConstr.destEvar !evdref f) (Array.to_list args) in + evdref := evd; imitate envk (EConstr.mkApp (EConstr.mkEvar e, args'))) | _ -> progress := true; match diff --git a/test-suite/bugs/bug_3209.v b/test-suite/bugs/bug_3209.v index b4075086d0b2..3435cbf04935 100644 --- a/test-suite/bugs/bug_3209.v +++ b/test-suite/bugs/bug_3209.v @@ -27,9 +27,11 @@ Axiom bar : forall (A : Prop) (P : foo A -> Prop), (A -> P (Foo A)) -> Prop. (* This used to fail with a Not_found, we fail more graciously but a heuristic could be implemented, e.g. in some smart occur-check - function, to find a solution of then form ?P := fun _ => ?P' *) + function, to find a solution of then form ?P := fun _ => ?P' -Fail Check (fun e : ?[T] => bar ?[A] ?[P] (fun g : ?[A'] => g e)). + Well, now we do.*) + +Check (fun e : ?[T] => bar ?[A] ?[P] (fun g : ?[A'] => g e)). (* This works and tells which solution we could have inferred *) From bd84e9d5642c4c4fe574cabbe3d4908851c3824a Mon Sep 17 00:00:00 2001 From: Quentin Vermande Date: Mon, 13 Oct 2025 11:33:29 +0200 Subject: [PATCH 2/5] overlays --- dev/ci/user-overlays/21180-Tragicus-evd-inst.sh | 3 +++ 1 file changed, 3 insertions(+) create mode 100644 dev/ci/user-overlays/21180-Tragicus-evd-inst.sh diff --git a/dev/ci/user-overlays/21180-Tragicus-evd-inst.sh b/dev/ci/user-overlays/21180-Tragicus-evd-inst.sh new file mode 100644 index 000000000000..8e47b3518412 --- /dev/null +++ b/dev/ci/user-overlays/21180-Tragicus-evd-inst.sh @@ -0,0 +1,3 @@ +overlay hott https://github.com/Tragicus/Coq-HoTT rocq19822 21180 +overlay argosy https://github.com/Tragicus/argosy rocq21180 21180 +overlay iris https://gitlab.mpi-sws.org/Tragicus/iris rocq21180 21180 From 800cec86ff9c68b9e2a80b385e081826305b209c Mon Sep 17 00:00:00 2001 From: Quentin Vermande Date: Tue, 21 Oct 2025 12:36:08 +0200 Subject: [PATCH 3/5] rm iris overlay --- dev/ci/user-overlays/21180-Tragicus-evd-inst.sh | 1 - 1 file changed, 1 deletion(-) diff --git a/dev/ci/user-overlays/21180-Tragicus-evd-inst.sh b/dev/ci/user-overlays/21180-Tragicus-evd-inst.sh index 8e47b3518412..efadc636f6e0 100644 --- a/dev/ci/user-overlays/21180-Tragicus-evd-inst.sh +++ b/dev/ci/user-overlays/21180-Tragicus-evd-inst.sh @@ -1,3 +1,2 @@ overlay hott https://github.com/Tragicus/Coq-HoTT rocq19822 21180 overlay argosy https://github.com/Tragicus/argosy rocq21180 21180 -overlay iris https://gitlab.mpi-sws.org/Tragicus/iris rocq21180 21180 From 4019ef09eb46bb9d5186f29a11945893e266a551 Mon Sep 17 00:00:00 2001 From: Quentin Vermande Date: Thu, 13 Nov 2025 16:23:42 +0100 Subject: [PATCH 4/5] changelog --- doc/changelog/14-misc/21180-evd-inst-Changed.rst | 4 ++++ 1 file changed, 4 insertions(+) create mode 100644 doc/changelog/14-misc/21180-evd-inst-Changed.rst diff --git a/doc/changelog/14-misc/21180-evd-inst-Changed.rst b/doc/changelog/14-misc/21180-evd-inst-Changed.rst new file mode 100644 index 000000000000..2bf5f08feab7 --- /dev/null +++ b/doc/changelog/14-misc/21180-evd-inst-Changed.rst @@ -0,0 +1,4 @@ +- **Changed:** + Rocq can now instantiate an evar `?a` with a term of the form `?b x` where `x` is not in the scope of `?a`. This allows unifying, e.g. `forall x : ?T, f (?a x)` with `forall _ : ?T, ?b`. In particular, it makes every tactic more powerful + (`#21180 `_, + by Quentin Vermande). From 1157d3d08650b4a36e9ab202f0d01eaa41d64975 Mon Sep 17 00:00:00 2001 From: Quentin Vermande Date: Mon, 27 Apr 2026 14:25:35 +0200 Subject: [PATCH 5/5] unimath overlay --- dev/ci/user-overlays/19822-Tragicus-evd-inst.sh | 1 + 1 file changed, 1 insertion(+) diff --git a/dev/ci/user-overlays/19822-Tragicus-evd-inst.sh b/dev/ci/user-overlays/19822-Tragicus-evd-inst.sh index 947658052a54..af0980e7999f 100644 --- a/dev/ci/user-overlays/19822-Tragicus-evd-inst.sh +++ b/dev/ci/user-overlays/19822-Tragicus-evd-inst.sh @@ -1 +1,2 @@ overlay hott https://github.com/Tragicus/Coq-HoTT rocq19822 19822 +overlay unimath https://github.com/Tragicus/UniMath rocq19822 19822