diff --git a/doc/lambdapi.bnf b/doc/lambdapi.bnf index 7b9c40d13..02ef7dbd0 100644 --- a/doc/lambdapi.bnf +++ b/doc/lambdapi.bnf @@ -12,160 +12,3 @@ QID ::= [UID "."]+ UID ::= "assert" | "assertnot" - ::= "require" "open" * ";" - | "require" * ";" - | "require" "as" ";" - | "open" * ";" - | * "symbol" * ":" - [] ";" - | * "symbol" * [":" ] - "≔" ";" - | * * "inductive" ("with" - )* ";" - | "rule" ("with" )* ";" - | "builtin" "≔" ";" - | "coerce_rule" ";" - | "unif_rule" ";" - | "notation" ";" - | ";" - - - ::= * "⊢" ":" - | * "⊢" "≡" - | "compute" - | "print" [] - | "proofterm" - | "debug" ("+"|"-") - | "flag" - | "prover" - | "prover_timeout" - | "verbose" - | "type" - - ::= UID - | QID - - ::= [] "associative" - | "commutative" - | "constant" - | "injective" - | "opaque" - | "private" - | "protected" - | "sequential" - - ::= UID - - ::= - | - - ::= - | - - ::= - | "(" + ":" ")" - | "[" + [":" ] "]" - - ::= - | - | "_" - - ::= - | - | - | "→" - - ::= "`" - | "Π" - | "λ" - | "let" * [":" ] "≔" "in" - - ::= + - - ::= - | "_" - | "TYPE" - | "?" UID [] - | "$" UID [] - | "(" ")" - | "[" "]" - | - - ::= "." "[" [ (";" )*] "]" - - ::= - | - - ::= UID - | QID - - ::= "@" UID - | "@" QID - - ::= + "," - | ":" "," - - ::= - | - | - - ::= "begin" + - | "begin" [] - - ::= "{" [] "}" - - ::= - | ";" - | ";" - - ::= * - - ::= "abort" - | "admitted" - | "end" - - ::= - | "admit" - | "apply" - | "assume" + - | "fail" - | "generalize" - | "have" ":" - | "induction" - | "refine" - | "reflexivity" - | "rewrite" [] [] - | "simplify" [] - | "solve" - | "symmetry" - | "why3" [] - - ::= - | "in" - | "in" "in" - | "in" ["in" ] - | "as" "in" - - ::= "." "[" "]" - - ::= * ":" "≔" ["|"] [ - ("|" )*] - - ::= * ":" - - ::= "↪" - - ::= "↪" "[" (";" - )* "]" - - ::= "≡" - - ::= "infix" [] - | "postfix" - | "prefix" - | "quantifier" - - ::= - | - - diff --git a/src/export/coq.ml b/src/export/coq.ml index c7b86cdf8..4ec830a74 100644 --- a/src/export/coq.ml +++ b/src/export/coq.ml @@ -179,6 +179,7 @@ let rw_patt : p_rw_patt pp = fun ppf p -> let tactic : p_tactic pp = fun ppf { elt; _ } -> begin match elt with + | P_tac_skolem -> out ppf "skolem" | P_tac_admit -> out ppf "admit" | P_tac_apply t -> out ppf "apply %a" term t | P_tac_assume ids -> diff --git a/src/handle/skolem.ml b/src/handle/skolem.ml new file mode 100644 index 000000000..d8947c080 --- /dev/null +++ b/src/handle/skolem.ml @@ -0,0 +1,198 @@ +(** Skolemization tactic. *) + +open Common +open Core open Term +open Fol + +let log = Logger.make 'a' "sklm" "skolemization" +let log = log.pp + +let add_var : ctxt -> tvar -> term -> ctxt = + fun c var typ -> c @ [ (var, typ, None) ] + +(* [new_skolem ss ctx ctr ex_typ] is called when existantial quantifier "∃y" + occurs. [ex_typ] is the type of the quantified variable "y". In order to + eliminate ∃ quantifier, we need to extend signature state [ss] with a + skolem term, represented by a fresh symbol that will later replace the + binded variable "y". Such skolem term may either be a skolem function or a + skolem constant: the type of a skolem term depends on registered variables + in [ctx]. For example, if a set of variables x1:a1, x2:a2,..., xn:an were + previously introduced by an universal quantifier, A skolem term "skt" will + take as arguments x1, ..., xn, and must therefore have type a1 -> a2 -> + ... -> an -> ex_typ. We use a counter [ctr] for naming the generated + symbols. OUT : Updated signature state [upt_sig] is returned, as well as + introduced symbol [symb_skt] and updated counter. *) +let new_skolem : Sig_state.t -> ctxt -> int -> term -> Sig_state.t * sym * int + = fun ss ctx ctr ex_typ -> + let skt_name = "f" ^ string_of_int ctr in + let skt, _ = Ctxt.to_prod ctx ex_typ in + let upt_sig, symb_skt = + Sig_state.add_symbol ss Public Const Eager true (Pos.none skt_name) skt [] + None + in + if Logger.log_enabled () then log "New symbol %a" Print.sym symb_skt; + (upt_sig, symb_skt, ctr + 1) + +(*[Subst_app ctx tb s] builds [f_appl], the application of a symbol [symb_skt] + and a list of variables extracted from context [ctx]. Then, the binded + variable in [tb] is substituted by [f_appl]*) +(*Assumes type of [symb_skt] correspond to variables's types as they are + listed in context [ctx] *) +let subst_app : ctxt -> tbinder -> sym -> term = + fun ctx tb symb_skt -> + (*args_list : [tvar list], are context's variables*) + let args_list = List.map (fun (v, _, _) -> mk_Vari v) ctx in + (*[add_args] build the application of [f_term] to the list of variables + [args_list].*) + let f_appl = add_args (mk_Symb symb_skt) args_list in + Bindlib.subst tb f_appl + +type quant = { + symb : sym; (** The symbol that stand for the quantifier. *) + dom : term; (** The domain of the quantification. *) + var : tvar; (** The variable bound by the quantification. *) + typ : term; + (** The type of the quantified variable {b NOTE} It should always be + [T dom] where [T] is the builtin that interprets type codes. *) +} +(** A structure to represent quantifiers in a FOF. *) + +(* add_quant ql symb_all symb_P Vari(x) type_a add in a list a representation + of the universal quantification of x:type_a on top of the list ql, and + return the list.*) +let add_quant : quant list -> sym -> term -> tvar -> term -> quant list = + fun qlist q d v t -> { symb = q; dom = d; var = v; typ = t } :: qlist + +(* [mk_quant t q] builds an application of the quantifier q on the proposition + f.*) +let mk_quant : term -> quant -> term = + fun f q -> + let tb = bind q.var lift f in + add_args (mk_Symb q.symb) [ q.dom; mk_Abst (q.typ, tb) ] + +(** [nnf_term cfg t] computes the negation normal form of a first order + formula. *) +let nnf : config -> term -> term = + fun cfg t -> + let rec nnf_prop t = + match get_args t with + | Symb s, [ t1; t2 ] when s == cfg.symb_and -> + add_args (mk_Symb s) [ nnf_prop t1; nnf_prop t2 ] + | Symb s, [ t1; t2 ] when s == cfg.symb_or -> + add_args (mk_Symb s) [ nnf_prop t1; nnf_prop t2 ] + | Symb s, [ t1; t2 ] when s == cfg.symb_imp -> + add_args (mk_Symb cfg.symb_or) [ neg t1; nnf_prop t2 ] + | Symb s, [ t ] when s == cfg.symb_not -> neg t + | Symb s, [ a; Abst (x, tb) ] when s == cfg.symb_all -> + let var, p = Bindlib.unbind tb in + let nnf_tb = bind var lift (nnf_prop p) in + add_args (mk_Symb cfg.symb_all) [ a; mk_Abst (x, nnf_tb) ] + | Symb s, [ a; Abst (x, tb) ] when s == cfg.symb_ex -> + let var, p = Bindlib.unbind tb in + let nnf_tb = bind var lift (nnf_prop p) in + add_args (mk_Symb cfg.symb_ex) [ a; mk_Abst (x, nnf_tb) ] + | Symb _, _ | Abst (_, _), _ -> t + | _, _ -> t + and neg t = + match get_args t with + | Symb s, [] when s == cfg.symb_bot -> mk_Symb cfg.symb_top + | Symb s, [] when s == cfg.symb_top -> mk_Symb cfg.symb_bot + | Symb s, [ t1; t2 ] when s == cfg.symb_and -> + add_args (mk_Symb cfg.symb_or) [ neg t1; neg t2 ] + | Symb s, [ t1; t2 ] when s == cfg.symb_or -> + add_args (mk_Symb cfg.symb_and) [ neg t1; neg t2 ] + | Symb s, [ _; _ ] when s == cfg.symb_imp -> neg (nnf_prop t) + | Symb s, [ nt ] when s == cfg.symb_not -> nnf_prop nt + | Symb s, [ a; Abst (x, tb) ] when s == cfg.symb_all -> + let var, p = Bindlib.unbind tb in + let neg_tb = bind var lift (neg p) in + add_args (mk_Symb cfg.symb_ex) [ a; mk_Abst (x, neg_tb) ] + | Symb s, [ a; Abst (x, tb) ] when s == cfg.symb_ex -> + let var, p = Bindlib.unbind tb in + let nnf_tb = bind var lift (neg p) in + add_args (mk_Symb cfg.symb_all) [ a; mk_Abst (x, nnf_tb) ] + | _, _ -> add_args (mk_Symb cfg.symb_not) [ t ] + in + nnf_prop t + +exception NotInNnf of term + +let pnf cfg t = + let rec prenex t = + match get_args t with + | Symb s, [ t1; t2 ] when s == cfg.symb_and -> + let qlist1, sub1 = prenex t1 in + let qlist2, sub2 = prenex t2 in + let t = add_args (mk_Symb s) [ sub1; sub2 ] in + let qlist = qlist1 @ qlist2 in + (qlist, t) + | Symb s, [ t1; t2 ] when s == cfg.symb_or -> + let qlist1, sub1 = prenex t1 in + let qlist2, sub2 = prenex t2 in + let t = add_args (mk_Symb s) [ sub1; sub2 ] in + let qlist = qlist1 @ qlist2 in + (qlist, t) + | Symb s, [ _; _ ] when s == cfg.symb_imp -> + raise @@ NotInNnf t + | Symb s, [ nt ] when s == cfg.symb_not -> + let res = + match nt with + | Vari _ -> ([], t) + | Symb _ -> ([], t) + | _ -> raise @@ NotInNnf t + in + res + | Symb s, [ a; Abst (x, tb) ] when s == cfg.symb_all -> + let var, f = Bindlib.unbind tb in + let qlist, sf = prenex f in + let qlist = add_quant qlist s a var x in + (qlist, sf) + | Symb s, [ a; Abst (x, tb) ] when s == cfg.symb_ex -> + let var, f = Bindlib.unbind tb in + let qlist, sf = prenex f in + let qlist = add_quant qlist s a var x in + (qlist, sf) + | _, _ -> ([], t) + in + let qlist, f = prenex t in + List.fold_left mk_quant f (List.rev qlist) + +(** [handle ss pos t] returns a skolemized form of term [t] (at position + [pos]). A term is skolemized when it has no existential quantifiers: to + this end, for each existential quantifier in [t], signature state [ss] is + extended with a new symbol in order to substitute the variable bound by + the said quantifier. + @raise NotProp when the argument [t] is not an encoded proposition. *) +let handle : Sig_state.t -> Pos.popt -> term -> term = + fun ss pos t -> + (*Gets user-defined symbol identifiers mapped using "builtin" command.*) + let cfg = get_config ss pos in + let t = nnf cfg t in + let t = + try pnf cfg t + with NotInNnf _ -> + assert false (* [t] is put into nnf before *) + in + let rec skolemisation ss ctx ctr t = + match get_args t with + | Symb s, [ _; Abst (y, tb) ] when s == cfg.symb_ex -> + (* When existential quantification occurs, quantified variable is + substituted by a fresh symbol*) + let maj_ss, nv_sym, maj_ctr = new_skolem ss ctx ctr y in + let maj_term = subst_app ctx tb nv_sym in + skolemisation maj_ss ctx maj_ctr maj_term + | Symb s, [ a; Abst (x, tb) ] when s == cfg.symb_all -> + (* When universal quantification occurs, quantified variable is added + to context*) + let var, f = Bindlib.unbind tb in + let maj_ctx = add_var ctx var a in + let maj_f = skolemisation ss maj_ctx ctr f in + let maj_tb = bind var lift maj_f in + (*Reconstruct a term of form ∀ x : P, t', with t' skolemized*) + add_args (mk_Symb s) [ a; mk_Abst (x, maj_tb) ] + | _ -> t + in + let skl_of_t = skolemisation ss [] 0 t in + if Logger.log_enabled () then + log "Skolemized form of %a is %a" Print.term t Print.term skl_of_t; + skl_of_t diff --git a/src/handle/skolem.mli b/src/handle/skolem.mli new file mode 100644 index 000000000..b9f998e56 --- /dev/null +++ b/src/handle/skolem.mli @@ -0,0 +1,19 @@ +open Common +open Core +open Term +open Fol + +(** [nnf cfg phi] returns the negation normal form of [phi], assuming it is + the encoding of a first-order formula using [cfg]. *) +val nnf : config -> term -> term + +exception NotInNnf of term + +(** [pnf cfg phi] returns the prenex normal form of [phi]. + @raise NotInNnf when formula [phi] is not in negation normal form. *) +val pnf : config -> term -> term + +(** [skolem ss pos t] returns the skolemized form of [t] ([pos] is used for + error messages). Existential quantifiers are replaced by new symbols that + are added in the signature state [ss]. *) +val handle : Sig_state.t -> Pos.popt -> term -> term diff --git a/src/handle/tactic.ml b/src/handle/tactic.ml index 3fdd7bea1..0fb74b016 100644 --- a/src/handle/tactic.ml +++ b/src/handle/tactic.ml @@ -331,6 +331,26 @@ let handle : | Typ gt::_ -> Why3_tactic.handle ss pos cfg gt; tac_admit ss sym_pos ps gt | _ -> assert false) + | P_tac_skolem -> + let sym_P = Builtin.get ss pos "P" in + let t = + match get_args gt.goal_type with + | Symb(s), [t] when s == sym_P -> t + | _ -> fatal pos "Goal not of form (%a _)@." sym sym_P + in + let skl_t = Skolem.handle ss sym_pos t in + (* FIXME. We generate an axiom ax: P skl_t → P t in order to build a proof + of P t from a proof of P skl_t. *) + let p_skl_t = mk_Appl (mk_Symb sym_P, skl_t) in + let c = Env.to_ctxt env in + let ax_typ = mk_Prod (p_skl_t, bind (new_tvar "_") lift gt.goal_type) in + let ax_typ, arity = Ctxt.to_prod c ax_typ in + let m = LibMeta.fresh (new_problem()) ax_typ arity in + (*FIXME: check that ax_typ has no meta.*) + let ax = add_axiom ss sym_pos m in + let p = new_problem() in + let new_goal = LibMeta.make p c p_skl_t in + tac_refine pos ps gt gs p (mk_Appl (mk_Symb ax, new_goal)) (** Representation of a tactic output. *) type tac_output = proof_state * Query.result diff --git a/src/parsing/lpLexer.ml b/src/parsing/lpLexer.ml index ff575c8c2..14f3d0dde 100644 --- a/src/parsing/lpLexer.ml +++ b/src/parsing/lpLexer.ml @@ -75,6 +75,7 @@ type token = | RULE | SEQUENTIAL | SIMPLIFY + | SKOLEM | SOLVE | SYMBOL | SYMMETRY @@ -242,6 +243,7 @@ let rec token lb = | "rule" -> RULE | "sequential" -> SEQUENTIAL | "simplify" -> SIMPLIFY + | "skolem" -> SKOLEM | "solve" -> SOLVE | "symbol" -> SYMBOL | "symmetry" -> SYMMETRY diff --git a/src/parsing/lpParser.mly b/src/parsing/lpParser.mly index 8c24556b8..5a09d4c74 100644 --- a/src/parsing/lpParser.mly +++ b/src/parsing/lpParser.mly @@ -68,6 +68,7 @@ %token RULE %token SEQUENTIAL %token SIMPLIFY +%token SKOLEM %token SOLVE %token SYMBOL %token SYMMETRY @@ -313,6 +314,7 @@ tactic: | REWRITE d=SIDE? p=rw_patt_spec? t=term { let b = match d with Some Pratter.Left -> false | _ -> true in make_pos $sloc (P_tac_rewrite(b,p,t)) } + | SKOLEM { make_pos $loc P_tac_skolem } | SIMPLIFY i=qid_or_nat? { make_pos $sloc (P_tac_simpl i) } | SOLVE { make_pos $sloc P_tac_solve } | SYMMETRY { make_pos $sloc P_tac_sym } diff --git a/src/parsing/pretty.ml b/src/parsing/pretty.ml index 25a8894af..c0fce3893 100644 --- a/src/parsing/pretty.ml +++ b/src/parsing/pretty.ml @@ -66,6 +66,7 @@ let _ = let open LpLexer in ; "rule", RULE ; "sequential", SEQUENTIAL ; "simplify", SIMPLIFY + ; "skolem", SKOLEM ; "solve", SOLVE ; "symbol", SYMBOL ; "symmetry", SYMMETRY @@ -276,6 +277,7 @@ let tactic : p_tactic pp = fun ppf { elt; _ } -> out ppf "rewrite%a%a %a" dir b (Option.pp pat) p term t | P_tac_simpl None -> out ppf "simplify" | P_tac_simpl (Some qid) -> out ppf "simplify %a" qident qid + | P_tac_skolem -> out ppf "skolem" | P_tac_solve -> out ppf "solve" | P_tac_sym -> out ppf "symmetry" | P_tac_why3 p -> diff --git a/src/parsing/syntax.ml b/src/parsing/syntax.ml index 7780c76c4..b444d1dc2 100644 --- a/src/parsing/syntax.ml +++ b/src/parsing/syntax.ml @@ -202,6 +202,7 @@ type p_tactic_aux = | P_tac_rewrite of bool * p_rw_patt option * p_term (* The boolean indicates if the equation is applied from left to right. *) | P_tac_simpl of p_qident option + | P_tac_skolem | P_tac_solve | P_tac_sym | P_tac_why3 of string option @@ -562,6 +563,7 @@ let fold_idents : ('a -> p_qident -> 'a) -> 'a -> p_command list -> 'a = | P_tac_sym | P_tac_why3 _ | P_tac_solve + | P_tac_skolem | P_tac_fail | P_tac_generalize _ | P_tac_induction -> (vs, a) diff --git a/tests/cnfnnf.ml b/tests/cnfnnf.ml new file mode 100644 index 000000000..51a3d6c4a --- /dev/null +++ b/tests/cnfnnf.ml @@ -0,0 +1,97 @@ +open Common +open Core +open Term +open Sig_state +open Parsing + +(** Hack to parse easily a single term *) +let parse_term s = + (* A hack to parse a term: wrap term [s] into [compute s;]. *) + let c = "compute " ^ s ^ ";" in + let command = Stream.next (Parser.Lp.parse_string "term" c) in + match command.elt with + | Syntax.P_query { elt = Syntax.P_query_normalize (t, _); _ } -> t + | _ -> assert false + +let scope_term ?(env = []) ss = Scope.scope_term true ss env + +let add_sym (ss, slist) id = + let ss, sym = + Sig_state.add_symbol ss Public Defin Eager true (Pos.none id) Term.mk_Type + [] None + in + (ss, sym :: slist) + +let sig_state : Sig_state.t = + let sign = Sig_state.create_sign (Path.ghost "cnfnnf") in + Sig_state.of_sign sign + +(** Builtin configuration for propositional logic. *) + +let fol_symb_str = [ "P"; "t"; "∨"; "∧"; "⇒"; "⊥"; "⊤"; "¬"; "∃"; "∀" ] + +(** [get_config ss pos] build the configuration using [ss]. *) +let get_config slist = + let get n = List.nth slist n in + Handle.Fol. + { + symb_P = get 0; + symb_T = get 1; + symb_or = get 2; + symb_and = get 3; + symb_imp = get 4; + symb_bot = get 5; + symb_top = get 6; + symb_not = get 7; + symb_ex = get 8; + symb_all = get 9; + } + +let mk_env symb_p = + let tv = [ "A"; "B" ] in + let rec aux e tlist = + let tb_p = _Symb symb_p in + match tlist with + | hd :: tl -> aux (Env.add (new_tvar hd) tb_p None e) tl + | [] -> e + in + aux Env.empty tv + +(** Setup a signature state, a first order logic configuration and an + environment to scope properly formulae. *) +let sig_state, cfg = + let ss, symlist = List.fold_left add_sym (sig_state, []) fol_symb_str in + Timed.(Print.sig_state := sig_state); + (ss, get_config (List.rev symlist)) + +(** An environment defining two variables [A] and [B]. *) +let env = Env.empty + |> Env.add (new_tvar "A") _Kind None + |> Env.add (new_tvar "B") _Kind None + +let test_nnf () = + let formula = + parse_term "∀ P (λ x1 : A, ¬ (∃ B (λ y1, ∨ (∨ x1 y1) ⊥)))" + |> scope_term ~env sig_state + in + let witness = "∀ P (λ x1, ∀ B (λ y1, ∧ (∧ (¬ x1) (¬ y1)) ⊤))" in + Alcotest.(check string) + "Negation normal form" witness + (Format.asprintf "%a" Print.term (Handle.Skolem.nnf cfg formula)) + +let test_pnf () = + let formula = + parse_term "∨ (∀ P (λ x1, x1)) A" |> scope_term ~env sig_state + in + let witness = "∀ P (λ x1, ∨ x1 A)" in + Alcotest.(check string) + "Prenex normal form" witness + (Format.asprintf "%a" Print.term (Handle.Skolem.pnf cfg formula)) + +let _ = + let open Alcotest in + run "proposition transformations" + [ + ( "prop", + [ test_case "nnf" `Quick test_nnf; test_case "pnf" `Quick test_pnf ] ); + ] diff --git a/tests/dune b/tests/dune index feeb644e1..746b88494 100644 --- a/tests/dune +++ b/tests/dune @@ -1,5 +1,5 @@ (tests - (names ok_ko rewriting purity kernel) + (names ok_ko rewriting purity kernel cnfnnf) (deps (glob_files OK/*.lp) (glob_files OK/*.dk) diff --git a/tests/skolem.lp b/tests/skolem.lp new file mode 100644 index 000000000..6b057d462 --- /dev/null +++ b/tests/skolem.lp @@ -0,0 +1,53 @@ +constant symbol Prop : TYPE; +builtin "Prop" ≔ Prop; +injective symbol π : Prop → TYPE; +builtin "P" ≔ π; +constant symbol Set : TYPE; +injective symbol τ : Set → TYPE; +builtin "T" ≔ τ; +inductive ℕ : TYPE ≔ // `dN +| 0 : ℕ +| s : ℕ → ℕ; +constant symbol nat : Set; +rule τ nat ↪ ℕ; + +symbol is0 : ℕ → Prop; +builtin "0" ≔ 0; +builtin "+1" ≔ s; +symbol one ≔ s 0; + +symbol + : ℕ → ℕ → ℕ; +notation + infix right 20; +rule 0 + $y ↪ $y +with s $x + $y ↪ s ($x + $y); + +symbol × : ℕ → ℕ → ℕ; // \times +notation × infix right 30; +rule 0 × _ ↪ 0 +with s $x × $y ↪ $y + $x × $y; + +constant symbol ∃ [a] : (τ a → Prop) → Prop; +notation ∃ quantifier; +builtin "ex" ≔ ∃; + +constant symbol ∀ [a] : (τ a → Prop) → Prop; +builtin "all" ≔ ∀; +constant symbol = [a] : τ a → τ a → Prop; +notation = infix 10; +builtin "eq" ≔ =; +symbol =-refl x : π(x = x); +constant symbol eq_refl [a] (x:τ a) : π (x = x); +constant symbol imp : Prop → Prop → Prop; +builtin "imp" ≔ imp; // écrire regle +rule π (imp $a $b) ↪ π $a → π $b; + +symbol zero_eq_zero : π (∃ (λ y : τ nat, (0 + y = 0))) ≔ +begin + print; + simplify +; + print; + skolem; + + print; + +end; \ No newline at end of file