Stream: Beginner Questions

Topic: Proof methods for software verification


view this post on Zulip Trinh Le Khanh (Oct 16 2020 at 10:15):

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:

  1. lemma test1: "(P 0 ⟶ ~P 1) ∧ (P 1 ⟶ ~P 0) ⟹ ~P 0∨~P 1"
    apply(auto)
    done
    It worked perfectly as I want.

  2. 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.

  3. 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.

view this post on Zulip Manuel Eberl (Oct 16 2020 at 10:29):

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.

view this post on Zulip Lukas Stevens (Oct 16 2020 at 10:32):

Zulip uses markdown as markup so you can use triple backticks for code like this:

f x = x

view this post on Zulip Manuel Eberl (Oct 16 2020 at 10:33):

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

view this post on Zulip Trinh Le Khanh (Oct 16 2020 at 10:33):

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

view this post on Zulip Manuel Eberl (Oct 16 2020 at 10:34):

If you want to do induction, you should specify what you want to do induction over.

view this post on Zulip Trinh Le Khanh (Oct 16 2020 at 10:35):

I defined the set B with 4 elements and used it but the 3rd lemma returned the same result.

view this post on Zulip Manuel Eberl (Oct 16 2020 at 10:38):

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.

view this post on Zulip Manuel Eberl (Oct 16 2020 at 10:38):

I think you really want to use ∀x∈I etc.

view this post on Zulip Manuel Eberl (Oct 16 2020 at 10:39):

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 ≠ {}).

view this post on Zulip Trinh Le Khanh (Oct 16 2020 at 10:44):

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

view this post on Zulip Manuel Eberl (Oct 16 2020 at 11:05):

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.

view this post on Zulip Trinh Le Khanh (Oct 16 2020 at 11:18):

(deleted)

view this post on Zulip Trinh Le Khanh (Oct 16 2020 at 11:31):

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:

  1. I define set I = {1, 2, 3, 4}
definition I :: "nat set" where
  "I = {1, 2, 3, 4}"
  1. Then, I write the lemma but remove the part 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?

view this post on Zulip Manuel Eberl (Oct 16 2020 at 11:47):

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

view this post on Zulip Trinh Le Khanh (Oct 16 2020 at 11:58):

Wow, that's awesome. Thank you very much.

view this post on Zulip Manuel Eberl (Oct 16 2020 at 12:17):

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/

view this post on Zulip Trinh Le Khanh (Oct 16 2020 at 12:24):

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

view this post on Zulip Manuel Eberl (Oct 16 2020 at 12:32):

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.

view this post on Zulip Trinh Le Khanh (Oct 16 2020 at 12:36):

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

view this post on Zulip Manuel Eberl (Oct 16 2020 at 14:12):

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.

view this post on Zulip Manuel Eberl (Oct 16 2020 at 14:16):

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.

view this post on Zulip Manuel Eberl (Oct 16 2020 at 14:16):

(then again, I am not sure if this holds in the first place)

view this post on Zulip Manuel Eberl (Oct 16 2020 at 14:28):

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.

view this post on Zulip Trinh Le Khanh (Oct 16 2020 at 14:44):

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}"

view this post on Zulip Manuel Eberl (Oct 16 2020 at 14:51):

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

view this post on Zulip Manuel Eberl (Oct 16 2020 at 14:52):

(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.)

view this post on Zulip Trinh Le Khanh (Oct 16 2020 at 15:10):

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))"

view this post on Zulip Manuel Eberl (Oct 16 2020 at 15:10):

Because it leads to a counterexample?

view this post on Zulip Manuel Eberl (Oct 16 2020 at 15:11):

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.

view this post on Zulip Trinh Le Khanh (Oct 16 2020 at 15:12):

But when you applied presburger+, it's solved, right?

view this post on Zulip Trinh Le Khanh (Oct 16 2020 at 15:14):

Ah, when I remove your definition of P and Q, it's unsolvable.

view this post on Zulip Manuel Eberl (Oct 16 2020 at 15:14):

I proved the negation of your lemma.

view this post on Zulip Manuel Eberl (Oct 16 2020 at 15:15):

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).

view this post on Zulip Trinh Le Khanh (Oct 16 2020 at 15:16):

Yes, I see. So the problem is the correctness of my lemma, not the definition.

view this post on Zulip Trinh Le Khanh (Oct 18 2020 at 23:37):

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

view this post on Zulip Manuel Eberl (Oct 19 2020 at 07:23):

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).

view this post on Zulip Trinh Le Khanh (Oct 19 2020 at 11:45):

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))"

view this post on Zulip Manuel Eberl (Oct 19 2020 at 15:19):

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.

view this post on Zulip Manuel Eberl (Oct 19 2020 at 15:19):

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

view this post on Zulip Trinh Le Khanh (Oct 19 2020 at 21:52):

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?

view this post on Zulip Trinh Le Khanh (Oct 20 2020 at 08:46):

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

view this post on Zulip Mathias Fleury (Oct 20 2020 at 08:56):

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

view this post on Zulip Trinh Le Khanh (Oct 20 2020 at 09:29):

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: Aug 13 2022 at 05:18 UTC