...

diff --git a/helm/software/matita/contribs/didactic/duality.ma b/helm/software/matita/contribs/didactic/duality.ma
new file mode 100644 (file)
index 0000000..4f16daf
--- /dev/null
+++ b/helm/software/matita/contribs/didactic/duality.ma
@@ -0,0 +1,126 @@
+
+include "nat/minus.ma".
+definition max : nat → nat → nat ≝ λa,b:nat.let rec max n m on n ≝ match n with [ O ⇒ b | S n ⇒ match m with [ O ⇒ a | S m ⇒ max n m]] in max a b.
+definition min : nat → nat → nat ≝ λa,b:nat.let rec min n m on n ≝ match n with [ O ⇒ a | S n ⇒ match m with [ O ⇒ b | S m ⇒ min n m]] in min a b.
+
+
+
+inductive Formula : Type ≝
+| FBot: Formula
+| FTop: (*BEGIN*)Formula(*END*)
+| FAtom: nat → Formula (* usiamo i naturali al posto delle lettere *)
+| FAnd: Formula → Formula → Formula
+| FOr: (*BEGIN*)Formula → Formula → Formula(*END*)
+| FImpl: (*BEGIN*)Formula → Formula → Formula(*END*)
+| FNot: (*BEGIN*)Formula → Formula(*END*)
+.
+
+
+
+let rec sem (v: nat → nat) (F: Formula) on F ≝
+ match F with
+  [ FBot ⇒ 0
+  | FTop ⇒ (*BEGIN*)1(*END*)
+  (*BEGIN*)
+  | FAtom n ⇒ v n
+  (*END*)
+  | FAnd F1 F2 ⇒ (*BEGIN*)min (sem v F1) (sem v F2)(*END*)
+  (*BEGIN*)
+  | FOr F1 F2 ⇒ max (sem v F1) (sem v F2)
+  | FImpl F1 F2 ⇒ max (1 - sem v F1) (sem v F2)
+  (*END*)
+  | FNot F1 ⇒ 1 - (sem v F1)
+  ]
+.
+
+
+definition if_then_else ≝ λT:Type.λe,t,f.match e return λ_.T with [ true ⇒ t | false ⇒ f].
+notation > "'if' term 19 e 'then' term 19 t 'else' term 90 f" non associative with precedence 90 for @{ 'if_then_else $e $t $f }.
+notation < "'if' \nbsp term 19 e \nbsp 'then' \nbsp term 19 t \nbsp 'else' \nbsp term 90 f \nbsp" non associative with precedence 90 for @{ 'if_then_else $e $t $f }.
+interpretation "Formula if_then_else" 'if_then_else e t f = (if_then_else _ e t f).
+notation < "[[ \nbsp term 19 a \nbsp ]] \nbsp \sub term 90 v" non associative with precedence 90 for @{ 'semantics $v $a }.
+notation > "[[ term 19 a ]] \sub term 90 v" non associative with precedence 90 for @{ 'semantics $v $a }.
+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).
+
+
+let rec subst (F: Formula) on F ≝
+ match F with
+  [ FBot ⇒ FBot
+  | FTop ⇒ FTop
+  | FAtom n ⇒ FNot (FAtom n)
+  | FAnd F1 F2 ⇒ FAnd (subst F1) (subst F2)
+  | FOr F1 F2 ⇒ FOr (subst F1) (subst F2)
+  | FImpl F1 F2 ⇒ FImpl (subst F1) (subst F2)
+  | FNot F ⇒ FNot (subst F)
+  ].
+
+
+definition equiv ≝ λF1,F2. ∀v.[[ F1 ]]_v = [[ F2 ]]_v.
+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).
+
+let rec dualize (F : Formula) on F : Formula ≝
+  match F with
+  [ FBot ⇒ FTop
+  | FTop ⇒ FBot
+  | FAtom n ⇒ FAtom n
+  | FAnd F1 F2 ⇒ FOr (dualize F1) (dualize F2)
+  | FOr F1 F2 ⇒ FAnd (dualize F1) (dualize F2)
+  | FImpl F1 F2 ⇒ FAnd (FNot (dualize F1)) (dualize F2)
+  | FNot F ⇒ FNot (dualize F)
+  ].
+
+
+lemma : F[G/x] ≡ F
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+lemma max_n_O : ∀n. max n O = n. intros; cases n; reflexivity; qed.
+
+lemma min_n_n : ∀n. min n n = n. intros; elim n; [reflexivity] simplify;assumption;
+
+lemma min_minus_n_m : ∀n,m. min (n-m) n = n-m. intro; elim n; try reflexivity;
+cases m; [
+simplify in ⊢ (? ? (? % ?) ?);simplify; rewrite > (H n1);
+
+lemma min_one :
+  ∀x,y.1 - max x y = min (1 -x) (1-y).
+intros; apply (nat_elim2 ???? y x); intros;
+[ rewrite > max_n_O;
+whd in ⊢ (? ? ? (? ? %));
+
+
+
+
+ 
+
+axiom dualize2 : ∀F. FNot (dualize F) ≡ subst F. 
+[[ subst f ]]v = [[ f ]]_(1-v)
+f=g -> subst f = subst g
+not f = not g => f = g
+
+theorem dualize1: ∀F1,F2. F1 ≡ F2 → dualize F1 ≡  dualize F2.
+intros;
+cut (FNot F1 ≡ FNot F2);
+.
+cut (dualize (subst F1) ≡ dualize (subst F2)).
+cut (subst (subst F1) ≡ subst (subst F2)).
+
+dual f = dual (subst subst f)
+       = (dual subst) (subst f)
+       = not (subst f)
+       =  
+