Merge pull request #21 from babaeee/mz3

Mz3
babaeee · Mar 19, 2023 · 598c21c · 598c21c
2 parents 2dcdaff + 9e964b8
commit 598c21c
Show file tree

Hide file tree

Showing 8 changed files with 129 additions and 1 deletion.
diff --git a/front/src/hakim/index.ts b/front/src/hakim/index.ts
@@ -264,6 +264,10 @@ export const spanPosOfHyp = async (
   l: number,
   r: number
 ): Promise<number | undefined> => {
+  if (l == null || r == null || l <= -1 || r <= -1) {
+    alert(`l or r is null or negative. l = ${l}, r = ${r}`);
+    return;
+  }
   const result = await instance.pos_of_span_hyp({ hyp, l, r });
   if (typeof result === "string") {
     alert(result);
@@ -275,6 +279,10 @@ export const spanPosOfGoal = async (
   l: number,
   r: number
 ): Promise<number | undefined> => {
+  if (l == null || r == null || l <= -1 || r <= -1) {
+    alert(`l or r is null or negative. l = ${l}, r = ${r}`);
+    return;
+  }
   const result = await instance.pos_of_span_goal({ l, r });
   if (typeof result === "string") {
     alert(result);

diff --git a/front/src/hakim/lib_text.ts b/front/src/hakim/lib_text.ts
@@ -15,6 +15,7 @@ import Game from "../../../library/Game.v";
 import Tuples from "../../../library/Tuples.v";
 import EnumerativeCombinatorics from "../../../library/EnumerativeCombinatorics.v";
 import Field from "../../../library/Field.v";
+import MetricSpace from "../../../library/MetricSpace.v";
 
 export const loadLibText = () => {
   return {
@@ -35,5 +36,6 @@ export const loadLibText = () => {
     "/Tuples": Tuples,
     "/EnumerativeCombinatorics": EnumerativeCombinatorics,
     "/Field": Field,
+    "/MetricSpace": MetricSpace,
   };
 };
diff --git a/hakim-engine/src/analysis/arith.rs b/hakim-engine/src/analysis/arith.rs
@@ -57,6 +57,14 @@ impl ConstRepr for BigInt {
     fn from_term(term: &Term) -> Option<Self> {
         match term {
             Term::Number { value } => Some(value.clone()),
+            Term::NumberR { value, point } => {
+                let makhraj = BigInt::pow(&10.into(), *point as u32);
+                if value % makhraj.clone() == 0.into() {
+                    Some(value / makhraj)
+                } else {
+                    None
+                }
+            }
             _ => None,
         }
     }
@@ -257,6 +265,21 @@ fn pow_to_arith<N: ConstRepr>(
             return r;
         }
     }
+    if let Some(num) = BigInt::from_term(op2.as_ref()) {
+        if <i32 as Into<BigInt>>::into(-5) <= num && num <= 5i32.into() {
+            let v = i32::abs(num.clone().try_into().unwrap());
+
+            let mut r = Const(1i32.into());
+            let op1a = term_ref_to_arith(op1, arena);
+            for _ in 0i32..v {
+                r = Mult(op1a, arena.alloc(r));
+            }
+            if num.sign() == Sign::Minus {
+                r = Div(arena.alloc(Const(1.into())), arena.alloc(r));
+            }
+            return r;
+        }
+    }
     atom_normalizer(app_ref!(pow(), op1, op2))
 }
 

diff --git a/hakim-engine/src/interactive/tactic/z3_auto.rs b/hakim-engine/src/interactive/tactic/z3_auto.rs
@@ -373,6 +373,17 @@ impl<'a> Z3Manager<'a> {
                                 }
                                 _ => (),
                             },
+                            Term::App { func, op: _ } => {
+                                if let Term::Axiom { unique_name, .. } = func.as_ref() {
+                                    if unique_name == "if_f" {
+                                        let prop = self.covert_prop_to_z3_bool(op.clone())?;
+                                        //let ty = self.convert_sort(ty)?;
+                                        let op1 = self.convert_general_term(op1.clone())?;
+                                        let op2 = self.convert_general_term(op2.clone())?;
+                                        return Some(prop.ite(&op1, &op2));
+                                    }
+                                }
+                            }
                             _ => (),
                         },
                         Term::Axiom { unique_name, .. } => match unique_name.as_str() {
@@ -610,5 +621,6 @@ mod tests {
         success("∀ k p: ℤ, ~ 2 * (2 * k ^ 2 + 2 * k) + 1 = 2 * p");
         success("∀ k: ℤ, True");
         success("∀ p q: ℤ, ~ 2 * gcd p q = 1");
+        success("∀ p q: ℤ, ~ p = q -> if_f (p = q) 1 0 = 0");
     }
 }
diff --git a/hakim-engine/src/parser/tests.rs b/hakim-engine/src/parser/tests.rs
@@ -233,6 +233,7 @@ fn abstr_infer() {
 fn abstr_prec() {
     parse_pretty("(∃ x: ℤ, 2 < x) → 2 | 5");
     parse_pretty("∃ x: ℤ, 2 < x → 2 | 5");
+    parse_pretty("∃ X: U, False");
 }
 
 #[test]

diff --git a/library/MetricSpace.v b/library/MetricSpace.v
@@ -0,0 +1,62 @@
+Definition Metric := λ X:U, λ d: X -> X -> ℝ, ∀ x y z: X, d x x = 0. ∧ d x y ≥ 0. ∧ (d x y = 0. -> x = y) ∧ d x y = d y x ∧ d x z ≤ d x y + d y z;
+
+Todo Metric_unfold: ∀ X: U, ∀ d: X -> X -> ℝ, Metric X d -> ( ∀ x y: X, d x y ≥ 0. ∧ (d x y = 0. -> x = y) ∧ (x = y -> d x y = 0.)) ∧ (∀ x y, d x y = d y x) ∧ (∀ x y z, d x z ≤ d x y + d y z);
+Todo Metric_fold: ∀ X: U, ∀ d: X -> X -> ℝ, (∀ x y z: X, d x x = 0. ∧ d x y ≥ 0. ∧ (d x y = 0. -> x = y) ∧ d x y = d y x ∧ d x z ≤ d x y + d y z) -> Metric X d;
+Suggest hyp default chain (apply Metric_unfold in $n) (destruct $n with (and_ind ? ?) to ($n_no_neg $n)) (destruct $n with (and_ind ? ?) to  ($n_sym $n_triangle_ineq)) with label Metric X d => (∀ x y: X, d x y ≥ 0. ∧ (d x y = 0. -> x = y) ) ∧ (∀ x y, d x y = d y x) ∧ (∀ x y z, d x z ≤ d x y + d y z);
+Suggest goal default apply Metric_fold with label Metric X d => ∀ x y z: X, d x y ≥ 0. ∧ (d x y = 0. -> x = y) ∧ d x y = d y x ∧ d x z ≤ d x y + d y z;
+
+Definition #1 ball := λ X: U, λ d: X → X → ℝ, λ u: X, λ r: ℝ, {x | d u x < r};
+
+Definition #1 open_set := λ X: U, λ d: X → X → ℝ, λ U: set X, ∀ x: X, x ∈ U -> ∃ r: ℝ, r > 0. ∧ (∀ y: X, d x y < r -> y ∈ U);
+Definition #1 is_lim_point := λ X: U, λ d: X → X → ℝ, λ E: set X, λ x: X, ∀ e: ℝ, e > 0. -> ∃ y, y ∈ E ∧ ~ y = x ∧ d x y < e;
+Definition #1 close_set := λ X: U, λ d: X → X → ℝ, λ E: set X, ∀ x, is_lim_point d E x -> x ∈ E;
+
+Todo open_set_unfold: ∀ X: U, ∀ d: X → X → ℝ, ∀ U: set X, open_set d U -> ∀ x: X, x ∈ U -> ∃ r: ℝ, r > 0. ∧ (∀ y: X, d x y < r -> y ∈ U);
+Todo open_set_fold: ∀ X: U, ∀ d: X → X → ℝ, ∀ U: set X, (∀ x: X, x ∈ U -> ∃ r: ℝ, r > 0. ∧ (∀ y: X, d x y < r -> y ∈ U)) -> open_set d U;
+Suggest hyp default apply open_set_unfold in $n with label open_set d U => ∀ x: X, x ∈ U -> ∃ r: ℝ, r > 0. ∧ (∀ y: X, d x y < r -> y ∈ U);
+Suggest goal default apply open_set_fold with label open_set d U => ∀ x: X, x ∈ U -> ∃ r: ℝ, r > 0. ∧ (∀ y: X, d x y < r -> y ∈ U);
+
+Todo is_lim_point_unfold: ∀ X: U, ∀ d: X → X → ℝ, ∀ E: set X, ∀ x: X, is_lim_point d E x -> ∀ e: ℝ, e > 0. -> ∃ y, y ∈ E ∧ ~ y = x ∧ d x y < e;
+Todo is_lim_point_fold: ∀ X: U, ∀ d: X → X → ℝ, ∀ E: set X, ∀ x: X, (∀ e: ℝ, e > 0. -> ∃ y, y ∈ E ∧ ~ y = x ∧ d x y < e) -> is_lim_point d E x;
+Suggest hyp default apply is_lim_point_unfold in $n with label is_lim_point d E x => ∀ e: ℝ, e > 0. -> ∃ y, y ∈ E ∧ ~ y = x ∧ d x y < e;
+Suggest goal default apply is_lim_point_fold with label is_lim_point d E x => ∀ e: ℝ, e > 0. -> ∃ y, y ∈ E ∧ ~ y = x ∧ d x y < e;
+
+Todo close_set_unfold: ∀ X: U, ∀ d: X → X → ℝ, ∀ E: set X, close_set d E -> ∀ x, is_lim_point d E x -> x ∈ E;
+Todo close_set_fold: ∀ X: U, ∀ d: X → X → ℝ, ∀ E: set X, (∀ x, is_lim_point d E x -> x ∈ E) -> close_set d E;
+Suggest hyp default apply close_set_unfold in $n with label close_set d E => ∀ x, is_lim_point d E x -> x ∈ E;
+Suggest goal default apply close_set_fold with label close_set d E => ∀ x, is_lim_point d E x -> x ∈ E;
+
+Import /Set;
+
+Todo close_set_to_open_set: ∀ X: U, ∀ d: X → X → ℝ, ∀ E: set X, open_set d (complement E) -> close_set d E;
+Todo open_set_to_close_set: ∀ X: U, ∀ d: X → X → ℝ, ∀ E: set X, close_set d E -> open_set d (complement E);
+Suggest hyp apply open_set_to_close_set in $n with label close_set d E => open_set d (complement E);
+Suggest goal apply close_set_to_open_set with label close_set d E => open_set d (complement E);
+
+Definition #1 Int := λ X: U, λ d: X → X → ℝ, λ E: set X, {x | ∃ r: ℝ, r > 0. ∧ (∀ y: X, d x y < r -> y ∈ E) };
+Definition #1 Cl := λ X: U, λ d: X → X → ℝ, λ E: set X, {x | x ∈ E ∨ is_lim_point d E x };
+
+Todo Int_unfold: ∀ X: U, ∀ d: X → X → ℝ, ∀ E: set X, ∀ x: X, x ∈ Int d E -> ∃ r: ℝ, r > 0. ∧ (∀ y: X, d x y < r -> y ∈ E);
+Todo Int_fold: ∀ X: U, ∀ d: X → X → ℝ, ∀ E: set X, ∀ x: X, (∃ r: ℝ, r > 0. ∧ (∀ y: X, d x y < r -> y ∈ E)) -> x ∈ Int d E;
+Suggest hyp default apply Int_unfold in $n with label x ∈ Int d E => ∃ r: ℝ, r > 0. ∧ (∀ y: X, d x y < r -> y ∈ E);
+Suggest goal default apply Int_fold with label x ∈ Int d E => ∃ r: ℝ, r > 0. ∧ (∀ y: X, d x y < r -> y ∈ E);
+
+Todo Cl_unfold: ∀ X: U, ∀ d: X → X → ℝ, ∀ E: set X, ∀ x: X, x ∈ Cl d E -> x ∈ E ∨ is_lim_point d E x;
+Todo Cl_fold: ∀ X: U, ∀ d: X → X → ℝ, ∀ E: set X, ∀ x: X, x ∈ E ∨ is_lim_point d E x -> x ∈ Cl d E;
+Suggest hyp default apply Cl_unfold in $n with label x ∈ Cl d E => x ∈ E ∨ is_lim_point d E x;
+Suggest goal default apply Cl_fold with label x ∈ Cl d E => x ∈ E ∨ is_lim_point d E x;
+
+Theorem Int_incl: ∀ X: Universe, ∀ d: X → X → ℝ, Metric X d → ∀ E: set X, Int d E ⊆ E;
+Proof;    
+    intros;
+    apply included_fold ;
+    intros;
+    apply Int_unfold in H0 ;
+    destruct H0 with (ex_ind ? ?) to (ق ق_property);
+    destruct ق_property with (and_ind ? ?) to (ق_property_l ق_property_r) ;
+    add_hyp ق_property_r_ex := (ق_property_r (a));
+    chain (apply Metric_unfold in H) (destruct H with (and_ind ? ?) to (H_no_neg H)) (destruct H with (and_ind ? ?) to  (H_sym H_triangle_ineq)) ;
+    add_hyp H_no_neg_ex := (H_no_neg (a));
+    add_hyp H_no_neg_ex_ex := (H_no_neg_ex (a));
+    z3;
+Qed;
diff --git a/library/RArith.v b/library/RArith.v
@@ -327,4 +327,16 @@ Axiom sup_lub: ∀ E: set ℝ, (∃ x, x ∈ E) -> bounded_abow E -> lub E (sup
 Todo lub_eq_sup: ∀ A: set ℝ, ∀ s, lub A s -> sup A = s;
 Suggest goal apply lub_eq_sup with label sup A = s => lub A s;
 Todo eq_sup_lub: ∀ A: set ℝ, ∀ s, sup A = s -> lub A s;
-Suggest hyp apply eq_sup_lub in $n with label sup A = s => lub A s;
+Suggest hyp apply eq_sup_lub in $n with label sup A = s => lub A s;
+
+Todo ceil: ∀ r: ℝ, ∃ n: ℤ, n / 1 ≥ r∧ n / 1 < r + 1.; 
+Todo lt_pow_lt: ∀ x a b: ℝ, x > 1. -> x ^ a < x ^ b -> a < b;
+Todo lt_pow_gt: ∀ x a b: ℝ, 0. < x -> x < 1. -> x ^ a > x ^ b -> a < b;
+Todo pow_lt_lt: ∀ x a b: ℝ, x > 1. -> a < b -> x ^ a < x ^ b;
+Todo pow_lt_gt: ∀ x a b: ℝ, 0. < x -> x < 1. -> a > b -> x ^ a < x ^ b;
+Todo pow_lt_1: ∀ x a: ℝ, x > 1. -> a > 0. -> x ^ a > 1.;
+Todo pow_plus: ∀ x a b: ℝ, x ≥ 0. -> x ^ (a + b) = x ^ a * x ^ b;
+Todo pow_pow: ∀ x a b: ℝ, x ≥ 0. -> (x ^ a) ^ b = x ^ (a * b);
+
+Suggest goal apply pow_plus with label Trivial;
+Suggest goal apply pow_pow with label Trivial;
diff --git a/library/Set.v b/library/Set.v
@@ -14,6 +14,14 @@ Todo eq_set_empty: ∀ A: U, ∀ S: set A, S = {} -> ∀ a: A, ~ a ∈ S;
 Todo empty_set_eq: ∀ A: U, ∀ S: set A, (∀ x: A, ~ x ∈ S) -> S = {};
 Suggest goal default apply empty_set_eq with label Trivial;
 
+Definition #1 complement := λ A: U, λ x: set A, {a | ~ a ∈ x};
+
+Todo complement_unfold: ∀ A: U, ∀ x: set A, ∀ a: A, a ∈ complement x -> (~ a ∈ x);
+Todo complement_fold: ∀ A: U, ∀ x: set A, ∀ a: A, (~ a ∈ x) -> a ∈ complement x;
+Todo in_complement_detect: ∀ A: U, ∀ x: set A, ∀ a: A, a ∈ complement x -> a ∈ complement x;
+Suggest hyp default chain (apply in_complement_detect in $n) (apply complement_unfold in $n) with label a ∈ complement x => ~ a ∈ x;
+Suggest goal default apply complement_fold with label a ∈ complement x => ~ a ∈ x;
+
 Theorem singleton_unfold: ∀ A: U, ∀ a b: A, b ∈ {a} -> a = b;
 Proof; intros; auto_set; Qed;
 Theorem singleton_fold: ∀ A: U, ∀ a b: A, a = b -> b ∈ {a};