+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| A.Asperti, C.Sacerdoti Coen, *)
+(* ||A|| E.Tassi, S.Zacchiroli *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU Lesser General Public License Version 2.1 *)
+(* *)
+(**************************************************************************)
+
(* Esercizio 0
===========
La semantica della formula `(A ∨ C)` nel mondo `v20` in cui
`A` vale `2` e `C` vale `0` deve valere `1`.
+ Decommenta ed esegui.
*)
-eval normalize on [[FOr (FAtom 0) (FAtom 2)]]_v20.
+
+(* eval normalize on [[FOr (FAtom 0) (FAtom 2)]]_v20. *)
(*DOCBEGIN
* 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 `equiv_rewrite` : `∀F1,F2,F3. F1 ≡ F2 → F1 ≡ F3 → F2 ≡ F3`
+* lemma `equiv_sym` : `∀F1,F2. F1 ≡ F2 → F2 ≡ F1`
DOCEND*)
Testare la funzione `negate`. Il risultato atteso è:
- FOr (FNot (FAtom O)) (FImpl FTop (FNot (FAtom 1)))
+ FOr (FNot (FAtom O)) (FImpl FTop (FNot (FAtom 1)))
+
+ Decommenta ed esegui
*)
-eval normalize on (negate (FOr (FAtom 0) (FImpl FTop (FAtom 1)))).
+(* eval normalize on (negate (FOr (FAtom 0) (FImpl FTop (FAtom 1)))). *)
(* ATTENZIONE
==========
notation "hvbox(a \nbsp break mstyle color #0000ff (≡) \nbsp b)" non associative with precedence 45 for @{ 'equivF $a $b }.
notation > "a ≡ b" non associative with precedence 50 for @{ equiv $a $b }.
interpretation "equivalence for Formulas" 'equivF a b = (equiv a b).
-lemma equiv_rewrite : ∀F1,F2,F3. F1 ≡ F2 → F1 ≡ F3 → F2 ≡ F3. intros; intro; autobatch. qed.
+lemma equiv_rewrite : ∀F1,F2,F3. F1 ≡ F2 → F1 ≡ F3 → F2 ≡ F3. intros; intro; rewrite < H; rewrite < H1; reflexivity. qed.
+lemma equiv_sym : ∀a,b.a ≡ b → b ≡ a. intros 4;symmetry;apply H;qed.
(* Esercizio 3
===========
Testare la funzione `dualize`. Il risultato atteso è:
FAnd (FNot (FAtom O)) (FOr (FAtom 1) FTop)
+
+ Decommenta ed esegui.
*)
-eval normalize on (dualize (FImpl (FAtom 0) (FAnd (FAtom 1) FBot))).
+(* eval normalize on (dualize (FImpl (FAtom 0) (FAnd (FAtom 1) FBot))). *)
(* Spiegazione
===========
the thesis becomes (dualize F1 ≡ dualize F2).
by (*BEGIN*)negate_fun(*END*), H we proved (negate F1 ≡ negate F2) (H1).
by (*BEGIN*)not_dualize_eq_negate(*END*), (*BEGIN*)equiv_rewrite(*END*), H1 we proved (FNot (dualize F1) ≡ negate F2) (H2).
- by (*BEGIN*)not_dualize_eq_negate(*END*), (*BEGIN*)equiv_rewrite(*END*), H2 we proved (FNot (dualize F1) ≡ FNot (dualize F2)) (H3).
+ by (*BEGIN*)not_dualize_eq_negate(*END*), (*BEGIN*)equiv_rewrite(*END*), H2, equiv_sym we proved (FNot (dualize F1) ≡ FNot (dualize F2)) (H3).
by (*BEGIN*)not_inj(*END*), H3 we proved (dualize F1 ≡ dualize F2) (H4).
by H4 done.
qed.