commit by user andrea

[helm.git] / weblib / basics / lists / append.ma

diff --git a/weblib/basics/lists/append.ma b/weblib/basics/lists/append.ma
new file mode 100644 (file)
index 0000000..73fbd36
--- /dev/null
+++ b/weblib/basics/lists/append.ma
@@ -0,0 +1,52 @@
+(* append *)
+
+include "basics/lists/lists.ma".
+include "basics/relations.ma".
+
+\ 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 ≝ 
+  match l1 with
+  [ nil ⇒  l2
+  | cons hd tl ⇒  hd :\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6 append A tl l2 ].
+
+interpretation "append" 'append l1 l2 = (append ? l1 l2).
+
+\ 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.
+#A #l (elim l) normalize // qed.
+
+\ 5img class="anchor" src="icons/tick.png" id="associative_append"\ 6theorem associative_append: 
+ ∀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).
+#A #l1 #l2 #l3 (elim l1) normalize // qed.
+
+\ 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.
+#A #a #l #l1 >\ 5a href="cic:/matita/basics/lists/append/associative_append.def(4)"\ 6associative_append\ 5/a\ 6 // qed.
+
+\ 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. 
+  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.
+#A #l1 #l2 #P (cases l1) normalize //
+#a #l3 #heq destruct
+qed.
+
+\ 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.
+  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.
+#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/
+qed.
+
+(* comparing lists *)
+
+\ 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 → 
+∃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).
+#A #l1 elim l1
+  [#l2 #l3 #l4 #Heq %{l3} %2 % // @Heq
+  |#a1 #tl1 #Hind #l2 #l3 cases l3
+    [#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 
+    |#a3 #tl3 #l4 normalize in ⊢ (%→?); #Heq cases (Hind l2 tl3 l4 ?)
+      [#l * * #Heq1 #Heq2 %{l}
+        [%1 % // >Heq1 >(\ 5a href="cic:/matita/basics/lists/lists/cons_injective_l.def(4)"\ 6cons_injective_l\ 5/a\ 6 ????? Heq) //
+        |%2 % // >Heq1 >(\ 5a href="cic:/matita/basics/lists/lists/cons_injective_l.def(4)"\ 6cons_injective_l\ 5/a\ 6 ????? Heq) //
+        ]
+      |@(\ 5a href="cic:/matita/basics/lists/lists/cons_injective_r.def(4)"\ 6cons_injective_r\ 5/a\ 6 ????? Heq) 
+      ]
+    ]
+  ]
+qed.
+