## Stream: Beginner Questions

### Topic: lemma cannot prove my formula

#### 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 = "

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?

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

#### 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?

#### Mathias Fleury (Nov 23 2020 at 05:49):

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

#### 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
``````

#### Mathias Fleury (Nov 23 2020 at 09:08):

`≡` is equal on the Pure level, not implication.

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

#### Trinh Le Khanh (Nov 23 2020 at 09:13):

I'm clear. Thank you for your explanation.

#### Trinh Le Khanh (Nov 23 2020 at 09:54):

(deleted)

Last updated: Aug 13 2022 at 05:18 UTC