From 28ff0f592a4d2ace38ec9ca9cd6e6cfb31f3f20d Mon Sep 17 00:00:00 2001 From: hkalbasi Date: Thu, 1 Feb 2024 15:11:38 +0330 Subject: [PATCH 1/5] Add cnt_firstn_le and cnt_ge_0 --- library/List.v | 2 ++ 1 file changed, 2 insertions(+) diff --git a/library/List.v b/library/List.v index 8115f19..f4b368c 100644 --- a/library/List.v +++ b/library/List.v @@ -119,6 +119,7 @@ Qed; Suggest hyp default apply nil_unique in $n with label |l| = 0 => l = []; Axiom #1 repeat: ∀ A: U, ℤ -> A -> list A; Axiom repeat_intro: ∀ A: U, ∀ x: A, ∀ t: ℤ, 0 ≤ t -> repeat t x = [x] + repeat (t - 1) x; +Todo cnt_ge_0: ∀ A: U, ∀ x: A, ∀ l: list A, 0 ≤ cnt x l; Todo repeat_unique: ∀ A: U, ∀ x: A, ∀ l: list A, cnt x l = |l| -> l = repeat (|l|) x; Todo repeat_len: ∀ A: U, ∀ x: A, ∀ t: ℤ, 0 ≤ t -> |repeat t x| = t; Todo repeat_cnt: ∀ A: U, ∀ x: A, ∀ t: ℤ, 0 ≤ t -> cnt x (repeat t x) = t; @@ -229,6 +230,7 @@ Todo firstn_append_r: ∀ T: U, ∀ a b: list T, ∀ m, m ≥ 0 -> firstn (a + b Todo firstn_append_l_len: ∀ T: U, ∀ a b: list T, firstn (a + b) (|a|) = a; Todo cnt_of_firstn_dis_range: ∀ T: U, ∀ a: list T, ∀ m, ∀ c, 0 ≤ cnt c (firstn a m) - cnt c (firstn a (m - 1)) ∧ cnt c (firstn a m) - cnt c (firstn a (m - 1)) ≤ 1; Todo cnt_of_firstn_dis_1: ∀ T: U, ∀ a: list T, ∀ m, ∀ c, cnt c (firstn a m) = cnt c (firstn a (m - 1)) + 1 -> firstn a m = firstn a (m - 1) + [c]; +Todo cnt_firstn_le: ∀ T: U, ∀ a: list T, ∀ m, ∀ c, cnt c (firstn a m) ≤ cnt c a; Todo member_set_firstn: ∀ T: U, ∀ l: list T, ∀ i, member_set (firstn l i) ⊆ member_set l; Todo len_firstn: ∀ T: U, ∀ l: list T, ∀ i, 0 ≤ i -> i ≤ |l| -> |firstn l i| = i; Todo firstn_firstn: ∀ T: U, ∀ l: list T, ∀ i j, i ≤ j -> firstn (firstn l j) i = firstn l i; From 31cb04fc7d84d495aa810f24991b618ef89f6b89 Mon Sep 17 00:00:00 2001 From: hkalbasi Date: Thu, 1 Feb 2024 17:54:15 +0330 Subject: [PATCH 2/5] Add button to disable auto filter --- .gitignore | 1 + Cargo.lock | 203 +++++++++++++++++++++-- front/src/components/proof/Toolbar.tsx | 4 +- front/src/components/setting/Setting.tsx | 10 ++ front/src/dev_mode/auto_proof_state.ts | 42 +++++ hakim-cli/Cargo.toml | 1 + hakim-cli/src/main.rs | 43 ++++- 7 files changed, 286 insertions(+), 18 deletions(-) create mode 100644 front/src/dev_mode/auto_proof_state.ts diff --git a/.gitignore b/.gitignore index cfdd8b9..4f4a293 100644 --- a/.gitignore +++ b/.gitignore @@ -5,3 +5,4 @@ flamegraph.svg .z3-trace hakim_log* node_modules +ignore diff --git a/Cargo.lock b/Cargo.lock index 552381d..84c8a9f 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -247,6 +247,54 @@ dependencies = [ "alloc-no-stdlib", ] +[[package]] +name = "anstream" +version = "0.6.11" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "6e2e1ebcb11de5c03c67de28a7df593d32191b44939c482e97702baaaa6ab6a5" +dependencies = [ + "anstyle", + "anstyle-parse", + "anstyle-query", + "anstyle-wincon", + "colorchoice", + "utf8parse", +] + +[[package]] +name = "anstyle" +version = "1.0.5" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "2faccea4cc4ab4a667ce676a30e8ec13922a692c99bb8f5b11f1502c72e04220" + +[[package]] +name = "anstyle-parse" +version = "0.2.3" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "c75ac65da39e5fe5ab759307499ddad880d724eed2f6ce5b5e8a26f4f387928c" +dependencies = [ + "utf8parse", +] + +[[package]] +name = "anstyle-query" +version = "1.0.2" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "e28923312444cdd728e4738b3f9c9cac739500909bb3d3c94b43551b16517648" +dependencies = [ + "windows-sys 0.52.0", +] + +[[package]] +name = "anstyle-wincon" +version = "3.0.2" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "1cd54b81ec8d6180e24654d0b371ad22fc3dd083b6ff8ba325b72e00c87660a7" +dependencies = [ + "anstyle", + "windows-sys 0.52.0", +] + [[package]] name = "arrayvec" version = "0.5.2" @@ -425,6 +473,46 @@ dependencies = [ "libloading", ] +[[package]] +name = "clap" +version = "4.4.18" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "1e578d6ec4194633722ccf9544794b71b1385c3c027efe0c55db226fc880865c" +dependencies = [ + "clap_builder", + "clap_derive", +] + +[[package]] +name = "clap_builder" +version = "4.4.18" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "4df4df40ec50c46000231c914968278b1eb05098cf8f1b3a518a95030e71d1c7" +dependencies = [ + "anstream", + "anstyle", + "clap_lex", + "strsim", +] + +[[package]] +name = "clap_derive" +version = "4.4.7" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "cf9804afaaf59a91e75b022a30fb7229a7901f60c755489cc61c9b423b836442" +dependencies = [ + "heck", + "proc-macro2", + "quote", + "syn 2.0.29", +] + +[[package]] +name = "clap_lex" +version = "0.6.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "702fc72eb24e5a1e48ce58027a675bc24edd52096d5397d4aea7c6dd9eca0bd1" + [[package]] name = "clipboard-win" version = "4.5.0" @@ -445,6 +533,12 @@ dependencies = [ "cc", ] +[[package]] +name = "colorchoice" +version = "1.0.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "acbf1af155f9b9ef647e42cdc158db4b64a1b61f743629225fde6f3e0be2a7c7" + [[package]] name = "console_error_panic_hook" version = "0.1.7" @@ -622,7 +716,7 @@ checksum = "136526188508e25c6fef639d7927dfb3e0e3084488bf202267829cf7fc23dbdd" dependencies = [ "errno-dragonfly", "libc", - "windows-sys", + "windows-sys 0.48.0", ] [[package]] @@ -653,7 +747,7 @@ checksum = "ef033ed5e9bad94e55838ca0ca906db0e043f517adda0c8b79c7a8c66c93c1b5" dependencies = [ "cfg-if 1.0.0", "rustix", - "windows-sys", + "windows-sys 0.48.0", ] [[package]] @@ -767,6 +861,7 @@ dependencies = [ name = "hakim-cli" version = "0.1.0" dependencies = [ + "clap", "hakim-engine", "rustyline", ] @@ -831,6 +926,12 @@ version = "0.12.3" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "8a9ee70c43aaf417c914396645a0fa852624801b24ebb7ae78fe8272889ac888" +[[package]] +name = "heck" +version = "0.4.1" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "95505c38b4572b2d910cecb0281560f54b440a19336cbbcb27bf6ce6adc6f5a8" + [[package]] name = "hermit-abi" version = "0.3.2" @@ -1090,7 +1191,7 @@ dependencies = [ "libc", "log", "wasi", - "windows-sys", + "windows-sys 0.48.0", ] [[package]] @@ -1244,7 +1345,7 @@ dependencies = [ "libc", "redox_syscall 0.3.5", "smallvec", - "windows-targets", + "windows-targets 0.48.5", ] [[package]] @@ -1491,7 +1592,7 @@ dependencies = [ "errno", "libc", "linux-raw-sys", - "windows-sys", + "windows-sys 0.48.0", ] [[package]] @@ -1654,7 +1755,7 @@ source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "2538b18701741680e0322a2302176d3253a35388e2e62f172f64f4f16605f877" dependencies = [ "libc", - "windows-sys", + "windows-sys 0.48.0", ] [[package]] @@ -1675,6 +1776,12 @@ version = "1.0.6" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "9e08d8363704e6c71fc928674353e6b7c23dcea9d82d7012c8faf2a3a025f8d0" +[[package]] +name = "strsim" +version = "0.10.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "73473c0e59e6d5812c5dfe2a064a6444949f089e20eec9a2e5506596494e4623" + [[package]] name = "syn" version = "1.0.109" @@ -1774,7 +1881,7 @@ dependencies = [ "pin-project-lite", "signal-hook-registry", "socket2", - "windows-sys", + "windows-sys 0.48.0", ] [[package]] @@ -2026,7 +2133,16 @@ version = "0.48.0" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "677d2418bec65e3338edb076e806bc1ec15693c5d0104683f2efe857f61056a9" dependencies = [ - "windows-targets", + "windows-targets 0.48.5", +] + +[[package]] +name = "windows-sys" +version = "0.52.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "282be5f36a8ce781fad8c8ae18fa3f9beff57ec1b52cb3de0789201425d9a33d" +dependencies = [ + "windows-targets 0.52.0", ] [[package]] @@ -2035,13 +2151,28 @@ version = "0.48.5" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "9a2fa6e2155d7247be68c096456083145c183cbbbc2764150dda45a87197940c" dependencies = [ - "windows_aarch64_gnullvm", - "windows_aarch64_msvc", - "windows_i686_gnu", - "windows_i686_msvc", - "windows_x86_64_gnu", - "windows_x86_64_gnullvm", - "windows_x86_64_msvc", + "windows_aarch64_gnullvm 0.48.5", + "windows_aarch64_msvc 0.48.5", + "windows_i686_gnu 0.48.5", + "windows_i686_msvc 0.48.5", + "windows_x86_64_gnu 0.48.5", + "windows_x86_64_gnullvm 0.48.5", + "windows_x86_64_msvc 0.48.5", +] + +[[package]] +name = "windows-targets" +version = "0.52.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "8a18201040b24831fbb9e4eb208f8892e1f50a37feb53cc7ff887feb8f50e7cd" +dependencies = [ + "windows_aarch64_gnullvm 0.52.0", + "windows_aarch64_msvc 0.52.0", + "windows_i686_gnu 0.52.0", + "windows_i686_msvc 0.52.0", + "windows_x86_64_gnu 0.52.0", + "windows_x86_64_gnullvm 0.52.0", + "windows_x86_64_msvc 0.52.0", ] [[package]] @@ -2050,42 +2181,84 @@ version = "0.48.5" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "2b38e32f0abccf9987a4e3079dfb67dcd799fb61361e53e2882c3cbaf0d905d8" +[[package]] +name = "windows_aarch64_gnullvm" +version = "0.52.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "cb7764e35d4db8a7921e09562a0304bf2f93e0a51bfccee0bd0bb0b666b015ea" + [[package]] name = "windows_aarch64_msvc" version = "0.48.5" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "dc35310971f3b2dbbf3f0690a219f40e2d9afcf64f9ab7cc1be722937c26b4bc" +[[package]] +name = "windows_aarch64_msvc" +version = "0.52.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "bbaa0368d4f1d2aaefc55b6fcfee13f41544ddf36801e793edbbfd7d7df075ef" + [[package]] name = "windows_i686_gnu" version = "0.48.5" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "a75915e7def60c94dcef72200b9a8e58e5091744960da64ec734a6c6e9b3743e" +[[package]] +name = "windows_i686_gnu" +version = "0.52.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "a28637cb1fa3560a16915793afb20081aba2c92ee8af57b4d5f28e4b3e7df313" + [[package]] name = "windows_i686_msvc" version = "0.48.5" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "8f55c233f70c4b27f66c523580f78f1004e8b5a8b659e05a4eb49d4166cca406" +[[package]] +name = "windows_i686_msvc" +version = "0.52.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "ffe5e8e31046ce6230cc7215707b816e339ff4d4d67c65dffa206fd0f7aa7b9a" + [[package]] name = "windows_x86_64_gnu" version = "0.48.5" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "53d40abd2583d23e4718fddf1ebec84dbff8381c07cae67ff7768bbf19c6718e" +[[package]] +name = "windows_x86_64_gnu" +version = "0.52.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "3d6fa32db2bc4a2f5abeacf2b69f7992cd09dca97498da74a151a3132c26befd" + [[package]] name = "windows_x86_64_gnullvm" version = "0.48.5" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "0b7b52767868a23d5bab768e390dc5f5c55825b6d30b86c844ff2dc7414044cc" +[[package]] +name = "windows_x86_64_gnullvm" +version = "0.52.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "1a657e1e9d3f514745a572a6846d3c7aa7dbe1658c056ed9c3344c4109a6949e" + [[package]] name = "windows_x86_64_msvc" version = "0.48.5" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "ed94fce61571a4006852b7389a063ab983c02eb1bb37b47f8272ce92d06d9538" +[[package]] +name = "windows_x86_64_msvc" +version = "0.52.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "dff9641d1cd4be8d1a070daf9e3773c5f67e78b4d9d42263020c057706765c04" + [[package]] name = "z3" version = "0.12.1" diff --git a/front/src/components/proof/Toolbar.tsx b/front/src/components/proof/Toolbar.tsx index 87824b7..c7e37f9 100644 --- a/front/src/components/proof/Toolbar.tsx +++ b/front/src/components/proof/Toolbar.tsx @@ -6,6 +6,7 @@ import css from "./toolbar.module.css"; import logo from "../../logo.png" import { flip, offset, shift, useFloating } from '@floating-ui/react-dom'; import { getDevState } from "../../dev_mode"; +import { useAutoProofState } from "../../dev_mode/auto_proof_state"; export const ToolButton = ({ label, onClick }: { label: string, onClick: any }) => { return ( @@ -111,10 +112,11 @@ const AutoProofButton = () => { }; export const Toolbar = () => { + const autoState = useAutoProofState(); return (
- + {autoState && } { getDevState() === "debug" && { const tactic = window.prompt(g`enter_tactic`); diff --git a/front/src/components/setting/Setting.tsx b/front/src/components/setting/Setting.tsx index b3a22d2..6379663 100644 --- a/front/src/components/setting/Setting.tsx +++ b/front/src/components/setting/Setting.tsx @@ -1,4 +1,5 @@ import { getDevState, setDevState, useDevState } from "../../dev_mode"; +import { getAutoProofState, setAutoProofState, useAutoProofState } from "../../dev_mode/auto_proof_state"; import { changeLang, g, getLang } from "../../i18n"; export const Setting = () => { @@ -9,11 +10,20 @@ export const Setting = () => { setDevState('off'); } }; + const changeAutoProofMode = () => { + if (getAutoProofState()) { + setAutoProofState(false); + } else { + setAutoProofState(true); + } + }; const devState = useDevState(); + const autoState = useAutoProofState(); return
  • {g`change_lang`}
  • {g`dev_mode`}
    • +
  • {g`auto_proof`}
; }; \ No newline at end of file diff --git a/front/src/dev_mode/auto_proof_state.ts b/front/src/dev_mode/auto_proof_state.ts new file mode 100644 index 0000000..e8aafe9 --- /dev/null +++ b/front/src/dev_mode/auto_proof_state.ts @@ -0,0 +1,42 @@ +import { useEffect, useState } from "react"; + +export const getAutoProofState = (): boolean => { + return (localStorage.getItem("auto_proof_state") !== "off"); +}; + +type EventListener = (s: boolean) => void; + +let listeners: EventListener[] = []; + +const emit = () => { + const v = getAutoProofState(); + console.log('Emitted auto proof state', v, ' to ', listeners.length, ' people'); + listeners.forEach((f) => f(v)); +}; + +const subscribe = (f: EventListener) => { + listeners.push(f); + emit(); + return () => { + listeners = listeners.filter((x) => x !== f); + }; +}; + +export const useAutoProofState = (): boolean => { + const [s, setS] = useState(getAutoProofState()); + useEffect(() => { + return subscribe(setS); + }, []); + return s; +}; + +export const setAutoProofState = (s: boolean) => { + if (s) { + localStorage.setItem("auto_proof_state", "on"); + } else { + localStorage.setItem("auto_proof_state", "off"); + } + emit(); +}; + + diff --git a/hakim-cli/Cargo.toml b/hakim-cli/Cargo.toml index 3b5e9e3..fa25ff7 100644 --- a/hakim-cli/Cargo.toml +++ b/hakim-cli/Cargo.toml @@ -6,5 +6,6 @@ edition = "2018" # See more keys and their definitions at https://doc.rust-lang.org/cargo/reference/manifest.html [dependencies] +clap = { version = "4.4.18", features = ["derive"] } hakim-engine = { path = "../hakim-engine" } rustyline = "9.0.0" diff --git a/hakim-cli/src/main.rs b/hakim-cli/src/main.rs index 3e75ff5..3c88034 100644 --- a/hakim-cli/src/main.rs +++ b/hakim-cli/src/main.rs @@ -1,8 +1,47 @@ +use clap::Parser; use hakim_engine::engine::Engine; +#[derive(Parser)] +enum Command { + Check { path: String }, + Interactive { goal: String }, +} + fn main() { - let eng = Engine::default(); - let mut session = eng.interactive_session("forall a b: U, forall f: forall x: a, b, forall x y: a, forall p: eq a x y, eq b (f x) (f y)").unwrap(); + let mut eng = Engine::default(); + eng.load_library("/").unwrap(); + let command = Command::parse(); + match command { + Command::Check { path } => { + let text = std::fs::read_to_string(path).expect("Error in openning file"); + let mut commands = text.split(';').map(|x| x.trim()); + let goal = commands.next().unwrap().strip_prefix("Goal ").unwrap(); + let mut session = eng.interactive_session(goal).unwrap(); + for command in commands { + if command == "Proof" || command.is_empty() { + continue; + } + match session.run_tactic(command) { + Ok(_) => (), + Err(e) => { + println!("Tactic Error: {:#?}", e); + return; + } + } + } + if !session.is_finished() { + println!("Proof is not finished"); + handle_session(session); + } + } + Command::Interactive { goal } => { + let session = eng.interactive_session(&goal).unwrap(); + handle_session(session); + } + } +} + +fn handle_session(mut session: hakim_engine::interactive::Session) { let mut rl = rustyline::Editor::<()>::new(); loop { session.print(); From e2bf40cbc441472743abd509090716ef71529641 Mon Sep 17 00:00:00 2001 From: hkalbasi Date: Thu, 1 Feb 2024 18:18:47 +0330 Subject: [PATCH 3/5] Add utm_reject_invalid_format --- library/Automata.v | 2 ++ 1 file changed, 2 insertions(+) diff --git a/library/Automata.v b/library/Automata.v index 810e3b4..fe5d650 100644 --- a/library/Automata.v +++ b/library/Automata.v @@ -171,6 +171,8 @@ Axiom utm_halt_fold: ∀ t: TM, ∀ s, turing_halt t s -> turing_halt universal_ Suggest goal default apply utm_halt_fold with label Destruct; Suggest hyp default apply utm_halt_unfold in $n with label Destruct; +Axiom utm_reject_invalid_format: ∀ s: list char, (~ ∃ t: TM, ∃ a: list char, s = turing_to_str t + "*" + a) → turing_reject universal_turing_machine s; + Axiom select_tm: list char -> TM; Axiom select_tm_fold: ∀ s, turing_accept (select_tm s) s; Axiom select_tm_unfold: ∀ s1 s2, turing_accept (select_tm s1) s2 -> s1 = s2; From f74e0d5153c942c1dd8f6124c6c40a849d09e5dc Mon Sep 17 00:00:00 2001 From: hkalbasi Date: Thu, 1 Feb 2024 18:35:06 +0330 Subject: [PATCH 4/5] Add valid_paren_cnt_eq --- library/EnumerativeCombinatorics.v | 1 + 1 file changed, 1 insertion(+) diff --git a/library/EnumerativeCombinatorics.v b/library/EnumerativeCombinatorics.v index 956f111..afe441f 100644 --- a/library/EnumerativeCombinatorics.v +++ b/library/EnumerativeCombinatorics.v @@ -1174,6 +1174,7 @@ Proof; lia; Qed; Todo valid_paren_cnt_right: ∀ a, valid_paren a -> ∀ k, 2 * k = |a| -> cnt ')' a = k; +Todo valid_paren_cnt_eq: ∀ a, valid_paren a -> cnt '(' a = cnt ')' a; Theorem count_of_lists: ∀ T: U, ∀ S: set T, ∀ m, 0 < m -> |S| = m -> ∀ n, 0 ≤ n -> |{ l: list T | member_set l ⊆ S ∧ |l| = n }| = m ^ n; Proof; From 3ff789b70a251cfe6e85fcbcfe42ba596e6717fa Mon Sep 17 00:00:00 2001 From: hkalbasi Date: Thu, 1 Feb 2024 22:46:51 +0330 Subject: [PATCH 5/5] Add append_len --- library/List.v | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/library/List.v b/library/List.v index f4b368c..73c3569 100644 --- a/library/List.v +++ b/library/List.v @@ -75,8 +75,9 @@ Qed; Todo cons_eq: ∀ T: U, ∀ x y: list T, ∀ a b, a :: x = b :: y -> a = b ∧ x = y; Todo append_eq: ∀ T: U, ∀ a b c d: list T, |a| = |b| -> a + c = b + d -> a = b ∧ c = d; +Todo append_len: ∀ T: U, ∀ a b: list T, |a + b| = |a| + |b|; -Todo tail_len: ∀ T: U, ∀ x: list T, ∀ n: ℤ, |x| = n + 1 → |tail x| = n; +Todo tail_len: ∀ T: U, ∀ x: list T, ∀ n: ℤ, 0 ≤ n -> |x| = n + 1 → |tail x| = n; Suggest goal auto apply tail_len with label Trivial; Theorem list_len_gt_0: ∀ A: U, ∀ x: list A, 0 ≤ |x|;