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)).
74 (if (eqb i n) then E1 else (X n))
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 ...