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 | X       : ℕ → F
  12 | EPlus   : F → F → F
  13 | ETimes  : F → F → F
  14 | EZero   : F
  15 | EOne    : 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 X.
  71   assume n : ℕ.
  72   the thesis becomes
  73     (equiv
  74       (if (eqb i n) then E1 else (X n))
  75       (subst (X n) E2 i)).
  76   the thesis becomes
  77     (equiv
  78       (if (eqb i n) then E1 else (X n))
  79       (if (eqb i n) then E2 else (X n))).
  80   we proceed by cases ...
  81
  82
  83
  84