Trinh Le Khanh (Nov 16 2020 at 16:32): 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?
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 ?x1is 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
≡ 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: Apr 25 2024 at 04:18 UTC