Powered by AppSignal & Oban Pro
Notesclub
Sign in with GitHub
created by hec & contributors
terms privacy

A Structured Set of Higher-Order Problems - Section 5

notebooks/structured_HOL_problems.livemd

avatar
Johannes Schuster
avatar
avatar
Share to X
Share to Bluesky
More notebooks

A Structured Set of Higher-Order Problems - Section 5

System.put_env("HEX_HTTP_CONCURRENCY", "1")
System.put_env("HEX_HTTP_TIMEOUT", "120")

Mix.install([
  {:shot25, path: Path.join(__DIR__, "..")},
  {:behold, "~> 1.1.0"},
  {:kino, "~> 0.17.0"}
])

Setup

import HOL.Data
import SHOT25.Prover
import BeHOLd.Parser
import BeHOLd.TPTP
import SHOT25.Runner
import SHOT25.PrettyPrint
alias BeHOLd.Data.Context

Logger.configure(level: :error)
form =
  Kino.Control.form(
    [
      name: Kino.Input.checkbox("Debug")
    ],
    report_changes: true
  )

Kino.listen(form, fn event ->
  if event.data.name == true do
    Logger.configure(level: :info)
    Logger.put_application_level(:hol, :error)
  else
    Logger.configure(level: :error)
  end
end)

form

Definitions

defmodule MyDefs do
  def leibnitz_eq(t) do
    type = String.replace(t, "$", "")
      |> String.replace("(", "OPEN")
      |> String.replace(")", "CLOSE")
      |> String.replace(">", "TO")
    "thf(leibnitz_eq_#{type},definition," <> "\n\t" <>
    "leibnitz_eq_#{type} =" <> "\n\t\t" <>
    "^[X : #{t}, Y : #{t}]: ![P : #{t}>$o]: P @ X <=> P @ Y" <> "\n" <>
    ").\n"
  end
  
  def andrews_eq(t) do
    type = String.replace(t, "$", "")
      |> String.replace("(", "OPEN")
      |> String.replace(")", "CLOSE")
      |> String.replace(">", "TO")
    "thf(andrews_eq_#{type},definition," <> "\n\t" <>
    "andrews_eq_#{type} =" <> "\n\t\t" <>
    "^[X : #{t}, Y : #{t}]:" <> "\n\t\t\t" <>
    "![Q : #{t}>#{t}>$o]: (![Z : #{t}]: Q @ Z @ Z) => (Q @ X @ Y)" <> "\n" <>
    ").\n"
  end
  
  def extens_eq(t1, t2) do
    type1 = String.replace(t1, "$", "")
      |> String.replace("(", "OPEN")
      |> String.replace(")", "CLOSE")
      |> String.replace(">", "TO")
    type2 = String.replace(t2, "$", "")
      |> String.replace("(", "OPEN")
      |> String.replace(")", "CLOSE")
      |> String.replace(">", "TO")
    "thf(extens_eq_#{type1}_#{type2},definition," <> "\n\t" <>
    "extens_eq_#{type1}_#{type2} =" <> "\n\t\t" <>
    "^[X : #{t1}>#{t2}, Y : #{t1}>#{t2}]: ![V : #{t1}]: X @ V = Y @ V" <> "\n" <>
    ").\n"
  end
end
import MyDefs

5.1 Properties of Equality

Example 6a)

"![X: $i]: X = X"
#  |> parse |> prove |> pp_proof_result |> IO.puts
# THM -> 0ms
{:ok, problem} = parse_string(leibnitz_eq("$i") <>
"thf(leibnitz_eq_reflexive,conjecture,
  ![X : $i] : leibnitz_eq_i @ X @ X
)."
)

# run_prover(problem)
# THM -> 2ms
{:ok, problem} = parse_string(andrews_eq("$i") <>
"thf(andrews_eq_reflexive,conjecture,
  ![X : $i] : andrews_eq_i @ X @ X
).")

# run_prover(problem)
# THM -> 2ms
{:ok, problem} = parse_string(extens_eq("$i", "$i") <>
"thf(extens_eq_reflexive,conjecture,
  ![X : $i>$i] : extens_eq_i_i @ X @ X
).")

# run_prover(problem)
# THM -> 3ms

Example 6b)

"![X : $i, Y : $i]: ((X = Y) => (Y = X))"
#  |> parse |> prove |> pp_proof_result |> IO.puts
# THM -> 30ms
{:ok, problem} = parse_string(leibnitz_eq("$i") <>
"
thf(leibnitz_eq_symm,conjecture,
  ![X : $i, Y : $i]: ((leibnitz_eq_i @ X @ Y) => (leibnitz_eq_i @ Y @ X))
).")

# run_prover(problem)
# THM -> 0.1s
{:ok, problem} = parse_string(andrews_eq("$i") <>
"thf(andrews_eq_symm,conjecture,
  ![X : $i, Y : $i]: ((andrews_eq_i @ X @ Y) => (andrews_eq_i @ Y @ X))
).")

# run_prover(problem)
# THM -> 5ms
{:ok, problem} = parse_string(extens_eq("$i", "$i") <>
"thf(extens_eq_symm,conjecture,
  ![X : $i>$i, Y : $i>$i]: ((extens_eq_i_i @ X @ Y) => (extens_eq_i_i @ Y @ X))
).")

# run_prover(problem)
# -> timeout

Example 6c)

"![X : $i, Y : $i, Z : $i]: (((X = Y) & (Y = Z)) => (X = Z))"
#  |> parse |> prove |> pp_proof_result |> IO.puts
# -> timeout
{:ok, problem} = parse_string(leibnitz_eq("$i") <>
"thf(leibnitz_eq_trans,conjecture,
  ![X : $i, Y : $i, Z : $i]: (
    ((leibnitz_eq_i @ X @ Y) & (leibnitz_eq_i @ Y @ Z))
    =>
    (leibnitz_eq_i @ X @ Z)
  )
).")

# run_prover(problem)
# -> timeout
{:ok, problem} = parse_string(andrews_eq("$i") <>
"thf(andrews_eq_trans,conjecture,
  ![X : $i, Y : $i, Z : $i]: (
    ((andrews_eq_i @ X @ Y) & (andrews_eq_i @ Y @ Z))
    =>
    (andrews_eq_i @ X @ Z)
  )
).")

# run_prover(problem)
# THM -> 10ms
{:ok, problem} = parse_string(extens_eq("$i", "$i") <>
"thf(extens_eq_trans,conjecture,
  ![X : $i>$i, Y : $i>$i, Z : $i>$i]: (
    ((extens_eq_i_i @ X @ Y) & (extens_eq_i_i @ Y @ Z))
    =>
    (extens_eq_i_i @ X @ Z)
  )
).")

# run_prover(problem)
# -> timeout

Example 7a)

"![X : $i, Y : $i, F : $i>$i]: ((X = Y) => ((F @ X) = (F @ Y)))"
#  |> parse |> prove |> pp_proof_result |> IO.puts
# THM -> 31ms
{:ok, problem} = parse_string(leibnitz_eq("$i") <>
"thf(leibnitz_congruent_i,conjecture,
  ![X : $i, Y : $i, F : $i>$i]: (
    (leibnitz_eq_i @ X @ Y) => (leibnitz_eq_i @ (F @ X) @ (F @ Y))
  )
).")

# run_prover(problem)
# THM -> 32ms
{:ok, problem} = parse_string(andrews_eq("$i") <>
"thf(andrews_congruent_i,conjecture,
  ![X : $i, Y : $i, F : $i>$i]: (
    (andrews_eq_i @ X @ Y) => (andrews_eq_i @ (F @ X) @ (F @ Y))
  )
).")

# run_prover(problem)
# THM -> 3ms
{:ok, problem} = parse_string(extens_eq("$i", "$i") <>
"thf(extens_congruent_i,conjecture,
  ![X : $i>$i, Y : $i>$i, F : ($i>$i)>$i>$i]: (
    (extens_eq_i_i @ X @ Y) => (extens_eq_i_i @ (F @ X) @ (F @ Y))
  )
).")

# run_prover(problem)
# -> timeout

Example 7b)

"![X : $i, Y : $i, P : $i>$o]: (((X = Y) & P @ X) => P @ Y)"
#  |> parse |> prove |> pp_proof_result |> IO.puts
# THM -> 8ms
{:ok, problem} = parse_string(leibnitz_eq("$i") <>
"thf(leibnitz_congruent_o,conjecture,
  ![X : $i, Y : $i, P : $i>$o]: (
    ((leibnitz_eq_i @ X @ Y) & (P @ X)) => (P @ Y)
  )
).")

# run_prover(problem)
# THM -> 7ms
{:ok, problem} = parse_string(andrews_eq("$i") <>
"thf(andrews_congruent_o,conjecture,
  ![X : $i, Y : $i, P : $i>$o]: (
    ((andrews_eq_i @ X @ Y) & (P @ X)) => (P @ Y)
  )
).")

# run_prover(problem)
# CSA -> 3ms
{:ok, problem} = parse_string(extens_eq("$i", "$i") <>
"thf(extens_congruent_i,conjecture,
  ![X : $i, Y : $i, P : $i>$o]: (
    ((extens_eq_i @ X @ Y) & (P @ X)) => (P @ Y)
  )
).")

# run_prover(problem)
# CSA -> 2ms

Example 8

{:ok, problem} = parse_string(leibnitz_eq("$i") <>
"thf(leibnitz_implies_primitive,conjecture,
  ![X : $i, Y : $i]: (
    (leibnitz_eq_i @ X @ Y) => (X = Y)
  )
).")

# run_prover(problem)
# THM -> 30ms

Example 9a)

"![F : $i>$i, G : $i>$i]: ((F = G) => (![X : $i]: ((F @ X) = (G @ X))))"
#  |> parse |> prove |> pp_proof_result |> IO.puts
# -> timeout
{:ok, problem} = parse_string(leibnitz_eq("$i") <> leibnitz_eq("($i>$i)") <>
"thf(leibnitz_trivial_extensional,conjecture,
![F : $i>$i, G: $i>$i]:
  ((leibnitz_eq_OPENiTOiCLOSE @ F @ G) => (![X : $i]: (leibnitz_eq_i @ (F @ X) @ (G @ X))))
).")

# run_prover(problem)
# THM -> 48ms
{:ok, problem} = parse_string(andrews_eq("$i") <> andrews_eq("($i>$i)") <>
"thf(andrews_trivial_extensional,conjecture,
![F : $i>$i, G: $i>$i]:
  ((andrews_eq_OPENiTOiCLOSE @ F @ G) => (![X : $i]: (andrews_eq_i @ (F @ X) @ (G @ X))))
).")

# run_prover(problem)
# THM -> 5ms

Example 9b)

"![A : $o, B : $o]: ((A = B) => (A <=> B))"
#  |> parse |> prove |> pp_proof_result |> IO.puts
# THM -> 2ms
{:ok, problem} = parse_string(leibnitz_eq("$o") <>
"thf(leibnitz_trivial_extensional,conjecture,
![A : $o, B : $o]: ((leibnitz_eq_o @ A @ B) => (A <=> B))
).")

# run_prover(problem)
# THM -> 7ms
{:ok, problem} = parse_string(andrews_eq("$o") <>
"thf(andrews_trivial_extensional,conjecture,
![A : $o, B : $o]: ((andrews_eq_o @ A @ B) => (A <=> B))
).")

# run_prover(problem)
# CSA -> 1ms

Example 10

"![A : $o, B : $o]: ((A <=> B) => (A = B))"
#  |> parse |> prove |> pp_proof_result |> IO.puts
# THM -> 1ms
{:ok, problem} = parse_string(leibnitz_eq("$o") <>
"thf(leibnitz_nontrivial_extensional,conjecture,
![A : $o, B : $o]: ((A <=> B) => (leibnitz_eq_o @ A @ B))
).")

# run_prover(problem)
# CSA -> 1ms
{:ok, problem} = parse_string(andrews_eq("$o") <>
"thf(andrews_nontrivial_extensional,conjecture,
![A : $o, B : $o]: ((A <=> B) => (andrews_eq_o @ A @ B))
).")

# run_prover(problem)
# THM -> 5ms

Example 11

"![F : $i>$i, G : $i>$i]: ((![X : $i]: ((F @ X) = (G @ X))) => F = G)"
#  |> parse |> prove |> pp_proof_result |> IO.puts
# -> timeout
{:ok, problem} = parse_string(leibnitz_eq("$i") <> leibnitz_eq("($i>$i)") <>
"thf(leibnitz_nontrivial_extensional,conjecture,
![F : $i>$i, G : $i>$i]:
  (![X : $i]: (
    (leibnitz_eq_i @ (F @ X) @ (G @ X))
    =>
    (leibnitz_eq_OPENiTOiCLOSE @ F @ G)
  ))
).")

# run_prover(problem)
# INC -> 10ms
{:ok, problem} = parse_string(andrews_eq("$i") <> andrews_eq("($i>$i)") <>
"thf(andrews_nontrivial_extensional,conjecture,
![F : $i>$i, G : $i>$i]:
  (![X : $i]: (
    (andrews_eq_i @ (F @ X) @ (G @ X))
    =>
    (andrews_eq_OPENiTOiCLOSE @ F @ G)
  ))
).")

# run_prover(problem)
# THM -> 29ms
{:ok, problem} = parse_string(extens_eq("$i", "$i") <> extens_eq("$i", "($i>$i)") <>
"thf(extens_nontrivial_extensional,conjecture,
![F : $i>$i>$i, G : $i>$i>$i]:
  (![X : $i]: (
    (extens_eq_i_i @ (F @ X) @ (G @ X))
    =>
    (extens_eq_i_OPENiTOiCLOSE @ F @ G)
  ))
).")

# run_prover(problem)
# INC -> 29.4s

5.2 Extensionality

Example 12

ctx = Context.new()
  |> Context.put_const("f", mk_type(:i, [mk_type(:i)]))

"(p @ (^[X : $i] : f @ X)) => p @ f"
#  |> parse(ctx) |> prove |> pp_proof_result |> IO.puts
# THM -> 1.4s

Example 13

ctx = Context.new() |> Context.put_const("f", mk_type(:i, [mk_type(:i)]))

"(![X : $i]: ((f @ X) = X)) & (p @ (^[X : $i] : X)) => (p @ (^[X : $i]: f @ X))"
#  |> parse(ctx) |> prove |> pp_proof_result |> IO.puts
# INC -> 11s
{:ok, problem} = parse_string(leibnitz_eq("$i") <>
"thf(conj,conjecture,
((![X : $i]: (leibnitz_eq_i @ (f @ X) @ X)) & (p @ ^[X : $i] : X)) => p @ ^[X : $i]: f @ X
).")

# run_prover(problem)
# INC -> 10.8s
{:ok, problem} = parse_string(andrews_eq("$i") <>
"thf(f_type,type, f : $i>$i).
thf(conj,conjecture,
((![X : $i]: (andrews_eq_i @ (f @ X) @ X)) & (p @ ^[X : $i] : X)) => p @ ^[X : $i]: f @ X
).")

# run_prover(problem)
# INC -> 0.1s

Example 14

ctx = Context.new() |> Context.put_const("f", mk_type(:i, [mk_type(:i)]))

"(![X : $i]: ((f @ X) = X)) & (p @ (^[X : $i] : X)) => (p @ f)"
#  |> parse(ctx) |> prove |> pp_proof_result |> IO.puts
# INC -> 10.5s
{:ok, problem} = parse_string(leibnitz_eq("$i") <>
"thf(f_type,type, f : $i>$i).
thf(conj,conjecture,
((![X : $i]: (leibnitz_eq_i @ (f @ X) @ X)) & (p @ ^[X : $i] : X)) => p @ f
).")

# run_prover(problem)
# INC -> 10.7s
{:ok, problem} = parse_string(andrews_eq("$i") <>
"thf(f_type,type, f : $i>$i).
thf(conj,conjecture,
((![X : $i]: (andrews_eq_i @ (f @ X) @ X)) & (p @ ^[X : $i] : X)) => p @ f
).")

# run_prover(problem)
# INC -> 96ms

Example 15

"p @ (a & b) => p @ (b & a)"
#  |> parse |> prove |> pp_proof_result |> IO.puts
# THM -> 2ms
"a & b & p @ a => p @ b"
#  |> parse |> prove |> pp_proof_result |> IO.puts
# CSA -> 1ms

Example 16

"p @ a & p @ b => p @ (a & b)"
#  |> parse |> prove |> pp_proof_result |> IO.puts
# CSA -> 27ms

Example 17

"~(a = (~a))"
#  |> parse |> prove |> pp_proof_result |> IO.puts
# THM -> 0ms

Example 18

ctx = Context.new()
  |> Context.put_const("h", mk_type(:i, [mk_type(:o)]))

"(h @ ((h @ $true) = (h @ $false))) = (h @ $false)"
#  |> parse(ctx) |> prove |> pp_proof_result |> IO.puts
# CSA -> 1ms
{:ok, problem} = parse_string(leibnitz_eq("$i") <>
"thf(conj,conjecture,
leibnitz_eq_i @ (h @ (leibnitz_eq_i @ (h @ $true) @ (h @ $false))) @ (h @ $false)
).")

# run_prover(problem)
# CSA -> 1ms
{:ok, problem} = parse_string(andrews_eq("$i") <>
"thf(h_type,type, h : $o>$i).
thf(conj,conjecture,
andrews_eq_i @ (h @ (andrews_eq_i @ (h @ $true) @ (h @ $false))) @ (h @ $false)
).")

# run_prover(problem)
# THM -> 2ms

Example 19

ctx = Context.new()
  |> Context.put_const("p", mk_type(:o, [mk_type(:i, [mk_type(:i)])]))
  |> Context.put_const("f", mk_type(:i, [mk_type(:o), mk_type(:i)]))
  |> Context.put_const("a", mk_type(:o, [mk_type(:i, [mk_type(:i)])]))
  |> Context.put_const("b", mk_type(:o))

"(p @ (^[X : $i]: f @ ((a @ (^[X : $i]: f @ b @ X)) & b) @ X)) => p @ (f @ (b & (a @ (f @ b))))"
#  |> parse(ctx) |> prove |> pp_proof_result |> IO.puts
# THM -> 1ms

Example 20a)

"![X : $o, Y : $o]: X & Y => ~(~X | ~Y)"
#  |> parse |> prove |> pp_proof_result |> IO.puts
# THM -> 1ms

Example 20b)

"![X : $o, Y : $o]: ((X & Y) = (~(~X | ~Y)))"
#  |> parse |> prove |> pp_proof_result |> IO.puts
# THM -> 2ms
{:ok, problem} = parse_string(leibnitz_eq("$o") <>
"thf(conj,conjecture,
![X : $o, Y : $o]: leibnitz_eq_o @ (X & Y) @ (~(~X | ~Y))
).")

# run_prover(problem)
# CSA -> 3ms
{:ok, problem} = parse_string(andrews_eq("$o") <>
"thf(conj,conjecture,
![X : $o, Y : $o]: andrews_eq_o @ (X & Y) @ (~(~X | ~Y))
).")

# run_prover(problem)
# THM -> 2ms

Example 20c)

"(^[U : $o, V: $o] : U & V) = (^[X : $o, Y : $o]: ~(~X | ~Y))"
#  |> parse |> prove |> pp_proof_result |> IO.puts
# THM -> 2ms
{:ok, problem} = parse_string(leibnitz_eq("($o>$o>$o)") <>
"thf(conj,conjecture,
leibnitz_eq_OPENoTOoTOoCLOSE @ (^[U : $o, V: $o] : U & V) @ (^[X : $o, Y : $o]: ~(~X | ~Y))
).")

# run_prover(problem)
# CSA -> 2ms
{:ok, problem} = parse_string(andrews_eq("($o>$o>$o)") <>
"thf(conj,conjecture,
andrews_eq_OPENoTOoTOoCLOSE @ (^[U : $o, V: $o] : U & V) @ (^[X : $o, Y : $o]: ~(~X | ~Y))
).")

# run_prover(problem)
# THM -> 2ms

Example 20d)

"(&) = (^[X : $o, Y : $o]: ~(~X | ~Y))"
#  |> parse |> prove |> pp_proof_result |> IO.puts
# THM -> 2ms
{:ok, problem} = parse_string(leibnitz_eq("($o>$o>$o)") <>
"thf(conj,conjecture,
leibnitz_eq_OPENoTOoTOoCLOSE @ (&) @ (^[X : $o, Y : $o]: ~(~X | ~Y))
).")

# run_prover(problem)
# CSA -> 2ms
{:ok, problem} = parse_string(andrews_eq("($o>$o>$o)") <>
"thf(conj,conjecture,
andrews_eq_OPENoTOoTOoCLOSE @ (&) @ (^[X : $o, Y : $o]: ~(~X | ~Y))
).")

# run_prover(problem)
# THM -> 2ms

Example 21

"
(
  (p @ ^[X : $o]: X) &
  (p @ ^[X : $o]: ~X) &
  (p @ ^[X : $o]: $false) &
  (p @ ^[X : $o]: $true)
)
=>
![Y : $o>$o]: p @ Y
"
#  |> parse |> prove |> pp_proof_result |> IO.puts
# CSA -> 2ms

Other notebooks:

Back