X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Flibrary%2Fdidactic%2Fexercises%2Fduality.ma;fp=helm%2Fsoftware%2Fmatita%2Flibrary%2Fdidactic%2Fexercises%2Fduality.ma;h=2862883c569e293ecd8b305600b654947686d893;hb=25564c06c570e5ab9be455904c0b381842f8d4c4;hp=28e254f9477726bdcc9fc84e717b74add40d6557;hpb=91f0c0e84bfe6bf22e960d466e16f7260a2882ee;p=helm.git

diff --git a/helm/software/matita/library/didactic/exercises/duality.ma b/helm/software/matita/library/didactic/exercises/duality.ma
index 28e254f94..2862883c5 100644
--- a/helm/software/matita/library/didactic/exercises/duality.ma
+++ b/helm/software/matita/library/didactic/exercises/duality.ma
@@ -164,6 +164,7 @@ sono necessari i seguenti lemmi:
 * 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*)
 
@@ -221,6 +222,7 @@ notation "hvbox(a \nbsp break mstyle color #0000ff (≡) \nbsp b)"  non associat
 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; rewrite < H; rewrite < H1; reflexivity. qed.
+lemma equiv_sym : ∀a,b.a ≡ b → b ≡ a. intros 4;symmetry;apply H;qed.
 
 (* Esercizio 3
    ===========
@@ -625,7 +627,7 @@ theorem duality: ∀F1,F2:Formula.F1 ≡ F2 → dualize F1 ≡ dualize F2.
  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.