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?

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

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?

Avoid `≡`

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

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

`≡`

is equal on the Pure level, not implication.

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

I'm clear. Thank you for your explanation.

(deleted)

Last updated: Jun 20 2024 at 08:21 UTC