From f20f1ac4aea15d81599bd2283c5440fce8d4cf6a Mon Sep 17 00:00:00 2001
From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Tue, 28 Oct 2008 22:17:11 +0000
Subject: [PATCH] done

---
 .../matita/contribs/didactic/duality.ma       | 36 ++++++++++---------
 1 file changed, 20 insertions(+), 16 deletions(-)

diff --git a/helm/software/matita/contribs/didactic/duality.ma b/helm/software/matita/contribs/didactic/duality.ma
index 62087ab4a..0138975b2 100644
--- a/helm/software/matita/contribs/didactic/duality.ma
+++ b/helm/software/matita/contribs/didactic/duality.ma
@@ -1,4 +1,10 @@
-(* 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
    ===========
@@ -144,7 +150,8 @@ 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_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`
@@ -161,6 +168,8 @@ lemma sem_bool : ∀F,v. [[ F ]]_v = 0 ∨ [[ F ]]_v = 1.  intros; elim F; simpl
 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
    ===========
@@ -516,13 +525,6 @@ qed.
    
    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*)
@@ -533,15 +535,17 @@ theorem not_inj:
  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.
 
-- 
2.39.2