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

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