-(* Esercitazione di logica 29/10/2008. *)
+(* Esercitazione di logica 29/10/2008.
+
+ Note per gli esercizi:
+
+ http://www.cs.unibo.it/~tassi/exercise-duality.ma.html
+
+*)
(* Esercizio 0
===========
librerie di teoremi già dimostrati. Per portare a termine l'esercitazione
sono necessari i seguenti lemmi:
-* lemma `sem_bool` : `∀F,v. [[ F ]]_v = 0 ∨ [[ F ]]_v = 1`
+* 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 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
===========
Dimostrare che la negazione è iniettiva
*)
-lemma minus_injective : ∀x.x≤1 → 1 - (1 - x) = x.
-intros; inversion H; intros; destruct; try 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; [2:apply le_n] apply le_O_n;qed.
-
theorem not_inj:
∀F,G:Formula.FNot F ≡ FNot G→F ≡ G.
(*BEGIN*)
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 (minus_injective [[F]]_v (sem_le_1 ??)).
- = (1 -
- = (1 - (1 - [[G]]_v))
-
- by H we proved ([[ FNot F ]]_v=[[ FNot G ]]_v) (H1).
- using H1 we proved (1 - [[ F ]]_v=1 - [[ G ]]_v) (H2).
- by minus_injective, sem_le_1 we proved ([[ F ]]_v=[[ G ]]_v) (H3);
+ = (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.