From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Sat, 18 Oct 2008 17:14:30 +0000 (+0000)
Subject: ...
X-Git-Tag: make_still_working~4673
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=1939d8c68af6adf4566bde37ed3c8f4972648183;p=helm.git

...
---

diff --git a/helm/software/matita/contribs/didactic/induction.ma b/helm/software/matita/contribs/didactic/induction.ma
index 2ae94646d..d8b64d7df 100644
--- a/helm/software/matita/contribs/didactic/induction.ma
+++ b/helm/software/matita/contribs/didactic/induction.ma
@@ -1,6 +1,9 @@
-(* Esercitazione di logica 22/10/2008.
+(* Esercitazione di logica 22/10/2008. *)
    
-   Esercizio 0: compilare i seguenti campi
+(* Esercizio 0 
+   ===========
+   
+   Compilare i seguenti campi:
    
    Nome1: ...
    Cognome1: ...
@@ -21,7 +24,8 @@
      account è mrossi deve salvare il file in /public/linguaggi_mrossi.ma
 *)
 
-(*  
+(*DOCBEGIN
+  
    Come scrivere i simboli
    =======================
    
@@ -108,16 +112,23 @@
    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*)
 
-(* non modificare le seguenti tre righe *)
+(* 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 l'albero di sintassi astratta delle formule *)
+(* Esercizio 1 
+   ===========
+   
+   Definire il linguaggio delle formule riempiendo gli spazi 
+*)
 inductive Formula : Type ≝
 | FBot: Formula
 | FTop: (*BEGIN*)Formula(*END*)
@@ -129,9 +140,13 @@ inductive Formula : Type ≝
 .
 
 
-(* Esercizio 2: Data la funzione di valutazione per gli atomi 'v', definire la 
+(* 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) *)
+   (o denotazione) 
+*)
 let rec sem (v: nat → nat) (F: Formula) on F ≝
  match F with
   [ FBot ⇒ 0
@@ -148,8 +163,10 @@ let rec sem (v: nat → nat) (F: Formula) on F ≝
   ]
 .
 
-
-(* I comandi che seguono definiscono la seguente notazione:
+(* NOTA
+   ====
+   
+   I comandi che seguono definiscono la seguente notazione:
 
    if e then risultato1 else risultato2
    
@@ -164,7 +181,11 @@ let rec sem (v: nat → nat) (F: Formula) on F ≝
    Questa notazione utilizza la funzione 'sem' precedentemente definita, in 
    particolare '[[ f ]]_v' è una abbreviazione per 'sem v f'.
 
-  Non modificare le linee seguenti, saltare all'esercizio 3 
+
+   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 }.
@@ -176,22 +197,47 @@ notation > "[[ term 19 a ]]_ term 90 v" non associative with precedence 90 for @
 interpretation "Semantic of Formula" 'semantics v a = (sem v a).
 
 
-(* TESTARE LA DEFINIZIONE DI SEM *)
-definition v110 ≝ λx.
+(* 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  (* Atom 0 ↦ 1 *)
  else if eqb x 1 then 1  (* Atom 1 ↦ 1 *)
  else if eqb x 2 then 0  (* Atom 2 ↦ 0 *)
+ else if eqb x 3 then 1  (* Atom 3 ↦ 1 *)
  else                 0. (* Atom _ ↦ 0 *) 
 
 
-definition formula1 ≝ (FAnd (FAtom 1) (FAtom 0)).
+definition esempio1 ≝ (FImpl (FAtom 3) (FOr (FAtom 2) (FAnd (FAtom 1) (FAtom 0)))).
 
+(* eval normalize on [[ esempio1 ]]_v1101. *)
 
-eval normalize on [[ formula1 ]]_v110.
 
-
-(* Esercizio 3: Definire la funzione di sostituzione di una formula 'G' al posto
-   degli atomi uguali a 'x' in una formula 'F'. *)
+(* 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
@@ -208,7 +254,10 @@ let rec subst (x:nat) (G: Formula) (F: Formula) on F ≝
 (* AGGIUNGERE ALCUNI TEST *)
 
 
-(* I comandi che seguono definiscono la seguente notazione:
+(* NOTA
+   ====
+   
+   I comandi che seguono definiscono la seguente notazione:
 
   * F [ G / x ]
   
@@ -221,7 +270,11 @@ let rec subst (x:nat) (G: Formula) (F: Formula) on F ≝
   Asserisce che for ogni funzione di valutazione 'v', la semantica di 'f'
   in 'v' è uguale alla semantica di 'g' in 'v'.
 
-  Non modificare le linee seguenti, saltare all'esercizio 4 
+
+  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 }.
@@ -232,9 +285,29 @@ notation > "a ≡ b" non associative with precedence 50 for @{ equiv $a $b }.
 interpretation "equivalence for Formulas" 'equivF a b = (equiv a b).
 
 
+(*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'
+   * 'suppose nome : tipo'
+   * we procede by induction on x to prove Q'
+   * the thesis becomes 
+   
+      
+DOCEND*)
 
-(* Esercizio 4: Prove the substitution theorem *)
-theorem substitution: ∀G1,G2,F,x. G1 ≡ G2 → F[G1/x] ≡ F[G2/x].
+(* 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*)
@@ -357,9 +430,6 @@ case FNot.
   (*END*)
   done.
 qed.
-
-eval normalize on 
-  (substitution (FAtom 1) (FAtom 1) formula1 1 (λ_.refl_eq ??) v110).
     
 (* Questionario