Try use Isabelle2024-RC2.

[kape1395]

I checked if this branch works with Isabelle 2024-RC2 with the hope that it will resolve the remaining problems.
Initially it failed to build the TLA+ theories with:

Session Pure/Pure
Session TLA+/TLA+
Building TLA+ ...
TLA+: theory TLA+.PredicateLogic
TLA+ FAILED (see also "isabelle build_log -H Error TLA+")
...
***       {identifier: thm list,
***        lhss: term list, name: string, proc: morphism -> proc}
***         -> simproc
***    Argument: "swap_cases_false" : string
***    Reason:
***       Can't unify string to
***          {identifier: thm list,
***           lhss: term list, name: string, proc: morphism -> proc}
***          (Incompatible types)
*** ML error (line 1431 of "~~/src/TLA+/PredicateLogic.thy"):
*** Type error in function application.
***    Function:
***       Simplifier.make_simproc Isabelle62650.ML_context "swap_cases_false" :
***       simproc
***    Argument: {lhss = [(Term.$ (... ..., ...))], proc = fn _ => fn ...} :
***       {lhss: term list, proc: 'a -> 'b -> cterm -> thm option}
***    Reason: Value being applied does not have a function type
*** ML error (line 1438 of "~~/src/TLA+/PredicateLogic.thy"):
*** Type error in function application.
***    Function: Simplifier.make_simproc Isabelle62650.ML_context :
***       {identifier: thm list,
***        lhss: term list, name: string, proc: morphism -> proc}
***         -> simproc
***    Argument: "cases_equal_conj_curry" : string
***    Reason:
***       Can't unify string to
***          {identifier: thm list,
***           lhss: term list, name: string, proc: morphism -> proc}
***          (Incompatible types)
*** ML error (line 1438 of "~~/src/TLA+/PredicateLogic.thy"):
*** Type error in function application.
***    Function:
***       Simplifier.make_simproc Isabelle62650.ML_context
***       "cases_equal_conj_curry"
***       : simproc
***    Argument: {lhss = [(Term.$ (... ..., ...))], proc = fn _ => fn ...} :
***       {lhss: term list, proc: 'a -> 'b -> cterm -> thm option}
***    Reason: Value being applied does not have a function type
*** 
*** At command "declaration" (line 1428 of "~~/src/TLA+/PredicateLogic.thy")
Unfinished session(s): TLA+

Maybe the API for Simplifier.make_simproc has changed. I tried to change the invocations. Now the failures are in simproc_setup, but the output is less informative.

Session Pure/Pure
Session TLA+/TLA+
Building TLA+ ...
TLA+: theory TLA+.PredicateLogic
TLA+ FAILED (see also "isabelle build_log -H Error TLA+")
*** Failed to load theory "TLA+.SetTheory" (unresolved "TLA+.PredicateLogic")
*** Failed to load theory "TLA+.Functions" (unresolved "TLA+.SetTheory")
*** Failed to load theory "TLA+.FixedPoints" (unresolved "TLA+.SetTheory")
*** Failed to load theory "TLA+.Integers" (unresolved "TLA+.FixedPoints", "TLA+.Functions")
*** Failed to load theory "TLA+.IntegerArithmetic" (unresolved "TLA+.Integers")
*** Failed to load theory "TLA+.Tuples" (unresolved "TLA+.IntegerArithmetic")
*** Failed to load theory "TLA+.IntegerDivision" (unresolved "TLA+.IntegerArithmetic")
*** Failed to load theory "TLA+.CaseExpressions" (unresolved "TLA+.Tuples")
*** Failed to load theory "TLA+.Strings" (unresolved "TLA+.Tuples")
*** Failed to load theory "Constant" (unresolved "TLA+.CaseExpressions", "TLA+.IntegerDivision", "TLA+.Strings")
*** Failed to load theory "Zenon" (unresolved "Constant")
*** ML error (line 1794 of "~~/src/TLA+/PredicateLogic.thy"):
*** Handler catches all exceptions.
*** At command "simproc_setup" (line 1776 of "~~/src/TLA+/PredicateLogic.thy")
Unfinished session(s): TLA+

@muenchnerkindl, could you take a look at the problem here?

To build only the Isabelle part, you can go to the deps/isabelle folder and run make clean all there.

[kape1395]

@muenchnerkindl, all the tests are passing with this Isabelle version. What do you think about merging it into #109 ?

[kape1395]

The TLAPS now works with the Isabelle2024-RC2, so I checked if the failures to prove some statements are still here (as in #109). And the problems are still here. I tried to investigate the case of the proofs in the CommunityModules. My findings are in this gist:

https://gist.github.com/kape1395/84562bf5679fe9f9f65c4d85715b7827#file-tlapm_e6d04a_debug-thy

In short, it looks to me that the auto method fails because it rewrites ∀ e ∈ S : op (e) = 0 to ⋀e. ... ⟹ e ∈ S ⟹ ... ⟹ op(e) = 0.

[muenchnerkindl]

@kape1395 I fail to reproduce your results. For me, neither simp nor auto solve your theorem, but blast does. The reduction from ∀ e ∈ S : op (e) = 0 to ⋀e. ... ⟹ e ∈ S ⟹ ... ⟹ op(e) = 0 is expected and should not cause problems.

As for Isabelle-2023, I get the following behavior:

lemma
  fixes S
  assumes "IsFiniteSet(S)"
  fixes op
  assumes "∀e ∈ S : op(e) ∈ Nat"
  (* assumes "f(S) = 0" *)
  assumes "⋀S::c. IsFiniteSet(S) 
             ⟹ (⋀op::c⇒c. ∀e ∈ S : op(e) ∈ Nat 
                   ⟹ ∀e ∈ S : op(e) = 0)"
  shows "∀e ∈ S : op(e) = 0"
  using assms apply auto done

works, but comment out the useless hypothesis, and auto fails (but blast or fast work). Can you reproduce this? I am completely clueless for the moment why this happens.

[kape1395]

Indeed, in Isabelle2023, your lemma is proved by auto, but fails if assumes "f(S) = 0" is uncommented. It also passes if this useless assumption is moved to be the last assumption.

Regarding the simp. Your lemma (with f(S) = 0 removed) fails if the proof is using assms apply simp done but passes with using assms by simp.

[kape1395]

And the simp method tolerates the useless assumption. The following passes on Isabelle2023.

lemma
  fixes S
  assumes "IsFiniteSet(S)"
  fixes op
  assumes "∀e ∈ S : op(e) ∈ Nat"
      and "f(S) = 0"
      and "⋀S::c. IsFiniteSet(S) 
             ⟹ (⋀op::c⇒c. ∀e ∈ S : op(e) ∈ Nat 
                   ⟹ ∀e ∈ S : op(e) = 0)"
  shows "∀e ∈ S : op(e) = 0"
  using assms by simp

and fails with using assms apply simp done.

[kape1395]

@muenchnerkindl, I forgot to tag you in the answers above.

[kape1395]

@muenchnerkindl, I found that there is declare [[simp_trace]] in isabelle.
For your lemma, the traces of using assms apply simp done and using assms by simp differ.
From the first look, it seems that the former case doesn't perform Applying instance of rewrite rule "Pure.norm_hhf_eq".
If needed, I can post the traces generated on my PC.

[muenchnerkindl]

@kape1395 Some more investigation and bisection revealed two issues in SetTheory.thy: (i) one elimination rule was (clearly) too general, and (ii) adding rule bspec to preprocessing for the simplifier also contributed to the observed failure of the auto method (for a reason that I do not understand). I fixed (i) and removed (ii) [the latter was also the case in the old Isabelle theory]. Unfortunately, removing (ii) cripples the prover quite a bit and I had to change several proofs throughout, but the test case that you observed now passes. Could you perhaps see how this version behaves on the TLAPS examples?

[kape1395]

@muenchnerkindl, it works much better now!

• The tlapm tests pass.
• The non-skipped (

  tlapm/.github/workflows/ci.yml

  Line 75 in 5ef530f

  SKIP=(

  ) files from the examples repo pass as well.
• There was a failing proof in CommunityModules (https://github.com/tlaplus/CommunityModules/blob/3fb30f52426b45cda44541b906ad9ebe16ce07c4/modules/FiniteSetsExt_theorems_proofs.tla#L172). I found that TLAPM was generating arith_plus for + in TLA, but there was no definition arith_plus in the new Isabelle theory. Could you look at my change (267496d), if it looks OK to you? With this change the proofs in the CommunityModules repo pass.

I'm still looking at the skipped modules in the examples repo:

• ./specifications/MisraReachability/ReachabilityProofs.tla -- was actually passing on the main branch, but now it fails. Maybe there was a reason why @ahelwer listed it as failing.
• ./specifications/byzpaxos/VoteProof.tla -- 2/761 obligations failed in the main branch, and now it's 6/761.

[kape1395]

@muenchnerkindl,
The failing obligation in ./specifications/MisraReachability/ReachabilityProofs.tla (examples repo) produces the following theory file. I simplified it a bit by renaming symbols and commenting out the unused assumptions.

From my findings:

• blast works for the original/generated lemma (with assumption v'43), but auto fails.
• auto passes if I replace assumption v'43 with v'43_upd.

theory tlapm_edef9e_debug imports Constant Zenon begin

declare [[simp_trace]]

lemma ob'1: (* ba8238e0781360a7e798bc9ab9035b5e *)
  fixes Node
  fixes Succ
  fixes S
  fixes T
  fixes n
(*assumes S_in : "S ∈ SUBSET Node"*)
(*assumes T_in : "T ∈ SUBSET Node"*)
(*assumes v'28: "∀ n ∈ (S) : (fapply ((Succ), (n))) ⊆ (((S) ∪ (T)))"*)
(*assumes n_in : "n ∈ ReachableFrom (S)"*)
  assumes v'42: "RR (0)"
  assumes v'43:     "⋀ ii :: c. ii ∈ Nat ⟹ RR (ii) ⟹ RR (addint (ii, Succ[0]))" (* NOTE: Only blast works with this.*)
(*assumes v'43_upd: "∀ ii ∈ Nat : (RR (ii) ⇒ RR (addint (ii, Succ[0])))" (* NOTE: auto works with this. *) *)
  assumes v'44: "⋀ PP :: c => c.
                    PP (0) ⟹
                    (∀ n_1 ∈ Nat : ((PP (n_1)) ⇒ (PP (addint ((n_1), (Succ[0])))))) ⟹
                    (∀ n_1 ∈ Nat : (PP (n_1)))"
  shows "∀ ii ∈ Nat : RR (ii)" (is "PROP ?ob'1")
  proof -
    show "PROP ?ob'1"
      using assms by auto  (* blast works. *)
  qed

end

[kape1395]

Interestingly, l2 below works, but l3 fails with auto.

lemma l2:
  fixes S P
  assumes "∀e ∈ S : P(e)"
  shows "⋀e. e ∈ S ⟹ P(e)"
  using assms by auto

lemma l3:
  fixes P
  assumes "∀e ∈ Nat : P(e)"
  shows "⋀e. e ∈ Nat ⟹ P(e)"
  using assms by auto (* WORKS with: `by (rule bspec)`, `by (rule l2)`, `by blast` *)

[kape1395]

@muenchnerkindl, after further experimentation, it looks like it's related to the bounded quantifiers. The rewrites are not done in the set over which the variable is quantified. The smallest example I found is:

lemma l3_experiments':
  fixes P
  assumes "∀e : e ∈ Nat ⇒ P(e)"
  shows "⋀e. e ∈ Nat ⟹ P(e)"
  using assms by auto (* works *)

lemma l3_experiments:
  fixes P
  assumes "∀e ∈ Nat : P(e)"
  shows "⋀e. e ∈ Nat ⟹ P(e)"
  using assms by auto (* fails. *)

Adding a rule

lemma bAll_unb [simp]:
  "(∀e ∈ T : P(e)) = (∀e : e ∈ T ⇒ P(e))"
  using bAll_def by simp

solves this exact problem (as well as the cases above), but creates a lot of failures (loops) in the TLA theory itself. Probably something different is needed.

[kape1395]

@muenchnerkindl, there are no more regressions than in the main branch.

• The tlapm tests pass.
• The proofs in CommunityModules pass.
• The same proofs pass in the Examples repo with --stretch 1.2. If the stretch is not used, 3/761 instead of 2/761 fail for specifications/byzpaxos/VoteProof.tla. But maybe that's good enough since that specification is failing with the main branch anyway.

[muenchnerkindl]

@kape1395 Thank you very much for investigating this further! I would have hoped the interference between bounded quantification and rewrite of Nat to be handled by the congruence rules bAllCong and bExCong but unfortunately that does not seem to be the case. Your changes appear to improve things a lot, let's go with them and observe how the situation evolves.

Please add the DCO to your commit so that it can be merged. Thanks again!

[kape1395]

@muenchnerkindl, thanks for reviewing the changes!

I believe the signoff/DCO is missing for your commit: d5d8dbf. All my commits are signed except the merge commits, but the DCO check was previously ignoring them.

Can we merge it anyway? The original Isabelle branch has a lot of commits with no signoff.

[muenchnerkindl]

The Linux foundation requires us to sign all commits: this was not the case before. In fact, I had noticed that I had forgotten to sign and tried to amend the commit but apparently this was counted as a separate commit. Hopefully this is now fixed.