************************************
Week 8: Full Proof of Associativity: 
************************************


Last time we proved associativity for the base case (aka case nil). This time we aim to fill the gap for the inductive step and complete the proof. 
Remember we try to prove ::

    app (app xs ys) zs = app xs (app ys zs)

The base case is when ``xs = []`` and we proved ::

    app (app [] ys) zs = app [] (app ys zs)   

For inductive step, we first give a diagrammatic proof. (On the board)

Notice that the inductive step which should be proved is ::

    app (app (x::xs) ys) zs = app (x::xs) (app ys zs) 

While the induction hypothesis is ::

    app (app xs ys) zs = app xs (app ys zs)






The full proof is as follows ::


    Signatures:
        app  : _a list -> _a list -> _a list ;
        rev  : _a list -> _a list ;

    Definitions:
        [app nil] : forall xs : _a list . app [] xs = xs : _a list ;
        [app xs]  : forall x : _a . forall xs : _a list . forall ys : _a list . app (x::xs) ys = x :: app xs ys : _a list ;
        [rev nil] : rev [] = [] : _a list ;
        [rev xs]  : forall xs : _a list . forall x : _a . rev (x :: xs) = app (rev xs) (x :: []) : _a list ;	


    Theorem [lemma]:
        Statement: forall xs : _a list . forall ys : _a list . forall zs : _a list .
                   app (app xs ys) zs = app xs (app ys zs) : _a list
        Proof:
            by induction on list:
            case nil:
                assume ys : _a list.
                assume zs : _a list.
                we know [prem 1] : app [] ys = ys : _a list because [app nil] with (ys).
                we know [prem 2] : app [] (app ys zs) = (app ys zs) : _a list because [app nil] with (app ys zs).

                we know [step 1] : app (app [] ys) zs = app ys zs : _a list because equality on ([prem 1]).
                we know [step 2] : app (app [] ys) zs = app [] (app ys zs) : _a list because equality on ([step 1];[prem 2]).
                by [step 2]
				
            case (x::xs): [IH] : forall ys : _a list . forall zs : _a list .
                            app (app xs ys) zs = app xs (app ys zs) : _a list .
                assume ys : _a list.
                assume zs : _a list.
                we know [prem 1] : app (x::xs) ys = x::(app xs ys) : _a list because [app xs] with (x;xs;ys).
                we know [prem 2] : app (x::(app xs ys)) zs = x::(app (app xs ys) zs) : _a list because [app xs] with (x;app xs ys;zs).
                we know [prem 3] : app (app xs ys) zs = app xs (app ys zs) : _a list because [IH] with (ys;zs).
                we know [prem 4] : app (x::xs) (app ys zs) = x::(app xs (app ys zs)) : _a list because [app xs] with (x;xs;app ys zs).

                we know [step 1] : app (app (x::xs) ys) zs = app (x::(app xs ys)) zs : _a list because equality on ([prem 1]).
                we know [step 2] : app (app (x::xs) ys) zs = x::(app (app xs ys) zs) : _a list because equality on ([step 1];[prem 2]).
                we know [step 3] : app (app (x::xs) ys) zs = x::(app xs (app ys zs)) : _a list because equality on ([step 2];[prem 3]).
                we know [step 4] : app (app (x::xs) ys) zs = app (x::xs) (app ys zs) : _a list because equality on ([step 3];[prem 4]).
                by [step 4]
        QED.

	
	
	
	
	
	
	

	
	

Now we can prove a more specific proposition ::



    Theorem [example 6]:
        Statement: forall xs : _a list . forall x : _a . forall ys : _a list .
               app (app (rev ys) (rev xs)) (x::[]) = app (rev ys) (app (rev xs) (x::[])) : _a list
        Proof:
            assume xs : _a list .
            assume x : _a .
            assume ys : _a list .
            [lemma] with (rev ys; rev xs; x::[])
        QED.