3 include "basics/lists/lists.ma".
4 include "basics/relations.ma".
6 let rec append A (l1:
\ 5a href="cic:/matita/basics/lists/lists/list.ind(1,0,1)"
\ 6list
\ 5/a
\ 6 A) l2 on l1 ≝
9 | cons hd tl ⇒ hd :
\ 5a title="cons" href="cic:/fakeuri.def(1)"
\ 6:
\ 5/a
\ 6 append A tl l2 ].
11 interpretation "append" 'append l1 l2 = (append ? l1 l2).
13 theorem 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.
16 theorem 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.
20 theorem 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.
23 theorem 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 //
29 theorem 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/
36 lemma 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).
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) //
47 |@(
\ 5a href="cic:/matita/basics/lists/lists/cons_injective_r.def(4)"
\ 6cons_injective_r
\ 5/a
\ 6 ????? Heq)