Hello everyone,
I'm working in the field of software verification and try to use Isabelle to prove the equivalence between two formulas. I tried three lemmas and have some questions as follows:
lemma test1: "(P 0 ⟶ ~P 1) ∧ (P 1 ⟶ ~P 0) ⟹ ~P 0∨~P 1"
apply(auto)
done
It worked perfectly as I want.
lemma test2: "(P 0 --> (~P 1 & ~P 2)) & (P 1 --> (~P 0 & ~P 2)) & (P 2 --> (~P 1 & ~P 0))
==> ((~P 1 & ~P 2) | (~P 0 & ~P 2) | (~P 1 & ~P 0))"
apply(auto)
done
When I added one more predicate "P 2", it run until out of memory. I don't think that the lemma is big enough unprovable like this.
lemma test3: "⋀i∈I.(P i ⟶ (⋀j∈I-{i}. ¬P j)) ⟹ ⋁i∈I.(⋀j∈I-{i}. ¬P j)"
apply (auto)
done
I tested a generic case and the Isabelle showed that "Failed to apply proof method". I tried to add "apply (induction)" and the result is "Failed to finish proof". So I guess the problem is about applying the right proof method, right? Then, I tried some other like "simp" or "rules" but they didn't work.
P.s: the symbol "bigvee" and "bigwedge" are redefined as follows (@Mathias Fleury re-defined it)
Screenshot-2020-10-16-at-12.13.52.png
Could you explain those questions, please? Thank you very much.
As for 2, auto
is not always the best way to go. In this particular case, it seems that the simplifier loops (no idea why). More specialised methods for logic/set theory like blast
and metis
and smt
solve this almost instantly. There are also more obscure ones (argo
, sat
, satx
) that do a good job here.
As for the bigvee thing, please post the actual source could and not just a screenshot. It's a lot of text to copy from a screenshot by hand. I don't really understand what the advantage of bigvee
and bigwedge
are over Bex
and Ball
, i.e. ∃x∈A. P x
instead of ⋁x∈A. P x
.
Zulip uses markdown as markup so you can use triple backticks for code like this:
f x = x
Also, I don't think 3 holds if I
is the empty set. The following can easily be proven by blast:
∀i∈I. P i ⟶ (∀j∈I-{i}. ¬P j) ⟹ I ≠ {} ⟹ ∃i∈I. ∀j∈I-{i}. ¬P j
This is the source code:
theory test1
imports Main
begin
context comm_monoid_add (*commutative monoid with addition*)
begin
sublocale bigvee: comm_monoid_set HOL.disj False
defines bigvee = bigvee.F and bigvee' = bigvee.G
by standard auto
abbreviation bigvee'' :: ‹bool set ⇒ bool› ("⋁")
where "⋁ ≡ bigvee (λx. x)"
sublocale bigwedge: comm_monoid_set HOL.conj True
defines bigwedge = bigwedge.F and bigwedge' = bigwedge.G
by standard auto
abbreviation bigwedge'' :: ‹bool set ⇒ bool› ("⋀")
where "⋀ ≡ bigwedge (λx. x)"
end
syntax (*Define pattern of bigwedge and bigvee*)
"_bigwedge" :: "pttrn ⇒ 'a set ⇒ 'b ⇒ 'b::comm_monoid_add" ("(2⋀(_/∈_)./ _)" [0, 51, 10] 10)
translations ― ‹Beware of argument permutation!›
"⋀i∈A. b" ⇌ "CONST bigwedge (λi. b) A"
syntax
"_bigvee" :: "pttrn ⇒ 'a set ⇒ 'b ⇒ 'b::comm_monoid_add" ("(2⋁(_/∈_)./ _)" [0, 51, 10] 10)
translations ― ‹Beware of argument permutation!› (*translation between parse rules or print rules*)
"⋁i∈A. b" ⇌ "CONST bigvee (λi. b) A"
(*CONST ensures that the given identifier is treated as constant term*)
instantiation bool :: comm_monoid_add
begin
definition zero_bool where
[simp]: ‹zero_bool = False›
definition plus_bool where
[simp]: ‹plus_bool = (∨)›
instance
by standard auto
end
thm bigvee_def
thm bigwedge_def
(*meaningful name*)
definition J :: "nat set" where
"J = {n . n > 0}"
definition U :: "nat set" where
"U = {n . n > 0}"
definition T :: "nat set" where
"T = {n . n > 0}"
definition I :: "nat set" where
"I = {n . n > 0}"
definition V :: "nat set" where
"V = {n . n > 0}"
definition K :: "nat set" where
"K = {n . n > 0}"
definition H :: "nat set" where
"H = {n . n > 0}"
definition L :: "nat set" where
"L = {n . n > 0}"
definition B :: "nat set" where
"B = {1, 2, 3, 4}"
lemma ‹finite A ⟹ (⋁i∈A. f i) ⟷ (∃i ∈ A. f i)›
apply (induction rule: finite_induct)
apply (auto simp: )
done
lemma ‹finite A ⟹ (⋀i∈A. f i) ⟷ A = {} ∨ (∀i ∈ A. f i)›
apply (induction rule: finite_induct)
apply (auto simp: )
done
lemma ‹infinite A ⟹ (⋀i∈A. f i) ⟷ True›
by auto
lemma test0:
‹(⋀j∈J. ⋀u∈U. ⋀t∈T. ⋀l∈L. ⋀l⇩1∈L-{l}. ¬P j u t l⇩1) ∨
(⋁i∈I. ⋁v∈V. ⋀k∈K. ⋁h∈H. Q i v k h) ⟹
(⋁i∈I. ⋁v∈V. ⋀k∈K. ⋁h∈H. Q i v k h) ∨ (⋀j∈J. ⋀u∈U. ⋀t∈T. ⋀l⇩1∈-{l}. ¬P j u t l⇩1)›
apply auto
done
lemma "∀ x. P x ⟶ P x"
apply (auto)
done
lemma test1: "(P 0 ⟶ ~P 1) ∧ (P 1 ⟶ ~P 0) ⟹ ~P 0∨~P 1"
apply(auto)
done
(*
lemma test2: "(P 0 --> (~P 1 & ~P 2)) & (P 1 --> (~P 0 & ~P 2)) & (P 2 --> (~P 1 & ~P 0))
==> ((~P 1 & ~P 2) | (~P 0 & ~P 2) | (~P 1 & ~P 0))"
apply(auto)
done *)
lemma test3: "⋀i∈I.(P i ⟶ (⋀j∈I-{i}. ¬P j)) ⟹ ⋁i∈I.(⋀j∈I-{i}. ¬P j)"
apply (induction)
apply (auto)
done
If you want to do induction, you should specify what you want to do induction over.
I defined the set B with 4 elements and used it but the 3rd lemma returned the same result.
Also note that bigwedge
over an infinite set is always true and bigvee
over an infinite set is always false. So 3 is trivially false because I
is infinite.
I think you really want to use ∀x∈I
etc.
then you don't need induction either, it's straightforward set theory and blast
can do it (as long as you feed in the fact that I ≠ {}
).
So if I have
I = {1, 2, 3, 4}
I can use this directly, right?
∀i∈I.⋀P i = P 1 ∧ P 2 ∧ P 3 ∧ P 4
∀i∈I.⋁P i = P 1 ∨ P 2 ∨ P 3 ∨ P 4
You probably mean
(∀i∈I. P i) = P 1 ∧ P 2 ∧ P 3 ∧ P 4
(∃i∈I. P i) = P 1 ∨ P 2 ∨ P 3 ∨ P 4
right?
In that case: Yes. You just have to unfold the definition of I
and then it simplifies to that.
(deleted)
Manuel Eberl said:
Also, I don't think 3 holds if
I
is the empty set. The following can easily be proven by blast:∀i∈I. P i ⟶ (∀j∈I-{i}. ¬P j) ⟹ I ≠ {} ⟹ ∃i∈I. ∀j∈I-{i}. ¬P j
Thank you. I tried this with blast
and it worked.
I also tried that:
definition I :: "nat set" where
"I = {1, 2, 3, 4}"
I ≠ {}
lemma test3: "∀i∈I. P i ⟶ (∀j∈I-{i}. ¬P j) ⟹ ∃i∈I. ∀j∈I-{i}. ¬P j"
apply (blast)
done
It's failed to prove. So I ≠ {}
seems mandatory despite we define set I or not, right?
blast
doesn't know how you defined the set. You can e.g. unfold the definition like this:
lemma test3: "∀i∈I. P i ⟶ (∀j∈I-{i}. ¬P j) ⟹ ∃i∈I. ∀j∈I-{i}. ¬P j"
unfolding I_def by blast
Or you can prove that I
is nonempty first and then supply that fact to blast:
lemma I_not_empty: "I ≠ {}"
by (auto simp: I_def)
lemma test3: "∀i∈I. P i ⟶ (∀j∈I-{i}. ¬P j) ⟹ ∃i∈I. ∀j∈I-{i}. ¬P j"
using I_not_empty by blast
Wow, that's awesome. Thank you very much.
If you want to learn Isabelle systematically, I suggest you work through the first half of the ‘Concrete Semantics’ books. It's online for free: http://www.concrete-semantics.org/
Thank you for your suggestion. After putting my lemma and choosing to prove them using metis
, the metis
is highlighted in purple (and my computer's fans are running so hard). Do you know the meaning of this color? (I just know that red for error). Screenshot-2020-10-16-at-14.19.08.png
It means that the command is still running. Metis might not be good enough to do something this big. Other methods might be. If you paste the full example in here, I can have a look at it.
Here you are. I tried blast first but it couldn't prove. Thus, I changed to metis.
theory MyMaths
imports Main
begin
definition xor :: "bool ⇒ bool ⇒ bool" where
"xor A B ≡ (A & ~B) | (~A & B)"
definition J :: "nat set" where
"J = {n . n > 0}"
definition U :: "nat set" where
"U = {n . n > 0}"
definition T :: "nat set" where
"T = {n . n > 0}"
definition I :: "nat set" where
"I = {n . n > 0}"
definition V :: "nat set" where
"V = {n . n > 0}"
definition K :: "nat set" where
"K = {n . n > 0}"
definition H :: "nat set" where
"H = {n . n > 0}"
definition L :: "nat set" where
"L = {n . n > 0}"
lemma "((∀l∈L.∀j∈J.∀u∈U.∀t∈T. ¬P j u t l) ∨ (∃h∈H.∃i∈I.∃v∈V.∀k∈K. (Q i v k h ∧ (∀h⇩1∈H-{h}. ¬Q i v k h⇩1))))
∧ (∃l∈L.∃h∈H.((∀j∈J.∀u∈U.∀t∈T.∀l⇩1∈L-{l}. ¬P j u t l⇩1) ∧ (∃i∈I.∃v∈V.∀k∈K.∀h⇩1∈H-{h}. ¬Q i v k h⇩1)))
⟹ (∃h∈H.((∀l∈L.∀j∈J.∀u∈U.∀t∈T. ¬P j u t l) ∧ (∀i∈I.∀v∈V.∀k∈K.∀h⇩1∈H-{h}.¬Q i v k h⇩1)))
∨ (∃l∈L.∃h∈H.(∀j∈J.∀u∈U.∀t∈T.∀l⇩1∈L-{l}. ¬P j u t l⇩1) ∧ (∃i∈I.∃v∈V.∀k∈K.(Q i v k h ∧ (∀h⇩1∈H-{h}. ¬Q i v k h⇩1))))"
unfolding I_def and V_def and K_def and H_def and J_def and U_def and T_def and L_def
using [[simp_trace]]
by metis
end
Okay, now you're back to infinite sets again. That means things like SAT solvers cannot be used. The definitions of your sets don't really make the problem any easier either, so I don't think unfolding helps.
Normally, I would say to tackle something like this with an SMT solver like Z3 or CVC4, but it seems this is too difficult for them.
(then again, I am not sure if this holds in the first place)
For two particular values of P
and Q
, I was able to prove the negation of your goal, so apparently it doesn't hold:
definition "P = (λa b c d. False)"
definition "Q = (λa b c d. a ≠ 1 ∧ (b = 1 ∧ c = 1 ∧ d = 1 ∨ b ≠ 1 ∧ c = 1 ∧ d ≠ 1))"
lemma "¬(((∀l∈L.∀j∈J.∀u∈U.∀t∈T. ¬P j u t l) ∨ (∃h∈H.∃i∈I.∃v∈V.∀k∈K. (Q i v k h ∧ (∀h⇩1∈H-{h}. ¬Q i v k h⇩1))))
∧ (∃l∈L.∃h∈H.((∀j∈J.∀u∈U.∀t∈T.∀l⇩1∈L-{l}. ¬P j u t l⇩1) ∧ (∃i∈I.∃v∈V.∀k∈K.∀h⇩1∈H-{h}. ¬Q i v k h⇩1)))
⟶ (∃h∈H.((∀l∈L.∀j∈J.∀u∈U.∀t∈T. ¬P j u t l) ∧ (∀i∈I.∀v∈V.∀k∈K.∀h⇩1∈H-{h}.¬Q i v k h⇩1)))
∨ (∃l∈L.∃h∈H.(∀j∈J.∀u∈U.∀t∈T.∀l⇩1∈L-{l}. ¬P j u t l⇩1) ∧ (∃i∈I.∃v∈V.∀k∈K.(Q i v k h ∧ (∀h⇩1∈H-{h}. ¬Q i v k h⇩1)))))"
unfolding I_def and V_def and K_def and H_def and J_def and U_def and T_def and L_def P_def Q_def
apply auto
apply (rule exI[of _ 2])
apply auto
subgoal for h
apply (rule bexI[of _ "h + 2"])
apply auto
done
The proof isn't pretty, but it gets the point across. I found that particular counterexample for P
and Q
using the nitpick
command.
I might make something wrong when typing the formulas. I'll check it again.
To make sure that they're not infinite sets. I re-defined as follows (each set has 99 elements):
definition J :: "nat set" where
"J = {n . n < 100}"
definition U :: "nat set" where
"U = {n . n < 100}"
definition T :: "nat set" where
"T = {n . n < 100}"
definition I :: "nat set" where
"I = {n . n < 100}"
definition V :: "nat set" where
"V = {n . n < 100}"
definition K :: "nat set" where
"K = {n . n < 100}"
definition H :: "nat set" where
"H = {n . n < 100}"
definition L :: "nat set" where
"L = {n . n < 100}"
Nope.
definition J :: "nat set" where
"J = {n . n < 100}"
definition U :: "nat set" where
"U = {n . n < 100}"
definition T :: "nat set" where
"T = {n . n < 100}"
definition I :: "nat set" where
"I = {n . n < 100}"
definition V :: "nat set" where
"V = {n . n < 100}"
definition K :: "nat set" where
"K = {n . n < 100}"
definition H :: "nat set" where
"H = {n . n < 100}"
definition L :: "nat set" where
"L = {n . n < 100}"
definition "P = (λa b c d. False)"
definition "Q = (λa b c d. a ≠ 1 ∧ (b = 1 ∧ c = 1 ∧ d = 1 ∨ b ≠ 1 ∧ c = 1 ∧ d ≠ 1))"
lemma *: "(∃x∈A - B. R x) ⟷ (∃x. x ∈ A ∧ x ∉ B ∧ R x)"
"(∀x∈A - B. R x) ⟷ (∀x. x ∉ A ∨ x ∈ B ∨ R x)"
by auto
lemma "¬(((∀l∈L.∀j∈J.∀u∈U.∀t∈T. ¬P j u t l) ∨ (∃h∈H.∃i∈I.∃v∈V.∀k∈K. (Q i v k h ∧ (∀h⇩1∈H-{h}. ¬Q i v k h⇩1))))
∧ (∃l∈L.∃h∈H.((∀j∈J.∀u∈U.∀t∈T.∀l⇩1∈L-{l}. ¬P j u t l⇩1) ∧ (∃i∈I.∃v∈V.∀k∈K.∀h⇩1∈H-{h}. ¬Q i v k h⇩1)))
⟶ (∃h∈H.((∀l∈L.∀j∈J.∀u∈U.∀t∈T. ¬P j u t l) ∧ (∀i∈I.∀v∈V.∀k∈K.∀h⇩1∈H-{h}.¬Q i v k h⇩1)))
∨ (∃l∈L.∃h∈H.(∀j∈J.∀u∈U.∀t∈T.∀l⇩1∈L-{l}. ¬P j u t l⇩1) ∧ (∃i∈I.∃v∈V.∀k∈K.(Q i v k h ∧ (∀h⇩1∈H-{h}. ¬Q i v k h⇩1)))))"
unfolding I_def and V_def and K_def and H_def and J_def and U_def and T_def and L_def P_def Q_def
apply (auto simp: *)
apply presburger+
done
(presburger
is a decision procedure for Presburger logic, i.e. linear arithmetic on integers plus quantifiers. It has pretty terrible performance, but in this case, it works pretty well.)
Can you explain why did you define P and Q like this?
definition "P = (λa b c d. False)"
definition "Q = (λa b c d. a ≠ 1 ∧ (b = 1 ∧ c = 1 ∧ d = 1 ∨ b ≠ 1 ∧ c = 1 ∧ d ≠ 1))"
Because it leads to a counterexample?
The way you stated your lemma, P
and Q
were free variables, i.e. you claimed that it holds for all values of P
and Q
. I showed that there are two particular values for which it does not hold.
But when you applied presburger+, it's solved, right?
Ah, when I remove your definition of P and Q, it's unsolvable.
I proved the negation of your lemma.
If we call the statement of your lemma foo(P,Q)
, you essentially claimed ∀P Q. foo(P,Q)
. I showed ∃P Q. ¬foo(P,Q)
.
Yes, I see. So the problem is the correctness of my lemma, not the definition.
The proof isn't pretty, but it gets the point across. I found that particular counterexample for P and Q using the
nitpick
command.
Hi Manuel, how can you generate the definition of P and Q using the nitpick
command? When I used this command, it showed hundreds of lines like this Screenshot-2020-10-19-at-01.36.04.png
I did it for the variant with {n. n > 0}
. Or rather, I think I even did it for the variant where all the sets where UNIV
(which I think should be equivalent).
I set up the variant with {n. n>0}
and the result is shown as follows:
Screenshot-2020-10-19-at-13.43.18.png
Screenshot-2020-10-19-at-13.43.48.png
How did you generate the definition of P and Q from them?
definition "P = (λa b c d. False)"
definition "Q = (λa b c d. a ≠ 1 ∧ (b = 1 ∧ c = 1 ∧ d = 1 ∨ b ≠ 1 ∧ c = 1 ∧ d ≠ 1))"
This is perhaps a bit tricky to read. If you look at the first one, you see that it's a predicate P a b c d that is defined to be false for all a, b, c, d ≤ 2 and unspecified everywhere else. So I went ahead and just defined it to be false everywhere.
For Q you just have to see for which combinations of the values 0,1,2 for a,b,c,d it is true and then write down a definition that does exactly that
Thank you :D. I have another question is that I'm testing my formulas with a small case. My code to setup is:
theory prog_2
imports Main
begin
(*P*)
definition J :: "nat set" where
"J = {0}"
definition U :: "nat set" where
"U = {0}"
definition T :: "nat set" where
"T = {0}"
definition L :: "nat set" where
"L = {0, 1}"
(*Q*)
definition I :: "nat set" where
"I = {0, 1}"
definition V :: "nat set" where
"V = {0}"
definition K :: "nat set" where
"K = {0}"
definition H :: "nat set" where
"H = {0, 1}"
(*test*)
value "∃l∈L.∃h∈H.(∀j∈J.∀u∈U.(∀t∈T. P j u t l ⟶ (∃i∈I.∃v∈V.∀k∈K. Q i v k h)))"
end
The result is:
(P 0 0 0 0 ⟶ Q 0 0 0 0 ∨ Q 1 0 0 0)
∨ (P 0 0 0 0 ⟶ Q 0 0 0 1 ∨ Q 1 0 0 1)
∨ (P 0 0 0 1 ⟶ Q 0 0 0 0 ∨ Q 1 0 0 0)
∨ (P 0 0 0 1 ⟶ Q 0 0 0 1 ∨ Q 1 0 0 1)
But my expected output is:
(P 0 0 0 0 ⟶ Q 0 0 0 0 ∨ Q 1 0 0 0)
∨ (P 0 0 0 0 ⟶ Q 0 0 0 0 ∨ Q 1 0 0 1)
∨ (P 0 0 0 0 ⟶ Q 0 0 0 1 ∨ Q 1 0 0 0)
∨ (P 0 0 0 0 ⟶ Q 0 0 0 1 ∨ Q 1 0 0 1)
∨ (P 0 0 0 1 ⟶ Q 0 0 0 0 ∨ Q 1 0 0 0)
∨ (P 0 0 0 1 ⟶ Q 0 0 0 0 ∨ Q 1 0 0 1)
∨ (P 0 0 0 1 ⟶ Q 0 0 0 1 ∨ Q 1 0 0 0)
∨ (P 0 0 0 1 ⟶ Q 0 0 0 1 ∨ Q 1 0 0 1)
I know that because I put ∃h∈H
out of the first open bracket, so the result has the same value at the h
position. I tried to move ∃h∈H
inside or use another variable like h1 but the result is not what I expected. Do you have any suggestion?
My solution is that I added the formula for the different h
like this
value "∃l∈L.∃h∈H.(∀j∈J.∀u∈U.(∀t∈T. P j u t l ⟶ (∃i∈I.∃v∈V.∀k∈K.∃h1∈H-{h}. Q i v k h1))
∨ (∀t∈T. P j u t l ⟶ (∃i∈I.∃v∈V.∀k∈K. Q i v k h)))"
It works. It seems not the smart way, though.
UPDATE: It DOESN'T works. It duplicated the result :D
I think that you are confusing $\forall \exists$ and $\exists\forall$. You version is equivalent to putting the $\exists$ inside the implication symbol:
lemma "(∃l∈L. (∀j∈J. ∀u∈U. (∀t∈T. (P j u t l ⟶ (∃h∈H. ∃i∈I.∃v∈V.∀k∈K. Q i v k h))))) ⟷
(∃l∈L.∃h∈H.(∀j∈J.∀u∈U.(∀t∈T. P j u t l ⟶ (∃i∈I.∃v∈V.∀k∈K.∃h1∈H-{h}. Q i v k h1))
∨ (∀t∈T. P j u t l ⟶ (∃i∈I.∃v∈V.∀k∈K. Q i v k h))))"
unfolding L_def I_def J_def V_def H_def T_def K_def
apply auto
done
I think that you are confusing \forall \exists∀∃ and \exists\forall∃∀. You version is equivalent to putting the \exists∃ inside the implication symbol
Thank you. I know that but this is a small piece of my code. I need something like
((P 0 0 0 0 ⟶ Q 0 0 0 0 ∨ Q 1 0 0 0) ∧ ¬(all the others))
∨ ((P 0 0 0 0 ⟶ Q 0 0 0 1 ∨ Q 1 0 0 1) ∧ ¬(all the others))
∨ ((P 0 0 0 0 ⟶ Q 0 0 0 0 ∨ Q 1 0 0 1) ∧ ¬(all the others))
∨ ((P 0 0 0 0 ⟶ Q 0 0 0 1 ∨ Q 1 0 0 0) ∧ ¬(all the others))
So if I put the \exists inside, it looks like:
((P 0 0 0 0 ⟶ (Q 0 0 0 0 ∨ Q 1 0 0 0) ∨ Q 0 0 0 1 ∨ Q 1 0 0 1) ∧ ¬(all the others))
The two things are different.
Last updated: Sep 11 2024 at 16:22 UTC