weblib/basics/lists/append.ma

   1 (* append *)
   2
   3 include "basics/lists/lists.ma".
   4 include "basics/relations.ma".
   5
   6 \ 5img class="anchor" src="icons/tick.png" id="append"\ 6let rec append A (l1: \ 5a href="cic:/matita/basics/lists/lists/list.ind(1,0,1)"\ 6list\ 5/a\ 6 A) l2 on l1 ≝
   7   match l1 with
   8   [ nil ⇒  l2
   9   | cons hd tl ⇒  hd :\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6 append A tl l2 ].
  10
  11 interpretation "append" 'append l1 l2 = (append ? l1 l2).
  12
  13 \ 5img class="anchor" src="icons/tick.png" id="append_nil"\ 6theorem append_nil: ∀A.∀l:\ 5a href="cic:/matita/basics/lists/lists/list.ind(1,0,1)"\ 6list\ 5/a\ 6 A.l \ 5a title="append" href="cic:/fakeuri.def(1)"\ 6@\ 5/a\ 6 [\ 5a title="nil" href="cic:/fakeuri.def(1)"\ 6]\ 5/a\ 6 \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 l.
  14 #A #l (elim l) normalize // qed.
  15
  16 \ 5img class="anchor" src="icons/tick.png" id="associative_append"\ 6theorem associative_append:
  17  ∀A.\ 5font class="Apple-style-span" color="#FF0000"\ 6\ 5a href="cic:/matita/basics/relations/associative.def(1)"\ 6associative\ 5/a\ 6 \ 5/font\ 6(\ 5a href="cic:/matita/basics/lists/lists/list.ind(1,0,1)"\ 6list\ 5/a\ 6 A) (\ 5a href="cic:/matita/basics/lists/append/append.fix(0,1,1)"\ 6append\ 5/a\ 6 A).
  18 #A #l1 #l2 #l3 (elim l1) normalize // qed.
  19
  20 \ 5img class="anchor" src="icons/tick.png" id="append_cons"\ 6theorem append_cons:∀A.∀a:A.∀l,l1.l\ 5a title="append" href="cic:/fakeuri.def(1)"\ 6@\ 5/a\ 6(a:\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6l1)\ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6(l\ 5a title="append" href="cic:/fakeuri.def(1)"\ 6@\ 5/a\ 6\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6[\ 5/a\ 6a\ 5a title="nil" href="cic:/fakeuri.def(1)"\ 6]\ 5/a\ 6)\ 5a title="append" href="cic:/fakeuri.def(1)"\ 6@\ 5/a\ 6l1.
  21 #A #a #l #l1 >\ 5a href="cic:/matita/basics/lists/append/associative_append.def(4)"\ 6associative_append\ 5/a\ 6 // qed.
  22
  23 \ 5img class="anchor" src="icons/tick.png" id="nil_append_elim"\ 6theorem nil_append_elim: ∀A.∀l1,l2: \ 5a href="cic:/matita/basics/lists/lists/list.ind(1,0,1)"\ 6list\ 5/a\ 6 A.∀P:?→?→Prop.
  24   l1\ 5a title="append" href="cic:/fakeuri.def(1)"\ 6@\ 5/a\ 6l2\ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6[\ 5a title="nil" href="cic:/fakeuri.def(1)"\ 6]\ 5/a\ 6 → P (\ 5a href="cic:/matita/basics/lists/lists/list.con(0,1,1)"\ 6nil\ 5/a\ 6 A) (\ 5a href="cic:/matita/basics/lists/lists/list.con(0,1,1)"\ 6nil\ 5/a\ 6 A) → P l1 l2.
  25 #A #l1 #l2 #P (cases l1) normalize //
  26 #a #l3 #heq destruct
  27 qed.
  28
  29 \ 5img class="anchor" src="icons/tick.png" id="nil_to_nil"\ 6theorem nil_to_nil:  ∀A.∀l1,l2:\ 5a href="cic:/matita/basics/lists/lists/list.ind(1,0,1)"\ 6list\ 5/a\ 6 A.
  30   l1\ 5a title="append" href="cic:/fakeuri.def(1)"\ 6@\ 5/a\ 6l2 \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 [\ 5a title="nil" href="cic:/fakeuri.def(1)"\ 6]\ 5/a\ 6 → l1 \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 [\ 5a title="nil" href="cic:/fakeuri.def(1)"\ 6]\ 5/a\ 6 \ 5a title="logical and" href="cic:/fakeuri.def(1)"\ 6∧\ 5/a\ 6 l2 \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 [\ 5a title="nil" href="cic:/fakeuri.def(1)"\ 6]\ 5/a\ 6.
  31 #A #l1 #l2 #isnil @(\ 5a href="cic:/matita/basics/lists/append/nil_append_elim.def(4)"\ 6nil_append_elim\ 5/a\ 6 A l1 l2) /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/basics/logic/And.con(0,1,2)"\ 6conj\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/
  32 qed.
  33
  34 (* comparing lists *)
  35
  36 \ 5img class="anchor" src="icons/tick.png" id="compare_append"\ 6lemma compare_append : ∀A,l1,l2,l3,l4. l1\ 5a title="append" href="cic:/fakeuri.def(1)"\ 6@\ 5/a\ 6l2 \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 l3\ 5a title="append" href="cic:/fakeuri.def(1)"\ 6@\ 5/a\ 6l4 →
  37 ∃l:\ 5a href="cic:/matita/basics/lists/lists/list.ind(1,0,1)"\ 6list\ 5/a\ 6 A\ 5a title="exists" href="cic:/fakeuri.def(1)"\ 6.\ 5/a\ 6(l1 \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 l3\ 5a title="append" href="cic:/fakeuri.def(1)"\ 6@\ 5/a\ 6l \ 5a title="logical and" href="cic:/fakeuri.def(1)"\ 6∧\ 5/a\ 6 l4\ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6l\ 5a title="append" href="cic:/fakeuri.def(1)"\ 6@\ 5/a\ 6l2) \ 5a title="logical or" href="cic:/fakeuri.def(1)"\ 6∨\ 5/a\ 6 (l3 \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 l1\ 5a title="append" href="cic:/fakeuri.def(1)"\ 6@\ 5/a\ 6l \ 5a title="logical and" href="cic:/fakeuri.def(1)"\ 6∧\ 5/a\ 6 l2\ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6l\ 5a title="append" href="cic:/fakeuri.def(1)"\ 6@\ 5/a\ 6l4).
  38 #A #l1 elim l1
  39   [#l2 #l3 #l4 #Heq %{l3} %2 % // @Heq
  40   |#a1 #tl1 #Hind #l2 #l3 cases l3
  41     [#l4 #Heq %{(a1:\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6tl1)} %1 % // @\ 5a href="cic:/matita/basics/logic/sym_eq.def(2)"\ 6sym_eq\ 5/a\ 6 @Heq
  42     |#a3 #tl3 #l4 normalize in ⊢ (%→?); #Heq cases (Hind l2 tl3 l4 ?)
  43       [#l * * #Heq1 #Heq2 %{l}
  44         [%1 % // >Heq1 >(\ 5a href="cic:/matita/basics/lists/lists/cons_injective_l.def(4)"\ 6cons_injective_l\ 5/a\ 6 ????? Heq) //
  45         |%2 % // >Heq1 >(\ 5a href="cic:/matita/basics/lists/lists/cons_injective_l.def(4)"\ 6cons_injective_l\ 5/a\ 6 ????? Heq) //
  46         ]
  47       |@(\ 5a href="cic:/matita/basics/lists/lists/cons_injective_r.def(4)"\ 6cons_injective_r\ 5/a\ 6 ????? Heq)
  48       ]
  49     ]
  50   ]
  51 qed.
  52