+(* 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, cercate di capire!)
+
+*)
+
+
(* Esercizio 0
===========
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).
-(*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 `decidable_eq_nat` : `∀x,y.x = y ∨ x ≠ y`
-
-
-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.
+
let rec subst (x:nat) (G: Formula) (F: Formula) on F ≝
match F with
[ FBot ⇒ FBot
notation > "a ≡ b" non associative with precedence 50 for @{ equiv $a $b }.
interpretation "equivalence for Formulas" 'equivF a b = (equiv a b).
+(*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 `eqb_n_n` : `∀x.eqb x x = true`
+* lemma `not_eq_to_eqb_false` : `∀x,y.x ≠ y → eqb x y = false`
+
+Il teorema di espansione di Shannon
+===================================
+
+Il teorema dice che data una formula `F`, e preso un atomo `x`, la seguente
+formula ha in un mondo `v` la stessa semantica di `F`:
+
+ if eqb [[FAtom x]]_v 0 then F[FBot/x] else (F[FTop/x])
+
+Ovvero, sostituisco l'atomo `x` con `FBot` se tale atomo è falso
+nel mondo `v`, altrimenti lo sostituisco con `FTop`.
+
+DOCEND*)
+
theorem shannon :
∀F,x,v. [[ if eqb [[FAtom x]]_v 0 then F[FBot/x] else (F[FTop/x]) ]]_v = [[F]]_v.
assume F : Formula.
assume x : ℕ.
assume v : (ℕ → ℕ).
we proceed by induction on F to prove ([[ if eqb [[FAtom x]]_v 0 then F[FBot/x] else (F[FTop/x]) ]]_v = [[F]]_v).
+(*DOCBEGIN
+
+La dimostrazione
+================
+
+La dimostrazione procede per induzione sulla formula `F`. Si ricorda che:
+
+1. Ogni volta che nella finestra di destra compare un simbolo `∀` oppure un
+ simbolo `→` è opportuno usare il comando `assume` oppure `suppose` (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 combinare le
+ ipotesi tra loro o 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.
+
+DOCEND*)
case FBot.
+(*DOCBEGIN
+
+Il caso FBot
+------------
+
+La tesi è
+
+ [[ if eqb [[FAtom x]]_v 0 then FBot[FBot/x] else (FBot[FTop/x]) ]]_v = [[FBot]]_v
+
+Si procede per casi su `eqb [[FAtom x]]_v 0`. In entrambi i casi basta
+espandere piano piano le definizioni.
+
+### I comandi da utilizzare
+
+ the thesis becomes (...).
+
+ we proceed by cases on (...) to prove (...).
+
+ case ... .
+
+ done.
+
+DOCEND*)
the thesis becomes ([[ if eqb [[FAtom x]]_v 0 then FBot[FBot/x] else (FBot[FTop/x]) ]]_v = [[FBot]]_v).
we proceed by cases on (eqb [[ FAtom x ]]_v 0)
to prove ([[ if eqb [[FAtom x]]_v 0 then FBot[FBot/x] else (FBot[FTop/x]) ]]_v = [[FBot]]_v).
case false.
done.
case FTop.
+(*DOCBEGIN
+
+Il caso FTop
+------------
+
+Analogo al caso FBot
+
+DOCEND*)
we proceed by cases on (eqb [[ FAtom x ]]_v 0)
to prove ([[ if eqb [[FAtom x]]_v 0 then FTop[FBot/x] else (FTop[FTop/x]) ]]_v = [[FTop]]_v).
case true.
case false.
done.
case FAtom.
+(*DOCBEGIN
+
+Il caso (FAtom n)
+-----------------
+
+Questo è il caso più difficile di tutta la dimostrazione.
+
+La tesi è `([[ if eqb [[ FAtom x ]]_v O then (FAtom n)[ FBot/x ] else (FAtom n[ FTop/x ]) ]]_v = [[ FAtom n ]]_ v)`
+
+Per dimostrarla è necessario utilizzare il lemma `decidable_eq_nat` per
+ottenere l'ipotesi agiuntiva `n = x ∨ n ≠ x` che chiameremo `H` e il lemma
+`sem_bool` per ottenre l'ipotesi aggiuntiva `[[ FAtom x ]]_v = 0 ∨ [[ FAtom x ]]_v = 1`
+che chiameremo `H1`.
+
+Si procede poi per casi sull'ipotesi `H`, e in ogni suo sotto caso si procede
+per casi su `H1`.
+
+Nei casi in cui è presente l'ipotesi aggiuntiva `n ≠ x` è bene
+ottenre tramite il lemma `not_eq_to_eqb_false` l'ipotesi aggiuntiva
+`eqb n x = false`.
+
+Abbiamo quindi quattro casi, in tutti si procede con un comando `conclude`:
+
+1. Caso in cui `n=x` e `[[ FAtom x ]]_v = 0`.
+
+ Utilizzando l'ipotesi `[[ FAtom x ]]_v = 0` e espandendo alcune definizioni
+ si ottiene che la parte sinistra della conclusione è
+
+ ([[ if eqb n x then FBot else (FAtom n) ]]_v)
+
+ Usando l'ipotesi `n = x`, poi il lemma `eqb_n_n` e espandendo alcune
+ definizioni si ottiene `0`. Tornando ad usare le due ipotesi
+ `n=x` e `[[ FAtom x ]]_v = 0` si ottiene una formula uguale al
+ lato destro della conclusione.
+
+2. Caso in cui `n=x` e `[[ FAtom x ]]_v = 1`.
+
+ Analogo al caso precedente.
+
+3. Caso in cui `n≠x` e `[[ FAtom x ]]_v = 0`.
+
+ Si ottiene l'ipotesi aggiuntiva `eqb n x = false` usando il lemma
+ `not_eq_to_eqb_false` insieme all'ipotesi `n ≠ x`. Usando il comando
+ conlude e l'ipotesi `[[ FAtom x ]]_v = 0`, la nuova ipotesi appena
+ ottenuta e espandendo alcune definizioni si ottiene una formula
+ uguale a quella di destra.
+
+4. Caso in cui `n≠x` e `[[ FAtom x ]]_v = 1`.
+
+ Analogo al caso precedente.
+
+### I comandi da usare
+
+* `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 sini 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*)
assume n : ℕ.
the thesis becomes ([[ if eqb [[ FAtom x ]]_v O then (FAtom n)[ FBot/x ] else (FAtom n[ FTop/x ]) ]]_v = [[ FAtom n ]]_ v).
by decidable_eq_nat we proved (n = x ∨ n ≠ x) (H).
= [[ FAtom n ]]_v by H2.
done.
case Right.
+ by not_eq_to_eqb_false, H2 we proved (eqb n x = false) (H3).
we proceed by cases on H1 to prove
([[ if eqb [[ FAtom x ]]_v O then (FAtom n)[ FBot/x ] else (FAtom n[ FTop/x ]) ]]_v = [[ FAtom n ]]_ v).
case Left.
conclude
([[ if eqb [[ FAtom x ]]_v O then (FAtom n)[ FBot/x ] else (FAtom n[ FTop/x ]) ]]_v)
- = ([[ if eqb 0 O then (FAtom n)[ FBot/x ] else (FAtom n[ FTop/x ]) ]]_v) by H3.
+ = ([[ if eqb 0 O then (FAtom n)[ FBot/x ] else (FAtom n[ FTop/x ]) ]]_v) by H4.
= [[ (FAtom n)[ FBot/x ] ]]_v.
= [[ if eqb n x then FBot else (FAtom n) ]]_v.
- = [[ if false then FBot else (FAtom n) ]]_v by (not_eq_to_eqb_false ?? H2).
+ = [[ if false then FBot else (FAtom n) ]]_v by H3.
= [[ FAtom n ]]_v.
done.
case Right.
conclude
([[ if eqb [[ FAtom x ]]_v O then (FAtom n)[ FBot/x ] else (FAtom n[ FTop/x ]) ]]_v)
- = ([[ if eqb 1 O then (FAtom n)[ FBot/x ] else (FAtom n[ FTop/x ]) ]]_v) by H3.
+ = ([[ if eqb 1 O then (FAtom n)[ FBot/x ] else (FAtom n[ FTop/x ]) ]]_v) by H4.
= [[ FAtom n[ FTop/x ] ]]_v.
= [[ if eqb n x then FTop else (FAtom n) ]]_v.
- = [[ if false then FTop else (FAtom n) ]]_v by (not_eq_to_eqb_false ?? H2).
+ = [[ if false then FTop else (FAtom n) ]]_v by H3.
= [[ FAtom n ]]_v.
done.
case FAnd.
+(*DOCBEGIN
+
+Il caso FAnd
+------------
+
+Una volta assunte eventuali sottoformule e ipotesi induttive
+la tesi diventa `([[ if eqb [[ FAtom x ]]_v O then ((FAnd f f1)[ FBot/x ]) else ((FAnd f f1)[ FTop/x ]) ]]_v = [[ FAnd f f1 ]]_v)`.
+
+DOCEND*)
assume f : Formula.
by induction hypothesis we know ([[ if eqb [[ FAtom x ]]_v O then f[ FBot/x ] else (f[ FTop/x ]) ]]_v = [[ f ]]_v) (H).
assume f1 : Formula.
= ([[ FAnd f f1 ]]_v).
done.
case FOr.
+(*DOCBEGIN
+
+Il caso For
+-----------
+
+Una volta assunte eventuali sottoformule e ipotesi induttive
+la tesi diventa `([[ if eqb [[ FAtom x ]]_v O then ((FOr f f1)[ FBot/x ]) else ((FOr f f1)[ FTop/x ]) ]]_v = [[ FOr f f1 ]]_v)`.
+
+Analogo al caso FAnd.
+
+DOCEND*)
assume f : Formula.
by induction hypothesis we know ([[ if eqb [[ FAtom x ]]_v O then f[ FBot/x ] else (f[ FTop/x ]) ]]_v = [[ f ]]_v) (H).
assume f1 : Formula.
= ([[ FOr f f1 ]]_v).
done.
case FImpl.
+(*DOCBEGIN
+
+Il caso FImpl
+-------------
+
+Una volta assunte eventuali sottoformule e ipotesi induttive
+la tesi diventa `([[ if eqb [[ FAtom x ]]_v O then ((FImpl f f1)[ FBot/x ]) else ((FImpl f f1)[ FTop/x ]) ]]_v = [[ FImpl f f1 ]]_v)`.
+
+Analogo al caso FAnd.
+
+DOCEND*)
assume f : Formula.
by induction hypothesis we know ([[ if eqb [[ FAtom x ]]_v O then f[ FBot/x ] else (f[ FTop/x ]) ]]_v = [[ f ]]_v) (H).
assume f1 : Formula.
= ([[ FImpl f f1 ]]_v).
done.
case FNot.
+(*DOCBEGIN
+
+Il caso
+-----------
+
+FISSARE BUG
+
+DOCEND*)
assume f : Formula.
by induction hypothesis we know ([[ if eqb [[ FAtom x ]]_v O then f[ FBot/x ] else (f[ FTop/x ]) ]]_v = [[ f ]]_v) (H).
the thesis becomes
= ([[ if true then ((FNot f)[ FBot/x ]) else ((FNot f)[ FTop/x ]) ]]_v).
= ([[ (FNot f)[ FBot/x ] ]]_v).
= ([[ FNot (f[ FBot/x ]) ]]_v).
+ (* FIXME, ASSERT IN PARAMOD = (1 - [[ f[ FBot/x ] ]]_v). = [[ FNot f ]]_v). *)
change with (1 - [[ f[ FBot/x ] ]]_v = [[ FNot f ]]_v).
= (1 - [[ f ]]_v) by H5.
change with ([[ FNot f ]]_v = [[ FNot f ]]_v).
done.
qed.
-let rec maxatom (F : Formula) on F : ℕ ≝
- match F with
- [ FTop ⇒ 0
- | FBot ⇒ 0
- | FAtom n ⇒ n
- | FAnd F1 F2 ⇒ max (maxatom F1) (maxatom F2)
- | FOr F1 F2 ⇒ max (maxatom F1) (maxatom F2)
- | FImpl F1 F2 ⇒ max (maxatom F1) (maxatom F2)
- | FNot F1 ⇒ maxatom F1
- ]
-.
-
-let rec expandall (F : Formula) (v : ℕ → ℕ) (n : nat) on n: Formula ≝
- match n with
- [ O ⇒ F
- | S m ⇒
- if eqb [[ FAtom n ]]_v 0
- then (expandall F v m)[FBot/n]
- else ((expandall F v m)[FTop/n])
- ]
-.
-
-lemma BDD : ∀F,n,v. [[ expandall F v n ]]_v = [[ F ]]_v.
-intros; elim n; simplify; [reflexivity]
-cases (sem_bool (FAtom (S n1)) v); simplify in H1; rewrite > H1; simplify;
-[ lapply (shannon (expandall F v n1) (S n1) v);
- simplify in Hletin; rewrite > H1 in Hletin; simplify in Hletin;
- rewrite > Hletin; assumption;
-| lapply (shannon (expandall F v n1) (S n1) v);
- simplify in Hletin; rewrite > H1 in Hletin; simplify in Hletin;
- rewrite > Hletin; assumption;]
-qed.
projects / helm.git / commitdiff