(* ========================================================================= *) (* *) (* * NUMERI NATURALI *) (* *) (* ========================================================================= *) (* ------------------------------------------------------------------------- *) (* COMANDI DI BASE *) (* Inductive X ... Definire un insieme induttivo *) (* Fixpoint f ... Definire una funzione ricorsiva *) (* match with Analisi per casi. *) (* *) (* Eval compute in Calcolare il valore di un termine *) (* Eval simpl in Semplificare un termine *) (* *) (* TATTICHE *) (* compute, simpl semplificazione *) (* rewrite H riscrivere usando l'equazione H *) (* reflexivity, dimostrare x=x *) (* symmetry, usando y=x dimostrare x=y *) (* transitivity x usando a=x e x=b dimostrare a=b *) (* ------------------------------------------------------------------------- *) (* ------------------------------------------------------------------------- *) (* ** Definizione dell'insieme dei numeri naturali *) (* *) (* I numeri naturali (nat) formano un insieme `induttivo', cioe' nat e' il *) (* piu' piccolo insieme tale che: *) (* - contiene `zero', che indicheremo con la lettera maiuscola "O", *) (* - se contiene n, contiene il suo successore, indicato `S n'. *) (* ------------------------------------------------------------------------- *) Inductive nat : Set := (* nat e' un insieme induttivo *) | O : nat (* O (zero) e' un `costruttore' di nat *) | S : nat -> nat. (* S (successore) e' un altro `costruttore' *) (* ------------------------------------------------------------------------- *) (* L'istruzione precedente definisce i termini nat O e S come specificato e *) (* fornisce i principi di induzione e di ricorsone nat_ind e nat_rec. *) (* ------------------------------------------------------------------------- *) Check O. Check S. Check (S (S O)). Check nat. Check nat_ind. (* Principio di induzione *) Check nat_rec. (* Principio di ricorsione *) (* ------------------------------------------------------------------------- *) (* Definizione di funzione ricorsive: il comando "Fixpoint" *) (* *) (* Il seguente comando definisce l'addizione "plus n m" per ricorsione *) (* strutturale sul primo argomento n. *) (* ------------------------------------------------------------------------- *) Fixpoint plus (n m : nat) { struct n } : nat := match n with | O => m | S n' => S (plus n' m) end. Check plus. Print plus. Check (plus O O). Eval compute in (plus O O). Definition zero := O. Definition one := S O. Definition two := S one. Definition three := S two. Definition four := S three. Check three. Print three. Eval compute in three. Eval compute in (plus two two). Remark two_two_four : plus two two = four. compute. reflexivity. Qed. Lemma O_plus : forall n, plus O n = n. intros. compute. reflexivity. Qed. Lemma plus_O : forall n, plus n O = n. induction n. compute. reflexivity. simpl. rewrite IHn. reflexivity. Qed. (* ------------------------------------------------------------------------- *) (* Esercizio: *) (* perche' le dimostrazioni di O_plus e plus_O sono cosi' diverse? *) (* ------------------------------------------------------------------------- *) Lemma plus_assoc : forall n m p, plus n (plus m p) = plus (plus n m) p. intros. induction n. simpl. reflexivity. simpl. rewrite IHn. reflexivity. Qed. (* ------------------------------------------------------------------------- *) (* Esercizio*: *) (* e' possibile dimostrare plus_assoc per induzione su m o su p? *) (* ------------------------------------------------------------------------- *) Lemma plus_comm : forall n m, plus n m = plus m n. induction n. intros. simpl. rewrite plus_O. reflexivity. intros. simpl. rewrite IHn. (* ------------------------------------------------------------------------- *) (* Problema: Qui e' necessario un lemma "plus_S". *) (* Quindi abbandoniamo questa dimostrazione per riprenderla piu' tardi. *) (* Cancellare questo tentativo di dimostrazione incompiuta. *) (* (Oppure usare il comando "Abort") *) (* ------------------------------------------------------------------------- *) Lemma plus_S : forall n m, plus n (S m) = S (plus n m). intros. induction n. simpl. reflexivity. simpl. rewrite IHn. reflexivity. Qed. (* ------------------------------------------------------------------------- *) (* Adesso possiamo riprendere e finire la dimostrazione di plus_comm. *) (* ------------------------------------------------------------------------- *) Lemma plus_comm : forall n m, plus n m = plus m n. induction n. intros. simpl. rewrite plus_O. reflexivity. intros. simpl. rewrite IHn. (* Eravamo arrivati qui! *) rewrite plus_S. reflexivity. Qed. (* ------------------------------------------------------------------------- *) (* Esercizio. *) (* La dimostrazione di "S_plus" e' molto piu' facile di quella di "plus_S". *) (* (Perche'?) Confrontare con il caso gia' visto di "O_plus" e "plus_O". *) (* ------------------------------------------------------------------------- *) Lemma S_plus : forall n m, plus (S n) m = S (plus n m). Qed. (* ------------------------------------------------------------------------- *) (* Esercizio. *) (* Definire la moltiplicazione (copiare e modificare per analogia il codice *) (* gia' visto sopra per la somma). Verificare il corretto funzionamento *) (* su alcuni esempi concreti (es. 2 x 3 = 6). Dimostrare le proprieta' *) (* elementari della moltiplicazione (elemento neutro a destra e sinistra, *) (* associativita', commutativita', distributivita' rispetto alla somma). *) (* ------------------------------------------------------------------------- *) Fixpoint mult ....