right associative with precedence 47
for @{'append $l1 $l2 }.
-interpretation "nil" 'nil = (nil _).
-interpretation "cons" 'cons hd tl = (cons _ hd tl).
+interpretation "nil" 'nil = (nil ?).
+interpretation "cons" 'cons hd tl = (cons ? hd tl).
(* theorem test_notation: [O; S O; S (S O)] = O :: S O :: S (S O) :: []. *)
[ nil => []
| (cons hd tl) => tl].
-interpretation "append" 'append l1 l2 = (append _ l1 l2).
+interpretation "append" 'append l1 l2 = (append ? l1 l2).
theorem append_nil: \forall A:Type.\forall l:list A.l @ [] = l.
intros;
| step : \forall l1,l2:list A. \forall x,y:A.
permut1 ? (l1 @ (x :: y :: l2)) (l1 @ (y :: x :: l2)).
-include "nat/nat.ma".
-
+(*
+
definition x1 \def S O.
definition x2 \def S x1.
definition x3 \def S x2.
apply (step ? (x1::[]) [] x2 x3).
qed.
-
-(*
theorem nil_append_nil_both:
\forall A:Type.\forall l1,l2:list A.
l1 @ l2 = [] \to l1 = [] \land l2 = [].
-*)
-
-(*
-include "nat/nat.ma".
theorem test_notation: [O; S O; S (S O)] = O :: S O :: S (S O) :: [].
reflexivity.
simplify.
reflexivity.
qed.
+
*)
definition nth ≝
[simplify;apply le_S_S;assumption
|simplify;apply le_S;assumption]]
qed.
+
+lemma length_append : ∀A,l,m.length A (l@m) = length A l + length A m.
+intros;elim l
+[reflexivity
+|simplify;rewrite < H;reflexivity]
+qed.