From cf915d76a2b2ae94640c27c7486bde51a2f62093 Mon Sep 17 00:00:00 2001
From: Nathan Koskas de Diego <nathan.koskasdediego@cea.fr>
Date: Sat, 26 Mar 2022 16:16:26 +0100
Subject: [PATCH] [qed] bug fixes
---
src/plugins/qed/term.ml | 15 ++++++++-------
1 file changed, 8 insertions(+), 7 deletions(-)
diff --git a/src/plugins/qed/term.ml b/src/plugins/qed/term.ml
index edd6f17443d..77ad2323425 100644
--- a/src/plugins/qed/term.ml
+++ b/src/plugins/qed/term.ml
@@ -2540,15 +2540,16 @@ struct
let xs = match q with
| Lambda -> xs
| Forall | Exists -> List.filter (fun x -> Vars.mem x e.vars) xs
- in
- let xs, xs2 = List.partition_map (fun x ->
+ in (* let_intro_case have to be called sequentially because of cases like
+ '\forall x y, 42 = x + y -> P' where we detect two let-in variables in parralel
+ but we can only simplify one in practice.*)
+ let e, xs = List.fold_left (fun (e, xs') x ->
match let_intro_case q x e with
- | None -> Left x
- | Some v -> Right (x, v)
- ) xs in
- let e = List.fold_right (fun (x, v) e -> e_subst_var x v e) xs2 e in
+ | None -> e, x::xs'
+ | Some v -> e_subst_var x v e, xs'
+ ) (e, []) (List.rev xs) in
let e = lc_close_xs xs e in
- List.fold_right (fun x e -> c_bind q (tau_of_var x) e) xs e
+ List.fold_left (fun e x -> c_bind q (tau_of_var x) e) e (List.rev xs)
let e_forall = bind_xs Forall
let e_exists = bind_xs Exists
--
GitLab