Stream: Beginner Questions

Topic: Proving lemma with abstract lists

view this post on Zulip 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: Apr 20 2024 at 08:16 UTC