Stream: Beginner Questions

Topic: Proving lemma with abstract lists

Trinh Le Khanh (Dec 28 2020 at 01:00):

Hello everyone,
I need to prove this lemma with abstract definitions of `t_betaSet`, `t_TrigInstance_1`, and `t_SyncInstance_1`. I firstly defined them by concrete values, then used abstract definitions. If I use a concrete definition, it's provable. Otherwise, it's unprovable. For detail, I present my process in the three below steps.

``````((∀t ∈ set t_SyncInstance_1. ∀l ∈ set (snd t). P (fst t) l ⟶ (∃alp ∈ set t_betaSet. (∃elm ∈ set alp. Q (fst elm) (snd elm)) ∧ (∀elm ∈ set alp.∀h ∈ set (lookup_1 (fst elm) t_TrigInstance_1) - {snd elm}. ¬Q (fst elm) h))) ∧ (∀pair ∈ set t_TrigInstance_1. ∀x ∈ set (snd pair). Q (fst pair) x ⟶ (∀y ∈ set (snd pair) - { x }. ¬ Q (fst pair) y)) ∧ (∀pair ∈ set t_SyncInstance_1. ∀x ∈ set (snd pair). P (fst pair) x ⟶ (∀y ∈ set (snd pair) - { x }. ¬ P (fst pair) y)))
⟹ (∃t ∈ set t_SyncInstance_1. ∃alp ∈ set t_betaSet.∃l ∈ set (snd t). P (fst t) l ⟶ ((∃elm ∈ set alp. Q (fst elm) (snd elm)) ∧ (∀elm ∈ set alp.∀h ∈ set (lookup_1 (fst elm) t_TrigInstance_1) - {snd elm}. ¬Q (fst elm) h) ∧ (∀l1 ∈ set (snd t) - {l}. ¬P (fst t) l1) ∧ (∀t1 ∈ set t_SyncInstance_1 - {t}.∀l2 ∈ set (snd t).¬P (fst t1) l2)))
``````
1. If I define all term like `t_betaSet`, `t_TrigInstance_1`, and `t_SyncInstance_1` by concrete values, the lemma is PROVABLE (I used sledgehammer):
``````definition t_betaSet :: "(nat * nat) list list" where
"t_betaSet = [[(5,7), (6,7)], [(5,7), (6,8)], [(5,8), (6,7)], [(5,8), (6,8)]]"

definition t_TrigInstance_1 :: "(nat * nat list) list" where
"t_TrigInstance_1 = [(5, [7, 8]), (6, [7, 8])]"

(*------*)
definition t_SyncInstance_1 :: "(nat * nat list) list" where
"t_SyncInstance_1 = [(0, [2,3])]"
(*------*)
lemma specific_proving: "((∀t ∈ set t_SyncInstance_1. ∀l ∈ set (snd t). P (fst t) l ⟶ (∃alp ∈ set t_betaSet. (∃elm ∈ set alp. Q (fst elm) (snd elm)) ∧ (∀elm ∈ set alp.∀h ∈ set (lookup_1 (fst elm) t_TrigInstance_1) - {snd elm}. ¬Q (fst elm) h))) ∧ (∀pair ∈ set t_TrigInstance_1. ∀x ∈ set (snd pair). Q (fst pair) x ⟶ (∀y ∈ set (snd pair) - { x }. ¬ Q (fst pair) y)) ∧ (∀pair ∈ set t_SyncInstance_1. ∀x ∈ set (snd pair). P (fst pair) x ⟶ (∀y ∈ set (snd pair) - { x }. ¬ P (fst pair) y)))
⟹ (∃t ∈ set t_SyncInstance_1. ∃alp ∈ set t_betaSet.∃l ∈ set (snd t). P (fst t) l ⟶ ((∃elm ∈ set alp. Q (fst elm) (snd elm)) ∧ (∀elm ∈ set alp.∀h ∈ set (lookup_1 (fst elm) t_TrigInstance_1) - {snd elm}. ¬Q (fst elm) h) ∧ (∀l1 ∈ set (snd t) - {l}. ¬P (fst t) l1) ∧ (∀t1 ∈ set t_SyncInstance_1 - {t}.∀l2 ∈ set (snd t).¬P (fst t1) l2)))"
unfolding t_SyncInstance_1_def t_TrigInstance_1_def t_betaSet_def
by (metis insert_Diff_single insert_iff list.simps(15) numeral_eq_iff old.prod.inject prod.collapse semiring_norm(88))
``````
1. In the second step, I defined all the terms inside the lemma. Then, I used `sledgehammer` to prove but it's UNPROVABLE. For detail, the sledgehammer supposed some solutions to try but when I use them, it's highlighted by red color.
However, if I use the command in the first step, it is PROVABLE.
``````lemma manual_specific_proving:
fixes t_SyncInstance_1 :: "(nat * nat list) list"
fixes t_TrigInstance_1 :: "(nat * nat list) list"
fixes t_betaSet :: "(nat * nat) list list"
assumes "t_TrigInstance_1 = [(5, [7, 8]), (6, [7, 8])]"
assumes "t_SyncInstance_1 = [(0, [2, 3, 4]), (1, [2, 3, 4])]"
assumes "t_betaSet = [[(5,7), (6,7)], [(5,7), (6,8)], [(5,8), (6,7)], [(5,8), (6,8)]]"
shows
"((∀t ∈ set t_SyncInstance_1. ∀l ∈ set (snd t). P (fst t) l ⟶ (∃alp ∈ set t_betaSet. (∃elm ∈ set alp. Q (fst elm) (snd elm)) ∧ (∀elm ∈ set alp.∀h ∈ set (lookup_1 (fst elm) t_TrigInstance_1) - {snd elm}. ¬Q (fst elm) h))) ∧ (∀pair ∈ set t_TrigInstance_1. ∀x ∈ set (snd pair). Q (fst pair) x ⟶ (∀y ∈ set (snd pair) - { x }. ¬ Q (fst pair) y)) ∧ (∀pair ∈ set t_SyncInstance_1. ∀x ∈ set (snd pair). P (fst pair) x ⟶ (∀y ∈ set (snd pair) - { x }. ¬ P (fst pair) y)))
⟹ (∃t ∈ set t_SyncInstance_1. ∃alp ∈ set t_betaSet.∃l ∈ set (snd t). P (fst t) l ⟶ ((∃elm ∈ set alp. Q (fst elm) (snd elm)) ∧ (∀elm ∈ set alp.∀h ∈ set (lookup_1 (fst elm) t_TrigInstance_1) - {snd elm}. ¬Q (fst elm) h) ∧ (∀l1 ∈ set (snd t) - {l}. ¬P (fst t) l1) ∧ (∀t1 ∈ set t_SyncInstance_1 - {t}.∀l2 ∈ set (snd t).¬P (fst t1) l2)))"
using assms
(*sledgehammer UNPROVABLE:by (smt insertI1 insert_Diff_if insert_commute list.simps(15) numeral_eq_iff  semiring_norm(88) singletonD snd_conv)*)
by (metis insert_Diff_single insert_iff list.simps(15) numeral_eq_iff old.prod.inject prod.collapse semiring_norm(88))
``````
1. I defined `t_SyncInstance_1` in an abstract way and try to prove it but it's UNPROVABLE. Can anyone give me some advice, please?
``````lemma abstract_proving:
fixes t_SyncInstance_1 :: "(nat * nat list) list"
fixes t_TrigInstance_1 :: "(nat * nat list) list"
fixes t_betaSet :: "(nat * nat) list list"
assumes "t_TrigInstance_1 = [(5, [7, 8]), (6, [7, 8])]"
assumes "t_betaSet = [[(5,7), (6,7)], [(5,7), (6,8)], [(5,8), (6,7)], [(5,8), (6,8)]]"
assumes "t_SyncInstance_1 ≠ []" and "∀sync ∈ set t_SyncInstance_1. length (snd sync) > 1"
shows
"((∀t ∈ set t_SyncInstance_1. ∀l ∈ set (snd t). P (fst t) l ⟶ (∃alp ∈ set t_betaSet. (∃elm ∈ set alp. Q (fst elm) (snd elm)) ∧ (∀elm ∈ set alp.∀h ∈ set (lookup_1 (fst elm) t_TrigInstance_1) - {snd elm}. ¬Q (fst elm) h))) ∧ (∀pair ∈ set t_TrigInstance_1. ∀x ∈ set (snd pair). Q (fst pair) x ⟶ (∀y ∈ set (snd pair) - { x }. ¬ Q (fst pair) y)) ∧ (∀pair ∈ set t_SyncInstance_1. ∀x ∈ set (snd pair). P (fst pair) x ⟶ (∀y ∈ set (snd pair) - { x }. ¬ P (fst pair) y)))
⟹ (∃t ∈ set t_SyncInstance_1. ∃alp ∈ set t_betaSet.∃l ∈ set (snd t). P (fst t) l ⟶ ((∃elm ∈ set alp. Q (fst elm) (snd elm)) ∧ (∀elm ∈ set alp.∀h ∈ set (lookup_1 (fst elm) t_TrigInstance_1) - {snd elm}. ¬Q (fst elm) h) ∧ (∀l1 ∈ set (snd t) - {l}. ¬P (fst t) l1) ∧ (∀t1 ∈ set t_SyncInstance_1 - {t}.∀l2 ∈ set (snd t).¬P (fst t1) l2)))"
using assms
proof (induction t_SyncInstance_1) print_cases
case Nil thus ?case by auto
next
case (Cons a t_SyncInstance_1)
assume
IH : "(∀t∈set t_SyncInstance_1.
∀l∈set (snd t).
P (fst t) l ⟶
(∃alp∈set t_betaSet.
(∃elm∈set alp. Q (fst elm) (snd elm)) ∧
(∀elm∈set alp.
∀h∈set (lookup_1 (fst elm) t_TrigInstance_1) - {snd elm}.
¬ Q (fst elm) h))) ∧
(∀pair∈set t_TrigInstance_1.
∀x∈set (snd pair).
Q (fst pair) x ⟶ (∀y∈set (snd pair) - {x}. ¬ Q (fst pair) y)) ∧
(∀pair∈set t_SyncInstance_1.
∀x∈set (snd pair).
P (fst pair) x ⟶ (∀y∈set (snd pair) - {x}. ¬ P (fst pair) y)) ⟹
t_TrigInstance_1 = [(5, [7, 8]), (6, [7, 8])] ⟹
t_betaSet =
[[(5, 7), (6, 7)], [(5, 7), (6, 8)], [(5, 8), (6, 7)], [(5, 8), (6, 8)]] ⟹
t_SyncInstance_1 ≠ [] ⟹
∀sync∈set t_SyncInstance_1. 1 < length (snd sync) ⟹
∃t∈set t_SyncInstance_1.
∃alp∈set t_betaSet.
∃l∈set (snd t).
P (fst t) l ⟶
(∃elm∈set alp. Q (fst elm) (snd elm)) ∧
(∀elm∈set alp.
∀h∈set (lookup_1 (fst elm) t_TrigInstance_1) - {snd elm}.
¬ Q (fst elm) h) ∧
(∀l1∈set (snd t) - {l}. ¬ P (fst t) l1) ∧
(∀t1∈set t_SyncInstance_1 - {t}. ∀l2∈set (snd t). ¬ P (fst t1) l2)"
and
prems :
"(∀t∈set (a # t_SyncInstance_1).
∀l∈set (snd t).
P (fst t) l ⟶
(∃alp∈set t_betaSet.
(∃elm∈set alp. Q (fst elm) (snd elm)) ∧
(∀elm∈set alp.
∀h∈set (lookup_1 (fst elm) t_TrigInstance_1) - {snd elm}.
¬ Q (fst elm) h))) ∧
(∀pair∈set t_TrigInstance_1.
∀x∈set (snd pair). Q (fst pair) x ⟶ (∀y∈set (snd pair) - {x}. ¬ Q (fst pair) y)) ∧
(∀pair∈set (a # t_SyncInstance_1).
∀x∈set (snd pair). P (fst pair) x ⟶ (∀y∈set (snd pair) - {x}. ¬ P (fst pair) y))"
"t_TrigInstance_1 = [(5, [7, 8]), (6, [7, 8])]"
"t_betaSet = [[(5, 7), (6, 7)], [(5, 7), (6, 8)], [(5, 8), (6, 7)], [(5, 8), (6, 8)]]"
"a # t_SyncInstance_1 ≠ []" "∀sync∈set (a # t_SyncInstance_1). 1 < length (snd sync)"
show ?case sledgehammer
qed
``````

Thank you very much.

Last updated: Dec 07 2023 at 20:16 UTC