(* 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
===========
* 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
+ 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
=======================
Per inserire i simboli matematici è necessario digitare il loro nome
-e poi premere CTRL-L. In generale i nomi dei simboli sono della forma
+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 `=>`.
* `≡` : `\equiv`
* `∀` : `\forall`
-La sintassi `∀v.P` significa "per tutti i `v` vale `P`".
+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)
*)
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 }.
+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 }.
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 *)
+ 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 (FAtom 3) (FOr (FAtom 2) (FAnd (FAtom 1) (FAtom 0)))).
+definition esempio1 ≝
+ (FImpl (FNot (FAtom 3)) (FOr (FAtom 2) (FAnd (FAtom 1) (FAtom 0)))).
eval normalize on [[ esempio1 ]]_v1101.
| FNot F ⇒ FNot (subst x G F)
].
-(* AGGIUNGERE ALCUNI TEST *)
-
(* NOTA
====
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
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)`
-* `by induction hypothesis we know P (name)`
-* `we procede by induction on x to prove Q`
-* `we procede by cases on x to prove Q`
+
+ 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`
-* `by name we proved P (name)`
+
+ 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*)
if eqb n x then G2 else (FAtom n)).
case true.
the thesis becomes (G1 ≡ G2).
- done.
+ by H done.
case false.
(*BEGIN*)
the thesis becomes (FAtom n ≡ FAtom n).
projects / helm.git / blobdiff