search

tlaplus / tlapm

The TLA Proof Manager
https://proofs.tlapl.us/
BSD 2-Clause "Simplified" License
65 stars 20 forks source link

Try use Isabelle2024-RC2. #124

Closed kape1395 closed 4 months ago

kape1395 commented 5 months ago

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 commented 5 months ago

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

kape1395 commented 5 months ago

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 commented 5 months ago

@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 commented 5 months ago

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 commented 5 months ago

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 commented 5 months ago

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

kape1395 commented 5 months ago

@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 commented 5 months ago

@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 commented 5 months ago

@muenchnerkindl, it works much better now!

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

kape1395 commented 5 months ago

@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:

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 commented 5 months ago

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 commented 5 months ago

@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 commented 4 months ago

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

muenchnerkindl commented 4 months ago

@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 commented 4 months ago

@muenchnerkindl, thanks for reviewing the changes!

I believe the signoff/DCO is missing for your commit: https://github.com/tlaplus/tlapm/pull/124/commits/d5d8dbf38a7e2cbe3c78309af375af61ec37935a. 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 commented 4 months ago

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.