helm/software/matita/contribs/didactic/duality.ma

   1
   2 include "nat/minus.ma".
   3 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.
   4 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.
   5
   6
   7
   8 inductive Formula : Type ≝
   9 | FBot: Formula
  10 | FTop: (*BEGIN*)Formula(*END*)
  11 | FAtom: nat → Formula (* usiamo i naturali al posto delle lettere *)
  12 | FAnd: Formula → Formula → Formula
  13 | FOr: (*BEGIN*)Formula → Formula → Formula(*END*)
  14 | FImpl: (*BEGIN*)Formula → Formula → Formula(*END*)
  15 | FNot: (*BEGIN*)Formula → Formula(*END*)
  16 .
  17
  18
  19
  20 let rec sem (v: nat → nat) (F: Formula) on F ≝
  21  match F with
  22   [ FBot ⇒ 0
  23   | FTop ⇒ (*BEGIN*)1(*END*)
  24   (*BEGIN*)
  25   | FAtom n ⇒ v n
  26   (*END*)
  27   | FAnd F1 F2 ⇒ (*BEGIN*)min (sem v F1) (sem v F2)(*END*)
  28   (*BEGIN*)
  29   | FOr F1 F2 ⇒ max (sem v F1) (sem v F2)
  30   | FImpl F1 F2 ⇒ max (1 - sem v F1) (sem v F2)
  31   (*END*)
  32   | FNot F1 ⇒ 1 - (sem v F1)
  33   ]
  34 .
  35
  36
  37 definition if_then_else ≝ λT:Type.λe,t,f.match e return λ_.T with [ true ⇒ t | false ⇒ f].
  38 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 }.
  39 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 }.
  40 interpretation "Formula if_then_else" 'if_then_else e t f = (if_then_else _ e t f).
  41 notation < "[[ \nbsp term 19 a \nbsp ]] \nbsp \sub term 90 v" non associative with precedence 90 for @{ 'semantics $v $a }.
  42 notation > "[[ term 19 a ]] \sub term 90 v" non associative with precedence 90 for @{ 'semantics $v $a }.
  43 notation > "[[ term 19 a ]]_ term 90 v" non associative with precedence 90 for @{ sem $v $a }.
  44 interpretation "Semantic of Formula" 'semantics v a = (sem v a).
  45
  46
  47 let rec subst (F: Formula) on F ≝
  48  match F with
  49   [ FBot ⇒ FBot
  50   | FTop ⇒ FTop
  51   | FAtom n ⇒ FNot (FAtom n)
  52   | FAnd F1 F2 ⇒ FAnd (subst F1) (subst F2)
  53   | FOr F1 F2 ⇒ FOr (subst F1) (subst F2)
  54   | FImpl F1 F2 ⇒ FImpl (subst F1) (subst F2)
  55   | FNot F ⇒ FNot (subst F)
  56   ].
  57
  58
  59 definition equiv ≝ λF1,F2. ∀v.[[ F1 ]]_v = [[ F2 ]]_v.
  60 notation "hvbox(a \nbsp break mstyle color #0000ff (≡) \nbsp b)"  non associative with precedence 45 for @{ 'equivF $a $b }.
  61 notation > "a ≡ b" non associative with precedence 50 for @{ equiv $a $b }.
  62 interpretation "equivalence for Formulas" 'equivF a b = (equiv a b).
  63
  64 let rec dualize (F : Formula) on F : Formula ≝
  65   match F with
  66   [ FBot ⇒ FTop
  67   | FTop ⇒ FBot
  68   | FAtom n ⇒ FAtom n
  69   | FAnd F1 F2 ⇒ FOr (dualize F1) (dualize F2)
  70   | FOr F1 F2 ⇒ FAnd (dualize F1) (dualize F2)
  71   | FImpl F1 F2 ⇒ FAnd (FNot (dualize F1)) (dualize F2)
  72   | FNot F ⇒ FNot (dualize F)
  73   ].
  74
  75
  76 lemma : F[G/x] ≡ F
  77
  78
  79
  80
  81
  82
  83
  84
  85
  86
  87
  88
  89
  90
  91 lemma max_n_O : ∀n. max n O = n. intros; cases n; reflexivity; qed.
  92
  93 lemma min_n_n : ∀n. min n n = n. intros; elim n; [reflexivity] simplify;assumption;
  94
  95 lemma min_minus_n_m : ∀n,m. min (n-m) n = n-m. intro; elim n; try reflexivity;
  96 cases m; [
  97 simplify in ⊢ (? ? (? % ?) ?);simplify; rewrite > (H n1);
  98
  99 lemma min_one :
 100   ∀x,y.1 - max x y = min (1 -x) (1-y).
 101 intros; apply (nat_elim2 ???? y x); intros;
 102 [ rewrite > max_n_O;
 103 whd in ⊢ (? ? ? (? ? %));
 104
 105
 106
 107
 108
 109
 110 axiom dualize2 : ∀F. FNot (dualize F) ≡ subst F.
 111 [[ subst f ]]v = [[ f ]]_(1-v)
 112 f=g -> subst f = subst g
 113 not f = not g => f = g
 114
 115 theorem dualize1: ∀F1,F2. F1 ≡ F2 → dualize F1 ≡  dualize F2.
 116 intros;
 117 cut (FNot F1 ≡ FNot F2);
 118 .
 119 cut (dualize (subst F1) ≡ dualize (subst F2)).
 120 cut (subst (subst F1) ≡ subst (subst F2)).
 121
 122 dual f = dual (subst subst f)
 123        = (dual subst) (subst f)
 124        = not (subst f)
 125        =
 126