From 3fb8d14cf916250b7cee73d237877f9e80a8d3d7 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Fr=C3=A9d=C3=A9ric=20Blanqui?= Date: Fri, 10 Jan 2025 14:52:13 +0100 Subject: [PATCH 1/4] =?UTF-8?q?theory=5Fhol.lp:=20rename=20T=20into=20?= =?UTF-8?q?=E2=8A=A4=20and=20F=20into=20=E2=8A=A5?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- TODO.md | 2 -- erasing.lp | 8 ++++---- theory_hol.lp | 6 +++--- 3 files changed, 7 insertions(+), 9 deletions(-) diff --git a/TODO.md b/TODO.md index 7d077b8e..2ee189a5 100644 --- a/TODO.md +++ b/TODO.md @@ -7,8 +7,6 @@ TODO - why the mapping of ITLIST does not work anymore ? -- in lp output, replace T by ⊤ ? - - write progress in an ocaml program, and estimate time wrt size of files - use a single term_abbrev file for each theorem, and split it diff --git a/erasing.lp b/erasing.lp index 55267b1e..89625400 100644 --- a/erasing.lp +++ b/erasing.lp @@ -29,11 +29,11 @@ builtin "ex_def" ≔ ∃_def; builtin "not" ≔ ¬; builtin "not_def" ≔ ¬_def; -builtin "True" ≔ T; -builtin "T_def" ≔ T_def; +builtin "True" ≔ ⊤; +builtin "T_def" ≔ ⊤_def; -builtin "False" ≔ F; -builtin "F_def" ≔ F_def; +builtin "False" ≔ ⊥; +builtin "F_def" ≔ ⊥_def; builtin "ex1" ≔ ∃₁; builtin "ex1_def" ≔ ∃₁_def; diff --git a/theory_hol.lp b/theory_hol.lp index 2f3c76e9..84a2a400 100644 --- a/theory_hol.lp +++ b/theory_hol.lp @@ -26,18 +26,18 @@ opaque symbol SYM [a] [x y : El a] (xy: Prf (= x y)) : Prf (= y x) ≔ /* HOL-Light derived connectives */ constant symbol ∃₁ [A] : El (fun (fun A bool) bool); constant symbol ¬ : El (fun bool bool); -constant symbol F : El bool; +constant symbol ⊥ : El bool; constant symbol ∨ : El (fun bool (fun bool bool)); constant symbol ∃ [A] : El (fun (fun A bool) bool); constant symbol ∀ [A] : El (fun (fun A bool) bool); constant symbol ⇒ : El (fun bool (fun bool bool)); constant symbol ∧ : El (fun bool (fun bool bool)); -constant symbol T : El bool; +constant symbol ⊤ : El bool; /* Natural deduction rules */ rule Prf (⇒ $p $q) ↪ Prf $p → Prf $q; rule Prf (∀ $p) ↪ Π x, Prf ($p x); -symbol Tᵢ : Prf T; +symbol ⊤ᵢ : Prf ⊤; symbol ∧ᵢ [p : El bool] : Prf p → Π [q : El bool], Prf q → Prf (∧ p q); symbol ∧ₑ₁ [p q : El bool] : Prf (∧ p q) → Prf p; symbol ∧ₑ₂ [p q : El bool] : Prf (∧ p q) → Prf q; From fd300ebf1a1481bb9d7f2014d183ff78d53673e7 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Fr=C3=A9d=C3=A9ric=20Blanqui?= Date: Fri, 10 Jan 2025 15:09:58 +0100 Subject: [PATCH 2/4] wip --- xlp.ml | 2 ++ 1 file changed, 2 insertions(+) diff --git a/xlp.ml b/xlp.ml index d6a8405e..e5b086ee 100644 --- a/xlp.ml +++ b/xlp.ml @@ -32,6 +32,8 @@ let name = | "==>" -> "⇒" | "!" -> "∀" | "?" -> "∃" + | "F" -> "⊥" + | "T" -> "⊤" | "?!" -> "∃₁" | "~" -> "¬" | "-->" -> "⟶" (* 27F6 *) From ceaeb6390a39751a772a63c21f2d7f6c8cf4bce3 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Fr=C3=A9d=C3=A9ric=20Blanqui?= Date: Fri, 10 Jan 2025 15:15:19 +0100 Subject: [PATCH 3/4] wip --- erasing.lp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/erasing.lp b/erasing.lp index 89625400..34e00433 100644 --- a/erasing.lp +++ b/erasing.lp @@ -39,7 +39,7 @@ builtin "ex1" ≔ ∃₁; builtin "ex1_def" ≔ ∃₁_def; // natural deduction rules -builtin "Logic.I" ≔ Tᵢ; +builtin "Logic.I" ≔ ⊤ᵢ; builtin "conj" ≔ ∧ᵢ; builtin "proj1" ≔ ∧ₑ₁; builtin "proj2" ≔ ∧ₑ₂; From 327fab5ffafd593b8e8f412cad1e4586bdcbacb2 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Fr=C3=A9d=C3=A9ric=20Blanqui?= Date: Fri, 10 Jan 2025 15:23:59 +0100 Subject: [PATCH 4/4] wip --- xlp.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/xlp.ml b/xlp.ml index e5b086ee..97c6e22d 100644 --- a/xlp.ml +++ b/xlp.ml @@ -506,7 +506,7 @@ let proof tvs rmap = int oc (pos_first (fun th -> concl th = t) !the_axioms); list_prefix " " typ oc (type_vars_in_term t); list_prefix " " term oc (frees t) - | Ptruth -> string oc "Tᵢ" + | Ptruth -> string oc "⊤ᵢ" | Pconj(k1,k2) -> string oc "∧ᵢ "; sub_at oc k1; char oc ' '; sub_at oc k2 | Pconjunct1 k -> string oc "∧ₑ₁ "; sub_at oc k | Pconjunct2 k -> string oc "∧ₑ₂ "; sub_at oc k