Stream: Beginner Questions

Topic: lemma cannot prove my formula


view this post on Zulip Trinh Le Khanh (Nov 16 2020 at 16:32):

Hi everybody,

I defined basic for my proving as follows:

(*----------set up Type and Instances------------*)
definition TypeTrig :: "nat list" (*port types*)
  where "TypeTrig = [0, 1]"

definition IncTrig :: "nat set list" (*port instances of each port type IncTrig*)
  where "IncTrig = [{10, 14}, {11,12,13}]"

definition TypeSync :: "nat list" (*port types*)
  where "TypeSync = [0]"

definition IncSync :: "nat set list" (*port instances of each port type IncTrig*)
  where "IncSync = [{5,6}]"

(*----------funcs for mapping and searching between types and instances------------*)
fun pair_ns :: "nat ⇒ nat list ⇒ (nat * nat) list" where
"pair_ns x [] = []" |
"pair_ns x (y # ys) = [(x,y)] @ (pair_ns x ys)"

fun pair_mapping :: "nat list ⇒ nat set list ⇒ (nat * nat) list" where
"pair_mapping [] [] = []" |
"pair_mapping (x # xs) [] = []" |
"pair_mapping [] (y # ys)  = []" |
"pair_mapping (x # xs) (y # ys) = pair_ns x (sorted_list_of_set y) @ pair_mapping xs ys "

fun pair_mapping_lists :: "nat list ⇒ nat set list ⇒ (nat * nat) list list" where
"pair_mapping_lists [] [] = []" |
"pair_mapping_lists (x # xs) [] = []" |
"pair_mapping_lists [] (y # ys)  = []" |
"pair_mapping_lists (x # xs) (y # ys) = [pair_ns x (sorted_list_of_set y)] @ pair_mapping_lists xs ys "

fun lookup :: "'k ⇒ ('k × 'v) list ⇒ 'v list" where
"lookup k [] = []" |
"lookup k (x#xs) = (if fst x = k then [(snd x)]@lookup k (xs) else lookup k xs)"

value "pair_mapping TypeTrig IncTrig"
value "pair_mapping_lists TypeTrig IncTrig"
value "length (pair_mapping_lists TypeTrig IncTrig)"
value "nth (pair_mapping_lists TypeTrig IncTrig) 0"
value "hd (pair_mapping_lists TypeTrig IncTrig)"

(*---------product functions for creating alphaSet and betaSet------------*)
fun product_2lists :: "'a list => 'a list => 'a list list" where
"product_2lists [] ys = []" |
"product_2lists xs [] = []" |
"product_2lists (x#xs) (y#ys) = [x # y # []] @ product_2lists xs (y#ys) @ product_2lists (x#[]) ys"

fun insert_list :: "'a => 'a list list => 'a list list" where
"insert_list x [] = []" |
"insert_list x (y#ys) = [List.insert x y] @ insert_list x (tl (y#ys))"

value "insert_list 3 [[1::nat,2], [4,5]]"

fun product_l2ll :: "'a list => 'a list list => 'a list list" where
"product_l2ll [] ys = []" |
"product_l2ll xs [] = []" |
"product_l2ll (x#xs) (ys) = insert_list x ys @ product_l2ll xs ys"

fun product_inListList :: "'a list list => 'a list list" where
"product_inListList [] = []" |
"product_inListList (x#[]) = (x#[])" |
"product_inListList (x#y#[]) = product_2lists x y" |
"product_inListList (x#ys) = product_l2ll x (product_inListList (ys))"

value "pair_mapping_lists TypeTrig IncTrig"
value "product_inListList (pair_mapping_lists TypeTrig IncTrig)"

definition betaSet :: "(nat*nat) list set" where
"betaSet = set (product_inListList (pair_mapping_lists TypeTrig IncTrig))"

definition alphaSet :: "(nat*nat) list set" where
"alphaSet = set (product_inListList (pair_mapping_lists TypeSync IncSync))"

definition trigInSet_of :: "nat ⇒ nat set" where
"trigInSet_of k = (if k ∈ (set TypeTrig) then set (lookup k (pair_mapping TypeTrig IncTrig)) else {})"

definition syncInSet_of :: "nat ⇒ nat set" where
"syncInSet_of t = (if t ∈ (set TypeSync) then set (lookup t (pair_mapping TypeSync IncSync)) else {})"

Then, I tried to prove this lemma:

lemma "∀bet∈betaSet.∀k∈(set TypeTrig). P k (hd (lookup k bet))
        ⟶ (∀h1∈(trigInSet_of k)-{(hd (lookup k bet))}.¬P k h1)
⟹ (∃bet∈betaSet.∀k∈(set TypeTrig).∀h1∈(trigInSet_of k)-{(hd (lookup k bet))}.¬P k h1)"
  unfolding betaSet_def TypeTrig_def IncTrig_def trigInSet_of_def
  apply auto
  done

But Isabelle keeps running forever at apply auto. I thought that because Isabelle doesn't calculate that lookup k bet always returns 1 value. So I added a lemma:

lemma lookup_length: "∀bet∈betaSet.∀k∈(set TypeTrig). (length (lookup k bet) = 1)"
  unfolding betaSet_def TypeTrig_def IncTrig_def
  apply auto
  done

lemma "∀bet∈betaSet.∀k∈(set TypeTrig). P k (hd (lookup k bet))
        ⟶ (∀h1∈(trigInSet_of k)-{(hd (lookup k bet))}.¬P k h1)
⟹ (∃bet∈betaSet.∀k∈(set TypeTrig).∀h1∈(trigInSet_of k)-{(hd (lookup k bet))}.¬P k h1)"
  unfolding betaSet_def TypeTrig_def IncTrig_def trigInSet_of_def
  using lookup_length
  apply auto
  done

The lookup_length is ok but the latter is still unprovable.
Then, I calculated each formula using value and wrote another lemma to prove the result from them:

value "∀bet∈betaSet.∀k∈(set TypeTrig).∀h∈(set (lookup k bet)). P k (hd (lookup k bet))
⟶ (∀h1∈(trigInSet_of k)-{(hd (lookup k bet))}.¬P k h1)"

value "(∃bet∈betaSet.∀k∈(set TypeTrig).∀h1∈(trigInSet_of k)-{(hd (lookup k bet))}.¬P k h1)"

lemma "(¬ P 0 14 ∧ ¬ P 1 12 ∧ ¬ P 1 13 ∨
 ¬ P 0 10 ∧ ¬ P 1 12 ∧ ¬ P 1 13 ∨
 ¬ P 0 10 ∧ ¬ P 1 11 ∧ ¬ P 1 13 ∨
 ¬ P 0 10 ∧ ¬ P 1 11 ∧ ¬ P 1 12 ∨ ¬ P 0 14 ∧ ¬ P 1 11 ∧ ¬ P 1 13 ∨ ¬ P 0 14 ∧ ¬ P 1 11 ∧ ¬ P 1 12)
⟹ (((P 0 10 ⟶ ¬ P 0 14) ∧ (P 1 11 ⟶ ¬ P 1 12 ∧ ¬ P 1 13)) ∧
 ((P 0 14 ⟶ ¬ P 0 10) ∧ (P 1 11 ⟶ ¬ P 1 12 ∧ ¬ P 1 13)) ∧
 ((P 0 14 ⟶ ¬ P 0 10) ∧ (P 1 12 ⟶ ¬ P 1 11 ∧ ¬ P 1 13)) ∧
 ((P 0 14 ⟶ ¬ P 0 10) ∧ (P 1 13 ⟶ ¬ P 1 11 ∧ ¬ P 1 12)) ∧
 ((P 0 10 ⟶ ¬ P 0 14) ∧ (P 1 12 ⟶ ¬ P 1 11 ∧ ¬ P 1 13)) ∧
 (P 0 10 ⟶ ¬ P 0 14) ∧ (P 1 13 ⟶ ¬ P 1 11 ∧ ¬ P 1 12))"
  apply auto
  done

It worked. Could you explain why Isabelle cannot prove my first formula, please?

view this post on Zulip Mathias Fleury (Nov 17 2020 at 06:09):

Tracing the simplifier shows that simp is already looping, but it is not immediately clear to me why (P 0 14 ⟹ ?x1 ∈ {10, 14} - {14} ⟹ P 0 ?x1 is generated and repeatedly rewritten, whatever the reason).

view this post on Zulip Trinh Le Khanh (Nov 23 2020 at 00:28):

Mathias Fleury said:

Tracing the simplifier shows that simp is already looping, but it is not immediately clear to me why (P 0 14 ⟹ ?x1 ∈ {10, 14} - {14} ⟹ P 0 ?x1 is generated and repeatedly rewritten, whatever the reason).

Hi Mathias,
What is the difference between and in lemma?
As I understand, is considered as imply (but P ⟹ Q ⟹ R means (P & Q) --> R
Meanwhile, is to present the equivalence between two formulas (e.g. P ≡ Q)
Is that right?
I tested these two lemmas and both of them are provable. I think in this case, and are the same

lemma: "∀x ∈ {0, 1}. P x ⟹ P 0 ∧ P 1"
  by auto
lemma: "∀x ∈ {0, 1}. P x ≡ P 0 ∧ P 1"
  by auto

Then, I tested a concrete example that is

lemma "((P 1 ⟶ ¬ P 2) ∧ (P 2 ⟶ ¬ P 1)) ⟹ (¬ P 1 ∨ ¬ P 2)"
by auto

It is provable.

lemma "((P 1 ⟶ ¬ P 2) ∧ (P 2 ⟶ ¬ P 1)) ≡ (¬ P 1 ∨ ¬ P 2)"
by auto

It's unprovable. However, if I use argo instead of auto, both of them are provable. Could you explain and confirm my understanding, please?

view this post on Zulip Mathias Fleury (Nov 23 2020 at 05:49):

Avoid unless you are programming a tool. It tends to confuse tactics like auto

view this post on Zulip Trinh Le Khanh (Nov 23 2020 at 08:39):

So is my understanding of them correct?
I asked this because when I used == instead of ==>, my lemma is provable. (This lemma aims to prove two formulas are equivalent)

lemma "∀bet∈betaSet.∀k∈(set TypeTrig). P k (hd (lookup k bet))
        ⟶ (∀h1∈(trigInSet_of k)-{(hd (lookup k bet))}.¬P k h1)
≡ (∃bet∈betaSet.∀k∈(set TypeTrig).∀h1∈(trigInSet_of k)-{(hd (lookup k bet))}.¬P k h1)"
  unfolding betaSet_def TypeTrig_def IncTrig_def trigInSet_of_def
  using [[simp_trace]]
  apply auto
  done

view this post on Zulip Mathias Fleury (Nov 23 2020 at 09:08):

is equal on the Pure level, not implication.

view this post on Zulip Mathias Fleury (Nov 23 2020 at 09:08):

I believe in your case it works because the LHS and the RHS are simplified separately, instead of being simplified together..

view this post on Zulip Trinh Le Khanh (Nov 23 2020 at 09:13):

I'm clear. Thank you for your explanation.

view this post on Zulip Trinh Le Khanh (Nov 23 2020 at 09:54):

(deleted)


Last updated: Aug 13 2022 at 05:18 UTC