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

   1
   2 include "nat/times.ma".
   3 include "nat/compare.ma".
   4
   5 definition if_then_else ≝ λT:Type.λe,t,f.match e return λ_.T with [ true ⇒ t | false ⇒ f].
   6 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 }.
   7 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 }.
   8 interpretation "Formula if_then_else" 'if_then_else e t f = (if_then_else _ e t f).
   9
  10 inductive F : Type ≝
  11 | EZero   : F
  12 | EOne    : F
  13 | EPlus   : F → F → F
  14 | ETimes  : F → F → F
  15 | X       : ℕ → F
  16 .
  17
  18 let rec val (E : F) (v : ℕ → ℕ) on E : ℕ :=
  19   match E with
  20   [ X i ⇒ v i
  21   | EPlus e1 e2 ⇒ (val e1 v) + (val e2 v)
  22   | ETimes e1 e2 ⇒ (val e1 v) * (val e2 v)
  23   | EZero ⇒ 0
  24   | EOne ⇒ 1
  25   ]
  26   .
  27
  28 definition v201 ≝ λx.
  29        if (eqb x 0) then 2
  30   else if (eqb x 1) then 0
  31   else if (eqb x 2) then 1
  32   else                   0
  33 .
  34
  35 eval normalize on
  36   (val
  37     (EPlus (X 3)
  38            (ETimes EOne (X 2))) v201).
  39
  40 let rec subst (E : F) (G : F) (i : ℕ) on E : F :=
  41   match E with
  42   [ X j => if (eqb i j) then G else (X j)
  43   | EPlus e1 e2 => EPlus (subst e1 G i) (subst e2 G i)
  44   | ETimes e1 e2 => ETimes (subst e1 G i) (subst e2 G i)
  45   | EZero => EZero
  46   | EOne => EOne
  47   ]
  48   .
  49
  50 eval normalize on
  51  (subst
  52   (EPlus (X 0) (ETimes (X 1) (X 2)))
  53   (EOne)
  54   1)
  55   .
  56
  57 definition equiv :=
  58  λe1,e2.∀v. val e1 v = val e2 v.
  59
  60 theorem sostituzione :
  61   ∀E1,E2,G,i.
  62    equiv E1 E2 → equiv (subst G E1 i) (subst G E2 i).
  63 assume E1 : F.
  64 assume E2 : F.
  65 assume G : F.
  66 assume i : ℕ.
  67 suppose (equiv E1 E2) (H).
  68 we proceed by induction on G to prove
  69   (equiv (subst G E1 i) (subst G E2 i)).
  70 case EZero.
  71   the thesis becomes (equiv (subst EZero E1 i) (subst EZero E2 i)).
  72   the thesis becomes (equiv EZero (subst EZero E2 i)).
  73   the thesis becomes (equiv EZero EZero).
  74   the thesis becomes (∀v.val EZero v = val EZero v).
  75   assume v : (ℕ → ℕ).
  76   the thesis becomes (0 = val EZero v).
  77   the thesis becomes (0 = 0).
  78   done.
  79 case EOne.
  80   the thesis becomes (∀v.val EOne v = val EOne v).
  81   assume v : (ℕ → ℕ).
  82   the thesis becomes (1 = 1).
  83   done.
  84 case EPlus.
  85   assume e1 : F.
  86   by induction hypothesis we know (equiv (subst e1 E1 i) (subst e1 E2 i)) (H1).
  87   assume e2 : F.
  88   by induction hypothesis we know (equiv (subst e2 E1 i) (subst e2 E2 i)) (H2).
  89   by H1 we proved (∀v.val (subst e1 E1 i) v = val (subst e1 E2 i) v) (H11).
  90   by H2 we proved (∀v.val (subst e2 E1 i) v = val (subst e2 E2 i) v) (H22).
  91   the thesis becomes
  92     (∀v. val (subst e1 E1 i) v + val (subst e2 E1 i) v =
  93          val (subst e1 E2 i) v + val (subst e2 E2 i) v).
  94   assume v : (ℕ → ℕ).
  95   conclude
  96     (val (subst e1 E1 i) v + val (subst e2 E1 i) v) =
  97     (val (subst e1 E1 i) v + val (subst e2 E2 i) v) by H11.
  98   conclude
  99     (val (subst e1 E1 i) v + val (subst e2 E1 i) v) =
 100     (val (subst e1 E1 i) v + val (subst e2 E1 i) v) by H22.
 101   done.