Need help in assignment task in logic proof field!

Question

We are currently struggling with this task in an exercise session. The problem is that none of us are that much familiar with proofing and this seems quite difficult. The task it self says:

A list represents a sequence of elements, e.g, $l_1 = [a,b,c]$ or $l_2 = [1,2,3,5,7,11]$ are two lists. The head of a non-empty list is its left-most element (1st element) and the tail of a list is a list containing all the elements except the head. Let $h$ show the head of a non-empty list $l$ and $t$ show its tail, we show the list $l$ by $h :: t$.

The predicate ${\rm take}(l,n,l_0)$ shows that the list $l_0$ contains the first $n$ elements of $l$. The function ${\rm length}(l)$ is defined as follows: $$\begin{cases} \forall h~\forall t~{\rm length}(h :: t) = 1 + {\rm length}(t) \\ {\rm length}([]) = 0 \end{cases}$$

Prove

$$[{\rm take}(l,n,l_0)] \implies {\rm length}(l_0) \le {\rm length}(l)$$

Note that if $l = l_0$, then ${\rm length}(l) = {\rm length}(l_0)$.

Answer 1

the statement length(l')<=length(l) is a valid logical formula that you should prove. Note that we define many predicates based on mathematical formulae, e.g. the predicate square(n,m) holds if m is the square of n defined as (m=n*n). You may rewrite this as a predicate if you like to, but you can prove it without that as well.

Answer 2

What you are trying to prove isn't a true statement. For example, consider

$$l = [1, 2, 3, 4, 5]$$ $$n = 2$$ $$l_0 = [1, 2, 3]$$

Then you have

$${\rm take}(l, n, l_0) \implies {\rm length}(l) \le {\rm length}(l_0)$$ $${\rm take}([1, 2, 3, 4, 5], 2, [1, 2, 3]) \implies 5 \le 3$$ $$\text{true} \implies \text{false}$$