Как поднять переходное отношение от элементов к спискам? - PullRequest
Новая
       55

Как поднять переходное отношение от элементов к спискам?

0 голосов
/ 24 октября 2018

Я пытаюсь доказать, что транзитивное отношение в элементах списков эквивалентно транзитивному отношению в списках (при некоторых условиях).

Вот первая лемма: 

lemma list_all2_rtrancl1:
  "(list_all2 P)⇧*⇧* xs ys ⟹
   list_all2 P⇧*⇧* xs ys"
  apply (induct rule: rtranclp_induct)
  apply (simp add: list.rel_refl)
  by (smt list_all2_trans rtranclp.rtrancl_into_rtrancl)

А вот симметричная лемма: 

lemma list_all2_rtrancl2:
  "(⋀x. P x x) ⟹
   list_all2 P⇧*⇧* xs ys ⟹
   (list_all2 P)⇧*⇧* xs ys"
  apply (erule list_all2_induct)
  apply simp

Я предполагаю, что отношение должно быть рефлексивным.Но, возможно, я должен использовать другие предположения.Лемма может быть доказана, если предположить, что P транзитивно, однако P не транзитивно.Я застрял.Не могли бы вы предложить, какие предположения выбрать и как доказать эту лемму?

Кажется, что Нитпик дает мне неправильный контрпример для конкретного случая последней леммы (xs = [0] и ys = [2]): 

lemma list_all2_rtrancl2_example:
  "list_all2 (λx y. x = y ∨ Suc x = y)⇧*⇧* xs ys ⟹
   (list_all2 (λx y. x = y ∨ Suc x = y))⇧*⇧* xs ys"
  nitpick

Я могу доказать, что лемма справедлива для этого примера: 

lemma list_all2_rtrancl2_example_0_2:
  "list_all2 (λx y. x = y ∨ Suc x = y)⇧*⇧* [0] [2] ⟹
   (list_all2 (λx y. x = y ∨ Suc x = y))⇧*⇧* [0] [2]"
  apply (rule_tac ?b="[1]" in converse_rtranclp_into_rtranclp; simp)
  apply (rule_tac ?b="[2]" in converse_rtranclp_into_rtranclp; simp)
  done

1 Ответ

0 голосов
/ 24 октября 2018

Может быть целесообразно использовать listrel вместо list_all2.Действительно, как показано ниже, они эквивалентны (см. set_listrel_eq_list_all2).Однако в стандартной библиотеке есть несколько теорем о listrel, у которых нет эквивалентов для list_all2. 

theory so_htlatrfetl_2
  imports Complex_Main
begin

lemma set_listrel_eq_list_all2: 
  "listrel {(x, y). r x y} = {(xs, ys). list_all2 r xs ys}"
  using list_all2_conv_all_nth listrel_iff_nth by fastforce

lemma listrel_tclosure_1: "(listrel r)⇧* ⊆ listrel (r⇧*)"
  by (simp add: listrel_rtrancl_eq_rtrancl_listrel1 
      listrel_subset_rtrancl_listrel1 rtrancl_subset_rtrancl)

lemma listrel_tclosure_2: "refl r ⟹ listrel (r⇧*) ⊆ (listrel r)⇧*"
  by (simp add: listrel1_subset_listrel listrel_rtrancl_eq_rtrancl_listrel1 
      rtrancl_mono)

context includes lifting_syntax
begin

lemma listrel_list_all2_transfer [transfer_rule]:
  "((=) ===> (=) ===> (=) ===> (=)) 
  (λr xs ys. (xs, ys) ∈ listrel {(x, y). r x y}) list_all2"
  unfolding rel_fun_def using set_listrel_eq_list_all2 listrel_iff_nth by blast

end

lemma list_all2_rtrancl_1:
  "(list_all2 r)⇧*⇧* xs ys ⟹ list_all2 r⇧*⇧* xs ys"
proof(transfer)
  fix r :: "'a ⇒ 'a ⇒ bool"
  fix xs :: "'a list"
  fix ys:: "'a list"
  assume "(λxs ys. (xs, ys) ∈ listrel {(x, y). r x y})⇧*⇧* xs ys"
  then have "(xs, ys) ∈ (listrel {(x, y). r x y})⇧*"
    unfolding rtranclp_def rtrancl_def by auto  
  then have "(xs, ys) ∈ listrel ({(x, y). r x y}⇧*)" 
    using listrel_tclosure_1 by auto
  then show "(xs, ys) ∈ listrel {(x, y). r⇧*⇧* x y}"
    unfolding rtranclp_def rtrancl_def by auto  
qed

lemma list_all2_rtrancl_2:
  "reflp r ⟹ list_all2 r⇧*⇧* xs ys ⟹ (list_all2 r)⇧*⇧* xs ys"
proof(transfer)
  fix r :: "'a ⇒ 'a ⇒ bool"
  fix xs :: "'a list"
  fix ys :: "'a list"
  assume as_reflp: "reflp r" 
  assume p_in_lr: "(xs, ys) ∈ listrel {(x, y). r⇧*⇧* x y}"
  from as_reflp have refl: "refl {(x, y). r x y}" 
    using reflp_refl_eq by fastforce
  from p_in_lr have "(xs, ys) ∈ listrel ({(x, y). r x y}⇧*)"
    unfolding rtranclp_def rtrancl_def by auto
  with refl have "(xs, ys) ∈ (listrel {(x, y). r x y})⇧*"
    using listrel_tclosure_2 by auto
  then show "(λxs ys. (xs, ys) ∈ listrel {(x, y). r x y})⇧*⇧* xs ys" 
    unfolding rtranclp_def rtrancl_def by auto
qed

end

Также предоставляется прямое доказательство для list_all2(наследие):

  1. list_all2_induct применяется к спискам;базовый случай тривиален.Отсюда осталось показать, что (L P)* x#xs y#ys, если (L (P*)) xs ys, (L P)* xs ys и P* x y.
  2. Идея состоит в том, что можно найти zs (например, xs) такой, что (L P) xs zs и (L P)+ zs ys.
  3. Затем, учитывая, что P* x y и P x x, по индукции на основе переходных свойств P*, (L P) x#xs y#zs.Следовательно, также, (L P)* x#xs y#zs.
  4. Кроме того, учитывая, что (L P)+ zs ys и P y y, по индукции (L P)+ y#zs y#ys.Таким образом, также, (L P)* y#zs y#ys.
  5. Из 3 и 4 заключаются (L P)* x#xs y#ys. 
theory so_htlatrfetl
imports  Complex_Main

begin

lemma list_all2_rtrancl2:
  assumes as_r: "(⋀x. P x x)" 
  shows "(list_all2 P⇧*⇧*) xs ys ⟹ (list_all2 P)⇧*⇧* xs ys"
proof(induction rule: list_all2_induct)
  case Nil then show ?case by simp
next
  case (Cons x xs y ys) show ?case
  proof -
    from as_r have lp_xs_xs: "list_all2 P xs xs" by (rule list_all2_refl)
    from Cons.hyps(1) have x_xs_y_zs: "(list_all2 P)⇧*⇧* (x#xs) (y#xs)"
    proof(induction rule: rtranclp_induct)
      case base then show ?case by simp
    next
      case (step y z) then show ?case 
      proof -
        have rt_step_2: "(list_all2 P)⇧*⇧* (y#xs) (z#xs)" 
          by (rule r_into_rtranclp, rule list_all2_Cons[THEN iffD2]) 
            (simp add: step.hyps(2) lp_xs_xs)
        from step.IH rt_step_2 show ?thesis by (rule rtranclp_trans) 
      qed      
    qed
    from Cons.IH have "(list_all2 P)⇧*⇧* (y#xs) (y#ys)"
    proof(induction rule: rtranclp_induct)
      case base then show ?case by simp
    next
      case (step ya za) show ?case
      proof -
        have rt_step_2: "(list_all2 P)⇧*⇧* (y#ya) (y#za)" 
          by (rule r_into_rtranclp, rule list_all2_Cons[THEN iffD2])     
            (simp add: step.hyps(2) as_r)
        from step.IH rt_step_2 show ?thesis by (rule rtranclp_trans)
      qed
    qed
    with x_xs_y_zs show ?thesis by simp
  qed
qed

end

Как примечание стороны, на мой взгляд (Я очень мало знаю о Нитпике), Нитпик не должен предоставлять недействительные контрпримеры без какого-либо предупреждения.Обычно я полагаю, что когда nitpick «подозревает», что контрпример может быть недействительным, он уведомляет пользователя о том, что этот пример «потенциально фальшивый».Может быть полезно отправить отчет об ошибке, если эта проблема не была зарегистрирована в другом месте.

...