2 include "nat/times.ma".
3 include "nat/compare.ma".
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).
18 let rec val (E : F) (v : ℕ → ℕ) on E : ℕ :=
21 | EPlus e1 e2 ⇒ (val e1 v) + (val e2 v)
22 | ETimes e1 e2 ⇒ (val e1 v) * (val e2 v)
30 else if (eqb x 1) then 0
31 else if (eqb x 2) then 1
38 (ETimes EOne (X 2))) v201).
40 let rec subst (E : F) (G : F) (i : ℕ) on E : F :=
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)
52 (EPlus (X 0) (ETimes (X 1) (X 2)))
58 λe1,e2.∀v. val e1 v = val e2 v.
60 theorem sostituzione :
62 equiv E1 E2 → equiv (subst G E1 i) (subst G E2 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)).
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).
76 the thesis becomes (0 = val EZero v).
77 the thesis becomes (0 = 0).
80 the thesis becomes (∀v.val EOne v = val EOne v).
82 the thesis becomes (1 = 1).
86 by induction hypothesis we know (equiv (subst e1 E1 i) (subst e1 E2 i)) (H1).
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).
92 (∀v. val (EPlus (subst e1 E1 i) (subst e2 E1 i)) v =
93 val (EPlus (subst e1 E2 i) (subst e2 E2 i)) v).
95 conclude (val (EPlus (subst e1 E1 i) (subst e2 E1 i)) v)
96 = (val (EPlus (subst e1 E1 i) (subst e2 E2 i)) v).
97 = (val (EPlus (subst e1 E2 i) (subst e2 E2 i)) v) by H22.
101 (if (eqb i n) then E1 else (X n))
105 (if (eqb i n) then E1 else (X n))
106 (if (eqb i n) then E2 else (X n))).
107 we proceed by cases ...