refactor(library/tools/super): move examples to test folder

library/tools/super/cdcl.lean

@@ -31,19 +31,3 @@ match res with
 end
 
 meta def cdcl : tactic unit := cdcl_t skip
-
-example {a} : a → ¬a → false := by cdcl
-example {a} : a ∨ ¬a := by cdcl
-example {a b} : a → (a → b) → b := by cdcl
-example {a b c} : (a → b) → (¬a → b) → (b → c) → b ∧ c := by cdcl
-
-private meta def lit_unification : tactic unit :=
-do ls ← local_context, first $ do l ← ls, [do apply l, assumption]
-example {p : ℕ → Type _} : p 2 ∨ p 4 → (p (2*2) → p (2+0)) → p (1+1) :=
-by cdcl_t lit_unification
-
-example {p : ℕ → Prop} :
-        list.foldl (λf v, f ∧ (v ∨ ¬v)) true (map p (list.range 5)) :=
-begin (target >>= whnf >>= change), cdcl end
-
-example {a b c : Type _} : (a → b) → (b → c) → (a → c) := by cdcl

library/tools/super/datatypes.lean

@@ -36,15 +36,6 @@ on_right_at' c i $ λhyp,
   | _ := failed
   end
 
-example (x y : ℕ) (h : nat.zero = nat.succ nat.zero) (h2 : nat.succ x = nat.succ y) : true := by do
-h ← get_local `h >>= clause.of_classical_proof,
-h2 ← get_local `h2 >>= clause.of_classical_proof,
-cs ← try_no_confusion_eq_r h 0,
-for' cs clause.validate,
-cs ← try_no_confusion_eq_r h2 0,
-for' cs clause.validate,
-to_expr `(trivial) >>= exact
-
 @[super.inf]
 meta def datatype_infs : inf_decl := inf_decl.mk 10 $ take given, do
 sequence' (do i ← list.range given↣c↣num_lits, [inf_if_successful 0 given $ try_no_confusion_eq_r given↣c i])

library/tools/super/default.lean

@@ -0,0 +1 @@
+import tools.super.prover

library/tools/super/lpo.lean

@@ -33,34 +33,3 @@ let nis := rb_map.of_list (list.zip_with_index ns) in
 | (some si, some ti) := to_bool (si > ti)
 | _ := ff
 end
-
-open tactic
-example (m n : ℕ) : true := by do
-e₁ ← to_expr `((0 + (m : ℕ)) + 0),
-e₂ ← to_expr `(0 + (0 + (m : ℕ))),
-e₃ ← to_expr `(0 + (m : ℕ)),
-prec ← return (contained_funsyms e₁)↣keys,
-prec_gt ← return $ prec_gt_of_name_list prec,
-guard $ lpo prec_gt e₁ e₃,
-guard $ lpo prec_gt e₂ e₃,
-to_expr `(trivial) >>= apply
-
-/-
-open tactic
-example (i : Type) (f : i → i) (c d x : i) : true := by do
-ef ← get_local `f, ec ← get_local `c, ed ← get_local `d,
-syms ← return [ef,ec,ed],
-prec_gt ← return $ prec_gt_of_name_list (list.map local_uniq_name [ef, ec, ed]),
-sequence' (do s1 ← syms, s2 ← syms, return (do
-  s1_fmt ← pp s1, s2_fmt ← pp s2,
-  trace (s1_fmt ++ to_fmt " > " ++ s2_fmt ++ to_fmt ": " ++ to_fmt (prec_gt s1 s2))
-)),
-
-exprs ← @mapM tactic _ _ _ to_expr [`(f c), `(f (f c)), `(f d), `(f x), `(f (f x))],
-sequence' (do e1 ← exprs, e2 ← exprs, return (do
-  e1_fmt ← pp e1, e2_fmt ← pp e2,
-  trace (e1_fmt ++ to_fmt" > " ++ e2_fmt ++ to_fmt": " ++ to_fmt (lpo prec_gt e1 e2))
-)),
-
-mk_const ``true.intro >>= apply
--/

library/tools/super/misc_preprocessing.lean

@@ -10,13 +10,6 @@ return $ list.bor $ do
   l2 ← qf^.1^.get_lits, guard l2^.is_pos,
   [decidable.to_bool $ l1^.formula = l2^.formula]
 
-open tactic
-example (i : Type) (p : i → i → Type) (c : i) (h : ∀ (x : i), p x c → p x c) : true := by do
-h ← get_local `h, hcls ← clause.of_classical_proof h,
-taut ← is_taut hcls,
-when (¬taut) failed,
-to_expr `(trivial) >>= apply
-
 meta def tautology_removal_pre : prover unit :=
 preprocessing_rule $ λnew, filter (λc, lift bnot $♯ is_taut c↣c) new
 

library/tools/super/splitting.lean

@@ -15,18 +15,6 @@ meta def get_components (hs : list expr) : list (list expr) :=
 (find_components hs (hs↣zip_with_index↣for $ λh, [h]))↣for $ λc,
 (sort_on (λh : expr × ℕ, h↣2) c)↣for $ λh, h↣1
 
-example (i : Type) (p q : i → Prop) (H : ∀x y, p x → q y → false) : true := by do
-h ← get_local `H >>= clause.of_classical_proof,
-(op, lcs) ← h↣open_constn h↣num_binders,
-guard $ (get_components lcs)↣length = 2,
-triv
-
-example (i : Type) (p : i → i → Prop) (H : ∀x y z, p x y → p y z → false) : true := by do
-h ← get_local `H >>= clause.of_classical_proof,
-(op, lcs) ← h↣open_constn h↣num_binders,
-guard $ (get_components lcs)↣length = 1,
-triv
-
 meta def extract_assertions : clause → prover (clause × list expr) | c :=
 if c↣num_lits = 0 then return (c, [])
 else if c↣num_quants ≠ 0 then do

library/tools/super/superposition.lean

@@ -80,21 +80,6 @@ new_fin_prf ←
             abs_rwr_ctx, (op2↣1↣close_const hi2)↣proof, new_hi2],
 clause.meta_closure (qf1↣2 ++ qf2↣2) $ (op1↣1↣inst new_fin_prf)↣close_constn (op1↣2 ++ op2↣2↣update_nth i2 new_hi2)
 
-example (i : Type) (a b : i) (p : i → Prop) (H : a = b) (Hpa : p a) : true := by do
-H ← get_local `H >>= clause.of_classical_proof,
-Hpa ← get_local `Hpa >>= clause.of_classical_proof,
-a ← get_local `a,
-try_sup (λx y, ff) H Hpa 0 0 [0] tt ``super.sup_ltr >>= clause.validate,
-to_expr `(trivial) >>= apply
-
-example (i : Type) (a b : i) (p : i → Prop) (H : a = b) (Hpa : p a → false) (Hpb : p b → false) : true := by do
-H ← get_local `H >>= clause.of_classical_proof,
-Hpa ← get_local `Hpa >>= clause.of_classical_proof,
-Hpb ← get_local `Hpb >>= clause.of_classical_proof,
-try_sup (λx y, ff) H Hpa 0 0 [0] tt ``super.sup_ltr >>= clause.validate,
-try_sup (λx y, ff) H Hpb 0 0 [0] ff ``super.sup_rtl >>= clause.validate,
-to_expr `(trivial) >>= apply
-
 meta def rwr_positions (c : clause) (i : nat) : list (list ℕ) :=
 get_rwr_positions (c↣get_lit i)↣formula
 

tests/lean/run/cdcl_examples.lean

@@ -0,0 +1,20 @@
+import tools.super.cdcl
+
+example {a} : a → ¬a → false := by cdcl
+example {a} : a ∨ ¬a := by cdcl
+example {a b} : a → (a → b) → b := by cdcl
+example {a b c} : (a → b) → (¬a → b) → (b → c) → b ∧ c := by cdcl
+
+open tactic monad
+
+private meta def lit_unification : tactic unit :=
+do ls ← local_context, first $ do l ← ls, [do apply l, assumption]
+
+example {p : ℕ → Type _} : p 2 ∨ p 4 → (p (2*2) → p (2+0)) → p (1+1) :=
+by cdcl_t lit_unification
+
+example {p : ℕ → Prop} :
+        list.foldl (λf v, f ∧ (v ∨ ¬v)) true (map p (list.range 5)) :=
+begin (target >>= whnf >>= change), cdcl end
+
+example {a b c : Type _} : (a → b) → (b → c) → (a → c) := by cdcl

tests/lean/run/super_examples.lean

@@ -1,4 +1,4 @@
-import .prover
+import tools.super
 open tactic
 
 constant nat_has_dvd : has_dvd nat

tests/lean/run/super_tests.lean

@@ -0,0 +1,77 @@
+import tools.super
+
+section
+open super tactic
+example (i : Type) (a b : i) (p : i → Prop) (H : a = b) (Hpa : p a) : true := by do
+H ← get_local `H >>= clause.of_classical_proof,
+Hpa ← get_local `Hpa >>= clause.of_classical_proof,
+a ← get_local `a,
+try_sup (λx y, ff) H Hpa 0 0 [0] tt ``super.sup_ltr >>= clause.validate,
+to_expr `(trivial) >>= apply
+
+example (i : Type) (a b : i) (p : i → Prop) (H : a = b) (Hpa : p a → false) (Hpb : p b → false) : true := by do
+H ← get_local `H >>= clause.of_classical_proof,
+Hpa ← get_local `Hpa >>= clause.of_classical_proof,
+Hpb ← get_local `Hpb >>= clause.of_classical_proof,
+try_sup (λx y, ff) H Hpa 0 0 [0] tt ``super.sup_ltr >>= clause.validate,
+try_sup (λx y, ff) H Hpb 0 0 [0] ff ``super.sup_rtl >>= clause.validate,
+to_expr `(trivial) >>= apply
+
+example (i : Type) (p q : i → Prop) (H : ∀x y, p x → q y → false) : true := by do
+h ← get_local `H >>= clause.of_classical_proof,
+(op, lcs) ← h↣open_constn h↣num_binders,
+guard $ (get_components lcs)↣length = 2,
+triv
+
+example (i : Type) (p : i → i → Prop) (H : ∀x y z, p x y → p y z → false) : true := by do
+h ← get_local `H >>= clause.of_classical_proof,
+(op, lcs) ← h↣open_constn h↣num_binders,
+guard $ (get_components lcs)↣length = 1,
+triv
+
+example (i : Type) (p : i → i → Type) (c : i) (h : ∀ (x : i), p x c → p x c) : true := by do
+h ← get_local `h, hcls ← clause.of_classical_proof h,
+taut ← is_taut hcls,
+when (¬taut) failed,
+to_expr `(trivial) >>= apply
+
+open tactic
+example (m n : ℕ) : true := by do
+e₁ ← to_expr `((0 + (m : ℕ)) + 0),
+e₂ ← to_expr `(0 + (0 + (m : ℕ))),
+e₃ ← to_expr `(0 + (m : ℕ)),
+prec ← return (contained_funsyms e₁)↣keys,
+prec_gt ← return $ prec_gt_of_name_list prec,
+guard $ lpo prec_gt e₁ e₃,
+guard $ lpo prec_gt e₂ e₃,
+to_expr `(trivial) >>= apply
+
+/-
+open tactic
+example (i : Type) (f : i → i) (c d x : i) : true := by do
+ef ← get_local `f, ec ← get_local `c, ed ← get_local `d,
+syms ← return [ef,ec,ed],
+prec_gt ← return $ prec_gt_of_name_list (list.map local_uniq_name [ef, ec, ed]),
+sequence' (do s1 ← syms, s2 ← syms, return (do
+  s1_fmt ← pp s1, s2_fmt ← pp s2,
+  trace (s1_fmt ++ to_fmt " > " ++ s2_fmt ++ to_fmt ": " ++ to_fmt (prec_gt s1 s2))
+)),
+
+exprs ← @mapM tactic _ _ _ to_expr [`(f c), `(f (f c)), `(f d), `(f x), `(f (f x))],
+sequence' (do e1 ← exprs, e2 ← exprs, return (do
+  e1_fmt ← pp e1, e2_fmt ← pp e2,
+  trace (e1_fmt ++ to_fmt" > " ++ e2_fmt ++ to_fmt": " ++ to_fmt (lpo prec_gt e1 e2))
+)),
+
+mk_const ``true.intro >>= apply
+-/
+open monad
+example (x y : ℕ) (h : nat.zero = nat.succ nat.zero) (h2 : nat.succ x = nat.succ y) : true := by do
+h ← get_local `h >>= clause.of_classical_proof,
+h2 ← get_local `h2 >>= clause.of_classical_proof,
+cs ← try_no_confusion_eq_r h 0,
+for' cs clause.validate,
+cs ← try_no_confusion_eq_r h2 0,
+for' cs clause.validate,
+to_expr `(trivial) >>= exact
+end