-(* 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: ...
account è mrossi deve salvare il file in /public/linguaggi_mrossi.ma
*)
-(*
+(*DOCBEGIN
+
Come scrivere i simboli
=======================
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*)
.
-(* 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
]
.
-
-(* I comandi che seguono definiscono la seguente notazione:
+(* NOTA
+ ====
+
+ I comandi che seguono definiscono la seguente notazione:
if e then risultato1 else risultato2
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 }.
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
(* AGGIUNGERE ALCUNI TEST *)
-(* I comandi che seguono definiscono la seguente notazione:
+(* NOTA
+ ====
+
+ I comandi che seguono definiscono la seguente notazione:
* F [ G / x ]
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 }.
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*)
(*END*)
done.
qed.
-
-eval normalize on
- (substitution (FAtom 1) (FAtom 1) formula1 1 (λ_.refl_eq ??) v110).
(* Questionario
projects / helm.git / commitdiff