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

   1 include "induction_support.ma".
   2
   3 inductive Formula : Type ≝
   4 | FBot: Formula
   5 | FTop: (*BEGIN*)Formula(*END*)
   6 | FAtom: nat → Formula
   7 | FNot: Formula → Formula
   8 | FAnd: (*BEGIN*)Formula → Formula → Formula(*END*)
   9 | FOr: (*BEGIN*)Formula → Formula → Formula(*END*)
  10 | FImpl: (*BEGIN*)Formula → Formula → Formula(*END*)
  11 .
  12
  13 let rec sem (v: nat -> nat) (F: formula) on F ≝
  14  match F with
  15   [ FBot ⇒ 0
  16   | FTop ⇒ (*BEGIN*)1(*END*)
  17   | FAtom n ⇒ v n
  18   | FNot F1 ⇒ 1 - sem v F1
  19   | FAnd F1 F2 ⇒ min (sem v F1) (sem v F2)
  20   (*BEGIN*)
  21   | FOr F1 F2 ⇒ max (sem v F1) (sem v F2)
  22   | FImpl F1 F2 ⇒ max (1 - sem v F1) (sem v F2)
  23   (*END*)
  24   ]
  25 .
  26
  27 definition if_then_else ≝
  28  λe,t,f.match e return λ_.Formula with [ true ⇒ t | false ⇒ f].
  29
  30 notation > "'if' term 19 e 'then' term 19 t 'else' term 90 f"
  31 non associative with precedence 19
  32 for @{ 'if_then_else $e $t $f }.
  33
  34 notation < "'if' \nbsp term 19 e \nbsp 'then' \nbsp term 19 t \nbsp 'else' \nbsp term 90 f \nbsp"
  35 non associative with precedence 19
  36 for @{ 'if_then_else $e $t $f }.
  37
  38 interpretation "Formula if_then_else" 'if_then_else e t f = (if_then_else e t f).
  39
  40 let rec subst (x:nat) (G: Formula) (F: formula) on F ≝
  41  match F with
  42   [ FBot ⇒ FBot
  43   | FTop ⇒ (*BEGIN*)FTop(*END*)
  44   | FAtom n ⇒ if eqb n x then G else (*BEGIN*)(FAtom n)(*END*)
  45   | FNot F ⇒ FNot (subst x G F)
  46   (*BEGIN*)
  47   | FAnd F1 F2 ⇒ FAnd (subst x G F1) (subst x G F2)
  48   | FOr F1 F2 ⇒ FOr (subst x G F1) (subst x G F2)
  49   | FImpl F1 F2 ⇒ FImpl (subst x G F1) (subst x G F2)
  50   (*END*)
  51   ].
  52
  53 definition equiv ≝ λv,F1,F2. sem v F1 = sem v F2.
  54
  55 notation "hvbox(a \nbsp break mstyle color #0000ff (≡) \sub v \nbsp b)"
  56 non associative with precedence 45
  57 for @{ 'equivF $v $a $b }.
  58
  59 notation > "a ≡_ term 90 v b" non associative with precedence 50
  60 for @{ equiv $v $a $b }.
  61
  62 interpretation "equivalence for Formulas" 'equivF v a b = (equiv v a b).
  63
  64 theorem substitution:
  65   ∀F1,F2,F,x,v. equiv v F1 F2 → equiv v (subst x F1 F) (subst x F2 F).
  66 assume F1 : Formula.
  67 assume F2 : Formula.
  68 assume F : Formula.
  69 assume x : ℕ.
  70 assume v : (ℕ → ℕ).
  71 assume H : (F1 ≡_v F2).
  72 we proceed by induction on F to prove (subst x F1 F ≡_v subst x F2 F).
  73 case Bot.
  74   the thesis becomes (FBot ≡_v (subst x F2 FBot)).
  75   the thesis becomes (FBot ≡_v FBot).
  76   the thesis becomes (sem v FBot = sem v FBot).
  77   the thesis becomes (0 = sem v FBot).
  78   the thesis becomes (0 = 0).
  79   done.
  80 case Top.
  81   (*BEGIN*)
  82   the thesis becomes (FTop ≡_v FTop).
  83   the thesis becomes (sem v FTop = sem v FTop).
  84   the thesis becomes (1 = 1).
  85   (*END*)
  86   done.
  87 case Atom.
  88   assume n : ℕ.
  89   the thesis becomes
  90     (if eqb n x then F1 else (FAtom n) ≡_v subst x F2 (FAtom n)).
  91   the thesis becomes
  92     (if eqb n x then F1 else (FAtom n) ≡_v
  93      if eqb n x then F2 else (FAtom n)).
  94   we proceed by cases on (eqb n x) to prove True. (*CSC*)
  95   case True.
  96     the thesis becomes (F1 ≡_v F2).
  97     done.
  98   case False.
  99     the thesis becomes (FAtom n ≡_v FAtom n).
 100     the thesis becomes (sem v (FAtom n) = sem v (FAtom n)).
 101     the thesis becomes (v n = v n).
 102     done.
 103 case Not.
 104   assume (*BEGIN*)f : Formula.(*END*)
 105   by induction hypothesis we know (subst x F1 f ≡_v subst x F2 f) (IH).
 106   the thesis becomes (FNot (subst x F1 f) ≡_v FNot (subst x F2 f)).
 107   the thesis becomes (sem v (FNot (subst x F1 f)) = sem v (FNot (subst x F2 f))).
 108   the thesis becomes (1 - sem v (subst x F1 f) = sem v (FNot (subst x F2 f))).
 109   the thesis becomes (1 - sem v (subst x F1 f) = 1 - sem v (subst x F2 f)).
 110   by IH we proved (sem v (subst x F1 f) = sem v (subst x F2 f)) (IH1).
 111   conclude (1-sem v (subst x F1 f)) = (1-sem v (subst x F2 f)) by IH1.
 112   done.
 113 case And.
 114   assume f : Formula.
 115   by induction hypothesis we know (subst x F1 f ≡_v subst x F2 f) (IH).
 116   assume f1 : Formula.
 117   by induction hypothesis we know (subst x F1 f1 ≡_v subst x F2 f1) (IH1).
 118   by IH we proved (sem v (subst x F1 f) = sem v (subst x F2 f)) (IH2).
 119   by IH1 we proved (sem v (subst x F1 f1) = sem v (subst x F2 f1)) (IH3).
 120   the thesis becomes
 121     (sem v (FAnd (subst x F1 f) (subst x F1 f1)) =
 122      sem v (FAnd (subst x F2 f) (subst x F2 f1))).
 123   the thesis becomes
 124     (min (sem v (subst x F1 f)) (sem v (subst x F1 f1)) =
 125      min (sem v (subst x F2 f)) (sem v (subst x F2 f1))).
 126   conclude
 127     (min (sem v (subst x F1 f)) (sem v (subst x F1 f1)))
 128     = (min (sem v (subst x F2 f)) (sem v (subst x F1 f1))) by IH2.
 129     = (*BEGIN*)(min (sem v (subst x F2 f)) (sem v (subst x F2 f1)))(*END*) by (*BEGIN*)IH3(*END*).
 130   done.
 131 (*BEGIN*)
 132 case Or.
 133   assume f : Formula.
 134   by induction hypothesis we know (subst x F1 f ≡_v subst x F2 f) (IH).
 135   assume f1 : Formula.
 136   by induction hypothesis we know (subst x F1 f1 ≡_v subst x F2 f1) (IH1).
 137   by IH we proved (sem v (subst x F1 f) = sem v (subst x F2 f)) (IH2).
 138   by IH1 we proved (sem v (subst x F1 f1) = sem v (subst x F2 f1)) (IH3).
 139   the thesis becomes
 140     (sem v (FOr (subst x F1 f) (subst x F1 f1)) =
 141      sem v (FOr (subst x F2 f) (subst x F2 f1))).
 142   the thesis becomes
 143     (max (sem v (subst x F1 f)) (sem v (subst x F1 f1)) =
 144      max (sem v (subst x F2 f)) (sem v (subst x F2 f1))).
 145   conclude
 146     (max (sem v (subst x F1 f)) (sem v (subst x F1 f1)))
 147     = (max (sem v (subst x F2 f)) (sem v (subst x F1 f1))) by IH2.
 148     = (max (sem v (subst x F2 f)) (sem v (subst x F2 f1))) by IH3.
 149   done.
 150 case Implication.
 151   assume f : Formula.
 152   by induction hypothesis we know (subst x F1 f ≡_v subst x F2 f) (IH).
 153   assume f1 : Formula.
 154   by induction hypothesis we know (subst x F1 f1 ≡_v subst x F2 f1) (IH1).
 155   the thesis becomes
 156     (max (1 - sem v (subst x F1 f)) (sem v (subst x F1 f1)) =
 157      max (1 - sem v (subst x F2 f)) (sem v (subst x F2 f1))).
 158   by IH we proved (sem v (subst x F1 f) = sem v (subst x F2 f)) (IH2).
 159   by IH1 we proved (sem v (subst x F1 f1) = sem v (subst x F2 f1)) (IH3).
 160   conclude
 161       (max (1-sem v (subst x F1 f)) (sem v (subst x F1 f1)))
 162     = (max (1-sem v (subst x F2 f)) (sem v (subst x F1 f1))) by IH2.
 163     = (max (1-sem v (subst x F2 f)) (sem v (subst x F2 f1))) by IH3.
 164   done.
 165 (*END*)
 166 qed.
 167
 168
 169