From e5041da652d8968d23b269cd60adef4c6c521c53 Mon Sep 17 00:00:00 2001 From: Claude Date: Sun, 19 Apr 2026 22:44:46 +0000 Subject: [PATCH] feat(corpus): expand synthetic proofs for least-represented provers Grow the per-prover corpora for the four provers with no public downloadable training data (tiny communities, small libraries): Nuprl: 50 -> 152 (+102, +204%) Minlog: 46 -> 148 (+102, +221%) Imandra: 47 -> 133 (+86, +183%) Twelf: 33 -> 118 (+85, +258%) New categories added to scripts/generate_synthetic_provers.jl: Nuprl: sets, relations, number_theory, real_analysis, computability, category_theory, topology, algebra, probability, bishop_analysis, proof_theory, information, quotient_types, w_types Minlog: lists, trees, classical_logic, sequent_calculus, induction_advanced, higher_order, program_verification, modal_logic, intuitionistic, games, realizers_advanced, bounded_arithmetic, finite_logic Twelf: binary_trees, substitution, session_types, linear_lf, metatheory, polymorphism, modules, records, traces, bigstep, hoas, parsing, automata, effects, numerics Imandra: trees, numerics, records, state_machines, crypto, blockchain, algebra, concurrency, databases, networking, security, ml_correctness Regenerated proof_states_{nuprl,minlog,twelf,imandra}.jsonl match the script. https://claude.ai/code/session_0173ntsBsELMiXaTWvtjXdN8 --- scripts/generate_synthetic_provers.jl | 591 +++++++++++++++++++++++ training_data/proof_states_imandra.jsonl | 180 +++++-- training_data/proof_states_minlog.jsonl | 194 ++++++-- training_data/proof_states_nuprl.jsonl | 202 ++++++-- training_data/proof_states_twelf.jsonl | 151 ++++-- 5 files changed, 1142 insertions(+), 176 deletions(-) diff --git a/scripts/generate_synthetic_provers.jl b/scripts/generate_synthetic_provers.jl index f27185c5..aa14f914 100644 --- a/scripts/generate_synthetic_provers.jl +++ b/scripts/generate_synthetic_provers.jl @@ -99,6 +99,150 @@ function generate_nuprl()::Vector{Dict{String,Any}} ("choice_nat", "all R:Nat->Nat->Prop. (all n:Nat. exists m:Nat. R(n,m)) => exists f:Nat->Nat. all n:Nat. R(n, f(n))", "Intro; CountableChoice; Auto"), ("well_ordering_nat", "all P:Nat->Prop. (exists n:Nat. P(n)) => exists m:Nat. P(m) & (all k:Nat. k < m => ~P(k))", "StrongInduction; Auto"), ("brouwer_continuity", "all f:(Nat->Nat)->Nat. exists n:Nat. all a,b:Nat->Nat. (all i:Nat. i < n => a(i) = b(i)) => f(a) = f(b)", "Continuity; Auto"), + ("church_rosser", "all M,N,P:Term. reduces(M, N) => reduces(M, P) => exists Q:Term. reduces(N, Q) & reduces(P, Q)", "Induction; Diamond; Auto"), + ("fan_theorem", "all T:Tree. (all b:Branch. bar(T, b)) => exists n:Nat. uniform_bar(T, n)", "BarInduction; Auto"), + ("kripke_schema", "all A:Prop. (A \\/ ~A) => decidable(A)", "Intro; OrElim; Auto"), + ] + + sets = [ + ("set_ext", "all A:Type, s1,s2:Set(A). (all x:A. x in s1 <=> x in s2) => s1 = s2", "Intro; SetExt; Auto"), + ("union_comm", "all A:Type, s1,s2:Set(A). union(s1, s2) = union(s2, s1)", "SetExt; Auto"), + ("union_assoc", "all A:Type, s1,s2,s3:Set(A). union(union(s1,s2),s3) = union(s1,union(s2,s3))", "SetExt; Auto"), + ("inter_comm", "all A:Type, s1,s2:Set(A). intersect(s1, s2) = intersect(s2, s1)", "SetExt; Auto"), + ("distrib_union_inter", "all A:Type, s1,s2,s3:Set(A). union(s1, intersect(s2, s3)) = intersect(union(s1,s2), union(s1,s3))", "SetExt; Auto"), + ("empty_subset", "all A:Type, s:Set(A). subset(empty, s)", "Intro; ElimEmpty; Auto"), + ("union_superset", "all A:Type, s1,s2:Set(A). subset(s1, union(s1, s2))", "Intro; UnionElim; Auto"), + ("power_set_monotone", "all A:Type, s1,s2:Set(A). subset(s1, s2) => subset(pow(s1), pow(s2))", "Intro; Intro; Apply; Auto"), + ("finite_union", "all A:Type, s1,s2:FiniteSet(A). finite(union(s1, s2))", "Intro; FiniteUnion; Auto"), + ("cardinal_union", "all A:Type, s1,s2:FiniteSet(A). card(union(s1,s2)) = card(s1) + card(s2) - card(intersect(s1,s2))", "InclusionExclusion; Auto"), + ] + + relations = [ + ("refl_closure", "all A:Type, R:A->A->Prop, x:A. refl_trans_closure(R)(x, x)", "Intro; RTC_Refl; Auto"), + ("trans_composition", "all A:Type, R:A->A->Prop, x,y,z:A. trans_closure(R)(x,y) => trans_closure(R)(y,z) => trans_closure(R)(x,z)", "Intro; Induction; Auto"), + ("equiv_sym", "all A:Type, R:A->A->Prop, x,y:A. equivalence(R) => R(x, y) => R(y, x)", "Intro; Intro; ApplySym; Auto"), + ("well_founded_induction", "all A:Type, R:A->A->Prop. well_founded(R) => all P:A->Prop. (all x:A. (all y:A. R(y,x) => P(y)) => P(x)) => all x:A. P(x)", "Intro; WFInduction; Auto"), + ("partial_order_antisym", "all A:Type, R:A->A->Prop, x,y:A. partial_order(R) => R(x,y) => R(y,x) => x = y", "Intro; ApplyAntisym; Auto"), + ("total_order_trichotomy", "all A:Type, R:A->A->Prop, x,y:A. total_order(R) => R(x,y) \\/ x = y \\/ R(y,x)", "Intro; Trichotomy; Auto"), + ("graph_path_compose", "all V:Type, E:V->V->Prop, x,y,z:V. path(E)(x,y) => path(E)(y,z) => path(E)(x,z)", "Induction; Auto"), + ("converse_relation", "all A,B:Type, R:A->B->Prop, x:A, y:B. R(x,y) <=> converse(R)(y,x)", "Intro; Split; Auto"), + ] + + number_theory = [ + ("euclid_lemma", "all p:Prime, a,b:Nat. divides(p, a*b) => divides(p, a) or divides(p, b)", "Intro; CaseGCD; Auto"), + ("fundamental_arith", "all n:Nat. n >= 2 => exists! ps:List(Prime). product(ps) = n", "StrongInduction; Auto"), + ("bezout", "all a,b:Nat. a > 0 \\/ b > 0 => exists x,y:Int. a*x + b*y = gcd(a,b)", "Intro; ExtendedEuclid; Auto"), + ("infinitude_primes", "all n:Nat. exists p:Prime. p > n", "Intro; Witness `factorial(n)+1`; Auto"), + ("wilson_theorem", "all p:Prime. (factorial(p-1) + 1) mod p = 0", "Intro; ModArith; Auto"), + ("fermat_little", "all p:Prime, a:Nat. coprime(a, p) => (a^(p-1)) mod p = 1", "Intro; GroupOrder; Auto"), + ("chinese_remainder", "all m,n:Nat. coprime(m,n) => all a,b:Int. exists x:Int. (x mod m = a) & (x mod n = b)", "Intro; Intro; CRT; Auto"), + ("sum_of_squares", "all n:Nat. (exists a,b:Nat. n = a*a + b*b) <=> all p:Prime. p `divides` n & p mod 4 = 3 => even(mult(p, n))", "Classify; Auto"), + ("pigeon_hole", "all n,m:Nat, f:Fin(n)->Fin(m). n > m => exists i,j:Fin(n). i <> j & f(i) = f(j)", "Intro; PHP; Auto"), + ] + + real_analysis = [ + ("lim_sum", "all f,g:Nat->Real, a,b:Real. lim(f) = a => lim(g) = b => lim(fun n. f(n)+g(n)) = a+b", "Intro; LimitArith; Auto"), + ("lim_prod", "all f,g:Nat->Real, a,b:Real. lim(f) = a => lim(g) = b => lim(fun n. f(n)*g(n)) = a*b", "Intro; LimitArith; Auto"), + ("squeeze", "all f,g,h:Nat->Real. (all n:Nat. f(n) <= g(n) <= h(n)) => lim(f) = lim(h) => lim(g) = lim(f)", "Intro; Squeeze; Auto"), + ("continuous_compose", "all f,g:Real->Real. continuous(f) => continuous(g) => continuous(compose(f, g))", "Intro; EpsilonDelta; Auto"), + ("ivt", "all f:Real->Real, a,b:Real, y:Real. continuous(f) => f(a) <= y <= f(b) => exists c:Real. a <= c <= b & f(c) = y", "Intro; Bisection; Auto"), + ("mvt", "all f:Real->Real, a,b:Real. differentiable(f) => a < b => exists c:Real. a < c < b & derivative(f)(c) = (f(b)-f(a))/(b-a)", "Intro; Rolle; Auto"), + ("cauchy_complete", "all s:Nat->Real. cauchy(s) => exists L:Real. lim(s) = L", "Intro; CompletenessAxiom; Auto"), + ("compact_attains", "all f:Real->Real, K:Set(Real). compact(K) => continuous(f) => exists m,M:Real. m in f(K) & M in f(K) & all y in f(K). m <= y <= M", "Intro; Intro; ExtremeValue; Auto"), + ] + + computability = [ + ("halting_undecidable", "~exists H:(Prog->Input->Bool). all p:Prog, x:Input. H(p, x) = true <=> halts(p, x)", "Diagonalization; Auto"), + ("rice_theorem", "all P:(Prog->Prop). nontrivial(P) => ~decidable(P)", "Intro; Reduction; Auto"), + ("recursion_theorem", "all f:Prog->Prog. exists e:Prog. equal_programs(e, f(e))", "KleeneRecursion; Auto"), + ("smn_theorem", "all n,m:Nat, f:Prog. exists s:Prog. all x,y:Input. run(f, pair(x,y)) = run(run(s, x), y)", "Intro; Intro; SMN; Auto"), + ("kleene_normal", "all f:PartialFn. exists e,U:Prog. all x:Input. f(x) = run(U, pair(e, x))", "Intro; NormalForm; Auto"), + ("church_turing_lambda", "all f:ComputableFn. exists t:Term. reduces_to_numeral(t(numeral(x)), numeral(f(x)))", "Intro; Encode; Auto"), + ] + + category_theory = [ + ("cat_comp_assoc", "all C:Cat, f:Hom(a,b), g:Hom(b,c), h:Hom(c,d). comp(comp(h,g),f) = comp(h,comp(g,f))", "Intro; CatAssoc; Auto"), + ("cat_id_left", "all C:Cat, f:Hom(a,b). comp(id(b), f) = f", "Intro; CatIdLeft; Auto"), + ("cat_id_right", "all C:Cat, f:Hom(a,b). comp(f, id(a)) = f", "Intro; CatIdRight; Auto"), + ("functor_comp", "all F:Functor, f:Hom(a,b), g:Hom(b,c). Fmap(comp(g,f)) = comp(Fmap(g), Fmap(f))", "Intro; FunctorLaw; Auto"), + ("functor_id", "all F:Functor, a:Obj. Fmap(id(a)) = id(Fobj(a))", "Intro; FunctorIdLaw; Auto"), + ("natural_trans", "all F,G:Functor, eta:NatTrans(F,G), f:Hom(a,b). comp(eta(b), Fmap_F(f)) = comp(Fmap_G(f), eta(a))", "Intro; Naturality; Auto"), + ("iso_compose", "all C:Cat, f:Hom(a,b), g:Hom(b,a). comp(g, f) = id(a) => comp(f, g) = id(b) => isomorphism(f)", "Intro; Isomorphism; Auto"), + ("product_universal", "all C:Cat, p:Obj, f:Hom(p,a), g:Hom(p,b). exists! h:Hom(p, prod(a,b)). comp(pi1, h) = f & comp(pi2, h) = g", "Intro; Universal; Auto"), + ] + + topology = [ + ("open_union", "all X:TopSpace, U,V:Open(X). open(union(U, V))", "Intro; OpenAxiom; Auto"), + ("open_finite_inter", "all X:TopSpace, U,V:Open(X). open(intersect(U, V))", "Intro; OpenAxiom; Auto"), + ("continuous_compose", "all X,Y,Z:TopSpace, f:X->Y, g:Y->Z. continuous(f) => continuous(g) => continuous(compose(g, f))", "Intro; Continuous; Auto"), + ("compact_closed", "all X:TopSpace, K:Subspace(X). compact(K) => hausdorff(X) => closed(K)", "Intro; Compact; Auto"), + ("connected_image", "all X,Y:TopSpace, f:X->Y. continuous(f) => connected(X) => connected(image(f))", "Intro; Connected; Auto"), + ("hausdorff_limit", "all X:TopSpace, s:Nat->X, L1,L2:X. hausdorff(X) => lim(s) = L1 => lim(s) = L2 => L1 = L2", "Intro; Hausdorff; Auto"), + ("homeomorphism", "all X,Y:TopSpace, f:X->Y. continuous(f) => continuous(inverse(f)) => homeomorphism(f)", "Intro; Homeomorphism; Auto"), + ] + + algebra = [ + ("group_inv_unique", "all G:Group, a,b,c:G. op(a,b) = e => op(a,c) = e => b = c", "Intro; Cancel; Auto"), + ("subgroup_closed", "all G:Group, H:Subgroup(G), a,b:H. op(a, b) in H", "Intro; SubgroupAxiom; Auto"), + ("lagrange", "all G:FinGroup, H:Subgroup(G). divides(order(H), order(G))", "Intro; Lagrange; Auto"), + ("homomorphism_kernel", "all G,H:Group, f:Homomorphism(G, H). subgroup(kernel(f), G)", "Intro; KernelAxiom; Auto"), + ("ring_add_group", "all R:Ring. group(R, +)", "Intro; RingAxiom; Auto"), + ("ideal_closed", "all R:Ring, I:Ideal(R), a:R, b:I. op(a, b) in I", "Intro; IdealAxiom; Auto"), + ("field_no_zero_div", "all F:Field, a,b:F. a*b = 0 => a = 0 or b = 0", "Intro; FieldAxiom; Auto"), + ("vector_space_sum", "all V:VectorSpace, v,w:V. v + w = w + v", "Intro; VectorAxiom; Auto"), + ] + + probability = [ + ("prob_nonneg", "all P:ProbMeasure, A:Event. P(A) >= 0", "Intro; ProbAxiom; Auto"), + ("prob_total", "all P:ProbMeasure. P(universe) = 1", "Intro; ProbAxiom; Auto"), + ("prob_additivity", "all P:ProbMeasure, A,B:Event. disjoint(A, B) => P(union(A, B)) = P(A) + P(B)", "Intro; Additivity; Auto"), + ("bayes_rule", "all P:ProbMeasure, A,B:Event. P(B) > 0 => P(A | B) = P(A & B) / P(B)", "Intro; BayesDef; Auto"), + ("conditional_indep", "all P:ProbMeasure, A,B,C:Event. indep(A, B | C) <=> P(A & B | C) = P(A | C) * P(B | C)", "Intro; Split; Auto"), + ("markov_ineq", "all X:RandomVar, a:PosReal. P(X >= a) <= E(X) / a", "Intro; Markov; Auto"), + ("expectation_linear", "all X,Y:RandomVar, a,b:Real. E(a*X + b*Y) = a*E(X) + b*E(Y)", "Intro; Linearity; Auto"), + ("variance_nonneg", "all X:RandomVar. var(X) >= 0", "Intro; Variance; Auto"), + ] + + bishop_analysis = [ + ("bishop_real_approx", "all x:Real, n:PosInt. exists q:Rational. abs(x - q) < 1/n", "Intro; ConstructReal; Auto"), + ("bishop_seq_modulus", "all s:Nat->Real, eps:PosReal. cauchy(s) => exists M:Nat. all m,n:Nat. m >= M => n >= M => abs(s(m) - s(n)) < eps", "Intro; Intro; ModulusCauchy; Auto"), + ("bishop_cont_uniform", "all f:Real->Real, K:CompactInterval. continuous(f) => uniformly_continuous_on(f, K)", "Intro; Intro; HeineCantor; Auto"), + ("bishop_rational_dense", "all a,b:Real. a < b => exists q:Rational. a < q < b", "Intro; RationalDensity; Auto"), + ("bishop_sqrt_exists", "all x:NonNegReal. exists y:NonNegReal. y*y = x", "Intro; Newton; Auto"), + ] + + proof_theory = [ + ("cut_elim_nuprl", "all A,B. |- A -> (A |- B) -> |- B", "Intros; CutAdmissible; Auto"), + ("proof_identity", "all A:Prop. |- A -> A", "Intro; Axiom; Auto"), + ("proof_weakening", "all A,B:Prop. |- B => (A |- B)", "Intros; Weakening; Auto"), + ("subtype_refl", "all T:Type. T subtype T", "Intro; SubtypeRefl; Auto"), + ("subtype_trans", "all T1,T2,T3:Type. T1 subtype T2 => T2 subtype T3 => T1 subtype T3", "Intros; SubtypeTrans; Auto"), + ("equality_symmetry", "all A:Type, x,y:A. x = y => y = x", "Intros; EqSym; Auto"), + ("equality_trans", "all A:Type, x,y,z:A. x = y => y = z => x = z", "Intros; EqTrans; Auto"), + ] + + information = [ + ("entropy_nonneg", "all P:ProbDist. entropy(P) >= 0", "Intro; EntropyDef; Auto"), + ("entropy_uniform_max", "all n:PosNat, P:ProbDist(Fin(n)). entropy(P) <= log(n)", "Intro; Intro; MaxEntropy; Auto"), + ("mutual_info_nonneg", "all X,Y:RandomVar. I(X; Y) >= 0", "Intro; MIDef; Auto"), + ("chain_rule_entropy", "all X,Y:RandomVar. H(X, Y) = H(X) + H(Y | X)", "Intro; ChainRule; Auto"), + ("kraft_inequality", "all C:PrefixCode. sum(c in C, 2^(-length(c))) <= 1", "Intro; Kraft; Auto"), + ("source_coding", "all X:RandomVar, eps:PosReal. exists n:PosNat, C:Code. expected_length(C(X^n)) / n <= H(X) + eps", "Intro; ShannonSource; Auto"), + ] + + quotient_types = [ + ("quotient_class", "all A:Type, R:Equiv(A), x,y:A. R(x,y) => [x]_R = [y]_R", "Intros; QuotientEq; Auto"), + ("quotient_lift", "all A,B:Type, R:Equiv(A), f:A->B. (all x,y:A. R(x,y) => f(x) = f(y)) => A/R -> B", "Intros; QuotientLift; Auto"), + ("nat_quot_modp", "all p:PosNat. Nat/cong(p) ~ Fin(p)", "Intro; Bijection; Auto"), + ("partition_quotient", "all A:Type, R:Equiv(A). partition(A, R) <=> A/R", "Intro; Partition; Auto"), + ("setoid_morphism", "all A,B:Setoid, f:A->B. morphism(f) <=> (all x,y:A. eq_A(x,y) => eq_B(f(x), f(y)))", "Intro; Morphism; Auto"), + ] + + w_types = [ + ("w_type", "all A:Type, B:A->Type. W(A, B) : Type", "Intros; WType; Auto"), + ("w_induction", "all A:Type, B:A->Type, P:W(A,B)->Prop. (all a:A, f:B(a)->W(A,B). (all b:B(a). P(f(b))) => P(sup(a, f))) => all w:W(A,B). P(w)", "Intros; WInduction; Auto"), + ("w_nat_iso", "Nat ~ W(Bool, lambda b. if b then Unit else Empty)", "Intro; Bijection; Auto"), + ("w_list_iso", "all A:Type. List(A) ~ W(1 + A, lambda s. match s with inl _ => Empty | inr _ => Unit)", "Intro; Bijection; Auto"), ] all_categories = [ @@ -107,6 +251,20 @@ function generate_nuprl()::Vector{Dict{String,Any}} ("lists", lists), ("logic", logic), ("constructive", constructive), + ("sets", sets), + ("relations", relations), + ("number_theory", number_theory), + ("real_analysis", real_analysis), + ("computability", computability), + ("category_theory", category_theory), + ("topology", topology), + ("algebra", algebra), + ("probability", probability), + ("bishop_analysis", bishop_analysis), + ("proof_theory", proof_theory), + ("information", information), + ("quotient_types", quotient_types), + ("w_types", w_types), ] proofs = Dict{String,Any}[] @@ -200,6 +358,147 @@ function generate_minlog()::Vector{Dict{String,Any}} ("realizer_inl", "[r : A -> A \\/ B] = lambda a. inl(a)", "normalize; refl"), ("realizer_inr", "[r : B -> A \\/ B] = lambda b. inr(b)", "normalize; refl"), ("realizer_case", "[r : (A -> C) -> (B -> C) -> A \\/ B -> C] = lambda f g s. case s of inl(a) => f a | inr(b) => g b", "normalize; refl"), + ("realizer_forall", "[r : (all x:N. A(x))] = lambda x. r_x", "normalize; refl"), + ("realizer_exists", "[r : (ex x:N. A(x))] = (n, proof_of_A(n))", "normalize; refl"), + ("realizer_induction", "[r : nat_rec] = lambda base step n. (rec base step n)", "normalize; refl"), + ] + + lists_minlog = [ + ("list_nil_append", "all l:list. nil ++ l = l", "intro; refl"), + ("list_append_nil", "all l:list. l ++ nil = l", "ind on l; [refl | assume IH; simp; use IH]"), + ("list_append_assoc", "all l1 l2 l3. (l1 ++ l2) ++ l3 = l1 ++ (l2 ++ l3)", "ind on l1; [refl | assume IH; simp; use IH]"), + ("list_length_append", "all l1 l2. length(l1 ++ l2) = length(l1) + length(l2)", "ind on l1; [refl | assume IH; simp; use IH]"), + ("list_rev_involutive", "all l. rev(rev(l)) = l", "ind on l; [refl | assume IH; simp; use rev_append; use IH]"), + ("list_rev_append", "all l1 l2. rev(l1 ++ l2) = rev(l2) ++ rev(l1)", "ind on l1; [simp; use list_append_nil | assume IH; simp; use IH; use list_append_assoc]"), + ("list_map_id", "all l. map(lambda x. x, l) = l", "ind on l; [refl | assume IH; simp; use IH]"), + ("list_map_compose", "all f g l. map(f, map(g, l)) = map(lambda x. f (g x), l)", "ind on l; [refl | assume IH; simp; use IH]"), + ("list_filter_length", "all p l. length(filter(p, l)) <= length(l)", "ind on l; [auto | assume IH; cases p; auto]"), + ("list_foldr_append", "all f z l1 l2. foldr(f, z, l1 ++ l2) = foldr(f, foldr(f, z, l2), l1)", "ind on l1; [refl | assume IH; simp; use IH]"), + ("list_all_forall", "all p l. (all x. mem(x, l) -> p(x)) -> list_all(p, l)", "ind on l; [auto | assume IH; cases; auto]"), + ] + + trees = [ + ("tree_height_nonneg", "all t. height(t) >= 0", "ind on t; auto"), + ("tree_size_nonneg", "all t. size(t) >= 1", "ind on t; auto"), + ("tree_leaves_ge_1", "all t. leaves(t) >= 1", "ind on t; auto"), + ("tree_mirror_involutive", "all t. mirror(mirror(t)) = t", "ind on t; [refl | assume IH1 IH2; simp; use IH1; use IH2]"), + ("tree_size_height", "all t. size(t) <= 2^(height(t)+1) - 1", "ind on t; [auto | assume IH1 IH2; simp; use IH1; use IH2]"), + ("bst_inorder_sorted", "all t. is_bst(t) -> sorted(inorder(t))", "ind on t; [auto | assume IH; split; auto]"), + ("tree_flatten_append", "all t1 t2. flatten(Node(t1, x, t2)) = flatten(t1) ++ [x] ++ flatten(t2)", "intro; refl"), + ("tree_count_sum", "all x t. count(x, flatten(t)) = count_tree(x, t)", "ind on t; auto"), + ] + + classical_logic = [ + ("tnd", "all A. A \\/ ~A", "use classical; auto"), + ("dne", "all A. ~~A -> A", "assume h; classical; auto"), + ("peirce_law", "all A B. ((A -> B) -> A) -> A", "assume h; classical; auto"), + ("contrapos_classical", "all A B. (~B -> ~A) -> (A -> B)", "assume h; classical; auto"), + ("or_impl", "all A B. (A \\/ B) -> (~A -> B)", "assume h nA; elim h; [assume a; absurd | assume b; exact b]"), + ("impl_or", "all A B. (A -> B) -> (~A \\/ B)", "assume h; classical; auto"), + ("and_not_or", "all A B. ~A /\\ ~B -> ~(A \\/ B)", "assume h; elim h; assume nA nB; intro; elim; auto"), + ("demorgan_classical_1", "all A B. ~(A /\\ B) -> (~A \\/ ~B)", "assume h; classical; auto"), + ("demorgan_classical_2", "all A B. ~(A \\/ B) <-> (~A /\\ ~B)", "split; intros; split; intros; auto"), + ("classical_exists", "all P. ~(all x. ~P(x)) -> ex x. P(x)", "assume h; classical; auto"), + ] + + sequent_calculus = [ + ("cut_elim", "all A B C. (Gamma |- A) -> (A, Gamma |- B) -> (Gamma |- B)", "intros; cut_admissible; auto"), + ("structural_weaken", "all A B. (Gamma |- B) -> (A, Gamma |- B)", "intros; weakening; auto"), + ("structural_contract", "all A B. (A, A, Gamma |- B) -> (A, Gamma |- B)", "intros; contraction; auto"), + ("structural_exchange", "all A B C. (A, B, Gamma |- C) -> (B, A, Gamma |- C)", "intros; exchange; auto"), + ("identity_axiom", "all A. (A |- A)", "intro; axiom"), + ("and_right", "all A B. (Gamma |- A) -> (Gamma |- B) -> (Gamma |- A /\\ B)", "intros; andR; auto"), + ("and_left_1", "all A B C. (A, Gamma |- C) -> (A /\\ B, Gamma |- C)", "intros; andL1; auto"), + ("impl_right", "all A B. (A, Gamma |- B) -> (Gamma |- A -> B)", "intros; implR; auto"), + ("impl_left", "all A B C. (Gamma |- A) -> (B, Gamma |- C) -> (A -> B, Gamma |- C)", "intros; implL; auto"), + ] + + induction_advanced = [ + ("strong_ind", "all P. (all n. (all m. m < n -> P(m)) -> P(n)) -> all n. P(n)", "assume h; strong_ind; auto"), + ("course_of_values", "all P. P(0) -> (all n. P(n) -> P(n+1)) -> all n. P(n)", "assume p0 step; nat_rec; auto"), + ("well_founded_acc", "all R. well_founded(R) -> all P. (all x. (all y. R(y,x) -> P(y)) -> P(x)) -> all x. P(x)", "assume wf ih; wf_rec; auto"), + ("mutual_ind_evenodd", "(all n. even(n) -> P(n)) /\\ (all n. odd(n) -> Q(n))", "mutual_ind; auto"), + ("struct_ind_list", "all P. P(nil) -> (all x xs. P(xs) -> P(cons x xs)) -> all l. P(l)", "assume p_nil p_cons; list_rec; auto"), + ("struct_ind_tree", "all P. P(leaf) -> (all t1 x t2. P(t1) -> P(t2) -> P(Node t1 x t2)) -> all t. P(t)", "assume p_leaf p_node; tree_rec; auto"), + ("transfinite_ind", "all P. (all beta. beta < alpha -> P(beta)) -> P(alpha)", "assume ih; transfinite; auto"), + ] + + higher_order = [ + ("higher_order_app", "all f x. (lambda y. f y) x = f x", "beta_reduce; refl"), + ("fun_ext_ho", "all f g. (all x. f x = g x) -> f = g", "assume h; fun_ext; auto"), + ("curry_uncurry", "all f x y. curry (uncurry f) x y = f x y", "intros; beta_reduce; refl"), + ("uncurry_curry", "all f p. uncurry (curry f) p = f p", "intro; cases p; beta_reduce; refl"), + ("compose_assoc", "all f g h. compose (compose f g) h = compose f (compose g h)", "fun_ext; beta_reduce; refl"), + ("id_left", "all f. compose id f = f", "fun_ext; beta_reduce; refl"), + ("id_right", "all f. compose f id = f", "fun_ext; beta_reduce; refl"), + ("ho_induction_schema", "all P. (all x. x = 0 \\/ (ex y. x = y+1 /\\ P(y))) -> P(0) -> all x. P(x)", "assume h p0; induct; auto"), + ] + + program_verification = [ + ("factorial_correct", "all n. factorial(n) >= 1", "ind on n; [simp; auto | assume IH; simp; use IH]"), + ("fibonacci_monotone", "all m n. m <= n -> fib(m) <= fib(n)", "assume h; ind on n; auto"), + ("sum_range_formula", "all n. sum(0..n, lambda i. i) = n * (n+1) / 2", "ind on n; auto"), + ("sort_preserves_elements", "all l. mset(sort l) = mset(l)", "ind on l; auto"), + ("reverse_length", "all l. length(reverse l) = length l", "ind on l; [refl | assume IH; simp; use length_append; use IH]"), + ("gcd_correct", "all a b. b > 0 -> divides(gcd(a,b), a) /\\ divides(gcd(a,b), b)", "strong_ind on b; cases; auto"), + ("is_sorted_cons", "all x xs. is_sorted(cons x xs) -> is_sorted xs", "intros; cases; auto"), + ("search_correct", "all x l. linear_search(x, l) = true <-> mem(x, l)", "ind on l; split; auto"), + ] + + modal_logic = [ + ("modal_k", "all A B. box(A -> B) -> box(A) -> box(B)", "intros; box_elim; auto"), + ("modal_t", "all A. box(A) -> A", "intro; reflexive_frame; auto"), + ("modal_4", "all A. box(A) -> box(box(A))", "intro; transitive_frame; auto"), + ("modal_5", "all A. dia(A) -> box(dia(A))", "intro; euclidean_frame; auto"), + ("modal_dual", "all A. dia(A) <-> ~box(~A)", "split; intros; auto"), + ("necessitation", "all A. |- A -> |- box(A)", "intro; necessitate; auto"), + ("distribution", "all A B. box(A /\\ B) <-> box(A) /\\ box(B)", "split; intros; split; box_elim; auto"), + ] + + intuitionistic = [ + ("disjunction_property", "all A B. (|- A \\/ B) -> (|- A) \\/ (|- B)", "assume h; intuit; auto"), + ("existence_property", "all P. (|- ex x. P(x)) -> ex witness. |- P(witness)", "assume h; intuit; auto"), + ("double_neg_shift", "all A. ~~(A \\/ ~A)", "intro; assume h; apply h; right; intro; apply h; left; auto"), + ("glivenko", "all A. (|- ~~A classically) -> (|- ~~A intuitionistically)", "assume h; glivenko; auto"), + ("kripke_model", "all w:World, A. forces(w, A) <-> satisfies(w, A)", "intro; split; kripke; auto"), + ("negation_translation", "all A. (~~A)_neg = ~~A_neg", "intro; neg_translation; auto"), + ("godel_neg", "all A. valid(A) <-> valid(~~A_neg)", "intro; split; godel_negative; auto"), + ] + + games = [ + ("game_det", "all G:Game. open(G) -> determined(G)", "assume h; gale_stewart; auto"), + ("strategy_winning", "all G:Game, sigma:Strategy. winning(sigma, G) -> all play. consistent(play, sigma) -> G_wins(play)", "assume w; intro con; auto"), + ("zermelo", "all G:FiniteGame. determined(G)", "intro; backward_induction; auto"), + ("minimax", "all G:ZeroSum, v:Value. v = max(min(payoff))", "intro; minimax_theorem; auto"), + ("nash_existence", "all G:FiniteGame. ex sigma. nash_equilibrium(sigma, G)", "intro; brouwer; auto"), + ] + + realizers_advanced = [ + ("realizer_nat_rec", "[r : nat_rec] = lambda base step n. (fix F lambda k. if k=0 then base else step k (F (k-1))) n", "normalize; refl"), + ("realizer_list_rec", "[r : list_rec] = lambda nil_case cons_case l. (fix F lambda xs. match xs with nil => nil_case | x::xs' => cons_case x (F xs')) l", "normalize; refl"), + ("realizer_bounded_search", "[r : bounded_search_lemma] = lambda p bound. search_loop p 0 bound", "normalize; refl"), + ("realizer_minimization", "[r : minimization] = lambda f. mu (lambda n. f n = 0)", "normalize; refl"), + ("realizer_fixpoint", "[r : fix_point_thm] = lambda f. fix f", "normalize; refl"), + ("realizer_choice", "[r : countable_choice] = lambda R. lambda n. choose (R n)", "normalize; refl"), + ] + + bounded_arithmetic = [ + ("bit_length", "all n. n > 0 -> bit_length(n) = floor(log2(n)) + 1", "strong_ind on n; auto"), + ("parity", "all n. parity(n) = n mod 2", "ind on n; auto"), + ("binary_rep", "all n. binary_decode(binary_encode(n)) = n", "ind on n; auto"), + ("pow_two_le", "all n. 2^n > n", "ind on n; auto"), + ("pigeon_bounded", "all f:fin(n)->fin(m). n > m -> ex i j. i <> j /\\ f(i) = f(j)", "assume; pigeonhole; auto"), + ("bounded_search", "all p:nat->bool. (ex n. n <= N /\\ p n = true) -> ex k. k <= N /\\ p k = true /\\ (all j. j < k -> p j = false)", "assume; bounded_search; auto"), + ("pspace_pspace", "pspace = pspace", "refl"), + ] + + finite_logic = [ + ("fin_sat_decidable", "all phi:Formula. decidable(sat(phi))", "intro; propositional_sat; auto"), + ("resolution_sound", "all phi. res_derives(empty, phi) -> unsat(phi)", "assume h; resolution_soundness; auto"), + ("resolution_complete", "all phi. unsat(phi) -> res_derives(empty, phi)", "assume h; resolution_completeness; auto"), + ("dpll_terminates", "all phi. terminates(dpll(phi))", "intro; wf_induct; auto"), + ("cnf_equivalent", "all phi. equivalent(phi, to_cnf(phi))", "intro; tseitin; auto"), + ("horn_sat_poly", "all phi:HornFormula. poly_time_decidable(sat(phi))", "intro; unit_propagation; auto"), ] all_categories = [ @@ -207,6 +506,19 @@ function generate_minlog()::Vector{Dict{String,Any}} ("arithmetic", arithmetic_extraction), ("extraction", program_extraction), ("realizability", realizability), + ("lists", lists_minlog), + ("trees", trees), + ("classical_logic", classical_logic), + ("sequent_calculus", sequent_calculus), + ("induction_advanced", induction_advanced), + ("higher_order", higher_order), + ("program_verification", program_verification), + ("modal_logic", modal_logic), + ("intuitionistic", intuitionistic), + ("games", games), + ("realizers_advanced", realizers_advanced), + ("bounded_arithmetic", bounded_arithmetic), + ("finite_logic", finite_logic), ] proofs = Dict{String,Any}[] @@ -289,11 +601,156 @@ function generate_twelf()::Vector{Dict{String,Any}} ("contra_pf", "contra : pf (imp (imp A B) (imp (not B) (not A))).", "contra = imp-i ([f:pf (imp A B)] imp-i ([nb:pf (not B)] not-i ([a:pf A] not-e nb (imp-e f a))))."), ] + binary_trees = [ + ("tree", "tree : type.", "empty : tree.\nnode : nat -> tree -> tree -> tree."), + ("insert_bst", "insert : nat -> tree -> tree -> type.", "insert-empty : insert X empty (node X empty empty).\ninsert-lt : insert X (node Y L R) (node Y L' R) <- leq X Y <- insert X L L'.\ninsert-gt : insert X (node Y L R) (node Y L R') <- leq Y X <- insert X R R'."), + ("tree_size", "tree-size : tree -> nat -> type.", "tree-size-empty : tree-size empty z.\ntree-size-node : tree-size (node X L R) (s N) <- tree-size L NL <- tree-size R NR <- plus NL NR N."), + ("tree_height", "tree-height : tree -> nat -> type.", "tree-height-empty : tree-height empty z.\ntree-height-node : tree-height (node X L R) (s H) <- tree-height L HL <- tree-height R HR <- max HL HR H."), + ("tree_member", "tree-member : nat -> tree -> type.", "tree-member-node : tree-member X (node X L R).\ntree-member-left : tree-member X (node Y L R) <- tree-member X L.\ntree-member-right : tree-member X (node Y L R) <- tree-member X R."), + ("tree_mirror", "mirror : tree -> tree -> type.", "mirror-empty : mirror empty empty.\nmirror-node : mirror (node X L R) (node X R' L') <- mirror L L' <- mirror R R'."), + ("mirror_involutive", "mirror-involutive : mirror T T' -> mirror T' T -> type.", "%mode mirror-involutive +D1 -D2."), + ("inorder_flatten", "inorder : tree -> list -> type.", "inorder-empty : inorder empty nil.\ninorder-node : inorder (node X L R) M <- inorder L ML <- inorder R MR <- append ML (cons X MR) M."), + ] + + substitution = [ + ("substitution", "subst' : (tm -> tm) -> tm -> tm -> type.", "subst'-id : subst' ([x] x) V V.\nsubst'-const : subst' ([x] C) V C."), + ("capture_avoid", "fresh : tm -> (tm -> tm) -> type.", "fresh-const : fresh V ([x] C).\nfresh-app : fresh V ([x] app (E1 x) (E2 x)) <- fresh V E1 <- fresh V E2."), + ("alpha_eq", "alpha-eq : tm -> tm -> type.", "alpha-eq-refl : alpha-eq E E.\nalpha-eq-lam : alpha-eq (lam T ([x] E x)) (lam T ([y] E y)) <- ({x} alpha-eq (E x) (E x))."), + ("beta_red", "beta-red : tm -> tm -> type.", "beta-red-step : beta-red (app (lam T E) V) (E V) <- value V."), + ("eta_red", "eta-red : tm -> tm -> type.", "eta-red-step : eta-red (lam T ([x] app E x)) E."), + ("subst_lemma", "subst-lemma : subst' E1 V1 E1' -> subst' E2 V2 E2' -> subst' ([x] E1 x) V1 E1'' -> type.", "%mode subst-lemma +D1 +D2 +D3."), + ] + + session_types = [ + ("channel", "chan : type.", "new-chan : chan."), + ("msg_type", "msg : type.", "unit-msg : msg.\nsum-msg : msg -> msg -> msg."), + ("protocol", "proto : type.", "send-proto : msg -> proto -> proto.\nrecv-proto : msg -> proto -> proto.\nend-proto : proto."), + ("duality", "dual : proto -> proto -> type.", "dual-end : dual end-proto end-proto.\ndual-send : dual (send-proto M P) (recv-proto M Q) <- dual P Q.\ndual-recv : dual (recv-proto M P) (send-proto M Q) <- dual P Q."), + ("session_safe", "session-safe : chan -> proto -> type.", "%mode session-safe +C +P."), + ("linear_use", "linear : chan -> type.", "linear-new : linear C <- new-chan."), + ] + + linear_lf = [ + ("linear_type", "ltp : type.", "lolli : ltp -> ltp -> ltp.\ntensor : ltp -> ltp -> ltp.\nwith-type : ltp -> ltp -> ltp.\none-type : ltp."), + ("linear_tm", "ltm : type.", "lapp : ltm -> ltm -> ltm.\nllam : ltp -> (ltm -> ltm) -> ltm.\npair-ltm : ltm -> ltm -> ltm.\nunit-ltm : ltm."), + ("linear_of", "lof : ltm -> ltp -> type.", "lof-lam : lof (llam T1 E) (lolli T1 T2) <- ({x:ltm} lof x T1 -> lof (E x) T2).\nlof-pair : lof (pair-ltm E1 E2) (tensor T1 T2) <- lof E1 T1 <- lof E2 T2.\nlof-unit : lof unit-ltm one-type."), + ("linear_safety", "linear-safety : lof E T -> step E E' -> lof E' T -> type.", "%mode linear-safety +D1 +D2 -D3."), + ("linear_single", "linear-single : ltm -> type.", "linear-single-var : linear-single (var X).\nlinear-single-app : linear-single (lapp E1 E2) <- linear-single E1 <- linear-single E2."), + ] + + metatheory = [ + ("weakening", "weakening : of E T -> of E T -> type.", "%mode weakening +Dof -Dof'."), + ("type_unique", "type-unique : of E T1 -> of E T2 -> eq T1 T2 -> type.", "%mode type-unique +D1 +D2 -D3."), + ("canonical_forms", "canonical : value V -> of V T -> type.", "%mode canonical +Dv +Dof."), + ("progress_lemma", "progress-lemma : of E T -> (value E + step E E') -> type.", "%mode progress-lemma +Dof -Dresult."), + ("preservation_lemma", "preservation-lemma : of E T -> step E E' -> of E' T -> type.", "%mode preservation-lemma +Dof +Dstep -Dof'."), + ("normalization", "strong-norm : of E T -> type.", "%mode strong-norm +Dof."), + ("confluence", "confluence : reduces E E1 -> reduces E E2 -> (reduces E1 E' /\\ reduces E2 E') -> type.", "%mode confluence +D1 +D2 -D3."), + ] + + polymorphism = [ + ("forall_type", "forall-tp : (tp -> tp) -> tp.", "forall-intro : of E (forall-tp A) <- ({X:tp} of E (A X)).\nforall-elim : of (tapp E T) (A T) <- of E (forall-tp A)."), + ("exists_type", "exists-tp : (tp -> tp) -> tp.", "pack : of (pack T E) (exists-tp A) <- of E (A T).\nunpack : of (open E1 [X] [x] E2) C <- of E1 (exists-tp A) <- ({X:tp} {x:tm} of x (A X) -> of (E2 X x) C)."), + ("type_abstraction", "tabs : tp -> (tp -> tm) -> tm.", "of-tabs : of (tabs K E) (forall-tp A) <- ({X:tp} of (E X) (A X))."), + ("param_poly", "parametricity : of E (forall-tp A) -> type.", "%mode parametricity +D."), + ("subtype", "sub : tp -> tp -> type.", "sub-refl : sub T T.\nsub-trans : sub T1 T3 <- sub T1 T2 <- sub T2 T3.\nsub-arrow : sub (arr S1 T1) (arr S2 T2) <- sub S2 S1 <- sub T1 T2."), + ] + + modules = [ + ("module_signature", "module-sig : type.", "mk-sig : list -> module-sig."), + ("module_impl", "module-impl : module-sig -> type.", "mk-impl : list -> module-impl Sig."), + ("functor", "functor : module-sig -> module-sig -> type.", "apply-functor : functor S1 S2 -> module-impl S1 -> module-impl S2 -> type."), + ("abstract_type", "abs-tp : type.", "pack-abs : tp -> (tp -> tp) -> abs-tp.\nopen-abs : abs-tp -> (tp -> tp -> tp) -> tp -> type."), + ("structure_eq", "struct-eq : module-impl S -> module-impl S -> type.", "%mode struct-eq +M1 +M2."), + ("include_module", "include : module-impl S1 -> module-impl S2 -> module-impl S3 -> type.", "%mode include +M1 +M2 -M3."), + ] + + records_twelf = [ + ("record", "record : type.", "empty-rec : record.\ncons-rec : label -> tm -> record -> record."), + ("label", "label : type.", "lab-a : label.\nlab-b : label.\nlab-c : label."), + ("rec_lookup", "lookup : label -> record -> tm -> type.", "lookup-head : lookup L (cons-rec L V R) V.\nlookup-tail : lookup L (cons-rec L' V R) V' <- lookup L R V'."), + ("rec_update", "update : label -> tm -> record -> record -> type.", "update-head : update L V (cons-rec L V' R) (cons-rec L V R).\nupdate-tail : update L V (cons-rec L' V' R) (cons-rec L' V' R') <- update L V R R'."), + ("rec_concat", "rec-concat : record -> record -> record -> type.", "rec-concat-nil : rec-concat empty-rec R R.\nrec-concat-cons : rec-concat (cons-rec L V R1) R2 (cons-rec L V R3) <- rec-concat R1 R2 R3."), + ] + + traces = [ + ("trace", "trace : type.", "empty-trace : trace.\nstep-trace : tm -> tm -> trace -> trace."), + ("trace_step", "trace-step : trace -> tm -> tm -> type.", "%mode trace-step +T +E -E'."), + ("trace_append", "trace-append : trace -> trace -> trace -> type.", "trace-app-nil : trace-append empty-trace T T.\ntrace-app-cons : trace-append (step-trace E1 E2 T1) T2 (step-trace E1 E2 T3) <- trace-append T1 T2 T3."), + ("evaluates", "evaluates : tm -> tm -> type.", "eval-refl : evaluates E E.\neval-step : evaluates E E'' <- step E E' <- evaluates E' E''."), + ("multistep", "multistep : tm -> tm -> trace -> type.", "multistep-refl : multistep E E empty-trace.\nmultistep-step : multistep E E'' (step-trace E E' T) <- step E E' <- multistep E' E'' T."), + ] + + bigstep = [ + ("bigstep", "bigstep : tm -> tm -> type.", "bigstep-val : bigstep V V <- value V.\nbigstep-app : bigstep (app E1 E2) V <- bigstep E1 (lam T E) <- bigstep E2 V2 <- bigstep (E V2) V."), + ("bigstep_det", "bigstep-det : bigstep E V1 -> bigstep E V2 -> eq V1 V2 -> type.", "%mode bigstep-det +D1 +D2 -D3."), + ("bigstep_value", "bigstep-value : bigstep E V -> value V -> type.", "%mode bigstep-value +D -Dv."), + ("bigstep_of", "bigstep-of : bigstep E V -> of E T -> of V T -> type.", "%mode bigstep-of +D1 +D2 -D3."), + ("bigstep_smallstep", "bigstep-smallstep : bigstep E V -> multistep E V _ -> type.", "%mode bigstep-smallstep +D1 -D2."), + ] + + hoas = [ + ("hoas_abs", "habs : (tm -> tm) -> tm.", "habs-intro : of (habs E) (arr T1 T2) <- ({x:tm} of x T1 -> of (E x) T2)."), + ("hoas_app", "happ : tm -> tm -> tm.", "happ-intro : of (happ E1 E2) T2 <- of E1 (arr T1 T2) <- of E2 T1."), + ("hoas_beta", "hstep : tm -> tm -> type.", "hstep-beta : hstep (happ (habs E) V) (E V) <- value V."), + ("hoas_subst", "hsubst : (tm -> tm) -> tm -> tm -> type.", "%mode hsubst +E +V -E'."), + ("parametric_hoas", "phabs : (tm -> tm) -> tm.", "%block phabs-block : block {x:tm}."), + ] + + parsing = [ + ("token", "token : type.", "tok-ident : string -> token.\ntok-num : nat -> token.\ntok-lparen : token.\ntok-rparen : token.\ntok-plus : token.\ntok-times : token."), + ("parse_expr", "parse : list -> tm -> list -> type.", "%mode parse +Input -Result -Rest."), + ("lex", "lex : string -> list -> type.", "%mode lex +Input -Tokens."), + ("ast", "ast : type.", "ast-num : nat -> ast.\nast-var : string -> ast.\nast-bin : op -> ast -> ast -> ast."), + ("op", "op : type.", "op-add : op.\nop-sub : op.\nop-mul : op.\nop-div : op."), + ("grammar", "grammar-rule : type.", "gr-term : symbol -> grammar-rule.\ngr-alt : grammar-rule -> grammar-rule -> grammar-rule.\ngr-seq : grammar-rule -> grammar-rule -> grammar-rule."), + ] + + automata = [ + ("dfa_state", "state : type.", "init-state : state.\ntrans-state : state -> char -> state."), + ("dfa_accept", "accepts : dfa -> string -> type.", "%mode accepts +D +S."), + ("nfa_run", "nfa-run : nfa -> list -> state -> type.", "%mode nfa-run +N +S -Q."), + ("regex", "regex : type.", "re-char : char -> regex.\nre-concat : regex -> regex -> regex.\nre-alt : regex -> regex -> regex.\nre-star : regex -> regex.\nre-epsilon : regex."), + ("regex_match", "re-match : regex -> string -> type.", "%mode re-match +R +S."), + ("pda", "pda-state : type.", "pda-init : pda-state.\npda-push : pda-state -> char -> stack -> pda-state."), + ] + + effects = [ + ("io_monad", "io : type -> type.", "io-return : A -> io A.\nio-bind : io A -> (A -> io B) -> io B."), + ("state_monad", "state-m : type -> type.", "state-return : A -> state-m A.\nstate-bind : state-m A -> (A -> state-m B) -> state-m B.\nstate-get : state-m state.\nstate-put : state -> state-m unit."), + ("exception", "exc : type -> type.", "exc-pure : A -> exc A.\nexc-raise : string -> exc A.\nexc-catch : exc A -> (string -> exc A) -> exc A."), + ("continuation", "cont : type -> type -> type.", "cont-pure : A -> cont A R.\ncont-callcc : ((A -> cont B R) -> cont A R) -> cont A R."), + ("free_monad", "free : type -> type.", "free-pure : A -> free A.\nfree-op : op-sig -> (result -> free A) -> free A."), + ] + + numerics_twelf = [ + ("add_zero_left", "add-zero-left : {N:nat} plus z N N -> type.", "%mode add-zero-left +N -D.\nadd-zero-left-z : add-zero-left z plus-z.\nadd-zero-left-s : add-zero-left (s N) plus-z <- add-zero-left N _."), + ("add_zero_right", "add-zero-right : {N:nat} plus N z N -> type.", "%mode add-zero-right +N -D.\nadd-zero-right-z : add-zero-right z plus-z.\nadd-zero-right-s : add-zero-right (s N) (plus-s D) <- add-zero-right N D."), + ("times_zero_right", "times-zero-right : {N:nat} times N z z -> type.", "%mode times-zero-right +N -D."), + ("div_algorithm", "div-mod : nat -> nat -> nat -> nat -> type.", "div-mod-base : div-mod M N z M <- lt M N.\ndiv-mod-rec : div-mod M N (s Q) R <- leq N M <- sub M N M' <- div-mod M' N Q R."), + ("gcd", "gcd : nat -> nat -> nat -> type.", "gcd-zero : gcd M z M.\ngcd-rec : gcd M N G <- modulo M N R <- gcd N R G."), + ] + all_categories = [ ("natural_numbers", natural_numbers), ("lambda_calculus", lambda_calculus), ("lists", lists), ("logic_framework", logic_framework), + ("binary_trees", binary_trees), + ("substitution", substitution), + ("session_types", session_types), + ("linear_lf", linear_lf), + ("metatheory", metatheory), + ("polymorphism", polymorphism), + ("modules", modules), + ("records", records_twelf), + ("traces", traces), + ("bigstep", bigstep), + ("hoas", hoas), + ("parsing", parsing), + ("automata", automata), + ("effects", effects), + ("numerics", numerics_twelf), ] proofs = Dict{String,Any}[] @@ -386,6 +843,128 @@ function generate_imandra()::Vector{Dict{String,Any}} ("cx_map_injective", "verify (fun f l1 l2 -> List.map f l1 = List.map f l2 ==> l1 = l2)", "CX: f = (fun _ -> 0), l1 = [1], l2 = [2]"), ("cx_sort_idempotent", "verify (fun l -> sort (sort l) = sort l)", "Verified: true (sort is idempotent)"), ("cx_filter_length", "verify (fun p l -> List.length (List.filter p l) <= List.length l)", "Verified: true"), + ("cx_subset_reflexive", "verify (fun s -> subset s s)", "Verified: true"), + ("cx_division_positive", "verify (fun x y -> x > 0 && y > 0 ==> x / y >= 0)", "Verified: true"), + ("cx_int_overflow", "verify (fun (x:int) -> x + 1 > x)", "CX: x = max_int -- overflow wraps to min_int"), + ("cx_float_assoc", "verify (fun (a:float) b c -> (a +. b) +. c = a +. (b +. c))", "CX: a=1e30, b= -1e30, c=1.0 -- floating point not associative"), + ] + + trees_imandra = [ + ("bst_insert_preserves", "theorem bst_insert_preserves x t = is_bst t ==> is_bst (bst_insert x t)", "[@@induct t] [@@auto]"), + ("bst_member_after_insert", "theorem bst_member_after_insert x t = bst_member x (bst_insert x t)", "[@@induct t] [@@auto]"), + ("tree_mirror_involutive", "theorem tree_mirror_involutive t = mirror (mirror t) = t", "[@@induct t]"), + ("tree_size_positive", "theorem tree_size_positive t = tree_size t >= 0", "[@@induct t]"), + ("tree_flatten_length", "theorem tree_flatten_length t = List.length (flatten t) = tree_size t", "[@@induct t]"), + ("heap_extract_min_sorted", "theorem heap_extract_min_sorted h = is_heap h ==> sorted (heapsort h)", "[@@induct h] [@@auto]"), + ("avl_balanced", "theorem avl_balanced t = is_avl t ==> abs (height (left t) - height (right t)) <= 1", "[@@induct t] [@@auto]"), + ("rbt_black_height", "theorem rbt_black_height t = is_rbt t ==> black_height (left t) = black_height (right t)", "[@@induct t] [@@auto]"), + ] + + numerics = [ + ("abs_diff_symmetric", "theorem abs_diff_symmetric x y = abs (x - y) = abs (y - x)", "[@@auto]"), + ("sqr_nonneg", "theorem sqr_nonneg x = x * x >= 0", "[@@auto]"), + ("ge_trans", "theorem ge_trans x y z = x >= y ==> y >= z ==> x >= z", "[@@auto]"), + ("eq_refl_trans", "theorem eq_refl_trans x y = x = y ==> y = x", "[@@auto]"), + ("neg_neg", "theorem neg_neg x = -(-x) = x", "[@@auto]"), + ("sub_self_zero", "theorem sub_self_zero x = x - x = 0", "[@@auto]"), + ("mul_distrib_sub", "theorem mul_distrib_sub x y z = x * (y - z) = x*y - x*z", "[@@auto]"), + ("pow_zero", "theorem pow_zero x = x > 0 ==> x ** 0 = 1", "[@@auto]"), + ("pow_succ", "theorem pow_succ x n = n >= 0 ==> x ** (n+1) = x * (x ** n)", "[@@induct n] [@@auto]"), + ("gcd_self", "theorem gcd_self n = n >= 0 ==> gcd n n = n", "[@@auto]"), + ("gcd_zero", "theorem gcd_zero n = n >= 0 ==> gcd n 0 = n", "[@@auto]"), + ("divides_refl", "theorem divides_refl n = n <> 0 ==> divides n n", "[@@auto]"), + ] + + records = [ + ("record_set_get", "theorem record_set_get r v = (set_field r v).field = v", "[@@auto]"), + ("record_get_set_idempotent", "theorem record_get_set_idempotent r = set_field r (r.field) = r", "[@@auto]"), + ("record_set_comm", "theorem record_set_comm r v1 v2 = set_f2 (set_f1 r v1) v2 = set_f1 (set_f2 r v2) v1", "[@@auto]"), + ("record_eq_fields", "theorem record_eq_fields r1 r2 = r1.a = r2.a ==> r1.b = r2.b ==> r1 = r2", "[@@auto]"), + ("option_some_inj", "theorem option_some_inj x y = Some x = Some y ==> x = y", "[@@auto]"), + ("option_none_not_some", "theorem option_none_not_some x = None <> Some x", "[@@auto]"), + ("tuple_fst_snd", "theorem tuple_fst_snd p = (fst p, snd p) = p", "[@@auto]"), + ] + + state_machines = [ + ("fsm_deterministic", "theorem fsm_deterministic s e = forall s1 s2. transition s e s1 ==> transition s e s2 ==> s1 = s2", "[@@auto]"), + ("fsm_reachable_trans", "theorem fsm_reachable_trans s1 s2 s3 = reachable s1 s2 ==> reachable s2 s3 ==> reachable s1 s3", "[@@induct] [@@auto]"), + ("fsm_initial_reachable", "theorem fsm_initial_reachable s = s = initial_state ==> reachable s s", "[@@auto]"), + ("fsm_no_deadlock", "theorem fsm_no_deadlock s = reachable initial_state s ==> exists e s'. transition s e s'", "[@@auto]"), + ("fsm_invariant_preserve", "theorem fsm_invariant_preserve s e s' = inv s ==> transition s e s' ==> inv s'", "[@@auto]"), + ("safety_property", "theorem safety_property s = reachable initial_state s ==> not (is_error s)", "[@@induct] [@@auto]"), + ("liveness_property", "theorem liveness_property s = reachable initial_state s ==> eventually goal_state s", "[@@auto]"), + ] + + crypto = [ + ("hash_deterministic", "theorem hash_deterministic m1 m2 = m1 = m2 ==> hash m1 = hash m2", "[@@auto]"), + ("signature_verify", "theorem signature_verify sk pk m = keypair sk pk ==> verify pk m (sign sk m) = true", "[@@auto]"), + ("encrypt_decrypt", "theorem encrypt_decrypt k m = decrypt k (encrypt k m) = m", "[@@auto]"), + ("merkle_root_unique", "theorem merkle_root_unique l1 l2 = merkle_root l1 = merkle_root l2 ==> l1 = l2", "[@@auto]"), + ("xor_involutive", "theorem xor_involutive x y = xor (xor x y) y = x", "[@@auto]"), + ("nonce_unique", "theorem nonce_unique n1 n2 = generate_nonce n1 = generate_nonce n2 ==> n1 = n2", "[@@auto]"), + ] + + blockchain = [ + ("block_prev_chain", "theorem block_prev_chain b = valid_chain b ==> prev_hash (head b) = hash (tail b)", "[@@induct b] [@@auto]"), + ("tx_balance_conservation", "theorem tx_balance_conservation tx = valid_tx tx ==> sum_inputs tx = sum_outputs tx + fee tx", "[@@auto]"), + ("utxo_no_double_spend", "theorem utxo_no_double_spend tx1 tx2 utxo = valid_tx tx1 ==> valid_tx tx2 ==> disjoint (inputs tx1) (inputs tx2)", "[@@auto]"), + ("consensus_majority", "theorem consensus_majority votes = count_yes votes > length votes / 2 ==> accepted votes", "[@@auto]"), + ("longest_chain", "theorem longest_chain c1 c2 = valid_chain c1 ==> valid_chain c2 ==> height c1 >= height c2 ==> canonical c1", "[@@auto]"), + ] + + algebra = [ + ("group_identity_unique", "theorem group_identity_unique e1 e2 = is_identity e1 ==> is_identity e2 ==> e1 = e2", "[@@auto]"), + ("group_inverse_unique", "theorem group_inverse_unique a b c = op a b = identity ==> op a c = identity ==> b = c", "[@@auto]"), + ("monoid_left_id", "theorem monoid_left_id a = op identity a = a", "[@@auto]"), + ("monoid_right_id", "theorem monoid_right_id a = op a identity = a", "[@@auto]"), + ("ring_distrib", "theorem ring_distrib a b c = mul a (add b c) = add (mul a b) (mul a c)", "[@@auto]"), + ("ring_zero_mul", "theorem ring_zero_mul a = mul zero a = zero", "[@@auto]"), + ("semilat_idempotent", "theorem semilat_idempotent a = meet a a = a", "[@@auto]"), + ] + + concurrency = [ + ("mutex_exclusive", "theorem mutex_exclusive s = acquired s ==> not (available s)", "[@@auto]"), + ("lock_release", "theorem lock_release s = acquire (release (acquire s)) = acquire s", "[@@auto]"), + ("queue_ordering", "theorem queue_ordering q msgs = push q msgs ==> fifo_order (drain q)", "[@@induct msgs] [@@auto]"), + ("actor_isolation", "theorem actor_isolation a b m = send a b m ==> state a = state a", "[@@auto]"), + ("atomic_read_write", "theorem atomic_read_write x v = read (write x v) = v", "[@@auto]"), + ("cas_success", "theorem cas_success x old new = read x = old ==> cas x old new = (true, write x new)", "[@@auto]"), + ("deadlock_free", "theorem deadlock_free tree = acyclic tree ==> not (deadlocked tree)", "[@@induct tree] [@@auto]"), + ] + + databases = [ + ("acid_atomicity", "theorem acid_atomicity tx db = commit tx db = Some db' \\/ commit tx db = None", "[@@auto]"), + ("rollback_inverse", "theorem rollback_inverse tx db = rollback tx (apply tx db) = db", "[@@auto]"), + ("isolation_serializable", "theorem isolation_serializable t1 t2 db = serializable [t1; t2] db = serializable [t2; t1] db", "[@@auto]"), + ("index_consistent", "theorem index_consistent idx tbl = valid_index idx tbl ==> forall k. lookup idx k = table_lookup tbl k", "[@@auto]"), + ("foreign_key", "theorem foreign_key p c = valid_db (p, c) ==> forall r in c. exists parent in p. fk_match r parent", "[@@auto]"), + ("normalization_bcnf", "theorem normalization_bcnf r = bcnf r ==> third_nf r", "[@@auto]"), + ] + + networking = [ + ("tcp_in_order", "theorem tcp_in_order conn pkts = established conn ==> tcp_deliver conn pkts = sort_by_seq pkts", "[@@induct pkts] [@@auto]"), + ("packet_checksum", "theorem packet_checksum p = valid_packet p ==> verify_checksum p = true", "[@@auto]"), + ("routing_loop_free", "theorem routing_loop_free graph = valid_routing graph ==> acyclic (next_hop graph)", "[@@auto]"), + ("tls_handshake_secrecy", "theorem tls_handshake_secrecy c s = secure_handshake c s ==> secret_key_safe c s", "[@@auto]"), + ("retry_idempotent", "theorem retry_idempotent req = idempotent req ==> retry req = send req", "[@@auto]"), + ] + + security = [ + ("auth_token_valid", "theorem auth_token_valid t = verify_token t = Some user ==> user = decode t", "[@@auto]"), + ("rbac_permission", "theorem rbac_permission u r p = has_role u r && role_has_perm r p ==> authorized u p", "[@@auto]"), + ("password_hash_oneway", "theorem password_hash_oneway p1 p2 = hash_pw p1 = hash_pw p2 ==> p1 = p2 \\/ collision p1 p2", "[@@auto]"), + ("input_sanitize", "theorem input_sanitize s = safe (sanitize s)", "[@@auto]"), + ("session_expiry", "theorem session_expiry s t = expired s t ==> not (valid_session s t)", "[@@auto]"), + ("audit_log_append", "theorem audit_log_append log e = append log e = log ++ [e]", "[@@auto]"), + ] + + ml_correctness = [ + ("gradient_descent_converge", "theorem gd_converge f lr x0 = convex f ==> lr > 0 ==> lr <= 1 / lipschitz f ==> converges (gd f lr x0)", "[@@auto]"), + ("softmax_sum_one", "theorem softmax_sum_one xs = List.length xs > 0 ==> List.fold_left (+.) 0.0 (softmax xs) = 1.0", "[@@auto]"), + ("relu_nonneg", "theorem relu_nonneg x = relu x >= 0.0", "[@@auto]"), + ("sigmoid_bounded", "theorem sigmoid_bounded x = 0.0 <= sigmoid x && sigmoid x <= 1.0", "[@@auto]"), + ("loss_nonneg", "theorem loss_nonneg y y_hat = mse y y_hat >= 0.0", "[@@auto]"), + ("backprop_chain", "theorem backprop_chain f g x = gradient (compose f g) x = gradient f (g x) *. gradient g x", "[@@auto]"), ] all_categories = [ @@ -394,6 +973,18 @@ function generate_imandra()::Vector{Dict{String,Any}} ("verification", verification), ("finance", finance), ("counterexamples", counterexamples), + ("trees", trees_imandra), + ("numerics", numerics), + ("records", records), + ("state_machines", state_machines), + ("crypto", crypto), + ("blockchain", blockchain), + ("algebra", algebra), + ("concurrency", concurrency), + ("databases", databases), + ("networking", networking), + ("security", security), + ("ml_correctness", ml_correctness), ] proofs = Dict{String,Any}[] diff --git a/training_data/proof_states_imandra.jsonl b/training_data/proof_states_imandra.jsonl index b16ea94e..404a8097 100644 --- a/training_data/proof_states_imandra.jsonl +++ b/training_data/proof_states_imandra.jsonl @@ -1,47 +1,133 @@ -{"id": 89500, "prover": "Imandra", "theorem": "add_comm", "goal": "theorem add_comm x y = x + y = y + x", "context": ["auto"], "tactic_proof": "[@@auto]", "source": "imandra_synthetic/arithmetic"} -{"id": 89501, "prover": "Imandra", "theorem": "add_assoc", "goal": "theorem add_assoc x y z = (x + y) + z = x + (y + z)", "context": ["auto"], "tactic_proof": "[@@auto]", "source": "imandra_synthetic/arithmetic"} -{"id": 89502, "prover": "Imandra", "theorem": "mul_comm", "goal": "theorem mul_comm x y = x * y = y * x", "context": ["auto"], "tactic_proof": "[@@auto]", "source": "imandra_synthetic/arithmetic"} -{"id": 89503, "prover": "Imandra", "theorem": "mul_assoc", "goal": "theorem mul_assoc x y z = (x * y) * z = x * (y * z)", "context": ["auto"], "tactic_proof": "[@@auto]", "source": "imandra_synthetic/arithmetic"} -{"id": 89504, "prover": "Imandra", "theorem": "distrib", "goal": "theorem distrib x y z = x * (y + z) = x * y + x * z", "context": ["auto"], "tactic_proof": "[@@auto]", "source": "imandra_synthetic/arithmetic"} -{"id": 89505, "prover": "Imandra", "theorem": "add_zero", "goal": "theorem add_zero x = x + 0 = x", "context": ["auto"], "tactic_proof": "[@@auto]", "source": "imandra_synthetic/arithmetic"} -{"id": 89506, "prover": "Imandra", "theorem": "mul_one", "goal": "theorem mul_one x = x * 1 = x", "context": ["auto"], "tactic_proof": "[@@auto]", "source": "imandra_synthetic/arithmetic"} -{"id": 89507, "prover": "Imandra", "theorem": "mul_zero", "goal": "theorem mul_zero x = x * 0 = 0", "context": ["auto"], "tactic_proof": "[@@auto]", "source": "imandra_synthetic/arithmetic"} -{"id": 89508, "prover": "Imandra", "theorem": "abs_nonneg", "goal": "theorem abs_nonneg x = abs x >= 0", "context": ["auto"], "tactic_proof": "[@@auto]", "source": "imandra_synthetic/arithmetic"} -{"id": 89509, "prover": "Imandra", "theorem": "abs_triangle", "goal": "theorem abs_triangle x y = abs (x + y) <= abs x + abs y", "context": ["auto"], "tactic_proof": "[@@auto]", "source": "imandra_synthetic/arithmetic"} -{"id": 89510, "prover": "Imandra", "theorem": "max_comm", "goal": "theorem max_comm x y = max x y = max y x", "context": ["auto"], "tactic_proof": "[@@auto]", "source": "imandra_synthetic/arithmetic"} -{"id": 89511, "prover": "Imandra", "theorem": "min_comm", "goal": "theorem min_comm x y = min x y = min y x", "context": ["auto"], "tactic_proof": "[@@auto]", "source": "imandra_synthetic/arithmetic"} -{"id": 89512, "prover": "Imandra", "theorem": "max_assoc", "goal": "theorem max_assoc x y z = max x (max y z) = max (max x y) z", "context": ["auto"], "tactic_proof": "[@@auto]", "source": "imandra_synthetic/arithmetic"} -{"id": 89513, "prover": "Imandra", "theorem": "min_max_absorb", "goal": "theorem min_max_absorb x y = min x (max x y) = x", "context": ["auto"], "tactic_proof": "[@@auto]", "source": "imandra_synthetic/arithmetic"} -{"id": 89514, "prover": "Imandra", "theorem": "div_mod_id", "goal": "theorem div_mod_id a b = b > 0 ==> a = b * (a / b) + (a mod b)", "context": ["auto"], "tactic_proof": "[@@auto]", "source": "imandra_synthetic/arithmetic"} -{"id": 89515, "prover": "Imandra", "theorem": "append_nil", "goal": "theorem append_nil l = l @ [] = l", "context": ["auto"], "tactic_proof": "[@@induct l]", "source": "imandra_synthetic/lists"} -{"id": 89516, "prover": "Imandra", "theorem": "append_assoc", "goal": "theorem append_assoc l1 l2 l3 = (l1 @ l2) @ l3 = l1 @ (l2 @ l3)", "context": ["auto"], "tactic_proof": "[@@induct l1]", "source": "imandra_synthetic/lists"} -{"id": 89517, "prover": "Imandra", "theorem": "length_append", "goal": "theorem length_append l1 l2 = List.length (l1 @ l2) = List.length l1 + List.length l2", "context": ["auto"], "tactic_proof": "[@@induct l1]", "source": "imandra_synthetic/lists"} -{"id": 89518, "prover": "Imandra", "theorem": "rev_rev", "goal": "theorem rev_rev l = List.rev (List.rev l) = l", "context": ["auto"], "tactic_proof": "[@@induct l] [@@auto]", "source": "imandra_synthetic/lists"} -{"id": 89519, "prover": "Imandra", "theorem": "map_id", "goal": "theorem map_id l = List.map (fun x -> x) l = l", "context": ["auto"], "tactic_proof": "[@@induct l]", "source": "imandra_synthetic/lists"} -{"id": 89520, "prover": "Imandra", "theorem": "map_compose", "goal": "theorem map_compose f g l = List.map f (List.map g l) = List.map (fun x -> f (g x)) l", "context": ["auto"], "tactic_proof": "[@@induct l]", "source": "imandra_synthetic/lists"} -{"id": 89521, "prover": "Imandra", "theorem": "length_map", "goal": "theorem length_map f l = List.length (List.map f l) = List.length l", "context": ["auto"], "tactic_proof": "[@@induct l]", "source": "imandra_synthetic/lists"} -{"id": 89522, "prover": "Imandra", "theorem": "length_rev", "goal": "theorem length_rev l = List.length (List.rev l) = List.length l", "context": ["auto"], "tactic_proof": "[@@induct l] [@@auto]", "source": "imandra_synthetic/lists"} -{"id": 89523, "prover": "Imandra", "theorem": "mem_append", "goal": "theorem mem_append x l1 l2 = List.mem x (l1 @ l2) = (List.mem x l1 || List.mem x l2)", "context": ["auto"], "tactic_proof": "[@@induct l1]", "source": "imandra_synthetic/lists"} -{"id": 89524, "prover": "Imandra", "theorem": "filter_append", "goal": "theorem filter_append p l1 l2 = List.filter p (l1 @ l2) = List.filter p l1 @ List.filter p l2", "context": ["auto"], "tactic_proof": "[@@induct l1]", "source": "imandra_synthetic/lists"} -{"id": 89525, "prover": "Imandra", "theorem": "flat_map_assoc", "goal": "theorem flat_map_assoc f g l = List.concat_map g (List.concat_map f l) = List.concat_map (fun x -> List.concat_map g (f x)) l", "context": ["auto"], "tactic_proof": "[@@induct l]", "source": "imandra_synthetic/lists"} -{"id": 89526, "prover": "Imandra", "theorem": "nth_map", "goal": "theorem nth_map f l i = i < List.length l ==> List.nth (List.map f l) i = f (List.nth l i)", "context": ["auto"], "tactic_proof": "[@@induct l] [@@auto]", "source": "imandra_synthetic/lists"} -{"id": 89527, "prover": "Imandra", "theorem": "for_all_append", "goal": "theorem for_all_append p l1 l2 = List.for_all p (l1 @ l2) = (List.for_all p l1 && List.for_all p l2)", "context": ["auto"], "tactic_proof": "[@@induct l1]", "source": "imandra_synthetic/lists"} -{"id": 89528, "prover": "Imandra", "theorem": "sorted_insert", "goal": "theorem sorted_insert x l = sorted l ==> sorted (insert x l)", "context": ["auto"], "tactic_proof": "[@@induct l] [@@auto]", "source": "imandra_synthetic/verification"} -{"id": 89529, "prover": "Imandra", "theorem": "sorted_sort", "goal": "theorem sorted_sort l = sorted (sort l)", "context": ["auto"], "tactic_proof": "[@@induct l] [@@auto]", "source": "imandra_synthetic/verification"} -{"id": 89530, "prover": "Imandra", "theorem": "perm_sort", "goal": "theorem perm_sort l = is_perm l (sort l)", "context": ["auto"], "tactic_proof": "[@@induct l] [@@auto]", "source": "imandra_synthetic/verification"} -{"id": 89531, "prover": "Imandra", "theorem": "bsearch_correct", "goal": "theorem bsearch_correct a v = sorted a ==> (match bsearch a v with Some i -> a.(i) = v | None -> not (Array.exists (fun x -> x = v) a))", "context": ["auto"], "tactic_proof": "[@@auto]", "source": "imandra_synthetic/verification"} -{"id": 89532, "prover": "Imandra", "theorem": "stack_push_pop", "goal": "theorem stack_push_pop x s = pop (push x s) = (x, s)", "context": ["auto"], "tactic_proof": "[@@auto]", "source": "imandra_synthetic/verification"} -{"id": 89533, "prover": "Imandra", "theorem": "queue_fifo", "goal": "theorem queue_fifo x q = not (is_empty q) ==> fst (dequeue (enqueue x q)) = front q", "context": ["auto"], "tactic_proof": "[@@auto]", "source": "imandra_synthetic/verification"} -{"id": 89534, "prover": "Imandra", "theorem": "rbt_invariant", "goal": "theorem rbt_invariant x t = is_rbt t ==> is_rbt (rbt_insert x t)", "context": ["auto"], "tactic_proof": "[@@induct t] [@@auto]", "source": "imandra_synthetic/verification"} -{"id": 89535, "prover": "Imandra", "theorem": "bst_invariant", "goal": "theorem bst_invariant x t = is_bst t ==> is_bst (bst_insert x t)", "context": ["auto"], "tactic_proof": "[@@induct t] [@@auto]", "source": "imandra_synthetic/verification"} -{"id": 89536, "prover": "Imandra", "theorem": "heap_insert_min", "goal": "theorem heap_insert_min x h = is_heap h ==> find_min (heap_insert x h) <= x", "context": ["auto"], "tactic_proof": "[@@induct h] [@@auto]", "source": "imandra_synthetic/verification"} -{"id": 89537, "prover": "Imandra", "theorem": "margin_nonneg", "goal": "theorem margin_nonneg acct = valid_account acct ==> margin_requirement acct >= 0.0", "context": ["auto"], "tactic_proof": "[@@auto]", "source": "imandra_synthetic/finance"} -{"id": 89538, "prover": "Imandra", "theorem": "order_fill_balance", "goal": "theorem order_fill_balance order book = valid_order order ==> balance_after (fill order book) >= 0.0", "context": ["auto"], "tactic_proof": "[@@auto]", "source": "imandra_synthetic/finance"} -{"id": 89539, "prover": "Imandra", "theorem": "matching_symmetric", "goal": "theorem matching_symmetric buy sell = can_match buy sell ==> can_match sell buy", "context": ["auto"], "tactic_proof": "[@@auto]", "source": "imandra_synthetic/finance"} -{"id": 89540, "prover": "Imandra", "theorem": "settlement_complete", "goal": "theorem settlement_complete trades = all_valid trades ==> is_settled (settle trades)", "context": ["auto"], "tactic_proof": "[@@auto]", "source": "imandra_synthetic/finance"} -{"id": 89541, "prover": "Imandra", "theorem": "risk_monotone", "goal": "theorem risk_monotone p1 p2 = portfolio_subset p1 p2 ==> risk p1 <= risk p2", "context": ["auto"], "tactic_proof": "[@@auto]", "source": "imandra_synthetic/finance"} -{"id": 89542, "prover": "Imandra", "theorem": "cx_list_rev_sorted", "goal": "verify (fun l -> sorted l ==> sorted (List.rev l))", "context": ["auto"], "tactic_proof": "CX: l = [1; 3; 2] -- List.rev [1;3;2] = [2;3;1] which is not sorted", "source": "imandra_synthetic/counterexamples"} -{"id": 89543, "prover": "Imandra", "theorem": "cx_append_comm", "goal": "verify (fun l1 l2 -> l1 @ l2 = l2 @ l1)", "context": ["auto"], "tactic_proof": "CX: l1 = [1], l2 = [2] -- [1;2] <> [2;1]", "source": "imandra_synthetic/counterexamples"} -{"id": 89544, "prover": "Imandra", "theorem": "cx_map_injective", "goal": "verify (fun f l1 l2 -> List.map f l1 = List.map f l2 ==> l1 = l2)", "context": ["auto"], "tactic_proof": "CX: f = (fun _ -> 0), l1 = [1], l2 = [2]", "source": "imandra_synthetic/counterexamples"} -{"id": 89545, "prover": "Imandra", "theorem": "cx_sort_idempotent", "goal": "verify (fun l -> sort (sort l) = sort l)", "context": ["auto"], "tactic_proof": "Verified: true (sort is idempotent)", "source": "imandra_synthetic/counterexamples"} -{"id": 89546, "prover": "Imandra", "theorem": "cx_filter_length", "goal": "verify (fun p l -> List.length (List.filter p l) <= List.length l)", "context": ["auto"], "tactic_proof": "Verified: true", "source": "imandra_synthetic/counterexamples"} +{"id":89500,"prover":"Imandra","theorem":"add_comm","goal":"theorem add_comm x y = x + y = y + x","context":["auto"],"tactic_proof":"[@@auto]","source":"imandra_synthetic/arithmetic"} +{"id":89501,"prover":"Imandra","theorem":"add_assoc","goal":"theorem add_assoc x y z = (x + y) + z = x + (y + z)","context":["auto"],"tactic_proof":"[@@auto]","source":"imandra_synthetic/arithmetic"} +{"id":89502,"prover":"Imandra","theorem":"mul_comm","goal":"theorem mul_comm x y = x * y = y * x","context":["auto"],"tactic_proof":"[@@auto]","source":"imandra_synthetic/arithmetic"} +{"id":89503,"prover":"Imandra","theorem":"mul_assoc","goal":"theorem mul_assoc x y z = (x * y) * z = x * (y * z)","context":["auto"],"tactic_proof":"[@@auto]","source":"imandra_synthetic/arithmetic"} +{"id":89504,"prover":"Imandra","theorem":"distrib","goal":"theorem distrib x y z = x * (y + z) = x * y + x * z","context":["auto"],"tactic_proof":"[@@auto]","source":"imandra_synthetic/arithmetic"} +{"id":89505,"prover":"Imandra","theorem":"add_zero","goal":"theorem add_zero x = x + 0 = x","context":["auto"],"tactic_proof":"[@@auto]","source":"imandra_synthetic/arithmetic"} +{"id":89506,"prover":"Imandra","theorem":"mul_one","goal":"theorem mul_one x = x * 1 = x","context":["auto"],"tactic_proof":"[@@auto]","source":"imandra_synthetic/arithmetic"} +{"id":89507,"prover":"Imandra","theorem":"mul_zero","goal":"theorem mul_zero x = x * 0 = 0","context":["auto"],"tactic_proof":"[@@auto]","source":"imandra_synthetic/arithmetic"} +{"id":89508,"prover":"Imandra","theorem":"abs_nonneg","goal":"theorem abs_nonneg x = abs x >= 0","context":["auto"],"tactic_proof":"[@@auto]","source":"imandra_synthetic/arithmetic"} +{"id":89509,"prover":"Imandra","theorem":"abs_triangle","goal":"theorem abs_triangle x y = abs (x + y) <= abs x + abs y","context":["auto"],"tactic_proof":"[@@auto]","source":"imandra_synthetic/arithmetic"} +{"id":89510,"prover":"Imandra","theorem":"max_comm","goal":"theorem max_comm x y = max x y = max y x","context":["auto"],"tactic_proof":"[@@auto]","source":"imandra_synthetic/arithmetic"} +{"id":89511,"prover":"Imandra","theorem":"min_comm","goal":"theorem min_comm x y = min x y = min y x","context":["auto"],"tactic_proof":"[@@auto]","source":"imandra_synthetic/arithmetic"} +{"id":89512,"prover":"Imandra","theorem":"max_assoc","goal":"theorem max_assoc x y z = max x (max y z) = max (max x y) z","context":["auto"],"tactic_proof":"[@@auto]","source":"imandra_synthetic/arithmetic"} +{"id":89513,"prover":"Imandra","theorem":"min_max_absorb","goal":"theorem min_max_absorb x y = min x (max x y) = x","context":["auto"],"tactic_proof":"[@@auto]","source":"imandra_synthetic/arithmetic"} +{"id":89514,"prover":"Imandra","theorem":"div_mod_id","goal":"theorem div_mod_id a b = b > 0 ==> a = b * (a / b) + (a mod b)","context":["auto"],"tactic_proof":"[@@auto]","source":"imandra_synthetic/arithmetic"} +{"id":89515,"prover":"Imandra","theorem":"append_nil","goal":"theorem append_nil l = l @ [] = l","context":["auto"],"tactic_proof":"[@@induct l]","source":"imandra_synthetic/lists"} +{"id":89516,"prover":"Imandra","theorem":"append_assoc","goal":"theorem append_assoc l1 l2 l3 = (l1 @ l2) @ l3 = l1 @ (l2 @ l3)","context":["auto"],"tactic_proof":"[@@induct l1]","source":"imandra_synthetic/lists"} +{"id":89517,"prover":"Imandra","theorem":"length_append","goal":"theorem length_append l1 l2 = List.length (l1 @ l2) = List.length l1 + List.length l2","context":["auto"],"tactic_proof":"[@@induct l1]","source":"imandra_synthetic/lists"} +{"id":89518,"prover":"Imandra","theorem":"rev_rev","goal":"theorem rev_rev l = List.rev (List.rev l) = l","context":["auto"],"tactic_proof":"[@@induct l] [@@auto]","source":"imandra_synthetic/lists"} +{"id":89519,"prover":"Imandra","theorem":"map_id","goal":"theorem map_id l = List.map (fun x -> x) l = l","context":["auto"],"tactic_proof":"[@@induct l]","source":"imandra_synthetic/lists"} +{"id":89520,"prover":"Imandra","theorem":"map_compose","goal":"theorem map_compose f g l = List.map f (List.map g l) = List.map (fun x -> f (g x)) l","context":["auto"],"tactic_proof":"[@@induct l]","source":"imandra_synthetic/lists"} +{"id":89521,"prover":"Imandra","theorem":"length_map","goal":"theorem length_map f l = List.length (List.map f l) = List.length l","context":["auto"],"tactic_proof":"[@@induct l]","source":"imandra_synthetic/lists"} +{"id":89522,"prover":"Imandra","theorem":"length_rev","goal":"theorem length_rev l = List.length (List.rev l) = List.length l","context":["auto"],"tactic_proof":"[@@induct l] [@@auto]","source":"imandra_synthetic/lists"} +{"id":89523,"prover":"Imandra","theorem":"mem_append","goal":"theorem mem_append x l1 l2 = List.mem x (l1 @ l2) = (List.mem x l1 || List.mem x l2)","context":["auto"],"tactic_proof":"[@@induct l1]","source":"imandra_synthetic/lists"} +{"id":89524,"prover":"Imandra","theorem":"filter_append","goal":"theorem filter_append p l1 l2 = List.filter p (l1 @ l2) = List.filter p l1 @ List.filter p l2","context":["auto"],"tactic_proof":"[@@induct l1]","source":"imandra_synthetic/lists"} +{"id":89525,"prover":"Imandra","theorem":"flat_map_assoc","goal":"theorem flat_map_assoc f g l = List.concat_map g (List.concat_map f l) = List.concat_map (fun x -> List.concat_map g (f x)) l","context":["auto"],"tactic_proof":"[@@induct l]","source":"imandra_synthetic/lists"} +{"id":89526,"prover":"Imandra","theorem":"nth_map","goal":"theorem nth_map f l i = i < List.length l ==> List.nth (List.map f l) i = f (List.nth l i)","context":["auto"],"tactic_proof":"[@@induct l] [@@auto]","source":"imandra_synthetic/lists"} +{"id":89527,"prover":"Imandra","theorem":"for_all_append","goal":"theorem for_all_append p l1 l2 = List.for_all p (l1 @ l2) = (List.for_all p l1 && List.for_all p l2)","context":["auto"],"tactic_proof":"[@@induct l1]","source":"imandra_synthetic/lists"} +{"id":89528,"prover":"Imandra","theorem":"sorted_insert","goal":"theorem sorted_insert x l = sorted l ==> sorted (insert x l)","context":["auto"],"tactic_proof":"[@@induct l] [@@auto]","source":"imandra_synthetic/verification"} +{"id":89529,"prover":"Imandra","theorem":"sorted_sort","goal":"theorem sorted_sort l = sorted (sort l)","context":["auto"],"tactic_proof":"[@@induct l] [@@auto]","source":"imandra_synthetic/verification"} +{"id":89530,"prover":"Imandra","theorem":"perm_sort","goal":"theorem perm_sort l = is_perm l (sort l)","context":["auto"],"tactic_proof":"[@@induct l] [@@auto]","source":"imandra_synthetic/verification"} +{"id":89531,"prover":"Imandra","theorem":"bsearch_correct","goal":"theorem bsearch_correct a v = sorted a ==> (match bsearch a v with Some i -> a.(i) = v | None -> not (Array.exists (fun x -> x = v) a))","context":["auto"],"tactic_proof":"[@@auto]","source":"imandra_synthetic/verification"} +{"id":89532,"prover":"Imandra","theorem":"stack_push_pop","goal":"theorem stack_push_pop x s = pop (push x s) = (x, s)","context":["auto"],"tactic_proof":"[@@auto]","source":"imandra_synthetic/verification"} +{"id":89533,"prover":"Imandra","theorem":"queue_fifo","goal":"theorem queue_fifo x q = not (is_empty q) ==> fst (dequeue (enqueue x q)) = front q","context":["auto"],"tactic_proof":"[@@auto]","source":"imandra_synthetic/verification"} +{"id":89534,"prover":"Imandra","theorem":"rbt_invariant","goal":"theorem rbt_invariant x t = is_rbt t ==> is_rbt (rbt_insert x t)","context":["auto"],"tactic_proof":"[@@induct t] [@@auto]","source":"imandra_synthetic/verification"} +{"id":89535,"prover":"Imandra","theorem":"bst_invariant","goal":"theorem bst_invariant x t = is_bst t ==> is_bst (bst_insert x t)","context":["auto"],"tactic_proof":"[@@induct t] [@@auto]","source":"imandra_synthetic/verification"} +{"id":89536,"prover":"Imandra","theorem":"heap_insert_min","goal":"theorem heap_insert_min x h = is_heap h ==> find_min (heap_insert x h) <= x","context":["auto"],"tactic_proof":"[@@induct h] [@@auto]","source":"imandra_synthetic/verification"} +{"id":89537,"prover":"Imandra","theorem":"margin_nonneg","goal":"theorem margin_nonneg acct = valid_account acct ==> margin_requirement acct >= 0.0","context":["auto"],"tactic_proof":"[@@auto]","source":"imandra_synthetic/finance"} +{"id":89538,"prover":"Imandra","theorem":"order_fill_balance","goal":"theorem order_fill_balance order book = valid_order order ==> balance_after (fill order book) >= 0.0","context":["auto"],"tactic_proof":"[@@auto]","source":"imandra_synthetic/finance"} +{"id":89539,"prover":"Imandra","theorem":"matching_symmetric","goal":"theorem matching_symmetric buy sell = can_match buy sell ==> can_match sell buy","context":["auto"],"tactic_proof":"[@@auto]","source":"imandra_synthetic/finance"} +{"id":89540,"prover":"Imandra","theorem":"settlement_complete","goal":"theorem settlement_complete trades = all_valid trades ==> is_settled (settle trades)","context":["auto"],"tactic_proof":"[@@auto]","source":"imandra_synthetic/finance"} +{"id":89541,"prover":"Imandra","theorem":"risk_monotone","goal":"theorem risk_monotone p1 p2 = portfolio_subset p1 p2 ==> risk p1 <= risk p2","context":["auto"],"tactic_proof":"[@@auto]","source":"imandra_synthetic/finance"} +{"id":89542,"prover":"Imandra","theorem":"cx_list_rev_sorted","goal":"verify (fun l -> sorted l ==> sorted (List.rev l))","context":["auto"],"tactic_proof":"CX: l = [1; 3; 2] -- List.rev [1;3;2] = [2;3;1] which is not sorted","source":"imandra_synthetic/counterexamples"} +{"id":89543,"prover":"Imandra","theorem":"cx_append_comm","goal":"verify (fun l1 l2 -> l1 @ l2 = l2 @ l1)","context":["auto"],"tactic_proof":"CX: l1 = [1], l2 = [2] -- [1;2] <> [2;1]","source":"imandra_synthetic/counterexamples"} +{"id":89544,"prover":"Imandra","theorem":"cx_map_injective","goal":"verify (fun f l1 l2 -> List.map f l1 = List.map f l2 ==> l1 = l2)","context":["auto"],"tactic_proof":"CX: f = (fun _ -> 0), l1 = [1], l2 = [2]","source":"imandra_synthetic/counterexamples"} +{"id":89545,"prover":"Imandra","theorem":"cx_sort_idempotent","goal":"verify (fun l -> sort (sort l) = sort l)","context":["auto"],"tactic_proof":"Verified: true (sort is idempotent)","source":"imandra_synthetic/counterexamples"} +{"id":89546,"prover":"Imandra","theorem":"cx_filter_length","goal":"verify (fun p l -> List.length (List.filter p l) <= List.length l)","context":["auto"],"tactic_proof":"Verified: true","source":"imandra_synthetic/counterexamples"} +{"id":89547,"prover":"Imandra","theorem":"cx_subset_reflexive","goal":"verify (fun s -> subset s s)","context":["auto"],"tactic_proof":"Verified: true","source":"imandra_synthetic/counterexamples"} +{"id":89548,"prover":"Imandra","theorem":"cx_division_positive","goal":"verify (fun x y -> x > 0 && y > 0 ==> x / y >= 0)","context":["auto"],"tactic_proof":"Verified: true","source":"imandra_synthetic/counterexamples"} +{"id":89549,"prover":"Imandra","theorem":"cx_int_overflow","goal":"verify (fun (x:int) -> x + 1 > x)","context":["auto"],"tactic_proof":"CX: x = max_int -- overflow wraps to min_int","source":"imandra_synthetic/counterexamples"} +{"id":89550,"prover":"Imandra","theorem":"cx_float_assoc","goal":"verify (fun (a:float) b c -> (a +. b) +. c = a +. (b +. c))","context":["auto"],"tactic_proof":"CX: a=1e30, b= -1e30, c=1.0 -- floating point not associative","source":"imandra_synthetic/counterexamples"} +{"id":89551,"prover":"Imandra","theorem":"bst_insert_preserves","goal":"theorem bst_insert_preserves x t = is_bst t ==> is_bst (bst_insert x t)","context":["auto"],"tactic_proof":"[@@induct t] [@@auto]","source":"imandra_synthetic/trees_imandra"} +{"id":89552,"prover":"Imandra","theorem":"bst_member_after_insert","goal":"theorem bst_member_after_insert x t = bst_member x (bst_insert x t)","context":["auto"],"tactic_proof":"[@@induct t] [@@auto]","source":"imandra_synthetic/trees_imandra"} +{"id":89553,"prover":"Imandra","theorem":"tree_mirror_involutive","goal":"theorem tree_mirror_involutive t = mirror (mirror t) = t","context":["auto"],"tactic_proof":"[@@induct t]","source":"imandra_synthetic/trees_imandra"} +{"id":89554,"prover":"Imandra","theorem":"tree_size_positive","goal":"theorem tree_size_positive t = tree_size t >= 0","context":["auto"],"tactic_proof":"[@@induct t]","source":"imandra_synthetic/trees_imandra"} +{"id":89555,"prover":"Imandra","theorem":"tree_flatten_length","goal":"theorem tree_flatten_length t = List.length (flatten t) = tree_size t","context":["auto"],"tactic_proof":"[@@induct t]","source":"imandra_synthetic/trees_imandra"} +{"id":89556,"prover":"Imandra","theorem":"heap_extract_min_sorted","goal":"theorem heap_extract_min_sorted h = is_heap h ==> sorted (heapsort h)","context":["auto"],"tactic_proof":"[@@induct h] [@@auto]","source":"imandra_synthetic/trees_imandra"} +{"id":89557,"prover":"Imandra","theorem":"avl_balanced","goal":"theorem avl_balanced t = is_avl t ==> abs (height (left t) - height (right t)) <= 1","context":["auto"],"tactic_proof":"[@@induct t] [@@auto]","source":"imandra_synthetic/trees_imandra"} +{"id":89558,"prover":"Imandra","theorem":"rbt_black_height","goal":"theorem rbt_black_height t = is_rbt t ==> black_height (left t) = black_height (right t)","context":["auto"],"tactic_proof":"[@@induct t] [@@auto]","source":"imandra_synthetic/trees_imandra"} +{"id":89559,"prover":"Imandra","theorem":"abs_diff_symmetric","goal":"theorem abs_diff_symmetric x y = abs (x - y) = abs (y - x)","context":["auto"],"tactic_proof":"[@@auto]","source":"imandra_synthetic/numerics"} +{"id":89560,"prover":"Imandra","theorem":"sqr_nonneg","goal":"theorem sqr_nonneg x = x * x >= 0","context":["auto"],"tactic_proof":"[@@auto]","source":"imandra_synthetic/numerics"} +{"id":89561,"prover":"Imandra","theorem":"ge_trans","goal":"theorem ge_trans x y z = x >= y ==> y >= z ==> x >= z","context":["auto"],"tactic_proof":"[@@auto]","source":"imandra_synthetic/numerics"} +{"id":89562,"prover":"Imandra","theorem":"eq_refl_trans","goal":"theorem eq_refl_trans x y = x = y ==> y = x","context":["auto"],"tactic_proof":"[@@auto]","source":"imandra_synthetic/numerics"} +{"id":89563,"prover":"Imandra","theorem":"neg_neg","goal":"theorem neg_neg x = -(-x) = x","context":["auto"],"tactic_proof":"[@@auto]","source":"imandra_synthetic/numerics"} +{"id":89564,"prover":"Imandra","theorem":"sub_self_zero","goal":"theorem sub_self_zero x = x - x = 0","context":["auto"],"tactic_proof":"[@@auto]","source":"imandra_synthetic/numerics"} +{"id":89565,"prover":"Imandra","theorem":"mul_distrib_sub","goal":"theorem mul_distrib_sub x y z = x * (y - z) = x*y - x*z","context":["auto"],"tactic_proof":"[@@auto]","source":"imandra_synthetic/numerics"} +{"id":89566,"prover":"Imandra","theorem":"pow_zero","goal":"theorem pow_zero x = x > 0 ==> x ** 0 = 1","context":["auto"],"tactic_proof":"[@@auto]","source":"imandra_synthetic/numerics"} +{"id":89567,"prover":"Imandra","theorem":"pow_succ","goal":"theorem pow_succ x n = n >= 0 ==> x ** (n+1) = x * (x ** n)","context":["auto"],"tactic_proof":"[@@induct n] [@@auto]","source":"imandra_synthetic/numerics"} +{"id":89568,"prover":"Imandra","theorem":"gcd_self","goal":"theorem gcd_self n = n >= 0 ==> gcd n n = n","context":["auto"],"tactic_proof":"[@@auto]","source":"imandra_synthetic/numerics"} +{"id":89569,"prover":"Imandra","theorem":"gcd_zero","goal":"theorem gcd_zero n = n >= 0 ==> gcd n 0 = n","context":["auto"],"tactic_proof":"[@@auto]","source":"imandra_synthetic/numerics"} +{"id":89570,"prover":"Imandra","theorem":"divides_refl","goal":"theorem divides_refl n = n <> 0 ==> divides n n","context":["auto"],"tactic_proof":"[@@auto]","source":"imandra_synthetic/numerics"} +{"id":89571,"prover":"Imandra","theorem":"record_set_get","goal":"theorem record_set_get r v = (set_field r v).field = v","context":["auto"],"tactic_proof":"[@@auto]","source":"imandra_synthetic/records"} +{"id":89572,"prover":"Imandra","theorem":"record_get_set_idempotent","goal":"theorem record_get_set_idempotent r = set_field r (r.field) = r","context":["auto"],"tactic_proof":"[@@auto]","source":"imandra_synthetic/records"} +{"id":89573,"prover":"Imandra","theorem":"record_set_comm","goal":"theorem record_set_comm r v1 v2 = set_f2 (set_f1 r v1) v2 = set_f1 (set_f2 r v2) v1","context":["auto"],"tactic_proof":"[@@auto]","source":"imandra_synthetic/records"} +{"id":89574,"prover":"Imandra","theorem":"record_eq_fields","goal":"theorem record_eq_fields r1 r2 = r1.a = r2.a ==> r1.b = r2.b ==> r1 = r2","context":["auto"],"tactic_proof":"[@@auto]","source":"imandra_synthetic/records"} +{"id":89575,"prover":"Imandra","theorem":"option_some_inj","goal":"theorem option_some_inj x y = Some x = Some y ==> x = y","context":["auto"],"tactic_proof":"[@@auto]","source":"imandra_synthetic/records"} +{"id":89576,"prover":"Imandra","theorem":"option_none_not_some","goal":"theorem option_none_not_some x = None <> Some x","context":["auto"],"tactic_proof":"[@@auto]","source":"imandra_synthetic/records"} +{"id":89577,"prover":"Imandra","theorem":"tuple_fst_snd","goal":"theorem tuple_fst_snd p = (fst p, snd p) = p","context":["auto"],"tactic_proof":"[@@auto]","source":"imandra_synthetic/records"} +{"id":89578,"prover":"Imandra","theorem":"fsm_deterministic","goal":"theorem fsm_deterministic s e = forall s1 s2. transition s e s1 ==> transition s e s2 ==> s1 = s2","context":["auto"],"tactic_proof":"[@@auto]","source":"imandra_synthetic/state_machines"} +{"id":89579,"prover":"Imandra","theorem":"fsm_reachable_trans","goal":"theorem fsm_reachable_trans s1 s2 s3 = reachable s1 s2 ==> reachable s2 s3 ==> reachable s1 s3","context":["induct","auto"],"tactic_proof":"[@@induct] [@@auto]","source":"imandra_synthetic/state_machines"} +{"id":89580,"prover":"Imandra","theorem":"fsm_initial_reachable","goal":"theorem fsm_initial_reachable s = s = initial_state ==> reachable s s","context":["auto"],"tactic_proof":"[@@auto]","source":"imandra_synthetic/state_machines"} +{"id":89581,"prover":"Imandra","theorem":"fsm_no_deadlock","goal":"theorem fsm_no_deadlock s = reachable initial_state s ==> exists e s'. transition s e s'","context":["auto"],"tactic_proof":"[@@auto]","source":"imandra_synthetic/state_machines"} +{"id":89582,"prover":"Imandra","theorem":"fsm_invariant_preserve","goal":"theorem fsm_invariant_preserve s e s' = inv s ==> transition s e s' ==> inv s'","context":["auto"],"tactic_proof":"[@@auto]","source":"imandra_synthetic/state_machines"} +{"id":89583,"prover":"Imandra","theorem":"safety_property","goal":"theorem safety_property s = reachable initial_state s ==> not (is_error s)","context":["induct","auto"],"tactic_proof":"[@@induct] [@@auto]","source":"imandra_synthetic/state_machines"} +{"id":89584,"prover":"Imandra","theorem":"liveness_property","goal":"theorem liveness_property s = reachable initial_state s ==> eventually goal_state s","context":["auto"],"tactic_proof":"[@@auto]","source":"imandra_synthetic/state_machines"} +{"id":89585,"prover":"Imandra","theorem":"hash_deterministic","goal":"theorem hash_deterministic m1 m2 = m1 = m2 ==> hash m1 = hash m2","context":["auto"],"tactic_proof":"[@@auto]","source":"imandra_synthetic/crypto"} +{"id":89586,"prover":"Imandra","theorem":"signature_verify","goal":"theorem signature_verify sk pk m = keypair sk pk ==> verify pk m (sign sk m) = true","context":["auto"],"tactic_proof":"[@@auto]","source":"imandra_synthetic/crypto"} +{"id":89587,"prover":"Imandra","theorem":"encrypt_decrypt","goal":"theorem encrypt_decrypt k m = decrypt k (encrypt k m) = m","context":["auto"],"tactic_proof":"[@@auto]","source":"imandra_synthetic/crypto"} +{"id":89588,"prover":"Imandra","theorem":"merkle_root_unique","goal":"theorem merkle_root_unique l1 l2 = merkle_root l1 = merkle_root l2 ==> l1 = l2","context":["auto"],"tactic_proof":"[@@auto]","source":"imandra_synthetic/crypto"} +{"id":89589,"prover":"Imandra","theorem":"xor_involutive","goal":"theorem xor_involutive x y = xor (xor x y) y = x","context":["auto"],"tactic_proof":"[@@auto]","source":"imandra_synthetic/crypto"} +{"id":89590,"prover":"Imandra","theorem":"nonce_unique","goal":"theorem nonce_unique n1 n2 = generate_nonce n1 = generate_nonce n2 ==> n1 = n2","context":["auto"],"tactic_proof":"[@@auto]","source":"imandra_synthetic/crypto"} +{"id":89591,"prover":"Imandra","theorem":"block_prev_chain","goal":"theorem block_prev_chain b = valid_chain b ==> prev_hash (head b) = hash (tail b)","context":["auto"],"tactic_proof":"[@@induct b] [@@auto]","source":"imandra_synthetic/blockchain"} +{"id":89592,"prover":"Imandra","theorem":"tx_balance_conservation","goal":"theorem tx_balance_conservation tx = valid_tx tx ==> sum_inputs tx = sum_outputs tx + fee tx","context":["auto"],"tactic_proof":"[@@auto]","source":"imandra_synthetic/blockchain"} +{"id":89593,"prover":"Imandra","theorem":"utxo_no_double_spend","goal":"theorem utxo_no_double_spend tx1 tx2 utxo = valid_tx tx1 ==> valid_tx tx2 ==> disjoint (inputs tx1) (inputs tx2)","context":["auto"],"tactic_proof":"[@@auto]","source":"imandra_synthetic/blockchain"} +{"id":89594,"prover":"Imandra","theorem":"consensus_majority","goal":"theorem consensus_majority votes = count_yes votes > length votes / 2 ==> accepted votes","context":["auto"],"tactic_proof":"[@@auto]","source":"imandra_synthetic/blockchain"} +{"id":89595,"prover":"Imandra","theorem":"longest_chain","goal":"theorem longest_chain c1 c2 = valid_chain c1 ==> valid_chain c2 ==> height c1 >= height c2 ==> canonical c1","context":["auto"],"tactic_proof":"[@@auto]","source":"imandra_synthetic/blockchain"} +{"id":89596,"prover":"Imandra","theorem":"group_identity_unique","goal":"theorem group_identity_unique e1 e2 = is_identity e1 ==> is_identity e2 ==> e1 = e2","context":["auto"],"tactic_proof":"[@@auto]","source":"imandra_synthetic/algebra"} +{"id":89597,"prover":"Imandra","theorem":"group_inverse_unique","goal":"theorem group_inverse_unique a b c = op a b = identity ==> op a c = identity ==> b = c","context":["auto"],"tactic_proof":"[@@auto]","source":"imandra_synthetic/algebra"} +{"id":89598,"prover":"Imandra","theorem":"monoid_left_id","goal":"theorem monoid_left_id a = op identity a = a","context":["auto"],"tactic_proof":"[@@auto]","source":"imandra_synthetic/algebra"} +{"id":89599,"prover":"Imandra","theorem":"monoid_right_id","goal":"theorem monoid_right_id a = op a identity = a","context":["auto"],"tactic_proof":"[@@auto]","source":"imandra_synthetic/algebra"} +{"id":89600,"prover":"Imandra","theorem":"ring_distrib","goal":"theorem ring_distrib a b c = mul a (add b c) = add (mul a b) (mul a c)","context":["auto"],"tactic_proof":"[@@auto]","source":"imandra_synthetic/algebra"} +{"id":89601,"prover":"Imandra","theorem":"ring_zero_mul","goal":"theorem ring_zero_mul a = mul zero a = zero","context":["auto"],"tactic_proof":"[@@auto]","source":"imandra_synthetic/algebra"} +{"id":89602,"prover":"Imandra","theorem":"semilat_idempotent","goal":"theorem semilat_idempotent a = meet a a = a","context":["auto"],"tactic_proof":"[@@auto]","source":"imandra_synthetic/algebra"} +{"id":89603,"prover":"Imandra","theorem":"mutex_exclusive","goal":"theorem mutex_exclusive s = acquired s ==> not (available s)","context":["auto"],"tactic_proof":"[@@auto]","source":"imandra_synthetic/concurrency"} +{"id":89604,"prover":"Imandra","theorem":"lock_release","goal":"theorem lock_release s = acquire (release (acquire s)) = acquire s","context":["auto"],"tactic_proof":"[@@auto]","source":"imandra_synthetic/concurrency"} +{"id":89605,"prover":"Imandra","theorem":"queue_ordering","goal":"theorem queue_ordering q msgs = push q msgs ==> fifo_order (drain q)","context":["auto"],"tactic_proof":"[@@induct msgs] [@@auto]","source":"imandra_synthetic/concurrency"} +{"id":89606,"prover":"Imandra","theorem":"actor_isolation","goal":"theorem actor_isolation a b m = send a b m ==> state a = state a","context":["auto"],"tactic_proof":"[@@auto]","source":"imandra_synthetic/concurrency"} +{"id":89607,"prover":"Imandra","theorem":"atomic_read_write","goal":"theorem atomic_read_write x v = read (write x v) = v","context":["auto"],"tactic_proof":"[@@auto]","source":"imandra_synthetic/concurrency"} +{"id":89608,"prover":"Imandra","theorem":"cas_success","goal":"theorem cas_success x old new = read x = old ==> cas x old new = (true, write x new)","context":["auto"],"tactic_proof":"[@@auto]","source":"imandra_synthetic/concurrency"} +{"id":89609,"prover":"Imandra","theorem":"deadlock_free","goal":"theorem deadlock_free tree = acyclic tree ==> not (deadlocked tree)","context":["auto"],"tactic_proof":"[@@induct tree] [@@auto]","source":"imandra_synthetic/concurrency"} +{"id":89610,"prover":"Imandra","theorem":"acid_atomicity","goal":"theorem acid_atomicity tx db = commit tx db = Some db' \\/ commit tx db = None","context":["auto"],"tactic_proof":"[@@auto]","source":"imandra_synthetic/databases"} +{"id":89611,"prover":"Imandra","theorem":"rollback_inverse","goal":"theorem rollback_inverse tx db = rollback tx (apply tx db) = db","context":["auto"],"tactic_proof":"[@@auto]","source":"imandra_synthetic/databases"} +{"id":89612,"prover":"Imandra","theorem":"isolation_serializable","goal":"theorem isolation_serializable t1 t2 db = serializable [t1; t2] db = serializable [t2; t1] db","context":["auto"],"tactic_proof":"[@@auto]","source":"imandra_synthetic/databases"} +{"id":89613,"prover":"Imandra","theorem":"index_consistent","goal":"theorem index_consistent idx tbl = valid_index idx tbl ==> forall k. lookup idx k = table_lookup tbl k","context":["auto"],"tactic_proof":"[@@auto]","source":"imandra_synthetic/databases"} +{"id":89614,"prover":"Imandra","theorem":"foreign_key","goal":"theorem foreign_key p c = valid_db (p, c) ==> forall r in c. exists parent in p. fk_match r parent","context":["auto"],"tactic_proof":"[@@auto]","source":"imandra_synthetic/databases"} +{"id":89615,"prover":"Imandra","theorem":"normalization_bcnf","goal":"theorem normalization_bcnf r = bcnf r ==> third_nf r","context":["auto"],"tactic_proof":"[@@auto]","source":"imandra_synthetic/databases"} +{"id":89616,"prover":"Imandra","theorem":"tcp_in_order","goal":"theorem tcp_in_order conn pkts = established conn ==> tcp_deliver conn pkts = sort_by_seq pkts","context":["auto"],"tactic_proof":"[@@induct pkts] [@@auto]","source":"imandra_synthetic/networking"} +{"id":89617,"prover":"Imandra","theorem":"packet_checksum","goal":"theorem packet_checksum p = valid_packet p ==> verify_checksum p = true","context":["auto"],"tactic_proof":"[@@auto]","source":"imandra_synthetic/networking"} +{"id":89618,"prover":"Imandra","theorem":"routing_loop_free","goal":"theorem routing_loop_free graph = valid_routing graph ==> acyclic (next_hop graph)","context":["auto"],"tactic_proof":"[@@auto]","source":"imandra_synthetic/networking"} +{"id":89619,"prover":"Imandra","theorem":"tls_handshake_secrecy","goal":"theorem tls_handshake_secrecy c s = secure_handshake c s ==> secret_key_safe c s","context":["auto"],"tactic_proof":"[@@auto]","source":"imandra_synthetic/networking"} +{"id":89620,"prover":"Imandra","theorem":"retry_idempotent","goal":"theorem retry_idempotent req = idempotent req ==> retry req = send req","context":["auto"],"tactic_proof":"[@@auto]","source":"imandra_synthetic/networking"} +{"id":89621,"prover":"Imandra","theorem":"auth_token_valid","goal":"theorem auth_token_valid t = verify_token t = Some user ==> user = decode t","context":["auto"],"tactic_proof":"[@@auto]","source":"imandra_synthetic/security"} +{"id":89622,"prover":"Imandra","theorem":"rbac_permission","goal":"theorem rbac_permission u r p = has_role u r && role_has_perm r p ==> authorized u p","context":["auto"],"tactic_proof":"[@@auto]","source":"imandra_synthetic/security"} +{"id":89623,"prover":"Imandra","theorem":"password_hash_oneway","goal":"theorem password_hash_oneway p1 p2 = hash_pw p1 = hash_pw p2 ==> p1 = p2 \\/ collision p1 p2","context":["auto"],"tactic_proof":"[@@auto]","source":"imandra_synthetic/security"} +{"id":89624,"prover":"Imandra","theorem":"input_sanitize","goal":"theorem input_sanitize s = safe (sanitize s)","context":["auto"],"tactic_proof":"[@@auto]","source":"imandra_synthetic/security"} +{"id":89625,"prover":"Imandra","theorem":"session_expiry","goal":"theorem session_expiry s t = expired s t ==> not (valid_session s t)","context":["auto"],"tactic_proof":"[@@auto]","source":"imandra_synthetic/security"} +{"id":89626,"prover":"Imandra","theorem":"audit_log_append","goal":"theorem audit_log_append log e = append log e = log ++ [e]","context":["auto"],"tactic_proof":"[@@auto]","source":"imandra_synthetic/security"} +{"id":89627,"prover":"Imandra","theorem":"gradient_descent_converge","goal":"theorem gd_converge f lr x0 = convex f ==> lr > 0 ==> lr <= 1 / lipschitz f ==> converges (gd f lr x0)","context":["auto"],"tactic_proof":"[@@auto]","source":"imandra_synthetic/ml_correctness"} +{"id":89628,"prover":"Imandra","theorem":"softmax_sum_one","goal":"theorem softmax_sum_one xs = List.length xs > 0 ==> List.fold_left (+.) 0.0 (softmax xs) = 1.0","context":["auto"],"tactic_proof":"[@@auto]","source":"imandra_synthetic/ml_correctness"} +{"id":89629,"prover":"Imandra","theorem":"relu_nonneg","goal":"theorem relu_nonneg x = relu x >= 0.0","context":["auto"],"tactic_proof":"[@@auto]","source":"imandra_synthetic/ml_correctness"} +{"id":89630,"prover":"Imandra","theorem":"sigmoid_bounded","goal":"theorem sigmoid_bounded x = 0.0 <= sigmoid x && sigmoid x <= 1.0","context":["auto"],"tactic_proof":"[@@auto]","source":"imandra_synthetic/ml_correctness"} +{"id":89631,"prover":"Imandra","theorem":"loss_nonneg","goal":"theorem loss_nonneg y y_hat = mse y y_hat >= 0.0","context":["auto"],"tactic_proof":"[@@auto]","source":"imandra_synthetic/ml_correctness"} +{"id":89632,"prover":"Imandra","theorem":"backprop_chain","goal":"theorem backprop_chain f g x = gradient (compose f g) x = gradient f (g x) *. gradient g x","context":["auto"],"tactic_proof":"[@@auto]","source":"imandra_synthetic/ml_correctness"} diff --git a/training_data/proof_states_minlog.jsonl b/training_data/proof_states_minlog.jsonl index 1f3dbab8..8e26368b 100644 --- a/training_data/proof_states_minlog.jsonl +++ b/training_data/proof_states_minlog.jsonl @@ -1,46 +1,148 @@ -{"id": 88500, "prover": "Minlog", "theorem": "imp_refl", "goal": "A -> A", "context": ["assume A", "exact A"], "tactic_proof": "assume A; exact A", "source": "minlog_synthetic/natural_deduction"} -{"id": 88501, "prover": "Minlog", "theorem": "imp_trans", "goal": "(A -> B) -> (B -> C) -> A -> C", "context": ["assume f", "assume g", "assume a", "exact (g (f a))"], "tactic_proof": "assume f; assume g; assume a; exact (g (f a))", "source": "minlog_synthetic/natural_deduction"} -{"id": 88502, "prover": "Minlog", "theorem": "and_intro", "goal": "A -> B -> A /\\ B", "context": ["assume a", "assume b", "split", "exact a", "exact b"], "tactic_proof": "assume a; assume b; split; [exact a | exact b]", "source": "minlog_synthetic/natural_deduction"} -{"id": 88503, "prover": "Minlog", "theorem": "and_elim_l", "goal": "A /\\ B -> A", "context": ["assume h", "elim h", "assume a", "assume b", "exact a"], "tactic_proof": "assume h; elim h; assume a; assume b; exact a", "source": "minlog_synthetic/natural_deduction"} -{"id": 88504, "prover": "Minlog", "theorem": "and_elim_r", "goal": "A /\\ B -> B", "context": ["assume h", "elim h", "assume a", "assume b", "exact b"], "tactic_proof": "assume h; elim h; assume a; assume b; exact b", "source": "minlog_synthetic/natural_deduction"} -{"id": 88505, "prover": "Minlog", "theorem": "or_intro_l", "goal": "A -> A \\/ B", "context": ["assume a", "left", "exact a"], "tactic_proof": "assume a; left; exact a", "source": "minlog_synthetic/natural_deduction"} -{"id": 88506, "prover": "Minlog", "theorem": "or_intro_r", "goal": "B -> A \\/ B", "context": ["assume b", "right", "exact b"], "tactic_proof": "assume b; right; exact b", "source": "minlog_synthetic/natural_deduction"} -{"id": 88507, "prover": "Minlog", "theorem": "or_elim", "goal": "(A -> C) -> (B -> C) -> A \\/ B -> C", "context": ["assume f", "assume g", "assume h", "elim h", "assume a", "exact (f a)", "assume b", "exact (g b)"], "tactic_proof": "assume f; assume g; assume h; elim h; [assume a; exact (f a) | assume b; exact (g b)]", "source": "minlog_synthetic/natural_deduction"} -{"id": 88508, "prover": "Minlog", "theorem": "false_elim", "goal": "F -> A", "context": ["assume h", "elim h"], "tactic_proof": "assume h; elim h", "source": "minlog_synthetic/natural_deduction"} -{"id": 88509, "prover": "Minlog", "theorem": "not_intro", "goal": "(A -> F) -> ~A", "context": ["assume f", "intro", "exact f"], "tactic_proof": "assume f; intro; exact f", "source": "minlog_synthetic/natural_deduction"} -{"id": 88510, "prover": "Minlog", "theorem": "double_neg_intro", "goal": "A -> ~~A", "context": ["assume a", "assume h", "exact (h a)"], "tactic_proof": "assume a; assume h; exact (h a)", "source": "minlog_synthetic/natural_deduction"} -{"id": 88511, "prover": "Minlog", "theorem": "contrapositive", "goal": "(A -> B) -> ~B -> ~A", "context": ["assume f", "assume nb", "assume a", "exact (nb (f a))"], "tactic_proof": "assume f; assume nb; assume a; exact (nb (f a))", "source": "minlog_synthetic/natural_deduction"} -{"id": 88512, "prover": "Minlog", "theorem": "and_comm", "goal": "A /\\ B -> B /\\ A", "context": ["assume h", "elim h", "assume a", "assume b", "split", "exact b", "exact a"], "tactic_proof": "assume h; elim h; assume a; assume b; split; [exact b | exact a]", "source": "minlog_synthetic/natural_deduction"} -{"id": 88513, "prover": "Minlog", "theorem": "or_comm", "goal": "A \\/ B -> B \\/ A", "context": ["assume h", "elim h", "assume a", "right", "exact a", "assume b", "left", "exact b"], "tactic_proof": "assume h; elim h; [assume a; right; exact a | assume b; left; exact b]", "source": "minlog_synthetic/natural_deduction"} -{"id": 88514, "prover": "Minlog", "theorem": "curry", "goal": "(A /\\ B -> C) -> A -> B -> C", "context": ["assume f", "assume a", "assume b", "exact (f (a, b))"], "tactic_proof": "assume f; assume a; assume b; exact (f (a, b))", "source": "minlog_synthetic/natural_deduction"} -{"id": 88515, "prover": "Minlog", "theorem": "add_zero", "goal": "all n. n + 0 = n", "context": ["ind on n", "refl", "assume IH", "simp", "exact IH"], "tactic_proof": "ind on n; [refl | assume IH; simp; exact IH]", "source": "minlog_synthetic/arithmetic"} -{"id": 88516, "prover": "Minlog", "theorem": "add_succ", "goal": "all m n. m + S(n) = S(m + n)", "context": ["ind on m", "refl", "assume IH", "simp", "use IH"], "tactic_proof": "ind on m; [refl | assume IH; simp; use IH]", "source": "minlog_synthetic/arithmetic"} -{"id": 88517, "prover": "Minlog", "theorem": "add_comm", "goal": "all m n. m + n = n + m", "context": ["ind on m", "use add_zero", "assume IH", "simp", "use add_succ", "use IH"], "tactic_proof": "ind on m; [use add_zero | assume IH; simp; use add_succ; use IH]", "source": "minlog_synthetic/arithmetic"} -{"id": 88518, "prover": "Minlog", "theorem": "add_assoc", "goal": "all m n k. (m + n) + k = m + (n + k)", "context": ["ind on m", "refl", "assume IH", "simp", "use IH"], "tactic_proof": "ind on m; [refl | assume IH; simp; use IH]", "source": "minlog_synthetic/arithmetic"} -{"id": 88519, "prover": "Minlog", "theorem": "mul_zero", "goal": "all n. n * 0 = 0", "context": ["ind on n", "refl", "assume IH", "simp", "use IH"], "tactic_proof": "ind on n; [refl | assume IH; simp; use IH]", "source": "minlog_synthetic/arithmetic"} -{"id": 88520, "prover": "Minlog", "theorem": "mul_succ", "goal": "all m n. m * S(n) = m + m * n", "context": ["ind on m", "refl", "assume IH", "simp", "use IH", "use add_assoc", "use add_comm"], "tactic_proof": "ind on m; [refl | assume IH; simp; use IH; use add_assoc; use add_comm]", "source": "minlog_synthetic/arithmetic"} -{"id": 88521, "prover": "Minlog", "theorem": "mul_comm", "goal": "all m n. m * n = n * m", "context": ["ind on m", "use mul_zero", "assume IH", "simp", "use mul_succ", "use IH"], "tactic_proof": "ind on m; [use mul_zero | assume IH; simp; use mul_succ; use IH]", "source": "minlog_synthetic/arithmetic"} -{"id": 88522, "prover": "Minlog", "theorem": "sub_self", "goal": "all n. n - n = 0", "context": ["ind on n", "refl", "assume IH", "simp", "use IH"], "tactic_proof": "ind on n; [refl | assume IH; simp; use IH]", "source": "minlog_synthetic/arithmetic"} -{"id": 88523, "prover": "Minlog", "theorem": "max_comm", "goal": "all m n. max(m, n) = max(n, m)", "context": ["cases", "auto"], "tactic_proof": "cases; auto", "source": "minlog_synthetic/arithmetic"} -{"id": 88524, "prover": "Minlog", "theorem": "min_comm", "goal": "all m n. min(m, n) = min(n, m)", "context": ["cases", "auto"], "tactic_proof": "cases; auto", "source": "minlog_synthetic/arithmetic"} -{"id": 88525, "prover": "Minlog", "theorem": "max_assoc", "goal": "all l m n. max(l, max(m, n)) = max(max(l, m), n)", "context": ["cases", "auto"], "tactic_proof": "cases; auto", "source": "minlog_synthetic/arithmetic"} -{"id": 88526, "prover": "Minlog", "theorem": "le_refl", "goal": "all n. n <= n", "context": ["intro", "refl"], "tactic_proof": "intro; refl", "source": "minlog_synthetic/arithmetic"} -{"id": 88527, "prover": "Minlog", "theorem": "le_trans", "goal": "all l m n. l <= m -> m <= n -> l <= n", "context": ["assume h1", "assume h2", "elim h1", "elim h2", "auto"], "tactic_proof": "assume h1; assume h2; elim h1; elim h2; auto", "source": "minlog_synthetic/arithmetic"} -{"id": 88528, "prover": "Minlog", "theorem": "le_antisym", "goal": "all m n. m <= n -> n <= m -> m = n", "context": ["assume h1", "assume h2", "elim h1", "elim h2", "auto"], "tactic_proof": "assume h1; assume h2; elim h1; elim h2; auto", "source": "minlog_synthetic/arithmetic"} -{"id": 88529, "prover": "Minlog", "theorem": "lt_succ", "goal": "all n. n < S(n)", "context": ["intro", "auto"], "tactic_proof": "intro; auto", "source": "minlog_synthetic/arithmetic"} -{"id": 88530, "prover": "Minlog", "theorem": "sqrt_extraction", "goal": "all n. ex m. m * m <= n /\\ n < (m+1) * (m+1)", "context": ["ind on n", "ex 0", "auto", "assume IH", "elim IH", "assume m", "cases", "ex m", "ex (S m)"], "tactic_proof": "ind on n; [ex 0; auto | assume IH; elim IH; assume m; cases; [ex m; auto | ex (S m); auto]]", "source": "minlog_synthetic/extraction"} -{"id": 88531, "prover": "Minlog", "theorem": "gcd_extraction", "goal": "all a b. b > 0 -> ex d. divides(d, a) /\\ divides(d, b) /\\ all c. divides(c, a) -> divides(c, b) -> divides(c, d)", "context": ["strong_ind on b", "cases", "auto"], "tactic_proof": "strong_ind on b; cases; auto", "source": "minlog_synthetic/extraction"} -{"id": 88532, "prover": "Minlog", "theorem": "div_extraction", "goal": "all a b. b > 0 -> ex q r. a = b * q + r /\\ r < b", "context": ["strong_ind on a", "cases", "auto"], "tactic_proof": "strong_ind on a; cases; auto", "source": "minlog_synthetic/extraction"} -{"id": 88533, "prover": "Minlog", "theorem": "prime_test", "goal": "all n. n >= 2 -> prime(n) \\/ ex d. 1 < d /\\ d < n /\\ divides(d, n)", "context": ["bounded_search", "auto"], "tactic_proof": "bounded_search; auto", "source": "minlog_synthetic/extraction"} -{"id": 88534, "prover": "Minlog", "theorem": "list_sort", "goal": "all l:list(nat). ex l'. sorted(l') /\\ perm(l, l')", "context": ["ind on l", "ex nil", "auto", "assume IH", "elim IH", "assume l'", "insert"], "tactic_proof": "ind on l; [ex nil; auto | assume IH; elim IH; assume l'; insert; auto]", "source": "minlog_synthetic/extraction"} -{"id": 88535, "prover": "Minlog", "theorem": "binary_search_extract", "goal": "all a:array(nat) v. sorted(a) -> (ex i. a[i] = v) \\/ (all i. a[i] <> v)", "context": ["log_search", "auto"], "tactic_proof": "log_search; auto", "source": "minlog_synthetic/extraction"} -{"id": 88536, "prover": "Minlog", "theorem": "min_element", "goal": "all l:list(nat). l <> nil -> ex m. mem(m, l) /\\ all x. mem(x, l) -> m <= x", "context": ["ind on l", "auto"], "tactic_proof": "ind on l; auto", "source": "minlog_synthetic/extraction"} -{"id": 88537, "prover": "Minlog", "theorem": "majority_element", "goal": "all l:list(nat). length(l) > 0 -> ex m. count(m, l) > length(l) / 2 \\/ all x. count(x, l) <= length(l) / 2", "context": ["boyer_moore", "auto"], "tactic_proof": "boyer_moore; auto", "source": "minlog_synthetic/extraction"} -{"id": 88538, "prover": "Minlog", "theorem": "realizer_identity", "goal": "[r : A -> A] = lambda x. x", "context": ["normalize", "refl"], "tactic_proof": "normalize; refl", "source": "minlog_synthetic/realizability"} -{"id": 88539, "prover": "Minlog", "theorem": "realizer_compose", "goal": "[r : (A -> B) -> (B -> C) -> A -> C] = lambda f g x. g (f x)", "context": ["normalize", "refl"], "tactic_proof": "normalize; refl", "source": "minlog_synthetic/realizability"} -{"id": 88540, "prover": "Minlog", "theorem": "realizer_pair", "goal": "[r : A -> B -> A /\\ B] = lambda a b. (a, b)", "context": ["normalize", "refl"], "tactic_proof": "normalize; refl", "source": "minlog_synthetic/realizability"} -{"id": 88541, "prover": "Minlog", "theorem": "realizer_fst", "goal": "[r : A /\\ B -> A] = lambda p. fst(p)", "context": ["normalize", "refl"], "tactic_proof": "normalize; refl", "source": "minlog_synthetic/realizability"} -{"id": 88542, "prover": "Minlog", "theorem": "realizer_snd", "goal": "[r : A /\\ B -> B] = lambda p. snd(p)", "context": ["normalize", "refl"], "tactic_proof": "normalize; refl", "source": "minlog_synthetic/realizability"} -{"id": 88543, "prover": "Minlog", "theorem": "realizer_inl", "goal": "[r : A -> A \\/ B] = lambda a. inl(a)", "context": ["normalize", "refl"], "tactic_proof": "normalize; refl", "source": "minlog_synthetic/realizability"} -{"id": 88544, "prover": "Minlog", "theorem": "realizer_inr", "goal": "[r : B -> A \\/ B] = lambda b. inr(b)", "context": ["normalize", "refl"], "tactic_proof": "normalize; refl", "source": "minlog_synthetic/realizability"} -{"id": 88545, "prover": "Minlog", "theorem": "realizer_case", "goal": "[r : (A -> C) -> (B -> C) -> A \\/ B -> C] = lambda f g s. case s of inl(a) => f a | inr(b) => g b", "context": ["normalize", "refl"], "tactic_proof": "normalize; refl", "source": "minlog_synthetic/realizability"} +{"id":88500,"prover":"Minlog","theorem":"imp_refl","goal":"A -> A","context":["assume A","exact A"],"tactic_proof":"assume A; exact A","source":"minlog_synthetic/natural_deduction"} +{"id":88501,"prover":"Minlog","theorem":"imp_trans","goal":"(A -> B) -> (B -> C) -> A -> C","context":["assume f","assume g","assume a","exact (g (f a))"],"tactic_proof":"assume f; assume g; assume a; exact (g (f a))","source":"minlog_synthetic/natural_deduction"} +{"id":88502,"prover":"Minlog","theorem":"and_intro","goal":"A -> B -> A /\\ B","context":["assume a","assume b","split","exact a","exact b"],"tactic_proof":"assume a; assume b; split; [exact a | exact b]","source":"minlog_synthetic/natural_deduction"} +{"id":88503,"prover":"Minlog","theorem":"and_elim_l","goal":"A /\\ B -> A","context":["assume h","elim h","assume a","assume b","exact a"],"tactic_proof":"assume h; elim h; assume a; assume b; exact a","source":"minlog_synthetic/natural_deduction"} +{"id":88504,"prover":"Minlog","theorem":"and_elim_r","goal":"A /\\ B -> B","context":["assume h","elim h","assume a","assume b","exact b"],"tactic_proof":"assume h; elim h; assume a; assume b; exact b","source":"minlog_synthetic/natural_deduction"} +{"id":88505,"prover":"Minlog","theorem":"or_intro_l","goal":"A -> A \\/ B","context":["assume a","left","exact a"],"tactic_proof":"assume a; left; exact a","source":"minlog_synthetic/natural_deduction"} +{"id":88506,"prover":"Minlog","theorem":"or_intro_r","goal":"B -> A \\/ B","context":["assume b","right","exact b"],"tactic_proof":"assume b; right; exact b","source":"minlog_synthetic/natural_deduction"} +{"id":88507,"prover":"Minlog","theorem":"or_elim","goal":"(A -> C) -> (B -> C) -> A \\/ B -> C","context":["assume f","assume g","assume h","elim h","assume a","exact (f a)","assume b","exact (g b)"],"tactic_proof":"assume f; assume g; assume h; elim h; [assume a; exact (f a) | assume b; exact (g b)]","source":"minlog_synthetic/natural_deduction"} +{"id":88508,"prover":"Minlog","theorem":"false_elim","goal":"F -> A","context":["assume h","elim h"],"tactic_proof":"assume h; elim h","source":"minlog_synthetic/natural_deduction"} +{"id":88509,"prover":"Minlog","theorem":"not_intro","goal":"(A -> F) -> ~A","context":["assume f","intro","exact f"],"tactic_proof":"assume f; intro; exact f","source":"minlog_synthetic/natural_deduction"} +{"id":88510,"prover":"Minlog","theorem":"double_neg_intro","goal":"A -> ~~A","context":["assume a","assume h","exact (h a)"],"tactic_proof":"assume a; assume h; exact (h a)","source":"minlog_synthetic/natural_deduction"} +{"id":88511,"prover":"Minlog","theorem":"contrapositive","goal":"(A -> B) -> ~B -> ~A","context":["assume f","assume nb","assume a","exact (nb (f a))"],"tactic_proof":"assume f; assume nb; assume a; exact (nb (f a))","source":"minlog_synthetic/natural_deduction"} +{"id":88512,"prover":"Minlog","theorem":"and_comm","goal":"A /\\ B -> B /\\ A","context":["assume h","elim h","assume a","assume b","split","exact b","exact a"],"tactic_proof":"assume h; elim h; assume a; assume b; split; [exact b | exact a]","source":"minlog_synthetic/natural_deduction"} +{"id":88513,"prover":"Minlog","theorem":"or_comm","goal":"A \\/ B -> B \\/ A","context":["assume h","elim h","assume a","right","exact a","assume b","left","exact b"],"tactic_proof":"assume h; elim h; [assume a; right; exact a | assume b; left; exact b]","source":"minlog_synthetic/natural_deduction"} +{"id":88514,"prover":"Minlog","theorem":"curry","goal":"(A /\\ B -> C) -> A -> B -> C","context":["assume f","assume a","assume b","exact (f (a, b))"],"tactic_proof":"assume f; assume a; assume b; exact (f (a, b))","source":"minlog_synthetic/natural_deduction"} +{"id":88515,"prover":"Minlog","theorem":"add_zero","goal":"all n. n + 0 = n","context":["ind on n","refl","assume IH","simp","exact IH"],"tactic_proof":"ind on n; [refl | assume IH; simp; exact IH]","source":"minlog_synthetic/arithmetic_extraction"} +{"id":88516,"prover":"Minlog","theorem":"add_succ","goal":"all m n. m + S(n) = S(m + n)","context":["ind on m","refl","assume IH","simp","use IH"],"tactic_proof":"ind on m; [refl | assume IH; simp; use IH]","source":"minlog_synthetic/arithmetic_extraction"} +{"id":88517,"prover":"Minlog","theorem":"add_comm","goal":"all m n. m + n = n + m","context":["ind on m","use add_zero","assume IH","simp","use add_succ","use IH"],"tactic_proof":"ind on m; [use add_zero | assume IH; simp; use add_succ; use IH]","source":"minlog_synthetic/arithmetic_extraction"} +{"id":88518,"prover":"Minlog","theorem":"add_assoc","goal":"all m n k. (m + n) + k = m + (n + k)","context":["ind on m","refl","assume IH","simp","use IH"],"tactic_proof":"ind on m; [refl | assume IH; simp; use IH]","source":"minlog_synthetic/arithmetic_extraction"} +{"id":88519,"prover":"Minlog","theorem":"mul_zero","goal":"all n. n * 0 = 0","context":["ind on n","refl","assume IH","simp","use IH"],"tactic_proof":"ind on n; [refl | assume IH; simp; use IH]","source":"minlog_synthetic/arithmetic_extraction"} +{"id":88520,"prover":"Minlog","theorem":"mul_succ","goal":"all m n. m * S(n) = m + m * n","context":["ind on m","refl","assume IH","simp","use IH","use add_assoc","use add_comm"],"tactic_proof":"ind on m; [refl | assume IH; simp; use IH; use add_assoc; use add_comm]","source":"minlog_synthetic/arithmetic_extraction"} +{"id":88521,"prover":"Minlog","theorem":"mul_comm","goal":"all m n. m * n = n * m","context":["ind on m","use mul_zero","assume IH","simp","use mul_succ","use IH"],"tactic_proof":"ind on m; [use mul_zero | assume IH; simp; use mul_succ; use IH]","source":"minlog_synthetic/arithmetic_extraction"} +{"id":88522,"prover":"Minlog","theorem":"sub_self","goal":"all n. n - n = 0","context":["ind on n","refl","assume IH","simp","use IH"],"tactic_proof":"ind on n; [refl | assume IH; simp; use IH]","source":"minlog_synthetic/arithmetic_extraction"} +{"id":88523,"prover":"Minlog","theorem":"max_comm","goal":"all m n. max(m, n) = max(n, m)","context":["cases","auto"],"tactic_proof":"cases; auto","source":"minlog_synthetic/arithmetic_extraction"} +{"id":88524,"prover":"Minlog","theorem":"min_comm","goal":"all m n. min(m, n) = min(n, m)","context":["cases","auto"],"tactic_proof":"cases; auto","source":"minlog_synthetic/arithmetic_extraction"} +{"id":88525,"prover":"Minlog","theorem":"max_assoc","goal":"all l m n. max(l, max(m, n)) = max(max(l, m), n)","context":["cases","auto"],"tactic_proof":"cases; auto","source":"minlog_synthetic/arithmetic_extraction"} +{"id":88526,"prover":"Minlog","theorem":"le_refl","goal":"all n. n <= n","context":["intro","refl"],"tactic_proof":"intro; refl","source":"minlog_synthetic/arithmetic_extraction"} +{"id":88527,"prover":"Minlog","theorem":"le_trans","goal":"all l m n. l <= m -> m <= n -> l <= n","context":["assume h1","assume h2","elim h1","elim h2","auto"],"tactic_proof":"assume h1; assume h2; elim h1; elim h2; auto","source":"minlog_synthetic/arithmetic_extraction"} +{"id":88528,"prover":"Minlog","theorem":"le_antisym","goal":"all m n. m <= n -> n <= m -> m = n","context":["assume h1","assume h2","elim h1","elim h2","auto"],"tactic_proof":"assume h1; assume h2; elim h1; elim h2; auto","source":"minlog_synthetic/arithmetic_extraction"} +{"id":88529,"prover":"Minlog","theorem":"lt_succ","goal":"all n. n < S(n)","context":["intro","auto"],"tactic_proof":"intro; auto","source":"minlog_synthetic/arithmetic_extraction"} +{"id":88530,"prover":"Minlog","theorem":"sqrt_extraction","goal":"all n. ex m. m * m <= n /\\ n < (m+1) * (m+1)","context":["ind on n","ex 0","auto","assume IH","elim IH","assume m","cases","ex m","ex (S m)"],"tactic_proof":"ind on n; [ex 0; auto | assume IH; elim IH; assume m; cases; [ex m; auto | ex (S m); auto]]","source":"minlog_synthetic/program_extraction"} +{"id":88531,"prover":"Minlog","theorem":"gcd_extraction","goal":"all a b. b > 0 -> ex d. divides(d, a) /\\ divides(d, b) /\\ all c. divides(c, a) -> divides(c, b) -> divides(c, d)","context":["strong_ind on b","cases","auto"],"tactic_proof":"strong_ind on b; cases; auto","source":"minlog_synthetic/program_extraction"} +{"id":88532,"prover":"Minlog","theorem":"div_extraction","goal":"all a b. b > 0 -> ex q r. a = b * q + r /\\ r < b","context":["strong_ind on a","cases","auto"],"tactic_proof":"strong_ind on a; cases; auto","source":"minlog_synthetic/program_extraction"} +{"id":88533,"prover":"Minlog","theorem":"prime_test","goal":"all n. n >= 2 -> prime(n) \\/ ex d. 1 < d /\\ d < n /\\ divides(d, n)","context":["bounded_search","auto"],"tactic_proof":"bounded_search; auto","source":"minlog_synthetic/program_extraction"} +{"id":88534,"prover":"Minlog","theorem":"list_sort","goal":"all l:list(nat). ex l'. sorted(l') /\\ perm(l, l')","context":["ind on l","ex nil","auto","assume IH","elim IH","assume l'","insert"],"tactic_proof":"ind on l; [ex nil; auto | assume IH; elim IH; assume l'; insert; auto]","source":"minlog_synthetic/program_extraction"} +{"id":88535,"prover":"Minlog","theorem":"binary_search_extract","goal":"all a:array(nat) v. sorted(a) -> (ex i. a[i] = v) \\/ (all i. a[i] <> v)","context":["log_search","auto"],"tactic_proof":"log_search; auto","source":"minlog_synthetic/program_extraction"} +{"id":88536,"prover":"Minlog","theorem":"min_element","goal":"all l:list(nat). l <> nil -> ex m. mem(m, l) /\\ all x. mem(x, l) -> m <= x","context":["ind on l","auto"],"tactic_proof":"ind on l; auto","source":"minlog_synthetic/program_extraction"} +{"id":88537,"prover":"Minlog","theorem":"majority_element","goal":"all l:list(nat). length(l) > 0 -> ex m. count(m, l) > length(l) / 2 \\/ all x. count(x, l) <= length(l) / 2","context":["boyer_moore","auto"],"tactic_proof":"boyer_moore; auto","source":"minlog_synthetic/program_extraction"} +{"id":88538,"prover":"Minlog","theorem":"realizer_identity","goal":"[r : A -> A] = lambda x. x","context":["normalize","refl"],"tactic_proof":"normalize; refl","source":"minlog_synthetic/realizability"} +{"id":88539,"prover":"Minlog","theorem":"realizer_compose","goal":"[r : (A -> B) -> (B -> C) -> A -> C] = lambda f g x. g (f x)","context":["normalize","refl"],"tactic_proof":"normalize; refl","source":"minlog_synthetic/realizability"} +{"id":88540,"prover":"Minlog","theorem":"realizer_pair","goal":"[r : A -> B -> A /\\ B] = lambda a b. (a, b)","context":["normalize","refl"],"tactic_proof":"normalize; refl","source":"minlog_synthetic/realizability"} +{"id":88541,"prover":"Minlog","theorem":"realizer_fst","goal":"[r : A /\\ B -> A] = lambda p. fst(p)","context":["normalize","refl"],"tactic_proof":"normalize; refl","source":"minlog_synthetic/realizability"} +{"id":88542,"prover":"Minlog","theorem":"realizer_snd","goal":"[r : A /\\ B -> B] = lambda p. snd(p)","context":["normalize","refl"],"tactic_proof":"normalize; refl","source":"minlog_synthetic/realizability"} +{"id":88543,"prover":"Minlog","theorem":"realizer_inl","goal":"[r : A -> A \\/ B] = lambda a. inl(a)","context":["normalize","refl"],"tactic_proof":"normalize; refl","source":"minlog_synthetic/realizability"} +{"id":88544,"prover":"Minlog","theorem":"realizer_inr","goal":"[r : B -> A \\/ B] = lambda b. inr(b)","context":["normalize","refl"],"tactic_proof":"normalize; refl","source":"minlog_synthetic/realizability"} +{"id":88545,"prover":"Minlog","theorem":"realizer_case","goal":"[r : (A -> C) -> (B -> C) -> A \\/ B -> C] = lambda f g s. case s of inl(a) => f a | inr(b) => g b","context":["normalize","refl"],"tactic_proof":"normalize; refl","source":"minlog_synthetic/realizability"} +{"id":88546,"prover":"Minlog","theorem":"realizer_forall","goal":"[r : (all x:N. A(x))] = lambda x. r_x","context":["normalize","refl"],"tactic_proof":"normalize; refl","source":"minlog_synthetic/realizability"} +{"id":88547,"prover":"Minlog","theorem":"realizer_exists","goal":"[r : (ex x:N. A(x))] = (n, proof_of_A(n))","context":["normalize","refl"],"tactic_proof":"normalize; refl","source":"minlog_synthetic/realizability"} +{"id":88548,"prover":"Minlog","theorem":"realizer_induction","goal":"[r : nat_rec] = lambda base step n. (rec base step n)","context":["normalize","refl"],"tactic_proof":"normalize; refl","source":"minlog_synthetic/realizability"} +{"id":88549,"prover":"Minlog","theorem":"list_nil_append","goal":"all l:list. nil ++ l = l","context":["intro","refl"],"tactic_proof":"intro; refl","source":"minlog_synthetic/lists_minlog"} +{"id":88550,"prover":"Minlog","theorem":"list_append_nil","goal":"all l:list. l ++ nil = l","context":["ind on l","refl","assume IH","simp","use IH"],"tactic_proof":"ind on l; [refl | assume IH; simp; use IH]","source":"minlog_synthetic/lists_minlog"} +{"id":88551,"prover":"Minlog","theorem":"list_append_assoc","goal":"all l1 l2 l3. (l1 ++ l2) ++ l3 = l1 ++ (l2 ++ l3)","context":["ind on l1","refl","assume IH","simp","use IH"],"tactic_proof":"ind on l1; [refl | assume IH; simp; use IH]","source":"minlog_synthetic/lists_minlog"} +{"id":88552,"prover":"Minlog","theorem":"list_length_append","goal":"all l1 l2. length(l1 ++ l2) = length(l1) + length(l2)","context":["ind on l1","refl","assume IH","simp","use IH"],"tactic_proof":"ind on l1; [refl | assume IH; simp; use IH]","source":"minlog_synthetic/lists_minlog"} +{"id":88553,"prover":"Minlog","theorem":"list_rev_involutive","goal":"all l. rev(rev(l)) = l","context":["ind on l","refl","assume IH","simp","use rev_append","use IH"],"tactic_proof":"ind on l; [refl | assume IH; simp; use rev_append; use IH]","source":"minlog_synthetic/lists_minlog"} +{"id":88554,"prover":"Minlog","theorem":"list_rev_append","goal":"all l1 l2. rev(l1 ++ l2) = rev(l2) ++ rev(l1)","context":["ind on l1","simp","use list_append_nil","assume IH","use IH","use list_append_assoc"],"tactic_proof":"ind on l1; [simp; use list_append_nil | assume IH; simp; use IH; use list_append_assoc]","source":"minlog_synthetic/lists_minlog"} +{"id":88555,"prover":"Minlog","theorem":"list_map_id","goal":"all l. map(lambda x. x, l) = l","context":["ind on l","refl","assume IH","simp","use IH"],"tactic_proof":"ind on l; [refl | assume IH; simp; use IH]","source":"minlog_synthetic/lists_minlog"} +{"id":88556,"prover":"Minlog","theorem":"list_map_compose","goal":"all f g l. map(f, map(g, l)) = map(lambda x. f (g x), l)","context":["ind on l","refl","assume IH","simp","use IH"],"tactic_proof":"ind on l; [refl | assume IH; simp; use IH]","source":"minlog_synthetic/lists_minlog"} +{"id":88557,"prover":"Minlog","theorem":"list_filter_length","goal":"all p l. length(filter(p, l)) <= length(l)","context":["ind on l","auto","assume IH","cases p"],"tactic_proof":"ind on l; [auto | assume IH; cases p; auto]","source":"minlog_synthetic/lists_minlog"} +{"id":88558,"prover":"Minlog","theorem":"list_foldr_append","goal":"all f z l1 l2. foldr(f, z, l1 ++ l2) = foldr(f, foldr(f, z, l2), l1)","context":["ind on l1","refl","assume IH","simp","use IH"],"tactic_proof":"ind on l1; [refl | assume IH; simp; use IH]","source":"minlog_synthetic/lists_minlog"} +{"id":88559,"prover":"Minlog","theorem":"list_all_forall","goal":"all p l. (all x. mem(x, l) -> p(x)) -> list_all(p, l)","context":["ind on l","auto","assume IH","cases"],"tactic_proof":"ind on l; [auto | assume IH; cases; auto]","source":"minlog_synthetic/lists_minlog"} +{"id":88560,"prover":"Minlog","theorem":"tree_height_nonneg","goal":"all t. height(t) >= 0","context":["ind on t","auto"],"tactic_proof":"ind on t; auto","source":"minlog_synthetic/trees"} +{"id":88561,"prover":"Minlog","theorem":"tree_size_nonneg","goal":"all t. size(t) >= 1","context":["ind on t","auto"],"tactic_proof":"ind on t; auto","source":"minlog_synthetic/trees"} +{"id":88562,"prover":"Minlog","theorem":"tree_leaves_ge_1","goal":"all t. leaves(t) >= 1","context":["ind on t","auto"],"tactic_proof":"ind on t; auto","source":"minlog_synthetic/trees"} +{"id":88563,"prover":"Minlog","theorem":"tree_mirror_involutive","goal":"all t. mirror(mirror(t)) = t","context":["ind on t","refl","assume IH1 IH2","simp","use IH1","use IH2"],"tactic_proof":"ind on t; [refl | assume IH1 IH2; simp; use IH1; use IH2]","source":"minlog_synthetic/trees"} +{"id":88564,"prover":"Minlog","theorem":"tree_size_height","goal":"all t. size(t) <= 2^(height(t)+1) - 1","context":["ind on t","auto","assume IH1 IH2","simp","use IH1","use IH2"],"tactic_proof":"ind on t; [auto | assume IH1 IH2; simp; use IH1; use IH2]","source":"minlog_synthetic/trees"} +{"id":88565,"prover":"Minlog","theorem":"bst_inorder_sorted","goal":"all t. is_bst(t) -> sorted(inorder(t))","context":["ind on t","auto","assume IH","split"],"tactic_proof":"ind on t; [auto | assume IH; split; auto]","source":"minlog_synthetic/trees"} +{"id":88566,"prover":"Minlog","theorem":"tree_flatten_append","goal":"all t1 t2. flatten(Node(t1, x, t2)) = flatten(t1) ++ [x] ++ flatten(t2)","context":["intro","refl"],"tactic_proof":"intro; refl","source":"minlog_synthetic/trees"} +{"id":88567,"prover":"Minlog","theorem":"tree_count_sum","goal":"all x t. count(x, flatten(t)) = count_tree(x, t)","context":["ind on t","auto"],"tactic_proof":"ind on t; auto","source":"minlog_synthetic/trees"} +{"id":88568,"prover":"Minlog","theorem":"tnd","goal":"all A. A \\/ ~A","context":["use classical","auto"],"tactic_proof":"use classical; auto","source":"minlog_synthetic/classical_logic"} +{"id":88569,"prover":"Minlog","theorem":"dne","goal":"all A. ~~A -> A","context":["assume h","classical","auto"],"tactic_proof":"assume h; classical; auto","source":"minlog_synthetic/classical_logic"} +{"id":88570,"prover":"Minlog","theorem":"peirce_law","goal":"all A B. ((A -> B) -> A) -> A","context":["assume h","classical","auto"],"tactic_proof":"assume h; classical; auto","source":"minlog_synthetic/classical_logic"} +{"id":88571,"prover":"Minlog","theorem":"contrapos_classical","goal":"all A B. (~B -> ~A) -> (A -> B)","context":["assume h","classical","auto"],"tactic_proof":"assume h; classical; auto","source":"minlog_synthetic/classical_logic"} +{"id":88572,"prover":"Minlog","theorem":"or_impl","goal":"all A B. (A \\/ B) -> (~A -> B)","context":["assume h nA","elim h","assume a","absurd","assume b","exact b"],"tactic_proof":"assume h nA; elim h; [assume a; absurd | assume b; exact b]","source":"minlog_synthetic/classical_logic"} +{"id":88573,"prover":"Minlog","theorem":"impl_or","goal":"all A B. (A -> B) -> (~A \\/ B)","context":["assume h","classical","auto"],"tactic_proof":"assume h; classical; auto","source":"minlog_synthetic/classical_logic"} +{"id":88574,"prover":"Minlog","theorem":"and_not_or","goal":"all A B. ~A /\\ ~B -> ~(A \\/ B)","context":["assume h","elim h","assume nA nB","intro","elim","auto"],"tactic_proof":"assume h; elim h; assume nA nB; intro; elim; auto","source":"minlog_synthetic/classical_logic"} +{"id":88575,"prover":"Minlog","theorem":"demorgan_classical_1","goal":"all A B. ~(A /\\ B) -> (~A \\/ ~B)","context":["assume h","classical","auto"],"tactic_proof":"assume h; classical; auto","source":"minlog_synthetic/classical_logic"} +{"id":88576,"prover":"Minlog","theorem":"demorgan_classical_2","goal":"all A B. ~(A \\/ B) <-> (~A /\\ ~B)","context":["split","intros","auto"],"tactic_proof":"split; intros; split; intros; auto","source":"minlog_synthetic/classical_logic"} +{"id":88577,"prover":"Minlog","theorem":"classical_exists","goal":"all P. ~(all x. ~P(x)) -> ex x. P(x)","context":["assume h","classical","auto"],"tactic_proof":"assume h; classical; auto","source":"minlog_synthetic/classical_logic"} +{"id":88578,"prover":"Minlog","theorem":"cut_elim","goal":"all A B C. (Gamma |- A) -> (A, Gamma |- B) -> (Gamma |- B)","context":["intros","cut_admissible","auto"],"tactic_proof":"intros; cut_admissible; auto","source":"minlog_synthetic/sequent_calculus"} +{"id":88579,"prover":"Minlog","theorem":"structural_weaken","goal":"all A B. (Gamma |- B) -> (A, Gamma |- B)","context":["intros","weakening","auto"],"tactic_proof":"intros; weakening; auto","source":"minlog_synthetic/sequent_calculus"} +{"id":88580,"prover":"Minlog","theorem":"structural_contract","goal":"all A B. (A, A, Gamma |- B) -> (A, Gamma |- B)","context":["intros","contraction","auto"],"tactic_proof":"intros; contraction; auto","source":"minlog_synthetic/sequent_calculus"} +{"id":88581,"prover":"Minlog","theorem":"structural_exchange","goal":"all A B C. (A, B, Gamma |- C) -> (B, A, Gamma |- C)","context":["intros","exchange","auto"],"tactic_proof":"intros; exchange; auto","source":"minlog_synthetic/sequent_calculus"} +{"id":88582,"prover":"Minlog","theorem":"identity_axiom","goal":"all A. (A |- A)","context":["intro","axiom"],"tactic_proof":"intro; axiom","source":"minlog_synthetic/sequent_calculus"} +{"id":88583,"prover":"Minlog","theorem":"and_right","goal":"all A B. (Gamma |- A) -> (Gamma |- B) -> (Gamma |- A /\\ B)","context":["intros","andR","auto"],"tactic_proof":"intros; andR; auto","source":"minlog_synthetic/sequent_calculus"} +{"id":88584,"prover":"Minlog","theorem":"and_left_1","goal":"all A B C. (A, Gamma |- C) -> (A /\\ B, Gamma |- C)","context":["intros","andL1","auto"],"tactic_proof":"intros; andL1; auto","source":"minlog_synthetic/sequent_calculus"} +{"id":88585,"prover":"Minlog","theorem":"impl_right","goal":"all A B. (A, Gamma |- B) -> (Gamma |- A -> B)","context":["intros","implR","auto"],"tactic_proof":"intros; implR; auto","source":"minlog_synthetic/sequent_calculus"} +{"id":88586,"prover":"Minlog","theorem":"impl_left","goal":"all A B C. (Gamma |- A) -> (B, Gamma |- C) -> (A -> B, Gamma |- C)","context":["intros","implL","auto"],"tactic_proof":"intros; implL; auto","source":"minlog_synthetic/sequent_calculus"} +{"id":88587,"prover":"Minlog","theorem":"strong_ind","goal":"all P. (all n. (all m. m < n -> P(m)) -> P(n)) -> all n. P(n)","context":["assume h","strong_ind","auto"],"tactic_proof":"assume h; strong_ind; auto","source":"minlog_synthetic/induction_advanced"} +{"id":88588,"prover":"Minlog","theorem":"course_of_values","goal":"all P. P(0) -> (all n. P(n) -> P(n+1)) -> all n. P(n)","context":["assume p0 step","nat_rec","auto"],"tactic_proof":"assume p0 step; nat_rec; auto","source":"minlog_synthetic/induction_advanced"} +{"id":88589,"prover":"Minlog","theorem":"well_founded_acc","goal":"all R. well_founded(R) -> all P. (all x. (all y. R(y,x) -> P(y)) -> P(x)) -> all x. P(x)","context":["assume wf ih","wf_rec","auto"],"tactic_proof":"assume wf ih; wf_rec; auto","source":"minlog_synthetic/induction_advanced"} +{"id":88590,"prover":"Minlog","theorem":"mutual_ind_evenodd","goal":"(all n. even(n) -> P(n)) /\\ (all n. odd(n) -> Q(n))","context":["mutual_ind","auto"],"tactic_proof":"mutual_ind; auto","source":"minlog_synthetic/induction_advanced"} +{"id":88591,"prover":"Minlog","theorem":"struct_ind_list","goal":"all P. P(nil) -> (all x xs. P(xs) -> P(cons x xs)) -> all l. P(l)","context":["assume p_nil p_cons","list_rec","auto"],"tactic_proof":"assume p_nil p_cons; list_rec; auto","source":"minlog_synthetic/induction_advanced"} +{"id":88592,"prover":"Minlog","theorem":"struct_ind_tree","goal":"all P. P(leaf) -> (all t1 x t2. P(t1) -> P(t2) -> P(Node t1 x t2)) -> all t. P(t)","context":["assume p_leaf p_node","tree_rec","auto"],"tactic_proof":"assume p_leaf p_node; tree_rec; auto","source":"minlog_synthetic/induction_advanced"} +{"id":88593,"prover":"Minlog","theorem":"transfinite_ind","goal":"all P. (all beta. beta < alpha -> P(beta)) -> P(alpha)","context":["assume ih","transfinite","auto"],"tactic_proof":"assume ih; transfinite; auto","source":"minlog_synthetic/induction_advanced"} +{"id":88594,"prover":"Minlog","theorem":"higher_order_app","goal":"all f x. (lambda y. f y) x = f x","context":["beta_reduce","refl"],"tactic_proof":"beta_reduce; refl","source":"minlog_synthetic/higher_order"} +{"id":88595,"prover":"Minlog","theorem":"fun_ext_ho","goal":"all f g. (all x. f x = g x) -> f = g","context":["assume h","fun_ext","auto"],"tactic_proof":"assume h; fun_ext; auto","source":"minlog_synthetic/higher_order"} +{"id":88596,"prover":"Minlog","theorem":"curry_uncurry","goal":"all f x y. curry (uncurry f) x y = f x y","context":["intros","beta_reduce","refl"],"tactic_proof":"intros; beta_reduce; refl","source":"minlog_synthetic/higher_order"} +{"id":88597,"prover":"Minlog","theorem":"uncurry_curry","goal":"all f p. uncurry (curry f) p = f p","context":["intro","cases p","beta_reduce","refl"],"tactic_proof":"intro; cases p; beta_reduce; refl","source":"minlog_synthetic/higher_order"} +{"id":88598,"prover":"Minlog","theorem":"compose_assoc","goal":"all f g h. compose (compose f g) h = compose f (compose g h)","context":["fun_ext","beta_reduce","refl"],"tactic_proof":"fun_ext; beta_reduce; refl","source":"minlog_synthetic/higher_order"} +{"id":88599,"prover":"Minlog","theorem":"id_left","goal":"all f. compose id f = f","context":["fun_ext","beta_reduce","refl"],"tactic_proof":"fun_ext; beta_reduce; refl","source":"minlog_synthetic/higher_order"} +{"id":88600,"prover":"Minlog","theorem":"id_right","goal":"all f. compose f id = f","context":["fun_ext","beta_reduce","refl"],"tactic_proof":"fun_ext; beta_reduce; refl","source":"minlog_synthetic/higher_order"} +{"id":88601,"prover":"Minlog","theorem":"ho_induction_schema","goal":"all P. (all x. x = 0 \\/ (ex y. x = y+1 /\\ P(y))) -> P(0) -> all x. P(x)","context":["assume h p0","induct","auto"],"tactic_proof":"assume h p0; induct; auto","source":"minlog_synthetic/higher_order"} +{"id":88602,"prover":"Minlog","theorem":"factorial_correct","goal":"all n. factorial(n) >= 1","context":["ind on n","simp","auto","assume IH","use IH"],"tactic_proof":"ind on n; [simp; auto | assume IH; simp; use IH]","source":"minlog_synthetic/program_verification"} +{"id":88603,"prover":"Minlog","theorem":"fibonacci_monotone","goal":"all m n. m <= n -> fib(m) <= fib(n)","context":["assume h","ind on n","auto"],"tactic_proof":"assume h; ind on n; auto","source":"minlog_synthetic/program_verification"} +{"id":88604,"prover":"Minlog","theorem":"sum_range_formula","goal":"all n. sum(0..n, lambda i. i) = n * (n+1) / 2","context":["ind on n","auto"],"tactic_proof":"ind on n; auto","source":"minlog_synthetic/program_verification"} +{"id":88605,"prover":"Minlog","theorem":"sort_preserves_elements","goal":"all l. mset(sort l) = mset(l)","context":["ind on l","auto"],"tactic_proof":"ind on l; auto","source":"minlog_synthetic/program_verification"} +{"id":88606,"prover":"Minlog","theorem":"reverse_length","goal":"all l. length(reverse l) = length l","context":["ind on l","refl","assume IH","simp","use length_append","use IH"],"tactic_proof":"ind on l; [refl | assume IH; simp; use length_append; use IH]","source":"minlog_synthetic/program_verification"} +{"id":88607,"prover":"Minlog","theorem":"gcd_correct","goal":"all a b. b > 0 -> divides(gcd(a,b), a) /\\ divides(gcd(a,b), b)","context":["strong_ind on b","cases","auto"],"tactic_proof":"strong_ind on b; cases; auto","source":"minlog_synthetic/program_verification"} +{"id":88608,"prover":"Minlog","theorem":"is_sorted_cons","goal":"all x xs. is_sorted(cons x xs) -> is_sorted xs","context":["intros","cases","auto"],"tactic_proof":"intros; cases; auto","source":"minlog_synthetic/program_verification"} +{"id":88609,"prover":"Minlog","theorem":"search_correct","goal":"all x l. linear_search(x, l) = true <-> mem(x, l)","context":["ind on l","split","auto"],"tactic_proof":"ind on l; split; auto","source":"minlog_synthetic/program_verification"} +{"id":88610,"prover":"Minlog","theorem":"modal_k","goal":"all A B. box(A -> B) -> box(A) -> box(B)","context":["intros","box_elim","auto"],"tactic_proof":"intros; box_elim; auto","source":"minlog_synthetic/modal_logic"} +{"id":88611,"prover":"Minlog","theorem":"modal_t","goal":"all A. box(A) -> A","context":["intro","reflexive_frame","auto"],"tactic_proof":"intro; reflexive_frame; auto","source":"minlog_synthetic/modal_logic"} +{"id":88612,"prover":"Minlog","theorem":"modal_4","goal":"all A. box(A) -> box(box(A))","context":["intro","transitive_frame","auto"],"tactic_proof":"intro; transitive_frame; auto","source":"minlog_synthetic/modal_logic"} +{"id":88613,"prover":"Minlog","theorem":"modal_5","goal":"all A. dia(A) -> box(dia(A))","context":["intro","euclidean_frame","auto"],"tactic_proof":"intro; euclidean_frame; auto","source":"minlog_synthetic/modal_logic"} +{"id":88614,"prover":"Minlog","theorem":"modal_dual","goal":"all A. dia(A) <-> ~box(~A)","context":["split","intros","auto"],"tactic_proof":"split; intros; auto","source":"minlog_synthetic/modal_logic"} +{"id":88615,"prover":"Minlog","theorem":"necessitation","goal":"all A. |- A -> |- box(A)","context":["intro","necessitate","auto"],"tactic_proof":"intro; necessitate; auto","source":"minlog_synthetic/modal_logic"} +{"id":88616,"prover":"Minlog","theorem":"distribution","goal":"all A B. box(A /\\ B) <-> box(A) /\\ box(B)","context":["split","intros","box_elim","auto"],"tactic_proof":"split; intros; split; box_elim; auto","source":"minlog_synthetic/modal_logic"} +{"id":88617,"prover":"Minlog","theorem":"disjunction_property","goal":"all A B. (|- A \\/ B) -> (|- A) \\/ (|- B)","context":["assume h","intuit","auto"],"tactic_proof":"assume h; intuit; auto","source":"minlog_synthetic/intuitionistic"} +{"id":88618,"prover":"Minlog","theorem":"existence_property","goal":"all P. (|- ex x. P(x)) -> ex witness. |- P(witness)","context":["assume h","intuit","auto"],"tactic_proof":"assume h; intuit; auto","source":"minlog_synthetic/intuitionistic"} +{"id":88619,"prover":"Minlog","theorem":"double_neg_shift","goal":"all A. ~~(A \\/ ~A)","context":["intro","assume h","apply h","right","left","auto"],"tactic_proof":"intro; assume h; apply h; right; intro; apply h; left; auto","source":"minlog_synthetic/intuitionistic"} +{"id":88620,"prover":"Minlog","theorem":"glivenko","goal":"all A. (|- ~~A classically) -> (|- ~~A intuitionistically)","context":["assume h","glivenko","auto"],"tactic_proof":"assume h; glivenko; auto","source":"minlog_synthetic/intuitionistic"} +{"id":88621,"prover":"Minlog","theorem":"kripke_model","goal":"all w:World, A. forces(w, A) <-> satisfies(w, A)","context":["intro","split","kripke","auto"],"tactic_proof":"intro; split; kripke; auto","source":"minlog_synthetic/intuitionistic"} +{"id":88622,"prover":"Minlog","theorem":"negation_translation","goal":"all A. (~~A)_neg = ~~A_neg","context":["intro","neg_translation","auto"],"tactic_proof":"intro; neg_translation; auto","source":"minlog_synthetic/intuitionistic"} +{"id":88623,"prover":"Minlog","theorem":"godel_neg","goal":"all A. valid(A) <-> valid(~~A_neg)","context":["intro","split","godel_negative","auto"],"tactic_proof":"intro; split; godel_negative; auto","source":"minlog_synthetic/intuitionistic"} +{"id":88624,"prover":"Minlog","theorem":"game_det","goal":"all G:Game. open(G) -> determined(G)","context":["assume h","gale_stewart","auto"],"tactic_proof":"assume h; gale_stewart; auto","source":"minlog_synthetic/games"} +{"id":88625,"prover":"Minlog","theorem":"strategy_winning","goal":"all G:Game, sigma:Strategy. winning(sigma, G) -> all play. consistent(play, sigma) -> G_wins(play)","context":["assume w","intro con","auto"],"tactic_proof":"assume w; intro con; auto","source":"minlog_synthetic/games"} +{"id":88626,"prover":"Minlog","theorem":"zermelo","goal":"all G:FiniteGame. determined(G)","context":["intro","backward_induction","auto"],"tactic_proof":"intro; backward_induction; auto","source":"minlog_synthetic/games"} +{"id":88627,"prover":"Minlog","theorem":"minimax","goal":"all G:ZeroSum, v:Value. v = max(min(payoff))","context":["intro","minimax_theorem","auto"],"tactic_proof":"intro; minimax_theorem; auto","source":"minlog_synthetic/games"} +{"id":88628,"prover":"Minlog","theorem":"nash_existence","goal":"all G:FiniteGame. ex sigma. nash_equilibrium(sigma, G)","context":["intro","brouwer","auto"],"tactic_proof":"intro; brouwer; auto","source":"minlog_synthetic/games"} +{"id":88629,"prover":"Minlog","theorem":"realizer_nat_rec","goal":"[r : nat_rec] = lambda base step n. (fix F lambda k. if k=0 then base else step k (F (k-1))) n","context":["normalize","refl"],"tactic_proof":"normalize; refl","source":"minlog_synthetic/realizers_advanced"} +{"id":88630,"prover":"Minlog","theorem":"realizer_list_rec","goal":"[r : list_rec] = lambda nil_case cons_case l. (fix F lambda xs. match xs with nil => nil_case | x::xs' => cons_case x (F xs')) l","context":["normalize","refl"],"tactic_proof":"normalize; refl","source":"minlog_synthetic/realizers_advanced"} +{"id":88631,"prover":"Minlog","theorem":"realizer_bounded_search","goal":"[r : bounded_search_lemma] = lambda p bound. search_loop p 0 bound","context":["normalize","refl"],"tactic_proof":"normalize; refl","source":"minlog_synthetic/realizers_advanced"} +{"id":88632,"prover":"Minlog","theorem":"realizer_minimization","goal":"[r : minimization] = lambda f. mu (lambda n. f n = 0)","context":["normalize","refl"],"tactic_proof":"normalize; refl","source":"minlog_synthetic/realizers_advanced"} +{"id":88633,"prover":"Minlog","theorem":"realizer_fixpoint","goal":"[r : fix_point_thm] = lambda f. fix f","context":["normalize","refl"],"tactic_proof":"normalize; refl","source":"minlog_synthetic/realizers_advanced"} +{"id":88634,"prover":"Minlog","theorem":"realizer_choice","goal":"[r : countable_choice] = lambda R. lambda n. choose (R n)","context":["normalize","refl"],"tactic_proof":"normalize; refl","source":"minlog_synthetic/realizers_advanced"} +{"id":88635,"prover":"Minlog","theorem":"bit_length","goal":"all n. n > 0 -> bit_length(n) = floor(log2(n)) + 1","context":["strong_ind on n","auto"],"tactic_proof":"strong_ind on n; auto","source":"minlog_synthetic/bounded_arithmetic"} +{"id":88636,"prover":"Minlog","theorem":"parity","goal":"all n. parity(n) = n mod 2","context":["ind on n","auto"],"tactic_proof":"ind on n; auto","source":"minlog_synthetic/bounded_arithmetic"} +{"id":88637,"prover":"Minlog","theorem":"binary_rep","goal":"all n. binary_decode(binary_encode(n)) = n","context":["ind on n","auto"],"tactic_proof":"ind on n; auto","source":"minlog_synthetic/bounded_arithmetic"} +{"id":88638,"prover":"Minlog","theorem":"pow_two_le","goal":"all n. 2^n > n","context":["ind on n","auto"],"tactic_proof":"ind on n; auto","source":"minlog_synthetic/bounded_arithmetic"} +{"id":88639,"prover":"Minlog","theorem":"pigeon_bounded","goal":"all f:fin(n)->fin(m). n > m -> ex i j. i <> j /\\ f(i) = f(j)","context":["assume","pigeonhole","auto"],"tactic_proof":"assume; pigeonhole; auto","source":"minlog_synthetic/bounded_arithmetic"} +{"id":88640,"prover":"Minlog","theorem":"bounded_search","goal":"all p:nat->bool. (ex n. n <= N /\\ p n = true) -> ex k. k <= N /\\ p k = true /\\ (all j. j < k -> p j = false)","context":["assume","bounded_search","auto"],"tactic_proof":"assume; bounded_search; auto","source":"minlog_synthetic/bounded_arithmetic"} +{"id":88641,"prover":"Minlog","theorem":"pspace_pspace","goal":"pspace = pspace","context":["refl"],"tactic_proof":"refl","source":"minlog_synthetic/bounded_arithmetic"} +{"id":88642,"prover":"Minlog","theorem":"fin_sat_decidable","goal":"all phi:Formula. decidable(sat(phi))","context":["intro","propositional_sat","auto"],"tactic_proof":"intro; propositional_sat; auto","source":"minlog_synthetic/finite_logic"} +{"id":88643,"prover":"Minlog","theorem":"resolution_sound","goal":"all phi. res_derives(empty, phi) -> unsat(phi)","context":["assume h","resolution_soundness","auto"],"tactic_proof":"assume h; resolution_soundness; auto","source":"minlog_synthetic/finite_logic"} +{"id":88644,"prover":"Minlog","theorem":"resolution_complete","goal":"all phi. unsat(phi) -> res_derives(empty, phi)","context":["assume h","resolution_completeness","auto"],"tactic_proof":"assume h; resolution_completeness; auto","source":"minlog_synthetic/finite_logic"} +{"id":88645,"prover":"Minlog","theorem":"dpll_terminates","goal":"all phi. terminates(dpll(phi))","context":["intro","wf_induct","auto"],"tactic_proof":"intro; wf_induct; auto","source":"minlog_synthetic/finite_logic"} +{"id":88646,"prover":"Minlog","theorem":"cnf_equivalent","goal":"all phi. equivalent(phi, to_cnf(phi))","context":["intro","tseitin","auto"],"tactic_proof":"intro; tseitin; auto","source":"minlog_synthetic/finite_logic"} +{"id":88647,"prover":"Minlog","theorem":"horn_sat_poly","goal":"all phi:HornFormula. poly_time_decidable(sat(phi))","context":["intro","unit_propagation","auto"],"tactic_proof":"intro; unit_propagation; auto","source":"minlog_synthetic/finite_logic"} diff --git a/training_data/proof_states_nuprl.jsonl b/training_data/proof_states_nuprl.jsonl index 28c35198..3d3e4cb6 100644 --- a/training_data/proof_states_nuprl.jsonl +++ b/training_data/proof_states_nuprl.jsonl @@ -1,50 +1,152 @@ -{"id": 88000, "prover": "Nuprl", "theorem": "add_comm", "goal": "all x,y:Int. (x + y) = (y + x)", "context": ["Auto"], "tactic_proof": "Auto", "source": "nuprl_synthetic/arithmetic"} -{"id": 88001, "prover": "Nuprl", "theorem": "add_assoc", "goal": "all x,y,z:Int. ((x + y) + z) = (x + (y + z))", "context": ["Auto"], "tactic_proof": "Auto", "source": "nuprl_synthetic/arithmetic"} -{"id": 88002, "prover": "Nuprl", "theorem": "mul_comm", "goal": "all x,y:Int. (x * y) = (y * x)", "context": ["Auto"], "tactic_proof": "Auto", "source": "nuprl_synthetic/arithmetic"} -{"id": 88003, "prover": "Nuprl", "theorem": "mul_assoc", "goal": "all x,y,z:Int. ((x * y) * z) = (x * (y * z))", "context": ["Auto"], "tactic_proof": "Auto", "source": "nuprl_synthetic/arithmetic"} -{"id": 88004, "prover": "Nuprl", "theorem": "distrib_left", "goal": "all x,y,z:Int. (x * (y + z)) = ((x * y) + (x * z))", "context": ["Auto"], "tactic_proof": "Auto", "source": "nuprl_synthetic/arithmetic"} -{"id": 88005, "prover": "Nuprl", "theorem": "add_zero", "goal": "all x:Int. (x + 0) = x", "context": ["Auto"], "tactic_proof": "Auto", "source": "nuprl_synthetic/arithmetic"} -{"id": 88006, "prover": "Nuprl", "theorem": "mul_one", "goal": "all x:Int. (x * 1) = x", "context": ["Auto"], "tactic_proof": "Auto", "source": "nuprl_synthetic/arithmetic"} -{"id": 88007, "prover": "Nuprl", "theorem": "add_inverse", "goal": "all x:Int. (x + (-x)) = 0", "context": ["Auto"], "tactic_proof": "Auto", "source": "nuprl_synthetic/arithmetic"} -{"id": 88008, "prover": "Nuprl", "theorem": "nat_induction", "goal": "all P:(Nat -> Prop). P(0) => (all n:Nat. P(n) => P(n+1)) => all n:Nat. P(n)", "context": ["Intro", "NatInd", "Auto"], "tactic_proof": "Intro; Intro; NatInd; Auto", "source": "nuprl_synthetic/arithmetic"} -{"id": 88009, "prover": "Nuprl", "theorem": "div_mod", "goal": "all a:Int, b:PosInt. a = (b * (a / b)) + (a mod b)", "context": ["Auto"], "tactic_proof": "Auto", "source": "nuprl_synthetic/arithmetic"} -{"id": 88010, "prover": "Nuprl", "theorem": "abs_nonneg", "goal": "all x:Int. 0 <= |x|", "context": ["CaseAnalysis `x >= 0`", "Auto"], "tactic_proof": "CaseAnalysis `x >= 0`; Auto", "source": "nuprl_synthetic/arithmetic"} -{"id": 88011, "prover": "Nuprl", "theorem": "triangle_ineq", "goal": "all x,y:Int. |x + y| <= |x| + |y|", "context": ["CaseAnalysis `x >= 0`", "CaseAnalysis `y >= 0`", "Auto"], "tactic_proof": "CaseAnalysis `x >= 0`; CaseAnalysis `y >= 0`; Auto", "source": "nuprl_synthetic/arithmetic"} -{"id": 88012, "prover": "Nuprl", "theorem": "even_or_odd", "goal": "all n:Nat. (exists k:Nat. n = 2*k) or (exists k:Nat. n = 2*k + 1)", "context": ["NatInd", "Auto", "OrElim"], "tactic_proof": "NatInd; Auto; OrElim; Auto", "source": "nuprl_synthetic/arithmetic"} -{"id": 88013, "prover": "Nuprl", "theorem": "gcd_divides", "goal": "all a,b:PosInt. divides(gcd(a,b), a) & divides(gcd(a,b), b)", "context": ["Unfold `gcd`", "NatInd", "Auto"], "tactic_proof": "Unfold `gcd`; NatInd; Auto", "source": "nuprl_synthetic/arithmetic"} -{"id": 88014, "prover": "Nuprl", "theorem": "prime_factorization", "goal": "all n:Nat. n >= 2 => exists ps:List(PosInt). all p in ps. prime(p) & product(ps) = n", "context": ["StrongInduction", "Auto"], "tactic_proof": "StrongInduction; Auto", "source": "nuprl_synthetic/arithmetic"} -{"id": 88015, "prover": "Nuprl", "theorem": "pair_eta", "goal": "all A,B:Type, p:A*B. p = ", "context": ["Intro", "PairElim", "Auto"], "tactic_proof": "Intro; PairElim; Auto", "source": "nuprl_synthetic/types"} -{"id": 88016, "prover": "Nuprl", "theorem": "sum_elim", "goal": "all A,B:Type, C:Type. (A -> C) -> (B -> C) -> (A + B) -> C", "context": ["Intro", "DecideElim", "Auto"], "tactic_proof": "Intro; Intro; Intro; DecideElim; Auto", "source": "nuprl_synthetic/types"} -{"id": 88017, "prover": "Nuprl", "theorem": "void_elim", "goal": "all A:Type. Void -> A", "context": ["Intro", "VoidElim", "Auto"], "tactic_proof": "Intro; VoidElim; Auto", "source": "nuprl_synthetic/types"} -{"id": 88018, "prover": "Nuprl", "theorem": "unit_unique", "goal": "all x,y:Unit. x = y", "context": ["Intro", "UnitElim", "Auto"], "tactic_proof": "Intro; Intro; UnitElim; Auto", "source": "nuprl_synthetic/types"} -{"id": 88019, "prover": "Nuprl", "theorem": "func_ext", "goal": "all A,B:Type, f,g:A->B. (all x:A. f(x) = g(x)) => f = g", "context": ["Intro", "FunExt", "Auto"], "tactic_proof": "Intro; FunExt; Auto", "source": "nuprl_synthetic/types"} -{"id": 88020, "prover": "Nuprl", "theorem": "curry_uncurry", "goal": "all A,B,C:Type, f:A*B->C. uncurry(curry(f)) = f", "context": ["Intro", "FunExt", "PairElim", "Auto"], "tactic_proof": "Intro; FunExt; Intro; PairElim; Auto", "source": "nuprl_synthetic/types"} -{"id": 88021, "prover": "Nuprl", "theorem": "dep_pair_eta", "goal": "all A:Type, B:A->Type, p:(x:A * B(x)). p = ", "context": ["Intro", "DPairElim", "Auto"], "tactic_proof": "Intro; DPairElim; Auto", "source": "nuprl_synthetic/types"} -{"id": 88022, "prover": "Nuprl", "theorem": "iso_nat_list_unit", "goal": "all n:Nat. exists l:List(Unit). length(l) = n", "context": ["NatInd", "Auto", "Witness `cons(tt, l)`"], "tactic_proof": "NatInd; Auto; Witness `cons(tt, l)`; Auto", "source": "nuprl_synthetic/types"} -{"id": 88023, "prover": "Nuprl", "theorem": "type_product_comm", "goal": "all A,B:Type. A*B ~ B*A", "context": ["Intro", "Iso", "Lambda x. ", "Lambda y. ", "Auto"], "tactic_proof": "Intro; Iso; Lambda x. ; Lambda y. ; Auto", "source": "nuprl_synthetic/types"} -{"id": 88024, "prover": "Nuprl", "theorem": "type_sum_comm", "goal": "all A,B:Type. A+B ~ B+A", "context": ["Intro", "Iso", "DecideElim", "Auto"], "tactic_proof": "Intro; Iso; DecideElim; Auto", "source": "nuprl_synthetic/types"} -{"id": 88025, "prover": "Nuprl", "theorem": "append_nil", "goal": "all A:Type, l:List(A). append(l, nil) = l", "context": ["ListInd", "Auto"], "tactic_proof": "ListInd; Auto", "source": "nuprl_synthetic/lists"} -{"id": 88026, "prover": "Nuprl", "theorem": "append_assoc", "goal": "all A:Type, l1,l2,l3:List(A). append(append(l1,l2),l3) = append(l1,append(l2,l3))", "context": ["ListInd `l1`", "Auto"], "tactic_proof": "ListInd `l1`; Auto", "source": "nuprl_synthetic/lists"} -{"id": 88027, "prover": "Nuprl", "theorem": "length_append", "goal": "all A:Type, l1,l2:List(A). length(append(l1,l2)) = length(l1) + length(l2)", "context": ["ListInd `l1`", "Auto"], "tactic_proof": "ListInd `l1`; Auto", "source": "nuprl_synthetic/lists"} -{"id": 88028, "prover": "Nuprl", "theorem": "map_id", "goal": "all A:Type, l:List(A). map(id, l) = l", "context": ["ListInd", "Auto"], "tactic_proof": "ListInd; Auto", "source": "nuprl_synthetic/lists"} -{"id": 88029, "prover": "Nuprl", "theorem": "map_compose", "goal": "all A,B,C:Type, f:B->C, g:A->B, l:List(A). map(f, map(g, l)) = map(compose(f,g), l)", "context": ["ListInd", "Auto"], "tactic_proof": "ListInd; Auto", "source": "nuprl_synthetic/lists"} -{"id": 88030, "prover": "Nuprl", "theorem": "reverse_reverse", "goal": "all A:Type, l:List(A). reverse(reverse(l)) = l", "context": ["ListInd", "Auto", "Unfold `reverse`"], "tactic_proof": "ListInd; Auto; Unfold `reverse`; Auto", "source": "nuprl_synthetic/lists"} -{"id": 88031, "prover": "Nuprl", "theorem": "length_reverse", "goal": "all A:Type, l:List(A). length(reverse(l)) = length(l)", "context": ["ListInd", "Auto"], "tactic_proof": "ListInd; Auto", "source": "nuprl_synthetic/lists"} -{"id": 88032, "prover": "Nuprl", "theorem": "member_append", "goal": "all A:Type, x:A, l1,l2:List(A). member(x, append(l1,l2)) <=> member(x,l1) or member(x,l2)", "context": ["ListInd `l1`", "Auto", "OrElim"], "tactic_proof": "ListInd `l1`; Auto; OrElim; Auto", "source": "nuprl_synthetic/lists"} -{"id": 88033, "prover": "Nuprl", "theorem": "filter_length", "goal": "all A:Type, p:A->Bool, l:List(A). length(filter(p, l)) <= length(l)", "context": ["ListInd", "Auto", "CaseAnalysis `p(hd)`"], "tactic_proof": "ListInd; Auto; CaseAnalysis `p(hd)`; Auto", "source": "nuprl_synthetic/lists"} -{"id": 88034, "prover": "Nuprl", "theorem": "foldr_append", "goal": "all A,B:Type, f:A->B->B, z:B, l1,l2:List(A). foldr(f, z, append(l1,l2)) = foldr(f, foldr(f,z,l2), l1)", "context": ["ListInd `l1`", "Auto"], "tactic_proof": "ListInd `l1`; Auto", "source": "nuprl_synthetic/lists"} -{"id": 88035, "prover": "Nuprl", "theorem": "modus_ponens", "goal": "all P,Q:Prop. P => (P => Q) => Q", "context": ["Intro", "Apply", "Auto"], "tactic_proof": "Intro; Intro; Apply; Auto", "source": "nuprl_synthetic/logic"} -{"id": 88036, "prover": "Nuprl", "theorem": "and_comm", "goal": "all P,Q:Prop. P & Q => Q & P", "context": ["Intro", "AndElim", "Split", "Auto"], "tactic_proof": "Intro; AndElim; Split; Auto", "source": "nuprl_synthetic/logic"} -{"id": 88037, "prover": "Nuprl", "theorem": "or_comm", "goal": "all P,Q:Prop. P or Q => Q or P", "context": ["Intro", "OrElim", "Right", "Auto", "Left"], "tactic_proof": "Intro; OrElim; [Right; Auto | Left; Auto]", "source": "nuprl_synthetic/logic"} -{"id": 88038, "prover": "Nuprl", "theorem": "double_neg_elim", "goal": "all P:Prop. ~~P => P", "context": ["Intro", "ByContradiction", "Auto"], "tactic_proof": "Intro; ByContradiction; Auto", "source": "nuprl_synthetic/logic"} -{"id": 88039, "prover": "Nuprl", "theorem": "de_morgan_and", "goal": "all P,Q:Prop. ~(P & Q) <=> (~P or ~Q)", "context": ["Split", "Intro", "ByContradiction", "Auto", "OrElim"], "tactic_proof": "Split; Intro; ByContradiction; Auto; Intro; OrElim; Auto", "source": "nuprl_synthetic/logic"} -{"id": 88040, "prover": "Nuprl", "theorem": "de_morgan_or", "goal": "all P,Q:Prop. ~(P or Q) <=> (~P & ~Q)", "context": ["Split", "Intro", "Apply", "Left", "Auto", "Right", "AndElim", "OrElim"], "tactic_proof": "Split; Intro; Split; Intro; Apply; Left; Auto; Intro; Apply; Right; Auto; Intro; AndElim; OrElim; Auto", "source": "nuprl_synthetic/logic"} -{"id": 88041, "prover": "Nuprl", "theorem": "contrapositive", "goal": "all P,Q:Prop. (P => Q) => (~Q => ~P)", "context": ["Intro", "Apply", "Auto"], "tactic_proof": "Intro; Intro; Intro; Apply; Auto", "source": "nuprl_synthetic/logic"} -{"id": 88042, "prover": "Nuprl", "theorem": "forall_implies_exists", "goal": "all A:Type, P:A->Prop, a:A. (all x:A. P(x)) => exists x:A. P(x)", "context": ["Intro", "Witness `a`", "Apply", "Auto"], "tactic_proof": "Intro; Intro; Witness `a`; Apply; Auto", "source": "nuprl_synthetic/logic"} -{"id": 88043, "prover": "Nuprl", "theorem": "exists_not_forall_not", "goal": "all A:Type, P:A->Prop. (exists x:A. P(x)) => ~(all x:A. ~P(x))", "context": ["Intro", "ExistsElim", "Apply", "Auto"], "tactic_proof": "Intro; ExistsElim; Intro; Apply; Auto", "source": "nuprl_synthetic/logic"} -{"id": 88044, "prover": "Nuprl", "theorem": "peirce", "goal": "all P,Q:Prop. ((P => Q) => P) => P", "context": ["Intro", "ByContradiction", "Apply", "Absurd", "Auto"], "tactic_proof": "Intro; ByContradiction; Apply; Intro; Absurd; Auto", "source": "nuprl_synthetic/logic"} -{"id": 88045, "prover": "Nuprl", "theorem": "nat_decidable_eq", "goal": "all m,n:Nat. (m = n) or ~(m = n)", "context": ["NatInd `m`", "NatInd `n`", "Auto", "CaseAnalysis"], "tactic_proof": "NatInd `m`; NatInd `n`; Auto; CaseAnalysis; Auto", "source": "nuprl_synthetic/constructive"} -{"id": 88046, "prover": "Nuprl", "theorem": "markov_nat", "goal": "all f:Nat->Bool. ~~(exists n:Nat. f(n) = true) => exists n:Nat. f(n) = true", "context": ["Intro", "BoundedSearch", "Auto"], "tactic_proof": "Intro; BoundedSearch; Auto", "source": "nuprl_synthetic/constructive"} -{"id": 88047, "prover": "Nuprl", "theorem": "choice_nat", "goal": "all R:Nat->Nat->Prop. (all n:Nat. exists m:Nat. R(n,m)) => exists f:Nat->Nat. all n:Nat. R(n, f(n))", "context": ["Intro", "CountableChoice", "Auto"], "tactic_proof": "Intro; CountableChoice; Auto", "source": "nuprl_synthetic/constructive"} -{"id": 88048, "prover": "Nuprl", "theorem": "well_ordering_nat", "goal": "all P:Nat->Prop. (exists n:Nat. P(n)) => exists m:Nat. P(m) & (all k:Nat. k < m => ~P(k))", "context": ["StrongInduction", "Auto"], "tactic_proof": "StrongInduction; Auto", "source": "nuprl_synthetic/constructive"} -{"id": 88049, "prover": "Nuprl", "theorem": "brouwer_continuity", "goal": "all f:(Nat->Nat)->Nat. exists n:Nat. all a,b:Nat->Nat. (all i:Nat. i < n => a(i) = b(i)) => f(a) = f(b)", "context": ["Continuity", "Auto"], "tactic_proof": "Continuity; Auto", "source": "nuprl_synthetic/constructive"} +{"id":88000,"prover":"Nuprl","theorem":"add_comm","goal":"all x,y:Int. (x + y) = (y + x)","context":["Auto"],"tactic_proof":"Auto","source":"nuprl_synthetic/arithmetic"} +{"id":88001,"prover":"Nuprl","theorem":"add_assoc","goal":"all x,y,z:Int. ((x + y) + z) = (x + (y + z))","context":["Auto"],"tactic_proof":"Auto","source":"nuprl_synthetic/arithmetic"} +{"id":88002,"prover":"Nuprl","theorem":"mul_comm","goal":"all x,y:Int. (x * y) = (y * x)","context":["Auto"],"tactic_proof":"Auto","source":"nuprl_synthetic/arithmetic"} +{"id":88003,"prover":"Nuprl","theorem":"mul_assoc","goal":"all x,y,z:Int. ((x * y) * z) = (x * (y * z))","context":["Auto"],"tactic_proof":"Auto","source":"nuprl_synthetic/arithmetic"} +{"id":88004,"prover":"Nuprl","theorem":"distrib_left","goal":"all x,y,z:Int. (x * (y + z)) = ((x * y) + (x * z))","context":["Auto"],"tactic_proof":"Auto","source":"nuprl_synthetic/arithmetic"} +{"id":88005,"prover":"Nuprl","theorem":"add_zero","goal":"all x:Int. (x + 0) = x","context":["Auto"],"tactic_proof":"Auto","source":"nuprl_synthetic/arithmetic"} +{"id":88006,"prover":"Nuprl","theorem":"mul_one","goal":"all x:Int. (x * 1) = x","context":["Auto"],"tactic_proof":"Auto","source":"nuprl_synthetic/arithmetic"} +{"id":88007,"prover":"Nuprl","theorem":"add_inverse","goal":"all x:Int. (x + (-x)) = 0","context":["Auto"],"tactic_proof":"Auto","source":"nuprl_synthetic/arithmetic"} +{"id":88008,"prover":"Nuprl","theorem":"nat_induction","goal":"all P:(Nat -> Prop). P(0) => (all n:Nat. P(n) => P(n+1)) => all n:Nat. P(n)","context":["Intro","NatInd","Auto"],"tactic_proof":"Intro; Intro; NatInd; Auto","source":"nuprl_synthetic/arithmetic"} +{"id":88009,"prover":"Nuprl","theorem":"div_mod","goal":"all a:Int, b:PosInt. a = (b * (a / b)) + (a mod b)","context":["Auto"],"tactic_proof":"Auto","source":"nuprl_synthetic/arithmetic"} +{"id":88010,"prover":"Nuprl","theorem":"abs_nonneg","goal":"all x:Int. 0 <= |x|","context":["CaseAnalysis `x >= 0`","Auto"],"tactic_proof":"CaseAnalysis `x >= 0`; Auto","source":"nuprl_synthetic/arithmetic"} +{"id":88011,"prover":"Nuprl","theorem":"triangle_ineq","goal":"all x,y:Int. |x + y| <= |x| + |y|","context":["CaseAnalysis `x >= 0`","CaseAnalysis `y >= 0`","Auto"],"tactic_proof":"CaseAnalysis `x >= 0`; CaseAnalysis `y >= 0`; Auto","source":"nuprl_synthetic/arithmetic"} +{"id":88012,"prover":"Nuprl","theorem":"even_or_odd","goal":"all n:Nat. (exists k:Nat. n = 2*k) or (exists k:Nat. n = 2*k + 1)","context":["NatInd","Auto","OrElim"],"tactic_proof":"NatInd; Auto; OrElim; Auto","source":"nuprl_synthetic/arithmetic"} +{"id":88013,"prover":"Nuprl","theorem":"gcd_divides","goal":"all a,b:PosInt. divides(gcd(a,b), a) & divides(gcd(a,b), b)","context":["Unfold `gcd`","NatInd","Auto"],"tactic_proof":"Unfold `gcd`; NatInd; Auto","source":"nuprl_synthetic/arithmetic"} +{"id":88014,"prover":"Nuprl","theorem":"prime_factorization","goal":"all n:Nat. n >= 2 => exists ps:List(PosInt). all p in ps. prime(p) & product(ps) = n","context":["StrongInduction","Auto"],"tactic_proof":"StrongInduction; Auto","source":"nuprl_synthetic/arithmetic"} +{"id":88015,"prover":"Nuprl","theorem":"pair_eta","goal":"all A,B:Type, p:A*B. p = ","context":["Intro","PairElim","Auto"],"tactic_proof":"Intro; PairElim; Auto","source":"nuprl_synthetic/types"} +{"id":88016,"prover":"Nuprl","theorem":"sum_elim","goal":"all A,B:Type, C:Type. (A -> C) -> (B -> C) -> (A + B) -> C","context":["Intro","DecideElim","Auto"],"tactic_proof":"Intro; Intro; Intro; DecideElim; Auto","source":"nuprl_synthetic/types"} +{"id":88017,"prover":"Nuprl","theorem":"void_elim","goal":"all A:Type. Void -> A","context":["Intro","VoidElim","Auto"],"tactic_proof":"Intro; VoidElim; Auto","source":"nuprl_synthetic/types"} +{"id":88018,"prover":"Nuprl","theorem":"unit_unique","goal":"all x,y:Unit. x = y","context":["Intro","UnitElim","Auto"],"tactic_proof":"Intro; Intro; UnitElim; Auto","source":"nuprl_synthetic/types"} +{"id":88019,"prover":"Nuprl","theorem":"func_ext","goal":"all A,B:Type, f,g:A->B. (all x:A. f(x) = g(x)) => f = g","context":["Intro","FunExt","Auto"],"tactic_proof":"Intro; FunExt; Auto","source":"nuprl_synthetic/types"} +{"id":88020,"prover":"Nuprl","theorem":"curry_uncurry","goal":"all A,B,C:Type, f:A*B->C. uncurry(curry(f)) = f","context":["Intro","FunExt","PairElim","Auto"],"tactic_proof":"Intro; FunExt; Intro; PairElim; Auto","source":"nuprl_synthetic/types"} +{"id":88021,"prover":"Nuprl","theorem":"dep_pair_eta","goal":"all A:Type, B:A->Type, p:(x:A * B(x)). p = ","context":["Intro","DPairElim","Auto"],"tactic_proof":"Intro; DPairElim; Auto","source":"nuprl_synthetic/types"} +{"id":88022,"prover":"Nuprl","theorem":"iso_nat_list_unit","goal":"all n:Nat. exists l:List(Unit). length(l) = n","context":["NatInd","Auto","Witness `cons(tt, l)`"],"tactic_proof":"NatInd; Auto; Witness `cons(tt, l)`; Auto","source":"nuprl_synthetic/types"} +{"id":88023,"prover":"Nuprl","theorem":"type_product_comm","goal":"all A,B:Type. A*B ~ B*A","context":["Intro","Iso","Lambda x. ","Lambda y. ","Auto"],"tactic_proof":"Intro; Iso; Lambda x. ; Lambda y. ; Auto","source":"nuprl_synthetic/types"} +{"id":88024,"prover":"Nuprl","theorem":"type_sum_comm","goal":"all A,B:Type. A+B ~ B+A","context":["Intro","Iso","DecideElim","Auto"],"tactic_proof":"Intro; Iso; DecideElim; Auto","source":"nuprl_synthetic/types"} +{"id":88025,"prover":"Nuprl","theorem":"append_nil","goal":"all A:Type, l:List(A). append(l, nil) = l","context":["ListInd","Auto"],"tactic_proof":"ListInd; Auto","source":"nuprl_synthetic/lists"} +{"id":88026,"prover":"Nuprl","theorem":"append_assoc","goal":"all A:Type, l1,l2,l3:List(A). append(append(l1,l2),l3) = append(l1,append(l2,l3))","context":["ListInd `l1`","Auto"],"tactic_proof":"ListInd `l1`; Auto","source":"nuprl_synthetic/lists"} +{"id":88027,"prover":"Nuprl","theorem":"length_append","goal":"all A:Type, l1,l2:List(A). length(append(l1,l2)) = length(l1) + length(l2)","context":["ListInd `l1`","Auto"],"tactic_proof":"ListInd `l1`; Auto","source":"nuprl_synthetic/lists"} +{"id":88028,"prover":"Nuprl","theorem":"map_id","goal":"all A:Type, l:List(A). map(id, l) = l","context":["ListInd","Auto"],"tactic_proof":"ListInd; Auto","source":"nuprl_synthetic/lists"} +{"id":88029,"prover":"Nuprl","theorem":"map_compose","goal":"all A,B,C:Type, f:B->C, g:A->B, l:List(A). map(f, map(g, l)) = map(compose(f,g), l)","context":["ListInd","Auto"],"tactic_proof":"ListInd; Auto","source":"nuprl_synthetic/lists"} +{"id":88030,"prover":"Nuprl","theorem":"reverse_reverse","goal":"all A:Type, l:List(A). reverse(reverse(l)) = l","context":["ListInd","Auto","Unfold `reverse`"],"tactic_proof":"ListInd; Auto; Unfold `reverse`; Auto","source":"nuprl_synthetic/lists"} +{"id":88031,"prover":"Nuprl","theorem":"length_reverse","goal":"all A:Type, l:List(A). length(reverse(l)) = length(l)","context":["ListInd","Auto"],"tactic_proof":"ListInd; Auto","source":"nuprl_synthetic/lists"} +{"id":88032,"prover":"Nuprl","theorem":"member_append","goal":"all A:Type, x:A, l1,l2:List(A). member(x, append(l1,l2)) <=> member(x,l1) or member(x,l2)","context":["ListInd `l1`","Auto","OrElim"],"tactic_proof":"ListInd `l1`; Auto; OrElim; Auto","source":"nuprl_synthetic/lists"} +{"id":88033,"prover":"Nuprl","theorem":"filter_length","goal":"all A:Type, p:A->Bool, l:List(A). length(filter(p, l)) <= length(l)","context":["ListInd","Auto","CaseAnalysis `p(hd)`"],"tactic_proof":"ListInd; Auto; CaseAnalysis `p(hd)`; Auto","source":"nuprl_synthetic/lists"} +{"id":88034,"prover":"Nuprl","theorem":"foldr_append","goal":"all A,B:Type, f:A->B->B, z:B, l1,l2:List(A). foldr(f, z, append(l1,l2)) = foldr(f, foldr(f,z,l2), l1)","context":["ListInd `l1`","Auto"],"tactic_proof":"ListInd `l1`; Auto","source":"nuprl_synthetic/lists"} +{"id":88035,"prover":"Nuprl","theorem":"modus_ponens","goal":"all P,Q:Prop. P => (P => Q) => Q","context":["Intro","Apply","Auto"],"tactic_proof":"Intro; Intro; Apply; Auto","source":"nuprl_synthetic/logic"} +{"id":88036,"prover":"Nuprl","theorem":"and_comm","goal":"all P,Q:Prop. P & Q => Q & P","context":["Intro","AndElim","Split","Auto"],"tactic_proof":"Intro; AndElim; Split; Auto","source":"nuprl_synthetic/logic"} +{"id":88037,"prover":"Nuprl","theorem":"or_comm","goal":"all P,Q:Prop. P or Q => Q or P","context":["Intro","OrElim","Right","Auto","Left"],"tactic_proof":"Intro; OrElim; [Right; Auto | Left; Auto]","source":"nuprl_synthetic/logic"} +{"id":88038,"prover":"Nuprl","theorem":"double_neg_elim","goal":"all P:Prop. ~~P => P","context":["Intro","ByContradiction","Auto"],"tactic_proof":"Intro; ByContradiction; Auto","source":"nuprl_synthetic/logic"} +{"id":88039,"prover":"Nuprl","theorem":"de_morgan_and","goal":"all P,Q:Prop. ~(P & Q) <=> (~P or ~Q)","context":["Split","Intro","ByContradiction","Auto","OrElim"],"tactic_proof":"Split; Intro; ByContradiction; Auto; Intro; OrElim; Auto","source":"nuprl_synthetic/logic"} +{"id":88040,"prover":"Nuprl","theorem":"de_morgan_or","goal":"all P,Q:Prop. ~(P or Q) <=> (~P & ~Q)","context":["Split","Intro","Apply","Left","Auto","Right","AndElim","OrElim"],"tactic_proof":"Split; Intro; Split; Intro; Apply; Left; Auto; Intro; Apply; Right; Auto; Intro; AndElim; OrElim; Auto","source":"nuprl_synthetic/logic"} +{"id":88041,"prover":"Nuprl","theorem":"contrapositive","goal":"all P,Q:Prop. (P => Q) => (~Q => ~P)","context":["Intro","Apply","Auto"],"tactic_proof":"Intro; Intro; Intro; Apply; Auto","source":"nuprl_synthetic/logic"} +{"id":88042,"prover":"Nuprl","theorem":"forall_implies_exists","goal":"all A:Type, P:A->Prop, a:A. (all x:A. P(x)) => exists x:A. P(x)","context":["Intro","Witness `a`","Apply","Auto"],"tactic_proof":"Intro; Intro; Witness `a`; Apply; Auto","source":"nuprl_synthetic/logic"} +{"id":88043,"prover":"Nuprl","theorem":"exists_not_forall_not","goal":"all A:Type, P:A->Prop. (exists x:A. P(x)) => ~(all x:A. ~P(x))","context":["Intro","ExistsElim","Apply","Auto"],"tactic_proof":"Intro; ExistsElim; Intro; Apply; Auto","source":"nuprl_synthetic/logic"} +{"id":88044,"prover":"Nuprl","theorem":"peirce","goal":"all P,Q:Prop. ((P => Q) => P) => P","context":["Intro","ByContradiction","Apply","Absurd","Auto"],"tactic_proof":"Intro; ByContradiction; Apply; Intro; Absurd; Auto","source":"nuprl_synthetic/logic"} +{"id":88045,"prover":"Nuprl","theorem":"nat_decidable_eq","goal":"all m,n:Nat. (m = n) or ~(m = n)","context":["NatInd `m`","NatInd `n`","Auto","CaseAnalysis"],"tactic_proof":"NatInd `m`; NatInd `n`; Auto; CaseAnalysis; Auto","source":"nuprl_synthetic/constructive"} +{"id":88046,"prover":"Nuprl","theorem":"markov_nat","goal":"all f:Nat->Bool. ~~(exists n:Nat. f(n) = true) => exists n:Nat. f(n) = true","context":["Intro","BoundedSearch","Auto"],"tactic_proof":"Intro; BoundedSearch; Auto","source":"nuprl_synthetic/constructive"} +{"id":88047,"prover":"Nuprl","theorem":"choice_nat","goal":"all R:Nat->Nat->Prop. (all n:Nat. exists m:Nat. R(n,m)) => exists f:Nat->Nat. all n:Nat. R(n, f(n))","context":["Intro","CountableChoice","Auto"],"tactic_proof":"Intro; CountableChoice; Auto","source":"nuprl_synthetic/constructive"} +{"id":88048,"prover":"Nuprl","theorem":"well_ordering_nat","goal":"all P:Nat->Prop. (exists n:Nat. P(n)) => exists m:Nat. P(m) & (all k:Nat. k < m => ~P(k))","context":["StrongInduction","Auto"],"tactic_proof":"StrongInduction; Auto","source":"nuprl_synthetic/constructive"} +{"id":88049,"prover":"Nuprl","theorem":"brouwer_continuity","goal":"all f:(Nat->Nat)->Nat. exists n:Nat. all a,b:Nat->Nat. (all i:Nat. i < n => a(i) = b(i)) => f(a) = f(b)","context":["Continuity","Auto"],"tactic_proof":"Continuity; Auto","source":"nuprl_synthetic/constructive"} +{"id":88050,"prover":"Nuprl","theorem":"church_rosser","goal":"all M,N,P:Term. reduces(M, N) => reduces(M, P) => exists Q:Term. reduces(N, Q) & reduces(P, Q)","context":["Induction","Diamond","Auto"],"tactic_proof":"Induction; Diamond; Auto","source":"nuprl_synthetic/constructive"} +{"id":88051,"prover":"Nuprl","theorem":"fan_theorem","goal":"all T:Tree. (all b:Branch. bar(T, b)) => exists n:Nat. uniform_bar(T, n)","context":["BarInduction","Auto"],"tactic_proof":"BarInduction; Auto","source":"nuprl_synthetic/constructive"} +{"id":88052,"prover":"Nuprl","theorem":"kripke_schema","goal":"all A:Prop. (A \\/ ~A) => decidable(A)","context":["Intro","OrElim","Auto"],"tactic_proof":"Intro; OrElim; Auto","source":"nuprl_synthetic/constructive"} +{"id":88053,"prover":"Nuprl","theorem":"set_ext","goal":"all A:Type, s1,s2:Set(A). (all x:A. x in s1 <=> x in s2) => s1 = s2","context":["Intro","SetExt","Auto"],"tactic_proof":"Intro; SetExt; Auto","source":"nuprl_synthetic/sets"} +{"id":88054,"prover":"Nuprl","theorem":"union_comm","goal":"all A:Type, s1,s2:Set(A). union(s1, s2) = union(s2, s1)","context":["SetExt","Auto"],"tactic_proof":"SetExt; Auto","source":"nuprl_synthetic/sets"} +{"id":88055,"prover":"Nuprl","theorem":"union_assoc","goal":"all A:Type, s1,s2,s3:Set(A). union(union(s1,s2),s3) = union(s1,union(s2,s3))","context":["SetExt","Auto"],"tactic_proof":"SetExt; Auto","source":"nuprl_synthetic/sets"} +{"id":88056,"prover":"Nuprl","theorem":"inter_comm","goal":"all A:Type, s1,s2:Set(A). intersect(s1, s2) = intersect(s2, s1)","context":["SetExt","Auto"],"tactic_proof":"SetExt; Auto","source":"nuprl_synthetic/sets"} +{"id":88057,"prover":"Nuprl","theorem":"distrib_union_inter","goal":"all A:Type, s1,s2,s3:Set(A). union(s1, intersect(s2, s3)) = intersect(union(s1,s2), union(s1,s3))","context":["SetExt","Auto"],"tactic_proof":"SetExt; Auto","source":"nuprl_synthetic/sets"} +{"id":88058,"prover":"Nuprl","theorem":"empty_subset","goal":"all A:Type, s:Set(A). subset(empty, s)","context":["Intro","ElimEmpty","Auto"],"tactic_proof":"Intro; ElimEmpty; Auto","source":"nuprl_synthetic/sets"} +{"id":88059,"prover":"Nuprl","theorem":"union_superset","goal":"all A:Type, s1,s2:Set(A). subset(s1, union(s1, s2))","context":["Intro","UnionElim","Auto"],"tactic_proof":"Intro; UnionElim; Auto","source":"nuprl_synthetic/sets"} +{"id":88060,"prover":"Nuprl","theorem":"power_set_monotone","goal":"all A:Type, s1,s2:Set(A). subset(s1, s2) => subset(pow(s1), pow(s2))","context":["Intro","Apply","Auto"],"tactic_proof":"Intro; Intro; Apply; Auto","source":"nuprl_synthetic/sets"} +{"id":88061,"prover":"Nuprl","theorem":"finite_union","goal":"all A:Type, s1,s2:FiniteSet(A). finite(union(s1, s2))","context":["Intro","FiniteUnion","Auto"],"tactic_proof":"Intro; FiniteUnion; Auto","source":"nuprl_synthetic/sets"} +{"id":88062,"prover":"Nuprl","theorem":"cardinal_union","goal":"all A:Type, s1,s2:FiniteSet(A). card(union(s1,s2)) = card(s1) + card(s2) - card(intersect(s1,s2))","context":["InclusionExclusion","Auto"],"tactic_proof":"InclusionExclusion; Auto","source":"nuprl_synthetic/sets"} +{"id":88063,"prover":"Nuprl","theorem":"refl_closure","goal":"all A:Type, R:A->A->Prop, x:A. refl_trans_closure(R)(x, x)","context":["Intro","RTC_Refl","Auto"],"tactic_proof":"Intro; RTC_Refl; Auto","source":"nuprl_synthetic/relations"} +{"id":88064,"prover":"Nuprl","theorem":"trans_composition","goal":"all A:Type, R:A->A->Prop, x,y,z:A. trans_closure(R)(x,y) => trans_closure(R)(y,z) => trans_closure(R)(x,z)","context":["Intro","Induction","Auto"],"tactic_proof":"Intro; Induction; Auto","source":"nuprl_synthetic/relations"} +{"id":88065,"prover":"Nuprl","theorem":"equiv_sym","goal":"all A:Type, R:A->A->Prop, x,y:A. equivalence(R) => R(x, y) => R(y, x)","context":["Intro","ApplySym","Auto"],"tactic_proof":"Intro; Intro; ApplySym; Auto","source":"nuprl_synthetic/relations"} +{"id":88066,"prover":"Nuprl","theorem":"well_founded_induction","goal":"all A:Type, R:A->A->Prop. well_founded(R) => all P:A->Prop. (all x:A. (all y:A. R(y,x) => P(y)) => P(x)) => all x:A. P(x)","context":["Intro","WFInduction","Auto"],"tactic_proof":"Intro; WFInduction; Auto","source":"nuprl_synthetic/relations"} +{"id":88067,"prover":"Nuprl","theorem":"partial_order_antisym","goal":"all A:Type, R:A->A->Prop, x,y:A. partial_order(R) => R(x,y) => R(y,x) => x = y","context":["Intro","ApplyAntisym","Auto"],"tactic_proof":"Intro; ApplyAntisym; Auto","source":"nuprl_synthetic/relations"} +{"id":88068,"prover":"Nuprl","theorem":"total_order_trichotomy","goal":"all A:Type, R:A->A->Prop, x,y:A. total_order(R) => R(x,y) \\/ x = y \\/ R(y,x)","context":["Intro","Trichotomy","Auto"],"tactic_proof":"Intro; Trichotomy; Auto","source":"nuprl_synthetic/relations"} +{"id":88069,"prover":"Nuprl","theorem":"graph_path_compose","goal":"all V:Type, E:V->V->Prop, x,y,z:V. path(E)(x,y) => path(E)(y,z) => path(E)(x,z)","context":["Induction","Auto"],"tactic_proof":"Induction; Auto","source":"nuprl_synthetic/relations"} +{"id":88070,"prover":"Nuprl","theorem":"converse_relation","goal":"all A,B:Type, R:A->B->Prop, x:A, y:B. R(x,y) <=> converse(R)(y,x)","context":["Intro","Split","Auto"],"tactic_proof":"Intro; Split; Auto","source":"nuprl_synthetic/relations"} +{"id":88071,"prover":"Nuprl","theorem":"euclid_lemma","goal":"all p:Prime, a,b:Nat. divides(p, a*b) => divides(p, a) or divides(p, b)","context":["Intro","CaseGCD","Auto"],"tactic_proof":"Intro; CaseGCD; Auto","source":"nuprl_synthetic/number_theory"} +{"id":88072,"prover":"Nuprl","theorem":"fundamental_arith","goal":"all n:Nat. n >= 2 => exists! ps:List(Prime). product(ps) = n","context":["StrongInduction","Auto"],"tactic_proof":"StrongInduction; Auto","source":"nuprl_synthetic/number_theory"} +{"id":88073,"prover":"Nuprl","theorem":"bezout","goal":"all a,b:Nat. a > 0 \\/ b > 0 => exists x,y:Int. a*x + b*y = gcd(a,b)","context":["Intro","ExtendedEuclid","Auto"],"tactic_proof":"Intro; ExtendedEuclid; Auto","source":"nuprl_synthetic/number_theory"} +{"id":88074,"prover":"Nuprl","theorem":"infinitude_primes","goal":"all n:Nat. exists p:Prime. p > n","context":["Intro","Witness `factorial(n)+1`","Auto"],"tactic_proof":"Intro; Witness `factorial(n)+1`; Auto","source":"nuprl_synthetic/number_theory"} +{"id":88075,"prover":"Nuprl","theorem":"wilson_theorem","goal":"all p:Prime. (factorial(p-1) + 1) mod p = 0","context":["Intro","ModArith","Auto"],"tactic_proof":"Intro; ModArith; Auto","source":"nuprl_synthetic/number_theory"} +{"id":88076,"prover":"Nuprl","theorem":"fermat_little","goal":"all p:Prime, a:Nat. coprime(a, p) => (a^(p-1)) mod p = 1","context":["Intro","GroupOrder","Auto"],"tactic_proof":"Intro; GroupOrder; Auto","source":"nuprl_synthetic/number_theory"} +{"id":88077,"prover":"Nuprl","theorem":"chinese_remainder","goal":"all m,n:Nat. coprime(m,n) => all a,b:Int. exists x:Int. (x mod m = a) & (x mod n = b)","context":["Intro","CRT","Auto"],"tactic_proof":"Intro; Intro; CRT; Auto","source":"nuprl_synthetic/number_theory"} +{"id":88078,"prover":"Nuprl","theorem":"sum_of_squares","goal":"all n:Nat. (exists a,b:Nat. n = a*a + b*b) <=> all p:Prime. p `divides` n & p mod 4 = 3 => even(mult(p, n))","context":["Classify","Auto"],"tactic_proof":"Classify; Auto","source":"nuprl_synthetic/number_theory"} +{"id":88079,"prover":"Nuprl","theorem":"pigeon_hole","goal":"all n,m:Nat, f:Fin(n)->Fin(m). n > m => exists i,j:Fin(n). i <> j & f(i) = f(j)","context":["Intro","PHP","Auto"],"tactic_proof":"Intro; PHP; Auto","source":"nuprl_synthetic/number_theory"} +{"id":88080,"prover":"Nuprl","theorem":"lim_sum","goal":"all f,g:Nat->Real, a,b:Real. lim(f) = a => lim(g) = b => lim(fun n. f(n)+g(n)) = a+b","context":["Intro","LimitArith","Auto"],"tactic_proof":"Intro; LimitArith; Auto","source":"nuprl_synthetic/real_analysis"} +{"id":88081,"prover":"Nuprl","theorem":"lim_prod","goal":"all f,g:Nat->Real, a,b:Real. lim(f) = a => lim(g) = b => lim(fun n. f(n)*g(n)) = a*b","context":["Intro","LimitArith","Auto"],"tactic_proof":"Intro; LimitArith; Auto","source":"nuprl_synthetic/real_analysis"} +{"id":88082,"prover":"Nuprl","theorem":"squeeze","goal":"all f,g,h:Nat->Real. (all n:Nat. f(n) <= g(n) <= h(n)) => lim(f) = lim(h) => lim(g) = lim(f)","context":["Intro","Squeeze","Auto"],"tactic_proof":"Intro; Squeeze; Auto","source":"nuprl_synthetic/real_analysis"} +{"id":88083,"prover":"Nuprl","theorem":"continuous_compose","goal":"all f,g:Real->Real. continuous(f) => continuous(g) => continuous(compose(f, g))","context":["Intro","EpsilonDelta","Auto"],"tactic_proof":"Intro; EpsilonDelta; Auto","source":"nuprl_synthetic/real_analysis"} +{"id":88084,"prover":"Nuprl","theorem":"ivt","goal":"all f:Real->Real, a,b:Real, y:Real. continuous(f) => f(a) <= y <= f(b) => exists c:Real. a <= c <= b & f(c) = y","context":["Intro","Bisection","Auto"],"tactic_proof":"Intro; Bisection; Auto","source":"nuprl_synthetic/real_analysis"} +{"id":88085,"prover":"Nuprl","theorem":"mvt","goal":"all f:Real->Real, a,b:Real. differentiable(f) => a < b => exists c:Real. a < c < b & derivative(f)(c) = (f(b)-f(a))/(b-a)","context":["Intro","Rolle","Auto"],"tactic_proof":"Intro; Rolle; Auto","source":"nuprl_synthetic/real_analysis"} +{"id":88086,"prover":"Nuprl","theorem":"cauchy_complete","goal":"all s:Nat->Real. cauchy(s) => exists L:Real. lim(s) = L","context":["Intro","CompletenessAxiom","Auto"],"tactic_proof":"Intro; CompletenessAxiom; Auto","source":"nuprl_synthetic/real_analysis"} +{"id":88087,"prover":"Nuprl","theorem":"compact_attains","goal":"all f:Real->Real, K:Set(Real). compact(K) => continuous(f) => exists m,M:Real. m in f(K) & M in f(K) & all y in f(K). m <= y <= M","context":["Intro","ExtremeValue","Auto"],"tactic_proof":"Intro; Intro; ExtremeValue; Auto","source":"nuprl_synthetic/real_analysis"} +{"id":88088,"prover":"Nuprl","theorem":"halting_undecidable","goal":"~exists H:(Prog->Input->Bool). all p:Prog, x:Input. H(p, x) = true <=> halts(p, x)","context":["Diagonalization","Auto"],"tactic_proof":"Diagonalization; Auto","source":"nuprl_synthetic/computability"} +{"id":88089,"prover":"Nuprl","theorem":"rice_theorem","goal":"all P:(Prog->Prop). nontrivial(P) => ~decidable(P)","context":["Intro","Reduction","Auto"],"tactic_proof":"Intro; Reduction; Auto","source":"nuprl_synthetic/computability"} +{"id":88090,"prover":"Nuprl","theorem":"recursion_theorem","goal":"all f:Prog->Prog. exists e:Prog. equal_programs(e, f(e))","context":["KleeneRecursion","Auto"],"tactic_proof":"KleeneRecursion; Auto","source":"nuprl_synthetic/computability"} +{"id":88091,"prover":"Nuprl","theorem":"smn_theorem","goal":"all n,m:Nat, f:Prog. exists s:Prog. all x,y:Input. run(f, pair(x,y)) = run(run(s, x), y)","context":["Intro","SMN","Auto"],"tactic_proof":"Intro; Intro; SMN; Auto","source":"nuprl_synthetic/computability"} +{"id":88092,"prover":"Nuprl","theorem":"kleene_normal","goal":"all f:PartialFn. exists e,U:Prog. all x:Input. f(x) = run(U, pair(e, x))","context":["Intro","NormalForm","Auto"],"tactic_proof":"Intro; NormalForm; Auto","source":"nuprl_synthetic/computability"} +{"id":88093,"prover":"Nuprl","theorem":"church_turing_lambda","goal":"all f:ComputableFn. exists t:Term. reduces_to_numeral(t(numeral(x)), numeral(f(x)))","context":["Intro","Encode","Auto"],"tactic_proof":"Intro; Encode; Auto","source":"nuprl_synthetic/computability"} +{"id":88094,"prover":"Nuprl","theorem":"cat_comp_assoc","goal":"all C:Cat, f:Hom(a,b), g:Hom(b,c), h:Hom(c,d). comp(comp(h,g),f) = comp(h,comp(g,f))","context":["Intro","CatAssoc","Auto"],"tactic_proof":"Intro; CatAssoc; Auto","source":"nuprl_synthetic/category_theory"} +{"id":88095,"prover":"Nuprl","theorem":"cat_id_left","goal":"all C:Cat, f:Hom(a,b). comp(id(b), f) = f","context":["Intro","CatIdLeft","Auto"],"tactic_proof":"Intro; CatIdLeft; Auto","source":"nuprl_synthetic/category_theory"} +{"id":88096,"prover":"Nuprl","theorem":"cat_id_right","goal":"all C:Cat, f:Hom(a,b). comp(f, id(a)) = f","context":["Intro","CatIdRight","Auto"],"tactic_proof":"Intro; CatIdRight; Auto","source":"nuprl_synthetic/category_theory"} +{"id":88097,"prover":"Nuprl","theorem":"functor_comp","goal":"all F:Functor, f:Hom(a,b), g:Hom(b,c). Fmap(comp(g,f)) = comp(Fmap(g), Fmap(f))","context":["Intro","FunctorLaw","Auto"],"tactic_proof":"Intro; FunctorLaw; Auto","source":"nuprl_synthetic/category_theory"} +{"id":88098,"prover":"Nuprl","theorem":"functor_id","goal":"all F:Functor, a:Obj. Fmap(id(a)) = id(Fobj(a))","context":["Intro","FunctorIdLaw","Auto"],"tactic_proof":"Intro; FunctorIdLaw; Auto","source":"nuprl_synthetic/category_theory"} +{"id":88099,"prover":"Nuprl","theorem":"natural_trans","goal":"all F,G:Functor, eta:NatTrans(F,G), f:Hom(a,b). comp(eta(b), Fmap_F(f)) = comp(Fmap_G(f), eta(a))","context":["Intro","Naturality","Auto"],"tactic_proof":"Intro; Naturality; Auto","source":"nuprl_synthetic/category_theory"} +{"id":88100,"prover":"Nuprl","theorem":"iso_compose","goal":"all C:Cat, f:Hom(a,b), g:Hom(b,a). comp(g, f) = id(a) => comp(f, g) = id(b) => isomorphism(f)","context":["Intro","Isomorphism","Auto"],"tactic_proof":"Intro; Isomorphism; Auto","source":"nuprl_synthetic/category_theory"} +{"id":88101,"prover":"Nuprl","theorem":"product_universal","goal":"all C:Cat, p:Obj, f:Hom(p,a), g:Hom(p,b). exists! h:Hom(p, prod(a,b)). comp(pi1, h) = f & comp(pi2, h) = g","context":["Intro","Universal","Auto"],"tactic_proof":"Intro; Universal; Auto","source":"nuprl_synthetic/category_theory"} +{"id":88102,"prover":"Nuprl","theorem":"open_union","goal":"all X:TopSpace, U,V:Open(X). open(union(U, V))","context":["Intro","OpenAxiom","Auto"],"tactic_proof":"Intro; OpenAxiom; Auto","source":"nuprl_synthetic/topology"} +{"id":88103,"prover":"Nuprl","theorem":"open_finite_inter","goal":"all X:TopSpace, U,V:Open(X). open(intersect(U, V))","context":["Intro","OpenAxiom","Auto"],"tactic_proof":"Intro; OpenAxiom; Auto","source":"nuprl_synthetic/topology"} +{"id":88104,"prover":"Nuprl","theorem":"continuous_compose","goal":"all X,Y,Z:TopSpace, f:X->Y, g:Y->Z. continuous(f) => continuous(g) => continuous(compose(g, f))","context":["Intro","Continuous","Auto"],"tactic_proof":"Intro; Continuous; Auto","source":"nuprl_synthetic/topology"} +{"id":88105,"prover":"Nuprl","theorem":"compact_closed","goal":"all X:TopSpace, K:Subspace(X). compact(K) => hausdorff(X) => closed(K)","context":["Intro","Compact","Auto"],"tactic_proof":"Intro; Compact; Auto","source":"nuprl_synthetic/topology"} +{"id":88106,"prover":"Nuprl","theorem":"connected_image","goal":"all X,Y:TopSpace, f:X->Y. continuous(f) => connected(X) => connected(image(f))","context":["Intro","Connected","Auto"],"tactic_proof":"Intro; Connected; Auto","source":"nuprl_synthetic/topology"} +{"id":88107,"prover":"Nuprl","theorem":"hausdorff_limit","goal":"all X:TopSpace, s:Nat->X, L1,L2:X. hausdorff(X) => lim(s) = L1 => lim(s) = L2 => L1 = L2","context":["Intro","Hausdorff","Auto"],"tactic_proof":"Intro; Hausdorff; Auto","source":"nuprl_synthetic/topology"} +{"id":88108,"prover":"Nuprl","theorem":"homeomorphism","goal":"all X,Y:TopSpace, f:X->Y. continuous(f) => continuous(inverse(f)) => homeomorphism(f)","context":["Intro","Homeomorphism","Auto"],"tactic_proof":"Intro; Homeomorphism; Auto","source":"nuprl_synthetic/topology"} +{"id":88109,"prover":"Nuprl","theorem":"group_inv_unique","goal":"all G:Group, a,b,c:G. op(a,b) = e => op(a,c) = e => b = c","context":["Intro","Cancel","Auto"],"tactic_proof":"Intro; Cancel; Auto","source":"nuprl_synthetic/algebra"} +{"id":88110,"prover":"Nuprl","theorem":"subgroup_closed","goal":"all G:Group, H:Subgroup(G), a,b:H. op(a, b) in H","context":["Intro","SubgroupAxiom","Auto"],"tactic_proof":"Intro; SubgroupAxiom; Auto","source":"nuprl_synthetic/algebra"} +{"id":88111,"prover":"Nuprl","theorem":"lagrange","goal":"all G:FinGroup, H:Subgroup(G). divides(order(H), order(G))","context":["Intro","Lagrange","Auto"],"tactic_proof":"Intro; Lagrange; Auto","source":"nuprl_synthetic/algebra"} +{"id":88112,"prover":"Nuprl","theorem":"homomorphism_kernel","goal":"all G,H:Group, f:Homomorphism(G, H). subgroup(kernel(f), G)","context":["Intro","KernelAxiom","Auto"],"tactic_proof":"Intro; KernelAxiom; Auto","source":"nuprl_synthetic/algebra"} +{"id":88113,"prover":"Nuprl","theorem":"ring_add_group","goal":"all R:Ring. group(R, +)","context":["Intro","RingAxiom","Auto"],"tactic_proof":"Intro; RingAxiom; Auto","source":"nuprl_synthetic/algebra"} +{"id":88114,"prover":"Nuprl","theorem":"ideal_closed","goal":"all R:Ring, I:Ideal(R), a:R, b:I. op(a, b) in I","context":["Intro","IdealAxiom","Auto"],"tactic_proof":"Intro; IdealAxiom; Auto","source":"nuprl_synthetic/algebra"} +{"id":88115,"prover":"Nuprl","theorem":"field_no_zero_div","goal":"all F:Field, a,b:F. a*b = 0 => a = 0 or b = 0","context":["Intro","FieldAxiom","Auto"],"tactic_proof":"Intro; FieldAxiom; Auto","source":"nuprl_synthetic/algebra"} +{"id":88116,"prover":"Nuprl","theorem":"vector_space_sum","goal":"all V:VectorSpace, v,w:V. v + w = w + v","context":["Intro","VectorAxiom","Auto"],"tactic_proof":"Intro; VectorAxiom; Auto","source":"nuprl_synthetic/algebra"} +{"id":88117,"prover":"Nuprl","theorem":"prob_nonneg","goal":"all P:ProbMeasure, A:Event. P(A) >= 0","context":["Intro","ProbAxiom","Auto"],"tactic_proof":"Intro; ProbAxiom; Auto","source":"nuprl_synthetic/probability"} +{"id":88118,"prover":"Nuprl","theorem":"prob_total","goal":"all P:ProbMeasure. P(universe) = 1","context":["Intro","ProbAxiom","Auto"],"tactic_proof":"Intro; ProbAxiom; Auto","source":"nuprl_synthetic/probability"} +{"id":88119,"prover":"Nuprl","theorem":"prob_additivity","goal":"all P:ProbMeasure, A,B:Event. disjoint(A, B) => P(union(A, B)) = P(A) + P(B)","context":["Intro","Additivity","Auto"],"tactic_proof":"Intro; Additivity; Auto","source":"nuprl_synthetic/probability"} +{"id":88120,"prover":"Nuprl","theorem":"bayes_rule","goal":"all P:ProbMeasure, A,B:Event. P(B) > 0 => P(A | B) = P(A & B) / P(B)","context":["Intro","BayesDef","Auto"],"tactic_proof":"Intro; BayesDef; Auto","source":"nuprl_synthetic/probability"} +{"id":88121,"prover":"Nuprl","theorem":"conditional_indep","goal":"all P:ProbMeasure, A,B,C:Event. indep(A, B | C) <=> P(A & B | C) = P(A | C) * P(B | C)","context":["Intro","Split","Auto"],"tactic_proof":"Intro; Split; Auto","source":"nuprl_synthetic/probability"} +{"id":88122,"prover":"Nuprl","theorem":"markov_ineq","goal":"all X:RandomVar, a:PosReal. P(X >= a) <= E(X) / a","context":["Intro","Markov","Auto"],"tactic_proof":"Intro; Markov; Auto","source":"nuprl_synthetic/probability"} +{"id":88123,"prover":"Nuprl","theorem":"expectation_linear","goal":"all X,Y:RandomVar, a,b:Real. E(a*X + b*Y) = a*E(X) + b*E(Y)","context":["Intro","Linearity","Auto"],"tactic_proof":"Intro; Linearity; Auto","source":"nuprl_synthetic/probability"} +{"id":88124,"prover":"Nuprl","theorem":"variance_nonneg","goal":"all X:RandomVar. var(X) >= 0","context":["Intro","Variance","Auto"],"tactic_proof":"Intro; Variance; Auto","source":"nuprl_synthetic/probability"} +{"id":88125,"prover":"Nuprl","theorem":"bishop_real_approx","goal":"all x:Real, n:PosInt. exists q:Rational. abs(x - q) < 1/n","context":["Intro","ConstructReal","Auto"],"tactic_proof":"Intro; ConstructReal; Auto","source":"nuprl_synthetic/bishop_analysis"} +{"id":88126,"prover":"Nuprl","theorem":"bishop_seq_modulus","goal":"all s:Nat->Real, eps:PosReal. cauchy(s) => exists M:Nat. all m,n:Nat. m >= M => n >= M => abs(s(m) - s(n)) < eps","context":["Intro","ModulusCauchy","Auto"],"tactic_proof":"Intro; Intro; ModulusCauchy; Auto","source":"nuprl_synthetic/bishop_analysis"} +{"id":88127,"prover":"Nuprl","theorem":"bishop_cont_uniform","goal":"all f:Real->Real, K:CompactInterval. continuous(f) => uniformly_continuous_on(f, K)","context":["Intro","HeineCantor","Auto"],"tactic_proof":"Intro; Intro; HeineCantor; Auto","source":"nuprl_synthetic/bishop_analysis"} +{"id":88128,"prover":"Nuprl","theorem":"bishop_rational_dense","goal":"all a,b:Real. a < b => exists q:Rational. a < q < b","context":["Intro","RationalDensity","Auto"],"tactic_proof":"Intro; RationalDensity; Auto","source":"nuprl_synthetic/bishop_analysis"} +{"id":88129,"prover":"Nuprl","theorem":"bishop_sqrt_exists","goal":"all x:NonNegReal. exists y:NonNegReal. y*y = x","context":["Intro","Newton","Auto"],"tactic_proof":"Intro; Newton; Auto","source":"nuprl_synthetic/bishop_analysis"} +{"id":88130,"prover":"Nuprl","theorem":"cut_elim_nuprl","goal":"all A,B. |- A -> (A |- B) -> |- B","context":["Intros","CutAdmissible","Auto"],"tactic_proof":"Intros; CutAdmissible; Auto","source":"nuprl_synthetic/proof_theory"} +{"id":88131,"prover":"Nuprl","theorem":"proof_identity","goal":"all A:Prop. |- A -> A","context":["Intro","Axiom","Auto"],"tactic_proof":"Intro; Axiom; Auto","source":"nuprl_synthetic/proof_theory"} +{"id":88132,"prover":"Nuprl","theorem":"proof_weakening","goal":"all A,B:Prop. |- B => (A |- B)","context":["Intros","Weakening","Auto"],"tactic_proof":"Intros; Weakening; Auto","source":"nuprl_synthetic/proof_theory"} +{"id":88133,"prover":"Nuprl","theorem":"subtype_refl","goal":"all T:Type. T subtype T","context":["Intro","SubtypeRefl","Auto"],"tactic_proof":"Intro; SubtypeRefl; Auto","source":"nuprl_synthetic/proof_theory"} +{"id":88134,"prover":"Nuprl","theorem":"subtype_trans","goal":"all T1,T2,T3:Type. T1 subtype T2 => T2 subtype T3 => T1 subtype T3","context":["Intros","SubtypeTrans","Auto"],"tactic_proof":"Intros; SubtypeTrans; Auto","source":"nuprl_synthetic/proof_theory"} +{"id":88135,"prover":"Nuprl","theorem":"equality_symmetry","goal":"all A:Type, x,y:A. x = y => y = x","context":["Intros","EqSym","Auto"],"tactic_proof":"Intros; EqSym; Auto","source":"nuprl_synthetic/proof_theory"} +{"id":88136,"prover":"Nuprl","theorem":"equality_trans","goal":"all A:Type, x,y,z:A. x = y => y = z => x = z","context":["Intros","EqTrans","Auto"],"tactic_proof":"Intros; EqTrans; Auto","source":"nuprl_synthetic/proof_theory"} +{"id":88137,"prover":"Nuprl","theorem":"entropy_nonneg","goal":"all P:ProbDist. entropy(P) >= 0","context":["Intro","EntropyDef","Auto"],"tactic_proof":"Intro; EntropyDef; Auto","source":"nuprl_synthetic/information"} +{"id":88138,"prover":"Nuprl","theorem":"entropy_uniform_max","goal":"all n:PosNat, P:ProbDist(Fin(n)). entropy(P) <= log(n)","context":["Intro","MaxEntropy","Auto"],"tactic_proof":"Intro; Intro; MaxEntropy; Auto","source":"nuprl_synthetic/information"} +{"id":88139,"prover":"Nuprl","theorem":"mutual_info_nonneg","goal":"all X,Y:RandomVar. I(X; Y) >= 0","context":["Intro","MIDef","Auto"],"tactic_proof":"Intro; MIDef; Auto","source":"nuprl_synthetic/information"} +{"id":88140,"prover":"Nuprl","theorem":"chain_rule_entropy","goal":"all X,Y:RandomVar. H(X, Y) = H(X) + H(Y | X)","context":["Intro","ChainRule","Auto"],"tactic_proof":"Intro; ChainRule; Auto","source":"nuprl_synthetic/information"} +{"id":88141,"prover":"Nuprl","theorem":"kraft_inequality","goal":"all C:PrefixCode. sum(c in C, 2^(-length(c))) <= 1","context":["Intro","Kraft","Auto"],"tactic_proof":"Intro; Kraft; Auto","source":"nuprl_synthetic/information"} +{"id":88142,"prover":"Nuprl","theorem":"source_coding","goal":"all X:RandomVar, eps:PosReal. exists n:PosNat, C:Code. expected_length(C(X^n)) / n <= H(X) + eps","context":["Intro","ShannonSource","Auto"],"tactic_proof":"Intro; ShannonSource; Auto","source":"nuprl_synthetic/information"} +{"id":88143,"prover":"Nuprl","theorem":"quotient_class","goal":"all A:Type, R:Equiv(A), x,y:A. R(x,y) => [x]_R = [y]_R","context":["Intros","QuotientEq","Auto"],"tactic_proof":"Intros; QuotientEq; Auto","source":"nuprl_synthetic/quotient_types"} +{"id":88144,"prover":"Nuprl","theorem":"quotient_lift","goal":"all A,B:Type, R:Equiv(A), f:A->B. (all x,y:A. R(x,y) => f(x) = f(y)) => A/R -> B","context":["Intros","QuotientLift","Auto"],"tactic_proof":"Intros; QuotientLift; Auto","source":"nuprl_synthetic/quotient_types"} +{"id":88145,"prover":"Nuprl","theorem":"nat_quot_modp","goal":"all p:PosNat. Nat/cong(p) ~ Fin(p)","context":["Intro","Bijection","Auto"],"tactic_proof":"Intro; Bijection; Auto","source":"nuprl_synthetic/quotient_types"} +{"id":88146,"prover":"Nuprl","theorem":"partition_quotient","goal":"all A:Type, R:Equiv(A). partition(A, R) <=> A/R","context":["Intro","Partition","Auto"],"tactic_proof":"Intro; Partition; Auto","source":"nuprl_synthetic/quotient_types"} +{"id":88147,"prover":"Nuprl","theorem":"setoid_morphism","goal":"all A,B:Setoid, f:A->B. morphism(f) <=> (all x,y:A. eq_A(x,y) => eq_B(f(x), f(y)))","context":["Intro","Morphism","Auto"],"tactic_proof":"Intro; Morphism; Auto","source":"nuprl_synthetic/quotient_types"} +{"id":88148,"prover":"Nuprl","theorem":"w_type","goal":"all A:Type, B:A->Type. W(A, B) : Type","context":["Intros","WType","Auto"],"tactic_proof":"Intros; WType; Auto","source":"nuprl_synthetic/w_types"} +{"id":88149,"prover":"Nuprl","theorem":"w_induction","goal":"all A:Type, B:A->Type, P:W(A,B)->Prop. (all a:A, f:B(a)->W(A,B). (all b:B(a). P(f(b))) => P(sup(a, f))) => all w:W(A,B). P(w)","context":["Intros","WInduction","Auto"],"tactic_proof":"Intros; WInduction; Auto","source":"nuprl_synthetic/w_types"} +{"id":88150,"prover":"Nuprl","theorem":"w_nat_iso","goal":"Nat ~ W(Bool, lambda b. if b then Unit else Empty)","context":["Intro","Bijection","Auto"],"tactic_proof":"Intro; Bijection; Auto","source":"nuprl_synthetic/w_types"} +{"id":88151,"prover":"Nuprl","theorem":"w_list_iso","goal":"all A:Type. List(A) ~ W(1 + A, lambda s. match s with inl _ => Empty | inr _ => Unit)","context":["Intro","Bijection","Auto"],"tactic_proof":"Intro; Bijection; Auto","source":"nuprl_synthetic/w_types"} diff --git a/training_data/proof_states_twelf.jsonl b/training_data/proof_states_twelf.jsonl index b5b6511a..5753c852 100644 --- a/training_data/proof_states_twelf.jsonl +++ b/training_data/proof_states_twelf.jsonl @@ -1,33 +1,118 @@ -{"id": 89000, "prover": "Twelf", "theorem": "nat", "goal": "nat : type.", "context": ["nat"], "tactic_proof": "z : nat.\ns : nat -> nat.", "source": "twelf_synthetic/natural_numbers"} -{"id": 89001, "prover": "Twelf", "theorem": "plus", "goal": "plus : nat -> nat -> nat -> type.", "context": ["plus"], "tactic_proof": "plus-z : plus z N N.\nplus-s : plus (s M) N (s P) <- plus M N P.", "source": "twelf_synthetic/natural_numbers"} -{"id": 89002, "prover": "Twelf", "theorem": "plus_comm", "goal": "plus-comm : plus M N P -> plus N M P -> type.", "context": ["plus-comm"], "tactic_proof": "plus-comm-z : plus-comm plus-z D <- plus-zero-right D.\nplus-comm-s : plus-comm (plus-s D1) D2 <- plus-comm D1 D3 <- plus-succ-right D3 D2.", "source": "twelf_synthetic/natural_numbers"} -{"id": 89003, "prover": "Twelf", "theorem": "plus_assoc", "goal": "plus-assoc : plus A B AB -> plus AB C ABC -> plus B C BC -> plus A BC ABC -> type.", "context": ["plus-assoc"], "tactic_proof": "%mode plus-assoc +D1 +D2 -D3 -D4.", "source": "twelf_synthetic/natural_numbers"} -{"id": 89004, "prover": "Twelf", "theorem": "times", "goal": "times : nat -> nat -> nat -> type.", "context": ["times"], "tactic_proof": "times-z : times z N z.\ntimes-s : times (s M) N P <- times M N Q <- plus N Q P.", "source": "twelf_synthetic/natural_numbers"} -{"id": 89005, "prover": "Twelf", "theorem": "leq", "goal": "leq : nat -> nat -> type.", "context": ["leq"], "tactic_proof": "leq-z : leq z N.\nleq-s : leq (s M) (s N) <- leq M N.", "source": "twelf_synthetic/natural_numbers"} -{"id": 89006, "prover": "Twelf", "theorem": "leq_refl", "goal": "leq-refl : {N:nat} leq N N -> type.", "context": ["leq-refl", "N"], "tactic_proof": "leq-refl-z : leq-refl z leq-z.\nleq-refl-s : leq-refl (s N) (leq-s D) <- leq-refl N D.", "source": "twelf_synthetic/natural_numbers"} -{"id": 89007, "prover": "Twelf", "theorem": "leq_trans", "goal": "leq-trans : leq A B -> leq B C -> leq A C -> type.", "context": ["leq-trans"], "tactic_proof": "%mode leq-trans +D1 +D2 -D3.", "source": "twelf_synthetic/natural_numbers"} -{"id": 89008, "prover": "Twelf", "theorem": "max", "goal": "max : nat -> nat -> nat -> type.", "context": ["max"], "tactic_proof": "max-zl : max z N N.\nmax-zr : max N z N.\nmax-ss : max (s M) (s N) (s P) <- max M N P.", "source": "twelf_synthetic/natural_numbers"} -{"id": 89009, "prover": "Twelf", "theorem": "even_odd", "goal": "even : nat -> type.\nodd : nat -> type.", "context": ["even", "odd"], "tactic_proof": "even-z : even z.\neven-s : even (s N) <- odd N.\nodd-s : odd (s N) <- even N.", "source": "twelf_synthetic/natural_numbers"} -{"id": 89010, "prover": "Twelf", "theorem": "tp", "goal": "tp : type.", "context": ["tp"], "tactic_proof": "arr : tp -> tp -> tp.\nunit : tp.", "source": "twelf_synthetic/lambda_calculus"} -{"id": 89011, "prover": "Twelf", "theorem": "tm", "goal": "tm : type.", "context": ["tm"], "tactic_proof": "app : tm -> tm -> tm.\nlam : tp -> (tm -> tm) -> tm.\nempty : tm.", "source": "twelf_synthetic/lambda_calculus"} -{"id": 89012, "prover": "Twelf", "theorem": "of", "goal": "of : tm -> tp -> type.", "context": ["of"], "tactic_proof": "of-app : of (app E1 E2) T <- of E1 (arr T2 T) <- of E2 T2.\nof-lam : of (lam T1 E) (arr T1 T2) <- ({x:tm} of x T1 -> of (E x) T2).\nof-empty : of empty unit.", "source": "twelf_synthetic/lambda_calculus"} -{"id": 89013, "prover": "Twelf", "theorem": "value", "goal": "value : tm -> type.", "context": ["value"], "tactic_proof": "value-lam : value (lam T E).\nvalue-empty : value empty.", "source": "twelf_synthetic/lambda_calculus"} -{"id": 89014, "prover": "Twelf", "theorem": "step", "goal": "step : tm -> tm -> type.", "context": ["step"], "tactic_proof": "step-app1 : step (app E1 E2) (app E1' E2) <- step E1 E1'.\nstep-app2 : step (app V E2) (app V E2') <- value V <- step E2 E2'.\nstep-beta : step (app (lam T E) V) (E V) <- value V.", "source": "twelf_synthetic/lambda_calculus"} -{"id": 89015, "prover": "Twelf", "theorem": "preservation", "goal": "preservation : of E T -> step E E' -> of E' T -> type.", "context": ["preservation"], "tactic_proof": "%mode preservation +Dof +Dstep -Dof'.\npreservation-app1 : preservation (of-app D1 D2) (step-app1 S) (of-app D1' D2) <- preservation D1 S D1'.\npreservation-beta : preservation (of-app (of-lam D1) D2) (step-beta V) (D1 _ D2).", "source": "twelf_synthetic/lambda_calculus"} -{"id": 89016, "prover": "Twelf", "theorem": "progress", "goal": "progress : of E T -> (value E + step E E') -> type.", "context": ["progress"], "tactic_proof": "%mode progress +Dof -Dresult.", "source": "twelf_synthetic/lambda_calculus"} -{"id": 89017, "prover": "Twelf", "theorem": "subst", "goal": "subst : (tm -> tm) -> tm -> tm -> type.", "context": ["subst"], "tactic_proof": "subst-var : subst ([x] x) V V.\nsubst-const : subst ([x] C) V C.\nsubst-app : subst ([x] app (E1 x) (E2 x)) V (app E1' E2') <- subst E1 V E1' <- subst E2 V E2'.\nsubst-lam : subst ([x] lam T ([y] E x y)) V (lam T E') <- ({y:tm} subst ([x] E x y) V (E' y)).", "source": "twelf_synthetic/lambda_calculus"} -{"id": 89018, "prover": "Twelf", "theorem": "list", "goal": "list : type.", "context": ["list"], "tactic_proof": "nil : list.\ncons : nat -> list -> list.", "source": "twelf_synthetic/lists"} -{"id": 89019, "prover": "Twelf", "theorem": "append", "goal": "append : list -> list -> list -> type.", "context": ["append"], "tactic_proof": "append-nil : append nil L L.\nappend-cons : append (cons H T) L (cons H R) <- append T L R.", "source": "twelf_synthetic/lists"} -{"id": 89020, "prover": "Twelf", "theorem": "append_assoc", "goal": "append-assoc : append L1 L2 L12 -> append L12 L3 L123 -> append L2 L3 L23 -> append L1 L23 L123 -> type.", "context": ["append-assoc"], "tactic_proof": "%mode append-assoc +D1 +D2 -D3 -D4.", "source": "twelf_synthetic/lists"} -{"id": 89021, "prover": "Twelf", "theorem": "reverse", "goal": "reverse : list -> list -> type.", "context": ["reverse"], "tactic_proof": "reverse-nil : reverse nil nil.\nreverse-cons : reverse (cons H T) R <- reverse T T' <- append T' (cons H nil) R.", "source": "twelf_synthetic/lists"} -{"id": 89022, "prover": "Twelf", "theorem": "length", "goal": "length : list -> nat -> type.", "context": ["length"], "tactic_proof": "length-nil : length nil z.\nlength-cons : length (cons H T) (s N) <- length T N.", "source": "twelf_synthetic/lists"} -{"id": 89023, "prover": "Twelf", "theorem": "member", "goal": "member : nat -> list -> type.", "context": ["member"], "tactic_proof": "member-head : member X (cons X L).\nmember-tail : member X (cons Y L) <- member X L.", "source": "twelf_synthetic/lists"} -{"id": 89024, "prover": "Twelf", "theorem": "sorted", "goal": "sorted : list -> type.", "context": ["sorted"], "tactic_proof": "sorted-nil : sorted nil.\nsorted-one : sorted (cons X nil).\nsorted-cons : sorted (cons X (cons Y L)) <- leq X Y <- sorted (cons Y L).", "source": "twelf_synthetic/lists"} -{"id": 89025, "prover": "Twelf", "theorem": "insert_sorted", "goal": "insert : nat -> list -> list -> type.", "context": ["insert"], "tactic_proof": "insert-nil : insert X nil (cons X nil).\ninsert-leq : insert X (cons Y L) (cons X (cons Y L)) <- leq X Y.\ninsert-gt : insert X (cons Y L) (cons Y L') <- insert X L L'.", "source": "twelf_synthetic/lists"} -{"id": 89026, "prover": "Twelf", "theorem": "prop", "goal": "o : type.", "context": ["o"], "tactic_proof": "imp : o -> o -> o.\nand : o -> o -> o.\nor : o -> o -> o.\nnot : o -> o.\nforall : (i -> o) -> o.\nexists : (i -> o) -> o.", "source": "twelf_synthetic/logic_framework"} -{"id": 89027, "prover": "Twelf", "theorem": "pf", "goal": "pf : o -> type.", "context": ["pf"], "tactic_proof": "imp-i : ({x:pf A} pf B) -> pf (imp A B).\nimp-e : pf (imp A B) -> pf A -> pf B.\nand-i : pf A -> pf B -> pf (and A B).\nand-e1 : pf (and A B) -> pf A.\nand-e2 : pf (and A B) -> pf B.\nor-i1 : pf A -> pf (or A B).\nor-i2 : pf B -> pf (or A B).\nor-e : pf (or A B) -> ({x:pf A} pf C) -> ({x:pf B} pf C) -> pf C.\nnot-i : ({x:pf A} pf false) -> pf (not A).\nnot-e : pf (not A) -> pf A -> pf false.\nforall-i : ({x:i} pf (A x)) -> pf (forall A).\nforall-e : pf (forall A) -> {T:i} pf (A T).\nexists-i : {T:i} pf (A T) -> pf (exists A).\nexists-e : pf (exists A) -> ({x:i} {y:pf (A x)} pf C) -> pf C.", "source": "twelf_synthetic/logic_framework"} -{"id": 89028, "prover": "Twelf", "theorem": "and_comm_pf", "goal": "and-comm : pf (imp (and A B) (and B A)).", "context": ["and-comm"], "tactic_proof": "and-comm = imp-i ([h:pf (and A B)] and-i (and-e2 h) (and-e1 h)).", "source": "twelf_synthetic/logic_framework"} -{"id": 89029, "prover": "Twelf", "theorem": "or_comm_pf", "goal": "or-comm : pf (imp (or A B) (or B A)).", "context": ["or-comm"], "tactic_proof": "or-comm = imp-i ([h:pf (or A B)] or-e h ([a] or-i2 a) ([b] or-i1 b)).", "source": "twelf_synthetic/logic_framework"} -{"id": 89030, "prover": "Twelf", "theorem": "modus_ponens_pf", "goal": "mp : pf A -> pf (imp A B) -> pf B.", "context": ["mp"], "tactic_proof": "mp = [a:pf A] [f:pf (imp A B)] imp-e f a.", "source": "twelf_synthetic/logic_framework"} -{"id": 89031, "prover": "Twelf", "theorem": "double_neg_intro_pf", "goal": "dn-intro : pf (imp A (not (not A))).", "context": ["dn-intro"], "tactic_proof": "dn-intro = imp-i ([a:pf A] not-i ([h:pf (not A)] not-e h a)).", "source": "twelf_synthetic/logic_framework"} -{"id": 89032, "prover": "Twelf", "theorem": "contra_pf", "goal": "contra : pf (imp (imp A B) (imp (not B) (not A))).", "context": ["contra"], "tactic_proof": "contra = imp-i ([f:pf (imp A B)] imp-i ([nb:pf (not B)] not-i ([a:pf A] not-e nb (imp-e f a)))).", "source": "twelf_synthetic/logic_framework"} +{"id":89000,"prover":"Twelf","theorem":"nat","goal":"nat : type.","context":["nat"],"tactic_proof":"z : nat.\ns : nat -> nat.","source":"twelf_synthetic/natural_numbers"} +{"id":89001,"prover":"Twelf","theorem":"plus","goal":"plus : nat -> nat -> nat -> type.","context":["plus"],"tactic_proof":"plus-z : plus z N N.\nplus-s : plus (s M) N (s P) <- plus M N P.","source":"twelf_synthetic/natural_numbers"} +{"id":89002,"prover":"Twelf","theorem":"plus_comm","goal":"plus-comm : plus M N P -> plus N M P -> type.","context":["plus-comm"],"tactic_proof":"plus-comm-z : plus-comm plus-z D <- plus-zero-right D.\nplus-comm-s : plus-comm (plus-s D1) D2 <- plus-comm D1 D3 <- plus-succ-right D3 D2.","source":"twelf_synthetic/natural_numbers"} +{"id":89003,"prover":"Twelf","theorem":"plus_assoc","goal":"plus-assoc : plus A B AB -> plus AB C ABC -> plus B C BC -> plus A BC ABC -> type.","context":["plus-assoc"],"tactic_proof":"%mode plus-assoc +D1 +D2 -D3 -D4.","source":"twelf_synthetic/natural_numbers"} +{"id":89004,"prover":"Twelf","theorem":"times","goal":"times : nat -> nat -> nat -> type.","context":["times"],"tactic_proof":"times-z : times z N z.\ntimes-s : times (s M) N P <- times M N Q <- plus N Q P.","source":"twelf_synthetic/natural_numbers"} +{"id":89005,"prover":"Twelf","theorem":"leq","goal":"leq : nat -> nat -> type.","context":["leq"],"tactic_proof":"leq-z : leq z N.\nleq-s : leq (s M) (s N) <- leq M N.","source":"twelf_synthetic/natural_numbers"} +{"id":89006,"prover":"Twelf","theorem":"leq_refl","goal":"leq-refl : {N:nat} leq N N -> type.","context":["leq-refl","N"],"tactic_proof":"leq-refl-z : leq-refl z leq-z.\nleq-refl-s : leq-refl (s N) (leq-s D) <- leq-refl N D.","source":"twelf_synthetic/natural_numbers"} +{"id":89007,"prover":"Twelf","theorem":"leq_trans","goal":"leq-trans : leq A B -> leq B C -> leq A C -> type.","context":["leq-trans"],"tactic_proof":"%mode leq-trans +D1 +D2 -D3.","source":"twelf_synthetic/natural_numbers"} +{"id":89008,"prover":"Twelf","theorem":"max","goal":"max : nat -> nat -> nat -> type.","context":["max"],"tactic_proof":"max-zl : max z N N.\nmax-zr : max N z N.\nmax-ss : max (s M) (s N) (s P) <- max M N P.","source":"twelf_synthetic/natural_numbers"} +{"id":89009,"prover":"Twelf","theorem":"even_odd","goal":"even : nat -> type.\nodd : nat -> type.","context":["even","odd"],"tactic_proof":"even-z : even z.\neven-s : even (s N) <- odd N.\nodd-s : odd (s N) <- even N.","source":"twelf_synthetic/natural_numbers"} +{"id":89010,"prover":"Twelf","theorem":"tp","goal":"tp : type.","context":["tp"],"tactic_proof":"arr : tp -> tp -> tp.\nunit : tp.","source":"twelf_synthetic/lambda_calculus"} +{"id":89011,"prover":"Twelf","theorem":"tm","goal":"tm : type.","context":["tm"],"tactic_proof":"app : tm -> tm -> tm.\nlam : tp -> (tm -> tm) -> tm.\nempty : tm.","source":"twelf_synthetic/lambda_calculus"} +{"id":89012,"prover":"Twelf","theorem":"of","goal":"of : tm -> tp -> type.","context":["of"],"tactic_proof":"of-app : of (app E1 E2) T <- of E1 (arr T2 T) <- of E2 T2.\nof-lam : of (lam T1 E) (arr T1 T2) <- ({x:tm} of x T1 -> of (E x) T2).\nof-empty : of empty unit.","source":"twelf_synthetic/lambda_calculus"} +{"id":89013,"prover":"Twelf","theorem":"value","goal":"value : tm -> type.","context":["value"],"tactic_proof":"value-lam : value (lam T E).\nvalue-empty : value empty.","source":"twelf_synthetic/lambda_calculus"} +{"id":89014,"prover":"Twelf","theorem":"step","goal":"step : tm -> tm -> type.","context":["step"],"tactic_proof":"step-app1 : step (app E1 E2) (app E1' E2) <- step E1 E1'.\nstep-app2 : step (app V E2) (app V E2') <- value V <- step E2 E2'.\nstep-beta : step (app (lam T E) V) (E V) <- value V.","source":"twelf_synthetic/lambda_calculus"} +{"id":89015,"prover":"Twelf","theorem":"preservation","goal":"preservation : of E T -> step E E' -> of E' T -> type.","context":["preservation"],"tactic_proof":"%mode preservation +Dof +Dstep -Dof'.\npreservation-app1 : preservation (of-app D1 D2) (step-app1 S) (of-app D1' D2) <- preservation D1 S D1'.\npreservation-beta : preservation (of-app (of-lam D1) D2) (step-beta V) (D1 _ D2).","source":"twelf_synthetic/lambda_calculus"} +{"id":89016,"prover":"Twelf","theorem":"progress","goal":"progress : of E T -> (value E + step E E') -> type.","context":["progress"],"tactic_proof":"%mode progress +Dof -Dresult.","source":"twelf_synthetic/lambda_calculus"} +{"id":89017,"prover":"Twelf","theorem":"subst","goal":"subst : (tm -> tm) -> tm -> tm -> type.","context":["subst"],"tactic_proof":"subst-var : subst ([x] x) V V.\nsubst-const : subst ([x] C) V C.\nsubst-app : subst ([x] app (E1 x) (E2 x)) V (app E1' E2') <- subst E1 V E1' <- subst E2 V E2'.\nsubst-lam : subst ([x] lam T ([y] E x y)) V (lam T E') <- ({y:tm} subst ([x] E x y) V (E' y)).","source":"twelf_synthetic/lambda_calculus"} +{"id":89018,"prover":"Twelf","theorem":"list","goal":"list : type.","context":["list"],"tactic_proof":"nil : list.\ncons : nat -> list -> list.","source":"twelf_synthetic/lists"} +{"id":89019,"prover":"Twelf","theorem":"append","goal":"append : list -> list -> list -> type.","context":["append"],"tactic_proof":"append-nil : append nil L L.\nappend-cons : append (cons H T) L (cons H R) <- append T L R.","source":"twelf_synthetic/lists"} +{"id":89020,"prover":"Twelf","theorem":"append_assoc","goal":"append-assoc : append L1 L2 L12 -> append L12 L3 L123 -> append L2 L3 L23 -> append L1 L23 L123 -> type.","context":["append-assoc"],"tactic_proof":"%mode append-assoc +D1 +D2 -D3 -D4.","source":"twelf_synthetic/lists"} +{"id":89021,"prover":"Twelf","theorem":"reverse","goal":"reverse : list -> list -> type.","context":["reverse"],"tactic_proof":"reverse-nil : reverse nil nil.\nreverse-cons : reverse (cons H T) R <- reverse T T' <- append T' (cons H nil) R.","source":"twelf_synthetic/lists"} +{"id":89022,"prover":"Twelf","theorem":"length","goal":"length : list -> nat -> type.","context":["length"],"tactic_proof":"length-nil : length nil z.\nlength-cons : length (cons H T) (s N) <- length T N.","source":"twelf_synthetic/lists"} +{"id":89023,"prover":"Twelf","theorem":"member","goal":"member : nat -> list -> type.","context":["member"],"tactic_proof":"member-head : member X (cons X L).\nmember-tail : member X (cons Y L) <- member X L.","source":"twelf_synthetic/lists"} +{"id":89024,"prover":"Twelf","theorem":"sorted","goal":"sorted : list -> type.","context":["sorted"],"tactic_proof":"sorted-nil : sorted nil.\nsorted-one : sorted (cons X nil).\nsorted-cons : sorted (cons X (cons Y L)) <- leq X Y <- sorted (cons Y L).","source":"twelf_synthetic/lists"} +{"id":89025,"prover":"Twelf","theorem":"insert_sorted","goal":"insert : nat -> list -> list -> type.","context":["insert"],"tactic_proof":"insert-nil : insert X nil (cons X nil).\ninsert-leq : insert X (cons Y L) (cons X (cons Y L)) <- leq X Y.\ninsert-gt : insert X (cons Y L) (cons Y L') <- insert X L L'.","source":"twelf_synthetic/lists"} +{"id":89026,"prover":"Twelf","theorem":"prop","goal":"o : type.","context":["o"],"tactic_proof":"imp : o -> o -> o.\nand : o -> o -> o.\nor : o -> o -> o.\nnot : o -> o.\nforall : (i -> o) -> o.\nexists : (i -> o) -> o.","source":"twelf_synthetic/logic_framework"} +{"id":89027,"prover":"Twelf","theorem":"pf","goal":"pf : o -> type.","context":["pf"],"tactic_proof":"imp-i : ({x:pf A} pf B) -> pf (imp A B).\nimp-e : pf (imp A B) -> pf A -> pf B.\nand-i : pf A -> pf B -> pf (and A B).\nand-e1 : pf (and A B) -> pf A.\nand-e2 : pf (and A B) -> pf B.\nor-i1 : pf A -> pf (or A B).\nor-i2 : pf B -> pf (or A B).\nor-e : pf (or A B) -> ({x:pf A} pf C) -> ({x:pf B} pf C) -> pf C.\nnot-i : ({x:pf A} pf false) -> pf (not A).\nnot-e : pf (not A) -> pf A -> pf false.\nforall-i : ({x:i} pf (A x)) -> pf (forall A).\nforall-e : pf (forall A) -> {T:i} pf (A T).\nexists-i : {T:i} pf (A T) -> pf (exists A).\nexists-e : pf (exists A) -> ({x:i} {y:pf (A x)} pf C) -> pf C.","source":"twelf_synthetic/logic_framework"} +{"id":89028,"prover":"Twelf","theorem":"and_comm_pf","goal":"and-comm : pf (imp (and A B) (and B A)).","context":["and-comm"],"tactic_proof":"and-comm = imp-i ([h:pf (and A B)] and-i (and-e2 h) (and-e1 h)).","source":"twelf_synthetic/logic_framework"} +{"id":89029,"prover":"Twelf","theorem":"or_comm_pf","goal":"or-comm : pf (imp (or A B) (or B A)).","context":["or-comm"],"tactic_proof":"or-comm = imp-i ([h:pf (or A B)] or-e h ([a] or-i2 a) ([b] or-i1 b)).","source":"twelf_synthetic/logic_framework"} +{"id":89030,"prover":"Twelf","theorem":"modus_ponens_pf","goal":"mp : pf A -> pf (imp A B) -> pf B.","context":["mp"],"tactic_proof":"mp = [a:pf A] [f:pf (imp A B)] imp-e f a.","source":"twelf_synthetic/logic_framework"} +{"id":89031,"prover":"Twelf","theorem":"double_neg_intro_pf","goal":"dn-intro : pf (imp A (not (not A))).","context":["dn-intro"],"tactic_proof":"dn-intro = imp-i ([a:pf A] not-i ([h:pf (not A)] not-e h a)).","source":"twelf_synthetic/logic_framework"} +{"id":89032,"prover":"Twelf","theorem":"contra_pf","goal":"contra : pf (imp (imp A B) (imp (not B) (not A))).","context":["contra"],"tactic_proof":"contra = imp-i ([f:pf (imp A B)] imp-i ([nb:pf (not B)] not-i ([a:pf A] not-e nb (imp-e f a)))).","source":"twelf_synthetic/logic_framework"} +{"id":89033,"prover":"Twelf","theorem":"tree","goal":"tree : type.","context":["tree"],"tactic_proof":"empty : tree.\nnode : nat -> tree -> tree -> tree.","source":"twelf_synthetic/binary_trees"} +{"id":89034,"prover":"Twelf","theorem":"insert_bst","goal":"insert : nat -> tree -> tree -> type.","context":["insert"],"tactic_proof":"insert-empty : insert X empty (node X empty empty).\ninsert-lt : insert X (node Y L R) (node Y L' R) <- leq X Y <- insert X L L'.\ninsert-gt : insert X (node Y L R) (node Y L R') <- leq Y X <- insert X R R'.","source":"twelf_synthetic/binary_trees"} +{"id":89035,"prover":"Twelf","theorem":"tree_size","goal":"tree-size : tree -> nat -> type.","context":["tree-size"],"tactic_proof":"tree-size-empty : tree-size empty z.\ntree-size-node : tree-size (node X L R) (s N) <- tree-size L NL <- tree-size R NR <- plus NL NR N.","source":"twelf_synthetic/binary_trees"} +{"id":89036,"prover":"Twelf","theorem":"tree_height","goal":"tree-height : tree -> nat -> type.","context":["tree-height"],"tactic_proof":"tree-height-empty : tree-height empty z.\ntree-height-node : tree-height (node X L R) (s H) <- tree-height L HL <- tree-height R HR <- max HL HR H.","source":"twelf_synthetic/binary_trees"} +{"id":89037,"prover":"Twelf","theorem":"tree_member","goal":"tree-member : nat -> tree -> type.","context":["tree-member"],"tactic_proof":"tree-member-node : tree-member X (node X L R).\ntree-member-left : tree-member X (node Y L R) <- tree-member X L.\ntree-member-right : tree-member X (node Y L R) <- tree-member X R.","source":"twelf_synthetic/binary_trees"} +{"id":89038,"prover":"Twelf","theorem":"tree_mirror","goal":"mirror : tree -> tree -> type.","context":["mirror"],"tactic_proof":"mirror-empty : mirror empty empty.\nmirror-node : mirror (node X L R) (node X R' L') <- mirror L L' <- mirror R R'.","source":"twelf_synthetic/binary_trees"} +{"id":89039,"prover":"Twelf","theorem":"mirror_involutive","goal":"mirror-involutive : mirror T T' -> mirror T' T -> type.","context":["mirror-involutive"],"tactic_proof":"%mode mirror-involutive +D1 -D2.","source":"twelf_synthetic/binary_trees"} +{"id":89040,"prover":"Twelf","theorem":"inorder_flatten","goal":"inorder : tree -> list -> type.","context":["inorder"],"tactic_proof":"inorder-empty : inorder empty nil.\ninorder-node : inorder (node X L R) M <- inorder L ML <- inorder R MR <- append ML (cons X MR) M.","source":"twelf_synthetic/binary_trees"} +{"id":89041,"prover":"Twelf","theorem":"substitution","goal":"subst' : (tm -> tm) -> tm -> tm -> type.","context":[],"tactic_proof":"subst'-id : subst' ([x] x) V V.\nsubst'-const : subst' ([x] C) V C.","source":"twelf_synthetic/substitution"} +{"id":89042,"prover":"Twelf","theorem":"capture_avoid","goal":"fresh : tm -> (tm -> tm) -> type.","context":["fresh"],"tactic_proof":"fresh-const : fresh V ([x] C).\nfresh-app : fresh V ([x] app (E1 x) (E2 x)) <- fresh V E1 <- fresh V E2.","source":"twelf_synthetic/substitution"} +{"id":89043,"prover":"Twelf","theorem":"alpha_eq","goal":"alpha-eq : tm -> tm -> type.","context":["alpha-eq"],"tactic_proof":"alpha-eq-refl : alpha-eq E E.\nalpha-eq-lam : alpha-eq (lam T ([x] E x)) (lam T ([y] E y)) <- ({x} alpha-eq (E x) (E x)).","source":"twelf_synthetic/substitution"} +{"id":89044,"prover":"Twelf","theorem":"beta_red","goal":"beta-red : tm -> tm -> type.","context":["beta-red"],"tactic_proof":"beta-red-step : beta-red (app (lam T E) V) (E V) <- value V.","source":"twelf_synthetic/substitution"} +{"id":89045,"prover":"Twelf","theorem":"eta_red","goal":"eta-red : tm -> tm -> type.","context":["eta-red"],"tactic_proof":"eta-red-step : eta-red (lam T ([x] app E x)) E.","source":"twelf_synthetic/substitution"} +{"id":89046,"prover":"Twelf","theorem":"subst_lemma","goal":"subst-lemma : subst' E1 V1 E1' -> subst' E2 V2 E2' -> subst' ([x] E1 x) V1 E1'' -> type.","context":["subst-lemma"],"tactic_proof":"%mode subst-lemma +D1 +D2 +D3.","source":"twelf_synthetic/substitution"} +{"id":89047,"prover":"Twelf","theorem":"channel","goal":"chan : type.","context":["chan"],"tactic_proof":"new-chan : chan.","source":"twelf_synthetic/session_types"} +{"id":89048,"prover":"Twelf","theorem":"msg_type","goal":"msg : type.","context":["msg"],"tactic_proof":"unit-msg : msg.\nsum-msg : msg -> msg -> msg.","source":"twelf_synthetic/session_types"} +{"id":89049,"prover":"Twelf","theorem":"protocol","goal":"proto : type.","context":["proto"],"tactic_proof":"send-proto : msg -> proto -> proto.\nrecv-proto : msg -> proto -> proto.\nend-proto : proto.","source":"twelf_synthetic/session_types"} +{"id":89050,"prover":"Twelf","theorem":"duality","goal":"dual : proto -> proto -> type.","context":["dual"],"tactic_proof":"dual-end : dual end-proto end-proto.\ndual-send : dual (send-proto M P) (recv-proto M Q) <- dual P Q.\ndual-recv : dual (recv-proto M P) (send-proto M Q) <- dual P Q.","source":"twelf_synthetic/session_types"} +{"id":89051,"prover":"Twelf","theorem":"session_safe","goal":"session-safe : chan -> proto -> type.","context":["session-safe"],"tactic_proof":"%mode session-safe +C +P.","source":"twelf_synthetic/session_types"} +{"id":89052,"prover":"Twelf","theorem":"linear_use","goal":"linear : chan -> type.","context":["linear"],"tactic_proof":"linear-new : linear C <- new-chan.","source":"twelf_synthetic/session_types"} +{"id":89053,"prover":"Twelf","theorem":"linear_type","goal":"ltp : type.","context":["ltp"],"tactic_proof":"lolli : ltp -> ltp -> ltp.\ntensor : ltp -> ltp -> ltp.\nwith-type : ltp -> ltp -> ltp.\none-type : ltp.","source":"twelf_synthetic/linear_lf"} +{"id":89054,"prover":"Twelf","theorem":"linear_tm","goal":"ltm : type.","context":["ltm"],"tactic_proof":"lapp : ltm -> ltm -> ltm.\nllam : ltp -> (ltm -> ltm) -> ltm.\npair-ltm : ltm -> ltm -> ltm.\nunit-ltm : ltm.","source":"twelf_synthetic/linear_lf"} +{"id":89055,"prover":"Twelf","theorem":"linear_of","goal":"lof : ltm -> ltp -> type.","context":["lof"],"tactic_proof":"lof-lam : lof (llam T1 E) (lolli T1 T2) <- ({x:ltm} lof x T1 -> lof (E x) T2).\nlof-pair : lof (pair-ltm E1 E2) (tensor T1 T2) <- lof E1 T1 <- lof E2 T2.\nlof-unit : lof unit-ltm one-type.","source":"twelf_synthetic/linear_lf"} +{"id":89056,"prover":"Twelf","theorem":"linear_safety","goal":"linear-safety : lof E T -> step E E' -> lof E' T -> type.","context":["linear-safety"],"tactic_proof":"%mode linear-safety +D1 +D2 -D3.","source":"twelf_synthetic/linear_lf"} +{"id":89057,"prover":"Twelf","theorem":"linear_single","goal":"linear-single : ltm -> type.","context":["linear-single"],"tactic_proof":"linear-single-var : linear-single (var X).\nlinear-single-app : linear-single (lapp E1 E2) <- linear-single E1 <- linear-single E2.","source":"twelf_synthetic/linear_lf"} +{"id":89058,"prover":"Twelf","theorem":"weakening","goal":"weakening : of E T -> of E T -> type.","context":["weakening"],"tactic_proof":"%mode weakening +Dof -Dof'.","source":"twelf_synthetic/metatheory"} +{"id":89059,"prover":"Twelf","theorem":"type_unique","goal":"type-unique : of E T1 -> of E T2 -> eq T1 T2 -> type.","context":["type-unique"],"tactic_proof":"%mode type-unique +D1 +D2 -D3.","source":"twelf_synthetic/metatheory"} +{"id":89060,"prover":"Twelf","theorem":"canonical_forms","goal":"canonical : value V -> of V T -> type.","context":["canonical"],"tactic_proof":"%mode canonical +Dv +Dof.","source":"twelf_synthetic/metatheory"} +{"id":89061,"prover":"Twelf","theorem":"progress_lemma","goal":"progress-lemma : of E T -> (value E + step E E') -> type.","context":["progress-lemma"],"tactic_proof":"%mode progress-lemma +Dof -Dresult.","source":"twelf_synthetic/metatheory"} +{"id":89062,"prover":"Twelf","theorem":"preservation_lemma","goal":"preservation-lemma : of E T -> step E E' -> of E' T -> type.","context":["preservation-lemma"],"tactic_proof":"%mode preservation-lemma +Dof +Dstep -Dof'.","source":"twelf_synthetic/metatheory"} +{"id":89063,"prover":"Twelf","theorem":"normalization","goal":"strong-norm : of E T -> type.","context":["strong-norm"],"tactic_proof":"%mode strong-norm +Dof.","source":"twelf_synthetic/metatheory"} +{"id":89064,"prover":"Twelf","theorem":"confluence","goal":"confluence : reduces E E1 -> reduces E E2 -> (reduces E1 E' /\\ reduces E2 E') -> type.","context":["confluence"],"tactic_proof":"%mode confluence +D1 +D2 -D3.","source":"twelf_synthetic/metatheory"} +{"id":89065,"prover":"Twelf","theorem":"forall_type","goal":"forall-tp : (tp -> tp) -> tp.","context":["forall-tp"],"tactic_proof":"forall-intro : of E (forall-tp A) <- ({X:tp} of E (A X)).\nforall-elim : of (tapp E T) (A T) <- of E (forall-tp A).","source":"twelf_synthetic/polymorphism"} +{"id":89066,"prover":"Twelf","theorem":"exists_type","goal":"exists-tp : (tp -> tp) -> tp.","context":["exists-tp"],"tactic_proof":"pack : of (pack T E) (exists-tp A) <- of E (A T).\nunpack : of (open E1 [X] [x] E2) C <- of E1 (exists-tp A) <- ({X:tp} {x:tm} of x (A X) -> of (E2 X x) C).","source":"twelf_synthetic/polymorphism"} +{"id":89067,"prover":"Twelf","theorem":"type_abstraction","goal":"tabs : tp -> (tp -> tm) -> tm.","context":["tabs"],"tactic_proof":"of-tabs : of (tabs K E) (forall-tp A) <- ({X:tp} of (E X) (A X)).","source":"twelf_synthetic/polymorphism"} +{"id":89068,"prover":"Twelf","theorem":"param_poly","goal":"parametricity : of E (forall-tp A) -> type.","context":["parametricity"],"tactic_proof":"%mode parametricity +D.","source":"twelf_synthetic/polymorphism"} +{"id":89069,"prover":"Twelf","theorem":"subtype","goal":"sub : tp -> tp -> type.","context":["sub"],"tactic_proof":"sub-refl : sub T T.\nsub-trans : sub T1 T3 <- sub T1 T2 <- sub T2 T3.\nsub-arrow : sub (arr S1 T1) (arr S2 T2) <- sub S2 S1 <- sub T1 T2.","source":"twelf_synthetic/polymorphism"} +{"id":89070,"prover":"Twelf","theorem":"module_signature","goal":"module-sig : type.","context":["module-sig"],"tactic_proof":"mk-sig : list -> module-sig.","source":"twelf_synthetic/modules"} +{"id":89071,"prover":"Twelf","theorem":"module_impl","goal":"module-impl : module-sig -> type.","context":["module-impl"],"tactic_proof":"mk-impl : list -> module-impl Sig.","source":"twelf_synthetic/modules"} +{"id":89072,"prover":"Twelf","theorem":"functor","goal":"functor : module-sig -> module-sig -> type.","context":["functor"],"tactic_proof":"apply-functor : functor S1 S2 -> module-impl S1 -> module-impl S2 -> type.","source":"twelf_synthetic/modules"} +{"id":89073,"prover":"Twelf","theorem":"abstract_type","goal":"abs-tp : type.","context":["abs-tp"],"tactic_proof":"pack-abs : tp -> (tp -> tp) -> abs-tp.\nopen-abs : abs-tp -> (tp -> tp -> tp) -> tp -> type.","source":"twelf_synthetic/modules"} +{"id":89074,"prover":"Twelf","theorem":"structure_eq","goal":"struct-eq : module-impl S -> module-impl S -> type.","context":["struct-eq"],"tactic_proof":"%mode struct-eq +M1 +M2.","source":"twelf_synthetic/modules"} +{"id":89075,"prover":"Twelf","theorem":"include_module","goal":"include : module-impl S1 -> module-impl S2 -> module-impl S3 -> type.","context":["include"],"tactic_proof":"%mode include +M1 +M2 -M3.","source":"twelf_synthetic/modules"} +{"id":89076,"prover":"Twelf","theorem":"record","goal":"record : type.","context":["record"],"tactic_proof":"empty-rec : record.\ncons-rec : label -> tm -> record -> record.","source":"twelf_synthetic/records_twelf"} +{"id":89077,"prover":"Twelf","theorem":"label","goal":"label : type.","context":["label"],"tactic_proof":"lab-a : label.\nlab-b : label.\nlab-c : label.","source":"twelf_synthetic/records_twelf"} +{"id":89078,"prover":"Twelf","theorem":"rec_lookup","goal":"lookup : label -> record -> tm -> type.","context":["lookup"],"tactic_proof":"lookup-head : lookup L (cons-rec L V R) V.\nlookup-tail : lookup L (cons-rec L' V R) V' <- lookup L R V'.","source":"twelf_synthetic/records_twelf"} +{"id":89079,"prover":"Twelf","theorem":"rec_update","goal":"update : label -> tm -> record -> record -> type.","context":["update"],"tactic_proof":"update-head : update L V (cons-rec L V' R) (cons-rec L V R).\nupdate-tail : update L V (cons-rec L' V' R) (cons-rec L' V' R') <- update L V R R'.","source":"twelf_synthetic/records_twelf"} +{"id":89080,"prover":"Twelf","theorem":"rec_concat","goal":"rec-concat : record -> record -> record -> type.","context":["rec-concat"],"tactic_proof":"rec-concat-nil : rec-concat empty-rec R R.\nrec-concat-cons : rec-concat (cons-rec L V R1) R2 (cons-rec L V R3) <- rec-concat R1 R2 R3.","source":"twelf_synthetic/records_twelf"} +{"id":89081,"prover":"Twelf","theorem":"trace","goal":"trace : type.","context":["trace"],"tactic_proof":"empty-trace : trace.\nstep-trace : tm -> tm -> trace -> trace.","source":"twelf_synthetic/traces"} +{"id":89082,"prover":"Twelf","theorem":"trace_step","goal":"trace-step : trace -> tm -> tm -> type.","context":["trace-step"],"tactic_proof":"%mode trace-step +T +E -E'.","source":"twelf_synthetic/traces"} +{"id":89083,"prover":"Twelf","theorem":"trace_append","goal":"trace-append : trace -> trace -> trace -> type.","context":["trace-append"],"tactic_proof":"trace-app-nil : trace-append empty-trace T T.\ntrace-app-cons : trace-append (step-trace E1 E2 T1) T2 (step-trace E1 E2 T3) <- trace-append T1 T2 T3.","source":"twelf_synthetic/traces"} +{"id":89084,"prover":"Twelf","theorem":"evaluates","goal":"evaluates : tm -> tm -> type.","context":["evaluates"],"tactic_proof":"eval-refl : evaluates E E.\neval-step : evaluates E E'' <- step E E' <- evaluates E' E''.","source":"twelf_synthetic/traces"} +{"id":89085,"prover":"Twelf","theorem":"multistep","goal":"multistep : tm -> tm -> trace -> type.","context":["multistep"],"tactic_proof":"multistep-refl : multistep E E empty-trace.\nmultistep-step : multistep E E'' (step-trace E E' T) <- step E E' <- multistep E' E'' T.","source":"twelf_synthetic/traces"} +{"id":89086,"prover":"Twelf","theorem":"bigstep","goal":"bigstep : tm -> tm -> type.","context":["bigstep"],"tactic_proof":"bigstep-val : bigstep V V <- value V.\nbigstep-app : bigstep (app E1 E2) V <- bigstep E1 (lam T E) <- bigstep E2 V2 <- bigstep (E V2) V.","source":"twelf_synthetic/bigstep"} +{"id":89087,"prover":"Twelf","theorem":"bigstep_det","goal":"bigstep-det : bigstep E V1 -> bigstep E V2 -> eq V1 V2 -> type.","context":["bigstep-det"],"tactic_proof":"%mode bigstep-det +D1 +D2 -D3.","source":"twelf_synthetic/bigstep"} +{"id":89088,"prover":"Twelf","theorem":"bigstep_value","goal":"bigstep-value : bigstep E V -> value V -> type.","context":["bigstep-value"],"tactic_proof":"%mode bigstep-value +D -Dv.","source":"twelf_synthetic/bigstep"} +{"id":89089,"prover":"Twelf","theorem":"bigstep_of","goal":"bigstep-of : bigstep E V -> of E T -> of V T -> type.","context":["bigstep-of"],"tactic_proof":"%mode bigstep-of +D1 +D2 -D3.","source":"twelf_synthetic/bigstep"} +{"id":89090,"prover":"Twelf","theorem":"bigstep_smallstep","goal":"bigstep-smallstep : bigstep E V -> multistep E V _ -> type.","context":["bigstep-smallstep"],"tactic_proof":"%mode bigstep-smallstep +D1 -D2.","source":"twelf_synthetic/bigstep"} +{"id":89091,"prover":"Twelf","theorem":"hoas_abs","goal":"habs : (tm -> tm) -> tm.","context":["habs"],"tactic_proof":"habs-intro : of (habs E) (arr T1 T2) <- ({x:tm} of x T1 -> of (E x) T2).","source":"twelf_synthetic/hoas"} +{"id":89092,"prover":"Twelf","theorem":"hoas_app","goal":"happ : tm -> tm -> tm.","context":["happ"],"tactic_proof":"happ-intro : of (happ E1 E2) T2 <- of E1 (arr T1 T2) <- of E2 T1.","source":"twelf_synthetic/hoas"} +{"id":89093,"prover":"Twelf","theorem":"hoas_beta","goal":"hstep : tm -> tm -> type.","context":["hstep"],"tactic_proof":"hstep-beta : hstep (happ (habs E) V) (E V) <- value V.","source":"twelf_synthetic/hoas"} +{"id":89094,"prover":"Twelf","theorem":"hoas_subst","goal":"hsubst : (tm -> tm) -> tm -> tm -> type.","context":["hsubst"],"tactic_proof":"%mode hsubst +E +V -E'.","source":"twelf_synthetic/hoas"} +{"id":89095,"prover":"Twelf","theorem":"parametric_hoas","goal":"phabs : (tm -> tm) -> tm.","context":["phabs"],"tactic_proof":"%block phabs-block : block {x:tm}.","source":"twelf_synthetic/hoas"} +{"id":89096,"prover":"Twelf","theorem":"token","goal":"token : type.","context":["token"],"tactic_proof":"tok-ident : string -> token.\ntok-num : nat -> token.\ntok-lparen : token.\ntok-rparen : token.\ntok-plus : token.\ntok-times : token.","source":"twelf_synthetic/parsing"} +{"id":89097,"prover":"Twelf","theorem":"parse_expr","goal":"parse : list -> tm -> list -> type.","context":["parse"],"tactic_proof":"%mode parse +Input -Result -Rest.","source":"twelf_synthetic/parsing"} +{"id":89098,"prover":"Twelf","theorem":"lex","goal":"lex : string -> list -> type.","context":["lex"],"tactic_proof":"%mode lex +Input -Tokens.","source":"twelf_synthetic/parsing"} +{"id":89099,"prover":"Twelf","theorem":"ast","goal":"ast : type.","context":["ast"],"tactic_proof":"ast-num : nat -> ast.\nast-var : string -> ast.\nast-bin : op -> ast -> ast -> ast.","source":"twelf_synthetic/parsing"} +{"id":89100,"prover":"Twelf","theorem":"op","goal":"op : type.","context":["op"],"tactic_proof":"op-add : op.\nop-sub : op.\nop-mul : op.\nop-div : op.","source":"twelf_synthetic/parsing"} +{"id":89101,"prover":"Twelf","theorem":"grammar","goal":"grammar-rule : type.","context":["grammar-rule"],"tactic_proof":"gr-term : symbol -> grammar-rule.\ngr-alt : grammar-rule -> grammar-rule -> grammar-rule.\ngr-seq : grammar-rule -> grammar-rule -> grammar-rule.","source":"twelf_synthetic/parsing"} +{"id":89102,"prover":"Twelf","theorem":"dfa_state","goal":"state : type.","context":["state"],"tactic_proof":"init-state : state.\ntrans-state : state -> char -> state.","source":"twelf_synthetic/automata"} +{"id":89103,"prover":"Twelf","theorem":"dfa_accept","goal":"accepts : dfa -> string -> type.","context":["accepts"],"tactic_proof":"%mode accepts +D +S.","source":"twelf_synthetic/automata"} +{"id":89104,"prover":"Twelf","theorem":"nfa_run","goal":"nfa-run : nfa -> list -> state -> type.","context":["nfa-run"],"tactic_proof":"%mode nfa-run +N +S -Q.","source":"twelf_synthetic/automata"} +{"id":89105,"prover":"Twelf","theorem":"regex","goal":"regex : type.","context":["regex"],"tactic_proof":"re-char : char -> regex.\nre-concat : regex -> regex -> regex.\nre-alt : regex -> regex -> regex.\nre-star : regex -> regex.\nre-epsilon : regex.","source":"twelf_synthetic/automata"} +{"id":89106,"prover":"Twelf","theorem":"regex_match","goal":"re-match : regex -> string -> type.","context":["re-match"],"tactic_proof":"%mode re-match +R +S.","source":"twelf_synthetic/automata"} +{"id":89107,"prover":"Twelf","theorem":"pda","goal":"pda-state : type.","context":["pda-state"],"tactic_proof":"pda-init : pda-state.\npda-push : pda-state -> char -> stack -> pda-state.","source":"twelf_synthetic/automata"} +{"id":89108,"prover":"Twelf","theorem":"io_monad","goal":"io : type -> type.","context":["io"],"tactic_proof":"io-return : A -> io A.\nio-bind : io A -> (A -> io B) -> io B.","source":"twelf_synthetic/effects"} +{"id":89109,"prover":"Twelf","theorem":"state_monad","goal":"state-m : type -> type.","context":["state-m"],"tactic_proof":"state-return : A -> state-m A.\nstate-bind : state-m A -> (A -> state-m B) -> state-m B.\nstate-get : state-m state.\nstate-put : state -> state-m unit.","source":"twelf_synthetic/effects"} +{"id":89110,"prover":"Twelf","theorem":"exception","goal":"exc : type -> type.","context":["exc"],"tactic_proof":"exc-pure : A -> exc A.\nexc-raise : string -> exc A.\nexc-catch : exc A -> (string -> exc A) -> exc A.","source":"twelf_synthetic/effects"} +{"id":89111,"prover":"Twelf","theorem":"continuation","goal":"cont : type -> type -> type.","context":["cont"],"tactic_proof":"cont-pure : A -> cont A R.\ncont-callcc : ((A -> cont B R) -> cont A R) -> cont A R.","source":"twelf_synthetic/effects"} +{"id":89112,"prover":"Twelf","theorem":"free_monad","goal":"free : type -> type.","context":["free"],"tactic_proof":"free-pure : A -> free A.\nfree-op : op-sig -> (result -> free A) -> free A.","source":"twelf_synthetic/effects"} +{"id":89113,"prover":"Twelf","theorem":"add_zero_left","goal":"add-zero-left : {N:nat} plus z N N -> type.","context":["add-zero-left","N"],"tactic_proof":"%mode add-zero-left +N -D.\nadd-zero-left-z : add-zero-left z plus-z.\nadd-zero-left-s : add-zero-left (s N) plus-z <- add-zero-left N _.","source":"twelf_synthetic/numerics_twelf"} +{"id":89114,"prover":"Twelf","theorem":"add_zero_right","goal":"add-zero-right : {N:nat} plus N z N -> type.","context":["add-zero-right","N"],"tactic_proof":"%mode add-zero-right +N -D.\nadd-zero-right-z : add-zero-right z plus-z.\nadd-zero-right-s : add-zero-right (s N) (plus-s D) <- add-zero-right N D.","source":"twelf_synthetic/numerics_twelf"} +{"id":89115,"prover":"Twelf","theorem":"times_zero_right","goal":"times-zero-right : {N:nat} times N z z -> type.","context":["times-zero-right","N"],"tactic_proof":"%mode times-zero-right +N -D.","source":"twelf_synthetic/numerics_twelf"} +{"id":89116,"prover":"Twelf","theorem":"div_algorithm","goal":"div-mod : nat -> nat -> nat -> nat -> type.","context":["div-mod"],"tactic_proof":"div-mod-base : div-mod M N z M <- lt M N.\ndiv-mod-rec : div-mod M N (s Q) R <- leq N M <- sub M N M' <- div-mod M' N Q R.","source":"twelf_synthetic/numerics_twelf"} +{"id":89117,"prover":"Twelf","theorem":"gcd","goal":"gcd : nat -> nat -> nat -> type.","context":["gcd"],"tactic_proof":"gcd-zero : gcd M z M.\ngcd-rec : gcd M N G <- modulo M N R <- gcd N R G.","source":"twelf_synthetic/numerics_twelf"}