From 45be898cdadf8ba9e83c319c1c9237432a14acc9 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Fr=C3=A9d=C3=A9ric=20Blanqui?= Date: Fri, 19 Jul 2024 14:38:39 +0200 Subject: [PATCH 1/6] fix dk output --- Makefile | 2 +- dkprint.ml | 147 +++++++++++++++++++++++++++++++++++----------------- globals.ml | 2 +- globals.mli | 2 +- lltodk.ml | 17 +++--- lltolp.ml | 14 ++--- lpprint.ml | 12 ++--- main.ml | 4 +- 8 files changed, 128 insertions(+), 72 deletions(-) diff --git a/Makefile b/Makefile index 183facb..7b6132a 100644 --- a/Makefile +++ b/Makefile @@ -41,7 +41,7 @@ SOURCES = log.ml version.ml config.dummy misc.ml heap.ml globals.ml error.ml \ COQSRC = zenon.v zenon_coqbool.v zenon_equiv.v zenon_induct.v zenon_focal.v zenon_arith.v zenon_arith_reals.v -DKSRC = cc.dk dk_bool.dk dk_logic.dk dk_tuple.dk basics_minimal.dk zen.dk zenon_focal.dk +DKSRC = cc.dk dk_bool.dk dk_logic.dk dk_tuple.dk basics_minimal.dk zen.dk zenon_focal.dk zenon.dk DOCSRC = diff --git a/dkprint.ml b/dkprint.ml index 4a353b8..a182b6b 100644 --- a/dkprint.ml +++ b/dkprint.ml @@ -1,10 +1,56 @@ open Printf open Dkterm +(* taken on 19/07/24 from +https://github.com/Deducteam/Dedukti/blob/master/parsing/lexer.mll *) +let forbidden_idents = [ + "(;" + ; ";)" + ; "." + ; "," + ; ":" + ; "==" + ; "[" + ; "]" + ; "{" + ; "}" + ; "(" + ; ")" + ; "-->" + ; "->" + ; "=>" + ; ":=" + ; "Type" + ; "def" + ; "defac" + ; "defacu" + ; "injective" + ; "thm" + ; "private" + ; "require" + ; "assert" + ; "#NAME" + ; "#REQUIRE" + ; "#EVAL" + ; "#INFER" + ; "#CHECK" + ; "#CHECKNOT" + ; "#ASSERT" + ; "#ASSERTNOT" + ; "#PRINT" + ; "#GDT" + ] + +let escape_name s = + let id_regex = Str.regexp "^[a-zA-Z_][a-zA-Z0-9_]*$" in + if Str.string_match id_regex s 0 + && List.for_all ((<>) s) forbidden_idents + then s else "{|" ^ s ^ "|}" + let rec print_dk_type o t = match t with - | Dktypetype -> fprintf o "zen.type" - | Dktypeprop -> fprintf o "zen.prop" + | Dktypetype -> fprintf o "zenon.type" + | Dktypeprop -> fprintf o "zenon.prop" | Dkarrow (l, r) -> begin List.iter (fun x -> fprintf o "%a -> " print_dk_type x) l; @@ -15,21 +61,28 @@ let rec print_dk_type o t = (get_var_newname var) print_dk_type t1 print_dk_type t2 | Dkpi _ -> assert false | Dkproof (t) -> - fprintf o "zen.proof (%a)" print_dk_term t - | t -> fprintf o "zen.term (%a)" print_dk_zentype t + fprintf o "zenon.proof (%a)" print_dk_term t + | t -> fprintf o "zenon.term (%a)" print_dk_zentype t and print_dk_zentype o t = match t with - | Dktypeiota -> fprintf o "zen.iota" + | Dktypeiota -> fprintf o "zenon.iota" | t -> print_dk_term o t and print_dk_cst o t = match t with | "Is_true" -> fprintf o "dk_logic.ebP" | "FOCAL.ifthenelse" -> fprintf o "dk_bool.ite" - | s -> if !Globals.signature_name = "" then fprintf o "%s" s else - if Mltoll.is_meta s then fprintf o "zen.select (zen.iota)" else - fprintf o "%s.%s" !Globals.signature_name s + | s -> + if Mltoll.is_meta s then fprintf o "zenon.select (zenon.iota)" + else + begin + if !Globals.signature_name = "" then fprintf o "%s" (escape_name s) + else fprintf o "%s.%s" !Globals.signature_name (escape_name s); + if !Globals.conjecture <> "" + && not !Globals.check_axiom && Typetptp.is_axiom s then + fprintf o " __negated_conjecture_proof__" + end and print_dk_term o t = match t with @@ -49,164 +102,164 @@ and print_dk_term o t = List.iter (fun x -> fprintf o " (%a)" print_dk_term x) l; (* fprintf o "\n ";*) end - | Dkseq -> fprintf o "zen.seq" + | Dkseq -> fprintf o "zenon.seq" | Dknot (t) -> - fprintf o "zen.not\n (%a)" print_dk_term t + fprintf o "zenon.not\n (%a)" print_dk_term t | Dkand (t1, t2) -> - fprintf o "zen.and\n (%a) (%a)" print_dk_term t1 print_dk_term t2 + fprintf o "zenon.and\n (%a) (%a)" print_dk_term t1 print_dk_term t2 | Dkor (t1, t2) -> - fprintf o "zen.or\n (%a) (%a)" print_dk_term t1 print_dk_term t2 + fprintf o "zenon.or\n (%a) (%a)" print_dk_term t1 print_dk_term t2 | Dkimply (t1, t2) -> - fprintf o "zen.imp\n (%a) (%a)" print_dk_term t1 print_dk_term t2 + fprintf o "zenon.imp\n (%a) (%a)" print_dk_term t1 print_dk_term t2 | Dkequiv (t1, t2) -> - fprintf o "zen.eqv\n (%a) (%a)" print_dk_term t1 print_dk_term t2 + fprintf o "zenon.eqv\n (%a) (%a)" print_dk_term t1 print_dk_term t2 | Dkforall (t1, t2) -> - fprintf o "zen.forall (%a)\n (%a)" print_dk_zentype t1 print_dk_term t2 + fprintf o "zenon.forall (%a)\n (%a)" print_dk_zentype t1 print_dk_term t2 | Dkexists (t1, t2) -> - fprintf o "zen.exists (%a)\n (%a)" print_dk_zentype t1 print_dk_term t2 + fprintf o "zenon.exists (%a)\n (%a)" print_dk_zentype t1 print_dk_term t2 | Dkforalltype (t) -> - fprintf o "zen.foralltype\n (%a)" print_dk_term t + fprintf o "zenon.foralltype\n (%a)" print_dk_term t | Dkexiststype (t) -> - fprintf o "zen.existstype\n (%a)" print_dk_term t - | Dktrue -> fprintf o "zen.True" - | Dkfalse -> fprintf o "zen.False" + fprintf o "zenon.existstype\n (%a)" print_dk_term t + | Dktrue -> fprintf o "zenon.True" + | Dkfalse -> fprintf o "zenon.False" | Dkequal (t1, t2, t3) -> - fprintf o "zen.equal (%a)\n (%a)\n (%a)" + fprintf o "zenon.equal (%a)\n (%a)\n (%a)" print_dk_zentype t1 print_dk_term t2 print_dk_term t3 - | DkRfalse (pr) -> fprintf o "zen.Rfalse\n (%a)" print_dk_term pr - | DkRnottrue (pr) -> fprintf o "zen.Rnottrue\n (%a)" print_dk_term pr + | DkRfalse (pr) -> fprintf o "zenon.Rfalse\n (%a)" print_dk_term pr + | DkRnottrue (pr) -> fprintf o "zenon.Rnottrue\n (%a)" print_dk_term pr | DkRaxiom (p, pr1, pr2) -> - fprintf o "zen.Raxiom\n (%a)\n (%a)\n (%a)\n" + fprintf o "zenon.Raxiom\n (%a)\n (%a)\n (%a)\n" print_dk_term p print_dk_term pr1 print_dk_term pr2 | DkRnoteq (a, t, pr) -> - fprintf o "zen.Rnoteq\n (%a)\n (%a)\n (%a)\n" + fprintf o "zenon.Rnoteq\n (%a)\n (%a)\n (%a)\n" print_dk_zentype a print_dk_term t print_dk_term pr | DkReqsym (a, t, u, pr1, pr2) -> - fprintf o "zen.Reqsym\n (%a)\n (%a)\n (%a)\n (%a)\n (%a)\n" + fprintf o "zenon.Reqsym\n (%a)\n (%a)\n (%a)\n (%a)\n (%a)\n" print_dk_zentype a print_dk_term t print_dk_term u print_dk_term pr1 print_dk_term pr2 | DkRcut (p, pr1, pr2) -> - fprintf o "zen.Rcut\n (%a)\n (%a)\n (%a)\n" + fprintf o "zenon.Rcut\n (%a)\n (%a)\n (%a)\n" print_dk_term p print_dk_term pr1 print_dk_term pr2 | DkRnotnot (p, pr1, pr2) -> - fprintf o "zen.Rnotnot\n (%a)\n (%a)\n (%a)\n" + fprintf o "zenon.Rnotnot\n (%a)\n (%a)\n (%a)\n" print_dk_term p print_dk_term pr1 print_dk_term pr2 | DkRand (p, q, pr1, pr2) -> - fprintf o "zen.Rand\n (%a)\n (%a)\n (%a)\n (%a)\n" + fprintf o "zenon.Rand\n (%a)\n (%a)\n (%a)\n (%a)\n" print_dk_term p print_dk_term q print_dk_term pr1 print_dk_term pr2 | DkRor (p, q, pr1, pr2, pr3) -> - fprintf o "zen.Ror\n (%a)\n (%a)\n (%a)\n (%a)\n (%a)\n" + fprintf o "zenon.Ror\n (%a)\n (%a)\n (%a)\n (%a)\n (%a)\n" print_dk_term p print_dk_term q print_dk_term pr1 print_dk_term pr2 print_dk_term pr3 | DkRimply (p, q, pr1, pr2, pr3) -> - fprintf o "zen.Rimply\n (%a)\n (%a)\n (%a)\n (%a)\n (%a)\n" + fprintf o "zenon.Rimply\n (%a)\n (%a)\n (%a)\n (%a)\n (%a)\n" print_dk_term p print_dk_term q print_dk_term pr1 print_dk_term pr2 print_dk_term pr3 | DkRequiv (p, q, pr1, pr2, pr3) -> - fprintf o "zen.Requiv\n (%a)\n (%a)\n (%a)\n (%a)\n (%a)\n" + fprintf o "zenon.Requiv\n (%a)\n (%a)\n (%a)\n (%a)\n (%a)\n" print_dk_term p print_dk_term q print_dk_term pr1 print_dk_term pr2 print_dk_term pr3 | DkRnotand (p, q, pr1, pr2, pr3) -> - fprintf o "zen.Rnotand\n (%a)\n (%a)\n (%a)\n (%a)\n (%a)\n" + fprintf o "zenon.Rnotand\n (%a)\n (%a)\n (%a)\n (%a)\n (%a)\n" print_dk_term p print_dk_term q print_dk_term pr1 print_dk_term pr2 print_dk_term pr3 | DkRnotor (p, q, pr1, pr2) -> - fprintf o "zen.Rnotor\n (%a)\n (%a)\n (%a)\n (%a)\n" + fprintf o "zenon.Rnotor\n (%a)\n (%a)\n (%a)\n (%a)\n" print_dk_term p print_dk_term q print_dk_term pr1 print_dk_term pr2 | DkRnotimply (p, q, pr1, pr2) -> - fprintf o "zen.Rnotimply\n (%a)\n (%a)\n (%a)\n (%a)\n" + fprintf o "zenon.Rnotimply\n (%a)\n (%a)\n (%a)\n (%a)\n" print_dk_term p print_dk_term q print_dk_term pr1 print_dk_term pr2 | DkRnotequiv (p, q, pr1, pr2, pr3) -> - fprintf o "zen.Rnotequiv\n (%a)\n (%a)\n (%a)\n (%a)\n (%a)\n" + fprintf o "zenon.Rnotequiv\n (%a)\n (%a)\n (%a)\n (%a)\n (%a)\n" print_dk_term p print_dk_term q print_dk_term pr1 print_dk_term pr2 print_dk_term pr3 | DkRex (a, p, pr1, pr2) -> - fprintf o "zen.Rex\n (%a)\n (%a)\n (%a)\n (%a)\n" + fprintf o "zenon.Rex\n (%a)\n (%a)\n (%a)\n (%a)\n" print_dk_zentype a print_dk_term p print_dk_term pr1 print_dk_term pr2 | DkRall (a, p, t, pr1, pr2) -> - fprintf o "zen.Rall\n (%a)\n (%a)\n (%a)\n (%a)\n (%a)\n" + fprintf o "zenon.Rall\n (%a)\n (%a)\n (%a)\n (%a)\n (%a)\n" print_dk_zentype a print_dk_term p print_dk_term t print_dk_term pr1 print_dk_term pr2 | DkRnotex (a, p, t, pr1, pr2) -> - fprintf o "zen.Rnotex\n (%a)\n (%a)\n (%a)\n (%a)\n (%a)\n" + fprintf o "zenon.Rnotex\n (%a)\n (%a)\n (%a)\n (%a)\n (%a)\n" print_dk_zentype a print_dk_term p print_dk_term t print_dk_term pr1 print_dk_term pr2 | DkRnotall (a, p, pr1, pr2) -> - fprintf o "zen.Rnotall\n (%a)\n (%a)\n (%a)\n (%a)\n" + fprintf o "zenon.Rnotall\n (%a)\n (%a)\n (%a)\n (%a)\n" print_dk_zentype a print_dk_term p print_dk_term pr1 print_dk_term pr2 | DkRextype (p, pr1, pr2) -> - fprintf o "zen.Rextype\n (%a)\n (%a)\n (%a)\n" + fprintf o "zenon.Rextype\n (%a)\n (%a)\n (%a)\n" print_dk_term p print_dk_term pr1 print_dk_term pr2 | DkRalltype (p, a, pr1, pr2) -> - fprintf o "zen.Ralltype\n (%a)\n (%a)\n (%a)\n (%a)\n" + fprintf o "zenon.Ralltype\n (%a)\n (%a)\n (%a)\n (%a)\n" print_dk_term p print_dk_zentype a print_dk_term pr1 print_dk_term pr2 | DkRnotextype (p, a, pr1, pr2) -> - fprintf o "zen.Rnotextype\n (%a)\n (%a)\n (%a)\n (%a)\n" + fprintf o "zenon.Rnotextype\n (%a)\n (%a)\n (%a)\n (%a)\n" print_dk_term p print_dk_zentype a print_dk_term pr1 print_dk_term pr2 | DkRnotalltype (p, pr1, pr2) -> - fprintf o "zen.Rnotalltype\n (%a)\n (%a)\n (%a)\n" + fprintf o "zenon.Rnotalltype\n (%a)\n (%a)\n (%a)\n" print_dk_term p print_dk_term pr1 print_dk_term pr2 | DkRsubst (a, p, t1, t2, pr1, pr2, pr3) -> - fprintf o "zen.Rsubst\n (%a)\n (%a)\n (%a)\n (%a)\n (%a)\n (%a)\n (%a)\n" + fprintf o "zenon.Rsubst\n (%a)\n (%a)\n (%a)\n (%a)\n (%a)\n (%a)\n (%a)\n" print_dk_zentype a print_dk_term p print_dk_term t1 @@ -215,7 +268,7 @@ and print_dk_term o t = print_dk_term pr2 print_dk_term pr3 | DkRconglr (a, p, t1, t2, pr1, pr2, pr3) -> - fprintf o "zen.Rconglr\n (%a)\n (%a)\n (%a)\n (%a)\n (%a)\n (%a)\n (%a)\n" + fprintf o "zenon.Rconglr\n (%a)\n (%a)\n (%a)\n (%a)\n (%a)\n (%a)\n (%a)\n" print_dk_zentype a print_dk_term p print_dk_term t1 @@ -224,7 +277,7 @@ and print_dk_term o t = print_dk_term pr2 print_dk_term pr3 | DkRcongrl (a, p, t1, t2, pr1, pr2, pr3) -> - fprintf o "zen.Rcongrl\n (%a)\n (%a)\n (%a)\n (%a)\n (%a)\n (%a)\n (%a)\n" + fprintf o "zenon.Rcongrl\n (%a)\n (%a)\n (%a)\n (%a)\n (%a)\n (%a)\n (%a)\n" print_dk_zentype a print_dk_term p print_dk_term t1 diff --git a/globals.ml b/globals.ml index 3ad0ad6..54e8a08 100644 --- a/globals.ml +++ b/globals.ml @@ -31,7 +31,7 @@ let debug_rwrt = ref false;; let output_sig = ref false;; let signature_name = ref "";; -let neg_conj = ref "";; +let conjecture = ref "";; let check_axiom = ref false;; let begin_comment() = diff --git a/globals.mli b/globals.mli index 6d918d4..f266da4 100644 --- a/globals.mli +++ b/globals.mli @@ -31,7 +31,7 @@ val debug_rwrt : bool ref;; val output_sig : bool ref;; val signature_name : string ref;; -val neg_conj : string ref;; +val conjecture : string ref;; val check_axiom : bool ref;; val begin_comment : unit -> string;; diff --git a/lltodk.ml b/lltodk.ml index d77097f..e5f98e0 100644 --- a/lltodk.ml +++ b/lltodk.ml @@ -1033,7 +1033,7 @@ let output oc phrases llp = let dkname = List.hd name in let prooftree = extract_prooftree llp in let dkproof = make_proof_term (List.hd goal) prooftree in - + fprintf oc "#REQUIRE zenon;\n\n"; if !Globals.signature_name = "" then List.iter (print_line oc) dksigs; fprintf oc "\n"; if !Globals.signature_name = "" then List.iter (print_line oc) dkctx; @@ -1059,9 +1059,14 @@ let output_term oc phrases _ llp = let dkgoal = translate_expr ngoal in let prooftree = extract_prooftree llp in let dkproof = make_proof_term (List.hd goal) prooftree in - if !Globals.signature_name = "" then () else fprintf oc "def delta : zen.proof (%a) \n := \n " print_dk_term dkgoal; - fprintf oc "zen.nnpp (%a)\n\n(%a)" - print_dk_term dkgoal - print_dk_term dkproof; - if !Globals.signature_name = "" then () else fprintf oc "."; + fprintf oc "#REQUIRE zenon.\n"; + if !Globals.signature_name <> "" then + fprintf oc "#REQUIRE %s.\n" !Globals.signature_name; + fprintf oc "\n[] S.%s ↪ " goal_name; + let n = !Globals.conjecture in + if n <> "" then + fprintf oc "__negated_conjecture_proof__ : proof (not %s) =>\n" n; + fprintf oc "zenon.nnpp (%a)\n(%a)" + print_dk_term dkgoal print_dk_term dkproof; + if !Globals.signature_name <> "" then fprintf oc "."; [] diff --git a/lltolp.ml b/lltolp.ml index 83fab8c..ecedbdb 100644 --- a/lltolp.ml +++ b/lltolp.ml @@ -1064,15 +1064,15 @@ let output_term oc phrases _ llp = if !Globals.signature_name <> "" then fprintf oc "require %s as S;\n" !Globals.signature_name; fprintf oc "\nrule S.%s ↪ " goal_name; - let n = !Globals.neg_conj in - if n <> "" then fprintf oc "λ %s,\n" n; + if !Globals.conjecture <> "" then + fprintf oc "λ __negated_conjecture_proof__,"; begin match dkgoal with - | Some g -> fprintf oc "\n nnpp (%a)\n (%a);\n" - print_dk_term g - print_dk_term dkproof - | None -> fprintf oc "\n %a;\n" - print_dk_term dkproof + | Some g -> + fprintf oc "\n nnpp (%a)\n (%a);\n" + print_dk_term g print_dk_term dkproof + | None -> + fprintf oc "\n %a;\n" print_dk_term dkproof end; [] diff --git a/lpprint.ml b/lpprint.ml index 1142c48..9c4b968 100644 --- a/lpprint.ml +++ b/lpprint.ml @@ -79,7 +79,6 @@ let escape_name s = && List.for_all ((<>) s) forbidden_idents then s else "{|" ^ s ^ "|}" - let rec print_dk_type_aux o (t, var_context) = match t with | Dktypetype -> fprintf o "Set" @@ -108,13 +107,14 @@ and print_dk_cst o t = | "Is_true" -> fprintf o "dk_logic.ebP" | "FOCAL.ifthenelse" -> fprintf o "dk_bool.ite" | s -> - if !Globals.signature_name = "" then fprintf o "%s" (escape_name s) - else if Mltoll.is_meta s then fprintf o "select ι" + if Mltoll.is_meta s then fprintf o "select ι" else begin - fprintf o "S.%s" (escape_name s); - if !Globals.neg_conj <> "" && not !Globals.check_axiom - && Typetptp.is_axiom s then fprintf o "%s" !Globals.neg_conj + if !Globals.signature_name = "" then fprintf o "%s" (escape_name s) + else fprintf o "S.%s" (escape_name s); + if !Globals.conjecture <> "" + && not !Globals.check_axiom && Typetptp.is_axiom s then + fprintf o " __negated_conjecture_proof__" end and print_dk_term_aux o (t, var_context) = diff --git a/main.ml b/main.ml index b624342..62e4a4c 100644 --- a/main.ml +++ b/main.ml @@ -182,9 +182,7 @@ let argspec = [ opt_level := 0; Globals.output_lp := true), " print the proof in lambdapi term format"; - "-conj", Arg.Unit (fun () -> Globals.neg_conj := - (* keep space at the beginning *) - " __negated_conjecture__"), + "-conj", Arg.String (fun s -> Globals.conjecture := s), " indicate whether there is an explicit conjecture"; "-check-axiom", Arg.Unit (fun () -> Globals.check_axiom := true), " indicate whether this is a GDV leaf problem"; From 8bcb5608ca645c83698f212288d991271323f4c6 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Fr=C3=A9d=C3=A9ric=20Blanqui?= Date: Fri, 19 Jul 2024 15:32:40 +0200 Subject: [PATCH 2/6] wip --- lltodk.ml | 2 +- zenon.dk | 169 ++++++++++++++++++++++++++++++++++++++++++++++++++++++ 2 files changed, 170 insertions(+), 1 deletion(-) create mode 100644 zenon.dk diff --git a/lltodk.ml b/lltodk.ml index e5f98e0..130fe45 100644 --- a/lltodk.ml +++ b/lltodk.ml @@ -1062,7 +1062,7 @@ let output_term oc phrases _ llp = fprintf oc "#REQUIRE zenon.\n"; if !Globals.signature_name <> "" then fprintf oc "#REQUIRE %s.\n" !Globals.signature_name; - fprintf oc "\n[] S.%s ↪ " goal_name; + fprintf oc "\n[] S.%s --> " goal_name; let n = !Globals.conjecture in if n <> "" then fprintf oc "__negated_conjecture_proof__ : proof (not %s) =>\n" n; diff --git a/zenon.dk b/zenon.dk new file mode 100644 index 0000000..d317209 --- /dev/null +++ b/zenon.dk @@ -0,0 +1,169 @@ +(; propositions ;) +prop : Type. +True : prop. +False : prop. +imp : prop -> prop -> prop. +def not : prop -> prop := p : prop => imp p False. +and : prop -> prop -> prop. +or : prop -> prop -> prop. +def eqv : prop -> prop -> prop := p : prop => q : prop => and (imp p q) (imp q p). + +(; sorts ;) +type : Type. +def iota : type. + +(; interpretation of sorts as types ;) +injective term : type -> Type. + +(; axiom saying that every sort is inhabited ;) +def select : a : type -> term a. + +(; sorted equality and quantifiers ;) +equal : a : type -> term a -> term a -> prop. +forall : a : type -> (term a -> prop) -> prop. +exists : a : type -> (term a -> prop) -> prop. + +(; interpretation of propositions as types ;) +injective proof : prop -> Type. +[p, q] proof (imp p q) --> proof p -> proof q. +[a, p] proof (forall a p) --> x : term a -> proof (p x). + +(; axiom equivalent to the excluded middle ;) +def nnpp : p : prop -> proof (not (not p)) -> proof p. + +(; epsilon ;) +def epsilon : a : type -> p : (term a -> prop) -> term a. +def epsilon_intro : a : type -> p : (term a -> prop) -> proof (exists a p) -> proof (p (epsilon a p)). + +(; Zenon rules ;) + +def Rfalse : proof False -> proof False. + +def Rnottrue : proof (not True) -> proof False. + +def Raxiom : p : prop -> proof p -> proof (not p) -> proof False. + +def Rnoteq : a : type -> t : term a -> proof (not (equal a t t)) -> proof False. + +def Reqsym : a : type -> + t : term a -> + u : term a -> + proof (equal a t u) -> + proof (not (equal a u t)) -> + proof False. + +def Rcut : p : prop -> + (proof p -> proof False) -> + (proof (not p) -> proof False) -> + proof False. + +def Rnotnot : p : prop -> + (proof p -> proof False) -> + proof (not (not p)) -> + proof False. + +def Rand : p : prop -> + q : prop -> + (proof p -> proof q -> proof False) -> + proof (and p q) -> + proof False. + +def Ror : p : prop -> + q : prop -> + (proof p -> proof False) -> + (proof q -> proof False) -> + proof (or p q) -> + proof False. + +def Rimply : p : prop -> + q : prop -> + (proof (not p) -> proof False) -> + (proof q -> proof False) -> + proof (imp p q) -> + proof False. + +def Requiv : p : prop -> + q : prop -> + (proof (not p) -> proof (not q) -> proof False) -> + (proof p -> proof q -> proof False) -> + proof (eqv p q) -> + proof False. + +def Rnotand : p : prop -> + q : prop -> + (proof (not p) -> proof False) -> + (proof (not q) -> proof False) -> + proof (not (and p q)) -> + proof False. + +def Rnotor : p : prop -> + q : prop -> + (proof (not p) -> proof (not q) -> proof False) -> + proof (not (or p q)) -> + proof False. + +def Rnotimply : p : prop -> + q : prop -> + (proof p -> proof (not q) -> proof False) -> + proof (not (imp p q)) -> + proof False. + +def Rnotequiv : p : prop -> + q : prop -> + (proof (not p) -> proof q -> proof False) -> + (proof p -> proof (not q) -> proof False) -> + proof (not (eqv p q)) -> + proof False. + +def Rex : a : type -> + p : (term a -> prop) -> + (t : term a -> proof (p t) -> proof False) -> + proof (exists a p) -> + proof False. + +def Rall : a : type -> + p : (term a -> prop) -> + t : term a -> + (proof (p t) -> proof False) -> + proof (forall a p) -> + proof False. + +def Rnotex : a : type -> + p : (term a -> prop) -> + t : term a -> + (proof (not (p t)) -> proof False) -> + proof (not (exists a p)) -> + proof False. + +def Rnotall : a : type -> + p : (term a -> prop) -> + (t : term a -> proof (not (p t)) -> proof False) -> + proof (not (forall a p)) -> + proof False. + +def Rsubst : a : type -> + p : (term a -> prop) -> + t1 : term a -> + t2 : term a -> + (proof (not (equal a t1 t2)) -> proof False) -> + (proof (p t2) -> proof False) -> + proof (p t1) -> + proof False. + +def Rconglr : a : type -> + p : (term a -> prop) -> + t1 : term a -> + t2 : term a -> + (proof (p t2) -> proof False) -> + proof (p t1) -> + proof (equal a t1 t2) -> + proof False. + +def Rcongrl : a : type -> + p : (term a -> prop) -> + t1 : term a -> + t2 : term a -> + (proof (p t2) -> proof False) -> + proof (p t1) -> + proof (equal a t2 t1) -> + proof False. From 18608bfe32a34fc31fe398315ce1b23b587ed741 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Fr=C3=A9d=C3=A9ric=20Blanqui?= Date: Fri, 19 Jul 2024 15:46:24 +0200 Subject: [PATCH 3/6] wip --- lltodk.ml | 1 + 1 file changed, 1 insertion(+) diff --git a/lltodk.ml b/lltodk.ml index 130fe45..d1c0cbc 100644 --- a/lltodk.ml +++ b/lltodk.ml @@ -1058,6 +1058,7 @@ let output_term oc phrases _ llp = in let dkgoal = translate_expr ngoal in let prooftree = extract_prooftree llp in + let goal_name = (List.hd llp).name in let dkproof = make_proof_term (List.hd goal) prooftree in fprintf oc "#REQUIRE zenon.\n"; if !Globals.signature_name <> "" then From 282a4b5449add45e8874a464c5a4822eef2152dd Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Fr=C3=A9d=C3=A9ric=20Blanqui?= Date: Fri, 19 Jul 2024 16:03:39 +0200 Subject: [PATCH 4/6] wip --- lltodk.ml | 7 +++++-- 1 file changed, 5 insertions(+), 2 deletions(-) diff --git a/lltodk.ml b/lltodk.ml index d1c0cbc..03f6281 100644 --- a/lltodk.ml +++ b/lltodk.ml @@ -1062,8 +1062,11 @@ let output_term oc phrases _ llp = let dkproof = make_proof_term (List.hd goal) prooftree in fprintf oc "#REQUIRE zenon.\n"; if !Globals.signature_name <> "" then - fprintf oc "#REQUIRE %s.\n" !Globals.signature_name; - fprintf oc "\n[] S.%s --> " goal_name; + begin + fprintf oc "#REQUIRE %s.\n" !Globals.signature_name; + fprintf oc "\n[] %s.%s --> " !Globals.signature_name goal_name + end + else fprintf oc "\n[] %s --> " goal_name; let n = !Globals.conjecture in if n <> "" then fprintf oc "__negated_conjecture_proof__ : proof (not %s) =>\n" n; From 5d70d1665bfe2c7470a0e71a93124debb6839244 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Fr=C3=A9d=C3=A9ric=20Blanqui?= Date: Fri, 19 Jul 2024 16:15:57 +0200 Subject: [PATCH 5/6] wip --- lltodk.ml | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/lltodk.ml b/lltodk.ml index 03f6281..8aeaee5 100644 --- a/lltodk.ml +++ b/lltodk.ml @@ -1067,9 +1067,9 @@ let output_term oc phrases _ llp = fprintf oc "\n[] %s.%s --> " !Globals.signature_name goal_name end else fprintf oc "\n[] %s --> " goal_name; - let n = !Globals.conjecture in - if n <> "" then - fprintf oc "__negated_conjecture_proof__ : proof (not %s) =>\n" n; + if !Globals.conjecture <> "" then + fprintf oc "__negated_conjecture_proof__ : \ + zenon.proof (zenon.not Signature.conjecture) =>\n"; fprintf oc "zenon.nnpp (%a)\n(%a)" print_dk_term dkgoal print_dk_term dkproof; if !Globals.signature_name <> "" then fprintf oc "."; From 91d5327f1e2ab54a106b4bb5880520d89d1b5175 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Fr=C3=A9d=C3=A9ric=20Blanqui?= Date: Fri, 19 Jul 2024 16:46:54 +0200 Subject: [PATCH 6/6] wip --- main.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/main.ml b/main.ml index 62e4a4c..4576e2a 100644 --- a/main.ml +++ b/main.ml @@ -182,7 +182,7 @@ let argspec = [ opt_level := 0; Globals.output_lp := true), " print the proof in lambdapi term format"; - "-conj", Arg.String (fun s -> Globals.conjecture := s), + "-conj", Arg.Unit (fun () -> Globals.conjecture := "conjecture"), " indicate whether there is an explicit conjecture"; "-check-axiom", Arg.Unit (fun () -> Globals.check_axiom := true), " indicate whether this is a GDV leaf problem";