mm0 add pub theorem -> expect failure

output.sh

 ✘  ~/projects/mm0   learn ±✚  ./examples/test_pub_theorem.sh
=== Setting up test files ===
=== First Verification (Base case) ===
elab test_thm.mm1
elabbed test_thm.mm1
1 sorts, 1 term/def, 3 ax/thm
Verification succeeded!
=== Experiment 1: Adding a new PUB theorem not declared in MM0 ===
elab test_thm.mm1
elabbed test_thm.mm1
1 sorts, 1 term/def, 4 ax/thm
stmt: F4
cmd: FE: End

at thm_2: invalid command keyword

theorem thm_1 (a b: wff): $ a -> b -> a $;

^

cmds:
  F6: Ref 0  // = expr a:wff
  F7: Ref 0  // = expr a:wff
  F8: Ref 0  // = expr a:wff
  F9: Ref 0  // = expr a:wff
  FA: Ref 0  // = expr a:wff
  FB: Term 0  // = im
  FB: Save
  FC: Term 0  // = im
  FC: Save
  FD: Thm 0  // = ax_1


Experiment 1: Verification FAILED! (exit code: 255)
=== Experiment 2: Adding a new LOCAL theorem not declared in MM0 ===
elab test_thm.mm1
elabbed test_thm.mm1
1 sorts, 1 term/def, 4 ax/thm
Experiment 2: Verification Succeeded!

test_pub_theorem.sh

#!/usr/bin/env bash
set -e

# Paths to executables
MM0_RS="./mm0-rs/target/release/mm0-rs"
MM0_C="./mm0-c/mm0-c"

echo "=== Setting up test files ==="
cat << 'EOF' > examples/test_thm.mm0
strict provable sort wff;
term im (p q: wff): wff; infixr im: $->$ prec 25;
axiom ax_1 (a b: wff): $ a -> b -> a $;
axiom ax_mp (a b: wff): $ a -> b $ > $ a $ > $ b $;
theorem thm_1 (a b: wff): $ a -> b -> a $;
EOF

cat << 'EOF' > examples/test_thm.mm1
strict provable sort wff;
term im (p q: wff): wff; infixr im: $->$ prec 25;
axiom ax_1 (a b: wff): $ a -> b -> a $;
axiom ax_mp (a b: wff): $ a -> b $ > $ a $ > $ b $;
pub theorem thm_1 (a b: wff): $ a -> b -> a $ =
  'ax_1;
EOF

echo "=== First Verification (Base case) ==="
$MM0_RS compile examples/test_thm.mm1 examples/test_thm.mmb
$MM0_C examples/test_thm.mmb < examples/test_thm.mm0
echo "Verification succeeded!"

echo "=== Experiment 1: Adding a new PUB theorem not declared in MM0 ==="
cat << 'EOF' > examples/test_thm.mm1
strict provable sort wff;
term im (p q: wff): wff; infixr im: $->$ prec 25;
axiom ax_1 (a b: wff): $ a -> b -> a $;
axiom ax_mp (a b: wff): $ a -> b $ > $ a $ > $ b $;
pub theorem thm_1 (a b: wff): $ a -> b -> a $ =
  'ax_1;
pub theorem thm_2 (a: wff): $ a -> a -> a $ =
  'ax_1;
EOF

$MM0_RS compile examples/test_thm.mm1 examples/test_thm.mmb
set +e
$MM0_C examples/test_thm.mmb < examples/test_thm.mm0
EXIT_CODE_EXP1=$?
set -e

if [ $EXIT_CODE_EXP1 -eq 0 ]; then
  echo "Experiment 1: Verification Succeeded!"
else
  echo "Experiment 1: Verification FAILED! (exit code: $EXIT_CODE_EXP1)"
fi

echo "=== Experiment 2: Adding a new LOCAL theorem not declared in MM0 ==="
cat << 'EOF' > examples/test_thm.mm1
strict provable sort wff;
term im (p q: wff): wff; infixr im: $->$ prec 25;
axiom ax_1 (a b: wff): $ a -> b -> a $;
axiom ax_mp (a b: wff): $ a -> b $ > $ a $ > $ b $;
pub theorem thm_1 (a b: wff): $ a -> b -> a $ =
  'ax_1;
theorem thm_2 (a: wff): $ a -> a -> a $ =
  'ax_1;
EOF

$MM0_RS compile examples/test_thm.mm1 examples/test_thm.mmb
set +e
$MM0_C examples/test_thm.mmb < examples/test_thm.mm0
EXIT_CODE_EXP2=$?
set -e

if [ $EXIT_CODE_EXP2 -eq 0 ]; then
  echo "Experiment 2: Verification Succeeded!"
else
  echo "Experiment 2: Verification FAILED! (exit code: $EXIT_CODE_EXP2)"
fi

# Clean up temp files
rm -f examples/test_thm.mm0 examples/test_thm.mm1 examples/test_thm.mmb