Regola 3. La funzione di inversione della lista ha una complessità di $n^2$
Dimostriamo per induzione, che l’uguaglianza stabilita dalla regola è vera per tutte le liste.
Vogliamo dimostrare che per ogni possibile lista vale l’equazione
Dobbiamo quindi dimostrare che per il caso base è vera rev(L_2)
Mi domando ora come arrivare all’eguaglianza da dimostrare. devo avere qualcossa del tipo app(l1, l2) ma ciò non corrisponde al caso base. abbiamo però già visto un’altra proprietà di app.
Ma grazie al lemma 1 posso dire che è uguale app(rev(l2), [ ])
E quindi posso concludere con app(rev(l2), rev([ ]))
Passo induttivo, la lista vale per a:list allora lo è per ogni altra lista.
Assumendo che la proprietà è valida per una lista l allora deve essere vera anche per a:l per ogni l appartenente alla lista a per ogni elemento dell’insieme A.
Comincio a dimostrare l’uguaglianza dalla parte sx: rev(app(a:l, l2)) (assumo che la lista abbia almeno un’elemento di a)
utilizzando la clausola induttiva di app → rev(a:app(l,l2))
a questo punto posso usare la clausola induttiva di rev (c’è almeno un’elemento nella lista) app(rev(l, l2), a:[ ])
Per ipotesi induttiva posso “rimpiazzare” rev(l, l2) con il membro destro: app(app(rev(l2), rev(l)), a:[ ]) (applicato ipotesi induttiva e sostituito l’espressione)
Abbiamo ora da fare la concatenazione di 3 liste app(rev(l2), rev(l)), a:[ ]) possiamo concatenare le prime due e il risultato con la 3° lista
L’associativa di app (lemma 2) faccio concatenazione tra la prima e il riusltato di concatenazione delle successive due: app(rev(l2), app(rev(l), a:[ ])
Uso la clausola induttiva al contrario per ottenere alla fine: app(rev(l2), rev(a : l)