From 29a3b796c630cb07a8e8972e38e1e45b5facce15 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?George=20P=C3=AErlea?= Date: Tue, 13 Feb 2024 17:15:41 +0800 Subject: [PATCH 1/2] Fix existentially quantified `Nat`s --- Auto/Translation/LamFOL2SMT.lean | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/Auto/Translation/LamFOL2SMT.lean b/Auto/Translation/LamFOL2SMT.lean index 03e9479..9ae01eb 100644 --- a/Auto/Translation/LamFOL2SMT.lean +++ b/Auto/Translation/LamFOL2SMT.lean @@ -297,7 +297,9 @@ def lamQuantified2STerm (forall? : Bool) (s : LamSort) (body : TransM LamAtom ST let dname ← disposableName let mut body' ← body if s == .base .nat then - body' := .qStrApp "=>" #[.qStrApp ">=" #[.bvar 0, .sConst (.num 0)], body'] + body' := match forall? with + | true => .qStrApp "=>" #[.qStrApp ">=" #[.bvar 0, .sConst (.num 0)], body'] + | false => .qStrApp "and" #[.qStrApp ">=" #[.bvar 0, .sConst (.num 0)], body'] match forall? with | true => return .forallE dname s' body' | false => return .existE dname s' body' From b42ec77f38ed0e25f71c9cc578cdbe2c4c81c3b0 Mon Sep 17 00:00:00 2001 From: Yicheng Qian <58621828+PratherConid@users.noreply.github.com> Date: Thu, 15 Feb 2024 21:44:17 +0800 Subject: [PATCH 2/2] minor change --- Auto/Translation/LamFOL2SMT.lean | 5 ++--- 1 file changed, 2 insertions(+), 3 deletions(-) diff --git a/Auto/Translation/LamFOL2SMT.lean b/Auto/Translation/LamFOL2SMT.lean index 9ae01eb..382390a 100644 --- a/Auto/Translation/LamFOL2SMT.lean +++ b/Auto/Translation/LamFOL2SMT.lean @@ -297,9 +297,8 @@ def lamQuantified2STerm (forall? : Bool) (s : LamSort) (body : TransM LamAtom ST let dname ← disposableName let mut body' ← body if s == .base .nat then - body' := match forall? with - | true => .qStrApp "=>" #[.qStrApp ">=" #[.bvar 0, .sConst (.num 0)], body'] - | false => .qStrApp "and" #[.qStrApp ">=" #[.bvar 0, .sConst (.num 0)], body'] + let connective := if forall? then "=>" else "and" + body' := .qStrApp connective #[.qStrApp ">=" #[.bvar 0, .sConst (.num 0)], body'] match forall? with | true => return .forallE dname s' body' | false => return .existE dname s' body'