From: Enrico Tassi Date: Sat, 15 Nov 2008 13:17:00 +0000 (+0000) Subject: housekeeping X-Git-Tag: make_still_working~4560 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=f1f445457c73202fd696c1b9fe0b24c0bafe2452;hp=3895bfa2b76c88af1d6ac41605ff17e2626d353a;p=helm.git housekeeping --- diff --git a/helm/software/matita/contribs/didactic/Makefile b/helm/software/matita/contribs/didactic/Makefile deleted file mode 100644 index d31ab5525..000000000 --- a/helm/software/matita/contribs/didactic/Makefile +++ /dev/null @@ -1,22 +0,0 @@ -include ../Makefile.defs - -DIR=$(shell basename $$PWD) - -$(DIR) all: - $(BIN)matitac -$(DIR).opt opt all.opt: - $(BIN)matitac.opt -clean: - $(BIN)matitaclean -clean.opt: - $(BIN)matitaclean.opt -depend: - $(BIN)matitadep -dot && rm depends.dot -depend.opt: - $(BIN)matitadep.opt -dot && rm depends.dot -exercise-%: % - cp $< $@ - perl -ne 'undef $$/;s/\(\*BEGIN.*?END\*\)/…/msg;print' -i $@ - perl -ne 'undef $$/;s/\(\*DOCBEGIN.*?DOCEND\*\)//msg;print' -i $@ - (echo ''; awk 'BEGIN { p = 0; } /DOCEND/ { p = 0; } { if (p == 1) print $$0; } /DOCBEGIN/ { p = 1;}' < $< | markdown; echo '') > $@.html - diff --git a/helm/software/matita/contribs/didactic/duality.ma b/helm/software/matita/contribs/didactic/duality.ma deleted file mode 100644 index c04859bd1..000000000 --- a/helm/software/matita/contribs/didactic/duality.ma +++ /dev/null @@ -1,619 +0,0 @@ -(* Esercitazione di logica 29/10/2008. - - Note per gli esercizi: - - http://www.cs.unibo.it/~tassi/exercise-duality.ma.html - -*) - -(* Esercizio 0 - =========== - - Compilare i seguenti campi: - - Nome1: ... - Cognome1: ... - Matricola1: ... - Account1: ... - - Nome2: ... - Cognome2: ... - Matricola2: ... - Account2: ... - - Prima di abbandonare la postazione: - - * salvare il file (menu `File ▹ Save as ...`) nella directory (cartella) - /public/ con nome linguaggi_Account1.ma, ad esempio Mario Rossi, il cui - account è mrossi, deve salvare il file in /public/linguaggi_mrossi.ma - - * mandatevi via email o stampate il file. Per stampare potete usare - usare l'editor gedit che offre la funzionalità di stampa -*) - -(*DOCBEGIN - -Il teorema di dualità -===================== - -Il teorema di dualizzazione dice che date due formule `F1` ed `F2`, -se le due formule sono equivalenti (`F1 ≡ F2`) allora anche le -loro dualizzate lo sono (`dualize F1 ≡ dualize F2`). - -L'ingrediente principale è la funzione di dualizzazione di una formula `F`: - - * Scambia FTop con FBot e viceversa - - * Scambia il connettivo FAnd con FOr e viceversa - - * Sostituisce il connettivo FImpl con FAnd e nega la - prima sottoformula. - - Ad esempio la formula `A → (B ∧ ⊥)` viene dualizzata in - `¬A ∧ (B ∨ ⊤)`. - -Per dimostrare il teorema di dualizzazione in modo agevole è necessario -definire altre nozioni: - -* La funzione `negate` che presa una formula `F` ne nega gli atomi. - Ad esempio la formula `(A ∨ (⊤ → B))` deve diventare `¬A ∨ (⊤ → ¬B)`. - -* La funzione `invert` permette di invertire un mondo `v`. - Ovvero, per ogni indice di atomo `i`, se `v i` restituisce - `1` allora `(invert v) i` restituisce `0` e viceversa. - -DOCEND*) - -(* ATTENZIONE - ========== - - Non modificare quanto segue -*) -include "nat/minus.ma". -definition if_then_else ≝ λT:Type.λe,t,f.match e return λ_.T with [ true ⇒ t | false ⇒ f]. -notation > "'if' term 19 e 'then' term 19 t 'else' term 90 f" non associative with precedence 19 for @{ 'if_then_else $e $t $f }. -notation < "'if' \nbsp term 19 e \nbsp 'then' \nbsp term 19 t \nbsp 'else' \nbsp term 90 f \nbsp" non associative with precedence 19 for @{ 'if_then_else $e $t $f }. -interpretation "Formula if_then_else" 'if_then_else e t f = (if_then_else _ e t f). -definition max ≝ λn,m. if eqb (n - m) 0 then m else n. -definition min ≝ λn,m. if eqb (n - m) 0 then n else m. - -(* Ripasso - ======= - - Il linguaggio delle formule, dove gli atomi sono - rapperesentati da un numero naturale -*) -inductive Formula : Type ≝ -| FBot: Formula -| FTop: Formula -| FAtom: nat → Formula -| FAnd: Formula → Formula → Formula -| FOr: Formula → Formula → Formula -| FImpl: Formula → Formula → Formula -| FNot: Formula → Formula -. - -(* Esercizio 1 - =========== - - Modificare la funzione `sem` scritta nella precedente - esercitazione in modo che valga solo 0 oppure 1 nel caso degli - atomi, anche nel caso in cui il mondo `v` restituisca un numero - maggiore di 1. - - Suggerimento: non è necessario usare il costrutto if_then_else - e tantomento il predicato di maggiore o uguale. È invece possibile - usare la funzione `min`. -*) -let rec sem (v: nat → nat) (F: Formula) on F : nat ≝ - match F with - [ FBot ⇒ 0 - | FTop ⇒ 1 - | FAtom n ⇒ (*BEGIN*)min (v n) 1(*END*) - | FAnd F1 F2 ⇒ min (sem v F1) (sem v F2) - | FOr F1 F2 ⇒ max (sem v F1) (sem v F2) - | FImpl F1 F2 ⇒ max (1 - sem v F1) (sem v F2) - | FNot F1 ⇒ 1 - (sem v F1) - ] -. - -(* ATTENZIONE - ========== - - Non modificare quanto segue. -*) -notation < "[[ \nbsp term 19 a \nbsp ]] \nbsp \sub term 90 v" non associative with precedence 90 for @{ 'semantics $v $a }. -notation > "[[ term 19 a ]] \sub term 90 v" non associative with precedence 90 for @{ 'semantics $v $a }. -notation > "[[ term 19 a ]]_ term 90 v" non associative with precedence 90 for @{ sem $v $a }. -interpretation "Semantic of Formula" 'semantics v a = (sem v a). - -definition v20 ≝ λx. - if eqb x 0 then 2 - else if eqb x 1 then 1 - else 0. - -(* Test 1 - ====== - - La semantica della formula `(A ∨ C)` nel mondo `v20` in cui - `A` vale `2` e `C` vale `0` deve valere `1`. - -*) -eval normalize on [[FOr (FAtom 0) (FAtom 2)]]_v20. - -(*DOCBEGIN - -La libreria di Matita -===================== - -Gli strumenti per la dimostrazione assistita sono corredati da -librerie di teoremi già dimostrati. Per portare a termine l'esercitazione -sono necessari i seguenti lemmi: - -* lemma `sem_le_1` : `∀F,v. [[ F ]]_v ≤ 1` -* lemma `min_1_1` : `∀x. x ≤ 1 → 1 - (1 - x) = x` -* lemma `min_bool` : `∀n. min n 1 = 0 ∨ min n 1 = 1` -* lemma `min_max` : `∀F,G,v.min (1 - [[F]]_v) (1 - [[G]]_v) = 1 - max [[F]]_v [[G]]_v` -* lemma `max_min` : `∀F,G,v.max (1 - [[F]]_v) (1 - [[G]]_v) = 1 - min [[F]]_v [[G]]_v` -* lemma `equiv_rewrite` : `∀F1,F2,F3. F1 ≡ F2 → F1 ≡ F3 → F2 ≡ F3` - -DOCEND*) - -(* ATTENZIONE - ========== - - Non modificare quanto segue. -*) -lemma sem_bool : ∀F,v. [[ F ]]_v = 0 ∨ [[ F ]]_v = 1. intros; elim F; simplify; [left;reflexivity; |right;reflexivity; |cases (v n);[left;|cases n1;right;]reflexivity; |4,5,6: cases H; cases H1; rewrite > H2; rewrite > H3; simplify; first [ left;reflexivity | right; reflexivity ]. |cases H; rewrite > H1; simplify;[right|left]reflexivity;] qed. -lemma min_bool : ∀n. min n 1 = 0 ∨ min n 1 = 1. intros; cases n; [left;reflexivity] cases n1; right; reflexivity; qed. -lemma min_max : ∀F,G,v. min (1 - [[F]]_v) (1 - [[G]]_v) = 1 - max [[F]]_v [[G]]_v. intros; cases (sem_bool F v);cases (sem_bool G v); rewrite > H; rewrite >H1; simplify; reflexivity; qed. -lemma max_min : ∀F,G,v. max (1 - [[F]]_v) (1 - [[G]]_v) = 1 - min [[F]]_v [[G]]_v. intros; cases (sem_bool F v);cases (sem_bool G v); rewrite > H; rewrite >H1; simplify; reflexivity; qed. -lemma min_1_1 : ∀x.x ≤ 1 → 1 - (1 - x) = x. intros; inversion H; intros; destruct; [reflexivity;] rewrite < (le_n_O_to_eq ? H1); reflexivity;qed. -lemma sem_le_1 : ∀F,v.[[F]]_v ≤ 1. intros; cases (sem_bool F v); rewrite > H; [apply le_O_n|apply le_n]qed. - -(* Esercizio 2 - =========== - - Definire per ricorsione strutturale la funzione `negate` - che presa una formula `F` ne nega gli atomi. - - Ad esempio la formula `(A ∨ (⊤ → B))` deve diventare - `¬A ∨ (⊤ → ¬B)`. -*) -let rec negate (F: Formula) on F : Formula ≝ - match F with - [ (*BEGIN*)FBot ⇒ FBot - | FTop ⇒ FTop - | FAtom n ⇒ FNot (FAtom n) - | FAnd F1 F2 ⇒ FAnd (negate F1) (negate F2) - | FOr F1 F2 ⇒ FOr (negate F1) (negate F2) - | FImpl F1 F2 ⇒ FImpl (negate F1) (negate F2) - | FNot F ⇒ FNot (negate F)(*END*) - ]. - -(* Test 2 - ====== - - Testare la funzione `negate`. Il risultato atteso è: - - FOr (FNot (FAtom O)) (FImpl FTop (FNot (FAtom 1))) -*) - -eval normalize on (negate (FOr (FAtom 0) (FImpl FTop (FAtom 1)))). - -(* ATTENZIONE - ========== - - Non modificare quanto segue -*) -definition equiv ≝ λF1,F2. ∀v.[[ F1 ]]_v = [[ F2 ]]_v. -notation "hvbox(a \nbsp break mstyle color #0000ff (≡) \nbsp b)" non associative with precedence 45 for @{ 'equivF $a $b }. -notation > "a ≡ b" non associative with precedence 50 for @{ equiv $a $b }. -interpretation "equivalence for Formulas" 'equivF a b = (equiv a b). -lemma equiv_rewrite : ∀F1,F2,F3. F1 ≡ F2 → F1 ≡ F3 → F2 ≡ F3. intros; intro; autobatch. qed. - -(* Esercizio 3 - =========== - - Definire per ricorsione strutturale la funzione di - dualizzazione di una formula `F`. Tale funzione: - - * Scambia FTop con FBot e viceversa - - * Scambia il connettivo FAnd con FOr e viceversa - - * Sostituisce il connettivo FImpl con FAnd e nega la - prima sottoformula. Il razionale è che `FImpl A B` - è semanticamente equivalente a `FOr (FNot A) B` il - cui duale è `FAnd (FNot A) B`. - - Ad esempio la formula `A → (B ∧ ⊥)` viene dualizzata in - `¬A ∧ (B ∨ ⊤)`. -*) -let rec dualize (F : Formula) on F : Formula ≝ - match F with - [ (*BEGIN*)FBot ⇒ FTop - | FTop ⇒ FBot - | FAtom n ⇒ FAtom n - | FAnd F1 F2 ⇒ FOr (dualize F1) (dualize F2) - | FOr F1 F2 ⇒ FAnd (dualize F1) (dualize F2) - | FImpl F1 F2 ⇒ FAnd (FNot (dualize F1)) (dualize F2) - | FNot F ⇒ FNot (dualize F)(*END*) - ]. - -(* Test 3 - ====== - - Testare la funzione `dualize`. Il risultato atteso è: - - FAnd (FNot (FAtom O)) (FOr (FAtom 1) FTop) -*) - -eval normalize on (dualize (FImpl (FAtom 0) (FAnd (FAtom 1) FBot))). - -(* Spiegazione - =========== - - La funzione `invert` permette di invertire un mondo `v`. - Ovvero, per ogni indice di atomo `i`, se `v i` restituisce - `1` allora `(invert v) i` restituisce `0` e viceversa. - -*) -definition invert ≝ - λv:ℕ → ℕ. λx. if eqb (min (v x) 1) 0 then 1 else 0. - -interpretation "Inversione del mondo" 'invert v = (invert v). - -(*DOCBEGIN - -Il linguaggio di dimostrazione di Matita -======================================== - -Per dimostrare il lemma `negate_invert` in modo agevole è necessario -utilizzare il seguente comando: - -* by H1, H2 we proved P (H) - - Il comando `by ... we proved` visto nella scorsa esercitazione - permette di utilizzare più ipotesi o lemmi alla volta - separandoli con una virgola. - -DOCEND*) - -(* Esercizio 4 - =========== - - Dimostrare il lemma `negate_invert` che asserisce che - la semantica in un mondo `v` associato alla formula - negata di `F` e uguale alla semantica associata - a `F` in un mondo invertito. -*) -lemma negate_invert: - ∀F:Formula.∀v:ℕ→ℕ.[[ negate F ]]_v=[[ F ]]_(invert v). -assume F:Formula. -assume v:(ℕ→ℕ). -we proceed by induction on F to prove ([[ negate F ]]_v=[[ F ]]_(invert v)). - case FBot. - (*BEGIN*) - the thesis becomes ([[ negate FBot ]]_v=[[ FBot ]]_(invert v)). - (*END*) - done. - case FTop. - (*BEGIN*) - the thesis becomes ([[ negate FTop ]]_v=[[ FTop ]]_(invert v)). - (*END*) - done. - case FAtom. - assume n : ℕ. - the thesis becomes ((*BEGIN*)[[ negate (FAtom n) ]]_v=[[ FAtom n ]]_(invert v)(*END*)). - the thesis becomes ((*BEGIN*)1 - (min (v n) 1)= min (invert v n) 1(*END*)). - the thesis becomes (1 - (min (v n) 1)= min (if eqb (min (v n) 1) 0 then 1 else 0) 1). - by min_bool we proved (min (v n) 1 = 0 ∨ min (v n) 1 = 1) (H1); - we proceed by cases on (H1) to prove (1 - (min (v n) 1)= min (if eqb (min (v n) 1) 0 then 1 else 0) 1). - case Left. - conclude - (1 - (min (v n) 1)) - = (1 - 0) by H. - = 1. - = (min 1 1). - = (min (if true then 1 else O) 1). - = (min (if eqb 0 0 then 1 else O) 1). - = (min (if eqb (min (v n) 1) O then 1 else O) 1) by H. - done. - case Right. - (*BEGIN*) - conclude - (1 - (min (v n) 1)) - = (1 - 1) by H. - = 0. - = (min 0 1). - = (min (if eqb 1 0 then 1 else O) 1). - = (min (if eqb (min (v n) 1) O then 1 else O) 1) by H. - (*END*) - done. - case FAnd. - assume f : Formula. - by induction hypothesis we know - ((*BEGIN*)[[ negate f ]]_v=[[ f ]]_(invert v)(*END*)) (H). - assume f1 : Formula. - by induction hypothesis we know - ((*BEGIN*)[[ negate f1 ]]_v=[[ f1 ]]_(invert v)(*END*)) (H1). - the thesis becomes - ([[ negate (FAnd f f1) ]]_v=[[ FAnd f f1 ]]_(invert v)). - the thesis becomes - (min [[ negate f ]]_v [[ negate f1]]_v = [[ FAnd f f1 ]]_(invert v)). - conclude - (min [[ negate f ]]_v [[ negate f1]]_v) - = (min [[ f ]]_(invert v) [[ negate f1]]_v) by (*BEGIN*)H(*END*). - = (min [[ f ]]_(invert v) [[ f1]]_(invert v)) by (*BEGIN*)H1(*END*). - done. - case FOr. - (*BEGIN*) - assume f : Formula. - by induction hypothesis we know - ([[ negate f ]]_v=[[ f ]]_(invert v)) (H). - assume f1 : Formula. - by induction hypothesis we know - ([[ negate f1 ]]_v=[[ f1 ]]_(invert v)) (H1). - the thesis becomes - ([[ negate (FOr f f1) ]]_v=[[ FOr f f1 ]]_(invert v)). - the thesis becomes - (max [[ negate f ]]_v [[ negate f1]]_v = [[ FOr f f1 ]]_(invert v)). - conclude - (max [[ negate f ]]_v [[ negate f1]]_v) - = (max [[ f ]]_(invert v) [[ negate f1]]_v) by H. - = (max [[ f ]]_(invert v) [[ f1]]_(invert v)) by H1. - (*END*) - done. - case FImpl. - (*BEGIN*) - assume f : Formula. - by induction hypothesis we know - ([[ negate f ]]_v=[[ f ]]_(invert v)) (H). - assume f1 : Formula. - by induction hypothesis we know - ([[ negate f1 ]]_v=[[ f1 ]]_(invert v)) (H1). - the thesis becomes - ([[ negate (FImpl f f1) ]]_v=[[ FImpl f f1 ]]_(invert v)). - the thesis becomes - (max (1 - [[ negate f ]]_v) [[ negate f1]]_v = [[ FImpl f f1 ]]_(invert v)). - conclude - (max (1 - [[ negate f ]]_v) [[ negate f1]]_v) - = (max (1 - [[ f ]]_(invert v)) [[ negate f1]]_v) by H. - = (max (1 - [[ f ]]_(invert v)) [[ f1]]_(invert v)) by H1. - (*END*) - done. - case FNot. - (*BEGIN*) - assume f : Formula. - by induction hypothesis we know - ([[ negate f ]]_v=[[ f ]]_(invert v)) (H). - the thesis becomes - ([[ negate (FNot f) ]]_v=[[ FNot f ]]_(invert v)). - the thesis becomes - (1 - [[ negate f ]]_v=[[ FNot f ]]_(invert v)). - conclude (1 - [[ negate f ]]_v) = (1 - [[f]]_(invert v)) by H. - (*END*) - done. -qed. - -(* Esercizio 5 - =========== - - Dimostrare che la funzione negate rispetta l'equivalenza. -*) -lemma negate_fun: - ∀F:Formula.∀G:Formula.F ≡ G → negate F ≡ negate G. - assume (*BEGIN*)F:Formula(*END*). - assume (*BEGIN*)G:Formula(*END*). - suppose (*BEGIN*)(F ≡ G) (H)(*END*). - the thesis becomes (*BEGIN*)(negate F ≡ negate G)(*END*). - the thesis becomes (*BEGIN*)(∀v:ℕ→ℕ.[[ negate F ]]_v=[[ negate G ]]_v)(*END*). - assume v:(ℕ→ℕ). - conclude - [[ negate F ]]_v - = [[ F ]]_(invert v) by (*BEGIN*)negate_invert(*END*). - = [[ G ]]_((*BEGIN*)invert v(*BEGIN*)) by (*BEGIN*)H(*BEGIN*). - = [[ negate G ]]_(*BEGIN*)v(*BEGIN*) by (*BEGIN*)negate_invert(*END*). - done. -qed. - -(* Esercizio 6 - =========== - - Dimostrare che per ogni formula `F`, `(negate F)` equivale a - dualizzarla e negarla. -*) -lemma not_dualize_eq_negate: - ∀F:Formula.negate F ≡ FNot (dualize F). - (*BEGIN*) - assume F:Formula. - the thesis becomes (∀v:ℕ→ℕ.[[negate F]]_v=[[FNot (dualize F)]]_v). - (*END*) - assume v:(ℕ→ℕ). - we proceed by induction on F to prove ([[negate F]]_v=[[FNot (dualize F)]]_v). - case FBot. - (*BEGIN*) - the thesis becomes ([[ negate FBot ]]_v=[[ FNot (dualize FBot) ]]_v). - (*END*) - done. - case FTop. - (*BEGIN*) - the thesis becomes ([[ negate FTop ]]_v=[[ FNot (dualize FTop) ]]_v). - (*END*) - done. - case FAtom. - (*BEGIN*) - assume n : ℕ. - the thesis becomes ([[ negate (FAtom n) ]]_v=[[ FNot (dualize (FAtom n)) ]]_v). - (*END*) - done. - case FAnd. - assume f : Formula. - by induction hypothesis we know - ([[ negate f ]]_v=[[ FNot (dualize f) ]]_v) (H). - assume f1 : Formula. - by induction hypothesis we know - ([[ negate f1 ]]_v=[[ FNot (dualize f1) ]]_v) (H1). - the thesis becomes - ([[ negate (FAnd f f1) ]]_v=[[ FNot (dualize (FAnd f f1)) ]]_v). - the thesis becomes - (min [[ negate f ]]_v [[ negate f1 ]]_v=[[ FNot (dualize (FAnd f f1)) ]]_v). - conclude - (min (*BEGIN*)[[ negate f ]]_v(*END*) (*BEGIN*)[[ negate f1 ]]_v(*END*)) - = (min (*BEGIN*)[[ FNot (dualize f) ]]_v(*END*) (*BEGIN*)[[ negate f1 ]]_v(*END*)) by H. - = (min (*BEGIN*)[[ FNot (dualize f) ]]_v(*END*) (*BEGIN*)[[ FNot (dualize f1) ]]_v(*END*)) by H1. - = (min (1 - [[ dualize f ]]_v) (1 - [[ dualize f1 ]]_v)). - = (1 - (max [[ dualize f ]]_v [[ dualize f1 ]]_v)) by min_max. - done. - case FOr. - (*BEGIN*) - assume f : Formula. - by induction hypothesis we know - ([[ negate f ]]_v=[[ FNot (dualize f) ]]_v) (H). - assume f1 : Formula. - by induction hypothesis we know - ([[ negate f1 ]]_v=[[ FNot (dualize f1) ]]_v) (H1). - the thesis becomes - ([[ negate (FOr f f1) ]]_v=[[ FNot (dualize (FOr f f1)) ]]_v). - the thesis becomes - (max [[ negate f ]]_v [[ negate f1 ]]_v=[[ FNot (dualize (FOr f f1)) ]]_v). - conclude - (max [[ negate f ]]_v [[ negate f1 ]]_v) - = (max [[ FNot (dualize f) ]]_v [[ negate f1 ]]_v) by H. - = (max [[ FNot (dualize f) ]]_v [[ FNot (dualize f1) ]]_v) by H1. - = (max (1 - [[ dualize f ]]_v) (1 - [[ dualize f1 ]]_v)). - = (1 - (min [[ dualize f ]]_v [[ dualize f1 ]]_v)) by max_min. - (*END*) - done. - case FImpl. - (*BEGIN*) - assume f : Formula. - by induction hypothesis we know - ([[ negate f ]]_v=[[ FNot (dualize f) ]]_v) (H). - assume f1 : Formula. - by induction hypothesis we know - ([[ negate f1 ]]_v=[[ FNot (dualize f1) ]]_v) (H1). - the thesis becomes - ([[ negate (FImpl f f1) ]]_v=[[ FNot (dualize (FImpl f f1)) ]]_v). - the thesis becomes - (max (1 - [[ negate f ]]_v) [[ negate f1 ]]_v=[[ FNot (dualize (FImpl f f1)) ]]_v). - conclude - (max (1-[[ negate f ]]_v) [[ negate f1 ]]_v) - = (max (1-[[ FNot (dualize f) ]]_v) [[ negate f1 ]]_v) by H. - = (max (1-[[ FNot (dualize f) ]]_v) [[ FNot (dualize f1) ]]_v) by H1. - = (max (1 - [[ FNot (dualize f) ]]_v) (1 - [[ dualize f1 ]]_v)). - = (1 - (min [[ FNot (dualize f) ]]_v [[ dualize f1 ]]_v)) by max_min. - (*END*) - done. - case FNot. - (*BEGIN*) - assume f : Formula. - by induction hypothesis we know - ([[ negate f ]]_v=[[ FNot (dualize f) ]]_v) (H). - the thesis becomes - ([[ negate (FNot f) ]]_v=[[ FNot (dualize (FNot f)) ]]_v). - the thesis becomes - (1 - [[ negate f ]]_v=[[ FNot (dualize (FNot f)) ]]_v). - conclude (1 - [[ negate f ]]_v) = (1 - [[ FNot (dualize f) ]]_v) by H. - (*END*) - done. -qed. - -(* Esercizio 7 - =========== - - Dimostrare che la negazione è iniettiva -*) -theorem not_inj: - ∀F,G:Formula.FNot F ≡ FNot G→F ≡ G. - (*BEGIN*) - assume F:Formula. - assume G:Formula. - suppose (FNot F ≡ FNot G) (H). - the thesis becomes (F ≡ G). - the thesis becomes (∀v:ℕ→ℕ.[[ F ]]_v=[[ G ]]_v). - (*END*) - assume v:(ℕ→ℕ). - by sem_le_1 we proved ([[F]]_v ≤ 1) (H1). - by (*BEGIN*)sem_le_1(*END*) we proved ([[G]]_v ≤ 1) (H2). - by min_1_1, H1 we proved (1 - (1 - [[F]]_v) = [[F]]_v) (H3). - by (*BEGIN*)min_1_1, H2(*END*) we proved ((*BEGIN*)1 - (1 - [[G]]_v)(*END*) = [[G]]_v) (H4). - conclude - ([[F]]_v) - = (1 - (1 - [[F]]_v)) by (*BEGIN*)H3(*END*). - = (1 - [[(*BEGIN*)FNot F(*END*)]]_v). - = (1 - [[ FNot G]]_v) by H. - = (1 - (*BEGIN*)(1 - [[G]]_v)(*END*)). - = [[G]]_v by (*BEGIN*)H4(*END*). - done. -qed. - -(*DOCBEGIN - -La prova del teorema di dualità -=============================== - -Il teorema di dualità accennato a lezione dice che se due formule -`F1` ed `F2` sono equivalenti, allora anche le formule duali lo sono. - - ∀F1,F2:Formula. F1 ≡ F2 → dualize F1 ≡ dualize F2. - -Per dimostrare tale teorema è bene suddividere la prova in lemmi intermedi - -1. lemma `negate_invert`, dimostrato per induzione su F, utilizzando - `min_bool` - - ∀F:Formula.∀v:ℕ→ℕ.[[ negate F ]]_v=[[ F ]]_(invert v). - -2. lemma `negate_fun`, conseguenza di `negate_invert` - - ∀F,G:Formula. F ≡ G → negate F ≡ negate G. - -2. lemma `not_dualize_eq_negate`, dimostrato per induzione su F, - utilizzando `max_min` e `min_max` - - ∀F:Formula. negate F ≡ FNot (dualize F) - -4. lemma `not_inj`, conseguenza di `sem_bool` - - ∀F,G:Formula. FNot F ≡ FNot G → F ≡ G - -Una volta dimostrati tali lemmi la prova del teorema di dualità -procede come di seguito: - -1. Assume l'ipotesi - - F1 ≡ F2 - -2. Utilizza `negate_fun` per ottenere - - negate F1 ≡ negate F2 - -3. Utilizzando due volte il lemma `not_dualize_eq_negate` e il lemma - `equiv_rewrite` ottiene - - FNot (dualize F1) ≡ FNot (dualize F2) - -4. Conclude utilizzando il lemma `not_inj` per ottenere la tesi - - dualize F1 ≡ dualize F2 - -DOCEND*) - -(* Esercizio 8 - =========== - - Dimostrare il teorema di dualità -*) -theorem duality: ∀F1,F2:Formula.F1 ≡ F2 → dualize F1 ≡ dualize F2. - assume F1:Formula. - assume F2:Formula. - suppose (F1 ≡ F2) (H). - the thesis becomes (dualize F1 ≡ dualize F2). - by (*BEGIN*)negate_fun(*END*), H we proved (negate F1 ≡ negate F2) (H1). - by (*BEGIN*)not_dualize_eq_negate(*END*), (*BEGIN*)equiv_rewrite(*END*), H1 we proved (FNot (dualize F1) ≡ negate F2) (H2). - by (*BEGIN*)not_dualize_eq_negate(*END*), (*BEGIN*)equiv_rewrite(*END*), H2 we proved (FNot (dualize F1) ≡ FNot (dualize F2)) (H3). - by (*BEGIN*)not_inj(*END*), H3 we proved (dualize F1 ≡ dualize F2) (H4). - by H4 done. -qed. diff --git a/helm/software/matita/contribs/didactic/induction.ma b/helm/software/matita/contribs/didactic/induction.ma deleted file mode 100644 index c4335ca3e..000000000 --- a/helm/software/matita/contribs/didactic/induction.ma +++ /dev/null @@ -1,568 +0,0 @@ -(* Esercitazione di logica 22/10/2008. *) - -(* Nota per gli studenti - ===================== - - * La lezione del pomeriggio con il Prof. Sacerdoti si terrà in aula - Pinkerle e non Cremona. - - * Un piccolo manuale sul software Matita è disponibile al seguente URL: - - http://mowgli.cs.unibo.it/~tassi/exercise-induction.ma.html - -*) - -(* Esercizio 0 - =========== - - Compilare i seguenti campi: - - Nome1: ... - Cognome1: ... - Matricola1: ... - Account1: ... - - Nome2: ... - Cognome2: ... - Matricola2: ... - Account2: ... - - Prima di abbandonare la postazione: - - * compilare il questionario in fondo al file - - * salvare il file (menu `File ▹ Save as ...`) nella directory (cartella) - /public/ con nome linguaggi_Account1.ma, ad esempio Mario Rossi, il cui - account è mrossi, deve salvare il file in /public/linguaggi_mrossi.ma - - * mandatevi via email o stampate il file. Per stampare potete usare - usare l'editor gedit che offre la funzionalità di stampa -*) - -(*DOCBEGIN - -Come scrivere i simboli -======================= - -Per inserire i simboli matematici è necessario digitare il loro nome -e poi premere ALT-L. In generale i nomi dei simboli sono della forma -`\nome`, ad esempio `\equiv`. Alcuni simboli molto frequenti hanno -dei sinonimi più comodi da digitare, per esemio `⇒` ha sia il nome -`\Rightarrow` sia `=>`. - -Segue un elenco dei simboli più comuni e i loro nomi separati da virgola, -Se sono necessari dei simboli non riportati di seguito si può visualizzare -l'intera lista dal menù a tendina `View ▹ TeX/UTF8 table`. - -* `→` : `\to`, `->` -* `⇒` : `\Rightarrow`, `=>` -* `ℕ` : `\naturals` -* `≝` : `\def`, `:=` -* `≡` : `\equiv` -* `∀` : `\forall` - -La sintassi `∀x.P` significa "per tutti gli `x` vale `P`". - -La sintassi `F → G` dove `F` e `G` sono proposizioni nel metalinguaggio -significa "`F` implica `G`". Attenzione, il simbolo `⇒` (usato a lezione) -non ha lo stesso significato in Matita. - -La sintassi `ℕ → ℕ` è il tipo delle funzioni che preso un numero naturale -restituiscono un numero naturale. - -La sintassi di Matita -===================== - -Il linguaggio di Matita si basa sul λ-calcolo CIC, la cui sintassi si -differenzia in vari aspetti da quella che solitamente viene utilizzata -per fare matematica, e ricorda quella di Scheme che state vedendo nel corso -di programmazione. - -* applicazione - - Se `f` è una funzione che si aspetta due argomenti, l'applucazione di `f` - agli argomenti `x` e `y` si scrive `(f x y)` e non `f(x,y)`. Le parentesi - possono essere omesse se il senso è chiaro dal contesto. In particolare - vengono omesse quando l'applicazione è argomento di un operatore binario. - Esempio: `f x y + f y x` si legge `(f x y) + (f y x)`. - -* minimo e massimo - - Le funzioni `min` e `max` non fanno eccezione, per calcolare il - massimo tra `x` e `y` si scrive `(max x y)` e non `max{x,y}` - -* Le funzioni definite per ricorsione strutturale utilizzano il costrutto - `let rec` (ricorsione) e il costrutto `match` (analisi per casi). - - Ad esempio la funzione count definita a lezione come - - count ⊤ ≝ 1 - count (F1 ∧ F2) ≝ 1 + count F1 + count F2 - ... - - la si esprime come - - let rec count F on F ≝ - match F with - [ ⊤ ⇒ 1 - | F1 ∧ F2 ⇒ 1 + count F1 + count F2 - ... - ]. - -* Per dare la definizione ricorsiva (di un linguaggio) si usa una sintassi - simile a BNF. Per esempio per definire - - ::= "+" | "*" | "0" | "1" - - si usa il seguente comando - - inductive A : Type ≝ - | Plus : A → A → A - | Times : A → A → A - | Zero : A - | One : A - . - -La ratio è che `Plus` prende due argomenti di tipo `A` per darmi un `A`, -mentre `Zero` non prende nessun argomento per darmi un `A`. Al posto di usare -operatori infissi `(0 + 0)` la definizione crea operatori prefissi (funzioni). -Quindi `(0+0)` si scriverà come `(Plus Zero Zero)`. - -DOCEND*) - -(* ATTENZIONE - ========== - - Non modificare le seguenti tre righe -*) -include "nat/minus.ma". -definition max : nat → nat → nat ≝ λa,b:nat.let rec max n m on n ≝ match n with [ O ⇒ b | S n ⇒ match m with [ O ⇒ a | S m ⇒ max n m]] in max a b. -definition min : nat → nat → nat ≝ λa,b:nat.let rec min n m on n ≝ match n with [ O ⇒ a | S n ⇒ match m with [ O ⇒ b | S m ⇒ min n m]] in min a b. - - -(* Esercizio 1 - =========== - - Definire il linguaggio delle formule riempiendo gli spazi -*) -inductive Formula : Type ≝ -| FBot: Formula -| FTop: (*BEGIN*)Formula(*END*) -| FAtom: nat → Formula (* usiamo i naturali al posto delle lettere *) -| FAnd: Formula → Formula → Formula -| FOr: (*BEGIN*)Formula → Formula → Formula(*END*) -| FImpl: (*BEGIN*)Formula → Formula → Formula(*END*) -| FNot: (*BEGIN*)Formula → Formula(*END*) -. - - -(* Esercizio 2 - =========== - - Data la funzione di valutazione per gli atomi `v`, definire la - funzione `sem` per una generica formula `F` che vi associa la semantica - (o denotazione) -*) -let rec sem (v: nat → nat) (F: Formula) on F ≝ - match F with - [ FBot ⇒ 0 - | FTop ⇒ (*BEGIN*)1(*END*) - (*BEGIN*) - | FAtom n ⇒ v n - (*END*) - | FAnd F1 F2 ⇒ (*BEGIN*)min (sem v F1) (sem v F2)(*END*) - (*BEGIN*) - | FOr F1 F2 ⇒ max (sem v F1) (sem v F2) - | FImpl F1 F2 ⇒ max (1 - sem v F1) (sem v F2) - (*END*) - | FNot F1 ⇒ 1 - (sem v F1) - ] -. - -(* NOTA - ==== - - I comandi che seguono definiscono la seguente notazione: - - if e then risultato1 else risultato2 - - Questa notazione permette di valutare l'espressione `e`. Se questa - è vera restituisce `risultato1`, altrimenti restituisce `risultato2`. - - Un esempio di espressione è `eqb n m`, che confronta i due numeri naturali - `n` ed `m`. - - * [[ formula ]]_v - - Questa notazione utilizza la funzione `sem` precedentemente definita, in - particolare `[[ f ]]_v` è una abbreviazione per `sem v f`. - - - ATTENZIONE - ========== - - Non modificare le linee seguenti -*) -definition if_then_else ≝ λT:Type.λe,t,f.match e return λ_.T with [ true ⇒ t | false ⇒ f]. -notation > "'if' term 19 e 'then' term 19 t 'else' term 90 f" non associative with precedence 90 for @{ 'if_then_else $e $t $f }. -notation < "'if' \nbsp term 19 e \nbsp 'then' \nbsp term 19 t \nbsp 'else' \nbsp term 90 f \nbsp" non associative with precedence 90 for @{ 'if_then_else $e $t $f }. -interpretation "Formula if_then_else" 'if_then_else e t f = (if_then_else _ e t f). -notation < "[[ \nbsp term 19 a \nbsp ]] \nbsp \sub term 90 v" non associative with precedence 90 for @{ 'semantics $v $a }. -notation > "[[ term 19 a ]] \sub term 90 v" non associative with precedence 90 for @{ 'semantics $v $a }. -notation > "[[ term 19 a ]]_ term 90 v" non associative with precedence 90 for @{ sem $v $a }. -interpretation "Semantic of Formula" 'semantics v a = (sem v a). - - -(* Test 1 - ====== - - Viene fornita una funzione di valutazione di esempio chiamata `v1101`. - Tale funzione associa agli atomi 0, 1 e 3 un valore pari a 1, - invece a 2,4,5,6... un valore pari a 0. - - Viene fornita una formula di esempio chiamata `esempio1` che rappresenta - la formula - - D => (C ∨ (B ∧ A)) - - Dove A è rappresentato con l'atomo 0, B con l'atomo 1, ... - - Tale formula è valida per la funzione di valutazione `v1101`. - - Il comando `eval normalize [[ esempio1 ]]_v1101` permette di calcolare - la funzione `sem` che avete appena definito. Tale funzione deve - computare a 1 (verrà mostrata una finestra col risultato). - Se così non fosse significa che avete commesso un errore nella - definizione di `sem` e prima di continuare è necessario che la sistemiate. -*) -definition v1101 ≝ λx. - if eqb x 0 then 1 (* FAtom 0 ↦ 1 *) - else if eqb x 1 then 1 (* FAtom 1 ↦ 1 *) - else if eqb x 2 then 0 (* FAtom 2 ↦ 0 *) - else if eqb x 3 then 1 (* FAtom 3 ↦ 1 *) - else 0. (* FAtom _ ↦ 0 *) - - -definition esempio1 ≝ - (FImpl (FNot (FAtom 3)) (FOr (FAtom 2) (FAnd (FAtom 1) (FAtom 0)))). - -eval normalize on [[ esempio1 ]]_v1101. - - -(* Esercizio 3 - =========== - - Definire la funzione di sostituzione di una formula `G` al posto - degli atomi uguali a `x` in una formula `F`. -*) -let rec subst (x:nat) (G: Formula) (F: Formula) on F ≝ - match F with - [ FBot ⇒ FBot - | FTop ⇒ (*BEGIN*)FTop(*END*) - | FAtom n ⇒ if (*BEGIN*)eqb n x(*END*) then (*BEGIN*)G(*END*) else ((*BEGIN*)FAtom n(*END*)) - (*BEGIN*) - | FAnd F1 F2 ⇒ FAnd (subst x G F1) (subst x G F2) - | FOr F1 F2 ⇒ FOr (subst x G F1) (subst x G F2) - | FImpl F1 F2 ⇒ FImpl (subst x G F1) (subst x G F2) - (*END*) - | FNot F ⇒ FNot (subst x G F) - ]. - - -(* NOTA - ==== - - I comandi che seguono definiscono la seguente notazione: - - * F [ G / x ] - - Questa notazione utilizza la funzione `subst` appena definita, in particolare - la scrittura `F [ G /x ]` è una abbreviazione per `subst x G F`. - - * F ≡ G - - Questa notazione è una abbreviazione per `∀v.[[ f ]]_v = [[ g ]]_v`. - Asserisce che for ogni funzione di valutazione `v`, la semantica di `f` - in `v` è uguale alla semantica di `g` in `v`. - - - ATTENZIONE - ========== - - Non modificare le linee seguenti -*) -notation < "t [ \nbsp term 19 a / term 19 b \nbsp ]" non associative with precedence 90 for @{ 'substitution $b $a $t }. -notation > "t [ term 90 a / term 90 b]" non associative with precedence 90 for @{ 'substitution $b $a $t }. -interpretation "Substitution for Formula" 'substitution b a t = (subst b a t). -definition equiv ≝ λF1,F2. ∀v.[[ F1 ]]_v = [[ F2 ]]_v. -notation "hvbox(a \nbsp break mstyle color #0000ff (≡) \nbsp b)" non associative with precedence 45 for @{ 'equivF $a $b }. -notation > "a ≡ b" non associative with precedence 50 for @{ equiv $a $b }. -interpretation "equivalence for Formulas" 'equivF a b = (equiv a b). - -(* Test 2 - ====== - - Viene fornita una formula di esempio `esempio2`, - e una formula `esempio3` che rimpiazzerà gli atomi - `FAtom 2` di `esempio2`. - - Il risultato atteso è la formula: - - FAnd (FImpl (FOr (FAtom O) (FAtom 1)) (FAtom 1)) - (FOr (FAtom O) (FAtom 1)) - -*) - -definition esempio2 ≝ (FAnd (FImpl (FAtom 2) (FAtom 1)) (FAtom 2)). - -definition esempio3 ≝ (FOr (FAtom 0) (FAtom 1)). - -eval normalize on (esempio2 [ esempio3 / 2]). - -(*DOCBEGIN - -Il linguaggio di dimostrazione di Matita -======================================== - -L'ultimo esercizio richiede di scrivere una dimostrazione. Tale dimostrazione -deve essere scritta utilizzando il linguaggio di dimostrazione di Matita. -Tale linguaggio è composto dai seguenti comandi: - -* `assume nome : tipo` - - Quando si deve dimostrare un tesi come `∀F : Formula.P`, il comando - `assume F : Formula` fissa una generica `Formula` `F` e la tesi - diventa `P` dove `F` è fissata. - -* `suppose P (nome)` - - Quando si deve dimostrare una tesi come `P → Q`, il comando - `suppose P (Ipotesi1)` da il nome `Ipotesi1` a `P` e cambia la tesi - `Q`, che ora può essere dimostrata facendo riferimento all'assunzione - `P` tramite il nome `Ipotesi1`. - -* `we procede by induction on F to prove Q` - - Se `F` è il nome di una (ad esempio) `Formula` precedentemente - assunta tramite il comando `assume`, inizia una prova per induzione su `F`. - -* `case name` - - Nelle prove per induzione o per casi, ogni caso deve iniziare con il - comando `case nome`, ad esempio se si procede per induzione di una - formula uno dei casi sarà quello in cui la formula è `⊥`, si deve quindi - iniziare la sotto dimostrazione per tale caso con `case ⊥`. - -* `we procede by cases on x to prove Q` - - Analogo a `we procede by induction on F to prove Q` - -* `by induction hypothesis we know P (name)` - - Nei casi non base di una prova per induzione sono disponibili delle ipotesi - induttive, quindi la tesi è della forma `P → Q`, ed è possibile - dare un nome a `P` e procedere a dimostrare `Q`. Simile a `suppose`. - -* `the thesis becomes P` - - Permette di modificare la tesi, utilizzando le definizioni (eventualmente - ricorsive) che vi compaiono. Ad esempio se la tesi fosse `min 3 5 = max 1 3` - si potrebbe usare il comando `the thesis becomes (3 = max 1 3)` in quanto - per definizione di minimo, il minimo tra `3` e `5` è `3`. - -* `by name1 we proved P (name2)` - - Permette di ottenere una nuova ipotesi `P` chiamandola `name2` utilizzando - l'ipotesi `name1`. - -* `conclude (P) = (Q) by name` - - Quando la tesi è della forma `P = Q`, si possono utilizzare delle ipotesi - della forma `A = B` riscrivendo `A` in `B` (o viceversa) in `P`. Per esempio - se la tesi fosse `sin π + 3 = 7 - 4` e si avesse una ipotesi `sin π = 0` dal - nome `H`, si potrebbe usare il comando `conclude (sin π + 3) = (0 + 3) by H` - per cambiare la conclusione in `0 + 3 = 7 - 4`. - -* `= (P) by name` - - Da utilizzare in seguito a un comando `conclude` per riscrivere con altre - ipotesi. - -* `done` - - Termina un caso della dimostrazione, è possibile utilizzarlo quando la tesi - è della forma `t = t`, ad esempio `0 = 0` oppure `v x = v x`. - -DOCEND*) - -(* Esercizio 4 - =========== - - Dimostra il teorema di sostituzione visto a lezione -*) -theorem sostituzione: ∀G1,G2,F,x. G1 ≡ G2 → F[G1/x] ≡ F[G2/x]. -assume G1 : Formula. -assume G2 : Formula. -(*BEGIN*) -assume F : Formula. -assume x : ℕ. -(*END*) -suppose (G1 ≡ G2) (H). -we proceed by induction on F to prove (F[ G1/x ] ≡ F[ G2/x ]). -case FBot. - the thesis becomes (FBot[ G1/x ] ≡ FBot[ G2/x ]). - the thesis becomes (FBot ≡ FBot[ G2/x ]). - the thesis becomes (FBot ≡ FBot). - the thesis becomes (∀v.[[FBot]]_v = [[FBot]]_v). - assume v : (ℕ → ℕ). - the thesis becomes (0 = [[FBot]]_v). - the thesis becomes (0 = 0). - done. -case FTop. - (*BEGIN*) - the thesis becomes (FTop[ G1/x ] ≡ FTop[ G2/x ]). - the thesis becomes (FTop ≡ FTop). - the thesis becomes (∀v. [[FTop]]_v = [[FTop]]_v). - assume v : (ℕ → ℕ). - the thesis becomes (1 = 1). - (*END*) - done. -case FAtom. - assume n : ℕ. - the thesis becomes ((FAtom n)[ G1/x ] ≡ (FAtom n)[ G2/x ]). - the thesis becomes - (if eqb n x then G1 else (FAtom n) ≡ (FAtom n)[ G2/x ]). - the thesis becomes - (if eqb n x then G1 else (FAtom n) ≡ - if eqb n x then G2 else (FAtom n)). - we proceed by cases on (eqb n x) to prove - (if eqb n x then G1 else (FAtom n) ≡ - if eqb n x then G2 else (FAtom n)). - case true. - the thesis becomes (G1 ≡ G2). - by H done. - case false. - (*BEGIN*) - the thesis becomes (FAtom n ≡ FAtom n). - the thesis becomes (∀v. [[FAtom n]]_v = [[FAtom n]]_v). - assume v : (ℕ → ℕ). - the thesis becomes (v n = v n). - (*END*) - done. -case FAnd. - assume F1 : Formula. - by induction hypothesis we know (F1[ G1/x ] ≡ F1[ G2/x ]) (IH1). - assume F2 : Formula. - by induction hypothesis we know (F2[ G1/x ] ≡ F2[ G2/x ]) (IH2). - the thesis becomes - (∀v.[[ (FAnd F1 F2)[ G1/x ] ]]_v = [[ (FAnd F1 F2)[ G2/x ] ]]_v). - assume v : (ℕ → ℕ). - the thesis becomes - (min ([[ F1[ G1/x ] ]]_v) ([[ F2[ G1/x ] ]]_v) = - min ([[ F1[ G2/x ] ]]_v) ([[ F2[ G2/x ] ]]_v)). - by IH1 we proved (∀v1.[[ F1[ G1/x ] ]]_v1 = [[ F1[ G2/x ] ]]_v1) (IH11). - by (*BEGIN*)IH2(*END*) we proved (∀v2.[[ F2[ G1/x ] ]]_v2 = [[ F2[ G2/x ] ]]_v2) (IH22). - by IH11 we proved ([[ F1[ G1/x ] ]]_v = [[ F1[ G2/x ] ]]_v) (IH111). - by (*BEGIN*)IH22(*END*) we proved ([[ F2[ G1/x ] ]]_v = [[ F2[ G2/x ] ]]_v) (IH222). - conclude - (min ([[ F1[ G1/x ] ]]_v) ([[ F2[ G1/x ] ]]_v)) - = (min ([[ F1[ G2/x ] ]]_v) ([[ F2[ G1/x ] ]]_v)) by IH222. - = (min ([[(F1[ G2/x ])]]_v) ([[(F2[ G2/x ])]]_v)) by (*BEGIN*)IH111(*END*). - (*END*) - done. -case FOr. - (*BEGIN*) - assume F1 : Formula. - by induction hypothesis we know (F1[ G1/x ] ≡ F1[ G2/x ]) (IH1). - assume F2 : Formula. - by induction hypothesis we know (F2[ G1/x ] ≡ F2[ G2/x ]) (IH2). - the thesis becomes - (∀v.[[ (FOr F1 F2)[ G1/x ] ]]_v = [[ (FOr F1 F2)[ G2/x ] ]]_v). - assume v : (ℕ → ℕ). - the thesis becomes - (max ([[ F1[ G1/x ] ]]_v) ([[ F2[ G1/x ] ]]_v) = - max ([[ F1[ G2/x ] ]]_v) ([[ F2[ G2/x ] ]]_v)). - by IH1 we proved (∀v1.[[ F1[ G1/x ] ]]_v1 = [[ F1[ G2/x ] ]]_v1) (IH11). - by IH2 we proved (∀v2.[[ F2[ G1/x ] ]]_v2 = [[ F2[ G2/x ] ]]_v2) (IH22). - by IH11 we proved ([[ F1[ G1/x ] ]]_v = [[ F1[ G2/x ] ]]_v) (IH111). - by IH22 we proved ([[ F2[ G1/x ] ]]_v = [[ F2[ G2/x ] ]]_v) (IH222). - conclude - (max ([[ F1[ G1/x ] ]]_v) ([[ F2[ G1/x ] ]]_v)) - = (max ([[ F1[ G2/x ] ]]_v) ([[ F2[ G1/x ] ]]_v)) by IH222. - = (max ([[(F1[ G2/x ])]]_v) ([[(F2[ G2/x ])]]_v)) by IH111. - (*END*) - done. -case FImpl. - (*BEGIN*) - assume F1 : Formula. - by induction hypothesis we know (F1[ G1/x ] ≡ F1[ G2/x ]) (IH1). - assume F2 : Formula. - by induction hypothesis we know (F2[ G1/x ] ≡ F2[ G2/x ]) (IH2). - the thesis becomes - (∀v.max (1 - [[ F1[ G1/x ] ]]_v) ([[ F2[ G1/x ] ]]_v) = - max (1 - [[ F1[ G2/x ] ]]_v) ([[ F2[ G2/x ] ]]_v)). - assume v : (ℕ → ℕ). - by IH1 we proved ([[ F1[ G1/x ] ]]_v = [[ F1[ G2/x ] ]]_v) (IH11). - by IH2 we proved ([[ F2[ G1/x ] ]]_v = [[ F2[ G2/x ] ]]_v) (IH22). - conclude - (max (1-[[ F1[ G1/x ] ]]_v) ([[ F2[ G1/x ] ]]_v)) - = (max (1-[[ F1[ G2/x ] ]]_v) ([[ F2[ G1/x ] ]]_v)) by IH11. - = (max (1-[[ F1[ G2/x ] ]]_v) ([[ F2[ G2/x ] ]]_v)) by IH22. - done. -case FNot. - (*BEGIN*) - assume F1 : Formula. - by induction hypothesis we know (F1[ G1/x ] ≡ F1[ G2/x ]) (IH). - the thesis becomes (FNot (F1[ G1/x ]) ≡ FNot (F1[ G2/x ])). - the thesis becomes (∀v.[[FNot (F1[ G1/x ])]]_v = [[FNot (F1[ G2/x ])]]_v). - assume v : (ℕ → ℕ). - the thesis becomes (1 - [[F1[ G1/x ]]]_v = [[FNot (F1[ G2/x ])]]_v). - the thesis becomes (1 - [[ F1[ G1/x ] ]]_v = 1 - [[ F1[ G2/x ] ]]_v). - by IH we proved (∀v1.[[ F1[ G1/x ] ]]_v1 = [[ F1[ G2/x ] ]]_v1) (IH1). - by IH1 we proved ([[ F1[ G1/x ] ]]_v = [[ F1[ G2/x ] ]]_v) (IH2). - conclude - (1-[[ F1[ G1/x ] ]]_v) - = (1-[[ F1[ G2/x ] ]]_v) by IH2. - (*END*) - done. -qed. - -(* Questionario - - Compilare mettendo una X nella risposta scelta. - - 1) Pensi che sia utile l'integrazione del corso con una attività di - laboratorio? - - [ ] per niente [ ] poco [ ] molto - - - 2) Pensi che gli esercizi proposti ti siano stati utili a capire meglio - quanto visto a lezione? - - [ ] per niente [ ] poco [ ] molto - - - 3) Gli esercizi erano - - [ ] troppo facili [ ] alla tua portata [ ] impossibili - - - 4) Il tempo a disposizione è stato - - [ ] poco [ ] giusto [ ] troppo - - - 5) Cose che miglioreresti nel software Matita - - ......... - - - 6) Suggerimenti sullo svolgimento delle attività in laboratorio - - ......... - - -*) - - diff --git a/helm/software/matita/contribs/didactic/shannon.ma b/helm/software/matita/contribs/didactic/shannon.ma deleted file mode 100644 index f708c19ba..000000000 --- a/helm/software/matita/contribs/didactic/shannon.ma +++ /dev/null @@ -1,519 +0,0 @@ -(* Esercizio -1 - ============ - - 1. Leggere ATTENTAMENTE, e magari stampare, la documentazione - reperibile all'URL seguente: - - http://mowgli.cs.unibo.it/~tassi/exercise-shannon.ma.html - - 2. Questa volta si fa sul serio: - - l'esercizio proposto è MOLTO difficile, occorre la vostra massima - concentrazione (leggi: niente cut&paste selvaggio) - -*) - - -(* Esercizio 0 - =========== - - Compilare i seguenti campi: - - Nome1: ... - Cognome1: ... - Matricola1: ... - Account1: ... - - Nome2: ... - Cognome2: ... - Matricola2: ... - Account2: ... - -*) - -(* ATTENZIONE - ========== - - Non modificare quanto segue -*) -include "nat/minus.ma". -definition if_then_else ≝ λT:Type.λe,t,f.match e return λ_.T with [ true ⇒ t | false ⇒ f]. -notation > "'if' term 19 e 'then' term 19 t 'else' term 90 f" non associative with precedence 19 for @{ 'if_then_else $e $t $f }. -notation < "'if' \nbsp term 19 e \nbsp 'then' \nbsp term 19 t \nbsp 'else' \nbsp term 90 f \nbsp" non associative with precedence 19 for @{ 'if_then_else $e $t $f }. -interpretation "Formula if_then_else" 'if_then_else e t f = (if_then_else _ e t f). -definition max ≝ λn,m. if eqb (n - m) 0 then m else n. -definition min ≝ λn,m. if eqb (n - m) 0 then n else m. - -(* Ripasso 1 - ========= - - Il linguaggio delle formule, dove gli atomi sono - rapperesentati da un numero naturale -*) -inductive Formula : Type ≝ -| FBot: Formula -| FTop: Formula -| FAtom: nat → Formula -| FAnd: Formula → Formula → Formula -| FOr: Formula → Formula → Formula -| FImpl: Formula → Formula → Formula -| FNot: Formula → Formula -. - -(* Ripasso 2 - ========= - - La semantica di una formula `F` in un mondo `v`: `[[ F ]]_v` -*) -let rec sem (v: nat → nat) (F: Formula) on F : nat ≝ - match F with - [ FBot ⇒ 0 - | FTop ⇒ 1 - | FAtom n ⇒ min (v n) 1 - | FAnd F1 F2 ⇒ min (sem v F1) (sem v F2) - | FOr F1 F2 ⇒ max (sem v F1) (sem v F2) - | FImpl F1 F2 ⇒ max (1 - sem v F1) (sem v F2) - | FNot F1 ⇒ 1 - (sem v F1) - ] -. - -(* ATTENZIONE - ========== - - Non modificare quanto segue. -*) -notation < "[[ \nbsp term 19 a \nbsp ]] \nbsp \sub term 90 v" non associative with precedence 90 for @{ 'semantics $v $a }. -notation > "[[ term 19 a ]] \sub term 90 v" non associative with precedence 90 for @{ 'semantics $v $a }. -notation > "[[ term 19 a ]]_ term 90 v" non associative with precedence 90 for @{ sem $v $a }. -interpretation "Semantic of Formula" 'semantics v a = (sem v a). -lemma sem_bool : ∀F,v. [[ F ]]_v = 0 ∨ [[ F ]]_v = 1. intros; elim F; simplify; [left;reflexivity; |right;reflexivity; |cases (v n);[left;|cases n1;right;]reflexivity; |4,5,6: cases H; cases H1; rewrite > H2; rewrite > H3; simplify; first [ left;reflexivity | right; reflexivity ]. |cases H; rewrite > H1; simplify;[right|left]reflexivity;] qed. - -(* Ripasso 3 - ========= - - L'operazione di sostituzione di una formula `G` al posto dell'atomo - `x` in una formula `F`: `F[G/x]` -*) - -let rec subst (x:nat) (G: Formula) (F: Formula) on F ≝ - match F with - [ FBot ⇒ FBot - | FTop ⇒ FTop - | FAtom n ⇒ if eqb n x then G else (FAtom n) - | FAnd F1 F2 ⇒ FAnd (subst x G F1) (subst x G F2) - | FOr F1 F2 ⇒ FOr (subst x G F1) (subst x G F2) - | FImpl F1 F2 ⇒ FImpl (subst x G F1) (subst x G F2) - | FNot F ⇒ FNot (subst x G F) - ]. - -(* ATTENZIONE - ========== - - Non modificare quanto segue. -*) -notation < "t [ \nbsp term 19 a / term 19 b \nbsp ]" non associative with precedence 19 for @{ 'substitution $b $a $t }. -notation > "t [ term 90 a / term 90 b]" non associative with precedence 19 for @{ 'substitution $b $a $t }. -interpretation "Substitution for Formula" 'substitution b a t = (subst b a t). -definition equiv ≝ λF1,F2. ∀v.[[ F1 ]]_v = [[ F2 ]]_v. -notation "hvbox(a \nbsp break mstyle color #0000ff (≡) \nbsp b)" non associative with precedence 45 for @{ 'equivF $a $b }. -notation > "a ≡ b" non associative with precedence 50 for @{ equiv $a $b }. -interpretation "equivalence for Formulas" 'equivF a b = (equiv a b). -lemma min_1_sem: ∀F,v.min 1 [[ F ]]_v = [[ F ]]_v. intros; cases (sem_bool F v); rewrite > H; reflexivity; qed. -lemma max_0_sem: ∀F,v.max [[ F ]]_v 0 = [[ F ]]_v. intros; cases (sem_bool F v); rewrite > H; reflexivity; qed. -definition IFTE := λA,B,C:Formula. FOr (FAnd A B) (FAnd (FNot A) C). - -(*DOCBEGIN - -La libreria di Matita -===================== - -Per portare a termine l'esercitazione sono necessari i seguenti lemmi: - -* lemma `decidable_eq_nat` : `∀x,y.x = y ∨ x ≠ y` -* lemma `sem_bool` : `∀F,v. [[ F ]]_v = 0 ∨ [[ F ]]_v = 1` -* lemma `not_eq_to_eqb_false` : `∀x,y.x ≠ y → eqb x y = false` -* lemma `eq_to_eqb_true` : `∀x,y.x = y → eqb x y = true` -* lemma `min_1_sem` : `∀F,v.min 1 [[ F ]]_v = [[ F ]]_v` -* lemma `max_0_sem` : `∀F,v.max [[ F ]]_v 0 = [[ F ]]_v` - -Nota su `x = y` e `eqb x y` ---------------------------- - -Se vi siete mai chiesti la differenza tra `x = y` ed `eqb x y` -quanto segue prova a chiarirla. - -Presi due numeri `x` e `y` in ℕ, dire che `x = y` significa i due numeri -sono lo stesso numero, ovvero che se `x` è il numero `3`, -anche `y` è il numero `3`. - -`eqb` è un funzione, un programma, che confronta due numeri naturali -e restituisce `true` se sono uguali, `false` se sono diversi. L'utilizzo -di tale programma è necessario per usare il costrutto (che è a sua volta -un programma) `if E then A else B`, che lancia il programma `E`, -e se il suo -risultato è `true` si comporta come `A` altrimenti come `B`. Come -ben sapete i programmi possono contenere errori. In particolare anche -`eqb` potrebbe essere sbagliato, e per esempio restituire sempre `true`. -I teoremi `eq_to_eqb_true` e -`not_eq_to_eqb_false` sono la dimostrazione che il programma `eqb` è -corretto, ovvero che che se `x = y` allora `eqb x y` restituisce `true`, -se `x ≠ y` allora `eqb x y` restituisce `false`. - -Il teorema di espansione di Shannon -=================================== - -Si definisce un connettivo logico `IFTE A B C` come - - FOr (FAnd A B) (FAnd (FNot A) C) - -Il teorema dice che data una formula `F`, e preso un atomo `x`, la seguente -formula è equivalente a `F`: - - IFTE (FAtom x) (F[FTop/x]) (F[FBot/x]) - -Ovvero, fissato un mondo `v`, sostituisco l'atomo `x` con `FBot` se tale -atomo è falso, lo sostituisco con `FTop` se è vero. - -La dimostrazione è composta da due lemmi, `shannon_false` e `shannon_true`. - -Vediamo solo la dimostrazione del primo, essendo il secondo del tutto analogo. -Il lemma asserisce quanto segue: - - ∀F,x,v. [[ FAtom x ]]_v = 0 → [[ F[FBot/x] ]]_v = [[ F ]]_v - -Una volta assunte la formula `F`, l'atomo `x`, il mondo `v` e aver -supposto che `[[ FAtom x ]]_v = 0` si procede per induzione su `F`. -I casi `FTop` e `FBot` sono banali. Nei casi `FAnd/FOr/FImpl/FNot`, -una volta assunte le sottoformule e le relative ipotesi induttive, -si conclude con una catena di uguaglianze. - -Il caso `FAtom` richiede maggiore cura. Assunto l'indice dell'atomo `n`, -occorre utilizzare il lemma `decidable_eq_nat` per ottenere l'ipotesi -aggiuntiva `n = x ∨ n ≠ x` (dove `x` è l'atomo su cui predica il teorema). -Si procede per casi sull'ipotesi appena ottenuta. -In entrambi i casi, usando i lemmi `eq_to_eqb_true` oppure `not_eq_to_eqb_false` -si ottengolo le ipotesi aggiuntive `(eqb n x = true)` oppure `(eqb n x = false)`. -Entrambi i casi si concludono con una catena di uguaglianze. - -Il teorema principale si dimostra utilizzando il lemma `sem_bool` per -ottenre l'ipotesi `[[ FAtom x ]]_v = 0 ∨ [[ FAtom x ]]_v = 1` su cui -si procede poi per casi. Entrambi i casi si concludono con -una catena di uguaglianze che utilizza i lemmi dimostrati in precedenza -e i lemmi `min_1_sem` oppure `max_0_sem`. - -DOCEND*) - -lemma shannon_false: - ∀F,x,v. [[ FAtom x ]]_v = 0 → [[ F[FBot/x] ]]_v = [[ F ]]_v. -(*BEGIN*) -assume F : Formula. -assume x : ℕ. -assume v : (ℕ → ℕ). -suppose ([[ FAtom x ]]_v = 0) (H). -we proceed by induction on F to prove ([[ F[FBot/x] ]]_v = [[ F ]]_v). -case FBot. - the thesis becomes ([[ FBot[FBot/x] ]]_v = [[ FBot ]]_v). - the thesis becomes ([[ FBot ]]_v = [[ FBot ]]_v). - done. -case FTop. - the thesis becomes ([[ FTop[FBot/x] ]]_v = [[ FTop ]]_v). - the thesis becomes ([[ FTop ]]_v = [[ FTop ]]_v). - done. -case FAtom. - assume n : ℕ. - the thesis becomes ([[ (FAtom n)[FBot/x] ]]_v = [[ FAtom n ]]_v). - the thesis becomes ([[ if eqb n x then FBot else (FAtom n) ]]_v = [[ FAtom n ]]_v). - by decidable_eq_nat we proved (n = x ∨ n ≠ x) (H1). - we proceed by cases on H1 to prove ([[ if eqb n x then FBot else (FAtom n) ]]_v = [[ FAtom n ]]_v). - case Left. - by H2, eq_to_eqb_true we proved (eqb n x = true) (H3). - conclude - ([[ if eqb n x then FBot else (FAtom n) ]]_v) - = ([[ if true then FBot else (FAtom n) ]]_v) by H3. - = ([[ FBot ]]_v). - = 0. - = ([[ FAtom x ]]_v) by H. - = ([[ FAtom n ]]_v) by H2. - done. - case Right. - by H2, not_eq_to_eqb_false we proved (eqb n x = false) (H3). - conclude - ([[ if eqb n x then FBot else (FAtom n) ]]_v) - = ([[ if false then FBot else (FAtom n) ]]_v) by H3. - = ([[ FAtom n ]]_v). - done. -case FAnd. - assume f1 : Formula. - by induction hypothesis we know ([[ f1[FBot/x] ]]_v = [[ f1 ]]_v) (H1). - assume f2 : Formula. - by induction hypothesis we know ([[ f2[FBot/x] ]]_v = [[ f2 ]]_v) (H2). - the thesis becomes ([[ (FAnd f1 f2)[FBot/x] ]]_v = [[ FAnd f1 f2 ]]_v). - conclude - ([[ (FAnd f1 f2)[FBot/x] ]]_v) - = ([[ FAnd (f1[FBot/x]) (f2[FBot/x]) ]]_v). - = (min [[ f1[FBot/x] ]]_v [[ f2[FBot/x] ]]_v). - = (min [[ f1 ]]_v [[ f2[FBot/x] ]]_v) by H1. - = (min [[ f1 ]]_v [[ f2 ]]_v) by H2. - = ([[ FAnd f1 f2 ]]_v). - done. -case FOr. - assume f1 : Formula. - by induction hypothesis we know ([[ f1[FBot/x] ]]_v = [[ f1 ]]_v) (H1). - assume f2 : Formula. - by induction hypothesis we know ([[ f2[FBot/x] ]]_v = [[ f2 ]]_v) (H2). - the thesis becomes ([[ (FOr f1 f2)[FBot/x] ]]_v = [[ FOr f1 f2 ]]_v). - conclude - ([[ (FOr f1 f2)[FBot/x] ]]_v) - = ([[ FOr (f1[FBot/x]) (f2[FBot/x]) ]]_v). - = (max [[ f1[FBot/x] ]]_v [[ f2[FBot/x] ]]_v). - = (max [[ f1 ]]_v [[ f2[FBot/x] ]]_v) by H1. - = (max [[ f1 ]]_v [[ f2 ]]_v) by H2. - = ([[ FOr f1 f2 ]]_v). - done. -case FImpl. - assume f1 : Formula. - by induction hypothesis we know ([[ f1[FBot/x] ]]_v = [[ f1 ]]_v) (H1). - assume f2 : Formula. - by induction hypothesis we know ([[ f2[FBot/x] ]]_v = [[ f2 ]]_v) (H2). - the thesis becomes ([[ (FImpl f1 f2)[FBot/x] ]]_v = [[ FImpl f1 f2 ]]_v). - conclude - ([[ (FImpl f1 f2)[FBot/x] ]]_v) - = ([[ FImpl (f1[FBot/x]) (f2[FBot/x]) ]]_v). - = (max (1 - [[ f1[FBot/x] ]]_v) [[ f2[FBot/x] ]]_v). - = (max (1 - [[ f1 ]]_v) [[ f2[FBot/x] ]]_v) by H1. - = (max (1 - [[ f1 ]]_v) [[ f2 ]]_v) by H2. - = ([[ FImpl f1 f2 ]]_v). - done. -case FNot. - assume f : Formula. - by induction hypothesis we know ([[ f[FBot/x] ]]_v = [[ f ]]_v) (H1). - the thesis becomes ([[ (FNot f)[FBot/x] ]]_v = [[ FNot f ]]_v). - conclude - ([[ (FNot f)[FBot/x] ]]_v) - = ([[ FNot (f[FBot/x]) ]]_v). - = (1 - [[ f[FBot/x] ]]_v). - = (1 - [[ f ]]_v) by H1. - = ([[ FNot f ]]_v). - done. -(*END*) -qed. - -lemma shannon_true: - ∀F,x,v. [[ FAtom x ]]_v = 1 → [[ F[FTop/x] ]]_v = [[ F ]]_v. -(*BEGIN*) -assume F : Formula. -assume x : ℕ. -assume v : (ℕ → ℕ). -suppose ([[ FAtom x ]]_v = 1) (H). -we proceed by induction on F to prove ([[ F[FTop/x] ]]_v = [[ F ]]_v). -case FBot. - the thesis becomes ([[ FBot[FTop/x] ]]_v = [[ FBot ]]_v). - the thesis becomes ([[ FBot ]]_v = [[ FBot ]]_v). - done. -case FTop. - the thesis becomes ([[ FTop[FTop/x] ]]_v = [[ FTop ]]_v). - the thesis becomes ([[ FTop ]]_v = [[ FTop ]]_v). - done. -case FAtom. - assume n : ℕ. - the thesis becomes ([[ (FAtom n)[FTop/x] ]]_v = [[ FAtom n ]]_v). - the thesis becomes ([[ if eqb n x then FTop else (FAtom n) ]]_v = [[ FAtom n ]]_v). - by decidable_eq_nat we proved (n = x ∨ n ≠ x) (H1). - we proceed by cases on H1 to prove ([[ if eqb n x then FTop else (FAtom n) ]]_v = [[ FAtom n ]]_v). - case Left. - by H2, eq_to_eqb_true we proved (eqb n x = true) (H3). - conclude - ([[ if eqb n x then FTop else (FAtom n) ]]_v) - = ([[ if true then FTop else (FAtom n) ]]_v) by H3. - = ([[ FTop ]]_v). - = 1. - = ([[ FAtom x ]]_v) by H. - = ([[ FAtom n ]]_v) by H2. - done. - case Right. - by H2, not_eq_to_eqb_false we proved (eqb n x = false) (H3). - conclude - ([[ if eqb n x then FTop else (FAtom n) ]]_v) - = ([[ if false then FTop else (FAtom n) ]]_v) by H3. - = ([[ FAtom n ]]_v). - done. -case FAnd. - assume f1 : Formula. - by induction hypothesis we know ([[ f1[FTop/x] ]]_v = [[ f1 ]]_v) (H1). - assume f2 : Formula. - by induction hypothesis we know ([[ f2[FTop/x] ]]_v = [[ f2 ]]_v) (H2). - the thesis becomes ([[ (FAnd f1 f2)[FTop/x] ]]_v = [[ FAnd f1 f2 ]]_v). - conclude - ([[ (FAnd f1 f2)[FTop/x] ]]_v) - = ([[ FAnd (f1[FTop/x]) (f2[FTop/x]) ]]_v). - = (min [[ f1[FTop/x] ]]_v [[ f2[FTop/x] ]]_v). - = (min [[ f1 ]]_v [[ f2[FTop/x] ]]_v) by H1. - = (min [[ f1 ]]_v [[ f2 ]]_v) by H2. - = ([[ FAnd f1 f2 ]]_v). - done. -case FOr. - assume f1 : Formula. - by induction hypothesis we know ([[ f1[FTop/x] ]]_v = [[ f1 ]]_v) (H1). - assume f2 : Formula. - by induction hypothesis we know ([[ f2[FTop/x] ]]_v = [[ f2 ]]_v) (H2). - the thesis becomes ([[ (FOr f1 f2)[FTop/x] ]]_v = [[ FOr f1 f2 ]]_v). - conclude - ([[ (FOr f1 f2)[FTop/x] ]]_v) - = ([[ FOr (f1[FTop/x]) (f2[FTop/x]) ]]_v). - = (max [[ f1[FTop/x] ]]_v [[ f2[FTop/x] ]]_v). - = (max [[ f1 ]]_v [[ f2[FTop/x] ]]_v) by H1. - = (max [[ f1 ]]_v [[ f2 ]]_v) by H2. - = ([[ FOr f1 f2 ]]_v). - done. -case FImpl. - assume f1 : Formula. - by induction hypothesis we know ([[ f1[FTop/x] ]]_v = [[ f1 ]]_v) (H1). - assume f2 : Formula. - by induction hypothesis we know ([[ f2[FTop/x] ]]_v = [[ f2 ]]_v) (H2). - the thesis becomes ([[ (FImpl f1 f2)[FTop/x] ]]_v = [[ FImpl f1 f2 ]]_v). - conclude - ([[ (FImpl f1 f2)[FTop/x] ]]_v) - = ([[ FImpl (f1[FTop/x]) (f2[FTop/x]) ]]_v). - = (max (1 - [[ f1[FTop/x] ]]_v) [[ f2[FTop/x] ]]_v). - = (max (1 - [[ f1 ]]_v) [[ f2[FTop/x] ]]_v) by H1. - = (max (1 - [[ f1 ]]_v) [[ f2 ]]_v) by H2. - = ([[ FImpl f1 f2 ]]_v). - done. -case FNot. - assume f : Formula. - by induction hypothesis we know ([[ f[FTop/x] ]]_v = [[ f ]]_v) (H1). - the thesis becomes ([[ (FNot f)[FTop/x] ]]_v = [[ FNot f ]]_v). - conclude - ([[ (FNot f)[FTop/x] ]]_v) - = ([[ FNot (f[FTop/x]) ]]_v). - = (1 - [[ f[FTop/x] ]]_v). - = (1 - [[ f ]]_v) by H1. - = ([[ FNot f ]]_v). - done. -(*END*) -qed. - -theorem shannon : - ∀F,x. IFTE (FAtom x) (F[FTop/x]) (F[FBot/x]) ≡ F. -(*BEGIN*) -assume F : Formula. -assume x : ℕ. -assume v : (ℕ → ℕ). -the thesis becomes ([[ IFTE (FAtom x) (F[FTop/x]) (F[FBot/x])]]_v = [[ F ]]_v). -by sem_bool we proved ([[ FAtom x]]_v = 0 ∨ [[ FAtom x]]_v = 1) (H). -we proceed by cases on H to prove ([[ IFTE (FAtom x) (F[FTop/x]) (F[FBot/x])]]_v = [[ F ]]_v). -case Left. - conclude - ([[ IFTE (FAtom x) (F[FTop/x]) (F[FBot/x])]]_v) - = ([[ FOr (FAnd (FAtom x) (F[FTop/x])) (FAnd (FNot (FAtom x)) (F[FBot/x]))]]_v). - = (max [[ (FAnd (FAtom x) (F[FTop/x])) ]]_v [[ (FAnd (FNot (FAtom x)) (F[FBot/x]))]]_v). - = (max (min [[ FAtom x ]]_v [[ F[FTop/x] ]]_v) (min (1 - [[ FAtom x ]]_v) [[ F[FBot/x] ]]_v)). - = (max (min 0 [[ F[FTop/x] ]]_v) (min (1 - 0) [[ F[FBot/x] ]]_v)) by H. - = (max 0 (min 1 [[ F[FBot/x] ]]_v)). - = (max 0 [[ F[FBot/x] ]]_v) by min_1_sem. - = ([[ F[FBot/x] ]]_v). - = ([[ F ]]_v) by H1, shannon_false. - done. -case Right. - conclude - ([[ IFTE (FAtom x) (F[FTop/x]) (F[FBot/x])]]_v) - = ([[ FOr (FAnd (FAtom x) (F[FTop/x])) (FAnd (FNot (FAtom x)) (F[FBot/x]))]]_v). - = (max [[ (FAnd (FAtom x) (F[FTop/x])) ]]_v [[ (FAnd (FNot (FAtom x)) (F[FBot/x]))]]_v). - = (max (min [[ FAtom x ]]_v [[ F[FTop/x] ]]_v) (min (1 - [[ FAtom x ]]_v) [[ F[FBot/x] ]]_v)). - = (max (min 1 [[ F[FTop/x] ]]_v) (min (1 - 1) [[ F[FBot/x] ]]_v)) by H. - = (max (min 1 [[ F[FTop/x] ]]_v) (min 0 [[ F[FBot/x] ]]_v)). - = (max [[ F[FTop/x] ]]_v (min 0 [[ F[FBot/x] ]]_v)) by min_1_sem. - = (max [[ F[FTop/x] ]]_v 0). - = ([[ F[FTop/x] ]]_v) by max_0_sem. - = ([[ F ]]_v) by H1, shannon_true. - done. -(*END*) -qed. - -(*DOCBEGIN - -Note generali -============= - -Si ricorda che: - -1. Ogni volta che nella finestra di destra compare un simbolo `∀` oppure un - simbolo `→` è opportuno usare il comando `assume` oppure `suppose` - oppure (se si è in un caso di una dimostrazione per induzione) il comando - `by induction hypothesis we know` (che vengono nuovamente spiegati in seguito). - -2. Ogni caso (o sotto caso) della dimostrazione: - - 1. Inizia con una sequenza di comandi `assume` o `suppose` oppure - `by induction hypothesis we know`. Tale sequenza di comandi può anche - essere vuota. - - 2. Continua poi con almeno un comando `the thesis becomes`. - - 3. Eventualmente seguono vari comandi `by ... we proved` per - utilizzare i teoremi già disponibili per generare nuove - ipotesi. - - 4. Eventualmente uno o più comandi `we proceed by cases on (...) to prove (...)`. - - 5. Se necessario un comando `conclude` seguito da un numero anche - molto lungo di passi `= (...) by ... .` per rendere la parte - sinistra della vostra tesi uguale alla parte destra. - - 6. Ogni caso termina con `done`. - -3. Ogni caso corrispondente a un nodo con sottoformule (FAnd/For/FNot) - avrà tante ipotesi induttive quante sono le sue sottoformule e tali - ipotesi sono necessarie per portare a termine la dimostrazione. - -I comandi da utilizzare -======================= - -* `the thesis becomes (...).` - - Afferma quale sia la tesi da dimostrare. Se ripetuto - permette di espandere le definizioni. - -* `we proceed by cases on (...) to prove (...).` - - Permette di andare per casi su una ipotesi (quando essa è della forma - `A ∨ B`). - - Esempio: `we proceed by cases on H to prove Q.` - -* `case ... .` - - Nelle dimostrazioni per casi o per induzioni si utulizza tale comando - per inizia la sotto prova relativa a un caso. Esempio: `case Fbot.` - -* `done.` - - Ogni caso di una dimostrazione deve essere terminato con il comando - `done.` - -* `assume ... : (...) .` - - Assume una formula o un numero, ad esempio `assume n : (ℕ).` assume - un numero naturale `n`. - -* `by ..., ..., ..., we proved (...) (...).` - - Permette di comporre lemmi e ipotesi per ottenere nuove ipotesi. - Ad esempio `by H, H1 we prove (F ≡ G) (H2).` ottiene una nuova ipotesi - `H2` che dice che `F ≡ G` componendo insieme `H` e `H1`. - -* `conclude (...) = (...) by ... .` - - Il comando conclude lavora SOLO sulla parte sinistra della tesi. È il comando - con cui si inizia una catena di uguaglianze. La prima formula che si - scrive deve essere esattamente uguale alla parte sinistra della conclusione - originale. Esempio `conclude ([[ FAtom x ]]_v) = ([[ FAtom n ]]_v) by H.` - Se la giustificazione non è un lemma o una ipotesi ma la semplice espansione - di una definizione, la parte `by ...` deve essere omessa. - -* `= (...) by ... .` - - Continua un comando `conclude`, lavorando sempre sulla parte sinistra della - tesi. - -DOCEND*) diff --git a/helm/software/matita/library/didactic/exercises/Makefile b/helm/software/matita/library/didactic/exercises/Makefile new file mode 100644 index 000000000..d31ab5525 --- /dev/null +++ b/helm/software/matita/library/didactic/exercises/Makefile @@ -0,0 +1,22 @@ +include ../Makefile.defs + +DIR=$(shell basename $$PWD) + +$(DIR) all: + $(BIN)matitac +$(DIR).opt opt all.opt: + $(BIN)matitac.opt +clean: + $(BIN)matitaclean +clean.opt: + $(BIN)matitaclean.opt +depend: + $(BIN)matitadep -dot && rm depends.dot +depend.opt: + $(BIN)matitadep.opt -dot && rm depends.dot +exercise-%: % + cp $< $@ + perl -ne 'undef $$/;s/\(\*BEGIN.*?END\*\)/…/msg;print' -i $@ + perl -ne 'undef $$/;s/\(\*DOCBEGIN.*?DOCEND\*\)//msg;print' -i $@ + (echo ''; awk 'BEGIN { p = 0; } /DOCEND/ { p = 0; } { if (p == 1) print $$0; } /DOCBEGIN/ { p = 1;}' < $< | markdown; echo '') > $@.html + diff --git a/helm/software/matita/library/didactic/exercises/duality.ma b/helm/software/matita/library/didactic/exercises/duality.ma new file mode 100644 index 000000000..c04859bd1 --- /dev/null +++ b/helm/software/matita/library/didactic/exercises/duality.ma @@ -0,0 +1,619 @@ +(* Esercitazione di logica 29/10/2008. + + Note per gli esercizi: + + http://www.cs.unibo.it/~tassi/exercise-duality.ma.html + +*) + +(* Esercizio 0 + =========== + + Compilare i seguenti campi: + + Nome1: ... + Cognome1: ... + Matricola1: ... + Account1: ... + + Nome2: ... + Cognome2: ... + Matricola2: ... + Account2: ... + + Prima di abbandonare la postazione: + + * salvare il file (menu `File ▹ Save as ...`) nella directory (cartella) + /public/ con nome linguaggi_Account1.ma, ad esempio Mario Rossi, il cui + account è mrossi, deve salvare il file in /public/linguaggi_mrossi.ma + + * mandatevi via email o stampate il file. Per stampare potete usare + usare l'editor gedit che offre la funzionalità di stampa +*) + +(*DOCBEGIN + +Il teorema di dualità +===================== + +Il teorema di dualizzazione dice che date due formule `F1` ed `F2`, +se le due formule sono equivalenti (`F1 ≡ F2`) allora anche le +loro dualizzate lo sono (`dualize F1 ≡ dualize F2`). + +L'ingrediente principale è la funzione di dualizzazione di una formula `F`: + + * Scambia FTop con FBot e viceversa + + * Scambia il connettivo FAnd con FOr e viceversa + + * Sostituisce il connettivo FImpl con FAnd e nega la + prima sottoformula. + + Ad esempio la formula `A → (B ∧ ⊥)` viene dualizzata in + `¬A ∧ (B ∨ ⊤)`. + +Per dimostrare il teorema di dualizzazione in modo agevole è necessario +definire altre nozioni: + +* La funzione `negate` che presa una formula `F` ne nega gli atomi. + Ad esempio la formula `(A ∨ (⊤ → B))` deve diventare `¬A ∨ (⊤ → ¬B)`. + +* La funzione `invert` permette di invertire un mondo `v`. + Ovvero, per ogni indice di atomo `i`, se `v i` restituisce + `1` allora `(invert v) i` restituisce `0` e viceversa. + +DOCEND*) + +(* ATTENZIONE + ========== + + Non modificare quanto segue +*) +include "nat/minus.ma". +definition if_then_else ≝ λT:Type.λe,t,f.match e return λ_.T with [ true ⇒ t | false ⇒ f]. +notation > "'if' term 19 e 'then' term 19 t 'else' term 90 f" non associative with precedence 19 for @{ 'if_then_else $e $t $f }. +notation < "'if' \nbsp term 19 e \nbsp 'then' \nbsp term 19 t \nbsp 'else' \nbsp term 90 f \nbsp" non associative with precedence 19 for @{ 'if_then_else $e $t $f }. +interpretation "Formula if_then_else" 'if_then_else e t f = (if_then_else _ e t f). +definition max ≝ λn,m. if eqb (n - m) 0 then m else n. +definition min ≝ λn,m. if eqb (n - m) 0 then n else m. + +(* Ripasso + ======= + + Il linguaggio delle formule, dove gli atomi sono + rapperesentati da un numero naturale +*) +inductive Formula : Type ≝ +| FBot: Formula +| FTop: Formula +| FAtom: nat → Formula +| FAnd: Formula → Formula → Formula +| FOr: Formula → Formula → Formula +| FImpl: Formula → Formula → Formula +| FNot: Formula → Formula +. + +(* Esercizio 1 + =========== + + Modificare la funzione `sem` scritta nella precedente + esercitazione in modo che valga solo 0 oppure 1 nel caso degli + atomi, anche nel caso in cui il mondo `v` restituisca un numero + maggiore di 1. + + Suggerimento: non è necessario usare il costrutto if_then_else + e tantomento il predicato di maggiore o uguale. È invece possibile + usare la funzione `min`. +*) +let rec sem (v: nat → nat) (F: Formula) on F : nat ≝ + match F with + [ FBot ⇒ 0 + | FTop ⇒ 1 + | FAtom n ⇒ (*BEGIN*)min (v n) 1(*END*) + | FAnd F1 F2 ⇒ min (sem v F1) (sem v F2) + | FOr F1 F2 ⇒ max (sem v F1) (sem v F2) + | FImpl F1 F2 ⇒ max (1 - sem v F1) (sem v F2) + | FNot F1 ⇒ 1 - (sem v F1) + ] +. + +(* ATTENZIONE + ========== + + Non modificare quanto segue. +*) +notation < "[[ \nbsp term 19 a \nbsp ]] \nbsp \sub term 90 v" non associative with precedence 90 for @{ 'semantics $v $a }. +notation > "[[ term 19 a ]] \sub term 90 v" non associative with precedence 90 for @{ 'semantics $v $a }. +notation > "[[ term 19 a ]]_ term 90 v" non associative with precedence 90 for @{ sem $v $a }. +interpretation "Semantic of Formula" 'semantics v a = (sem v a). + +definition v20 ≝ λx. + if eqb x 0 then 2 + else if eqb x 1 then 1 + else 0. + +(* Test 1 + ====== + + La semantica della formula `(A ∨ C)` nel mondo `v20` in cui + `A` vale `2` e `C` vale `0` deve valere `1`. + +*) +eval normalize on [[FOr (FAtom 0) (FAtom 2)]]_v20. + +(*DOCBEGIN + +La libreria di Matita +===================== + +Gli strumenti per la dimostrazione assistita sono corredati da +librerie di teoremi già dimostrati. Per portare a termine l'esercitazione +sono necessari i seguenti lemmi: + +* lemma `sem_le_1` : `∀F,v. [[ F ]]_v ≤ 1` +* lemma `min_1_1` : `∀x. x ≤ 1 → 1 - (1 - x) = x` +* lemma `min_bool` : `∀n. min n 1 = 0 ∨ min n 1 = 1` +* lemma `min_max` : `∀F,G,v.min (1 - [[F]]_v) (1 - [[G]]_v) = 1 - max [[F]]_v [[G]]_v` +* lemma `max_min` : `∀F,G,v.max (1 - [[F]]_v) (1 - [[G]]_v) = 1 - min [[F]]_v [[G]]_v` +* lemma `equiv_rewrite` : `∀F1,F2,F3. F1 ≡ F2 → F1 ≡ F3 → F2 ≡ F3` + +DOCEND*) + +(* ATTENZIONE + ========== + + Non modificare quanto segue. +*) +lemma sem_bool : ∀F,v. [[ F ]]_v = 0 ∨ [[ F ]]_v = 1. intros; elim F; simplify; [left;reflexivity; |right;reflexivity; |cases (v n);[left;|cases n1;right;]reflexivity; |4,5,6: cases H; cases H1; rewrite > H2; rewrite > H3; simplify; first [ left;reflexivity | right; reflexivity ]. |cases H; rewrite > H1; simplify;[right|left]reflexivity;] qed. +lemma min_bool : ∀n. min n 1 = 0 ∨ min n 1 = 1. intros; cases n; [left;reflexivity] cases n1; right; reflexivity; qed. +lemma min_max : ∀F,G,v. min (1 - [[F]]_v) (1 - [[G]]_v) = 1 - max [[F]]_v [[G]]_v. intros; cases (sem_bool F v);cases (sem_bool G v); rewrite > H; rewrite >H1; simplify; reflexivity; qed. +lemma max_min : ∀F,G,v. max (1 - [[F]]_v) (1 - [[G]]_v) = 1 - min [[F]]_v [[G]]_v. intros; cases (sem_bool F v);cases (sem_bool G v); rewrite > H; rewrite >H1; simplify; reflexivity; qed. +lemma min_1_1 : ∀x.x ≤ 1 → 1 - (1 - x) = x. intros; inversion H; intros; destruct; [reflexivity;] rewrite < (le_n_O_to_eq ? H1); reflexivity;qed. +lemma sem_le_1 : ∀F,v.[[F]]_v ≤ 1. intros; cases (sem_bool F v); rewrite > H; [apply le_O_n|apply le_n]qed. + +(* Esercizio 2 + =========== + + Definire per ricorsione strutturale la funzione `negate` + che presa una formula `F` ne nega gli atomi. + + Ad esempio la formula `(A ∨ (⊤ → B))` deve diventare + `¬A ∨ (⊤ → ¬B)`. +*) +let rec negate (F: Formula) on F : Formula ≝ + match F with + [ (*BEGIN*)FBot ⇒ FBot + | FTop ⇒ FTop + | FAtom n ⇒ FNot (FAtom n) + | FAnd F1 F2 ⇒ FAnd (negate F1) (negate F2) + | FOr F1 F2 ⇒ FOr (negate F1) (negate F2) + | FImpl F1 F2 ⇒ FImpl (negate F1) (negate F2) + | FNot F ⇒ FNot (negate F)(*END*) + ]. + +(* Test 2 + ====== + + Testare la funzione `negate`. Il risultato atteso è: + + FOr (FNot (FAtom O)) (FImpl FTop (FNot (FAtom 1))) +*) + +eval normalize on (negate (FOr (FAtom 0) (FImpl FTop (FAtom 1)))). + +(* ATTENZIONE + ========== + + Non modificare quanto segue +*) +definition equiv ≝ λF1,F2. ∀v.[[ F1 ]]_v = [[ F2 ]]_v. +notation "hvbox(a \nbsp break mstyle color #0000ff (≡) \nbsp b)" non associative with precedence 45 for @{ 'equivF $a $b }. +notation > "a ≡ b" non associative with precedence 50 for @{ equiv $a $b }. +interpretation "equivalence for Formulas" 'equivF a b = (equiv a b). +lemma equiv_rewrite : ∀F1,F2,F3. F1 ≡ F2 → F1 ≡ F3 → F2 ≡ F3. intros; intro; autobatch. qed. + +(* Esercizio 3 + =========== + + Definire per ricorsione strutturale la funzione di + dualizzazione di una formula `F`. Tale funzione: + + * Scambia FTop con FBot e viceversa + + * Scambia il connettivo FAnd con FOr e viceversa + + * Sostituisce il connettivo FImpl con FAnd e nega la + prima sottoformula. Il razionale è che `FImpl A B` + è semanticamente equivalente a `FOr (FNot A) B` il + cui duale è `FAnd (FNot A) B`. + + Ad esempio la formula `A → (B ∧ ⊥)` viene dualizzata in + `¬A ∧ (B ∨ ⊤)`. +*) +let rec dualize (F : Formula) on F : Formula ≝ + match F with + [ (*BEGIN*)FBot ⇒ FTop + | FTop ⇒ FBot + | FAtom n ⇒ FAtom n + | FAnd F1 F2 ⇒ FOr (dualize F1) (dualize F2) + | FOr F1 F2 ⇒ FAnd (dualize F1) (dualize F2) + | FImpl F1 F2 ⇒ FAnd (FNot (dualize F1)) (dualize F2) + | FNot F ⇒ FNot (dualize F)(*END*) + ]. + +(* Test 3 + ====== + + Testare la funzione `dualize`. Il risultato atteso è: + + FAnd (FNot (FAtom O)) (FOr (FAtom 1) FTop) +*) + +eval normalize on (dualize (FImpl (FAtom 0) (FAnd (FAtom 1) FBot))). + +(* Spiegazione + =========== + + La funzione `invert` permette di invertire un mondo `v`. + Ovvero, per ogni indice di atomo `i`, se `v i` restituisce + `1` allora `(invert v) i` restituisce `0` e viceversa. + +*) +definition invert ≝ + λv:ℕ → ℕ. λx. if eqb (min (v x) 1) 0 then 1 else 0. + +interpretation "Inversione del mondo" 'invert v = (invert v). + +(*DOCBEGIN + +Il linguaggio di dimostrazione di Matita +======================================== + +Per dimostrare il lemma `negate_invert` in modo agevole è necessario +utilizzare il seguente comando: + +* by H1, H2 we proved P (H) + + Il comando `by ... we proved` visto nella scorsa esercitazione + permette di utilizzare più ipotesi o lemmi alla volta + separandoli con una virgola. + +DOCEND*) + +(* Esercizio 4 + =========== + + Dimostrare il lemma `negate_invert` che asserisce che + la semantica in un mondo `v` associato alla formula + negata di `F` e uguale alla semantica associata + a `F` in un mondo invertito. +*) +lemma negate_invert: + ∀F:Formula.∀v:ℕ→ℕ.[[ negate F ]]_v=[[ F ]]_(invert v). +assume F:Formula. +assume v:(ℕ→ℕ). +we proceed by induction on F to prove ([[ negate F ]]_v=[[ F ]]_(invert v)). + case FBot. + (*BEGIN*) + the thesis becomes ([[ negate FBot ]]_v=[[ FBot ]]_(invert v)). + (*END*) + done. + case FTop. + (*BEGIN*) + the thesis becomes ([[ negate FTop ]]_v=[[ FTop ]]_(invert v)). + (*END*) + done. + case FAtom. + assume n : ℕ. + the thesis becomes ((*BEGIN*)[[ negate (FAtom n) ]]_v=[[ FAtom n ]]_(invert v)(*END*)). + the thesis becomes ((*BEGIN*)1 - (min (v n) 1)= min (invert v n) 1(*END*)). + the thesis becomes (1 - (min (v n) 1)= min (if eqb (min (v n) 1) 0 then 1 else 0) 1). + by min_bool we proved (min (v n) 1 = 0 ∨ min (v n) 1 = 1) (H1); + we proceed by cases on (H1) to prove (1 - (min (v n) 1)= min (if eqb (min (v n) 1) 0 then 1 else 0) 1). + case Left. + conclude + (1 - (min (v n) 1)) + = (1 - 0) by H. + = 1. + = (min 1 1). + = (min (if true then 1 else O) 1). + = (min (if eqb 0 0 then 1 else O) 1). + = (min (if eqb (min (v n) 1) O then 1 else O) 1) by H. + done. + case Right. + (*BEGIN*) + conclude + (1 - (min (v n) 1)) + = (1 - 1) by H. + = 0. + = (min 0 1). + = (min (if eqb 1 0 then 1 else O) 1). + = (min (if eqb (min (v n) 1) O then 1 else O) 1) by H. + (*END*) + done. + case FAnd. + assume f : Formula. + by induction hypothesis we know + ((*BEGIN*)[[ negate f ]]_v=[[ f ]]_(invert v)(*END*)) (H). + assume f1 : Formula. + by induction hypothesis we know + ((*BEGIN*)[[ negate f1 ]]_v=[[ f1 ]]_(invert v)(*END*)) (H1). + the thesis becomes + ([[ negate (FAnd f f1) ]]_v=[[ FAnd f f1 ]]_(invert v)). + the thesis becomes + (min [[ negate f ]]_v [[ negate f1]]_v = [[ FAnd f f1 ]]_(invert v)). + conclude + (min [[ negate f ]]_v [[ negate f1]]_v) + = (min [[ f ]]_(invert v) [[ negate f1]]_v) by (*BEGIN*)H(*END*). + = (min [[ f ]]_(invert v) [[ f1]]_(invert v)) by (*BEGIN*)H1(*END*). + done. + case FOr. + (*BEGIN*) + assume f : Formula. + by induction hypothesis we know + ([[ negate f ]]_v=[[ f ]]_(invert v)) (H). + assume f1 : Formula. + by induction hypothesis we know + ([[ negate f1 ]]_v=[[ f1 ]]_(invert v)) (H1). + the thesis becomes + ([[ negate (FOr f f1) ]]_v=[[ FOr f f1 ]]_(invert v)). + the thesis becomes + (max [[ negate f ]]_v [[ negate f1]]_v = [[ FOr f f1 ]]_(invert v)). + conclude + (max [[ negate f ]]_v [[ negate f1]]_v) + = (max [[ f ]]_(invert v) [[ negate f1]]_v) by H. + = (max [[ f ]]_(invert v) [[ f1]]_(invert v)) by H1. + (*END*) + done. + case FImpl. + (*BEGIN*) + assume f : Formula. + by induction hypothesis we know + ([[ negate f ]]_v=[[ f ]]_(invert v)) (H). + assume f1 : Formula. + by induction hypothesis we know + ([[ negate f1 ]]_v=[[ f1 ]]_(invert v)) (H1). + the thesis becomes + ([[ negate (FImpl f f1) ]]_v=[[ FImpl f f1 ]]_(invert v)). + the thesis becomes + (max (1 - [[ negate f ]]_v) [[ negate f1]]_v = [[ FImpl f f1 ]]_(invert v)). + conclude + (max (1 - [[ negate f ]]_v) [[ negate f1]]_v) + = (max (1 - [[ f ]]_(invert v)) [[ negate f1]]_v) by H. + = (max (1 - [[ f ]]_(invert v)) [[ f1]]_(invert v)) by H1. + (*END*) + done. + case FNot. + (*BEGIN*) + assume f : Formula. + by induction hypothesis we know + ([[ negate f ]]_v=[[ f ]]_(invert v)) (H). + the thesis becomes + ([[ negate (FNot f) ]]_v=[[ FNot f ]]_(invert v)). + the thesis becomes + (1 - [[ negate f ]]_v=[[ FNot f ]]_(invert v)). + conclude (1 - [[ negate f ]]_v) = (1 - [[f]]_(invert v)) by H. + (*END*) + done. +qed. + +(* Esercizio 5 + =========== + + Dimostrare che la funzione negate rispetta l'equivalenza. +*) +lemma negate_fun: + ∀F:Formula.∀G:Formula.F ≡ G → negate F ≡ negate G. + assume (*BEGIN*)F:Formula(*END*). + assume (*BEGIN*)G:Formula(*END*). + suppose (*BEGIN*)(F ≡ G) (H)(*END*). + the thesis becomes (*BEGIN*)(negate F ≡ negate G)(*END*). + the thesis becomes (*BEGIN*)(∀v:ℕ→ℕ.[[ negate F ]]_v=[[ negate G ]]_v)(*END*). + assume v:(ℕ→ℕ). + conclude + [[ negate F ]]_v + = [[ F ]]_(invert v) by (*BEGIN*)negate_invert(*END*). + = [[ G ]]_((*BEGIN*)invert v(*BEGIN*)) by (*BEGIN*)H(*BEGIN*). + = [[ negate G ]]_(*BEGIN*)v(*BEGIN*) by (*BEGIN*)negate_invert(*END*). + done. +qed. + +(* Esercizio 6 + =========== + + Dimostrare che per ogni formula `F`, `(negate F)` equivale a + dualizzarla e negarla. +*) +lemma not_dualize_eq_negate: + ∀F:Formula.negate F ≡ FNot (dualize F). + (*BEGIN*) + assume F:Formula. + the thesis becomes (∀v:ℕ→ℕ.[[negate F]]_v=[[FNot (dualize F)]]_v). + (*END*) + assume v:(ℕ→ℕ). + we proceed by induction on F to prove ([[negate F]]_v=[[FNot (dualize F)]]_v). + case FBot. + (*BEGIN*) + the thesis becomes ([[ negate FBot ]]_v=[[ FNot (dualize FBot) ]]_v). + (*END*) + done. + case FTop. + (*BEGIN*) + the thesis becomes ([[ negate FTop ]]_v=[[ FNot (dualize FTop) ]]_v). + (*END*) + done. + case FAtom. + (*BEGIN*) + assume n : ℕ. + the thesis becomes ([[ negate (FAtom n) ]]_v=[[ FNot (dualize (FAtom n)) ]]_v). + (*END*) + done. + case FAnd. + assume f : Formula. + by induction hypothesis we know + ([[ negate f ]]_v=[[ FNot (dualize f) ]]_v) (H). + assume f1 : Formula. + by induction hypothesis we know + ([[ negate f1 ]]_v=[[ FNot (dualize f1) ]]_v) (H1). + the thesis becomes + ([[ negate (FAnd f f1) ]]_v=[[ FNot (dualize (FAnd f f1)) ]]_v). + the thesis becomes + (min [[ negate f ]]_v [[ negate f1 ]]_v=[[ FNot (dualize (FAnd f f1)) ]]_v). + conclude + (min (*BEGIN*)[[ negate f ]]_v(*END*) (*BEGIN*)[[ negate f1 ]]_v(*END*)) + = (min (*BEGIN*)[[ FNot (dualize f) ]]_v(*END*) (*BEGIN*)[[ negate f1 ]]_v(*END*)) by H. + = (min (*BEGIN*)[[ FNot (dualize f) ]]_v(*END*) (*BEGIN*)[[ FNot (dualize f1) ]]_v(*END*)) by H1. + = (min (1 - [[ dualize f ]]_v) (1 - [[ dualize f1 ]]_v)). + = (1 - (max [[ dualize f ]]_v [[ dualize f1 ]]_v)) by min_max. + done. + case FOr. + (*BEGIN*) + assume f : Formula. + by induction hypothesis we know + ([[ negate f ]]_v=[[ FNot (dualize f) ]]_v) (H). + assume f1 : Formula. + by induction hypothesis we know + ([[ negate f1 ]]_v=[[ FNot (dualize f1) ]]_v) (H1). + the thesis becomes + ([[ negate (FOr f f1) ]]_v=[[ FNot (dualize (FOr f f1)) ]]_v). + the thesis becomes + (max [[ negate f ]]_v [[ negate f1 ]]_v=[[ FNot (dualize (FOr f f1)) ]]_v). + conclude + (max [[ negate f ]]_v [[ negate f1 ]]_v) + = (max [[ FNot (dualize f) ]]_v [[ negate f1 ]]_v) by H. + = (max [[ FNot (dualize f) ]]_v [[ FNot (dualize f1) ]]_v) by H1. + = (max (1 - [[ dualize f ]]_v) (1 - [[ dualize f1 ]]_v)). + = (1 - (min [[ dualize f ]]_v [[ dualize f1 ]]_v)) by max_min. + (*END*) + done. + case FImpl. + (*BEGIN*) + assume f : Formula. + by induction hypothesis we know + ([[ negate f ]]_v=[[ FNot (dualize f) ]]_v) (H). + assume f1 : Formula. + by induction hypothesis we know + ([[ negate f1 ]]_v=[[ FNot (dualize f1) ]]_v) (H1). + the thesis becomes + ([[ negate (FImpl f f1) ]]_v=[[ FNot (dualize (FImpl f f1)) ]]_v). + the thesis becomes + (max (1 - [[ negate f ]]_v) [[ negate f1 ]]_v=[[ FNot (dualize (FImpl f f1)) ]]_v). + conclude + (max (1-[[ negate f ]]_v) [[ negate f1 ]]_v) + = (max (1-[[ FNot (dualize f) ]]_v) [[ negate f1 ]]_v) by H. + = (max (1-[[ FNot (dualize f) ]]_v) [[ FNot (dualize f1) ]]_v) by H1. + = (max (1 - [[ FNot (dualize f) ]]_v) (1 - [[ dualize f1 ]]_v)). + = (1 - (min [[ FNot (dualize f) ]]_v [[ dualize f1 ]]_v)) by max_min. + (*END*) + done. + case FNot. + (*BEGIN*) + assume f : Formula. + by induction hypothesis we know + ([[ negate f ]]_v=[[ FNot (dualize f) ]]_v) (H). + the thesis becomes + ([[ negate (FNot f) ]]_v=[[ FNot (dualize (FNot f)) ]]_v). + the thesis becomes + (1 - [[ negate f ]]_v=[[ FNot (dualize (FNot f)) ]]_v). + conclude (1 - [[ negate f ]]_v) = (1 - [[ FNot (dualize f) ]]_v) by H. + (*END*) + done. +qed. + +(* Esercizio 7 + =========== + + Dimostrare che la negazione è iniettiva +*) +theorem not_inj: + ∀F,G:Formula.FNot F ≡ FNot G→F ≡ G. + (*BEGIN*) + assume F:Formula. + assume G:Formula. + suppose (FNot F ≡ FNot G) (H). + the thesis becomes (F ≡ G). + the thesis becomes (∀v:ℕ→ℕ.[[ F ]]_v=[[ G ]]_v). + (*END*) + assume v:(ℕ→ℕ). + by sem_le_1 we proved ([[F]]_v ≤ 1) (H1). + by (*BEGIN*)sem_le_1(*END*) we proved ([[G]]_v ≤ 1) (H2). + by min_1_1, H1 we proved (1 - (1 - [[F]]_v) = [[F]]_v) (H3). + by (*BEGIN*)min_1_1, H2(*END*) we proved ((*BEGIN*)1 - (1 - [[G]]_v)(*END*) = [[G]]_v) (H4). + conclude + ([[F]]_v) + = (1 - (1 - [[F]]_v)) by (*BEGIN*)H3(*END*). + = (1 - [[(*BEGIN*)FNot F(*END*)]]_v). + = (1 - [[ FNot G]]_v) by H. + = (1 - (*BEGIN*)(1 - [[G]]_v)(*END*)). + = [[G]]_v by (*BEGIN*)H4(*END*). + done. +qed. + +(*DOCBEGIN + +La prova del teorema di dualità +=============================== + +Il teorema di dualità accennato a lezione dice che se due formule +`F1` ed `F2` sono equivalenti, allora anche le formule duali lo sono. + + ∀F1,F2:Formula. F1 ≡ F2 → dualize F1 ≡ dualize F2. + +Per dimostrare tale teorema è bene suddividere la prova in lemmi intermedi + +1. lemma `negate_invert`, dimostrato per induzione su F, utilizzando + `min_bool` + + ∀F:Formula.∀v:ℕ→ℕ.[[ negate F ]]_v=[[ F ]]_(invert v). + +2. lemma `negate_fun`, conseguenza di `negate_invert` + + ∀F,G:Formula. F ≡ G → negate F ≡ negate G. + +2. lemma `not_dualize_eq_negate`, dimostrato per induzione su F, + utilizzando `max_min` e `min_max` + + ∀F:Formula. negate F ≡ FNot (dualize F) + +4. lemma `not_inj`, conseguenza di `sem_bool` + + ∀F,G:Formula. FNot F ≡ FNot G → F ≡ G + +Una volta dimostrati tali lemmi la prova del teorema di dualità +procede come di seguito: + +1. Assume l'ipotesi + + F1 ≡ F2 + +2. Utilizza `negate_fun` per ottenere + + negate F1 ≡ negate F2 + +3. Utilizzando due volte il lemma `not_dualize_eq_negate` e il lemma + `equiv_rewrite` ottiene + + FNot (dualize F1) ≡ FNot (dualize F2) + +4. Conclude utilizzando il lemma `not_inj` per ottenere la tesi + + dualize F1 ≡ dualize F2 + +DOCEND*) + +(* Esercizio 8 + =========== + + Dimostrare il teorema di dualità +*) +theorem duality: ∀F1,F2:Formula.F1 ≡ F2 → dualize F1 ≡ dualize F2. + assume F1:Formula. + assume F2:Formula. + suppose (F1 ≡ F2) (H). + the thesis becomes (dualize F1 ≡ dualize F2). + by (*BEGIN*)negate_fun(*END*), H we proved (negate F1 ≡ negate F2) (H1). + by (*BEGIN*)not_dualize_eq_negate(*END*), (*BEGIN*)equiv_rewrite(*END*), H1 we proved (FNot (dualize F1) ≡ negate F2) (H2). + by (*BEGIN*)not_dualize_eq_negate(*END*), (*BEGIN*)equiv_rewrite(*END*), H2 we proved (FNot (dualize F1) ≡ FNot (dualize F2)) (H3). + by (*BEGIN*)not_inj(*END*), H3 we proved (dualize F1 ≡ dualize F2) (H4). + by H4 done. +qed. diff --git a/helm/software/matita/library/didactic/exercises/shannon.ma b/helm/software/matita/library/didactic/exercises/shannon.ma new file mode 100644 index 000000000..f708c19ba --- /dev/null +++ b/helm/software/matita/library/didactic/exercises/shannon.ma @@ -0,0 +1,519 @@ +(* Esercizio -1 + ============ + + 1. Leggere ATTENTAMENTE, e magari stampare, la documentazione + reperibile all'URL seguente: + + http://mowgli.cs.unibo.it/~tassi/exercise-shannon.ma.html + + 2. Questa volta si fa sul serio: + + l'esercizio proposto è MOLTO difficile, occorre la vostra massima + concentrazione (leggi: niente cut&paste selvaggio) + +*) + + +(* Esercizio 0 + =========== + + Compilare i seguenti campi: + + Nome1: ... + Cognome1: ... + Matricola1: ... + Account1: ... + + Nome2: ... + Cognome2: ... + Matricola2: ... + Account2: ... + +*) + +(* ATTENZIONE + ========== + + Non modificare quanto segue +*) +include "nat/minus.ma". +definition if_then_else ≝ λT:Type.λe,t,f.match e return λ_.T with [ true ⇒ t | false ⇒ f]. +notation > "'if' term 19 e 'then' term 19 t 'else' term 90 f" non associative with precedence 19 for @{ 'if_then_else $e $t $f }. +notation < "'if' \nbsp term 19 e \nbsp 'then' \nbsp term 19 t \nbsp 'else' \nbsp term 90 f \nbsp" non associative with precedence 19 for @{ 'if_then_else $e $t $f }. +interpretation "Formula if_then_else" 'if_then_else e t f = (if_then_else _ e t f). +definition max ≝ λn,m. if eqb (n - m) 0 then m else n. +definition min ≝ λn,m. if eqb (n - m) 0 then n else m. + +(* Ripasso 1 + ========= + + Il linguaggio delle formule, dove gli atomi sono + rapperesentati da un numero naturale +*) +inductive Formula : Type ≝ +| FBot: Formula +| FTop: Formula +| FAtom: nat → Formula +| FAnd: Formula → Formula → Formula +| FOr: Formula → Formula → Formula +| FImpl: Formula → Formula → Formula +| FNot: Formula → Formula +. + +(* Ripasso 2 + ========= + + La semantica di una formula `F` in un mondo `v`: `[[ F ]]_v` +*) +let rec sem (v: nat → nat) (F: Formula) on F : nat ≝ + match F with + [ FBot ⇒ 0 + | FTop ⇒ 1 + | FAtom n ⇒ min (v n) 1 + | FAnd F1 F2 ⇒ min (sem v F1) (sem v F2) + | FOr F1 F2 ⇒ max (sem v F1) (sem v F2) + | FImpl F1 F2 ⇒ max (1 - sem v F1) (sem v F2) + | FNot F1 ⇒ 1 - (sem v F1) + ] +. + +(* ATTENZIONE + ========== + + Non modificare quanto segue. +*) +notation < "[[ \nbsp term 19 a \nbsp ]] \nbsp \sub term 90 v" non associative with precedence 90 for @{ 'semantics $v $a }. +notation > "[[ term 19 a ]] \sub term 90 v" non associative with precedence 90 for @{ 'semantics $v $a }. +notation > "[[ term 19 a ]]_ term 90 v" non associative with precedence 90 for @{ sem $v $a }. +interpretation "Semantic of Formula" 'semantics v a = (sem v a). +lemma sem_bool : ∀F,v. [[ F ]]_v = 0 ∨ [[ F ]]_v = 1. intros; elim F; simplify; [left;reflexivity; |right;reflexivity; |cases (v n);[left;|cases n1;right;]reflexivity; |4,5,6: cases H; cases H1; rewrite > H2; rewrite > H3; simplify; first [ left;reflexivity | right; reflexivity ]. |cases H; rewrite > H1; simplify;[right|left]reflexivity;] qed. + +(* Ripasso 3 + ========= + + L'operazione di sostituzione di una formula `G` al posto dell'atomo + `x` in una formula `F`: `F[G/x]` +*) + +let rec subst (x:nat) (G: Formula) (F: Formula) on F ≝ + match F with + [ FBot ⇒ FBot + | FTop ⇒ FTop + | FAtom n ⇒ if eqb n x then G else (FAtom n) + | FAnd F1 F2 ⇒ FAnd (subst x G F1) (subst x G F2) + | FOr F1 F2 ⇒ FOr (subst x G F1) (subst x G F2) + | FImpl F1 F2 ⇒ FImpl (subst x G F1) (subst x G F2) + | FNot F ⇒ FNot (subst x G F) + ]. + +(* ATTENZIONE + ========== + + Non modificare quanto segue. +*) +notation < "t [ \nbsp term 19 a / term 19 b \nbsp ]" non associative with precedence 19 for @{ 'substitution $b $a $t }. +notation > "t [ term 90 a / term 90 b]" non associative with precedence 19 for @{ 'substitution $b $a $t }. +interpretation "Substitution for Formula" 'substitution b a t = (subst b a t). +definition equiv ≝ λF1,F2. ∀v.[[ F1 ]]_v = [[ F2 ]]_v. +notation "hvbox(a \nbsp break mstyle color #0000ff (≡) \nbsp b)" non associative with precedence 45 for @{ 'equivF $a $b }. +notation > "a ≡ b" non associative with precedence 50 for @{ equiv $a $b }. +interpretation "equivalence for Formulas" 'equivF a b = (equiv a b). +lemma min_1_sem: ∀F,v.min 1 [[ F ]]_v = [[ F ]]_v. intros; cases (sem_bool F v); rewrite > H; reflexivity; qed. +lemma max_0_sem: ∀F,v.max [[ F ]]_v 0 = [[ F ]]_v. intros; cases (sem_bool F v); rewrite > H; reflexivity; qed. +definition IFTE := λA,B,C:Formula. FOr (FAnd A B) (FAnd (FNot A) C). + +(*DOCBEGIN + +La libreria di Matita +===================== + +Per portare a termine l'esercitazione sono necessari i seguenti lemmi: + +* lemma `decidable_eq_nat` : `∀x,y.x = y ∨ x ≠ y` +* lemma `sem_bool` : `∀F,v. [[ F ]]_v = 0 ∨ [[ F ]]_v = 1` +* lemma `not_eq_to_eqb_false` : `∀x,y.x ≠ y → eqb x y = false` +* lemma `eq_to_eqb_true` : `∀x,y.x = y → eqb x y = true` +* lemma `min_1_sem` : `∀F,v.min 1 [[ F ]]_v = [[ F ]]_v` +* lemma `max_0_sem` : `∀F,v.max [[ F ]]_v 0 = [[ F ]]_v` + +Nota su `x = y` e `eqb x y` +--------------------------- + +Se vi siete mai chiesti la differenza tra `x = y` ed `eqb x y` +quanto segue prova a chiarirla. + +Presi due numeri `x` e `y` in ℕ, dire che `x = y` significa i due numeri +sono lo stesso numero, ovvero che se `x` è il numero `3`, +anche `y` è il numero `3`. + +`eqb` è un funzione, un programma, che confronta due numeri naturali +e restituisce `true` se sono uguali, `false` se sono diversi. L'utilizzo +di tale programma è necessario per usare il costrutto (che è a sua volta +un programma) `if E then A else B`, che lancia il programma `E`, +e se il suo +risultato è `true` si comporta come `A` altrimenti come `B`. Come +ben sapete i programmi possono contenere errori. In particolare anche +`eqb` potrebbe essere sbagliato, e per esempio restituire sempre `true`. +I teoremi `eq_to_eqb_true` e +`not_eq_to_eqb_false` sono la dimostrazione che il programma `eqb` è +corretto, ovvero che che se `x = y` allora `eqb x y` restituisce `true`, +se `x ≠ y` allora `eqb x y` restituisce `false`. + +Il teorema di espansione di Shannon +=================================== + +Si definisce un connettivo logico `IFTE A B C` come + + FOr (FAnd A B) (FAnd (FNot A) C) + +Il teorema dice che data una formula `F`, e preso un atomo `x`, la seguente +formula è equivalente a `F`: + + IFTE (FAtom x) (F[FTop/x]) (F[FBot/x]) + +Ovvero, fissato un mondo `v`, sostituisco l'atomo `x` con `FBot` se tale +atomo è falso, lo sostituisco con `FTop` se è vero. + +La dimostrazione è composta da due lemmi, `shannon_false` e `shannon_true`. + +Vediamo solo la dimostrazione del primo, essendo il secondo del tutto analogo. +Il lemma asserisce quanto segue: + + ∀F,x,v. [[ FAtom x ]]_v = 0 → [[ F[FBot/x] ]]_v = [[ F ]]_v + +Una volta assunte la formula `F`, l'atomo `x`, il mondo `v` e aver +supposto che `[[ FAtom x ]]_v = 0` si procede per induzione su `F`. +I casi `FTop` e `FBot` sono banali. Nei casi `FAnd/FOr/FImpl/FNot`, +una volta assunte le sottoformule e le relative ipotesi induttive, +si conclude con una catena di uguaglianze. + +Il caso `FAtom` richiede maggiore cura. Assunto l'indice dell'atomo `n`, +occorre utilizzare il lemma `decidable_eq_nat` per ottenere l'ipotesi +aggiuntiva `n = x ∨ n ≠ x` (dove `x` è l'atomo su cui predica il teorema). +Si procede per casi sull'ipotesi appena ottenuta. +In entrambi i casi, usando i lemmi `eq_to_eqb_true` oppure `not_eq_to_eqb_false` +si ottengolo le ipotesi aggiuntive `(eqb n x = true)` oppure `(eqb n x = false)`. +Entrambi i casi si concludono con una catena di uguaglianze. + +Il teorema principale si dimostra utilizzando il lemma `sem_bool` per +ottenre l'ipotesi `[[ FAtom x ]]_v = 0 ∨ [[ FAtom x ]]_v = 1` su cui +si procede poi per casi. Entrambi i casi si concludono con +una catena di uguaglianze che utilizza i lemmi dimostrati in precedenza +e i lemmi `min_1_sem` oppure `max_0_sem`. + +DOCEND*) + +lemma shannon_false: + ∀F,x,v. [[ FAtom x ]]_v = 0 → [[ F[FBot/x] ]]_v = [[ F ]]_v. +(*BEGIN*) +assume F : Formula. +assume x : ℕ. +assume v : (ℕ → ℕ). +suppose ([[ FAtom x ]]_v = 0) (H). +we proceed by induction on F to prove ([[ F[FBot/x] ]]_v = [[ F ]]_v). +case FBot. + the thesis becomes ([[ FBot[FBot/x] ]]_v = [[ FBot ]]_v). + the thesis becomes ([[ FBot ]]_v = [[ FBot ]]_v). + done. +case FTop. + the thesis becomes ([[ FTop[FBot/x] ]]_v = [[ FTop ]]_v). + the thesis becomes ([[ FTop ]]_v = [[ FTop ]]_v). + done. +case FAtom. + assume n : ℕ. + the thesis becomes ([[ (FAtom n)[FBot/x] ]]_v = [[ FAtom n ]]_v). + the thesis becomes ([[ if eqb n x then FBot else (FAtom n) ]]_v = [[ FAtom n ]]_v). + by decidable_eq_nat we proved (n = x ∨ n ≠ x) (H1). + we proceed by cases on H1 to prove ([[ if eqb n x then FBot else (FAtom n) ]]_v = [[ FAtom n ]]_v). + case Left. + by H2, eq_to_eqb_true we proved (eqb n x = true) (H3). + conclude + ([[ if eqb n x then FBot else (FAtom n) ]]_v) + = ([[ if true then FBot else (FAtom n) ]]_v) by H3. + = ([[ FBot ]]_v). + = 0. + = ([[ FAtom x ]]_v) by H. + = ([[ FAtom n ]]_v) by H2. + done. + case Right. + by H2, not_eq_to_eqb_false we proved (eqb n x = false) (H3). + conclude + ([[ if eqb n x then FBot else (FAtom n) ]]_v) + = ([[ if false then FBot else (FAtom n) ]]_v) by H3. + = ([[ FAtom n ]]_v). + done. +case FAnd. + assume f1 : Formula. + by induction hypothesis we know ([[ f1[FBot/x] ]]_v = [[ f1 ]]_v) (H1). + assume f2 : Formula. + by induction hypothesis we know ([[ f2[FBot/x] ]]_v = [[ f2 ]]_v) (H2). + the thesis becomes ([[ (FAnd f1 f2)[FBot/x] ]]_v = [[ FAnd f1 f2 ]]_v). + conclude + ([[ (FAnd f1 f2)[FBot/x] ]]_v) + = ([[ FAnd (f1[FBot/x]) (f2[FBot/x]) ]]_v). + = (min [[ f1[FBot/x] ]]_v [[ f2[FBot/x] ]]_v). + = (min [[ f1 ]]_v [[ f2[FBot/x] ]]_v) by H1. + = (min [[ f1 ]]_v [[ f2 ]]_v) by H2. + = ([[ FAnd f1 f2 ]]_v). + done. +case FOr. + assume f1 : Formula. + by induction hypothesis we know ([[ f1[FBot/x] ]]_v = [[ f1 ]]_v) (H1). + assume f2 : Formula. + by induction hypothesis we know ([[ f2[FBot/x] ]]_v = [[ f2 ]]_v) (H2). + the thesis becomes ([[ (FOr f1 f2)[FBot/x] ]]_v = [[ FOr f1 f2 ]]_v). + conclude + ([[ (FOr f1 f2)[FBot/x] ]]_v) + = ([[ FOr (f1[FBot/x]) (f2[FBot/x]) ]]_v). + = (max [[ f1[FBot/x] ]]_v [[ f2[FBot/x] ]]_v). + = (max [[ f1 ]]_v [[ f2[FBot/x] ]]_v) by H1. + = (max [[ f1 ]]_v [[ f2 ]]_v) by H2. + = ([[ FOr f1 f2 ]]_v). + done. +case FImpl. + assume f1 : Formula. + by induction hypothesis we know ([[ f1[FBot/x] ]]_v = [[ f1 ]]_v) (H1). + assume f2 : Formula. + by induction hypothesis we know ([[ f2[FBot/x] ]]_v = [[ f2 ]]_v) (H2). + the thesis becomes ([[ (FImpl f1 f2)[FBot/x] ]]_v = [[ FImpl f1 f2 ]]_v). + conclude + ([[ (FImpl f1 f2)[FBot/x] ]]_v) + = ([[ FImpl (f1[FBot/x]) (f2[FBot/x]) ]]_v). + = (max (1 - [[ f1[FBot/x] ]]_v) [[ f2[FBot/x] ]]_v). + = (max (1 - [[ f1 ]]_v) [[ f2[FBot/x] ]]_v) by H1. + = (max (1 - [[ f1 ]]_v) [[ f2 ]]_v) by H2. + = ([[ FImpl f1 f2 ]]_v). + done. +case FNot. + assume f : Formula. + by induction hypothesis we know ([[ f[FBot/x] ]]_v = [[ f ]]_v) (H1). + the thesis becomes ([[ (FNot f)[FBot/x] ]]_v = [[ FNot f ]]_v). + conclude + ([[ (FNot f)[FBot/x] ]]_v) + = ([[ FNot (f[FBot/x]) ]]_v). + = (1 - [[ f[FBot/x] ]]_v). + = (1 - [[ f ]]_v) by H1. + = ([[ FNot f ]]_v). + done. +(*END*) +qed. + +lemma shannon_true: + ∀F,x,v. [[ FAtom x ]]_v = 1 → [[ F[FTop/x] ]]_v = [[ F ]]_v. +(*BEGIN*) +assume F : Formula. +assume x : ℕ. +assume v : (ℕ → ℕ). +suppose ([[ FAtom x ]]_v = 1) (H). +we proceed by induction on F to prove ([[ F[FTop/x] ]]_v = [[ F ]]_v). +case FBot. + the thesis becomes ([[ FBot[FTop/x] ]]_v = [[ FBot ]]_v). + the thesis becomes ([[ FBot ]]_v = [[ FBot ]]_v). + done. +case FTop. + the thesis becomes ([[ FTop[FTop/x] ]]_v = [[ FTop ]]_v). + the thesis becomes ([[ FTop ]]_v = [[ FTop ]]_v). + done. +case FAtom. + assume n : ℕ. + the thesis becomes ([[ (FAtom n)[FTop/x] ]]_v = [[ FAtom n ]]_v). + the thesis becomes ([[ if eqb n x then FTop else (FAtom n) ]]_v = [[ FAtom n ]]_v). + by decidable_eq_nat we proved (n = x ∨ n ≠ x) (H1). + we proceed by cases on H1 to prove ([[ if eqb n x then FTop else (FAtom n) ]]_v = [[ FAtom n ]]_v). + case Left. + by H2, eq_to_eqb_true we proved (eqb n x = true) (H3). + conclude + ([[ if eqb n x then FTop else (FAtom n) ]]_v) + = ([[ if true then FTop else (FAtom n) ]]_v) by H3. + = ([[ FTop ]]_v). + = 1. + = ([[ FAtom x ]]_v) by H. + = ([[ FAtom n ]]_v) by H2. + done. + case Right. + by H2, not_eq_to_eqb_false we proved (eqb n x = false) (H3). + conclude + ([[ if eqb n x then FTop else (FAtom n) ]]_v) + = ([[ if false then FTop else (FAtom n) ]]_v) by H3. + = ([[ FAtom n ]]_v). + done. +case FAnd. + assume f1 : Formula. + by induction hypothesis we know ([[ f1[FTop/x] ]]_v = [[ f1 ]]_v) (H1). + assume f2 : Formula. + by induction hypothesis we know ([[ f2[FTop/x] ]]_v = [[ f2 ]]_v) (H2). + the thesis becomes ([[ (FAnd f1 f2)[FTop/x] ]]_v = [[ FAnd f1 f2 ]]_v). + conclude + ([[ (FAnd f1 f2)[FTop/x] ]]_v) + = ([[ FAnd (f1[FTop/x]) (f2[FTop/x]) ]]_v). + = (min [[ f1[FTop/x] ]]_v [[ f2[FTop/x] ]]_v). + = (min [[ f1 ]]_v [[ f2[FTop/x] ]]_v) by H1. + = (min [[ f1 ]]_v [[ f2 ]]_v) by H2. + = ([[ FAnd f1 f2 ]]_v). + done. +case FOr. + assume f1 : Formula. + by induction hypothesis we know ([[ f1[FTop/x] ]]_v = [[ f1 ]]_v) (H1). + assume f2 : Formula. + by induction hypothesis we know ([[ f2[FTop/x] ]]_v = [[ f2 ]]_v) (H2). + the thesis becomes ([[ (FOr f1 f2)[FTop/x] ]]_v = [[ FOr f1 f2 ]]_v). + conclude + ([[ (FOr f1 f2)[FTop/x] ]]_v) + = ([[ FOr (f1[FTop/x]) (f2[FTop/x]) ]]_v). + = (max [[ f1[FTop/x] ]]_v [[ f2[FTop/x] ]]_v). + = (max [[ f1 ]]_v [[ f2[FTop/x] ]]_v) by H1. + = (max [[ f1 ]]_v [[ f2 ]]_v) by H2. + = ([[ FOr f1 f2 ]]_v). + done. +case FImpl. + assume f1 : Formula. + by induction hypothesis we know ([[ f1[FTop/x] ]]_v = [[ f1 ]]_v) (H1). + assume f2 : Formula. + by induction hypothesis we know ([[ f2[FTop/x] ]]_v = [[ f2 ]]_v) (H2). + the thesis becomes ([[ (FImpl f1 f2)[FTop/x] ]]_v = [[ FImpl f1 f2 ]]_v). + conclude + ([[ (FImpl f1 f2)[FTop/x] ]]_v) + = ([[ FImpl (f1[FTop/x]) (f2[FTop/x]) ]]_v). + = (max (1 - [[ f1[FTop/x] ]]_v) [[ f2[FTop/x] ]]_v). + = (max (1 - [[ f1 ]]_v) [[ f2[FTop/x] ]]_v) by H1. + = (max (1 - [[ f1 ]]_v) [[ f2 ]]_v) by H2. + = ([[ FImpl f1 f2 ]]_v). + done. +case FNot. + assume f : Formula. + by induction hypothesis we know ([[ f[FTop/x] ]]_v = [[ f ]]_v) (H1). + the thesis becomes ([[ (FNot f)[FTop/x] ]]_v = [[ FNot f ]]_v). + conclude + ([[ (FNot f)[FTop/x] ]]_v) + = ([[ FNot (f[FTop/x]) ]]_v). + = (1 - [[ f[FTop/x] ]]_v). + = (1 - [[ f ]]_v) by H1. + = ([[ FNot f ]]_v). + done. +(*END*) +qed. + +theorem shannon : + ∀F,x. IFTE (FAtom x) (F[FTop/x]) (F[FBot/x]) ≡ F. +(*BEGIN*) +assume F : Formula. +assume x : ℕ. +assume v : (ℕ → ℕ). +the thesis becomes ([[ IFTE (FAtom x) (F[FTop/x]) (F[FBot/x])]]_v = [[ F ]]_v). +by sem_bool we proved ([[ FAtom x]]_v = 0 ∨ [[ FAtom x]]_v = 1) (H). +we proceed by cases on H to prove ([[ IFTE (FAtom x) (F[FTop/x]) (F[FBot/x])]]_v = [[ F ]]_v). +case Left. + conclude + ([[ IFTE (FAtom x) (F[FTop/x]) (F[FBot/x])]]_v) + = ([[ FOr (FAnd (FAtom x) (F[FTop/x])) (FAnd (FNot (FAtom x)) (F[FBot/x]))]]_v). + = (max [[ (FAnd (FAtom x) (F[FTop/x])) ]]_v [[ (FAnd (FNot (FAtom x)) (F[FBot/x]))]]_v). + = (max (min [[ FAtom x ]]_v [[ F[FTop/x] ]]_v) (min (1 - [[ FAtom x ]]_v) [[ F[FBot/x] ]]_v)). + = (max (min 0 [[ F[FTop/x] ]]_v) (min (1 - 0) [[ F[FBot/x] ]]_v)) by H. + = (max 0 (min 1 [[ F[FBot/x] ]]_v)). + = (max 0 [[ F[FBot/x] ]]_v) by min_1_sem. + = ([[ F[FBot/x] ]]_v). + = ([[ F ]]_v) by H1, shannon_false. + done. +case Right. + conclude + ([[ IFTE (FAtom x) (F[FTop/x]) (F[FBot/x])]]_v) + = ([[ FOr (FAnd (FAtom x) (F[FTop/x])) (FAnd (FNot (FAtom x)) (F[FBot/x]))]]_v). + = (max [[ (FAnd (FAtom x) (F[FTop/x])) ]]_v [[ (FAnd (FNot (FAtom x)) (F[FBot/x]))]]_v). + = (max (min [[ FAtom x ]]_v [[ F[FTop/x] ]]_v) (min (1 - [[ FAtom x ]]_v) [[ F[FBot/x] ]]_v)). + = (max (min 1 [[ F[FTop/x] ]]_v) (min (1 - 1) [[ F[FBot/x] ]]_v)) by H. + = (max (min 1 [[ F[FTop/x] ]]_v) (min 0 [[ F[FBot/x] ]]_v)). + = (max [[ F[FTop/x] ]]_v (min 0 [[ F[FBot/x] ]]_v)) by min_1_sem. + = (max [[ F[FTop/x] ]]_v 0). + = ([[ F[FTop/x] ]]_v) by max_0_sem. + = ([[ F ]]_v) by H1, shannon_true. + done. +(*END*) +qed. + +(*DOCBEGIN + +Note generali +============= + +Si ricorda che: + +1. Ogni volta che nella finestra di destra compare un simbolo `∀` oppure un + simbolo `→` è opportuno usare il comando `assume` oppure `suppose` + oppure (se si è in un caso di una dimostrazione per induzione) il comando + `by induction hypothesis we know` (che vengono nuovamente spiegati in seguito). + +2. Ogni caso (o sotto caso) della dimostrazione: + + 1. Inizia con una sequenza di comandi `assume` o `suppose` oppure + `by induction hypothesis we know`. Tale sequenza di comandi può anche + essere vuota. + + 2. Continua poi con almeno un comando `the thesis becomes`. + + 3. Eventualmente seguono vari comandi `by ... we proved` per + utilizzare i teoremi già disponibili per generare nuove + ipotesi. + + 4. Eventualmente uno o più comandi `we proceed by cases on (...) to prove (...)`. + + 5. Se necessario un comando `conclude` seguito da un numero anche + molto lungo di passi `= (...) by ... .` per rendere la parte + sinistra della vostra tesi uguale alla parte destra. + + 6. Ogni caso termina con `done`. + +3. Ogni caso corrispondente a un nodo con sottoformule (FAnd/For/FNot) + avrà tante ipotesi induttive quante sono le sue sottoformule e tali + ipotesi sono necessarie per portare a termine la dimostrazione. + +I comandi da utilizzare +======================= + +* `the thesis becomes (...).` + + Afferma quale sia la tesi da dimostrare. Se ripetuto + permette di espandere le definizioni. + +* `we proceed by cases on (...) to prove (...).` + + Permette di andare per casi su una ipotesi (quando essa è della forma + `A ∨ B`). + + Esempio: `we proceed by cases on H to prove Q.` + +* `case ... .` + + Nelle dimostrazioni per casi o per induzioni si utulizza tale comando + per inizia la sotto prova relativa a un caso. Esempio: `case Fbot.` + +* `done.` + + Ogni caso di una dimostrazione deve essere terminato con il comando + `done.` + +* `assume ... : (...) .` + + Assume una formula o un numero, ad esempio `assume n : (ℕ).` assume + un numero naturale `n`. + +* `by ..., ..., ..., we proved (...) (...).` + + Permette di comporre lemmi e ipotesi per ottenere nuove ipotesi. + Ad esempio `by H, H1 we prove (F ≡ G) (H2).` ottiene una nuova ipotesi + `H2` che dice che `F ≡ G` componendo insieme `H` e `H1`. + +* `conclude (...) = (...) by ... .` + + Il comando conclude lavora SOLO sulla parte sinistra della tesi. È il comando + con cui si inizia una catena di uguaglianze. La prima formula che si + scrive deve essere esattamente uguale alla parte sinistra della conclusione + originale. Esempio `conclude ([[ FAtom x ]]_v) = ([[ FAtom n ]]_v) by H.` + Se la giustificazione non è un lemma o una ipotesi ma la semplice espansione + di una definizione, la parte `by ...` deve essere omessa. + +* `= (...) by ... .` + + Continua un comando `conclude`, lavorando sempre sulla parte sinistra della + tesi. + +DOCEND*) diff --git a/helm/software/matita/library/didactic/exercises/substitution.ma b/helm/software/matita/library/didactic/exercises/substitution.ma new file mode 100644 index 000000000..c4335ca3e --- /dev/null +++ b/helm/software/matita/library/didactic/exercises/substitution.ma @@ -0,0 +1,568 @@ +(* Esercitazione di logica 22/10/2008. *) + +(* Nota per gli studenti + ===================== + + * La lezione del pomeriggio con il Prof. Sacerdoti si terrà in aula + Pinkerle e non Cremona. + + * Un piccolo manuale sul software Matita è disponibile al seguente URL: + + http://mowgli.cs.unibo.it/~tassi/exercise-induction.ma.html + +*) + +(* Esercizio 0 + =========== + + Compilare i seguenti campi: + + Nome1: ... + Cognome1: ... + Matricola1: ... + Account1: ... + + Nome2: ... + Cognome2: ... + Matricola2: ... + Account2: ... + + Prima di abbandonare la postazione: + + * compilare il questionario in fondo al file + + * salvare il file (menu `File ▹ Save as ...`) nella directory (cartella) + /public/ con nome linguaggi_Account1.ma, ad esempio Mario Rossi, il cui + account è mrossi, deve salvare il file in /public/linguaggi_mrossi.ma + + * mandatevi via email o stampate il file. Per stampare potete usare + usare l'editor gedit che offre la funzionalità di stampa +*) + +(*DOCBEGIN + +Come scrivere i simboli +======================= + +Per inserire i simboli matematici è necessario digitare il loro nome +e poi premere ALT-L. In generale i nomi dei simboli sono della forma +`\nome`, ad esempio `\equiv`. Alcuni simboli molto frequenti hanno +dei sinonimi più comodi da digitare, per esemio `⇒` ha sia il nome +`\Rightarrow` sia `=>`. + +Segue un elenco dei simboli più comuni e i loro nomi separati da virgola, +Se sono necessari dei simboli non riportati di seguito si può visualizzare +l'intera lista dal menù a tendina `View ▹ TeX/UTF8 table`. + +* `→` : `\to`, `->` +* `⇒` : `\Rightarrow`, `=>` +* `ℕ` : `\naturals` +* `≝` : `\def`, `:=` +* `≡` : `\equiv` +* `∀` : `\forall` + +La sintassi `∀x.P` significa "per tutti gli `x` vale `P`". + +La sintassi `F → G` dove `F` e `G` sono proposizioni nel metalinguaggio +significa "`F` implica `G`". Attenzione, il simbolo `⇒` (usato a lezione) +non ha lo stesso significato in Matita. + +La sintassi `ℕ → ℕ` è il tipo delle funzioni che preso un numero naturale +restituiscono un numero naturale. + +La sintassi di Matita +===================== + +Il linguaggio di Matita si basa sul λ-calcolo CIC, la cui sintassi si +differenzia in vari aspetti da quella che solitamente viene utilizzata +per fare matematica, e ricorda quella di Scheme che state vedendo nel corso +di programmazione. + +* applicazione + + Se `f` è una funzione che si aspetta due argomenti, l'applucazione di `f` + agli argomenti `x` e `y` si scrive `(f x y)` e non `f(x,y)`. Le parentesi + possono essere omesse se il senso è chiaro dal contesto. In particolare + vengono omesse quando l'applicazione è argomento di un operatore binario. + Esempio: `f x y + f y x` si legge `(f x y) + (f y x)`. + +* minimo e massimo + + Le funzioni `min` e `max` non fanno eccezione, per calcolare il + massimo tra `x` e `y` si scrive `(max x y)` e non `max{x,y}` + +* Le funzioni definite per ricorsione strutturale utilizzano il costrutto + `let rec` (ricorsione) e il costrutto `match` (analisi per casi). + + Ad esempio la funzione count definita a lezione come + + count ⊤ ≝ 1 + count (F1 ∧ F2) ≝ 1 + count F1 + count F2 + ... + + la si esprime come + + let rec count F on F ≝ + match F with + [ ⊤ ⇒ 1 + | F1 ∧ F2 ⇒ 1 + count F1 + count F2 + ... + ]. + +* Per dare la definizione ricorsiva (di un linguaggio) si usa una sintassi + simile a BNF. Per esempio per definire + + ::= "+" | "*" | "0" | "1" + + si usa il seguente comando + + inductive A : Type ≝ + | Plus : A → A → A + | Times : A → A → A + | Zero : A + | One : A + . + +La ratio è che `Plus` prende due argomenti di tipo `A` per darmi un `A`, +mentre `Zero` non prende nessun argomento per darmi un `A`. Al posto di usare +operatori infissi `(0 + 0)` la definizione crea operatori prefissi (funzioni). +Quindi `(0+0)` si scriverà come `(Plus Zero Zero)`. + +DOCEND*) + +(* ATTENZIONE + ========== + + Non modificare le seguenti tre righe +*) +include "nat/minus.ma". +definition max : nat → nat → nat ≝ λa,b:nat.let rec max n m on n ≝ match n with [ O ⇒ b | S n ⇒ match m with [ O ⇒ a | S m ⇒ max n m]] in max a b. +definition min : nat → nat → nat ≝ λa,b:nat.let rec min n m on n ≝ match n with [ O ⇒ a | S n ⇒ match m with [ O ⇒ b | S m ⇒ min n m]] in min a b. + + +(* Esercizio 1 + =========== + + Definire il linguaggio delle formule riempiendo gli spazi +*) +inductive Formula : Type ≝ +| FBot: Formula +| FTop: (*BEGIN*)Formula(*END*) +| FAtom: nat → Formula (* usiamo i naturali al posto delle lettere *) +| FAnd: Formula → Formula → Formula +| FOr: (*BEGIN*)Formula → Formula → Formula(*END*) +| FImpl: (*BEGIN*)Formula → Formula → Formula(*END*) +| FNot: (*BEGIN*)Formula → Formula(*END*) +. + + +(* Esercizio 2 + =========== + + Data la funzione di valutazione per gli atomi `v`, definire la + funzione `sem` per una generica formula `F` che vi associa la semantica + (o denotazione) +*) +let rec sem (v: nat → nat) (F: Formula) on F ≝ + match F with + [ FBot ⇒ 0 + | FTop ⇒ (*BEGIN*)1(*END*) + (*BEGIN*) + | FAtom n ⇒ v n + (*END*) + | FAnd F1 F2 ⇒ (*BEGIN*)min (sem v F1) (sem v F2)(*END*) + (*BEGIN*) + | FOr F1 F2 ⇒ max (sem v F1) (sem v F2) + | FImpl F1 F2 ⇒ max (1 - sem v F1) (sem v F2) + (*END*) + | FNot F1 ⇒ 1 - (sem v F1) + ] +. + +(* NOTA + ==== + + I comandi che seguono definiscono la seguente notazione: + + if e then risultato1 else risultato2 + + Questa notazione permette di valutare l'espressione `e`. Se questa + è vera restituisce `risultato1`, altrimenti restituisce `risultato2`. + + Un esempio di espressione è `eqb n m`, che confronta i due numeri naturali + `n` ed `m`. + + * [[ formula ]]_v + + Questa notazione utilizza la funzione `sem` precedentemente definita, in + particolare `[[ f ]]_v` è una abbreviazione per `sem v f`. + + + ATTENZIONE + ========== + + Non modificare le linee seguenti +*) +definition if_then_else ≝ λT:Type.λe,t,f.match e return λ_.T with [ true ⇒ t | false ⇒ f]. +notation > "'if' term 19 e 'then' term 19 t 'else' term 90 f" non associative with precedence 90 for @{ 'if_then_else $e $t $f }. +notation < "'if' \nbsp term 19 e \nbsp 'then' \nbsp term 19 t \nbsp 'else' \nbsp term 90 f \nbsp" non associative with precedence 90 for @{ 'if_then_else $e $t $f }. +interpretation "Formula if_then_else" 'if_then_else e t f = (if_then_else _ e t f). +notation < "[[ \nbsp term 19 a \nbsp ]] \nbsp \sub term 90 v" non associative with precedence 90 for @{ 'semantics $v $a }. +notation > "[[ term 19 a ]] \sub term 90 v" non associative with precedence 90 for @{ 'semantics $v $a }. +notation > "[[ term 19 a ]]_ term 90 v" non associative with precedence 90 for @{ sem $v $a }. +interpretation "Semantic of Formula" 'semantics v a = (sem v a). + + +(* Test 1 + ====== + + Viene fornita una funzione di valutazione di esempio chiamata `v1101`. + Tale funzione associa agli atomi 0, 1 e 3 un valore pari a 1, + invece a 2,4,5,6... un valore pari a 0. + + Viene fornita una formula di esempio chiamata `esempio1` che rappresenta + la formula + + D => (C ∨ (B ∧ A)) + + Dove A è rappresentato con l'atomo 0, B con l'atomo 1, ... + + Tale formula è valida per la funzione di valutazione `v1101`. + + Il comando `eval normalize [[ esempio1 ]]_v1101` permette di calcolare + la funzione `sem` che avete appena definito. Tale funzione deve + computare a 1 (verrà mostrata una finestra col risultato). + Se così non fosse significa che avete commesso un errore nella + definizione di `sem` e prima di continuare è necessario che la sistemiate. +*) +definition v1101 ≝ λx. + if eqb x 0 then 1 (* FAtom 0 ↦ 1 *) + else if eqb x 1 then 1 (* FAtom 1 ↦ 1 *) + else if eqb x 2 then 0 (* FAtom 2 ↦ 0 *) + else if eqb x 3 then 1 (* FAtom 3 ↦ 1 *) + else 0. (* FAtom _ ↦ 0 *) + + +definition esempio1 ≝ + (FImpl (FNot (FAtom 3)) (FOr (FAtom 2) (FAnd (FAtom 1) (FAtom 0)))). + +eval normalize on [[ esempio1 ]]_v1101. + + +(* Esercizio 3 + =========== + + Definire la funzione di sostituzione di una formula `G` al posto + degli atomi uguali a `x` in una formula `F`. +*) +let rec subst (x:nat) (G: Formula) (F: Formula) on F ≝ + match F with + [ FBot ⇒ FBot + | FTop ⇒ (*BEGIN*)FTop(*END*) + | FAtom n ⇒ if (*BEGIN*)eqb n x(*END*) then (*BEGIN*)G(*END*) else ((*BEGIN*)FAtom n(*END*)) + (*BEGIN*) + | FAnd F1 F2 ⇒ FAnd (subst x G F1) (subst x G F2) + | FOr F1 F2 ⇒ FOr (subst x G F1) (subst x G F2) + | FImpl F1 F2 ⇒ FImpl (subst x G F1) (subst x G F2) + (*END*) + | FNot F ⇒ FNot (subst x G F) + ]. + + +(* NOTA + ==== + + I comandi che seguono definiscono la seguente notazione: + + * F [ G / x ] + + Questa notazione utilizza la funzione `subst` appena definita, in particolare + la scrittura `F [ G /x ]` è una abbreviazione per `subst x G F`. + + * F ≡ G + + Questa notazione è una abbreviazione per `∀v.[[ f ]]_v = [[ g ]]_v`. + Asserisce che for ogni funzione di valutazione `v`, la semantica di `f` + in `v` è uguale alla semantica di `g` in `v`. + + + ATTENZIONE + ========== + + Non modificare le linee seguenti +*) +notation < "t [ \nbsp term 19 a / term 19 b \nbsp ]" non associative with precedence 90 for @{ 'substitution $b $a $t }. +notation > "t [ term 90 a / term 90 b]" non associative with precedence 90 for @{ 'substitution $b $a $t }. +interpretation "Substitution for Formula" 'substitution b a t = (subst b a t). +definition equiv ≝ λF1,F2. ∀v.[[ F1 ]]_v = [[ F2 ]]_v. +notation "hvbox(a \nbsp break mstyle color #0000ff (≡) \nbsp b)" non associative with precedence 45 for @{ 'equivF $a $b }. +notation > "a ≡ b" non associative with precedence 50 for @{ equiv $a $b }. +interpretation "equivalence for Formulas" 'equivF a b = (equiv a b). + +(* Test 2 + ====== + + Viene fornita una formula di esempio `esempio2`, + e una formula `esempio3` che rimpiazzerà gli atomi + `FAtom 2` di `esempio2`. + + Il risultato atteso è la formula: + + FAnd (FImpl (FOr (FAtom O) (FAtom 1)) (FAtom 1)) + (FOr (FAtom O) (FAtom 1)) + +*) + +definition esempio2 ≝ (FAnd (FImpl (FAtom 2) (FAtom 1)) (FAtom 2)). + +definition esempio3 ≝ (FOr (FAtom 0) (FAtom 1)). + +eval normalize on (esempio2 [ esempio3 / 2]). + +(*DOCBEGIN + +Il linguaggio di dimostrazione di Matita +======================================== + +L'ultimo esercizio richiede di scrivere una dimostrazione. Tale dimostrazione +deve essere scritta utilizzando il linguaggio di dimostrazione di Matita. +Tale linguaggio è composto dai seguenti comandi: + +* `assume nome : tipo` + + Quando si deve dimostrare un tesi come `∀F : Formula.P`, il comando + `assume F : Formula` fissa una generica `Formula` `F` e la tesi + diventa `P` dove `F` è fissata. + +* `suppose P (nome)` + + Quando si deve dimostrare una tesi come `P → Q`, il comando + `suppose P (Ipotesi1)` da il nome `Ipotesi1` a `P` e cambia la tesi + `Q`, che ora può essere dimostrata facendo riferimento all'assunzione + `P` tramite il nome `Ipotesi1`. + +* `we procede by induction on F to prove Q` + + Se `F` è il nome di una (ad esempio) `Formula` precedentemente + assunta tramite il comando `assume`, inizia una prova per induzione su `F`. + +* `case name` + + Nelle prove per induzione o per casi, ogni caso deve iniziare con il + comando `case nome`, ad esempio se si procede per induzione di una + formula uno dei casi sarà quello in cui la formula è `⊥`, si deve quindi + iniziare la sotto dimostrazione per tale caso con `case ⊥`. + +* `we procede by cases on x to prove Q` + + Analogo a `we procede by induction on F to prove Q` + +* `by induction hypothesis we know P (name)` + + Nei casi non base di una prova per induzione sono disponibili delle ipotesi + induttive, quindi la tesi è della forma `P → Q`, ed è possibile + dare un nome a `P` e procedere a dimostrare `Q`. Simile a `suppose`. + +* `the thesis becomes P` + + Permette di modificare la tesi, utilizzando le definizioni (eventualmente + ricorsive) che vi compaiono. Ad esempio se la tesi fosse `min 3 5 = max 1 3` + si potrebbe usare il comando `the thesis becomes (3 = max 1 3)` in quanto + per definizione di minimo, il minimo tra `3` e `5` è `3`. + +* `by name1 we proved P (name2)` + + Permette di ottenere una nuova ipotesi `P` chiamandola `name2` utilizzando + l'ipotesi `name1`. + +* `conclude (P) = (Q) by name` + + Quando la tesi è della forma `P = Q`, si possono utilizzare delle ipotesi + della forma `A = B` riscrivendo `A` in `B` (o viceversa) in `P`. Per esempio + se la tesi fosse `sin π + 3 = 7 - 4` e si avesse una ipotesi `sin π = 0` dal + nome `H`, si potrebbe usare il comando `conclude (sin π + 3) = (0 + 3) by H` + per cambiare la conclusione in `0 + 3 = 7 - 4`. + +* `= (P) by name` + + Da utilizzare in seguito a un comando `conclude` per riscrivere con altre + ipotesi. + +* `done` + + Termina un caso della dimostrazione, è possibile utilizzarlo quando la tesi + è della forma `t = t`, ad esempio `0 = 0` oppure `v x = v x`. + +DOCEND*) + +(* Esercizio 4 + =========== + + Dimostra il teorema di sostituzione visto a lezione +*) +theorem sostituzione: ∀G1,G2,F,x. G1 ≡ G2 → F[G1/x] ≡ F[G2/x]. +assume G1 : Formula. +assume G2 : Formula. +(*BEGIN*) +assume F : Formula. +assume x : ℕ. +(*END*) +suppose (G1 ≡ G2) (H). +we proceed by induction on F to prove (F[ G1/x ] ≡ F[ G2/x ]). +case FBot. + the thesis becomes (FBot[ G1/x ] ≡ FBot[ G2/x ]). + the thesis becomes (FBot ≡ FBot[ G2/x ]). + the thesis becomes (FBot ≡ FBot). + the thesis becomes (∀v.[[FBot]]_v = [[FBot]]_v). + assume v : (ℕ → ℕ). + the thesis becomes (0 = [[FBot]]_v). + the thesis becomes (0 = 0). + done. +case FTop. + (*BEGIN*) + the thesis becomes (FTop[ G1/x ] ≡ FTop[ G2/x ]). + the thesis becomes (FTop ≡ FTop). + the thesis becomes (∀v. [[FTop]]_v = [[FTop]]_v). + assume v : (ℕ → ℕ). + the thesis becomes (1 = 1). + (*END*) + done. +case FAtom. + assume n : ℕ. + the thesis becomes ((FAtom n)[ G1/x ] ≡ (FAtom n)[ G2/x ]). + the thesis becomes + (if eqb n x then G1 else (FAtom n) ≡ (FAtom n)[ G2/x ]). + the thesis becomes + (if eqb n x then G1 else (FAtom n) ≡ + if eqb n x then G2 else (FAtom n)). + we proceed by cases on (eqb n x) to prove + (if eqb n x then G1 else (FAtom n) ≡ + if eqb n x then G2 else (FAtom n)). + case true. + the thesis becomes (G1 ≡ G2). + by H done. + case false. + (*BEGIN*) + the thesis becomes (FAtom n ≡ FAtom n). + the thesis becomes (∀v. [[FAtom n]]_v = [[FAtom n]]_v). + assume v : (ℕ → ℕ). + the thesis becomes (v n = v n). + (*END*) + done. +case FAnd. + assume F1 : Formula. + by induction hypothesis we know (F1[ G1/x ] ≡ F1[ G2/x ]) (IH1). + assume F2 : Formula. + by induction hypothesis we know (F2[ G1/x ] ≡ F2[ G2/x ]) (IH2). + the thesis becomes + (∀v.[[ (FAnd F1 F2)[ G1/x ] ]]_v = [[ (FAnd F1 F2)[ G2/x ] ]]_v). + assume v : (ℕ → ℕ). + the thesis becomes + (min ([[ F1[ G1/x ] ]]_v) ([[ F2[ G1/x ] ]]_v) = + min ([[ F1[ G2/x ] ]]_v) ([[ F2[ G2/x ] ]]_v)). + by IH1 we proved (∀v1.[[ F1[ G1/x ] ]]_v1 = [[ F1[ G2/x ] ]]_v1) (IH11). + by (*BEGIN*)IH2(*END*) we proved (∀v2.[[ F2[ G1/x ] ]]_v2 = [[ F2[ G2/x ] ]]_v2) (IH22). + by IH11 we proved ([[ F1[ G1/x ] ]]_v = [[ F1[ G2/x ] ]]_v) (IH111). + by (*BEGIN*)IH22(*END*) we proved ([[ F2[ G1/x ] ]]_v = [[ F2[ G2/x ] ]]_v) (IH222). + conclude + (min ([[ F1[ G1/x ] ]]_v) ([[ F2[ G1/x ] ]]_v)) + = (min ([[ F1[ G2/x ] ]]_v) ([[ F2[ G1/x ] ]]_v)) by IH222. + = (min ([[(F1[ G2/x ])]]_v) ([[(F2[ G2/x ])]]_v)) by (*BEGIN*)IH111(*END*). + (*END*) + done. +case FOr. + (*BEGIN*) + assume F1 : Formula. + by induction hypothesis we know (F1[ G1/x ] ≡ F1[ G2/x ]) (IH1). + assume F2 : Formula. + by induction hypothesis we know (F2[ G1/x ] ≡ F2[ G2/x ]) (IH2). + the thesis becomes + (∀v.[[ (FOr F1 F2)[ G1/x ] ]]_v = [[ (FOr F1 F2)[ G2/x ] ]]_v). + assume v : (ℕ → ℕ). + the thesis becomes + (max ([[ F1[ G1/x ] ]]_v) ([[ F2[ G1/x ] ]]_v) = + max ([[ F1[ G2/x ] ]]_v) ([[ F2[ G2/x ] ]]_v)). + by IH1 we proved (∀v1.[[ F1[ G1/x ] ]]_v1 = [[ F1[ G2/x ] ]]_v1) (IH11). + by IH2 we proved (∀v2.[[ F2[ G1/x ] ]]_v2 = [[ F2[ G2/x ] ]]_v2) (IH22). + by IH11 we proved ([[ F1[ G1/x ] ]]_v = [[ F1[ G2/x ] ]]_v) (IH111). + by IH22 we proved ([[ F2[ G1/x ] ]]_v = [[ F2[ G2/x ] ]]_v) (IH222). + conclude + (max ([[ F1[ G1/x ] ]]_v) ([[ F2[ G1/x ] ]]_v)) + = (max ([[ F1[ G2/x ] ]]_v) ([[ F2[ G1/x ] ]]_v)) by IH222. + = (max ([[(F1[ G2/x ])]]_v) ([[(F2[ G2/x ])]]_v)) by IH111. + (*END*) + done. +case FImpl. + (*BEGIN*) + assume F1 : Formula. + by induction hypothesis we know (F1[ G1/x ] ≡ F1[ G2/x ]) (IH1). + assume F2 : Formula. + by induction hypothesis we know (F2[ G1/x ] ≡ F2[ G2/x ]) (IH2). + the thesis becomes + (∀v.max (1 - [[ F1[ G1/x ] ]]_v) ([[ F2[ G1/x ] ]]_v) = + max (1 - [[ F1[ G2/x ] ]]_v) ([[ F2[ G2/x ] ]]_v)). + assume v : (ℕ → ℕ). + by IH1 we proved ([[ F1[ G1/x ] ]]_v = [[ F1[ G2/x ] ]]_v) (IH11). + by IH2 we proved ([[ F2[ G1/x ] ]]_v = [[ F2[ G2/x ] ]]_v) (IH22). + conclude + (max (1-[[ F1[ G1/x ] ]]_v) ([[ F2[ G1/x ] ]]_v)) + = (max (1-[[ F1[ G2/x ] ]]_v) ([[ F2[ G1/x ] ]]_v)) by IH11. + = (max (1-[[ F1[ G2/x ] ]]_v) ([[ F2[ G2/x ] ]]_v)) by IH22. + done. +case FNot. + (*BEGIN*) + assume F1 : Formula. + by induction hypothesis we know (F1[ G1/x ] ≡ F1[ G2/x ]) (IH). + the thesis becomes (FNot (F1[ G1/x ]) ≡ FNot (F1[ G2/x ])). + the thesis becomes (∀v.[[FNot (F1[ G1/x ])]]_v = [[FNot (F1[ G2/x ])]]_v). + assume v : (ℕ → ℕ). + the thesis becomes (1 - [[F1[ G1/x ]]]_v = [[FNot (F1[ G2/x ])]]_v). + the thesis becomes (1 - [[ F1[ G1/x ] ]]_v = 1 - [[ F1[ G2/x ] ]]_v). + by IH we proved (∀v1.[[ F1[ G1/x ] ]]_v1 = [[ F1[ G2/x ] ]]_v1) (IH1). + by IH1 we proved ([[ F1[ G1/x ] ]]_v = [[ F1[ G2/x ] ]]_v) (IH2). + conclude + (1-[[ F1[ G1/x ] ]]_v) + = (1-[[ F1[ G2/x ] ]]_v) by IH2. + (*END*) + done. +qed. + +(* Questionario + + Compilare mettendo una X nella risposta scelta. + + 1) Pensi che sia utile l'integrazione del corso con una attività di + laboratorio? + + [ ] per niente [ ] poco [ ] molto + + + 2) Pensi che gli esercizi proposti ti siano stati utili a capire meglio + quanto visto a lezione? + + [ ] per niente [ ] poco [ ] molto + + + 3) Gli esercizi erano + + [ ] troppo facili [ ] alla tua portata [ ] impossibili + + + 4) Il tempo a disposizione è stato + + [ ] poco [ ] giusto [ ] troppo + + + 5) Cose che miglioreresti nel software Matita + + ......... + + + 6) Suggerimenti sullo svolgimento delle attività in laboratorio + + ......... + + +*) + +